law lookup_preserves_critbit

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/invariants.bend:125

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as Native

125# Lookup preserves even the strengthened discriminator/prefix predicate. The
126# general storage preservation law does not need an assumed valid input tree.
127law lookup_preserves_critbit:
128  for -V: Data
129  for +d: V
130  for +m: Map<&2, V>
131  for +key: String
132  {critbit(V, Native.lookup_map(V, Map.get(V, d, m, key))) == critbit(V, m) : Bool}