let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
s1 = s2
let A be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for s1, s2 being State of A st IC s1 = IC s2 & DataPart s1 = DataPart s2 holds
s1 = s2
set D = Data-Locations ;
let s1, s2 be State of A; :: thesis: ( IC s1 = IC s2 & DataPart s1 = DataPart s2 implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: DataPart s1 = DataPart s2 ; :: thesis: s1 = s2
A3: dom s2 = {(IC )} \/ (Data-Locations ) by Th13;
A4: dom s1 = {(IC )} \/ (Data-Locations ) by Th13;
then s1 | {(IC )} = s2 | {(IC )} by A1, A3, GRFUNC_1:29;
then s1 | ({(IC )} \/ (Data-Locations )) = s2 | ({(IC )} \/ (Data-Locations )) by A2, RELAT_1:150;
then s1 | ({(IC )} \/ (Data-Locations )) = s2 | ({(IC )} \/ (Data-Locations )) ;
hence s1 = s2 | (dom s2) by A4, A3
.= s2 ;
:: thesis: verum