let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for S being stored-program AMI-Struct of IL,N
for I being Instruction of S st I is halting holds
I is Exec-preserving
let IL be non empty set ; :: thesis: for S being stored-program AMI-Struct of IL,N
for I being Instruction of S st I is halting holds
I is Exec-preserving
let S be stored-program AMI-Struct of IL,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 IL implies Exec I,s1, Exec I,s2 equal_outside IL )
assume A2: s1,s2 equal_outside IL ; :: thesis: Exec I,s1, Exec I,s2 equal_outside IL
( Exec I,s1 = s1 & Exec I,s2 = s2 ) by A1;
hence Exec I,s1, Exec I,s2 equal_outside IL by A2; :: thesis: verum