set D = Int-Locations \/ FinSeq-Locations ;
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 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 implies for k being Element of NAT holds
( Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
assume A1: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or not DataPart s1 = DataPart s2 or for k being Element of NAT holds
( Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
assume A2: I is_halting_on s1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Element of NAT holds
( Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
assume A3: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of NAT holds
( Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
set ss1 = s1 +* (I +* (Start-At (insloc 0 )));
set ss2 = s2 +* (I +* (Start-At (insloc 0 )));
( I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) & I c= I +* (Start-At (insloc 0 )) ) by FUNCT_4:26, SCMFSA8A:9;
then A4: I c= s1 +* (I +* (Start-At (insloc 0 ))) by XBOOLE_1:1;
( I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) & I c= I +* (Start-At (insloc 0 )) ) by FUNCT_4:26, SCMFSA8A:9;
then A5: I c= s2 +* (I +* (Start-At (insloc 0 ))) by XBOOLE_1:1;

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT & CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) )
A6: s1 +* (I +* (Start-At (insloc 0 ))),s2 +* (I +* (Start-At (insloc 0 ))) equal_outside NAT by A3, SCMFSA8B:7;
I is_closed_on s2 by A1, A2, A3, SCMFSA8B:8;
then for m being Element of NAT st m < k holds
IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),m) in dom I by SCMFSA7B:def 7;
hence Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT by A4, A5, A6, SCMFSA6B:21; :: thesis: CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)
then A7: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:121;
A8: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A1, SCMFSA7B:def 7;
I is_closed_on s2 by A1, A2, A3, SCMFSA8B:8;
then A9: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I by SCMFSA7B:def 7;
thus CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) = (s2 +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k)) by AMI_1:54
.= I . (IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k)) by A5, A9, GRFUNC_1:8
.= (s1 +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)) by A4, A7, A8, GRFUNC_1:8
.= CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:54 ; :: thesis: verum

end;