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