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

proof

A3: now :: thesis:

hereby :: thesis:

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

end;

let k be Element of NAT ; :: thesis:
assume A6: S₁[k] ; :: thesis:
let ss be State of SCM+FSA; :: thesis:
let pp be Instruction-Sequence of SCM+FSA; :: thesis:
assume ss . (intloc 0) = 1 ; :: thesis:
set s2 = Initialized ss;
set p2 = pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))));
A7: loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) c= pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by FUNCT_4:25;
set s1 = Initialized ss;
set p1 = pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))));
assume A8: ss . a = k + 1 ; :: thesis:
A9: Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)) = Following ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss)))))) by EXTPRO_1:3
.= Exec ((CurInstr ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss)))))) ;
set s3 = Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1));
set p3 = pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))));
assume A10: ss . a > 0 ; :: thesis:
A11: ( I1 is_closed_onInit ss,pp & I1 is_halting_onInit ss,pp ) by Th25, Th26;
then A12: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_halting_onInit ss,pp by A10, Th35;
if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_onInit ss,pp by A10, A11, Th35;
then A13: Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)) = Exec ((goto 0),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss)))))) by A12, A9, Th59;
A14: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_onInit ss,pp by A10, A11, Th35;
A15: 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 ;
A16: 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)))))))) by CARD_1:62
.= 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)))))) by CARD_1:62 ;

A17: now :: thesis:

A18: I1 is_halting_onInit ss,pp by Th26;
then A19: I1 is_halting_on Initialized ss,pp by Th31;
I1 is_closed_onInit ss,pp by Th25;
then IExec ((if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))),pp,ss) = (IExec (I1,pp,ss)) +* (Start-At ((((card (Goto 2)) + (card I1)) + 3),SCM+FSA)) by A10, A18, Th36;
then A20: (IExec ((if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))),pp,ss)) . a = (IExec (I1,pp,ss)) . a by SCMFSA_3:3;

hereby :: thesis:

thus 0 in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A16, A15, AFINSQ_1:66; :: thesis:
((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 A15, NAT_1:13;
then (card I1) + 3 < card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A16, 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:

end;

consider Is being State of SCM+FSA such that
A21: Is = Initialized (Initialized ss) ;
A22: Is = (Initialized ss) +* ((Initialize ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) by A21, FUNCT_4:93
.= ((Initialized ss) +* (Initialize ((intloc 0) .--> 1))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= Initialize (Initialized ss) by FUNCT_4:93 ;
I1 is_closed_onInit ss,pp by Th25;
then A23: I1 is_closed_on Initialized ss,pp by Th30;
I1 is_halting_onInit ss,pp by Th26;
then A24: I1 is_halting_on Initialized ss,pp by Th31;
A25: (Initialized ss) . a > 0 by A10, SCMFSA_M:37;
then A26: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_halting_on Initialized ss,pp by A23, A24, SCMFSA8B:15;
thus Initialized (Initialized ss) = Initialized ss ; :: thesis:

A27: now :: thesis:

let b be Int-Location; :: thesis:
(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . b = (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))))) . b by A13, SCMFSA_2:69;
hence (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . b = (Comput ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . b by A21, A12, A14, Th57; :: thesis:

end;

then (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (Comput ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . a
.= (IExec ((if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))),pp,ss)) . a by A26, A22, SCMFSA8C:58 ;
hence (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (Comput ((pp +* I1),(Initialize (Initialized ss)),(LifeSpan ((pp +* I1),(Initialize (Initialized ss)))))) . a by A19, A20, SCMFSA8C:58
.= (ss . a) - 1 by A1, Th54 ;
:: thesis:
A28: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_on Initialized ss,pp by A25, A23, A24, SCMFSA8B:15;
(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = (Comput ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is,(LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),Is)))) . (intloc 0) by A27
.= 1 by A26, A28, A22, SCMFSA8C:67 ;
hence (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 ; :: thesis:

end;

hence ( (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . a = (ss . a) - 1 & (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) . (intloc 0) = 1 ) ; :: thesis:
A29: IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) = 0 by A13, SCMFSA_2:69;

per cases ;

suppose A30: k = 0 ; :: thesis:

take m = (((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1) + 1; :: thesis:
A31: CurInstr ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) = (pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) . 0 by A29, PBOOLE:143
.= (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . 0 by A17, A7, GRFUNC_1:2
.= a =0_goto ((card I1) + 3) by A3, FUNCT_4:105 ;
A32: Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)) = Following ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) by EXTPRO_1:3
.= Exec ((a =0_goto ((card I1) + 3)),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) by A31 ;
then IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1))) = (card I1) + 3 by A8, A17, A30, SCMFSA_2:70;
then A33: CurInstr ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)))) = (pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) . ((card I1) + 3) by PBOOLE:143
.= (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) . ((card I1) + 3) by A17, A7, GRFUNC_1:2
.= goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) by A3, FUNCT_4:105 ;
Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),m) = Following ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)))) by EXTPRO_1:3
.= Exec ((goto (card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))))),(Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),(((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1)))) by A33 ;
hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by SCMFSA_2:69; :: thesis:

hereby :: thesis:

let n be Element of NAT ; :: thesis:
assume n < m ; :: thesis:
then n <= ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1 by NAT_1:13;
then A34: ( n <= (LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1 or n = ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1 ) by NAT_1:8;

per cases by A34, NAT_1:8;

suppose A35: n <= LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss)) ; :: thesis:

end;

suppose n = (LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1 ; :: thesis:

hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A13, A17, SCMFSA_2:69; :: thesis:

end;

suppose n = ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + 1 ; :: thesis:

end;

suppose A39: k > 0 ; :: thesis:

consider Is3 being State of SCM+FSA such that
A40: Is3 = Initialized (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1))) ;
consider m0 being Element of NAT such that
A41: IC (Comput (((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Is3 +* (Initialize ((intloc 0) .--> 1))),m0)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) and
A42: for n being Element of NAT st n < m0 holds
IC (Comput (((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))) +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized Is3),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A6, A39, A8, A17, A40;
take m = ((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1) + m0; :: thesis:
A43: Initialized (Initialized (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)))) = Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),((LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1)) by A29, A17, SCMFSA_M:8;
thus IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),m)) = card (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A40, A41, A43, EXTPRO_1:4; :: thesis:

hereby :: thesis:

let n be Element of NAT ; :: thesis:
assume A44: n < m ; :: thesis:
A45: ( I1 is_closed_onInit ss,pp & I1 is_halting_onInit ss,pp ) by Th25, Th26;
then A46: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_closed_onInit ss,pp by A10, Th35;
A47: if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))) is_halting_onInit ss,pp by A10, A45, Th35;

per cases by NAT_1:13;

suppose n <= LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss)) ; :: thesis:

then A48: IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) = IC (Comput ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss),n)) by A46, A47, Th57;
IC (Comput ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss),n)) in dom (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) by A46, Def4;
hence IC (Comput ((pp +* (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))))),(Initialized ss),n)) in dom (loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))) by A48, FUNCT_4:99; :: thesis:

end;

suppose A49: (LifeSpan ((pp +* (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0))))))),(Initialized ss))) + 1 <= n ; :: thesis:

end;

assume A53: s . (intloc 0) = 1 ; :: thesis:
assume A54: s . a > 0 ; :: thesis:
then reconsider sa = s . a as Element of NAT by INT_1:3;
A55: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A55, A2);
then A56: S₁[sa] ;
A57: dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
IC <> intloc 0 by SCMFSA_2:56;
then not intloc 0 in dom (Start-At (0,SCM+FSA)) by A57, TARSKI:def 1;
then A58: (Initialize s) . (intloc 0) = 1 by A53, FUNCT_4:11;
IC in dom (Start-At (0,SCM+FSA)) by A57, TARSKI:def 1;
then A59: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then A60: dom (Start-At (0,SCM+FSA)) misses dom ((intloc 0) .--> 1) by A57, SCMFSA_2:56, ZFMISC_1:11;
Initialized s = s +* ((Start-At (0,SCM+FSA)) +* ((intloc 0) .--> 1)) by A60, FUNCT_4:35
.= (Initialize s) +* ((intloc 0) .--> 1) by FUNCT_4:14
.= ((Initialize s) +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) by A60, FUNCT_4:115
.= Initialized (Initialize s) by FUNCT_4:14
.= Initialize s by A58, A59, SCMFSA_M:8 ;
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 A56, A53, A54;
hence loop (if=0 (a,(Goto 2),(I ";" (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,p by SCMFSA8A:def 2; :: thesis: