def rot_lo.double.get2

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

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

653def rot_lo.double.get2(
654  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp),
655  ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp),
656  +x: K, +k: K, +v: V, +lo: O.OMap<K, V>, +hk: K, +hv: V, +mk: K, +mv: V,
657  +ml: O.OMap<K, V>, +mh: O.OMap<K, V>, +hh: O.OMap<K, V>,
658  +khm: {cmp(k, mk) == LT{} : Cmp}, +mhk: {cmp(mk, hk) == LT{} : Cmp}
659) -> {g(~K, ~V, ~cmp, O.OMap.bin(K, V, mk, mv, O.OMap.bin(K, V, k, v, lo, ml),
660        O.OMap.bin(K, V, hk, hv, mh, hh)), x)
661      == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, O.OBin{0, hk, hv, O.OBin{0, mk, mv, ml, mh}, hh}}, x)
662      : Maybe<&2, V>}:
663  +a = {O.OBin{0, k, v, lo, ml} : O.OMap<K, V>}
664  +b = {O.OBin{0, hk, hv, mh, hh} : O.OMap<K, V>}
665  +l = {O.OBin{0, mk, mv, a, b} : O.OMap<K, V>}
666  +m = {O.OBin{0, mk, mv, ml, mh} : O.OMap<K, V>}
667  +r1 = {O.OBin{0, hk, hv, m, hh} : O.OMap<K, V>}
668  split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, v, lo, r1) : Maybe<&2, V>},
669    cmp(x, k),
670    +e => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, a, x), g(~K, ~V, ~cmp, lo, x),
671      get.lt(~K, ~V, ~cmp, x, mk, mv, a, b, trans(x, k, mk, e, khm)),
672      get.lt(~K, ~V, ~cmp, x, k, v, lo, ml, e)),
673    e => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{v} : Maybe<&2, V>}, x, k, eq(x, k, e),
674      mtr(V, g(~K, ~V, ~cmp, l, k), g(~K, ~V, ~cmp, a, k), Some{v},
675        get.lt(~K, ~V, ~cmp, k, mk, mv, a, b, khm),
676        get.here(~K, ~V, ~cmp, ~refl, k, v, lo, ml))),
677    +e => split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, hv, m, hh) : Maybe<&2, V>},
678      cmp(x, hk),
679      +e2 => split(c => {getc(~K, ~V, ~cmp, c, x, mv, a, b)
680          == getc(~K, ~V, ~cmp, c, x, mv, ml, mh) : Maybe<&2, V>},
681        cmp(x, mk),
682        e3 => get.gt(~K, ~V, ~cmp, x, k, v, lo, ml, e),
683        e3 => {==},
684        e3 => get.lt(~K, ~V, ~cmp, x, hk, hv, mh, hh, e2)),
685      e2 => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{hv} : Maybe<&2, V>}, x, hk, eq(x, hk, e2),
686        mtr(V, g(~K, ~V, ~cmp, l, hk), g(~K, ~V, ~cmp, b, hk), Some{hv},
687          get.gt(~K, ~V, ~cmp, hk, mk, mv, a, b, gt_of_lt(~K, ~cmp, ~flip, mk, hk, mhk)),
688          get.here(~K, ~V, ~cmp, ~refl, hk, hv, mh, hh))),
689      +e2 => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, b, x), g(~K, ~V, ~cmp, hh, x),
690        get.gt(~K, ~V, ~cmp, x, mk, mv, a, b,
691          gt_of_lt(~K, ~cmp, ~flip, mk, x,
692            trans(mk, hk, x, mhk, gt_flip(~K, ~cmp, ~flip, x, hk, e2)))),
693        get.gt(~K, ~V, ~cmp, x, hk, hv, mh, hh, e2))))