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 ^ <*p*>) ^ <*('not' q)*>;
set f2 = (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>;
assume A1: |- (f ^ <*p*>) ^ <*('not' q)*> ; :: thesis:
A2: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> by Th5;
Suc ((f ^ <*p*>) ^ <*('not' q)*>) = 'not' q by Th5;
then A3: Suc ((f ^ <*p*>) ^ <*('not' q)*>) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) by Th5;
A4: Ant ((f ^ <*p*>) ^ <*('not' q)*>) = f ^ <*p*> by Th5;
then A5: Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>)) = f by Th5;
( Suc (Ant ((f ^ <*p*>) ^ <*('not' q)*>)) = p & 0 + 1 <= len (Ant ((f ^ <*p*>) ^ <*('not' q)*>)) ) by A4, Th5, Th10;
then A6: |- (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*> by A1, A2, A3, Th13, Th36;
set f4 = (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>;
set f3 = (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>;
A7: 1 < len ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) by Th9;
A8: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> by Th5;
then A9: 1 < len ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) by Th9;
Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ (<*q*> ^ <*p*>) by A8, FINSEQ_1:32;
then A10: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q,p*> by FINSEQ_1:def 9;
then (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) . ((len f) + 1) = q by A5, Th14;
then A11: (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) . ((len f) + 1) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) by Th5;
1 in dom <*q,p*> by Th14;
then (len f) + 1 in dom (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) by A5, A10, FINSEQ_1:28;
then A12: |- (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*> by A11, Lm2, Th33;
A13: Suc ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) = 'not' p by Th5;
then A14: Suc ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) by Th5;
Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> by Th5;
then A15: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>) by Th5;
Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = 'not' q by Th5;
then A16: Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) = 'not' (Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) by Th5;
A17: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*> by Th5;
then Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ (<*q*> ^ <*('not' p)*>) by FINSEQ_1:32;
then A18: Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q,('not' p)*> by FINSEQ_1:def 9;
then (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 2) = 'not' p by A5, Th14;
then A19: (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 2) = Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>) by Th5;
2 in dom <*q,('not' p)*> by Th14;
then (len f) + 2 in dom (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) by A5, A18, FINSEQ_1:28;
then A20: |- (((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*> by A19, Lm2, Th33;
A21: Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>) = ((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*> by A8, Th5;
then Suc (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>)) = p by Th5;
then A22: 'not' (Suc (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>))) = Suc (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) by A17, Th5;
0 + 1 <= len ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*('not' q)*>) by Th10;
then |- (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' (Suc ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)))*> by A6, A16, A15, Th3;
then A23: |- (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*> by A12, Th44;
A24: Ant (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>)) = (Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*> by A21, Th5;
then Ant (Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*('not' p)*>) ^ <*('not' p)*>)) = Ant (Ant ((Ant ((((Ant (Ant ((f ^ <*p*>) ^ <*('not' q)*>))) ^ <*q*>) ^ <*p*>) ^ <*q*>)) ^ <*('not' p)*>)) by A17, Th5;
hence |- (f ^ <*q*>) ^ <*('not' p)*> by A5, A23, A20, A9, A7, A24, A22, A13, A14, Th37; :: thesis: