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