let s1, s2 be State of SCMPDS; :: thesis: for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS st I is_closed_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 holds
for k being Element of NAT holds
( NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) & CurInstr (P1,(Comput (P1,s1,k))) = CurInstr (P2,(Comput (P2,s2,k))) )
let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCMPDS st I is_closed_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 holds
for k being Element of NAT holds
( NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) & CurInstr (P1,(Comput (P1,s1,k))) = CurInstr (P2,(Comput (P2,s2,k))) )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1,P1 & stop I c= P1 & stop I c= P2 & Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & NPP s1 = NPP s2 implies for k being Element of NAT holds
( NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) & CurInstr (P1,(Comput (P1,s1,k))) = CurInstr (P2,(Comput (P2,s2,k))) ) )
set iI = stop I;
assume that
A3: I is_closed_on s1,P1 and
A4: stop I c= P1 and
A5: stop I c= P2 and
B4: Start-At (0,SCMPDS) c= s1 and
B5: Start-At (0,SCMPDS) c= s2 and
A6: NPP s1 = NPP s2 ; :: thesis: for k being Element of NAT holds
( NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) & CurInstr (P1,(Comput (P1,s1,k))) = CurInstr (P2,(Comput (P2,s2,k))) )
A1: s1 = Initialize s1 by B4, FUNCT_4:104;
A2: s2 = Initialize s2 by B5, FUNCT_4:104;
A7: P2 = P2 +* (stop I) by A5, FUNCT_4:104;
A8: DataPart s1 = DataPart s2 by A6, SCMPDS_6:4;
P1 = P1 +* (stop I) by A4, FUNCT_4:104;
hence for k being Element of NAT holds
( NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) & CurInstr (P1,(Comput (P1,s1,k))) = CurInstr (P2,(Comput (P2,s2,k))) ) by A3, A7, A8, Th25, A1, A2; :: thesis: verum