let s1, s2 be State of SCMPDS ; :: thesis: for I being Program of SCMPDS st I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) )
let I be Program of SCMPDS ; :: thesis: ( I is_closed_on s1 & Initialized (stop I) c= s1 & Initialized (stop I) c= s2 & s1,s2 equal_outside NAT implies for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) ) )
set iI = Initialized (stop I);
assume that
A1: I is_closed_on s1 and
A2: Initialized (stop I) c= s1 and
A3: Initialized (stop I) c= s2 and
A4: s1,s2 equal_outside NAT ; :: thesis: for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) )
A5: s2 = s2 +* (Initialized (stop I)) by A3, FUNCT_4:79;
A6: DataPart s1 = DataPart s2 by A4, SCMPDS_6:4;
s1 = s1 +* (Initialized (stop I)) by A2, FUNCT_4:79;
hence for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) ) by A1, A5, A6, Th25; :: thesis: verum