let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st 1 <= len f & |- f & |- f ^ <*p*> holds
|- (Ant f) ^ <*p*>
let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al st 1 <= len f & |- f & |- f ^ <*p*> holds
|- (Ant f) ^ <*p*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( 1 <= len f & |- f & |- f ^ <*p*> implies |- (Ant f) ^ <*p*> )
assume that
A1: 1 <= len f and
A2: |- f and
A3: |- f ^ <*p*> ; :: thesis: |- (Ant f) ^ <*p*>
set f2 = ((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>;
set f1 = ((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>;
A4: Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>) = (Ant f) ^ <*('not' (Suc f))*> by Th5;
then A5: len (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>)) in dom (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>)) by Th10;
((Ant f) ^ <*('not' (Suc f))*>) . ((len (Ant f)) + 1) = 'not' (Suc f) by FINSEQ_1:42;
then (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>)) . ((len (Ant f)) + 1) = 'not' (Suc f) by Th5;
then (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>)) . ((len (Ant f)) + 1) = Suc (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>) by Th5;
then (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>)) . (len (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>))) = Suc (((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*>) by A4, FINSEQ_2:16;
then A6: |- ((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*> by A5, Lm2, Th33;
set f4 = (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>;
((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*> = (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*('not' (Suc f))*> by Th5;
then A7: ((Ant f) ^ <*('not' (Suc f))*>) ^ <*('not' (Suc f))*> = (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*('not' (Suc (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)))*> by Th5;
( Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>) = (Ant f) ^ <*('not' (Suc f))*> & Suc (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>) = Suc f ) by Th5;
then |- ((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*> by A2, Th8, Th36;
then A8: |- (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*> by A6, A7, Th44;
set f3 = f ^ <*p*>;
1 + 1 <= (len f) + 1 by A1, XREAL_1:6;
then 1 + 1 <= (len f) + (len <*p*>) by FINSEQ_1:39;
then 1 + 1 <= len (f ^ <*p*>) by FINSEQ_1:22;
then A9: 1 < len (f ^ <*p*>) by NAT_1:13;
A10: Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>) = (Ant f) ^ <*('not' (Suc f))*> by Th5;
then Suc (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) = 'not' (Suc f) by Th5;
then Suc (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) = 'not' (Suc (Ant (f ^ <*p*>))) by Th5;
then A11: Suc (Ant ((Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>)) = 'not' (Suc (Ant (f ^ <*p*>))) by Th5;
1 <= len (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) by A10, Th10;
then 1 + 1 <= (len (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>))) + 1 by XREAL_1:6;
then 1 + 1 <= (len (Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>))) + (len <*p*>) by FINSEQ_1:39;
then 1 + 1 <= len ((Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>) by FINSEQ_1:22;
then A12: 1 < len ((Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>) by NAT_1:13;
Ant ((Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>) = Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>) by Th5;
then Ant (Ant ((Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>)) = Ant f by A10, Th5;
then A13: Ant (Ant ((Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>)) = Ant (Ant (f ^ <*p*>)) by Th5;
Suc ((Ant (((Ant f) ^ <*('not' (Suc f))*>) ^ <*(Suc f)*>)) ^ <*p*>) = p by Th5;
then |- (Ant (Ant (f ^ <*p*>))) ^ <*(Suc (f ^ <*p*>))*> by A3, A8, A9, A12, A13, A11, Th5, Th37;
then |- (Ant f) ^ <*(Suc (f ^ <*p*>))*> by Th5;
hence |- (Ant f) ^ <*p*> by Th5; :: thesis: verum