let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P
let s be State of SCM+FSA; :: thesis: for I being good parahalting Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P
let I be good parahalting Program of SCM+FSA; :: thesis: for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P
let a be read-write Int-Location; :: thesis: ( not I destroys a & s . (intloc 0) = 1 & s . a > 0 implies loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P )
set I2 = if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))));
reconsider I1 = I ";" (SubFrom (a,(intloc 0))) as parahalting Program of SCM+FSA ;
set i = a =0_goto ((card I1) + 3);
defpred S₁[ Nat] means for s being State of SCM+FSA st s . (intloc 0) = 1 & s . a = $1 & s . a > 0 holds
( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize s),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) . a = (s . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize s),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize s))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize s),k)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize s),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) ) );
assume A1: not I destroys a ; :: thesis: ( not s . (intloc 0) = 1 or not s . a > 0 or loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P )
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
let ss be State of SCM+FSA; :: thesis: ( ss . (intloc 0) = 1 & ss . a = k + 1 & ss . a > 0 implies ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),k)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) ) ) )
assume A4: ss . (intloc 0) = 1 ; :: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),k)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) ) ) )
set s2 = Initialize ss;
set P2 = P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))));
set s1 = Initialize ss;
set P1 = P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))));
A5: loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) c= P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by FUNCT_4:25;
assume A6: ss . a = k + 1 ; :: thesis: ( not ss . a > 0 or ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),k)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) ) ) )
set s3 = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1));
set P3 = P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))));
assume A7: ss . a > 0 ; :: thesis: ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 & ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),k)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) ) )
A8: Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)) = Following ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss)))))) by EXTPRO_1:3;
A9: I1 is_halting_on ss,P by SCMFSA7B:19;
A10: I1 is_closed_on ss,P by SCMFSA7B:18;
then A11: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A7, A9, SCMFSA8B:15;
A12: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_halting_on ss,P by A7, A10, A9, SCMFSA8B:15;
A13: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A7, A10, A9, SCMFSA8B:15;
then A14: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) = (Exec ((goto 0),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))))))) . (IC ) by A12, A8, Lm1
.= 0 by SCMFSA_2:69 ;
A15: Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)) = Exec ((goto 0),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss)))))) by A13, A12, A8, Lm1;

A16: now :: thesis: ( 0 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & (card I1) + 3 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & intloc 0 in dom ss & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 )

A17: I1 is_halting_on Initialized ss,P by SCMFSA7B:19;
A18: I1 is_closed_on Initialized ss,P by SCMFSA7B:18;
IExec ((if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))),P,ss) = (IExec (I1,P,ss)) +* (Start-At ((((card (Goto 2)) + (card I1)) + 3),SCM+FSA)) by A7, A17, A18, SCMFSA8B:16;
then A19: (IExec ((if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))),P,ss)) . a = (IExec (I1,P,ss)) . a by SCMFSA_3:3;
A20: card (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) = ((card (Goto 2)) + (card I1)) + 4 by SCMFSA8B:11
.= ((card I1) + 1) + 4 by SCMFSA8A:15
.= ((card I1) + 3) + 2 ;
A21: card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) = card (dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))))
.= card (dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by FUNCT_4:99
.= card (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) ;

hereby :: thesis: ( intloc 0 in dom ss & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 )

thus 0 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A21, AFINSQ_1:66; :: thesis: (card I1) + 3 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))
((card I1) + 3) + (1 + 1) = (((card I1) + 3) + 1) + 1 ;
then ((card I1) + 3) + 1 < card (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by A20, NAT_1:13;
then (card I1) + 3 < card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A21, NAT_1:13;
hence (card I1) + 3 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by AFINSQ_1:66; :: thesis: verum

end;

thus intloc 0 in dom ss by SCMFSA_2:42; :: thesis: ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 )
then A22: ss +* ((intloc 0) .--> 1) = ss by A4, FUNCT_7:109;
A23: I1 is_closed_on Initialized ss,P by SCMFSA7B:18;
A24: I1 is_halting_on Initialized ss,P by SCMFSA7B:19;
A25: (Initialized ss) . a > 0 by A7, SCMFSA_M:37;
then A26: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_halting_on Initialized ss,P by A23, A24, SCMFSA8B:15;
A27: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_on Initialized ss,P by A25, A23, A24, SCMFSA8B:15;
consider Is being State of SCM+FSA such that
A28: Is = Initialize (Initialized ss) ;
set IP = P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))));
A29: Initialize (Initialized ss) = Initialize (Initialized ss)
.= ((ss +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= Initialize ss by A22
.= Initialize ss ;

A30: now :: thesis: for b being Int-Location holds (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . b = (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . b

let b be Int-Location; :: thesis: (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . b = (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . b
A31: Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is))) = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is))) by A12, A11, A29, A28, Th76;
(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . b = (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))))) . b by A15, SCMFSA_2:69;
hence (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . b = (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . b by A29, A28, A31; :: thesis: verum

end;

then (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . a
.= (IExec ((if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))),P,ss)) . a by A28, A26, Th58 ;
hence (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (Comput ((P +* I1),((Initialized ss) +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I1),(Initialize (Initialized ss)))))) . a by A17, A19, Th58
.= (ss . a) - 1 by A1, Th69 ;
:: thesis: (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1
A32: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is good by Th82;
(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . (intloc 0) by A30
.= 1 by A28, A26, A27, A32, Th67 ;
hence (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 ; :: thesis: verum

end;

hence ( (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . a = (ss . a) - 1 & (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) . (intloc 0) = 1 ) ; :: thesis: ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),k)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) )

A33: now :: thesis: ( (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . 0 = a =0_goto ((card I1) + 3) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . 0 <> halt SCM+FSA & 0 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) )

A34: (Macro (a =0_goto ((card I1) + 3))) . 0 <> halt SCM+FSA by COMPOS_1:58;
A35: 0 in dom (Macro (a =0_goto ((card I1) + 3))) by COMPOS_1:60;
if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) = ((((a =0_goto ((card I1) + 3)) ";" I1) ";" (Goto ((card (Goto 2)) + 1))) ";" (Goto 2)) ";" (Stop SCM+FSA) by SCMFSA8B:def 1
.= (((a =0_goto ((card I1) + 3)) ";" (I1 ";" (Goto ((card (Goto 2)) + 1)))) ";" (Goto 2)) ";" (Stop SCM+FSA) by SCMFSA6A:29
.= ((a =0_goto ((card I1) + 3)) ";" ((I1 ";" (Goto ((card (Goto 2)) + 1))) ";" (Goto 2))) ";" (Stop SCM+FSA) by SCMFSA6A:29
.= (a =0_goto ((card I1) + 3)) ";" (((I1 ";" (Goto ((card (Goto 2)) + 1))) ";" (Goto 2)) ";" (Stop SCM+FSA)) by SCMFSA6A:29
.= (Macro (a =0_goto ((card I1) + 3))) ";" (((I1 ";" (Goto ((card (Goto 2)) + 1))) ";" (Goto 2)) ";" (Stop SCM+FSA)) ;
hence (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . 0 = (Macro (a =0_goto ((card I1) + 3))) . 0 by A35, A34, SCMFSA6A:15
.= a =0_goto ((card I1) + 3) by COMPOS_1:58 ;
:: thesis: ( (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . 0 <> halt SCM+FSA & 0 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) )
hence (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . 0 <> halt SCM+FSA ; :: thesis: ( 0 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) )
A36: card (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) = ((card (Goto 2)) + (card I1)) + 4 by SCMFSA8B:11
.= ((card I1) + 1) + 4 by SCMFSA8A:15
.= ((card I1) + 3) + 2 ;
hence 0 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by AFINSQ_1:66; :: thesis: ( (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) & (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) )
card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) = card (dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))))
.= card (dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by FUNCT_4:99
.= card (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) ;
then card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) = (card I1) + (3 + 2) by A36;
hence (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) = goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by Th83; :: thesis: ( (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) )
hence (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) . ((card I1) + 3) <> halt SCM+FSA ; :: thesis: (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))

hereby :: thesis: verum

((card I1) + 3) + 0 < card (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by A36, XREAL_1:6;
hence (card I1) + 3 in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by AFINSQ_1:66; :: thesis: verum

end;

end;

hereby :: thesis: verum

per cases ( k = 0 or k > 0 ) ;

suppose A37: k = 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) )

