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)*>) ^ <*q*> holds
|- (f ^ <*('not' q)*>) ^ <*p*>
let p, q be Element of CQC-WFF Al; for f being FinSequence of CQC-WFF Al st |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- (f ^ <*('not' q)*>) ^ <*p*>
let f be FinSequence of CQC-WFF Al; ( |- (f ^ <*('not' p)*>) ^ <*q*> implies |- (f ^ <*('not' q)*>) ^ <*p*> )
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*>
; |- (f ^ <*('not' q)*>) ^ <*p*>
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; verum