let s be State of SCM+FSA; :: according to SCMFSA6B:def 4 :: thesis: ( (I ';' J) +* (Start-At (0,SCM+FSA)) c= s implies for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) )
set SA0 = Start-At (0,SCM+FSA);
A1: I +* (Start-At (0,SCM+FSA)) c= s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
assume A2: (I ';' J) +* (Start-At (0,SCM+FSA)) c= s ; :: thesis: for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0)
then A3: s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) = s by FUNCT_4:79;
( dom (Start-At (0,SCM+FSA)) = {(IC SCM+FSA)} & intloc 0 <> IC SCM+FSA ) 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 A4: not intloc 0 in dom (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
Start-At (0,SCM+FSA) c= (I ';' J) +* (Start-At (0,SCM+FSA)) by FUNCT_4:26;
then A5: Start-At (0,SCM+FSA) c= s by A2, XBOOLE_1:1;
A6: s +* ((I ';' J) +* (Start-At (0,SCM+FSA))) = Initialize (s +* (I ';' J)) by FUNCT_4:15
.= (Initialize s) +* (I ';' J) by COMPOS_1:83
.= s +* (I ';' J) by A5, FUNCT_4:79 ;

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

suppose A7: ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) halts_on s +* (I +* (Start-At (0,SCM+FSA))) ; :: thesis: for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0)

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

hereby :: thesis: verum

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

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

(Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) . (intloc 0) = (s +* (I +* (Start-At (0,SCM+FSA)))) . (intloc 0) by A1, Def4
.= s . (intloc 0) by A4, FUNCT_4:12 ;
hence (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) by A3, A7, A9, Th40, SCMFSA10:92; :: thesis: verum

end;

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

set LS = LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))));
consider p being Element of NAT such that
A11: k = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 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;
( dom (Start-At (0,SCM+FSA)) = {(IC SCM+FSA)} & intloc 0 <> IC SCM+FSA ) 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 A14: not intloc 0 in dom (J +* (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
reconsider r = r as Element of NAT by ORDINAL1:def 13;
( dom (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),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 +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),r))) + (card I)),SCM+FSA)) by TARSKI:def 1;
then A15: ((Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),r)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),r))) + (card I)),SCM+FSA))) . (intloc 0) = (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),r)) . (intloc 0) by FUNCT_4:12;
A16: (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),r)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),r))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + r)) equal_outside NAT by A2, A6, A7, A8, Th42;
J +* (Start-At (0,SCM+FSA)) c= (Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then (Comput ((ProgramPart ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))),r)) . (intloc 0) = ((Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) +* (J +* (Start-At (0,SCM+FSA)))) . (intloc 0) by Def4
.= (Result ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) . (intloc 0) by A14, FUNCT_4:12
.= (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))) . (intloc 0) by A7, EXTPRO_1:23
.= (s +* (I +* (Start-At (0,SCM+FSA)))) . (intloc 0) by A1, Def4
.= s . (intloc 0) by A4, FUNCT_4:12 ;
hence (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) by A3, A11, A13, A15, A16, SCMFSA10:92; :: thesis: verum

end;

end;

end;

end;

suppose A17: not ProgramPart (s +* (I +* (Start-At (0,SCM+FSA)))) halts_on s +* (I +* (Start-At (0,SCM+FSA))) ; :: thesis: for k being Element of NAT holds (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0)

let k be Element of NAT ; :: thesis: (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0)
I +* (Start-At (0,SCM+FSA)) c= s +* (I +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),k)) . (intloc 0) = (s +* (I +* (Start-At (0,SCM+FSA)))) . (intloc 0) by Def4
.= s . (intloc 0) by A4, FUNCT_4:12 ;
hence (Comput ((ProgramPart s),s,k)) . (intloc 0) = s . (intloc 0) by A3, A17, Th41, SCMFSA10:92; :: thesis: verum

end;

end;