take m = (((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1) + 1; :: thesis: ( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) )
A38: CurInstr ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) = (P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) . 0 by A14, PBOOLE:143
.= (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . 0 by A16, A5, GRFUNC_1:2
.= a =0_goto ((card I1) + 3) by A33, FUNCT_4:105 ;
A39: (P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) /. (IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) = (P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) . (IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) by PBOOLE:143;
A40: Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)) = Following ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) by EXTPRO_1:3
.= Exec ((a =0_goto ((card I1) + 3)),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) by A38 ;
then A41: CurInstr ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) = (P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) . ((card I1) + 3) by A39, A6, A16, A37, SCMFSA_2:70
.= (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . ((card I1) + 3) by A16, A5, GRFUNC_1:2
.= goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by A33, FUNCT_4:105 ;
Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),m) = Following ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) by EXTPRO_1:3
.= Exec ((goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),(((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1)))) by A41 ;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by SCMFSA_2:69; :: thesis: for n being Element of NAT st n < m holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < m implies IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) )
assume n < m ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))
then n <= ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 by NAT_1:13;
then A42: ( n <= (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 or n = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 ) by NAT_1:8;

per cases ( n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss)) or n = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 or n = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 ) by A42, NAT_1:8;

suppose A43: n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss)) ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))

A44: I1 is_halting_on ss,P by SCMFSA7B:19;
A45: I1 is_closed_on ss,P by SCMFSA7B:18;
then A46: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A7, A44, SCMFSA8B:15;
if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_halting_on ss,P by A7, A45, A44, SCMFSA8B:15;
then Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss),n) = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n) by A43, A46, Th76;
then A47: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) = IC (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) ;
IC (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by A46, SCMFSA7B:def 6;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A47, FUNCT_4:99; :: thesis: verum

end;

suppose n = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))

hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A14, A16; :: thesis: verum

end;

suppose n = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + 1 ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))

hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A6, A16, A37, A40, SCMFSA_2:70; :: thesis: verum

end;

end;

end;

end;

suppose A48: k > 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) )

consider Is3 being State of SCM+FSA such that
A49: Is3 = Initialized (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) ;
A50: Initialize (Initialized (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) = (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) +* ((IC ) .--> 0) by A14, A16, SCMFSA_M:8;
A51: Is3 . (intloc 0) = 1 by A49, SCMFSA_M:9;
Is3 . a = k by A6, A16, A49, SCMFSA_M:37;
then consider m0 being Element of NAT such that
A52: IC (Comput (((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize Is3),m0)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) and
A53: for n being Element of NAT st n < m0 holds
IC (Comput (((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize Is3),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A3, A48, A51;
take m = ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) + m0; :: thesis: ( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < m holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) )
A54: IC in dom (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) by MEMSTR_0:2;
A55: Initialize (Initialized (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)))) = (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) +* ((IC ) .--> 0) by A50
.= (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))) +* (Start-At (0,SCM+FSA))
.= Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1)) by A14, A54, FUNCT_7:109 ;
thus IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A49, A52, A55, EXTPRO_1:4; :: thesis: for n being Element of NAT st n < m holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < m implies IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) )
assume A56: n < m ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))
A57: I1 is_halting_on ss,P by SCMFSA7B:19;
A58: I1 is_closed_on ss,P by SCMFSA7B:18;
then A59: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_on ss,P by A7, A57, SCMFSA8B:15;
A60: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_halting_on ss,P by A7, A58, A57, SCMFSA8B:15;

per cases ( n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss)) or (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 <= n ) by NAT_1:13;

suppose n <= LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss)) ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))

then Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss),n) = Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n) by A59, A60, Th76;
then A61: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) = IC (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) ;
IC (Comput ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss),n)) in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by A59, SCMFSA7B:def 6;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A61, FUNCT_4:99; :: thesis: verum

end;

suppose A62: (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1 <= n ; :: thesis: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),b₁)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))

consider mm being Element of NAT such that
A63: mm = n -' ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) ;
n - ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) >= 0 by A62, XREAL_1:48;
then A64: mm = n - ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) by A63, XREAL_0:def 2;
mm + ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) = n by A62, A63, XREAL_1:235;
then A65: IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) = IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1))),mm)) by EXTPRO_1:4;
m0 = m - ((LifeSpan ((P +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialize ss))) + 1) ;
then mm < m0 by A56, A64, XREAL_1:9;
hence IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A49, A53, A55, A65; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

assume A66: s . (intloc 0) = 1 ; :: thesis: ( not s . a > 0 or loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P )
assume A67: s . a > 0 ; :: thesis: loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P
then reconsider sa = s . a as Element of NAT by INT_1:3;
A68: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A68, A2);
then S₁[sa] ;
then ex k being Element of NAT st
( IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize s),k)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) & ( for n being Element of NAT st n < k holds
IC (Comput ((P +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialize s),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) ) ) by A66, A67;
hence loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P by SCMFSA8A:def 2; :: thesis: verum