let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program realistic Exec-preserving AMI-Struct of N
for s1, s2 being State of S st s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) holds
for l being Instruction of S holds (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )})
let S be non empty stored-program realistic Exec-preserving AMI-Struct of N; :: thesis: for s1, s2 being State of S st s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) holds
for l being Instruction of S holds (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )})
let s1, s2 be State of S; :: thesis: ( s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) implies for l being Instruction of S holds (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )}) )
assume A1: s1 | ((Data-Locations S) \/ {(IC )}) = s2 | ((Data-Locations S) \/ {(IC )}) ; :: thesis: for l being Instruction of S holds (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )})
let l be Instruction of S; :: thesis: (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )})
s1,s2 equal_outside NAT by A1, COMPOS_1:175;
then Exec (l,s1), Exec (l,s2) equal_outside NAT by Def20;
hence (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )}) by COMPOS_1:175; :: thesis: verum