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: ( s1,s2 equal_outside NAT implies Exec (I,s1), Exec (I,s2) equal_outside NAT )
assume A2: s1,s2 equal_outside NAT ; :: thesis: Exec (I,s1), Exec (I,s2) equal_outside NAT
Exec (I,s1) = s1 by A1;
hence Exec (I,s1), Exec (I,s2) equal_outside NAT by A1, A2; :: thesis: verum