let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1, s2 being State of SCMPDS
for I being Program of st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 holds
I is_closed_on s2,P2
let s1, s2 be State of SCMPDS; :: thesis: for I being Program of st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 holds
I is_closed_on s2,P2
let I be Program of ; :: thesis: ( DataPart s1 = DataPart s2 & I is_closed_on s1,P1 implies I is_closed_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);
assume A1: DataPart s1 = DataPart s2 ; :: thesis: ( not I is_closed_on s1,P1 or I is_closed_on s2,P2 )
A2: Comput ((P2 +* (stop I)),(Initialize s2),0) = Initialize s2 by EXTPRO_1:2;
A3: Comput ((P1 +* (stop I)),(Initialize s1),0) = Initialize s1 by EXTPRO_1:2;
then A4: DataPart (Comput ((P1 +* (stop I)),(Initialize s1),0)) = DataPart s1 by MEMSTR_0:45
.= DataPart (Comput ((P2 +* (stop I)),(Initialize s2),0)) by A1, A2, MEMSTR_0:45 ;
defpred S1[ 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)) );
A5: 0 in dom (stop I) by COMPOS_1:36;
assume A6: I is_closed_on s1,P1 ; :: thesis: I is_closed_on s2,P2
A7: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A8: Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)) = Following ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) by EXTPRO_1:3;
assume A9: S1[k] ; :: thesis: S1[k + 1]
then A10: 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;
stop I c= P2 +* (stop I) by FUNCT_4:25;
then A11: stop I c= P2 +* (stop I) ;
A12: IC (Comput ((P1 +* (stop I)),(Initialize s1),(k + 1))) in dom (stop I) by A6;
A13: Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)) = Following ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) by EXTPRO_1:3;
Comput ((P1 +* (stop I)),(Initialize s1),k) = Comput ((P2 +* (stop I)),(Initialize s2),k) by A9, A10, SCMPDS_4:2;
then A14: Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)) = Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)) by A9, A8, A13;
then A15: Comput ((P1 +* (stop I)),(Initialize s1),(k + 1)) = Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)) ;
A16: IC (Comput ((P1 +* (stop I)),(Initialize s1),(k + 1))) = IC (Comput ((P2 +* (stop I)),(Initialize s2),(k + 1))) by A14;
A17: (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;
A18: (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 stop I c= P1 +* (stop I) ;
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 A12, A17, GRFUNC_1:2
.= CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),(k + 1)))) by A11, A16, A12, A18, GRFUNC_1:2 ;
hence S1[k + 1] by A15; :: thesis: verum
end;
A19: IC (Comput ((P2 +* (stop I)),(Initialize s2),0)) = IC (Initialize s2) by A2
.= 0 by MEMSTR_0:def 11 ;
A20: (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;
A21: (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;
A22: IC (Comput ((P1 +* (stop I)),(Initialize s1),0)) = IC (Initialize s1) by A3
.= 0 by MEMSTR_0:def 11 ;
then CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),0))) = (stop I) . 0 by A5, A20, FUNCT_4:13
.= CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),0))) by A19, A5, A21, FUNCT_4:13 ;
then A23: S1[ 0 ] by A22, A19, A4;
now :: thesis: for k being Nat holds IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I)
let k be Nat; :: thesis: IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I)
A24: for k being Nat holds S1[k] from NAT_1:sch 2(A23, A7);
 IC (Comput ((P1 +* (stop I)),(Initialize s1),k)) in dom (stop I) by A6;
hence IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I) by A24; :: thesis: verum
end;
hence I is_closed_on s2,P2 ; :: thesis: verum