let a be Int_position ; :: thesis: for s1, s2 being State of SCMPDS
for k1 being Integer st s1,s2 equal_outside NAT holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let s1, s2 be State of SCMPDS; :: thesis: for k1 being Integer st s1,s2 equal_outside NAT holds
s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let k1 be Integer; :: thesis: ( s1,s2 equal_outside NAT implies s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1)) )
assume A1: s1,s2 equal_outside NAT ; :: 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