def rot_hi.single.get

bend-kit-collections@0.1.4.1 · PROOF.bend:747

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

747def rot_hi.single.get(
748  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp),
749  ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp),
750  +x: K, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap<K, V>, +lh: O.OMap<K, V>,
751  +hi: O.OMap<K, V>, +lkk: {cmp(lk, k) == LT{} : Cmp}
752) -> {g(~K, ~V, ~cmp, O.OMap.bin(K, V, lk, lv, ll, O.OMap.bin(K, V, k, v, lh, hi)), x)
753      == g(~K, ~V, ~cmp, O.OBin{0, k, v, O.OBin{0, lk, lv, ll, lh}, hi}, x) : Maybe<&2, V>}:
754  +b = {O.OBin{0, k, v, lh, hi} : O.OMap<K, V>}
755  +l = {O.OBin{0, lk, lv, ll, b} : O.OMap<K, V>}
756  +ln = {O.OBin{0, lk, lv, ll, lh} : O.OMap<K, V>}
757  split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, v, ln, hi) : Maybe<&2, V>},
758    cmp(x, k),
759    e => split(c => {getc(~K, ~V, ~cmp, c, x, lv, ll, b)
760        == getc(~K, ~V, ~cmp, c, x, lv, ll, lh) : Maybe<&2, V>},
761      cmp(x, lk),
762      e2 => {==},
763      e2 => {==},
764      e2 => get.lt(~K, ~V, ~cmp, x, k, v, lh, hi, e)),
765    e => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{v} : Maybe<&2, V>}, x, k, eq(x, k, e),
766      mtr(V, g(~K, ~V, ~cmp, l, k), g(~K, ~V, ~cmp, b, k), Some{v},
767        get.gt(~K, ~V, ~cmp, k, lk, lv, ll, b, gt_of_lt(~K, ~cmp, ~flip, lk, k, lkk)),
768        get.here(~K, ~V, ~cmp, ~refl, k, v, lh, hi))),
769    +e => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, b, x), g(~K, ~V, ~cmp, hi, x),
770      get.gt(~K, ~V, ~cmp, x, lk, lv, ll, b,
771        gt_of_lt(~K, ~cmp, ~flip, lk, x,
772          trans(lk, k, x, lkk, gt_flip(~K, ~cmp, ~flip, x, k, e)))),
773      get.gt(~K, ~V, ~cmp, x, k, v, lh, hi, e)))