let s1, s2 be State of SCM+FSA; :: thesis: ( s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies DataPart s1 = DataPart s2 )
set D = Data-Locations ;
assume A1: s1 . (intloc 0) = s2 . (intloc 0) ; :: thesis: ( ex a being read-write Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
assume A2: for a being read-write Int-Location holds s1 . a = s2 . a ; :: thesis: ( ex f being FinSeq-Location st not s1 . f = s2 . f or DataPart s1 = DataPart s2 )
A3: dom (DataPart s1) = (dom s1) /\ (Data-Locations ) by RELAT_1:61
.= ((Data-Locations ) \/ {(IC )}) /\ (Data-Locations ) by MEMSTR_0:13
.= (dom s2) /\ (Data-Locations ) by MEMSTR_0:13
.= dom (DataPart s2) by RELAT_1:61 ;
assume A4: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: DataPart s1 = DataPart s2

now :: thesis: for x being object st x in dom (DataPart s1) holds
(DataPart s1) . x = (DataPart s2) . x

let x be object ; :: thesis: ( x in dom (DataPart s1) implies (DataPart s1) . b₁ = (DataPart s2) . b₁ )
assume A5: x in dom (DataPart s1) ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁
then A6: x in (dom s1) /\ (Data-Locations ) by RELAT_1:61;
then A7: x in dom s1 by XBOOLE_0:def 4;

per cases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A7, Th1;

suppose A8: x is Int-Location ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

hereby :: thesis: verum

per cases ( x is read-write Int-Location or not x is read-write Int-Location ) ;

suppose A9: x is read-write Int-Location ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A2, A9
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; :: thesis: verum

end;

suppose A10: x is not read-write Int-Location ; :: thesis: (DataPart s1) . x = (DataPart s2) . x

reconsider a = x as Int-Location by A8;
a = intloc 0 by A10, Def2;
hence (DataPart s1) . x = s2 . a by A1, A5, FUNCT_1:47
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ;
:: thesis: verum

end;

end;

end;

end;

suppose A11: x is FinSeq-Location ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

thus (DataPart s1) . x = s1 . x by A5, FUNCT_1:47
.= s2 . x by A4, A11
.= (DataPart s2) . x by A3, A5, FUNCT_1:47 ; :: thesis: verum

end;

suppose x = IC ; :: thesis: (DataPart s1) . b₁ = (DataPart s2) . b₁

then not x in Data-Locations by STRUCT_0:3;
hence (DataPart s1) . x = (DataPart s2) . x by A6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then DataPart s1 c= DataPart s2 by A3, GRFUNC_1:2;
hence DataPart s1 = DataPart s2 by A3, GRFUNC_1:3; :: thesis: verum