proofs/containers/balanced_search_tree/vapi.bend
bend-collections-laws-containers@1.0.0.0 · 155 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
8import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/sim.bend as SM
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as OK
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as OR
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/reads.bend as RD
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cur.bend as CU
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vdef.bend as VD
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsp.bend as VS
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vnav.bend as VN
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vit.bend as VI
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vsz.bend as VZ
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/vclr.bend as VC
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/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
31def 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})>:
32 match p:
33 case Tuple{+c2, Tuple{+h1, rest}}:
34 (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))
35
36def 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})>:
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
44def 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)):
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<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))
48
49def 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))):
50 view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, True{})
51
52def 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))):
53 view_extreme_ok(~K, ~V, ~cmp, ~o, w, hw, False{})
54
55
56def 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)):
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<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))
60
61
62def 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)):
63 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, False{}, False{})
64
65def 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)):
66 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, False{}, True{})
67
68def 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)):
69 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, True{}, True{})
70
71def 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)):
72 view_nav_ok(~K, ~V, ~cmp, ~o, w, hw, k, True{}, False{})
73
74# ---- size ----
75
76def 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))):
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<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))
80
81# ---- clear ----
82
83
84def 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{}}))):
85 match r:
86 case Tuple{hal, Tuple{hwa, hfb}}:
87 %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, _)))
88 +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)))
89 %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{}}))))
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<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)))
91 +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))
92 +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))
93 +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))))
94 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))
95
96
97def 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{}}))):
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
102def 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{}}))):
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
107def 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{}}))):
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
112def 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{}}))):
113 match r:
114 case Tuple{hbu, Tuple{hwb, hlb}}:
115 %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, _)))
116 +err = LL.spec_rev_rev(M.Entry<K, V>, xa)
117 +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))))
118 %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{}}))))
119 +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)
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<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)))))
121 +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)))
122 +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))
123 +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))
124 +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))
125 +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)))
126 +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)
127 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)))
128
129
130def 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{}}))):
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
135def 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{}}))):
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
140def 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{}}))):
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
145def 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}))):
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
152def 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))):
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)