seq_xmpls: THEORY

BEGIN

X, Y: TYPE
A, B, C, D: bool
P, Q, T: PRED[X]
R: [X, Y -> bool]

seq1: THEOREM A OR (A IMPLIES B)

seq2: THEOREM (A IMPLIES B) IFF (NOT A OR B)

seq3: THEOREM ((A AND B) OR (C AND D)) IMPLIES ((A OR C) AND (B OR D))

seq4: THEOREM (EXISTS (x:X): NOT P(x)) OR (FORALL (x:X): P(x))

seq5: THEOREM (EXISTS (y:Y): FORALL (x:X): R(x,y)) IMPLIES
        (FORALL (x:X): EXISTS (y:Y): R(x,y))

seq6: THEOREM ((FORALL (x:X): P(x)) OR (FORALL (x:X): Q(x))) IMPLIES
        (FORALL (x:X): P(x) OR Q(x))

seq7: THEOREM (FORALL (x,y:X): P(x) OR Q(y)) OR (FORALL (y,z:X): Q(y) OR T(z))
         IMPLIES (FORALL (x,y,z:X): P(x) OR Q(y) OR T(z))

END seq_xmpls