let Al be QC-alphabet ; for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(p => q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
let p, q be Element of CQC-WFF Al; for f being FinSequence of CQC-WFF Al st |- f ^ <*(p => q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; ( |- f ^ <*(p => q)*> & |- f ^ <*p*> implies |- f ^ <*q*> )
assume that
A1:
|- f ^ <*(p => q)*>
and
A2:
|- f ^ <*p*>
; |- f ^ <*q*>
set f3 = (f ^ <*q*>) ^ <*q*>;
set f2 = (f ^ <*('not' p)*>) ^ <*('not' p)*>;
set f1 = (f ^ <*('not' p)*>) ^ <*p*>;
A3:
Ant ((f ^ <*('not' p)*>) ^ <*p*>) = f ^ <*('not' p)*>
by Th5;
Suc (f ^ <*p*>) = p
by Th5;
then A4:
Suc (f ^ <*p*>) = Suc ((f ^ <*('not' p)*>) ^ <*p*>)
by Th5;
A5:
0 + 1 <= len ((f ^ <*('not' p)*>) ^ <*('not' p)*>)
by Th10;
A6:
Ant ((f ^ <*q*>) ^ <*q*>) = f ^ <*q*>
by Th5;
then A7:
(Ant ((f ^ <*q*>) ^ <*q*>)) . ((len f) + 1) = q
by FINSEQ_1:42;
(len f) + 1 = (len f) + (len <*q*>)
by FINSEQ_1:39;
then
(len f) + 1 = len (Ant ((f ^ <*q*>) ^ <*q*>))
by A6, FINSEQ_1:22;
then A8:
(len f) + 1 in dom (Ant ((f ^ <*q*>) ^ <*q*>))
by A6, Th10;
Suc ((f ^ <*q*>) ^ <*q*>) = q
by Th5;
then A9:
|- (f ^ <*q*>) ^ <*q*>
by A7, A8, Lm2, Th33;
A10:
Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ <*('not' p)*>
by Th5;
(len f) + 1 = (len f) + (len <*('not' p)*>)
by FINSEQ_1:39;
then
(len f) + 1 = len (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>))
by A10, FINSEQ_1:22;
then A11:
(len f) + 1 in dom (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>))
by A10, Th10;
A12:
Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = 'not' p
by Th5;
then A13:
'not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)) = Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>)
by Th5;
(Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 1) = 'not' p
by A10, FINSEQ_1:42;
then A14:
|- (f ^ <*('not' p)*>) ^ <*('not' p)*>
by A11, A12, Lm2, Th33;
Ant ((f ^ <*('not' p)*>) ^ <*p*>) = Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)
by A10, Th5;
then A15:
|- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*('not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)))*>
by A14, A5, A13, Th3;
Ant (f ^ <*p*>) = f
by Th5;
then
|- (f ^ <*('not' p)*>) ^ <*p*>
by A2, A3, A4, Th8, Th36;
then
|- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*q*>
by A15, Th44;
then
|- (f ^ <*(('not' p) 'or' q)*>) ^ <*q*>
by A3, A9, Th52;
then A16:
|- (f ^ <*('not' (('not' ('not' p)) '&' ('not' q)))*>) ^ <*q*>
by QC_LANG2:def 3;
set f4 = (f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>;
set f5 = (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*p*>;
set f6 = (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>;
A17:
( Ant ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*p*>) = Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) & Suc ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*p*>) = p )
by Th5;
A18:
( Ant ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>) = Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) & Suc ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>) = 'not' q )
by Th5;
A19:
Suc ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) = ('not' ('not' p)) '&' ('not' q)
by Th5;
then
|- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>
by A16, Th40, Th48;
then A20:
|- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*p*>
by Th54;
|- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>
by A16, A19, Th41, Th48;
then
|- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*(p '&' ('not' q))*>
by A20, A17, A18, Th39;
then
|- (f ^ <*('not' q)*>) ^ <*(p '&' ('not' q))*>
by Th5;
then
|- (f ^ <*('not' (p '&' ('not' q)))*>) ^ <*q*>
by Th48;
then A21:
|- (f ^ <*(p => q)*>) ^ <*q*>
by QC_LANG2:def 2;
1 <= len (f ^ <*(p => q)*>)
by Th10;
then
|- (Ant (f ^ <*(p => q)*>)) ^ <*q*>
by A1, A21, Th45;
hence
|- f ^ <*q*>
by Th5; verum