let p, q be Element of CQC-WFF ; :: thesis: for f being FinSequence of CQC-WFF st |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF ; :: thesis: ( |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> implies |- f ^ <*q*> )
assume A1: ( |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> ) ; :: thesis: |- f ^ <*q*>
set f1 = (f ^ <*('not' p)*>) ^ <*p*>;
A2: ( Ant ((f ^ <*('not' p)*>) ^ <*p*>) = f ^ <*('not' p)*> & Ant (f ^ <*p*>) = f & Suc (f ^ <*p*>) = p ) by CALCUL_1:5;
then ( Ant (f ^ <*p*>) is_Subsequence_of Ant ((f ^ <*('not' p)*>) ^ <*p*>) & Suc (f ^ <*p*>) = Suc ((f ^ <*('not' p)*>) ^ <*p*>) ) by CALCUL_1:5, CALCUL_1:8;
then A3: |- (f ^ <*('not' p)*>) ^ <*p*> by A1, CALCUL_1:36;
set f2 = (f ^ <*('not' p)*>) ^ <*('not' p)*>;
A4: ( Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ <*('not' p)*> & Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = 'not' p ) by CALCUL_1:5;
then A5: (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 1) = 'not' p by FINSEQ_1:59;
(len f) + 1 = (len f) + (len <*('not' p)*>) by FINSEQ_1:56;
then (len f) + 1 = len (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) by A4, FINSEQ_1:35;
then (len f) + 1 in dom (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) by A4, CALCUL_1:10;
then Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) is_tail_of Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A4, A5, CALCUL_1:def 3;
then A6: |- (f ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_1:33;
A7: 0 + 1 <= len ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by CALCUL_1:10;
( Ant ((f ^ <*('not' p)*>) ^ <*p*>) = Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) & 'not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)) = Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) ) by A4, CALCUL_1:5;
then |- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*('not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)))*> by A6, A7, CALCUL_1:3;
then A8: |- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*q*> by A3, CALCUL_1:44;
set f3 = (f ^ <*q*>) ^ <*q*>;
A9: ( Ant ((f ^ <*q*>) ^ <*q*>) = f ^ <*q*> & Suc ((f ^ <*q*>) ^ <*q*>) = q ) by CALCUL_1:5;
then A10: (Ant ((f ^ <*q*>) ^ <*q*>)) . ((len f) + 1) = q by FINSEQ_1:59;
(len f) + 1 = (len f) + (len <*q*>) by FINSEQ_1:56;
then (len f) + 1 = len (Ant ((f ^ <*q*>) ^ <*q*>)) by A9, FINSEQ_1:35;
then (len f) + 1 in dom (Ant ((f ^ <*q*>) ^ <*q*>)) by A9, CALCUL_1:10;
then Suc ((f ^ <*q*>) ^ <*q*>) is_tail_of Ant ((f ^ <*q*>) ^ <*q*>) by A9, A10, CALCUL_1:def 3;
then |- (f ^ <*q*>) ^ <*q*> by CALCUL_1:33;
then |- (f ^ <*(('not' p) 'or' q)*>) ^ <*q*> by A2, A8, CALCUL_1:53;
then |- (f ^ <*('not' (('not' ('not' p)) '&' ('not' q)))*>) ^ <*q*> by QC_LANG2:def 3;
then A11: |- (f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*> by CALCUL_1:48;
set f4 = (f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>;
Suc ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) = ('not' ('not' p)) '&' ('not' q) by CALCUL_1:5;
then A12: ( |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*> & |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*> ) by A11, CALCUL_1:40, CALCUL_1:41;
set f5 = (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>;
set f6 = (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>;
( Ant ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>) = Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) & Suc ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>) = 'not' ('not' p) & 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 CALCUL_1:5;
then |- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*(('not' ('not' p)) '&' ('not' q))*> by A12, CALCUL_1:39;
then |- (f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*> by CALCUL_1:5;
then |- (f ^ <*('not' (('not' ('not' p)) '&' ('not' q)))*>) ^ <*q*> by CALCUL_1:48;
then A13: |- (f ^ <*(('not' p) 'or' q)*>) ^ <*q*> by QC_LANG2:def 3;
1 <= len (f ^ <*(('not' p) 'or' q)*>) by CALCUL_1:10;
then |- (Ant (f ^ <*(('not' p) 'or' q)*>)) ^ <*q*> by A1, A13, CALCUL_1:45;
hence |- f ^ <*q*> by CALCUL_1:5; :: thesis: verum