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