FDL > PVS > Prelude > xor_def : Theory

PVS-2.4 prelude.pvs

 xor_def provides the definition for XOR.  Note that this is not built in
 to the prover, so this definition will need to be expanded in order to use
 it.

xor_def : THEORY
BEGIN

A: VAR bool

B: VAR bool

XOR(A, B): bool = A /= B;

xor def: LEMMA (A XOR B) = IF A THEN NOT B ELSE B ENDIF

END xor_def