let i be Instruction of SCMPDS; :: according to AMISTD_2:def 21 :: thesis: i is Exec-preserving
thus for s1, s2 being State of SCMPDS st NPP s1 = NPP s2 holds
NPP (Exec (i,s1)) = NPP (Exec (i,s2)) by Th15; :: according to AMISTD_2:def 20 :: thesis: verum