law omap_del_searchtree

bend-kit-collections@0.1.4.1 · LAWS.bend:172

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O

172law omap_del_searchtree:
173  for ~K: Data
174  for ~V: Data
175  for ~cmp: K -> K -> Cmp
176  for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
177  for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
178  for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
179  for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
180  for m: O.OMap<K, V>
181  for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
182  for +k: K
183  {searchtree(~K, ~V, ~cmp, O.OMap.del(~K, ~V, ~cmp, m, k)) == True{} : Bool}