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*> holds
|- f ^ <*(p => q)*>
let p, q be Element of CQC-WFF Al; for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*(p => q)*>
let f be FinSequence of CQC-WFF Al; ( |- (f ^ <*p*>) ^ <*q*> implies |- f ^ <*(p => q)*> )
assume A1:
|- (f ^ <*p*>) ^ <*q*>
; |- f ^ <*(p => q)*>
set g1 = ((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>;
set g = (f ^ <*p*>) ^ <*q*>;
A2:
Ant (((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) = (f ^ <*(p '&' ('not' q))*>) ^ <*p*>
by CALCUL_1:5;
Suc ((f ^ <*p*>) ^ <*q*>) = q
by CALCUL_1:5;
then A3:
Suc (((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) = Suc ((f ^ <*p*>) ^ <*q*>)
by CALCUL_1:5;
A4:
Ant ((f ^ <*p*>) ^ <*q*>) = f ^ <*p*>
by CALCUL_1:5;
then A5:
0 + 1 <= len (Ant ((f ^ <*p*>) ^ <*q*>))
by CALCUL_1:10;
A6:
|- (f ^ <*(p '&' ('not' q))*>) ^ <*(p '&' ('not' q))*>
by Th21;
then A7:
|- (f ^ <*(p '&' ('not' q))*>) ^ <*p*>
by Th22;
( Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = f & Suc (Ant ((f ^ <*p*>) ^ <*q*>)) = p )
by A4, CALCUL_1:5;
then
|- ((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>
by A1, A5, A3, A2, CALCUL_1:13, CALCUL_1:36;
then A8:
|- (f ^ <*(p '&' ('not' q))*>) ^ <*q*>
by A7, Th24;
A9:
|- (f ^ <*('not' (p '&' ('not' q)))*>) ^ <*('not' (p '&' ('not' q)))*>
by Th21;
|- (f ^ <*(p '&' ('not' q))*>) ^ <*('not' q)*>
by A6, Th23;
then
|- (f ^ <*(p '&' ('not' q))*>) ^ <*('not' (p '&' ('not' q)))*>
by A8, Th25;
then
|- f ^ <*('not' (p '&' ('not' q)))*>
by A9, Th26;
hence
|- f ^ <*(p => q)*>
by QC_LANG2:def 2; verum