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