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