let s be State of SCM+FSA; :: according to SCM_HALT:def 2 :: thesis: ( Initialize ((intloc 0) .--> 1) c= s implies for p being Instruction-Sequence of SCM+FSA st I ";" J c= p holds
for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for p being Instruction-Sequence of SCM+FSA st I ";" J c= p holds
for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1
then A2: Initialized s = s by FUNCT_4:98;
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( I ";" J c= p implies for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A3: I ";" J c= p ; :: thesis: for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1
then A4: p +* (I ";" J) = p by FUNCT_4:98;
A5: I c= p +* I by FUNCT_4:25;
A6: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:25;

per cases ( p +* I halts_on Initialized s or not p +* I halts_on Initialized s ) ;

suppose A7: p +* I halts_on Initialized s ; :: thesis: for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1

let k be Nat; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1
A8: Initialized s = s by A1, FUNCT_4:98;

per cases ( k <= LifeSpan ((p +* I),(Initialized s)) or k > LifeSpan ((p +* I),(Initialized s)) ) ;

suppose A9: k <= LifeSpan ((p +* I),(Initialized s)) ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1

(Comput ((p +* I),(Initialized s),k)) . (intloc 0) = 1 by Def2, A5, A6;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A2, A7, A9, Th12, A4; :: thesis: verum

end;

suppose A10: k > LifeSpan ((p +* I),(Initialized s)) ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1

set LS = LifeSpan ((p +* I),(Initialized s));
consider pp being Element of NAT such that
A11: k = (LifeSpan ((p +* I),(Initialized s))) + pp and
A12: 1 <= pp by A10, FINSEQ_4:84;
consider r being Nat such that
A13: pp = 1 + r by A12, NAT_1:10;
reconsider r = r as Element of NAT by ORDINAL1:def 12;
set Rr = Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r);
set Sr = Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA);
A14: Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:25;
J c= (p +* I) +* J by FUNCT_4:25;
then A15: (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) . (intloc 0) = 1 by Def2, A14;
( dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by SCMFSA_2:56;
then A16: not intloc 0 in dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
(Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),(Initialized s))) + 1) + r)) by A1, A7, A8, Th14, A3;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A11, A13, A15, A16, A4, FUNCT_4:11; :: thesis: verum

end;

end;

end;

suppose A17: not p +* I halts_on Initialized s ; :: thesis: for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1

let k be Nat; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1
(Comput ((p +* I),(Initialized s),k)) . (intloc 0) = 1 by Def2, A5, A6;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A2, A4, A17, Th15; :: thesis: verum

end;

end;