let k1 be Integer; for a being Int_position
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let a be Int_position; for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let s1, s2 be State of SCMPDS; ( DataPart s1 = DataPart s2 implies s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1)) )
assume A1:
DataPart s1 = DataPart s2
; s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
A2:
a in SCM-Data-Loc
by AMI_2:def 16;
then A3: s1 . a =
(DataPart s1) . a
by FUNCT_1:49, SCMPDS_2:84
.=
s2 . a
by A1, A2, FUNCT_1:49, SCMPDS_2:84
;
A4:
DataLoc ((s1 . a),k1) in SCM-Data-Loc
by AMI_2:def 16;
hence s1 . (DataLoc ((s1 . a),k1)) =
(DataPart s1) . (DataLoc ((s1 . a),k1))
by FUNCT_1:49, SCMPDS_2:84
.=
s2 . (DataLoc ((s2 . a),k1))
by A1, A4, A3, FUNCT_1:49, SCMPDS_2:84
;
verum