let s be State of SCM+FSA; :: according to SCM_HALT:def 3 :: thesis: ( Initialized (I ';' J) c= s implies for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I ';' J c= p holds
for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1 )
A1: Initialized (I ';' J) = (I ';' J) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15;
assume A2: Initialized (I ';' J) c= s ; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I ';' J c= p holds
for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1
then A3: s +* (Initialized (I ';' J)) = s by FUNCT_4:79;
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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:79;
Initialize ((intloc 0) .--> 1) c= (I ';' J) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then A6: Initialize ((intloc 0) .--> 1) c= s by A2, A1, XBOOLE_1:1;
s +* (Initialized (I ';' J)) = (s +* (I ';' J)) +* (Initialize ((intloc 0) .--> 1)) by A1, FUNCT_4:15
.= (s +* (Initialize ((intloc 0) .--> 1))) +* (I ';' J) by Th19
.= s +* (I ';' J) by A6, FUNCT_4:79 ;
then A7: s = s +* (I ';' J) by A2, FUNCT_4:79;
A8: I c= p +* I by FUNCT_4:26;
A9: Initialized I c= s +* (Initialized I) by FUNCT_4:26;

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

suppose A10: p +* I halts_on s +* (Initialized I) ; :: 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: s +* (Initialized I) = s +* (I +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= (s +* I) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= (s +* (Initialize ((intloc 0) .--> 1))) +* I by Th19
.= s +* I by A6, FUNCT_4:79 ;

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

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

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

end;

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

set LS = LifeSpan ((p +* I),(s +* (Initialized I)));
consider pp being Element of NAT such that
A15: k = (LifeSpan ((p +* I),(s +* (Initialized I)))) + pp and
A16: 1 <= pp by A14, FINSEQ_4:99;
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 13;
set Rr = Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r);
set Sr = Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA);
A18: Initialized J c= (Result ((p +* I),(s +* I))) +* (Initialized J) by FUNCT_4:26;
J c= (p +* I) +* J by FUNCT_4:26;
then A19: (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r)) . (intloc 0) = 1 by Def3, A18;
( dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by FUNCOP_1:19, SCMFSA_2:81;
then not intloc 0 in dom (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
then A20: ((Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA))) . (intloc 0) = (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r)) . (intloc 0) by FUNCT_4:12;
(Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),(s +* I))) +* (Initialized J)),r))) + (card I)),SCM+FSA)), Comput ((p +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + r)) equal_outside NAT by A2, A10, A11, Th26, A4;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A7, A15, A17, A19, A20, SCMFSA10:92, A5; :: thesis: verum

end;

end;

end;

suppose A21: not p +* I halts_on s +* (Initialized I) ; :: 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),(s +* (Initialized I)),k)) . (intloc 0) = 1 by Def3, A8, A9;
hence (Comput (p,s,k)) . (intloc 0) = 1 by A3, A21, Th27, SCMFSA10:92, A5; :: thesis: verum

end;

end;