let s1, s2 be State of SCMPDS ; :: thesis: ( ( for x being set holds
( ( x in SCM-Data-Loc implies s1 . x = t . x ) & ( x in NAT implies s1 . x = goto 0 ) & ( x = IC SCMPDS implies s1 . x = 0 ) ) ) & ( for x being set holds
( ( x in SCM-Data-Loc implies s2 . x = t . x ) & ( x in NAT implies s2 . x = goto 0 ) & ( x = IC SCMPDS implies s2 . x = 0 ) ) ) implies s1 = s2 )
assume that
A3: for x being set holds
( ( x in SCM-Data-Loc implies s1 . x = t . x ) & ( x in NAT implies s1 . x = goto 0 ) & ( x = IC SCMPDS implies s1 . x = 0 ) ) and
A4: for x being set holds
( ( x in SCM-Data-Loc implies s2 . x = t . x ) & ( x in NAT implies s2 . x = goto 0 ) & ( x = IC SCMPDS implies s2 . x = 0 ) ) ; :: thesis: s1 = s2

A5: now

let a be Int_position ; :: thesis: s1 . a = s2 . a
A6: a in SCM-Data-Loc by SCMPDS_2:def 2;
hence s1 . a = t . a by A3
.= s2 . a by A4, A6 ;
:: thesis: verum

end;

A7: now

let i be Element of NAT ; :: thesis: s1 . i = s2 . i
thus s1 . i = goto 0 by A3
.= s2 . i by A4 ; :: thesis: verum

end;

IC s1 = 0 by A3
.= IC s2 by A4 ;
hence s1 = s2 by A5, A7, SCMPDS_2:54; :: thesis: verum