An expression defined by cases is of the form if P then TelseU, which takes the value T if the
proposition P is true and the value U if the proposition P is
false. This is the notation we will use in this section: the Watson
P || T , U.
Any term may appear in the role of P; we adopt Frege's convention that any object not equal to the truth value true is understood to play the role of the truth value false where a proposition is expected. We refer to P as the hypothesis of the expression, and to T and U as its branches (positive and negative, respectively).
We present the axioms of definition by cases supported by Watson. Notice that equality appears as a term-forming operation as well as in the role of a predicate here; it should be clear what is meant by each instance of the symbol once this is understood.
U = if false then Telse U.
(true = false) = false.
These axioms, together with the axioms of equational reasoning above, are sufficient to interpret the logic of propositional connectives and identity. This has been demonstrated using the prover; it is also explained in an unpublished paper  of Holmes available on the Web.
This logic of case expressions will probably not be familiar to the reader, but it should at least be clear that the axioms are true. To see that they are sufficient to support propositional logic and the logic of identity requires a little work.