let s1, s2 be State of SCMPDS ; :: thesis: for I, J being Program of SCMPDS st DataPart s1 = DataPart s2 holds
s1 +* (Initialized I),s2 +* (Initialized J) equal_outside NAT
let I, J be Program of SCMPDS ; :: thesis: ( DataPart s1 = DataPart s2 implies s1 +* (Initialized I),s2 +* (Initialized J) equal_outside NAT )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: s1 +* (Initialized I),s2 +* (Initialized J) equal_outside NAT
set II = Initialized I;
set S1 = s1 +* (Initialized I);
set IJ = Initialized J;
set S2 = s2 +* (Initialized J);
A2: ( IC (s1 +* (Initialized I)) = 0 & IC (s2 +* (Initialized J)) = 0 ) by FUNCT_4:26, SCMPDS_5:18;
DataPart (s1 +* (Initialized I)) = DataPart s1 by Th9
.= DataPart (s2 +* (Initialized J)) by A1, Th9 ;
hence s1 +* (Initialized I),s2 +* (Initialized J) equal_outside NAT by A2, Th4; :: thesis: verum