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