let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite 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 IC-Ins-separated definite 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 )})
NPP s1 = NPP s2 by A1, COMPOS_1:175;
then NPP (Exec (l,s1)) = NPP (Exec (l,s2)) by Def20;
hence (Exec (l,s1)) | ((Data-Locations S) \/ {(IC )}) = (Exec (l,s2)) | ((Data-Locations S) \/ {(IC )}) by COMPOS_1:175; :: thesis: verum