let s be State of SCM+FSA; :: according to SCM_HALT:def 3 :: thesis: ( Initialized (I ';' J) c= s implies for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1 )
A1: Initialized (I ';' J) = (I ';' J) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15;
A2: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
assume A3: Initialized (I ';' J) c= s ; :: thesis: for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1
then A4: s +* (Initialized (I ';' J)) = s by FUNCT_4:79;
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= (I ';' J) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then A5: ((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= s by A3, A1, XBOOLE_1:1;
s +* (Initialized (I ';' J)) = (s +* (I ';' J)) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by A1, FUNCT_4:15
.= (s +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) +* (I ';' J) by Th19
.= s +* (I ';' J) by A5, FUNCT_4:79 ;
then A6: s = s +* (I ';' J) by A3, FUNCT_4:79;

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

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

let k be Element of NAT ; :: thesis: (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1
A8: s +* (Initialized I) = s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) by FUNCT_4:15
.= (s +* I) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= (s +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) +* I by Th19
.= s +* I by A5, FUNCT_4:79 ;

hereby :: thesis: verum

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

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

(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) . (intloc 0) = 1 by A2, Def3;
hence (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1 by A4, A7, A9, Th24, SCMFSA10:92; :: thesis: verum

end;

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

set LS = LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)));
consider p being Element of NAT such that
A11: k = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + p and
A12: 1 <= p by A10, FINSEQ_4:99;
consider r being Nat such that
A13: p = 1 + r by A12, NAT_1:10;
reconsider r = r as Element of NAT by ORDINAL1:def 13;
set Rr = Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r);
set Sr = Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA);
Initialized J c= (Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J) by FUNCT_4:26;
then A14: (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r)) . (intloc 0) = 1 by Def3;
( dom (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA)) = {(IC SCM+FSA)} & intloc 0 <> IC SCM+FSA ) by FUNCOP_1:19, SCMFSA_2:81;
then not intloc 0 in dom (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
then A15: ((Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA))) . (intloc 0) = (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r)) . (intloc 0) by FUNCT_4:12;
(Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + r)) equal_outside NAT by A3, A7, A8, Th26;
hence (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1 by A6, A11, A13, A14, A15, SCMFSA10:92; :: thesis: verum

end;

end;

end;

end;

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

let k be Element of NAT ; :: thesis: (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1
Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),k)) . (intloc 0) = 1 by Def3;
hence (Comput ((ProgramPart s),s,k)) . (intloc 0) = 1 by A4, A16, Th27, SCMFSA10:92; :: thesis: verum

end;

end;