let s be State of SCM+FSA; :: according to SCM_HALT:def 3 :: 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 Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A2: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for p being Instruction-Sequence of SCM+FSA st I ';' J c= p holds
for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1
then A3: Initialized s = s by FUNCT_4:98;
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( I ';' J c= p implies for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1 )
assume A4: I ';' J c= p ; :: thesis: for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1
then A5: p +* (I ';' J) = p by FUNCT_4:98;
A8: I c= p +* I by FUNCT_4:25;
A9: 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 A10: p +* I halts_on Initialized s ; :: thesis: for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1

let k be Element of NAT ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1
A11: Initialized s = s by A2, FUNCT_4:98;

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

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

(Comput ((p +* I),(Initialized s),k)) . (intloc 0) = 1 by Def3, A8, A9;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A3, A10, A12, Th24, A5; :: thesis: verum

end;

suppose A14: 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
A15: k = (LifeSpan ((p +* I),(Initialized s))) + pp and
A16: 1 <= pp by A14, FINSEQ_4:84;
consider r being Nat such that
A17: pp = 1 + r by A16, 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);
A18: 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 A19: (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),r)) . (intloc 0) = 1 by Def3, A18;
( 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 FUNCOP_1:13, SCMFSA_2:56;
then B20: 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 A2, A10, A11, Th26, A4;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A15, A17, A19, B20, A5, FUNCT_4:11; :: thesis: verum

end;

end;

end;

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

let k be Element of NAT ; :: thesis: (Comput (p,s,k)) . (intloc 0) = 1
(Comput ((p +* I),(Initialized s),k)) . (intloc 0) = 1 by Def3, A8, A9;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A3, A5, A21, Th27; :: thesis: verum

end;

end;