let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1,P1 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & stop I c= P1 & stop I c= P2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let s1, s2 be State of SCMPDS; :: thesis: for I being Program of SCMPDS st I is_closed_on s1,P1 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & stop I c= P1 & stop I c= P2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1,P1 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & stop I c= P1 & stop I c= P2 & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
set pI = stop I;
assume that
A1: I is_closed_on s1,P1 and
A2: Start-At (0,SCMPDS) c= s1 and
A3: Start-At (0,SCMPDS) c= s2 and
B2: stop I c= P1 and
B3: stop I c= P2 and
A4: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A5: IC in dom (Start-At (0,SCMPDS)) by COMPOS_1:def 16;
then A6: IC s1 = (Start-At (0,SCMPDS)) . (IC ) by A2, GRFUNC_1:8
.= IC s2 by A3, A5, GRFUNC_1:8 ;
defpred S₁[ Element of NAT ] means ( IC (Comput (P1,s1,$1)) = IC (Comput (P2,s2,$1)) & CurInstr (P1,(Comput (P1,s1,$1))) = CurInstr (P2,(Comput (P2,s2,$1))) & DataPart (Comput (P1,s1,$1)) = DataPart (Comput (P2,s2,$1)) );
A8: s1 = Initialize s1 by A2, FUNCT_4:104;
B9: P1 +* (stop I) = P1 by B2, FUNCT_4:104;
A9: s1 = Initialize s1 by A8;
then IC (Comput (P1,s1,0)) in dom (stop I) by A1, SCMPDS_6:def 2, B9;
then A10: IC s1 in dom (stop I) by EXTPRO_1:3;
then A11: P1 . (IC s1) = (stop I) . (IC s1) by GRFUNC_1:8, B2
.= P2 . (IC s2) by A10, A6, GRFUNC_1:8, B3 ;
A12: DataPart (Comput (P1,s1,0)) = DataPart s2 by A4, EXTPRO_1:3
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:3 ;
A13: Comput (P1,s1,0) = s1 by EXTPRO_1:3;
A14: Comput (P2,s2,0) = s2 by EXTPRO_1:3;
A15: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:158;
A16: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:158;
A17: CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by A13
.= CurInstr (P2,s2) by A11, A15, A16
.= CurInstr (P2,(Comput (P2,s2,0))) by A14 ;
A18: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A19: S₁[k] ; :: thesis: S₁[k + 1]
set l = IC (Comput (P1,s1,(k + 1)));
A20: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A1, A9, SCMPDS_6:def 2, B9;
set i = CurInstr (P1,(Comput (P1,s1,k)));
A23: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,k)))),(Comput (P1,s1,k))) ;
A25: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,k)))),(Comput (P2,s2,k))) by A19 ;
hence IC (Comput (P1,s1,(k + 1))) = IC (Comput (P2,s2,(k + 1))) by A19, A23, Th23; :: thesis: ( CurInstr (P1,(Comput (P1,s1,(k + 1)))) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
A26: P1 /. (IC (Comput (P1,s1,(k + 1)))) = P1 . (IC (Comput (P1,s1,(k + 1)))) by PBOOLE:158;
A27: P2 /. (IC (Comput (P2,s2,(k + 1)))) = P2 . (IC (Comput (P2,s2,(k + 1)))) by PBOOLE:158;
thus CurInstr (P1,(Comput (P1,s1,(k + 1)))) = P1 . (IC (Comput (P1,s1,(k + 1)))) by A26
.= (stop I) . (IC (Comput (P1,s1,(k + 1)))) by A20, GRFUNC_1:8, B2
.= P2 . (IC (Comput (P1,s1,(k + 1)))) by A20, GRFUNC_1:8, B3
.= P2 . (IC (Comput (P1,s1,(k + 1))))
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by A19, A23, A25, Th23, A27 ; :: thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A19, A23, A25, Th23; :: thesis: verum

end;

IC (Comput (P1,s1,0)) = IC s1 by EXTPRO_1:3
.= IC (Comput (P2,s2,0)) by A6, EXTPRO_1:3 ;
then A28: S₁[ 0 ] by A17, A12;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A28, A18); :: thesis: verum