1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/order.bend as O 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/balanced_search_tree/main.bend as S 8 import ../../../src/containers/balanced_search_tree.bend as M 9 import ./state.bend as ST 10 import ./mirror.bend as MI 11 import ./sim.bend as SM 12 import ./ok.bend as OK 13 import ./ord.bend as OR 14 import ./reads.bend as RD 15 import ./cur.bend as CU 16 import ./vdef.bend as VD 17 import ./vsp.bend as VS 18 import ./vnav.bend as VN 19 import ./vit.bend as VI 20 import ./vsz.bend as VZ 21 import ./vclr.bend as VC 22 import ./capi.bend as CA 23 24 # The implementation's view reads, cursor, size and clear refine the 25 # specification's, for every good view. (source: tools/generators/tm_hand/vapi.src) 26 27 28 # ---- the view's cursor ---- 29 30 31 def cex_cst(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -mc: MI.MCursor, -sp: S.Cursor, -r: M.Cursor, +hs: {r == MI.rc(~K, ~V, ~cmp, mc) : M.Cursor}, p: Sigma<&1, &1, MI.MCursor, c2 => {mc == c2 : MI.MCursor} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>) -> Sigma<&1, &1, MI.MCursor, c2 => {r == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 32 match p: 33 case Tuple{+c2, Tuple{+h1, rest}}: 34 (c2, (L.subst(MI.MCursor, z => {r == MI.rc(~K, ~V, ~cmp, z) : M.Cursor}, mc, c2, h1, hs), rest)) 35 36 def view_iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor, c2 => {M.view_iterator(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor} & ({S.view_iterator(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>: 37 match w: 38 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 39 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)) 40 41 # ---- first, last and searches ---- 42 43 44 def view_extreme_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +first: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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)): 45 match w: 46 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 47 VD.vm_pok(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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>, 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>, S.pick(Bool, d2, Bool.not(first), first), S.head(M.Entry, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.last(M.Entry, 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)) 48 49 def view_first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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))): 50 view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, True{}) 51 52 def view_last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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))): 53 view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, False{}) 54 55 56 def view_nav_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K, +higher: Bool, +incl: Bool) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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)): 57 match w: 58 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 59 VD.vm_pok(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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>, 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)) 60 61 62 def view_lower_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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)): 63 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, False{}, False{}) 64 65 def view_floor_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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)): 66 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, False{}, True{}) 67 68 def view_ceiling_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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)): 69 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, True{}, True{}) 70 71 def view_higher_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry>, 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)): 72 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, True{}, False{}) 73 74 # ---- size ---- 75 76 def view_size_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +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))): 77 match w: 78 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 79 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, 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)) 80 81 # ---- clear ---- 82 83 84 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>, +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, +hi2: M.Bound, +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 & 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>, +xb: List<&2, M.Entry>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>}, r: {VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>})) -> 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{}}))): 85 match r: 86 case Tuple{hal, Tuple{hwa, hfb}}: 87 %Equal.sym(M.Cursor, 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, 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 & Nat, M.Cursor, 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, _))) 88 +hnt = Equal.trans(Nat, SC.length(M.Entry, SC.append(M.Entry, xa, xb)), Nat.add(SC.length(M.Entry, xa), SC.length(M.Entry, xb)), Nat.add(SC.length(M.Entry, xb), SC.length(M.Entry, xa)), LL.length_append(M.Entry, xa, xb), N.add_comm(SC.length(M.Entry, xa), SC.length(M.Entry, xb))) 89 %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry, xb), SC.length(M.Entry, xa)), Equal.trans(Nat, n, SC.length(M.Entry, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry, xb), SC.length(M.Entry, 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry, SC.append(M.Entry, xa, xb)), Nat.add(SC.length(M.Entry, xb), SC.length(M.Entry, xa)), VS.cong(List<&2, M.Entry>, Nat, q => SC.length(M.Entry, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, 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{}})))) 90 +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, 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, xb)), VS.start_fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry>, 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, xb), hfb))) 91 +hsp0 = Equal.trans(S.Cursor, 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, xb)), None{}, lo2, hi2, True{}}, S.CR{S.TM{l, SC.append(M.Entry, xa, xb)}, S.key_m(K, V, S.head(M.Entry, xb)), None{}, lo2, hi2, True{}}, VS.cong(Maybe<&2, K>, S.Cursor, 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, xb)), hk), VS.cong(List<&2, M.Entry>, S.Cursor, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.head(M.Entry, xb)), None{}, lo2, hi2, True{}}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, xa, xb), hab)) 92 +hord0 = L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, xa, xb), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 93 +eo = Equal.trans(List<&2, M.Entry>, 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, xa, xb)), SC.append(M.Entry, xa, S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), VS.cong(List<&2, M.Entry>, List<&2, M.Entry>, q => S.outside(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, xa, xb), hab), Equal.trans(List<&2, M.Entry>, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry, xa, xb)), SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry, 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>, List<&2, M.Entry>, q => SC.append(M.Entry, 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)))) 94 L.subst(S.View, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry, xb), SC.length(M.Entry, 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, 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>, S.View, z => S.VW{S.TM{l, z}, lo2, hi2, False{}}, SC.append(M.Entry, 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>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry, 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, 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)) 95 96 97 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>, +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, +hi2: M.Bound, +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 & 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>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry, xb) : Maybe<&2, M.Entry>}))>>) -> 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{}}))): 98 match sp: 99 case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}: 100 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) 101 102 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>, +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, +hi2: M.Bound, +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 & 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{}}))): 103 match r: 104 case Tuple{h2, h3}: 105 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))) 106 107 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>, +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, +hi2: M.Bound, 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 & 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{}}))): 108 match r: 109 case Tuple{+j, Tuple{+h1, r2}}: 110 vcf1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2) 111 112 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>, +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, +hi2: M.Bound, +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 & 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>, +xb: List<&2, M.Entry>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>}, r: {VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry, S.last(M.Entry, xa), None{}) : Maybe<&2, M.Entry>})) -> 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{}}))): 113 match r: 114 case Tuple{hbu, Tuple{hwb, hlb}}: 115 %Equal.sym(M.Cursor, 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, 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 & Nat, M.Cursor, 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, _))) 116 +err = LL.spec_rev_rev(M.Entry, xa) 117 +hnt = Equal.trans(Nat, SC.length(M.Entry, SC.append(M.Entry, xa, xb)), Nat.add(SC.length(M.Entry, xa), SC.length(M.Entry, xb)), Nat.add(SC.length(M.Entry, SC.reverse(M.Entry, xa)), SC.length(M.Entry, xb)), LL.length_append(M.Entry, xa, xb), VS.cong(Nat, Nat, q => Nat.add(q, SC.length(M.Entry, xb)), SC.length(M.Entry, xa), SC.length(M.Entry, SC.reverse(M.Entry, xa)), Equal.sym(Nat, SC.length(M.Entry, SC.reverse(M.Entry, xa)), SC.length(M.Entry, xa), LL.length_rev(M.Entry, xa)))) 118 %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry, SC.reverse(M.Entry, xa)), SC.length(M.Entry, xb)), Equal.trans(Nat, n, SC.length(M.Entry, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry, SC.reverse(M.Entry, xa)), SC.length(M.Entry, 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry, SC.append(M.Entry, xa, xb)), Nat.add(SC.length(M.Entry, SC.reverse(M.Entry, xa)), SC.length(M.Entry, xb)), VS.cong(List<&2, M.Entry>, Nat, q => SC.length(M.Entry, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, 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{}})))) 119 +hab2 = L.subst(List<&2, M.Entry>, q => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry, q, xb) : List<&2, M.Entry>}, xa, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), Equal.sym(List<&2, M.Entry>, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), xa, err), hab) 120 +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, xa)), VS.start_lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry>, 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, xa), Equal.trans(Maybe<&2, M.Entry>, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), OR.orm(M.Entry, S.last(M.Entry, xa), None{}), S.last(M.Entry, xa), hlb, OR.orm_none(M.Entry, S.last(M.Entry, xa))))) 121 +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.key_m(K, V, S.last(M.Entry, xa)), S.key_m(K, V, S.last(M.Entry, SC.reverse(M.Entry, SC.reverse(M.Entry, 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, xa)), h2, hk0), VS.cong(List<&2, M.Entry>, Maybe<&2, K>, q => S.key_m(K, V, S.last(M.Entry, q)), xa, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), Equal.sym(List<&2, M.Entry>, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), xa, err))) 122 +hsp0 = Equal.trans(S.Cursor, 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, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)))), None{}, lo2, hi2, False{}}, S.CR{S.TM{l, SC.append(M.Entry, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), xb)}, S.key_m(K, V, S.last(M.Entry, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)))), None{}, lo2, hi2, False{}}, VS.cong(Maybe<&2, K>, S.Cursor, 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, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)))), hk), VS.cong(List<&2, M.Entry>, S.Cursor, z => S.CR{S.TM{l, z}, S.key_m(K, V, S.last(M.Entry, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)))), None{}, lo2, hi2, False{}}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), xb), hab2)) 123 +hord0 = L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), xb), hab2, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 124 +eo1 = Equal.trans(List<&2, M.Entry>, 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, xa, xb)), SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), VS.cong(List<&2, M.Entry>, List<&2, M.Entry>, q => S.outside(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, xa, xb), hab), VC.out_app(~K, ~V, ~cmp, lo2, hi2, xa, xb)) 125 +eo2 = Equal.trans(List<&2, M.Entry>, SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), xb), SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry, SC.reverse(M.Entry, xa))), xb), VS.cong(List<&2, M.Entry>, List<&2, M.Entry>, q => SC.append(M.Entry, 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>, List<&2, M.Entry>, q => SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, q), xb), xa, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), Equal.sym(List<&2, M.Entry>, SC.reverse(M.Entry, SC.reverse(M.Entry, xa)), xa, err))) 126 +eo = Equal.trans(List<&2, M.Entry>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, xa), S.outside(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry, SC.reverse(M.Entry, xa))), xb), eo1, eo2) 127 L.subst(S.View, z => VD.VOK(~K, ~V, ~cmp, z, M.view_clear_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry, SC.reverse(M.Entry, xa)), SC.length(M.Entry, 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, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry, SC.reverse(M.Entry, 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>, S.View, z => S.VW{S.TM{l, z}, lo2, hi2, True{}}, SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry, SC.reverse(M.Entry, xa))), xb), S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.sym(List<&2, M.Entry>, S.outside(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry, S.outside(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry, SC.reverse(M.Entry, 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, xb), xb, SC.reverse(M.Entry, 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))) 128 129 130 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>, +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, +hi2: M.Bound, +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 & 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>, xa => Sigma<&1, &1, List<&2, M.Entry>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry, xa, xb) : List<&2, M.Entry>} & ({VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry, S.last(M.Entry, xa), None{}) : Maybe<&2, M.Entry>}))>>) -> 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{}}))): 131 match sp: 132 case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}: 133 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) 134 135 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>, +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, +hi2: M.Bound, +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 & 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{}}))): 136 match r: 137 case Tuple{h2, h3}: 138 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))) 139 140 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>, +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, +hi2: M.Bound, 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 & 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{}}))): 141 match r: 142 case Tuple{+j, Tuple{+h1, r2}}: 143 vcb1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2) 144 145 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>, +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, +hi2: M.Bound, +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}))): 146 match d2: 147 case True{}: 148 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{})) 149 case False{}: 150 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{})) 151 152 def view_clear_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +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))): 153 match w: 154 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 155 vclr_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2)