let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*('not' ('not' p))*> holds
|- f ^ <*p*>
let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*('not' ('not' p))*> holds
|- f ^ <*p*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( |- f ^ <*('not' ('not' p))*> implies |- f ^ <*p*> )
assume A1: |- f ^ <*('not' ('not' p))*> ; :: thesis: |- f ^ <*p*>
set f5 = f ^ <*('not' ('not' p))*>;
set f4 = ((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>;
set f2 = ((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>;
set f1 = ((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>;
set f3 = (Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>;
A2: Suc (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = 'not' p by Th5;
A3: Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = (f ^ <*('not' ('not' p))*>) ^ <*('not' p)*> by Th5;
then A4: 1 < len ((Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>) by Th9;
Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ (<*('not' ('not' p))*> ^ <*('not' p)*>) by A3, FINSEQ_1:32;
then A5: Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ <*('not' ('not' p)),('not' p)*> by FINSEQ_1:def 9;
(len f) + 2 = (len f) + (len <*('not' ('not' p)),('not' p)*>) by FINSEQ_1:44;
then (len f) + 2 = len (Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) by A5, FINSEQ_1:22;
then A6: (len f) + 2 in dom (Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) by A3, Th10;
(Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 2) = 'not' p by A5, Th14;
then A7: |- ((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*> by A2, A6, Lm2, Th33;
A8: 1 < len (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>) by Th9;
A9: Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>) = (f ^ <*('not' ('not' p))*>) ^ <*('not' p)*> by Th5;
then Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>) = f ^ (<*('not' ('not' p))*> ^ <*('not' p)*>) by FINSEQ_1:32;
then A10: Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>) = f ^ <*('not' ('not' p)),('not' p)*> by FINSEQ_1:def 9;
(len f) + 2 = (len f) + (len <*('not' ('not' p)),('not' p)*>) by FINSEQ_1:44;
then (len f) + 2 = len (Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>)) by A10, FINSEQ_1:22;
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:6;
then A11: (len f) + 1 in dom (Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>)) by FINSEQ_3:25;
0 + 1 <= len (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>) by Th10;
then A12: ((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;
A13: 1 <= len (f ^ <*('not' ('not' p))*>) by Th10;
A14: Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>) = (f ^ <*('not' ('not' p))*>) ^ <*p*> by Th5;
then Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>) = f ^ (<*('not' ('not' p))*> ^ <*p*>) by FINSEQ_1:32;
then A15: Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>) = f ^ <*('not' ('not' p)),p*> by FINSEQ_1:def 9;
A16: Ant ((Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>) = Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>) by Th5;
then Suc (Ant ((Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>)) = 'not' p by A3, Th5;
then A17: Suc (Ant ((Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>)) = 'not' (Suc (Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>))) by A14, Th5;
(len f) + 2 = (len f) + (len <*('not' ('not' p)),p*>) by FINSEQ_1:44;
then (len f) + 2 = len (Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>)) by A15, FINSEQ_1:22;
then A18: (len f) + 2 in dom (Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>)) by A14, Th10;
A19: Suc (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>) = 'not' ('not' p) by Th5;
then A20: 'not' (Suc (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) = Suc (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>) by Th5;
(Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>)) . ((len f) + 1) = 'not' ('not' p) by A10, Th14;
then A21: |- ((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*> by A11, A19, Lm2, Th33;
A22: Suc (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>) = p by Th5;
then A23: Suc ((Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>) = Suc (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>) by Th5;
(Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>)) . ((len f) + 2) = p by A15, Th14;
then A24: |- ((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*> by A18, A22, Lm2, Th33;
Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' ('not' p))*>) by A9, Th5;
then A25: |- (Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*> by A7, A21, A12, A20, Th44;
A26: Ant (Ant ((Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>)) = f ^ <*('not' ('not' p))*> by A3, A16, Th5;
then Ant (Ant ((Ant (((f ^ <*('not' ('not' p))*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) ^ <*p*>)) = Ant (Ant (((f ^ <*('not' ('not' p))*>) ^ <*p*>) ^ <*p*>)) by A14, Th5;
then |- (f ^ <*('not' ('not' p))*>) ^ <*p*> by A25, A22, A24, A23, A26, A17, A4, A8, Th37;
then |- (Ant (f ^ <*('not' ('not' p))*>)) ^ <*p*> by A1, A13, Th45;
hence |- f ^ <*p*> by Th5; :: thesis: verum