let I be Instruction of S; :: thesis: ( I is halting implies I is Exec-preserving )
assume A1: for s being State of S holds Exec (I,s) = s ; :: according to EXTPRO_1:def 3 :: thesis: I is Exec-preserving
let s1, s2 be State of S; :: according to AMISTD_2:def 20 :: thesis: ( NPP s1 = NPP s2 implies NPP (Exec (I,s1)) = NPP (Exec (I,s2)) )
assume A2: NPP s1 = NPP s2 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
Exec (I,s1) = s1 by A1;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A1, A2; :: thesis: verum