let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f & |- (Ant f) ^ <*('not' (Suc f))*> holds
|- (Ant f) ^ <*p*>
let p be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al st |- f & |- (Ant f) ^ <*('not' (Suc f))*> holds
|- (Ant f) ^ <*p*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( |- f & |- (Ant f) ^ <*('not' (Suc f))*> implies |- (Ant f) ^ <*p*> )
assume that
A1: |- f and
A2: |- (Ant f) ^ <*('not' (Suc f))*> ; :: thesis: |- (Ant f) ^ <*p*>
set f1 = ((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>;
( Ant (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>) = (Ant f) ^ <*('not' p)*> & Suc f = Suc (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>) ) by Th5;
then A3: |- ((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*> by A1, Th8, Th36;
set f3 = ((Ant f) ^ <*('not' p)*>) ^ <*('not' (Suc f))*>;
set f2 = (Ant f) ^ <*('not' (Suc f))*>;
Suc ((Ant f) ^ <*('not' (Suc f))*>) = 'not' (Suc f) by Th5;
then A4: Suc ((Ant f) ^ <*('not' (Suc f))*>) = Suc (((Ant f) ^ <*('not' p)*>) ^ <*('not' (Suc f))*>) by Th5;
( Ant (((Ant f) ^ <*('not' p)*>) ^ <*('not' (Suc f))*>) = (Ant f) ^ <*('not' p)*> & Ant ((Ant f) ^ <*('not' (Suc f))*>) = Ant f ) by Th5;
then A5: |- ((Ant f) ^ <*('not' p)*>) ^ <*('not' (Suc f))*> by A2, A4, Th8, Th36;
Suc (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>) = Suc f by Th5;
then A6: 'not' (Suc (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>)) = Suc (((Ant f) ^ <*('not' p)*>) ^ <*('not' (Suc f))*>) by Th5;
A7: 1 < len (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>) by Th9;
A8: Ant (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>) = (Ant f) ^ <*('not' p)*> by Th5;
then ( Ant (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>) = Ant (((Ant f) ^ <*('not' p)*>) ^ <*('not' (Suc f))*>) & Suc (Ant (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>)) = 'not' p ) by Th5;
then |- (Ant (Ant (((Ant f) ^ <*('not' p)*>) ^ <*(Suc f)*>))) ^ <*p*> by A3, A5, A6, A7, Th38;
hence |- (Ant f) ^ <*p*> by A8, Th5; :: thesis: verum