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