let a be Int_position ; :: thesis: for s1, s2 being State of SCMPDS
for k1 being Integer st NPP s1 = NPP s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let s1, s2 be State of SCMPDS; :: thesis: for k1 being Integer st NPP s1 = NPP s2 holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let k1 be Integer; :: thesis: ( NPP s1 = NPP s2 implies s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1)) )
assume A1: NPP s1 = NPP s2 ; :: thesis: s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
hence s1 . (DataLoc ((s1 . a),k1)) = s1 . (DataLoc ((s2 . a),k1)) by Th13
.= s2 . (DataLoc ((s2 . a),k1)) by A1, Th13 ;
:: thesis: verum