let s1, s2 be State of SCMPDS; :: thesis: for I, J being Program of SCMPDS st DataPart s1 = DataPart s2 holds
NPP (Initialize s1) = NPP (Initialize s2)
let I, J be Program of SCMPDS; :: thesis: ( DataPart s1 = DataPart s2 implies NPP (Initialize s1) = NPP (Initialize s2) )
assume A1: DataPart s1 = DataPart s2 ; :: thesis: NPP (Initialize s1) = NPP (Initialize s2)
set S1 = Initialize s1;
set S2 = Initialize s2;
A4: ( IC (Initialize s1) = 0 & IC (Initialize s2) = 0 ) by COMPOS_1:223;
DataPart (Initialize s1) = DataPart s1 by COMPOS_1:80
.= DataPart (Initialize s2) by A1, COMPOS_1:80 ;
hence NPP (Initialize s1) = NPP (Initialize s2) by A4, Th4; :: thesis: verum