let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1, s2 being State of SCMPDS
for I being Program of SCMPDS 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 SCMPDS; :: thesis: for I being Program of SCMPDS 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 SCMPDS; :: 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 pI = stop I;
set S1 = Initialize s1;
set S2 = Initialize s2;
set E1 = P1 +* (stop I);
set E2 = P2 +* (stop I);
defpred S₁[ Element of NAT ] means ( IC (Comput ((P1 +* (stop I)),(Initialize s1),$1)) = IC (Comput ((P2 +* (stop I)),(Initialize s2),$1)) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),$1))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),$1))) & DataPart (Comput ((P1 +* (stop I)),(Initialize s1),$1)) = DataPart (Comput ((P2 +* (stop I)),(Initialize s2),$1)) );
A3: Comput ((P1 +* (stop I)),(Initialize s1),0) = Initialize s1 by EXTPRO_1:2;
A4: Comput ((P2 +* (stop I)),(Initialize s2),0) = Initialize s2 by EXTPRO_1:2;
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 A5: Comput ((P1 +* (stop I)),(Initialize s1),0) = Comput ((P2 +* (stop I)),(Initialize s2),0) by A3, A4, MEMSTR_0:80;
A6: 0 in dom (stop I) by COMPOS_1:36;
assume A9: 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 ) )

A10: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
A12: Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)) = Following ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) by EXTPRO_1:3;
assume A13: S₁[k] ; :: thesis: S₁[k + 1]
then for a being Int_position holds (Comput ((P1 +* (stop I)),(Initialize s1),k)) . a = (Comput ((P2 +* (stop I)),(Initialize s2),k)) . a by SCMPDS_4:8;
then A14: Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) by A13, SCMPDS_4:2;
A15: stop I c= P2 +* (stop I) by FUNCT_4:25;
A16: IC (Comput ((P1 +* (stop I)),(Initialize s1),(k + 1))) in dom (stop I) by A9, Def2;
Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)) = Following ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) by EXTPRO_1:3;
then B18: Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)) = Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)) by A13, A14, A12;
then A18: IC (Comput ((P1 +* (stop I)),(Initialize s1),(k + 1))) = IC (Comput ((P2 +* (stop I)),(Initialize s2),(k + 1))) ;
A19: (P1 +* (stop I)) /. (IC (Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)))) = (P1 +* (stop I)) . (IC (Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)))) by PBOOLE:143;
A20: (P2 +* (stop I)) /. (IC (Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)))) = (P2 +* (stop I)) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)))) by PBOOLE:143;
stop I c= P1 +* (stop I) by FUNCT_4:25;
then CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)))) = (stop I) . (IC (Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)))) by A16, A19, GRFUNC_1:2
.= CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)))) by A15, A18, A16, A20, GRFUNC_1:2 ;
hence S₁[k + 1] by B18; :: thesis: verum

end;

A24: IC (Comput ((P2 +* (stop I)),(Initialize s2),0)) = IC (Initialize s2) by A4
.= 0 by MEMSTR_0:def 8 ;
assume I is_halting_on s1,P1 ; :: thesis: ( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
then P1 +* (stop I) halts_on Initialize s1 by Def3;
then consider m being Element of NAT such that
A25: CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),m))) = halt SCMPDS by EXTPRO_1:29;
A26: (P1 +* (stop I)) /. (IC (Comput ((P1 +* (stop I)),(Initialize s1),0))) = (P1 +* (stop I)) . (IC (Comput ((P1 +* (stop I)),(Initialize s1),0))) by PBOOLE:143;
A27: (P2 +* (stop I)) /. (IC (Comput ((P2 +* (stop I)),(Initialize s2),0))) = (P2 +* (stop I)) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),0))) by PBOOLE:143;
IC (Comput ((P1 +* (stop I)),(Initialize s1),0)) = IC (Initialize s1) by A3
.= 0 by MEMSTR_0:def 8 ;
then CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),0))) = (stop I) . 0 by A6, A26, FUNCT_4:13
.= CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),0))) by A24, A6, A27, FUNCT_4:13 ;
then A29: S₁[ 0 ] by A5;

now

let k be Element of NAT ; :: thesis: IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I)
A30: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A29, A10);
IC (Comput ((P1 +* (stop I)),(Initialize s1),k)) in dom (stop I) by A9, Def2;
hence IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I) by A30; :: thesis: verum

end;

hence I is_closed_on s2,P2 by Def2; :: thesis: I is_halting_on s2,P2
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A29, A10);
then CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),m))) = halt SCMPDS by A25;
then P2 +* (stop I) halts_on Initialize s2 by EXTPRO_1:29;
hence I is_halting_on s2,P2 by Def3; :: thesis: verum