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