let N be non empty with_non-empty_elements set ; :: thesis: for S being stored-program AMI-Struct of N
for I being Instruction of S st I is halting holds
I is Exec-preserving
let S be stored-program AMI-Struct of N; :: thesis: for I being Instruction of S st I is halting holds
I is Exec-preserving
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 19 :: 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