for term being bin-term
for s1, s2 being State of SCM st ( for dn being Element of NAT st dn <= max_Data-Loc_in term holds
s1 . (dl. dn) = s2 . (dl. dn) ) holds
term @ s1 = term @ s2