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