let s1, s2 be State of ; :: thesis: for I being Program of st DataPart s1 = DataPart s2 & I is_closed_on s1 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )
let I be Program of ; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1 & I is_halting_on s1 implies ( I is_closed_on s2 & I is_halting_on s2 ) )
set S1 = s1 +* (I +* (Start-At (insloc 0 )));
set S2 = s2 +* (I +* (Start-At (insloc 0 )));
defpred S₁[ Element of NAT ] means ( IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & DataPart (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = DataPart (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) );
A1: IC SCM+FSA in {(IC SCM+FSA )} by TARSKI:def 1;
A2: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A3: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A4: {(IC SCM+FSA )} = dom (Start-At (insloc 0 )) by FUNCOP_1:19;
A5: Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 = s1 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
Start-At (insloc 0 ) c= I +* (Start-At (insloc 0 )) by FUNCT_4:26;
then A6: dom (Start-At (insloc 0 )) c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
then A7: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A1, A4, A5, FUNCT_4:14
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A1, A4, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
A8: Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 = s2 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
then A9: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A1, A4, A6, FUNCT_4:14
.= (Start-At (insloc 0 )) . (IC SCM+FSA ) by A1, A4, FUNCT_4:14
.= insloc 0 by FUNCOP_1:87 ;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1 or not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )
then A10: Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 , Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 equal_outside NAT by A5, A8, Th7;
assume A11: I is_closed_on s1 ; :: thesis: ( not I is_halting_on s1 or ( I is_closed_on s2 & I is_halting_on s2 ) )

A12: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A13: Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ;
assume A14: S₁[k] ; :: thesis: S₁[k + 1]
then A15: for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f by SCMFSA6A:38;
for a being Int-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . a = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . a by A14, SCMFSA6A:38;
then A16: Computation (s1 +* (I +* (Start-At (insloc 0 )))),k, Computation (s2 +* (I +* (Start-At (insloc 0 )))),k equal_outside NAT by A14, A15, SCMFSA6A:28;
I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then I c= s2 +* (I +* (Start-At (insloc 0 ))) by A2, XBOOLE_1:1;
then A17: I c= Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) by AMI_1:81;
A18: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) in dom I by A11, SCMFSA7B:def 7;
A19: Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) ;
then A20: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A14, A16, A13, AMI_1:121, SCMFSA6A:32;
I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then I c= s1 +* (I +* (Start-At (insloc 0 ))) by A2, XBOOLE_1:1;
then I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) by AMI_1:81;
then CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1))) by A18, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A17, A20, A18, GRFUNC_1:8 ;
hence S₁[k + 1] by A14, A16, A19, A13, A20, SCMFSA6A:32, SCMFSA6A:39; :: thesis: verum

end;

assume I is_halting_on s1 ; :: thesis: ( I is_closed_on s2 & I is_halting_on s2 )
then ProgramPart (s1 +* (I +* (Start-At (insloc 0 )))) halts_on s1 +* (I +* (Start-At (insloc 0 ))) by SCMFSA7B:def 8;
then consider m being Element of NAT such that
A21: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),m) = halt SCM+FSA by AMI_1:146;
A22: insloc 0 in dom I by A11, Th3;
then CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (I +* (Start-At (insloc 0 ))) . (insloc 0 ) by A5, A7, A3, FUNCT_4:14
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by A8, A9, A3, A22, FUNCT_4:14 ;
then A23: S₁[ 0 ] by A7, A9, A10, SCMFSA6A:39;

now

let k be Element of NAT ; :: thesis: IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I
A24: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A11, SCMFSA7B:def 7;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A23, A12);
hence IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A24; :: thesis: verum

end;

hence I is_closed_on s2 by SCMFSA7B:def 7; :: thesis: I is_halting_on s2
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A23, A12);
then CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),m) = halt SCM+FSA by A21;
then ProgramPart (s2 +* (I +* (Start-At (insloc 0 )))) halts_on s2 +* (I +* (Start-At (insloc 0 ))) by AMI_1:146;
hence I is_halting_on s2 by SCMFSA7B:def 8; :: thesis: verum