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 (Computation s,k) . (intloc 0 ) = 1 )
assume A1: Initialized (I ';' J) c= s ; :: thesis: for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = 1
then A2: s +* (Initialized (I ';' J)) = s by FUNCT_4:79;
A3: Initialized (I ';' J) = (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:15;
((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= (I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A4: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s by A1, A3, XBOOLE_1:1;
s +* (Initialized (I ';' J)) = (s +* (I ';' J)) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) by A3, FUNCT_4:15
.= (s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* (I ';' J) by Th19
.= s +* (I ';' J) by A4, FUNCT_4:79 ;
then A5: s = s +* (I ';' J) by A1, FUNCT_4:79;
A6: Initialized I c= s +* (Initialized I) by FUNCT_4:26;

per cases ( s +* (Initialized I) is halting or not s +* (Initialized I) is halting ) ;

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

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

hereby :: thesis: verum

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

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

(Computation (s +* (Initialized I)),k) . (intloc 0 ) = 1 by A6, Def3;
hence (Computation s,k) . (intloc 0 ) = 1 by A2, A7, A9, Th24, SCMFSA6A:30; :: thesis: verum

end;

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

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

end;

end;

end;

end;

suppose A15: not s +* (Initialized I) is halting ; :: thesis: for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = 1

let k be Element of NAT ; :: thesis: (Computation s,k) . (intloc 0 ) = 1
Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then (Computation (s +* (Initialized I)),k) . (intloc 0 ) = 1 by Def3;
hence (Computation s,k) . (intloc 0 ) = 1 by A2, A15, Th27, SCMFSA6A:30; :: thesis: verum

end;

end;