let t1, t2 be State of ; :: thesis: ( DataPart t1 = DataPart t2 implies Dstate t1 = Dstate t2 )
set s1 = Dstate t1;
set s2 = Dstate t2;

A1: now

let i be Instruction-Location of SCMPDS ; :: thesis: (Dstate t1) . i = (Dstate t2) . i
A2: i in NAT by AMI_1:def 4;
hence (Dstate t1) . i = goto 0 by Def1
.= (Dstate t2) . i by A2, Def1 ;
:: thesis: verum

end;

assume A3: DataPart t1 = DataPart t2 ; :: thesis: Dstate t1 = Dstate t2

A4: now

let a be Int_position ; :: thesis: (Dstate t1) . a = (Dstate t2) . a
A5: a in SCM-Data-Loc by SCMPDS_2:def 2;
hence (Dstate t1) . a = t1 . a by Def1
.= t2 . a by A3, SCMPDS_3:4
.= (Dstate t2) . a by A5, Def1 ;
:: thesis: verum

end;

IC (Dstate t1) = inspos 0 by Def1
.= IC (Dstate t2) by Def1 ;
hence Dstate t1 = Dstate t2 by A4, A1, SCMPDS_2:54; :: thesis: verum