law omap_put_searchtree

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

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

158law omap_put_searchtree:
159  for ~K: Data
160  for ~V: Data
161  for ~cmp: K -> K -> Cmp
162  for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
163  for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
164  for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
165  for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
166  for m: O.OMap<K, V>
167  for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
168  for +k: K
169  for +v: V
170  {searchtree(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, m, k, v)) == True{} : Bool}