let s1, s2 be State of ; :: thesis: for I being Program of 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) )
set D = Int-Locations \/ FinSeq-Locations ;
let I be Program of ; :: 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) ) )
set ss2 = s2 +* (I +* (Start-At (insloc 0 )));
set ss1 = s1 +* (I +* (Start-At (insloc 0 )));
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) )
A4: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
A5: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A6: I c= s2 +* (I +* (Start-At (insloc 0 ))) by A4, XBOOLE_1:1;
I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A7: I c= s1 +* (I +* (Start-At (insloc 0 ))) by A5, 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) )
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: 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;
s1 +* (I +* (Start-At (insloc 0 ))),s2 +* (I +* (Start-At (insloc 0 ))) equal_outside NAT by A3, SCMFSA8B:7;
hence Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT by A7, A6, A9, SCMFSA6B:21; :: thesis: CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)
then A10: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:121;
I is_closed_on s2 by A1, A2, A3, SCMFSA8B:8;
then A11: 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 A6, A11, GRFUNC_1:8
.= (s1 +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)) by A7, A10, A8, GRFUNC_1:8
.= CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:54 ; :: thesis: verum

end;