let s be State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: ( Start-At (0,SCM+FSA) 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: Start-At (0,SCM+FSA) 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 +* (Start-At (0,SCM+FSA)) = s by FUNCT_4:104;
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:104;
( 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 by FUNCT_4:26;
then dom (Start-At (0,SCM+FSA)) c= dom (Initialize I) by RELAT_1:25;
then B6: not intloc 0 in dom (Start-At (0,SCM+FSA)) by A6;

per cases ( P +* I halts_on s +* (Start-At (0,SCM+FSA)) or not P +* I halts_on s +* (Start-At (0,SCM+FSA)) ) ;

suppose A9: P +* I halts_on s +* (Start-At (0,SCM+FSA)) ; :: 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 +* (Start-At (0,SCM+FSA)) = s by A1, FUNCT_4:104;

hereby :: thesis: verum

per cases ( k <= LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))) or k > LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))) ) ;

suppose A11: k <= LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))) ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

XX: NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),k)) by Th40, A9, A11;
Start-At (0,SCM+FSA) c= s +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
then (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) . (intloc 0) = (s +* (Start-At (0,SCM+FSA))) . (intloc 0) by Def4, A4
.= s . (intloc 0) by B6, FUNCT_4:12 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A5, XX, SCMFSA10:92; :: thesis: verum

end;

suppose A14: k > LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA)))) ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

set LS = LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))));
consider p being Element of NAT such that
A15: k = (LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 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 A18: not intloc 0 in dom (Start-At (0,SCM+FSA)) by TARSKI: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 +* (Start-At (0,SCM+FSA))))) +* (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 +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
then A19: (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),r)),(card I))) . (intloc 0) = (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),r)) . (intloc 0) by FUNCT_4:12;
A20: NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),r)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + r))) by A1, A9, Th42, A3, A10;
A21: Start-At (0,SCM+FSA) c= (Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
A22: J c= (P +* I) +* J by FUNCT_4:26;
B23: Start-At (0,SCM+FSA) c= s +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
C23: (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),r)) . (intloc 0) = ((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))) . (intloc 0) by Def4, A22, A21
.= (Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) . (intloc 0) by A18, FUNCT_4:12
.= (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))))) . (intloc 0) by A9, EXTPRO_1:23
.= (s +* (Start-At (0,SCM+FSA))) . (intloc 0) by Def4, A4, B23
.= s . (intloc 0) by B6, FUNCT_4:12 ;
(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Start-At (0,SCM+FSA))))) +* (Start-At (0,SCM+FSA))),r)) . (intloc 0) = (Comput (P,(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + r))) . (intloc 0) by A20, A5, A19, SCMFSA10:92;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A15, A17, C23; :: thesis: verum

end;

end;

end;

end;

suppose A24: not P +* I halts_on s +* (Start-At (0,SCM+FSA)) ; :: 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: Start-At (0,SCM+FSA) c= s +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
XX: NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),k)) by A24, Th41;
(Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) . (intloc 0) = (s +* (Start-At (0,SCM+FSA))) . (intloc 0) by Def4, A4, A25
.= s . (intloc 0) by B6, FUNCT_4:12 ;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A5, XX, SCMFSA10:92; :: thesis: verum

end;

end;