let s be State of SCM+FSA ; :: according to SCMFSA6B:def 4 :: thesis: ( (I ';' J) +* (Start-At (insloc 0 )) c= s implies for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) )
set SA0 = Start-At (insloc 0 );
A1: I +* (Start-At (insloc 0 )) c= s +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
assume A2: (I ';' J) +* (Start-At (insloc 0 )) c= s ; :: thesis: for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
then A3: s +* ((I ';' J) +* (Start-At (insloc 0 ))) = s by FUNCT_4:79;
( dom (Start-At (insloc 0 )) = {(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 (insloc 0 )) ) by SCMFSA6A:47, TARSKI:def 1;
then not intloc 0 in (dom I) \/ (dom (Start-At (insloc 0 ))) by XBOOLE_0:def 3;
then A4: not intloc 0 in dom (I +* (Start-At (insloc 0 ))) by FUNCT_4:def 1;
Start-At (insloc 0 ) c= (I ';' J) +* (Start-At (insloc 0 )) by FUNCT_4:26;
then A5: Start-At (insloc 0 ) c= s by A2, XBOOLE_1:1;
A6: s +* ((I ';' J) +* (Start-At (insloc 0 ))) = (s +* (I ';' J)) +* (Start-At (insloc 0 )) by FUNCT_4:15
.= (s +* (Start-At (insloc 0 ))) +* (I ';' J) by Th14
.= s +* (I ';' J) by A5, FUNCT_4:79 ;

per cases ( s +* (I +* (Start-At (insloc 0 ))) is halting or not s +* (I +* (Start-At (insloc 0 ))) is halting ) ;

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

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

hereby :: thesis: verum

per cases ( k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) or k > LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ) ;

suppose A9: k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )

(Computation (s +* (I +* (Start-At (insloc 0 )))),k) . (intloc 0 ) = (s +* (I +* (Start-At (insloc 0 )))) . (intloc 0 ) by A1, Def4
.= s . (intloc 0 ) by A4, FUNCT_4:12 ;
hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by A3, A7, A9, Th40, SCMFSA6A:30; :: thesis: verum

end;

suppose A10: k > LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )

set LS = LifeSpan (s +* (I +* (Start-At (insloc 0 ))));
consider p being Element of NAT such that
A11: k = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + p and
A12: 1 <= p by A10, FSM_1:1;
consider r being Nat such that
A13: p = 1 + r by A12, NAT_1:10;
( dom (Start-At (insloc 0 )) = {(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 (insloc 0 )) ) by SCMFSA6A:47, TARSKI:def 1;
then not intloc 0 in (dom J) \/ (dom (Start-At (insloc 0 ))) by XBOOLE_0:def 3;
then A14: not intloc 0 in dom (J +* (Start-At (insloc 0 ))) by FUNCT_4:def 1;
reconsider r = r as Element of NAT by ORDINAL1:def 13;
( dom (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),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 +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),r)) + (card I))) by TARSKI:def 1;
then A15: ((Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),r) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),r)) + (card I)))) . (intloc 0 ) = (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),r) . (intloc 0 ) by FUNCT_4:12;
A16: (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),r) +* (Start-At ((IC (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),r)) + (card I))), Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + r) equal_outside NAT by A2, A6, A7, A8, Th42;
J +* (Start-At (insloc 0 )) c= (Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then (Computation ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))),r) . (intloc 0 ) = ((Result (s +* (I +* (Start-At (insloc 0 ))))) +* (J +* (Start-At (insloc 0 )))) . (intloc 0 ) by Def4
.= (Result (s +* (I +* (Start-At (insloc 0 ))))) . (intloc 0 ) by A14, FUNCT_4:12
.= (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) . (intloc 0 ) by A7, AMI_1:122
.= (s +* (I +* (Start-At (insloc 0 )))) . (intloc 0 ) by A1, Def4
.= s . (intloc 0 ) by A4, FUNCT_4:12 ;
hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by A3, A11, A13, A15, A16, SCMFSA6A:30; :: thesis: verum

end;

end;

end;

end;

suppose A17: not s +* (I +* (Start-At (insloc 0 ))) is halting ; :: thesis: for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = s . (intloc 0 )

let k be Element of NAT ; :: thesis: (Computation s,k) . (intloc 0 ) = s . (intloc 0 )
I +* (Start-At (insloc 0 )) c= s +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . (intloc 0 ) = (s +* (I +* (Start-At (insloc 0 )))) . (intloc 0 ) by Def4
.= s . (intloc 0 ) by A4, FUNCT_4:12 ;
hence (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) by A3, A17, Th41, SCMFSA6A:30; :: thesis: verum

end;

end;