let P1, P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
let I be Program of SCM+FSA; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 implies ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) )
set S1 = s1 +* (Initialize I);
set S2 = s2 +* (Initialize I);
A1: ProgramPart I = I by RELAT_1:209;
defpred S₁[ Nat] means ( IC (Comput ((P1 +* I),(s1 +* (Initialize I)),$1)) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),$1)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),$1))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),$1))) & DataPart (Comput ((P1 +* I),(s1 +* (Initialize I)),$1)) = DataPart (Comput ((P2 +* I),(s2 +* (Initialize I)),$1)) );
A2: IC in {(IC )} by TARSKI:def 1;
A3: {(IC )} = dom (Start-At (0,SCM+FSA)) by FUNCOP_1:19;
A4: Comput ((P1 +* I),(s1 +* (Initialize I)),0) = s1 +* (Initialize I) by EXTPRO_1:3;
Start-At (0,SCM+FSA) c= Initialize I by FUNCT_4:26;
then A5: dom (Start-At (0,SCM+FSA)) c= dom (Initialize I) by GRFUNC_1:8;
then A6: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0)) = (Initialize I) . (IC ) by A2, A3, A4, FUNCT_4:14
.= (Start-At (0,SCM+FSA)) . (IC ) by A2, A3, FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
A7: Comput ((P2 +* I),(s2 +* (Initialize I)),0) = s2 +* (Initialize I) by EXTPRO_1:3;
then A8: IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0)) = (Initialize I) . (IC ) by A2, A3, A5, FUNCT_4:14
.= (Start-At (0,SCM+FSA)) . (IC ) by A2, A3, FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
assume DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1,P1 or not I is_halting_on s1,P1 or ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) )
then A9: Comput ((P1 +* I),(s1 +* (Initialize I)),0), Comput ((P2 +* I),(s2 +* (Initialize I)),0) equal_outside NAT by A4, A7, Th7;
assume A10: I is_closed_on s1,P1 ; :: thesis: ( not I is_halting_on s1,P1 or ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) )

A11: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A12: Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)) = Following ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k)))),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) ;
assume A13: S₁[k] ; :: thesis: S₁[k + 1]
then A14: for f being FinSeq-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . f = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . f by SCMFSA6A:38;
for a being Int-Location holds (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) . a = (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) . a by A13, SCMFSA6A:38;
then A15: Comput ((P1 +* I),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT by A13, A14, SCMFSA10:91;
A16: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1))) in dom I by A10, SCMFSA7B:def 7, A1;
Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)) = Following ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) by EXTPRO_1:4
.= Exec ((CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k)))),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) ;
then A17: Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)), Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)) equal_outside NAT by A13, A15, A12, AMISTD_2:def 20;
A18: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1))) = IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1))) by COMPOS_1:24, A17;
A19: (P1 +* I) /. (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) by PBOOLE:158;
A20: (P2 +* I) /. (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) = (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) by PBOOLE:158;
A21: I c= P1 +* I by FUNCT_4:26;
A22: I c= P2 +* I by FUNCT_4:26;
CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) = I . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),(k + 1)))) by A16, A19, GRFUNC_1:8, A21
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),(k + 1)))) by A18, A16, A20, GRFUNC_1:8, A22 ;
hence S₁[k + 1] by COMPOS_1:24, COMPOS_1:138, A17; :: thesis: verum

end;

assume I is_halting_on s1,P1 ; :: thesis: ( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
then P1 +* I halts_on s1 +* (Initialize I) by SCMFSA7B:def 8, A1;
then consider m being Element of NAT such that
A23: CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),m))) = halt SCM+FSA by EXTPRO_1:30;
A24: (P1 +* I) /. (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0))) = (P1 +* I) . (IC (Comput ((P1 +* I),(s1 +* (Initialize I)),0))) by PBOOLE:158;
A25: (P2 +* I) /. (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0))) = (P2 +* I) . (IC (Comput ((P2 +* I),(s2 +* (Initialize I)),0))) by PBOOLE:158;
A26: 0 in dom I by A10, Th3;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),0))) = I . 0 by A6, A24, FUNCT_4:14
.= CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),0))) by A8, A26, A25, FUNCT_4:14 ;
then A27: S₁[ 0 ] by A6, A8, A9, COMPOS_1:138;

now

let k be Element of NAT ; :: thesis: IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I
A28: IC (Comput ((P1 +* I),(s1 +* (Initialize I)),k)) in dom I by A10, SCMFSA7B:def 7, A1;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A27, A11);
hence IC (Comput ((P2 +* I),(s2 +* (Initialize I)),k)) in dom I by A28; :: thesis: verum

end;

hence I is_closed_on s2,P2 by SCMFSA7B:def 7, A1; :: thesis: I is_halting_on s2,P2
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A27, A11);
then CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),m))) = halt SCM+FSA by A23;
then P2 +* I halts_on s2 +* (Initialize I) by EXTPRO_1:30;
hence I is_halting_on s2,P2 by SCMFSA7B:def 8, A1; :: thesis: verum