let Al be QC-alphabet ; 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; 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; ( 1 <= len f & |- f & |- f ^ <*p*> implies |- (Ant f) ^ <*p*> )
assume that
A1:
1 <= len f
and
A2:
|- f
and
A3:
|- f ^ <*p*>
; |- (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; verum