let s be State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: ( Initialize (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) = s . (intloc 0) )
assume A1: Initialize (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) = s . (intloc 0)
then A2: s +* (Initialize (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) = s . (intloc 0) )
assume A3: I ';' J c= P ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A4: I c= P +* I by FUNCT_4:26;
A5: P = P +* (I ';' J) by A3, FUNCT_4:79;
( dom (Start-At (0,SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by FUNCOP_1:19, SCMFSA_2:81;
then ( not intloc 0 in dom I & not intloc 0 in dom (Start-At (0,SCM+FSA)) ) by SCMFSA6A:47, TARSKI:def 1;
then not intloc 0 in (dom I) \/ (dom (Start-At (0,SCM+FSA))) by XBOOLE_0:def 3;
then A6: not intloc 0 in dom (Initialize I) by FUNCT_4:def 1;
Start-At (0,SCM+FSA) c= Initialize (I ';' J) by FUNCT_4:26;
then A7: Start-At (0,SCM+FSA) c= s by A1, XBOOLE_1:1;
A8: s +* (Initialize (I ';' J)) = Initialize (s +* (I ';' J)) by FUNCT_4:15
.= (Initialize s) +* (I ';' J) by COMPOS_1:83
.= s +* (I ';' J) by A7, FUNCT_4:79 ;

per cases ( P +* I halts_on s +* (Initialize I) or not P +* I halts_on s +* (Initialize I) ) ;

suppose A9: P +* I halts_on s +* (Initialize I) ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A10: s +* (Initialize I) = Initialize (s +* I) by FUNCT_4:15
.= (Initialize s) +* I by COMPOS_1:83
.= s +* I by A7, FUNCT_4:79 ;

hereby :: thesis: verum

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

suppose A11: k <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

A12: Initialize I c= s +* (Initialize I) by FUNCT_4:26;
A13: (Comput ((P +* I),(s +* (Initialize I)),k)) . (intloc 0) = (s +* (Initialize I)) . (intloc 0) by Def4, A4, A12
.= s . (intloc 0) by A6, FUNCT_4:12 ;
Comput ((P +* I),(s +* (Initialize I)),k), Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),k) equal_outside NAT by Th40, A9, A11;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, SCMFSA10:92, A13, A5; :: thesis: verum

end;

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

set LS = LifeSpan ((P +* I),(s +* (Initialize I)));
consider p being Element of NAT such that
A15: k = (LifeSpan ((P +* I),(s +* (Initialize I)))) + p and
A16: 1 <= p by A14, FINSEQ_4:99;
consider r being Nat such that
A17: p = 1 + r by A16, NAT_1:10;
( dom (Start-At (0,SCM+FSA)) = {(IC )} & intloc 0 <> IC ) by FUNCOP_1:19, SCMFSA_2:81;
then ( not intloc 0 in dom J & not intloc 0 in dom (Start-At (0,SCM+FSA)) ) by SCMFSA6A:47, TARSKI:def 1;
then not intloc 0 in (dom J) \/ (dom (Start-At (0,SCM+FSA))) by XBOOLE_0:def 3;
then A18: not intloc 0 in dom (Initialize J) by FUNCT_4:def 1;
reconsider r = r as Element of NAT by ORDINAL1:def 13;
( dom (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (J +* (Start-At (0,SCM+FSA)))),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 +* (Start-At (0,SCM+FSA)))))) +* (Initialize J)),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
then A19: ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),r)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),r))) + (card I)),SCM+FSA))) . (intloc 0) = (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),r)) . (intloc 0) by FUNCT_4:12;
A20: (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),r)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),r))) + (card I)),SCM+FSA)), Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + r)) equal_outside NAT by A1, A8, A9, A10, Th42, A3;
A21: Initialize J c= (Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J) by FUNCT_4:26;
A22: J c= (P +* I) +* J by FUNCT_4:26;
A23: Initialize I c= s +* (Initialize I) by FUNCT_4:26;
(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),r)) . (intloc 0) = ((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)) . (intloc 0) by Def4, A22, A21
.= (Result ((P +* I),(s +* (Initialize I)))) . (intloc 0) by A18, FUNCT_4:12
.= (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) . (intloc 0) by A9, EXTPRO_1:23
.= (s +* (Initialize I)) . (intloc 0) by Def4, A4, A23
.= s . (intloc 0) by A6, FUNCT_4:12 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A15, A17, A19, A20, SCMFSA10:92, A5; :: thesis: verum

end;

end;

end;

end;

suppose A24: not P +* I halts_on s +* (Initialize I) ; :: thesis: for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

let k be Element of NAT ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A25: Initialize I c= s +* (Initialize I) by FUNCT_4:26;
(Comput ((P +* I),(s +* (Initialize I)),k)) . (intloc 0) = (s +* (Initialize I)) . (intloc 0) by Def4, A4, A25
.= s . (intloc 0) by A6, FUNCT_4:12 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A24, Th41, SCMFSA10:92, A5; :: thesis: verum

end;

end;