proofs/containers/balanced_search_tree/nsf.bend
bend-collections-laws-containers@1.0.0.0 · 655 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/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
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/dynamic_array/state.bend as DAS
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/bk.bend as BK
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsr.bend as NR
12
13# One field of the TreeMap's node store: the field list of a node list
14# (length, reads, updates, appends, dropping the last) and the field's block
15# under Array.get / Array.set / doubling, for every node list of length at
16# most the capacity 2^d, d <= l <= 31.
17
18
19# Some{x} gives x
20def unsome(~K: Data, m: Maybe<&2, M.Node<K>>, +dv: M.Node<K>) -> M.Node<K>:
21 match m:
22 case None{}:
23 dv
24 case Some{x}:
25 x
26
27def mb(~K: Data, m: Maybe<&2, M.Node<K>>) -> Bool:
28 match m:
29 case None{}:
30 False{}
31 case Some{x}:
32 True{}
33
34def unsomeA(-A: Data, m: Maybe<&2, A>, +dv: A) -> A:
35 match m:
36 case None{}:
37 dv
38 case Some{x}:
39 x
40
41# updating a slot with the value it holds changes nothing
42def upd_same(-A: Data, +ys: List<&2, A>, +i: Nat, +z: A, +h: {SC.nth(A, ys, i) == Some{z} : Maybe<&2, A>}) -> {SC.update(A, ys, i, z) == ys : List<&2, A>}:
43 match ys i:
44 case Nil{} _:
45 {==}
46 case Con{+x, r} 0n:
47 Equal.cong(Maybe<&2, A>, List<&2, A>, w => Con{unsomeA(A, w, x), r}, Some{z}, Some{x}, Equal.sym(Maybe<&2, A>, Some{x}, Some{z}, h))
48 case Con{+x, +r} 1n+q:
49 LL.cons_cong(A, x, SC.update(A, r, q, z), r, upd_same(A, r, q, z, h))
50
51def tags_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.tags(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
52 match xs:
53 case Nil{}:
54 {==}
55 case Con{x, +r}:
56 N.succ_cong(SC.length(Nat, NR.tags(~K, r)), SC.length(M.Node<K>, r), tags_len(~K, r))
57
58def tags_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.tags(~K, xs), i) == Some{M.ntag(~K, y)} : Maybe<&2, Nat>}:
59 match xs i:
60 case Nil{} _:
61 Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.ntag(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
62 case Con{+x, r} 0n:
63 Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.ntag(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
64 case Con{x, +r} 1n+q:
65 tags_nth(~K, r, q, y, h)
66
67def tags_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.tags(~K, xs), i, M.ntag(~K, y)) == NR.tags(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
68 match xs i:
69 case Nil{} _:
70 {==}
71 case Con{x, r} 0n:
72 {==}
73 case Con{+x, +r} 1n+q:
74 LL.cons_cong(Nat, M.ntag(~K, x), SC.update(Nat, NR.tags(~K, r), q, M.ntag(~K, y)), NR.tags(~K, SC.update(M.Node<K>, r, q, y)), tags_upd(~K, r, q, y))
75
76def tags_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.tags(~K, xs), M.ntag(~K, y)) == NR.tags(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
77 match xs:
78 case Nil{}:
79 {==}
80 case Con{+x, +r}:
81 LL.cons_cong(Nat, M.ntag(~K, x), SC.snoc(Nat, NR.tags(~K, r), M.ntag(~K, y)), NR.tags(~K, SC.snoc(M.Node<K>, r, y)), tags_snoc(~K, r, y))
82
83def tags_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.tags(~K, xs)) == NR.tags(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
84 match xs:
85 case Nil{}:
86 {==}
87 case Con{x, Nil{}}:
88 {==}
89 case Con{+x, Con{+y, +t}}:
90 LL.cons_cong(Nat, M.ntag(~K, x), SC.init(Nat, NR.tags(~K, Con{y, t})), NR.tags(~K, SC.init(M.Node<K>, Con{y, t})), tags_init(~K, Con{y, t}))
91
92# the field block: a slot below the length reads the field
93def tag_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), M.ntag(~K, y)) : Array<Nat> & Nat}:
94 +fl = NR.tags(~K, xs)
95 +t = BK.bk(Nat, d, fl, 0n)
96 +hlen = tags_len(~K, xs)
97 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
98 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
99 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
100 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
101 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
102 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.ntag(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.ntag(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), tags_nth(~K, xs, i, y, hy)))
103 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.ntag(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
104 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
105 AR.get(Nat, d, t, U32.from_nat(i), M.ntag(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
106
107# a slot below the length written with a node's field
108def tag_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
109 +fl = NR.tags(~K, xs)
110 +t = BK.bk(Nat, d, fl, 0n)
111 +hlen = tags_len(~K, xs)
112 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
113 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
114 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
115 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
116 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
117 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.ntag(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.ntag(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), tags_nth(~K, xs, i, y0, hy0)))
118 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.ntag(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
119 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
120 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.ntag(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.ntag(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.ntag(~K, y), M.ntag(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
121 %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.ntag(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
122 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.ntag(~K, y)), BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.ntag(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.ntag(~K, y)), 0n), BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.ntag(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.ntag(~K, y)), NR.tags(~K, SC.update(M.Node<K>, xs, i, y)), tags_upd(~K, xs, i, y))))
123
124# the slot at the length (inside the capacity) written: an append
125def tag_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.ntag(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
126 +fl = NR.tags(~K, xs)
127 +t = BK.bk(Nat, d, fl, 0n)
128 +n = SC.length(M.Node<K>, xs)
129 +hlen = tags_len(~K, xs)
130 +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
131 +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
132 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
133 +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
134 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
135 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
136 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.ntag(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.ntag(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.ntag(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
137 %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.ntag(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
138 %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.ntag(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
139 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.ntag(~K, y)), BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.ntag(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.ntag(~K, y)), 0n), BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.ntag(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.ntag(~K, y)), NR.tags(~K, SC.snoc(M.Node<K>, xs, y)), tags_snoc(~K, xs, y))))
140
141# the block doubled with a default half
142def tag_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)) : Array<Nat>}:
143 +fl = NR.tags(~K, xs)
144 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), tags_len(~K, xs)), hc)
145 %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
146 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
147
148# the last slot reset to the encoding of Free{0}: a pop
149def tag_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(m), M.ntag(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
150 +fl = NR.tags(~K, xs)
151 +t = BK.bk(Nat, d, fl, 0n)
152 +hlen = tags_len(~K, xs)
153 +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
154 +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
155 +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
156 +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
157 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
158 +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
159 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.ntag(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.ntag(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), tags_nth(~K, xs, m, y0, hy0)))
160 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.ntag(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
161 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
162 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.ntag(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
163 %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
164 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.tags(~K, SC.init(M.Node<K>, xs)), tags_init(~K, xs))))
165
166# updating a node that keeps this field leaves the field list
167def tags_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.ntag(~K, x) == M.ntag(~K, y) : Nat}) -> {NR.tags(~K, SC.update(M.Node<K>, xs, i, x)) == NR.tags(~K, xs) : List<&2, Nat>}:
168 %tags_upd(~K, xs, i, x) : {_ == NR.tags(~K, xs) : List<&2, Nat>}
169 %Equal.sym(Nat, M.ntag(~K, x), M.ntag(~K, y), he) : {SC.update(Nat, NR.tags(~K, xs), i, _) == NR.tags(~K, xs) : List<&2, Nat>}
170 upd_same(Nat, NR.tags(~K, xs), i, M.ntag(~K, y), tags_nth(~K, xs, i, y, hy))
171
172def lefts_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.lefts(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
173 match xs:
174 case Nil{}:
175 {==}
176 case Con{x, +r}:
177 N.succ_cong(SC.length(Nat, NR.lefts(~K, r)), SC.length(M.Node<K>, r), lefts_len(~K, r))
178
179def lefts_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.lefts(~K, xs), i) == Some{M.nleft(~K, y)} : Maybe<&2, Nat>}:
180 match xs i:
181 case Nil{} _:
182 Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.nleft(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
183 case Con{+x, r} 0n:
184 Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.nleft(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
185 case Con{x, +r} 1n+q:
186 lefts_nth(~K, r, q, y, h)
187
188def lefts_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.lefts(~K, xs), i, M.nleft(~K, y)) == NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
189 match xs i:
190 case Nil{} _:
191 {==}
192 case Con{x, r} 0n:
193 {==}
194 case Con{+x, +r} 1n+q:
195 LL.cons_cong(Nat, M.nleft(~K, x), SC.update(Nat, NR.lefts(~K, r), q, M.nleft(~K, y)), NR.lefts(~K, SC.update(M.Node<K>, r, q, y)), lefts_upd(~K, r, q, y))
196
197def lefts_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.lefts(~K, xs), M.nleft(~K, y)) == NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
198 match xs:
199 case Nil{}:
200 {==}
201 case Con{+x, +r}:
202 LL.cons_cong(Nat, M.nleft(~K, x), SC.snoc(Nat, NR.lefts(~K, r), M.nleft(~K, y)), NR.lefts(~K, SC.snoc(M.Node<K>, r, y)), lefts_snoc(~K, r, y))
203
204def lefts_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.lefts(~K, xs)) == NR.lefts(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
205 match xs:
206 case Nil{}:
207 {==}
208 case Con{x, Nil{}}:
209 {==}
210 case Con{+x, Con{+y, +t}}:
211 LL.cons_cong(Nat, M.nleft(~K, x), SC.init(Nat, NR.lefts(~K, Con{y, t})), NR.lefts(~K, SC.init(M.Node<K>, Con{y, t})), lefts_init(~K, Con{y, t}))
212
213# the field block: a slot below the length reads the field
214def left_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), M.nleft(~K, y)) : Array<Nat> & Nat}:
215 +fl = NR.lefts(~K, xs)
216 +t = BK.bk(Nat, d, fl, 0n)
217 +hlen = lefts_len(~K, xs)
218 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
219 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
220 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
221 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
222 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
223 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nleft(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nleft(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), lefts_nth(~K, xs, i, y, hy)))
224 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nleft(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
225 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
226 AR.get(Nat, d, t, U32.from_nat(i), M.nleft(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
227
228# a slot below the length written with a node's field
229def left_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), M.nleft(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
230 +fl = NR.lefts(~K, xs)
231 +t = BK.bk(Nat, d, fl, 0n)
232 +hlen = lefts_len(~K, xs)
233 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
234 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
235 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
236 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
237 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
238 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nleft(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nleft(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), lefts_nth(~K, xs, i, y0, hy0)))
239 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nleft(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
240 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
241 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.nleft(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.nleft(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.nleft(~K, y), M.nleft(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
242 %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nleft(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
243 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.nleft(~K, y)), BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.nleft(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.nleft(~K, y)), 0n), BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.nleft(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.nleft(~K, y)), NR.lefts(~K, SC.update(M.Node<K>, xs, i, y)), lefts_upd(~K, xs, i, y))))
244
245# the slot at the length (inside the capacity) written: an append
246def left_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nleft(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
247 +fl = NR.lefts(~K, xs)
248 +t = BK.bk(Nat, d, fl, 0n)
249 +n = SC.length(M.Node<K>, xs)
250 +hlen = lefts_len(~K, xs)
251 +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
252 +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
253 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
254 +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
255 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
256 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
257 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.nleft(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.nleft(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.nleft(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
258 %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nleft(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
259 %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nleft(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
260 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.nleft(~K, y)), BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.nleft(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.nleft(~K, y)), 0n), BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.nleft(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.nleft(~K, y)), NR.lefts(~K, SC.snoc(M.Node<K>, xs, y)), lefts_snoc(~K, xs, y))))
261
262# the block doubled with a default half
263def left_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)) : Array<Nat>}:
264 +fl = NR.lefts(~K, xs)
265 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), lefts_len(~K, xs)), hc)
266 %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
267 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
268
269# the last slot reset to the encoding of Free{0}: a pop
270def left_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(m), M.nleft(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
271 +fl = NR.lefts(~K, xs)
272 +t = BK.bk(Nat, d, fl, 0n)
273 +hlen = lefts_len(~K, xs)
274 +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
275 +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
276 +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
277 +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
278 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
279 +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
280 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.nleft(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.nleft(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), lefts_nth(~K, xs, m, y0, hy0)))
281 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nleft(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
282 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
283 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.nleft(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
284 %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
285 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.lefts(~K, SC.init(M.Node<K>, xs)), lefts_init(~K, xs))))
286
287# updating a node that keeps this field leaves the field list
288def lefts_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nleft(~K, x) == M.nleft(~K, y) : Nat}) -> {NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)) == NR.lefts(~K, xs) : List<&2, Nat>}:
289 %lefts_upd(~K, xs, i, x) : {_ == NR.lefts(~K, xs) : List<&2, Nat>}
290 %Equal.sym(Nat, M.nleft(~K, x), M.nleft(~K, y), he) : {SC.update(Nat, NR.lefts(~K, xs), i, _) == NR.lefts(~K, xs) : List<&2, Nat>}
291 upd_same(Nat, NR.lefts(~K, xs), i, M.nleft(~K, y), lefts_nth(~K, xs, i, y, hy))
292
293def rights_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.rights(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
294 match xs:
295 case Nil{}:
296 {==}
297 case Con{x, +r}:
298 N.succ_cong(SC.length(Nat, NR.rights(~K, r)), SC.length(M.Node<K>, r), rights_len(~K, r))
299
300def rights_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.rights(~K, xs), i) == Some{M.nright(~K, y)} : Maybe<&2, Nat>}:
301 match xs i:
302 case Nil{} _:
303 Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.nright(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
304 case Con{+x, r} 0n:
305 Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.nright(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
306 case Con{x, +r} 1n+q:
307 rights_nth(~K, r, q, y, h)
308
309def rights_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.rights(~K, xs), i, M.nright(~K, y)) == NR.rights(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
310 match xs i:
311 case Nil{} _:
312 {==}
313 case Con{x, r} 0n:
314 {==}
315 case Con{+x, +r} 1n+q:
316 LL.cons_cong(Nat, M.nright(~K, x), SC.update(Nat, NR.rights(~K, r), q, M.nright(~K, y)), NR.rights(~K, SC.update(M.Node<K>, r, q, y)), rights_upd(~K, r, q, y))
317
318def rights_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.rights(~K, xs), M.nright(~K, y)) == NR.rights(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
319 match xs:
320 case Nil{}:
321 {==}
322 case Con{+x, +r}:
323 LL.cons_cong(Nat, M.nright(~K, x), SC.snoc(Nat, NR.rights(~K, r), M.nright(~K, y)), NR.rights(~K, SC.snoc(M.Node<K>, r, y)), rights_snoc(~K, r, y))
324
325def rights_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.rights(~K, xs)) == NR.rights(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
326 match xs:
327 case Nil{}:
328 {==}
329 case Con{x, Nil{}}:
330 {==}
331 case Con{+x, Con{+y, +t}}:
332 LL.cons_cong(Nat, M.nright(~K, x), SC.init(Nat, NR.rights(~K, Con{y, t})), NR.rights(~K, SC.init(M.Node<K>, Con{y, t})), rights_init(~K, Con{y, t}))
333
334# the field block: a slot below the length reads the field
335def right_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), M.nright(~K, y)) : Array<Nat> & Nat}:
336 +fl = NR.rights(~K, xs)
337 +t = BK.bk(Nat, d, fl, 0n)
338 +hlen = rights_len(~K, xs)
339 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
340 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
341 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
342 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
343 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
344 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nright(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nright(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), rights_nth(~K, xs, i, y, hy)))
345 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nright(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
346 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
347 AR.get(Nat, d, t, U32.from_nat(i), M.nright(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
348
349# a slot below the length written with a node's field
350def right_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
351 +fl = NR.rights(~K, xs)
352 +t = BK.bk(Nat, d, fl, 0n)
353 +hlen = rights_len(~K, xs)
354 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
355 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
356 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
357 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
358 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
359 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nright(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nright(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), rights_nth(~K, xs, i, y0, hy0)))
360 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nright(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
361 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
362 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.nright(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.nright(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.nright(~K, y), M.nright(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
363 %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nright(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
364 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.nright(~K, y)), BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.nright(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.nright(~K, y)), 0n), BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.nright(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.nright(~K, y)), NR.rights(~K, SC.update(M.Node<K>, xs, i, y)), rights_upd(~K, xs, i, y))))
365
366# the slot at the length (inside the capacity) written: an append
367def right_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nright(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
368 +fl = NR.rights(~K, xs)
369 +t = BK.bk(Nat, d, fl, 0n)
370 +n = SC.length(M.Node<K>, xs)
371 +hlen = rights_len(~K, xs)
372 +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
373 +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
374 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
375 +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
376 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
377 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
378 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.nright(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.nright(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.nright(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
379 %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nright(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
380 %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nright(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
381 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.nright(~K, y)), BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.nright(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.nright(~K, y)), 0n), BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.nright(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.nright(~K, y)), NR.rights(~K, SC.snoc(M.Node<K>, xs, y)), rights_snoc(~K, xs, y))))
382
383# the block doubled with a default half
384def right_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)) : Array<Nat>}:
385 +fl = NR.rights(~K, xs)
386 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), rights_len(~K, xs)), hc)
387 %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
388 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
389
390# the last slot reset to the encoding of Free{0}: a pop
391def right_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(m), M.nright(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
392 +fl = NR.rights(~K, xs)
393 +t = BK.bk(Nat, d, fl, 0n)
394 +hlen = rights_len(~K, xs)
395 +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
396 +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
397 +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
398 +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
399 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
400 +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
401 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.nright(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.nright(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), rights_nth(~K, xs, m, y0, hy0)))
402 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nright(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
403 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
404 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.nright(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
405 %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
406 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.rights(~K, SC.init(M.Node<K>, xs)), rights_init(~K, xs))))
407
408# updating a node that keeps this field leaves the field list
409def rights_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nright(~K, x) == M.nright(~K, y) : Nat}) -> {NR.rights(~K, SC.update(M.Node<K>, xs, i, x)) == NR.rights(~K, xs) : List<&2, Nat>}:
410 %rights_upd(~K, xs, i, x) : {_ == NR.rights(~K, xs) : List<&2, Nat>}
411 %Equal.sym(Nat, M.nright(~K, x), M.nright(~K, y), he) : {SC.update(Nat, NR.rights(~K, xs), i, _) == NR.rights(~K, xs) : List<&2, Nat>}
412 upd_same(Nat, NR.rights(~K, xs), i, M.nright(~K, y), rights_nth(~K, xs, i, y, hy))
413
414def parents_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Nat, NR.parents(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
415 match xs:
416 case Nil{}:
417 {==}
418 case Con{x, +r}:
419 N.succ_cong(SC.length(Nat, NR.parents(~K, r)), SC.length(M.Node<K>, r), parents_len(~K, r))
420
421def parents_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Nat, NR.parents(~K, xs), i) == Some{M.nparent(~K, y)} : Maybe<&2, Nat>}:
422 match xs i:
423 case Nil{} _:
424 Empty.absurd({SC.nth(Nat, Nil{}, i) == Some{M.nparent(~K, y)} : Maybe<&2, Nat>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
425 case Con{+x, r} 0n:
426 Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Nat>, z => Some{M.nparent(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
427 case Con{x, +r} 1n+q:
428 parents_nth(~K, r, q, y, h)
429
430def parents_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Nat, NR.parents(~K, xs), i, M.nparent(~K, y)) == NR.parents(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Nat>}:
431 match xs i:
432 case Nil{} _:
433 {==}
434 case Con{x, r} 0n:
435 {==}
436 case Con{+x, +r} 1n+q:
437 LL.cons_cong(Nat, M.nparent(~K, x), SC.update(Nat, NR.parents(~K, r), q, M.nparent(~K, y)), NR.parents(~K, SC.update(M.Node<K>, r, q, y)), parents_upd(~K, r, q, y))
438
439def parents_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Nat, NR.parents(~K, xs), M.nparent(~K, y)) == NR.parents(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Nat>}:
440 match xs:
441 case Nil{}:
442 {==}
443 case Con{+x, +r}:
444 LL.cons_cong(Nat, M.nparent(~K, x), SC.snoc(Nat, NR.parents(~K, r), M.nparent(~K, y)), NR.parents(~K, SC.snoc(M.Node<K>, r, y)), parents_snoc(~K, r, y))
445
446def parents_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Nat, NR.parents(~K, xs)) == NR.parents(~K, SC.init(M.Node<K>, xs)) : List<&2, Nat>}:
447 match xs:
448 case Nil{}:
449 {==}
450 case Con{x, Nil{}}:
451 {==}
452 case Con{+x, Con{+y, +t}}:
453 LL.cons_cong(Nat, M.nparent(~K, x), SC.init(Nat, NR.parents(~K, Con{y, t})), NR.parents(~K, SC.init(M.Node<K>, Con{y, t})), parents_init(~K, Con{y, t}))
454
455# the field block: a slot below the length reads the field
456def parent_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i)) == (AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), M.nparent(~K, y)) : Array<Nat> & Nat}:
457 +fl = NR.parents(~K, xs)
458 +t = BK.bk(Nat, d, fl, 0n)
459 +hlen = parents_len(~K, xs)
460 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
461 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
462 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
463 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
464 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
465 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nparent(~K, y)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nparent(~K, y)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), parents_nth(~K, xs, i, y, hy)))
466 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nparent(~K, y)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
467 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
468 AR.get(Nat, d, t, U32.from_nat(i), M.nparent(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))
469
470# a slot below the length written with a node's field
471def parent_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}:
472 +fl = NR.parents(~K, xs)
473 +t = BK.bk(Nat, d, fl, 0n)
474 +hlen = parents_len(~K, xs)
475 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
476 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
477 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
478 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
479 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
480 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), i), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), Some{M.nparent(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, i), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), i), SC.nth(Nat, fl, i), Some{M.nparent(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, i, hiF, hcF), parents_nth(~K, xs, i, y0, hy0)))
481 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nparent(~K, y0)} : Maybe<&2, Nat>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
482 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
483 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(i), M.nparent(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(i)), M.nparent(~K, y))), AR.set(Nat, d, t, U32.from_nat(i), M.nparent(~K, y), M.nparent(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
484 %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nparent(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n)) : Array<Nat>}
485 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, i, M.nparent(~K, y)), BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, i, M.nparent(~K, y)), BK.bk(Nat, d, SC.update(Nat, fl, i, M.nparent(~K, y)), 0n), BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), 0n), BK.bk_set(Nat, d, fl, 0n, i, M.nparent(~K, y), hiF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.update(Nat, fl, i, M.nparent(~K, y)), NR.parents(~K, SC.update(M.Node<K>, xs, i, y)), parents_upd(~K, xs, i, y))))
486
487# the slot at the length (inside the capacity) written: an append
488def parent_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(SC.length(M.Node<K>, xs)), M.nparent(~K, y)) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}:
489 +fl = NR.parents(~K, xs)
490 +t = BK.bk(Nat, d, fl, 0n)
491 +n = SC.length(M.Node<K>, xs)
492 +hlen = parents_len(~K, xs)
493 +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
494 +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), n, hlen), hn)
495 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), SC.length(Nat, fl)), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), SC.length(Nat, fl)), Some{0n}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, SC.length(Nat, fl)), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), BK.fill_at_len(Nat, SC.pow2(d), fl, 0n, hnF))
496 +hx1 = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, SC.length(Nat, fl), n, hlen, hx0)
497 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{0n} : Maybe<&2, Nat>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
498 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
499 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(n), M.nparent(~K, y)), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(n)), M.nparent(~K, y))), AR.set(Nat, d, t, U32.from_nat(n), M.nparent(~K, y), 0n, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
500 %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nparent(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
501 %hlen : {AR.thaw(Nat, AR.upd(Nat, d, t, _, M.nparent(~K, y))) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n)) : Array<Nat>}
502 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, SC.length(Nat, fl), M.nparent(~K, y)), BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, SC.length(Nat, fl), M.nparent(~K, y)), BK.bk(Nat, d, SC.snoc(Nat, fl, M.nparent(~K, y)), 0n), BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), 0n), BK.bk_push(Nat, d, fl, 0n, M.nparent(~K, y), hnF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.snoc(Nat, fl, M.nparent(~K, y)), NR.parents(~K, SC.snoc(M.Node<K>, xs, y)), parents_snoc(~K, xs, y))))
503
504# the block doubled with a default half
505def parent_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), Array.new(Nat, d, 0n)} == AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.parents(~K, xs), 0n)) : Array<Nat>}:
506 +fl = NR.parents(~K, xs)
507 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), parents_len(~K, xs)), hc)
508 %Equal.sym(Array<Nat>, Array.new(Nat, d, 0n), AR.thaw(Nat, AR.trep(Nat, d, 0n)), AR.new(Nat, d, 0n)) : {ANode{AR.thaw(Nat, BK.bk(Nat, d, fl, 0n)), _} == AR.thaw(Nat, BK.bk(Nat, 1n+d, fl, 0n)) : Array<Nat>}
509 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.TNode{BK.bk(Nat, d, fl, 0n), AR.trep(Nat, d, 0n)}, BK.bk(Nat, 1n+d, fl, 0n), BK.bk_grow(Nat, d, fl, 0n, hcF))
510
511# the last slot reset to the encoding of Free{0}: a pop
512def parent_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(m), M.nparent(~K, M.Free{0n})) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}:
513 +fl = NR.parents(~K, xs)
514 +t = BK.bk(Nat, d, fl, 0n)
515 +hlen = parents_len(~K, xs)
516 +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
517 +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
518 +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
519 +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hi)
520 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Nat, fl), Equal.sym(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), hlen), hc)
521 +hmF = Equal.trans(Nat, SC.length(Nat, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
522 +hx0 = Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, AR.slots(Nat, t), m), SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), Some{M.nparent(~K, y0)}, Equal.cong(List<&2, Nat>, Maybe<&2, Nat>, z => SC.nth(Nat, z, m), AR.slots(Nat, t), BK.fillv(Nat, SC.pow2(d), fl, 0n), BK.bk_slots(Nat, d, fl, 0n)), Equal.trans(Maybe<&2, Nat>, SC.nth(Nat, BK.fillv(Nat, SC.pow2(d), fl, 0n), m), SC.nth(Nat, fl, m), Some{M.nparent(~K, y0)}, BK.fill_nth(Nat, SC.pow2(d), fl, 0n, m, hiF, hcF), parents_nth(~K, xs, m, y0, hy0)))
523 +hx = L.subst(Nat, z => {SC.nth(Nat, AR.slots(Nat, t), z) == Some{M.nparent(~K, y0)} : Maybe<&2, Nat>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
524 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
525 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, t), U32.from_nat(m), 0n), AR.thaw(Nat, AR.upd(Nat, d, t, U32.to_nat(U32.from_nat(m)), 0n)), AR.set(Nat, d, t, U32.from_nat(m), 0n, M.nparent(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Nat, d, fl, 0n))) : {_ == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
526 %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Nat, AR.upd(Nat, d, t, _, 0n)) == AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)) : Array<Nat>}
527 Equal.cong(AR.Tree<Nat>, Array<Nat>, z => AR.thaw(Nat, z), AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n), Equal.trans(AR.Tree<Nat>, AR.upd(Nat, d, t, m, 0n), BK.bk(Nat, d, SC.init(Nat, fl), 0n), BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n), BK.bk_pop(Nat, d, fl, 0n, m, hmF, hcF), Equal.cong(List<&2, Nat>, AR.Tree<Nat>, z => BK.bk(Nat, d, z, 0n), SC.init(Nat, fl), NR.parents(~K, SC.init(M.Node<K>, xs)), parents_init(~K, xs))))
528
529# updating a node that keeps this field leaves the field list
530def parents_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nparent(~K, x) == M.nparent(~K, y) : Nat}) -> {NR.parents(~K, SC.update(M.Node<K>, xs, i, x)) == NR.parents(~K, xs) : List<&2, Nat>}:
531 %parents_upd(~K, xs, i, x) : {_ == NR.parents(~K, xs) : List<&2, Nat>}
532 %Equal.sym(Nat, M.nparent(~K, x), M.nparent(~K, y), he) : {SC.update(Nat, NR.parents(~K, xs), i, _) == NR.parents(~K, xs) : List<&2, Nat>}
533 upd_same(Nat, NR.parents(~K, xs), i, M.nparent(~K, y), parents_nth(~K, xs, i, y, hy))
534
535def keys_len(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.length(Maybe<&2, K>, NR.keys(~K, xs)) == SC.length(M.Node<K>, xs) : Nat}:
536 match xs:
537 case Nil{}:
538 {==}
539 case Con{x, +r}:
540 N.succ_cong(SC.length(Maybe<&2, K>, NR.keys(~K, r)), SC.length(M.Node<K>, r), keys_len(~K, r))
541
542def keys_nth(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +h: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {SC.nth(Maybe<&2, K>, NR.keys(~K, xs), i) == Some{M.nkey(~K, y)} : Maybe<&2, Maybe<&2, K>>}:
543 match xs i:
544 case Nil{} _:
545 Empty.absurd({SC.nth(Maybe<&2, K>, Nil{}, i) == Some{M.nkey(~K, y)} : Maybe<&2, Maybe<&2, K>>}, L.false_true(Equal.cong(Maybe<&2, M.Node<K>>, Bool, z => mb(~K, z), None{}, Some{y}, h)))
546 case Con{+x, r} 0n:
547 Equal.cong(Maybe<&2, M.Node<K>>, Maybe<&2, Maybe<&2, K>>, z => Some{M.nkey(~K, unsome(~K, z, x))}, Some{x}, Some{y}, h)
548 case Con{x, +r} 1n+q:
549 keys_nth(~K, r, q, y, h)
550
551def keys_upd(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>) -> {SC.update(Maybe<&2, K>, NR.keys(~K, xs), i, M.nkey(~K, y)) == NR.keys(~K, SC.update(M.Node<K>, xs, i, y)) : List<&2, Maybe<&2, K>>}:
552 match xs i:
553 case Nil{} _:
554 {==}
555 case Con{x, r} 0n:
556 {==}
557 case Con{+x, +r} 1n+q:
558 LL.cons_cong(Maybe<&2, K>, M.nkey(~K, x), SC.update(Maybe<&2, K>, NR.keys(~K, r), q, M.nkey(~K, y)), NR.keys(~K, SC.update(M.Node<K>, r, q, y)), keys_upd(~K, r, q, y))
559
560def keys_snoc(~K: Data, +xs: List<&2, M.Node<K>>, +y: M.Node<K>) -> {SC.snoc(Maybe<&2, K>, NR.keys(~K, xs), M.nkey(~K, y)) == NR.keys(~K, SC.snoc(M.Node<K>, xs, y)) : List<&2, Maybe<&2, K>>}:
561 match xs:
562 case Nil{}:
563 {==}
564 case Con{+x, +r}:
565 LL.cons_cong(Maybe<&2, K>, M.nkey(~K, x), SC.snoc(Maybe<&2, K>, NR.keys(~K, r), M.nkey(~K, y)), NR.keys(~K, SC.snoc(M.Node<K>, r, y)), keys_snoc(~K, r, y))
566
567def keys_init(~K: Data, +xs: List<&2, M.Node<K>>) -> {SC.init(Maybe<&2, K>, NR.keys(~K, xs)) == NR.keys(~K, SC.init(M.Node<K>, xs)) : List<&2, Maybe<&2, K>>}:
568 match xs:
569 case Nil{}:
570 {==}
571 case Con{x, Nil{}}:
572 {==}
573 case Con{+x, Con{+y, +t}}:
574 LL.cons_cong(Maybe<&2, K>, M.nkey(~K, x), SC.init(Maybe<&2, K>, NR.keys(~K, Con{y, t})), NR.keys(~K, SC.init(M.Node<K>, Con{y, t})), keys_init(~K, Con{y, t}))
575
576# the field block: a slot below the length reads the field
577def key_get(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}) -> {Array.get(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i)) == (AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), M.nkey(~K, y)) : Array<Maybe<&2, K>> & Maybe<&2, K>}:
578 +fl = NR.keys(~K, xs)
579 +t = BK.bk(Maybe<&2, K>, d, fl, None{})
580 +hlen = keys_len(~K, xs)
581 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y, hy)
582 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
583 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
584 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hi)
585 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hc)
586 +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), i), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), Some{M.nkey(~K, y)}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, i), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), SC.nth(Maybe<&2, K>, fl, i), Some{M.nkey(~K, y)}, BK.fill_nth(Maybe<&2, K>, SC.pow2(d), fl, None{}, i, hiF, hcF), keys_nth(~K, xs, i, y, hy)))
587 +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{M.nkey(~K, y)} : Maybe<&2, Maybe<&2, K>>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
588 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
589 AR.get(Maybe<&2, K>, d, t, U32.from_nat(i), M.nkey(~K, y), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))
590
591# a slot below the length written with a node's field
592def key_set(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}, +y: M.Node<K>) -> {Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.nkey(~K, y)) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{})) : Array<Maybe<&2, K>>}:
593 +fl = NR.keys(~K, xs)
594 +t = BK.bk(Maybe<&2, K>, d, fl, None{})
595 +hlen = keys_len(~K, xs)
596 +hi = LL.nth_lt_length(M.Node<K>, xs, i, y0, hy0)
597 +hip = N.lt_le_trans(i, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
598 +eu = U.to_nat_from_nat(i, d, DAS.le32(d, l, hd, hl), hip)
599 +hiF = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hi)
600 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hc)
601 +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), i), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), Some{M.nkey(~K, y0)}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, i), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), i), SC.nth(Maybe<&2, K>, fl, i), Some{M.nkey(~K, y0)}, BK.fill_nth(Maybe<&2, K>, SC.pow2(d), fl, None{}, i, hiF, hcF), keys_nth(~K, xs, i, y0, hy0)))
602 +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{M.nkey(~K, y0)} : Maybe<&2, Maybe<&2, K>>}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hx0)
603 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu), hip)
604 %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, t), U32.from_nat(i), M.nkey(~K, y)), AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, U32.to_nat(U32.from_nat(i)), M.nkey(~K, y))), AR.set(Maybe<&2, K>, d, t, U32.from_nat(i), M.nkey(~K, y), M.nkey(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))) : {_ == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{})) : Array<Maybe<&2, K>>}
605 %Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, eu) : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, M.nkey(~K, y))) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{})) : Array<Maybe<&2, K>>}
606 Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.upd(Maybe<&2, K>, d, t, i, M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{}), Equal.trans(AR.Tree<Maybe<&2, K>>, AR.upd(Maybe<&2, K>, d, t, i, M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, SC.update(Maybe<&2, K>, fl, i, M.nkey(~K, y)), None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), None{}), BK.bk_set(Maybe<&2, K>, d, fl, None{}, i, M.nkey(~K, y), hiF, hcF), Equal.cong(List<&2, Maybe<&2, K>>, AR.Tree<Maybe<&2, K>>, z => BK.bk(Maybe<&2, K>, d, z, None{}), SC.update(Maybe<&2, K>, fl, i, M.nkey(~K, y)), NR.keys(~K, SC.update(M.Node<K>, xs, i, y)), keys_upd(~K, xs, i, y))))
607
608# the slot at the length (inside the capacity) written: an append
609def key_push(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +y: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), M.nkey(~K, y)) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}:
610 +fl = NR.keys(~K, xs)
611 +t = BK.bk(Maybe<&2, K>, d, fl, None{})
612 +n = SC.length(M.Node<K>, xs)
613 +hlen = keys_len(~K, xs)
614 +eu = U.to_nat_from_nat(n, d, DAS.le32(d, l, hd, hl), hn)
615 +hnF = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), n, hlen), hn)
616 +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), SC.length(Maybe<&2, K>, fl)), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), SC.length(Maybe<&2, K>, fl)), Some{None{}}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, SC.length(Maybe<&2, K>, fl)), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), BK.fill_at_len(Maybe<&2, K>, SC.pow2(d), fl, None{}, hnF))
617 +hx1 = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{None{}} : Maybe<&2, Maybe<&2, K>>}, SC.length(Maybe<&2, K>, fl), n, hlen, hx0)
618 +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{None{}} : Maybe<&2, Maybe<&2, K>>}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hx1)
619 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, n, U32.to_nat(U32.from_nat(n)), Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu), hn)
620 %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, t), U32.from_nat(n), M.nkey(~K, y)), AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, U32.to_nat(U32.from_nat(n)), M.nkey(~K, y))), AR.set(Maybe<&2, K>, d, t, U32.from_nat(n), M.nkey(~K, y), None{}, DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))) : {_ == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}
621 %Equal.sym(Nat, U32.to_nat(U32.from_nat(n)), n, eu) : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, M.nkey(~K, y))) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}
622 %hlen : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, M.nkey(~K, y))) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{})) : Array<Maybe<&2, K>>}
623 Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.upd(Maybe<&2, K>, d, t, SC.length(Maybe<&2, K>, fl), M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{}), Equal.trans(AR.Tree<Maybe<&2, K>>, AR.upd(Maybe<&2, K>, d, t, SC.length(Maybe<&2, K>, fl), M.nkey(~K, y)), BK.bk(Maybe<&2, K>, d, SC.snoc(Maybe<&2, K>, fl, M.nkey(~K, y)), None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), None{}), BK.bk_push(Maybe<&2, K>, d, fl, None{}, M.nkey(~K, y), hnF), Equal.cong(List<&2, Maybe<&2, K>>, AR.Tree<Maybe<&2, K>>, z => BK.bk(Maybe<&2, K>, d, z, None{}), SC.snoc(Maybe<&2, K>, fl, M.nkey(~K, y)), NR.keys(~K, SC.snoc(M.Node<K>, xs, y)), keys_snoc(~K, xs, y))))
624
625# the block doubled with a default half
626def key_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {ANode{AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), Array.new(Maybe<&2, K>, d, None{})} == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, 1n+d, NR.keys(~K, xs), None{})) : Array<Maybe<&2, K>>}:
627 +fl = NR.keys(~K, xs)
628 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), keys_len(~K, xs)), hc)
629 %Equal.sym(Array<Maybe<&2, K>>, Array.new(Maybe<&2, K>, d, None{}), AR.thaw(Maybe<&2, K>, AR.trep(Maybe<&2, K>, d, None{})), AR.new(Maybe<&2, K>, d, None{})) : {ANode{AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, fl, None{})), _} == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, 1n+d, fl, None{})) : Array<Maybe<&2, K>>}
630 Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.TNode{BK.bk(Maybe<&2, K>, d, fl, None{}), AR.trep(Maybe<&2, K>, d, None{})}, BK.bk(Maybe<&2, K>, 1n+d, fl, None{}), BK.bk_grow(Maybe<&2, K>, d, fl, None{}, hcF))
631
632# the last slot reset to the encoding of Free{0}: a pop
633def key_drop(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node<K>>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node<K>, xs) == 1n+m : Nat}, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, m) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(m), M.nkey(~K, M.Free{0n})) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{})) : Array<Maybe<&2, K>>}:
634 +fl = NR.keys(~K, xs)
635 +t = BK.bk(Maybe<&2, K>, d, fl, None{})
636 +hlen = keys_len(~K, xs)
637 +hi = LL.nth_lt_length(M.Node<K>, xs, m, y0, hy0)
638 +hip = N.lt_le_trans(m, SC.length(M.Node<K>, xs), SC.pow2(d), hi, hc)
639 +eu = U.to_nat_from_nat(m, d, DAS.le32(d, l, hd, hl), hip)
640 +hiF = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hi)
641 +hcF = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), SC.length(Maybe<&2, K>, fl), Equal.sym(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), hlen), hc)
642 +hmF = Equal.trans(Nat, SC.length(Maybe<&2, K>, fl), SC.length(M.Node<K>, xs), 1n+m, hlen, hm)
643 +hx0 = Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), m), SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), m), Some{M.nkey(~K, y0)}, Equal.cong(List<&2, Maybe<&2, K>>, Maybe<&2, Maybe<&2, K>>, z => SC.nth(Maybe<&2, K>, z, m), AR.slots(Maybe<&2, K>, t), BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), BK.bk_slots(Maybe<&2, K>, d, fl, None{})), Equal.trans(Maybe<&2, Maybe<&2, K>>, SC.nth(Maybe<&2, K>, BK.fillv(Maybe<&2, K>, SC.pow2(d), fl, None{}), m), SC.nth(Maybe<&2, K>, fl, m), Some{M.nkey(~K, y0)}, BK.fill_nth(Maybe<&2, K>, SC.pow2(d), fl, None{}, m, hiF, hcF), keys_nth(~K, xs, m, y0, hy0)))
644 +hx = L.subst(Nat, z => {SC.nth(Maybe<&2, K>, AR.slots(Maybe<&2, K>, t), z) == Some{M.nkey(~K, y0)} : Maybe<&2, Maybe<&2, K>>}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hx0)
645 +hiu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, m, U32.to_nat(U32.from_nat(m)), Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu), hip)
646 %Equal.sym(Array<Maybe<&2, K>>, Array.set(Maybe<&2, K>, AR.thaw(Maybe<&2, K>, t), U32.from_nat(m), None{}), AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, U32.to_nat(U32.from_nat(m)), None{})), AR.set(Maybe<&2, K>, d, t, U32.from_nat(m), None{}, M.nkey(~K, y0), DAS.lt32(d, l, hd, hl), hiu, hx, BK.bk_perfect(Maybe<&2, K>, d, fl, None{}))) : {_ == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{})) : Array<Maybe<&2, K>>}
647 %Equal.sym(Nat, U32.to_nat(U32.from_nat(m)), m, eu) : {AR.thaw(Maybe<&2, K>, AR.upd(Maybe<&2, K>, d, t, _, None{})) == AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{})) : Array<Maybe<&2, K>>}
648 Equal.cong(AR.Tree<Maybe<&2, K>>, Array<Maybe<&2, K>>, z => AR.thaw(Maybe<&2, K>, z), AR.upd(Maybe<&2, K>, d, t, m, None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}), Equal.trans(AR.Tree<Maybe<&2, K>>, AR.upd(Maybe<&2, K>, d, t, m, None{}), BK.bk(Maybe<&2, K>, d, SC.init(Maybe<&2, K>, fl), None{}), BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}), BK.bk_pop(Maybe<&2, K>, d, fl, None{}, m, hmF, hcF), Equal.cong(List<&2, Maybe<&2, K>>, AR.Tree<Maybe<&2, K>>, z => BK.bk(Maybe<&2, K>, d, z, None{}), SC.init(Maybe<&2, K>, fl), NR.keys(~K, SC.init(M.Node<K>, xs)), keys_init(~K, xs))))
649
650# updating a node that keeps this field leaves the field list
651def keys_keep(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +x: M.Node<K>, +hy: {SC.nth(M.Node<K>, xs, i) == Some{y} : Maybe<&2, M.Node<K>>}, +he: {M.nkey(~K, x) == M.nkey(~K, y) : Maybe<&2, K>}) -> {NR.keys(~K, SC.update(M.Node<K>, xs, i, x)) == NR.keys(~K, xs) : List<&2, Maybe<&2, K>>}:
652 %keys_upd(~K, xs, i, x) : {_ == NR.keys(~K, xs) : List<&2, Maybe<&2, K>>}
653 %Equal.sym(Maybe<&2, K>, M.nkey(~K, x), M.nkey(~K, y), he) : {SC.update(Maybe<&2, K>, NR.keys(~K, xs), i, _) == NR.keys(~K, xs) : List<&2, Maybe<&2, K>>}
654 upd_same(Maybe<&2, K>, NR.keys(~K, xs), i, M.nkey(~K, y), keys_nth(~K, xs, i, y, hy))
655