let s1, s2 be State of SCMPDS; :: thesis: ( IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1 . a = s2 . a ; :: thesis: s1 = s2
A3: the carrier of SCMPDS = {()} \/ SCM-Data-Loc by
.= {()} \/ SCM-Data-Loc ;
A4: dom (s2 | (dom s2)) = (dom s2) /\ (dom s2) by RELAT_1:61
.= dom s2
.= {()} \/ SCM-Data-Loc by ;
A5: dom (s1 | (dom s1)) = (dom s1) /\ (dom s1) by RELAT_1:61
.= dom s1
.= {()} \/ SCM-Data-Loc by ;
A6: ( s1 | (dom s1) = s1 & s2 | (dom s2) = s2 ) by RELAT_1:69;
now :: thesis: for x being object st x in {()} \/ SCM-Data-Loc holds
(s1 | (dom s1)) . x = (s2 | (dom s2)) . x
let x be object ; :: thesis: ( x in {()} \/ SCM-Data-Loc implies (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1 )
assume A7: x in {()} \/ SCM-Data-Loc ; :: thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
per cases ( x in {()} or x in SCM-Data-Loc ) by ;
suppose x in {()} ; :: thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
then A8: x = IC by TARSKI:def 1;
hence (s1 | (dom s1)) . x = IC s1 by
.= (s2 | (dom s2)) . x by ;
:: thesis: verum
end;
suppose x in SCM-Data-Loc ; :: thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
then A9: x is Int_position by AMI_2:def 16;
thus (s1 | (dom s1)) . x = s1 . x by
.= s2 . x by A2, A9
.= (s2 | (dom s2)) . x by ; :: thesis: verum
end;
end;
end;
hence s1 = s2 by ; :: thesis: verum