let p, q be Element of CQC-WFF ; :: thesis: for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*('not' q)*> holds
|- (f ^ <*q*>) ^ <*('not' p)*>
let f be FinSequence of CQC-WFF ; :: thesis: ( |- (f ^ <*p*>) ^ <*('not' q)*> implies |- (f ^ <*q*>) ^ <*('not' p)*> )
set f1 = (f ^ <*p*>) ^ <*('not' q)*>;
set f2 = (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>;
assume A1: |- (f ^ <*p*>) ^ <*('not' q)*> ; :: thesis: |- (f ^ <*q*>) ^ <*('not' p)*>
A2: ( Ant ((f ^ <*p*>) ^ <*('not' q)*>) = f ^ <*p*> & Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> ) by Th5;
then A3: ( Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>)) = f & Suc (Ant ((f ^ <*p*>) ^ <*('not' q)*>)) = p & Suc ((f ^ <*p*>) ^ <*('not' q)*>) = 'not' q ) by Th5;
then A4: Suc ((f ^ <*p*>) ^ <*('not' q)*>) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) by Th5;
0 + 1 <= len (Ant ((f ^ <*p*>) ^ <*('not' q)*>)) by A2, Th10;
then A5: |- (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*> by A1, A2, A3, A4, Th13, Th36;
set f3 = (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>;
A6: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> by Th5;
then Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ (<*q*> ^ <*p*>) by FINSEQ_1:45;
then A7: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q,p*> by FINSEQ_1:def 9;
then (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) . ((len f) + 1) = q by A3, Th14;
then A8: (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) . ((len f) + 1) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) by Th5;
1 in dom <*q,p*> by Th14;
then (len f) + 1 in dom (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) by A3, A7, FINSEQ_1:41;
then Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) is_tail_of Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) by A8, Def3;
then A9: |- (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*> by Th33;
( Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = 'not' q & Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> ) by Th5;
then A10: ( Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = 'not' (Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) & Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) ) by Th5;
0 + 1 <= len ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) by Th10;
then |- (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' (Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)))*> by A5, A10, Th3;
then A11: |- (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*> by A9, Th44;
set f4 = (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>;
A12: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*> by Th5;
then Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ (<*q*> ^ <*('not' p)*>) by FINSEQ_1:45;
then A13: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q,('not' p)*> by FINSEQ_1:def 9;
then (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 2) = 'not' p by A3, Th14;
then A14: (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 2) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) by Th5;
2 in dom <*q,('not' p)*> by Th14;
then (len f) + 2 in dom (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) by A3, A13, FINSEQ_1:41;
then Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) is_tail_of Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) by A14, Def3;
then A15: |- (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*> by Th33;
A16: ( 1 < len ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) & 1 < len ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) ) by A6, Th9;
A17: Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> by A6, Th5;
then A18: Ant (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>)) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*> by Th5;
then A19: Ant (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) = Ant (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>)) by A12, Th5;
Suc (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>)) = p by A17, Th5;
then A20: 'not' (Suc (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>))) = Suc (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) by A12, Th5;
A21: Suc ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) = 'not' p by Th5;
then Suc ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) by Th5;
hence |- (f ^ <*q*>) ^ <*('not' p)*> by A3, A11, A15, A16, A18, A19, A20, A21, Th37; :: thesis: verum