~/bend-docscommunity

proofs/containers/balanced_search_tree/vw.bend source

proofs/containers/balanced_search_tree/vw.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/order.bend as Oimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/balanced_search_tree/main.bend as Simport ../../../src/containers/balanced_search_tree.bend as Mimport ./state.bend as STimport ./mirror.bend as MIimport ./sim.bend as SMimport ./ok.bend as OKimport ./reads.bend as RDimport ./putm.bend as PMimport ./rmv.bend as RVimport ./cur.bend as CUimport ./vdef.bend as VD# The implementation's views refine the specification's: a view of a good# shadow is realized by the implementation's view and modelled by the# specification's over the shadow's model; every view operation gives the# real view (and answer) of a good view whose model is the specification's# result. (source: tools/generators/tm_hand/vw.src)# ---- making views ----def head_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +up: M.Bound<K>) -> VD.VOK(~K, ~V, ~cmp, S.head_map(K, V, ST.model(~K, ~V, ~cmp, sh), up), M.head_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), up)):  (MI.MV{sh, M.Unbounded{}, up, False{}}, (SM.head_map_s(~K, ~V, ~cmp, sh, up, OK.dg_good(~K, ~V, ~cmp, sh, hg)), ({==}, hg)))def tail_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound<K>) -> VD.VOK(~K, ~V, ~cmp, S.tail_map(K, V, ST.model(~K, ~V, ~cmp, sh), lw), M.tail_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw)):  (MI.MV{sh, lw, M.Unbounded{}, False{}}, (SM.tail_map_s(~K, ~V, ~cmp, sh, lw, OK.dg_good(~K, ~V, ~cmp, sh, hg)), ({==}, hg)))def descending_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.descending_map(K, V, ST.model(~K, ~V, ~cmp, sh)), M.descending_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):  (MI.MV{sh, M.Unbounded{}, M.Unbounded{}, True{}}, (SM.descending_map_s(~K, ~V, ~cmp, sh, OK.dg_good(~K, ~V, ~cmp, sh, hg)), ({==}, hg)))def view_reverse_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_reverse(K, V, VD.vmod(~K, ~V, ~cmp, w)), M.view_reverse(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))):  match w:    case MI.MV{+s, +lo2, +hi2, +d2}:      (MI.MV{s, lo2, hi2, Bool.not(d2)}, (SM.view_reverse_s(~K, ~V, ~cmp, MI.MV{s, lo2, hi2, d2}, OK.dg_good(~K, ~V, ~cmp, s, hw)), ({==}, hw)))def view_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh<K, V>, s2 => {M.view_finish(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap<K, V, cmp>} & ({S.view_finish(K, V, VD.vmod(~K, ~V, ~cmp, w)) == ST.model(~K, ~V, ~cmp, s2) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>:  match w:    case MI.MV{+s, +lo2, +hi2, +d2}:      (s, (SM.view_finish_s(~K, ~V, ~cmp, MI.MV{s, lo2, hi2, d2}, OK.dg_good(~K, ~V, ~cmp, s, hw)), ({==}, hw)))# ---- sub_map: the bounds checked ----def rmod(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Result<&1, &1, MI.MInvalid<K, V>, MI.MView<K, V>>) -> Result<&1, &1, S.InvalidView<K, V>, S.View<K, V>>:  match r:    case Done{w}:      Done{VD.vmod(~K, ~V, ~cmp, w)}    case Fail{MI.MI{s, e}}:      Fail{S.IV{ST.model(~K, ~V, ~cmp, s), e}}def rgood(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Result<&1, &1, MI.MInvalid<K, V>, MI.MView<K, V>>) -> Bool:  match r:    case Done{w}:      VD.vgood(~K, ~V, ~cmp, w)    case Fail{MI.MI{s, e}}:      ST.good(~K, ~V, ~cmp, s)def ROK(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sp: Result<&1, &1, S.InvalidView<K, V>, S.View<K, V>>, r: Result<&1, &1, M.InvalidView<K, V, cmp>, M.View<K, V, cmp>>) -> Type:  Sigma<&1, &1, Result<&1, &1, MI.MInvalid<K, V>, MI.MView<K, V>>, x => {r == MI.rr(~K, ~V, ~cmp, x) : Result<&1, &1, M.InvalidView<K, V, cmp>, M.View<K, V, cmp>>} & ({sp == rmod(~K, ~V, ~cmp, x) : Result<&1, &1, S.InvalidView<K, V>, S.View<K, V>>} & {rgood(~K, ~V, ~cmp, x) == True{} : Bool})>def bv_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +a: M.Bound<K>, +b: M.Bound<K>) -> {M.bounds_valid(~K, ~V, ~cmp, a, b) == S.bounds_valid(~K, ~cmp, a, b) : Bool}:  match a b:    case M.Unbounded{} M.Unbounded{}:      {==}    case M.Unbounded{} M.Inclusive{y}:      {==}    case M.Unbounded{} M.Exclusive{y}:      {==}    case M.Inclusive{x} M.Unbounded{}:      {==}    case M.Exclusive{x} M.Unbounded{}:      {==}    case M.Inclusive{+x} M.Inclusive{+y}:      CU.oo_eq(cmp(x, y), True{})    case M.Inclusive{+x} M.Exclusive{+y}:      CU.oo_eq(cmp(x, y), True{})    case M.Exclusive{+x} M.Inclusive{+y}:      CU.oo_eq(cmp(x, y), True{})    case M.Exclusive{+x} M.Exclusive{+y}:      CU.oo_eq(cmp(x, y), True{})def sub_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound<K>, +up: M.Bound<K>, +b: Bool) -> {S.view_checked(K, V, ST.model(~K, ~V, ~cmp, sh), lw, up, b) == rmod(~K, ~V, ~cmp, MI.view_checked(~K, ~V, ~cmp, sh, lw, up, False{}, b)) : Result<&1, &1, S.InvalidView<K, V>, S.View<K, V>>} & {rgood(~K, ~V, ~cmp, MI.view_checked(~K, ~V, ~cmp, sh, lw, up, False{}, b)) == True{} : Bool}:  match b:    case True{}:      ({==}, hg)    case False{}:      ({==}, hg)def sub_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound<K>, +up: M.Bound<K>) -> ROK(~K, ~V, ~cmp, S.sub_map(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), lw, up), M.sub_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw, up)):  %bv_eq(~K, ~V, ~cmp, lw, up) : ROK(~K, ~V, ~cmp, S.view_checked(K, V, ST.model(~K, ~V, ~cmp, sh), lw, up, _), M.sub_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw, up))  (MI.sub_map(~K, ~V, ~cmp, sh, lw, up), (SM.sub_map_s(~K, ~V, ~cmp, sh, lw, up, OK.dg_good(~K, ~V, ~cmp, sh, hg)), sub_b(~K, ~V, ~cmp, sh, hg, lw, up, M.bounds_valid(~K, ~V, ~cmp, lw, up))))# ---- get and contains_key: the key in range, then the map's ----def vget_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, +k: K, +b: Bool) -> {MI.view_get_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, b) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, b, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView<K, V> & Maybe<&2, V>}:  match b:    case True{}:      %Equal.sym(ST.Sh<K, V> & Maybe<&2, V>, MI.get(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), RD.get_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)) : {MI.view_value(~K, ~V, ~cmp, lo2, hi2, d2, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, True{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView<K, V> & Maybe<&2, V>}      {==}    case False{}:      {==}def vget_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, +k: K) -> {MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView<K, V> & Maybe<&2, V>}:  %Equal.sym(Bool, M.in_range(~K, ~V, ~cmp, k, lo2, hi2), S.in_range(~K, ~cmp, k, lo2, hi2), CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2)) : {MI.view_get_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView<K, V> & Maybe<&2, V>}  vget_b(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, d2, k, S.in_range(~K, ~cmp, k, lo2, hi2))def view_get_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_get(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):  match w:    case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}:      VD.vm_pok(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), M.view_get(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), SM.view_get_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), VD.vm_exact(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}), vget_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k), {==}, hw))def vcv_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w2: MI.MView<K, V>, +o: Maybe<&2, V>) -> {MI.view_contains_value(~K, ~V, ~cmp, (w2, o)) == (w2, S.is_some(V, o)) : MI.MView<K, V> & Bool}:  match o:    case None{}:      {==}    case Some{x}:      {==}def view_contains_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_contains_key(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):  match w:    case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}:      +hm = Equal.trans(MI.MView<K, V> & Bool, MI.view_contains_key(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), MI.view_contains_value(~K, ~V, ~cmp, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}))), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.is_some(V, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}))), L.subst(MI.MView<K, V> & Maybe<&2, V>, z => {MI.view_contains_value(~K, ~V, ~cmp, MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k)) == MI.view_contains_value(~K, ~V, ~cmp, z) : MI.MView<K, V> & Bool}, MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})), vget_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k), {==}), vcv_eq(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})))      VD.vm_pok(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_contains_key(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), M.view_contains_key(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), SM.view_contains_key_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), VD.vm_exact(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_contains_key(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.is_some(V, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})), hm, {==}, hw))# ---- put and remove: the key in range, then the map's ----# a map result rewrapped in the view's boundsdef rw_put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, r: ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, -a: M.TreeMap<K, V, cmp>, +o: Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, +h: {MI.rp(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, r) == (a, o) : M.TreeMap<K, V, cmp> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}) -> {MI.rvp(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, MI.view_put_finish(~K, ~V, ~cmp, lo2, hi2, d2, r)) == (M.View{a, lo2, hi2, d2}, o) : M.View<K, V, cmp> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}:  match r:    case Tuple{+m, +x}:      L.subst(M.TreeMap<K, V, cmp> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, z => {(M.View{ST.real(~K, ~V, ~cmp, m), lo2, hi2, d2}, x) == (M.View{Pair.fst(M.TreeMap<K, V, cmp>, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, z), lo2, hi2, d2}, Pair.snd(M.TreeMap<K, V, cmp>, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, z)) : M.View<K, V, cmp> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}, (ST.real(~K, ~V, ~cmp, m), x), (a, o), h, {==})def rw_val(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, r: ST.Sh<K, V> & Maybe<&2, V>, -a: M.TreeMap<K, V, cmp>, +o: Maybe<&2, V>, +h: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, r) == (a, o) : M.TreeMap<K, V, cmp> & Maybe<&2, V>}) -> {MI.rvp(~K, ~V, ~cmp, Maybe<&2, V>, MI.view_value(~K, ~V, ~cmp, lo2, hi2, d2, r)) == (M.View{a, lo2, hi2, d2}, o) : M.View<K, V, cmp> & Maybe<&2, V>}:  match r:    case Tuple{+m, +x}:      L.subst(M.TreeMap<K, V, cmp> & Maybe<&2, V>, z => {(M.View{ST.real(~K, ~V, ~cmp, m), lo2, hi2, d2}, x) == (M.View{Pair.fst(M.TreeMap<K, V, cmp>, Maybe<&2, V>, z), lo2, hi2, d2}, Pair.snd(M.TreeMap<K, V, cmp>, Maybe<&2, V>, z)) : M.View<K, V, cmp> & Maybe<&2, V>}, (ST.real(~K, ~V, ~cmp, m), x), (a, o), h, {==})def vput_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, +k: K, +v: V, p: OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v))) -> VD.VM(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, True{}), MI.view_put_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, lo2, hi2, d2, True{})):  match p:    case Tuple{+s2, Tuple{+o, Tuple{+h1, Tuple{+h2, h3}}}}:      %Equal.sym(S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), (ST.model(~K, ~V, ~cmp, s2), o), h2) : VD.VM(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.rewrap_put(K, V, lo2, hi2, d2, _), MI.view_put_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, lo2, hi2, d2, True{}))      (MI.MV{s2, lo2, hi2, d2}, (o, (rw_put(~K, ~V, ~cmp, lo2, hi2, d2, MI.put(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v), ST.real(~K, ~V, ~cmp, s2), o, h1), ({==}, h3))))def vput_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, +k: K, +v: V, +b: Bool) -> VD.VM(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, b), MI.view_put_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, lo2, hi2, d2, b)):  match b:    case True{}:      vput_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, d2, k, v, PM.put_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v))    case False{}:      (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, (Fail{M.Rejected{M.OutOfRange{}, k, v}}, ({==}, ({==}, hg))))def view_put_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K, +v: V) -> VD.VPOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.view_put(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, v), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k, v)):  match w:    case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}:      %CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2) : VD.VPOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, _), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k, v))      VD.vm_pok(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, M.in_range(~K, ~V, ~cmp, k, lo2, hi2)), MI.view_put(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, v), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k, v), SM.view_put_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, v, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), vput_b(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k, v, M.in_range(~K, ~V, ~cmp, k, lo2, hi2)))def vrem_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, +k: K, p: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k))) -> VD.VM(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, True{}), MI.view_remove_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, True{})):  match p:    case Tuple{+s2, Tuple{+o, Tuple{+h1, Tuple{+h2, h3}}}}:      %Equal.sym(S.Model<K, V> & Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), (ST.model(~K, ~V, ~cmp, s2), o), h2) : VD.VM(~K, ~V, ~cmp, Maybe<&2, V>, S.rewrap_val(K, V, lo2, hi2, d2, _), MI.view_remove_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, True{}))      (MI.MV{s2, lo2, hi2, d2}, (o, (rw_val(~K, ~V, ~cmp, lo2, hi2, d2, MI.remove(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.real(~K, ~V, ~cmp, s2), o, h1), ({==}, h3))))def vrem_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool, +k: K, +b: Bool) -> VD.VM(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, b), MI.view_remove_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, b)):  match b:    case True{}:      vrem_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, d2, k, RV.rm_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k))    case False{}:      (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, (None{}, ({==}, ({==}, hg))))def view_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView<K, V>, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)):  match w:    case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}:      %CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2) : VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, _), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k))      VD.vm_pok(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, M.in_range(~K, ~V, ~cmp, k, lo2, hi2)), MI.view_remove(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), SM.view_remove_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), vrem_b(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k, M.in_range(~K, ~V, ~cmp, k, lo2, hi2)))