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