proofs/containers/balanced_search_tree/vapi.bend source
proofs/containers/balanced_search_tree/vapi.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/list.bend as LLimport ../../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 ./ord.bend as ORimport ./reads.bend as RDimport ./cur.bend as CUimport ./vdef.bend as VDimport ./vsp.bend as VSimport ./vnav.bend as VNimport ./vit.bend as VIimport ./vsz.bend as VZimport ./vclr.bend as VCimport ./capi.bend as CA# The implementation's view reads, cursor, size and clear refine the# specification's, for every good view. (source: tools/generators/tm_hand/vapi.src)# ---- the view's cursor ----def cex_cst(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -mc: MI.MCursor<K, V>, -sp: S.Cursor<K, V>, -r: M.Cursor<K, V, cmp>, +hs: {r == MI.rc(~K, ~V, ~cmp, mc) : M.Cursor<K, V, cmp>}, p: Sigma<&1, &1, MI.MCursor<K, V>, c2 => {mc == c2 : MI.MCursor<K, V>} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {r == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: match p: case Tuple{+c2, Tuple{+h1, rest}}: (c2, (L.subst(MI.MCursor<K, V>, z => {r == MI.rc(~K, ~V, ~cmp, z) : M.Cursor<K, V, cmp>}, mc, c2, h1, hs), rest))def view_iterator_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}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.view_iterator(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.view_iterator(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: match w: case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: cex_cst(~K, ~V, ~cmp, MI.view_iterator(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), S.view_iterator(~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})), M.view_iterator(~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})), SM.view_iterator_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), VI.vit_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2))# ---- first, last and searches ----def view_extreme_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}, +first: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_extreme(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), first), M.view_extreme(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), first)): 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, M.Entry<K, V>>, S.view_extreme(~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}), first), MI.view_extreme(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, first), M.view_extreme(~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}), first), SM.view_extreme_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, first, 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, M.Entry<K, V>>, S.view_extreme(~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}), first), MI.view_extreme(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, first), MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, M.Entry<K, V>>, S.pick(Bool, d2, Bool.not(first), first), S.head(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.last(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))), VN.vx_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, first), {==}, hw))def view_first_entry_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}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_first_entry(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_first_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, True{})def view_last_entry_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}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_last_entry(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_last_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, False{})def view_nav_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, +higher: Bool, +incl: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, higher, incl), M.view_nav(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k, higher, incl)): 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, M.Entry<K, V>>, S.view_nav(~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, higher, incl), MI.view_nav(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, higher, incl), M.view_nav(~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, higher, incl), SM.view_nav_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, higher, incl, 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, M.Entry<K, V>>, S.view_nav(~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, higher, incl), MI.view_nav(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, higher, incl), MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.nav(~K, ~V, ~cmp, k, S.pick(Bool, d2, Bool.not(higher), higher), incl, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), VN.vn_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k, higher, incl), {==}, hw))def view_lower_entry_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, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, False{}, False{}), M.view_lower_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, False{}, False{})def view_floor_entry_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, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, False{}, True{}), M.view_floor_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, False{}, True{})def view_ceiling_entry_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, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, True{}, True{}), M.view_ceiling_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, True{}, True{})def view_higher_entry_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, M.Entry<K, V>>, S.view_nav(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, True{}, False{}), M.view_higher_entry(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, True{}, False{})# ---- size ----def view_size_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}) -> VD.VPOK(~K, ~V, ~cmp, Nat, S.view_size(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_size(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): 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, Nat, S.view_size(~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})), MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), M.view_size(~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})), SM.view_size_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, 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, Nat, S.view_size(~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})), MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), VZ.view_size_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2), {==}, hw))# ---- clear ----def vcf3(~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>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>})) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, False{}})), M.view_clear(~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, False{}}))): match r: case Tuple{hal, Tuple{hwa, hfb}}: %Equal.sym(M.Cursor<K, V, cmp>, M.view_iterator(~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, False{}})), MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}}), Equal.trans(M.Cursor<K, V, cmp>, M.view_iterator(~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, False{}})), MI.rc(~K, ~V, ~cmp, MI.view_iterator(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}})), MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}}), SM.view_iterator_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), VS.cong(ST.Sh<K, V> & Nat, M.Cursor<K, V, cmp>, z => MI.rc(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, True{}, z)), MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1))) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+n, M.iterator_next(~K, ~V, ~cmp, _))) +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), LL.length_append(M.Entry<K, V>, xa, xb), N.add_comm(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb))) %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, lo2, hi2, False{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+_, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})))) +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), h2, Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), VS.start_fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.head(M.Entry<K, V>, xb), hfb))) +hsp0 = Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}}), S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, xb)), None{}, lo2, hi2, True{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, xa, xb)}, S.key_m(K, V, S.head(M.Entry<K, V>, xb)), None{}, lo2, hi2, True{}}, VS.cong(Maybe<&2, K>, S.Cursor<K, V>, z => S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, z, None{}, lo2, hi2, True{}}, CU.ck(~K, nl, j), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), hk), VS.cong(List<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.head(M.Entry<K, V>, xb)), None{}, lo2, hi2, True{}}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab)) +hord0 = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) +eo = Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.outside(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), VC.out_app(~K, ~V, ~cmp, lo2, hi2, xa, xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, q, S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), S.outside(~K, ~V, ~cmp, lo2, hi2, xa), xa, VC.out_id(~K, ~V, ~cmp, lo2, hi2, xa, hwa)))) L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})))), S.VW{S.TM{l, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, xb))}, lo2, hi2, False{}}, S.VW{S.TM{l, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, lo2, hi2, False{}}, VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, z}, lo2, hi2, False{}}, SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry<K, V>, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), eo)), VC.clf(~K, ~V, ~cmp, ~o, ~(nc => nh => CA.iterator_next_ok(~K, ~V, ~cmp, ~o, nc, nh)), ~(rc => rh => CA.iterator_remove_ok(~K, ~V, ~cmp, ~o, rc, rh)), l, lo2, hi2, SC.length(M.Entry<K, V>, xa), xa, xb, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}}, None{}, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, True{}), hsp0, hord0, hal))def vcf2(~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>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, False{}})), M.view_clear(~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, False{}}))): match sp: case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}: vcf3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)def vcf1(~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>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, False{}})), M.view_clear(~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, False{}}))): match r: case Tuple{h2, h3}: vcf2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_fal(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))def vcf(~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>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, False{}})), M.view_clear(~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, False{}}))): match r: case Tuple{+j, Tuple{+h1, r2}}: vcf1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)def vcb3(~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>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>})) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, True{}})), M.view_clear(~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, True{}}))): match r: case Tuple{hbu, Tuple{hwb, hlb}}: %Equal.sym(M.Cursor<K, V, cmp>, M.view_iterator(~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, True{}})), MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}}), Equal.trans(M.Cursor<K, V, cmp>, M.view_iterator(~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, True{}})), MI.rc(~K, ~V, ~cmp, MI.view_iterator(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}})), MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}}), SM.view_iterator_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), VS.cong(ST.Sh<K, V> & Nat, M.Cursor<K, V, cmp>, z => MI.rc(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, False{}, z)), MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1))) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+n, M.iterator_next(~K, ~V, ~cmp, _))) +err = LL.spec_rev_rev(M.Entry<K, V>, xa) +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), LL.length_append(M.Entry<K, V>, xa, xb), VS.cong(Nat, Nat, q => Nat.add(q, SC.length(M.Entry<K, V>, xb)), SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(Nat, SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xa), LL.length_rev(M.Entry<K, V>, xa)))) %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : VD.VOK(~K, ~V, ~cmp, S.VW{S.TM{l, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, lo2, hi2, True{}}, M.view_clear_loop(~K, ~V, ~cmp, 1n+_, M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})))) +hab2 = L.subst(List<&2, M.Entry<K, V>>, q => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, q, xb) : List<&2, M.Entry<K, V>>}, xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err), hab) +hk0 = Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), VS.start_lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last(M.Entry<K, V>, xa), Equal.trans(Maybe<&2, M.Entry<K, V>>, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}), S.last(M.Entry<K, V>, xa), hlb, OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, xa))))) +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), h2, hk0), VS.cong(List<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, S.last(M.Entry<K, V>, q)), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err))) +hsp0 = Equal.trans(S.Cursor<K, V>, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}}), S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), None{}, lo2, hi2, False{}}, S.CR{S.TM{l, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xb)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), None{}, lo2, hi2, False{}}, VS.cong(Maybe<&2, K>, S.Cursor<K, V>, z => S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, z, None{}, lo2, hi2, False{}}, CU.ck(~K, nl, j), S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), hk), VS.cong(List<&2, M.Entry<K, V>>, S.Cursor<K, V>, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), None{}, lo2, hi2, False{}}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xb), hab2)) +hord0 = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xb), hab2, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) +eo1 = Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.outside(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), VC.out_app(~K, ~V, ~cmp, lo2, hi2, xa, xb)) +eo2 = Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), xb), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), q), S.outside(~K, ~V, ~cmp, lo2, hi2, xb), xb, VC.out_id(~K, ~V, ~cmp, lo2, hi2, xb, hwb)), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, q), xb), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err))) +eo = Equal.trans(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), xb), eo1, eo2) L.subst(S.View<K, V>, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})))), S.VW{S.TM{l, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), xb)}, lo2, hi2, True{}}, S.VW{S.TM{l, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, lo2, hi2, True{}}, VS.cong(List<&2, M.Entry<K, V>>, S.View<K, V>, z => S.VW{S.TM{l, z}, lo2, hi2, True{}}, SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), xb), S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.sym(List<&2, M.Entry<K, V>>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry<K, V>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), xb), eo)), VC.clb(~K, ~V, ~cmp, ~o, ~(nc => nh => CA.iterator_next_ok(~K, ~V, ~cmp, ~o, nc, nh)), ~(rc => rh => CA.iterator_remove_ok(~K, ~V, ~cmp, ~o, rc, rh)), l, lo2, hi2, SC.length(M.Entry<K, V>, xb), xb, SC.reverse(M.Entry<K, V>, xa), MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}}, None{}, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, False{}), hsp0, hord0, VS.allbu_rev(~K, ~V, ~cmp, hi2, xa, hbu)))def vcb2(~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>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>}))>>) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, True{}})), M.view_clear(~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, True{}}))): match sp: case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}: vcb3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)def vcb1(~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>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, True{}})), M.view_clear(~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, True{}}))): match r: case Tuple{h2, h3}: vcb2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_lbu(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))def vcb(~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>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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, True{}})), M.view_clear(~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, True{}}))): match r: case Tuple{+j, Tuple{+h1, r2}}: vcb1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)def vclr_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) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~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})), M.view_clear(~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}))): match d2: case True{}: vcb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, hi2, False{})) case False{}: vcf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, True{}))def view_clear_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}) -> VD.VOK(~K, ~V, ~cmp, S.view_clear(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)), M.view_clear(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): match w: case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: vclr_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2)