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 AMI_1:def 8 :: 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