set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At (insloc 0 )) c= s1 & I +* (Start-At (insloc 0 )) c= s2 & ex k being Element of NAT st Computation s1,k,s2 equal_outside NAT holds
Result s1, Result s2 equal_outside NAT
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At (insloc 0 )) c= s1 & I +* (Start-At (insloc 0 )) c= s2 & ex k being Element of NAT st Computation s1,k,s2 equal_outside NAT implies Result s1, Result s2 equal_outside NAT )
assume A1: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or not I +* (Start-At (insloc 0 )) c= s1 or not I +* (Start-At (insloc 0 )) c= s2 or for k being Element of NAT holds not Computation s1,k,s2 equal_outside NAT or Result s1, Result s2 equal_outside NAT )
assume A2: I is_halting_on s1 ; :: thesis: ( not I +* (Start-At (insloc 0 )) c= s1 or not I +* (Start-At (insloc 0 )) c= s2 or for k being Element of NAT holds not Computation s1,k,s2 equal_outside NAT or Result s1, Result s2 equal_outside NAT )
assume A3: I +* (Start-At (insloc 0 )) c= s1 ; :: thesis: ( not I +* (Start-At (insloc 0 )) c= s2 or for k being Element of NAT holds not Computation s1,k,s2 equal_outside NAT or Result s1, Result s2 equal_outside NAT )
assume A4: I +* (Start-At (insloc 0 )) c= s2 ; :: thesis: ( for k being Element of NAT holds not Computation s1,k,s2 equal_outside NAT or Result s1, Result s2 equal_outside NAT )
given k being Element of NAT such that A5: Computation s1,k,s2 equal_outside NAT ; :: thesis: Result s1, Result s2 equal_outside NAT
set s3 = Computation s1,k;
A6: s2 = s2 +* (I +* (Start-At (insloc 0 ))) by A4, FUNCT_4:79;
IC (Computation s1,k) = IC s2 by A5, SCMFSA8A:6
.= IC ((s2 +* I) +* (Start-At (insloc 0 ))) by A6, FUNCT_4:15
.= insloc 0 by AMI_1:111 ;
then ( IC SCM+FSA in dom (Computation s1,k) & (Computation s1,k) . (IC SCM+FSA ) = insloc 0 ) by AMI_1:94;
then A7: (IC SCM+FSA ) .--> (insloc 0 ) c= Computation s1,k by FUNCOP_1:88;
A8: DataPart (Computation s1,k) = DataPart s2 by A5, SCMFSA8A:6;
I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then I c= s1 by A3, XBOOLE_1:1;
then I c= Computation s1,k by AMI_1:86;
then I +* (Start-At (insloc 0 )) c= Computation s1,k by A7, FUNCT_4:92;
then A9: Computation s1,k = (Computation s1,k) +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:79;
A10: s1 = s1 +* (I +* (Start-At (insloc 0 ))) by A3, FUNCT_4:79;

now

let n be Element of NAT ; :: thesis: IC (Computation (Computation s1,k),n) in dom I
IC (Computation (Computation s1,k),n) = IC (Computation s1,(k + n)) by AMI_1:51;
hence IC (Computation (Computation s1,k),n) in dom I by A1, A10, SCMFSA7B:def 7; :: thesis: verum

end;

then A11: I is_closed_on Computation s1,k by A9, SCMFSA7B:def 7;
A12: s1 is halting by A2, A10, SCMFSA7B:def 8;
then consider n being Element of NAT such that
A13: CurInstr (Computation s1,n) = halt SCM+FSA by AMI_1:def 20;
CurInstr (Computation (Computation s1,k),n) = CurInstr (Computation s1,(k + n)) by AMI_1:51
.= CurInstr (Computation s1,n) by A13, AMI_1:52, NAT_1:11 ;
then Computation s1,k is halting by A13, AMI_1:def 20;
then I is_halting_on Computation s1,k by A9, SCMFSA7B:def 8;
then A14: Result (Computation s1,k), Result s2 equal_outside NAT by A6, A8, A9, A11, Th101;
consider k being Element of NAT such that
A15: CurInstr (Computation s1,k) = halt SCM+FSA by A12, AMI_1:def 20;
s1 . (IC (Computation s1,k)) = halt SCM+FSA by A15, AMI_1:54;
hence Result s1, Result s2 equal_outside NAT by A14, AMI_1:57; :: thesis: verum