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) 'or' 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 ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; ( |- f ^ <*(('not' p) 'or' q)*> & |- f ^ <*p*> implies |- f ^ <*q*> )
assume that
A1:
|- f ^ <*(('not' p) 'or' q)*>
and
A2:
|- f ^ <*p*>
; |- f ^ <*q*>
set f1 = (f ^ <*('not' p)*>) ^ <*p*>;
A3:
Ant ((f ^ <*('not' p)*>) ^ <*p*>) = f ^ <*('not' p)*>
by CALCUL_1:5;
A4:
Ant (f ^ <*p*>) = f
by CALCUL_1:5;
Suc (f ^ <*p*>) = p
by CALCUL_1:5;
then
Suc (f ^ <*p*>) = Suc ((f ^ <*('not' p)*>) ^ <*p*>)
by CALCUL_1:5;
then A5:
|- (f ^ <*('not' p)*>) ^ <*p*>
by A2, A3, A4, CALCUL_1:8, CALCUL_1:36;
set f2 = (f ^ <*('not' p)*>) ^ <*('not' p)*>;
A6:
Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ <*('not' p)*>
by CALCUL_1:5;
A7:
Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = 'not' p
by CALCUL_1:5;
A8:
(Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 1) = 'not' p
by A6, FINSEQ_1:42;
(len f) + 1 = (len f) + (len <*('not' p)*>)
by FINSEQ_1:39;
then
(len f) + 1 = len (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>))
by A6, FINSEQ_1:22;
then
(len f) + 1 in dom (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>))
by A6, CALCUL_1:10;
then
Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) is_tail_of Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)
by A7, A8, CALCUL_1:def 16;
then A9:
|- (f ^ <*('not' p)*>) ^ <*('not' p)*>
by CALCUL_1:33;
A10:
0 + 1 <= len ((f ^ <*('not' p)*>) ^ <*('not' p)*>)
by CALCUL_1:10;
A11:
Ant ((f ^ <*('not' p)*>) ^ <*p*>) = Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)
by A6, CALCUL_1:5;
'not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)) = Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>)
by A7, CALCUL_1:5;
then
|- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*('not' (Suc ((f ^ <*('not' p)*>) ^ <*p*>)))*>
by A9, A10, A11, CALCUL_1:3;
then A12:
|- (Ant ((f ^ <*('not' p)*>) ^ <*p*>)) ^ <*q*>
by A5, CALCUL_1:44;
set f3 = (f ^ <*q*>) ^ <*q*>;
A13:
Ant ((f ^ <*q*>) ^ <*q*>) = f ^ <*q*>
by CALCUL_1:5;
A14:
Suc ((f ^ <*q*>) ^ <*q*>) = q
by CALCUL_1:5;
A15:
(Ant ((f ^ <*q*>) ^ <*q*>)) . ((len f) + 1) = q
by A13, FINSEQ_1:42;
(len f) + 1 = (len f) + (len <*q*>)
by FINSEQ_1:39;
then
(len f) + 1 = len (Ant ((f ^ <*q*>) ^ <*q*>))
by A13, FINSEQ_1:22;
then
(len f) + 1 in dom (Ant ((f ^ <*q*>) ^ <*q*>))
by A13, CALCUL_1:10;
then
Suc ((f ^ <*q*>) ^ <*q*>) is_tail_of Ant ((f ^ <*q*>) ^ <*q*>)
by A14, A15, CALCUL_1:def 16;
then
|- (f ^ <*q*>) ^ <*q*>
by CALCUL_1:33;
then
|- (f ^ <*(('not' p) 'or' q)*>) ^ <*q*>
by A3, A12, CALCUL_1:53;
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))*>;
A17:
Suc ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>) = ('not' ('not' p)) '&' ('not' q)
by CALCUL_1:5;
then A18:
|- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>
by A16, CALCUL_1:40, CALCUL_1:48;
A19:
|- (Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>
by A16, A17, CALCUL_1:41, CALCUL_1:48;
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)*>;
A20:
Ant ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>) = Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)
by CALCUL_1:5;
A21:
Suc ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' ('not' p))*>) = 'not' ('not' p)
by CALCUL_1:5;
A22:
Ant ((Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)) ^ <*('not' q)*>) = Ant ((f ^ <*('not' q)*>) ^ <*(('not' ('not' p)) '&' ('not' q))*>)
by CALCUL_1:5;
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 A18, A19, A20, A21, A22, 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 A23:
|- (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, A23, CALCUL_1:45;
hence
|- f ^ <*q*>
by CALCUL_1:5; verum