Fig. 1 Main screen. Display of proof that the AND-operator (&) is commutative.
Fig. 2 Logic menu. The rules of inference.
Fig. 3 Premise form. Used here to enter and verify the premise 'P & Q'.
Fig. 4 Substitution form. Used here to substitute 'a' for 'b' on line 2 of a proof.
Fig. 5 Induction Shortcut form. Used here to prove that, for
all natural numbers x, we have ~x=x+1.
Fig. 6 Subset Axiom form. Used here to select a subset r from
the set u such that x is an element of r if and only if x is not
an element of itself.