proofs/containers/balanced_search_tree/nsl.bend
bend-collections-laws-containers@1.0.0.0 · 536 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/array.bend as AR
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
8import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as DE
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/bk.bend as BK
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsr.bend as NR
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/nsf.bend as NF
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/da.bend as DA
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
14
15# The TreeMap's node store (the ns_* functions of the implementation) on the
16# realization of a node list xs of length at most 2^d, d <= l <= 31: a read
17# returns the list's node, a write in range updates the list, an append
18# snocs it (doubling the capacity when full and below the limit), clear
19# empties it. These are the statements the dynamic-array lemmas of arr.bend
20# make for a dynamic array of nodes.
21
22
23def isj(-A: Data, m: Maybe<&2, A>) -> Bool:
24 match m:
25 case None{}:
26 False{}
27 case Some{x}:
28 True{}
29
30# a slot below the length holds something
31def nth_isj(-A: Data, +xs: List<&2, A>, +i: Nat, +h: {Nat.is_lt(i, SC.length(A, xs)) == True{} : Bool}) -> {isj(A, SC.nth(A, xs, i)) == True{} : Bool}:
32 match xs i:
33 case Nil{} _:
34 Empty.absurd({isj(A, SC.nth(A, Nil{}, i)) == True{} : Bool}, N.lt_zero_absurd(i, h))
35 case Con{x, r} 0n:
36 {==}
37 case Con{x, +r} 1n+q:
38 nth_isj(A, r, q, h)
39
40def len_init(-A: Data, +xs: List<&2, A>, +m: Nat, +h: {SC.length(A, xs) == 1n+m : Nat}) -> {SC.length(A, SC.init(A, xs)) == m : Nat}:
41 match xs m:
42 case Nil{} _:
43 Empty.absurd({SC.length(A, SC.init(A, Nil{})) == m : Nat}, N.zero_succ(m, h))
44 case Con{x, Nil{}} 0n:
45 {==}
46 case Con{x, Nil{}} 1n+q:
47 Empty.absurd({SC.length(A, SC.init(A, Con{x, Nil{}})) == 1n+q : Nat}, N.zero_succ(q, N.succ_inj(0n, 1n+q, h)))
48 case Con{x, Con{y, t}} 0n:
49 Empty.absurd({SC.length(A, SC.init(A, Con{x, Con{y, t}})) == 0n : Nat}, N.succ_zero(SC.length(A, t), N.succ_inj(1n+SC.length(A, t), 0n, h)))
50 case Con{x, Con{+y, +t}} 1n+q:
51 N.succ_cong(SC.length(A, SC.init(A, Con{y, t})), q, len_init(A, Con{y, t}, q, N.succ_inj(1n+SC.length(A, t), 1n+q, h)))
52
53# a node is its encoding read back
54def mk_enc(~K: Data, +y: M.Node<K>) -> {M.mk_node(~K, M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), M.nparent(~K, y), M.nkey(~K, y)) == y : M.Node<K>}:
55 match y:
56 case M.Free{x}:
57 {==}
58 case M.N{True{}, lf, rt, pa, k}:
59 {==}
60 case M.N{False{}, lf, rt, pa, k}:
61 {==}
62
63# ---- length ----
64
65def ns_length_ok(~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.ns_length(~K, NR.real(~K, l, d, xs)) == (NR.real(~K, l, d, xs), SC.length(M.Node<K>, xs)) : M.NodeStore<K> & Nat}:
66 {==}
67
68# ---- read ----
69
70def get_some(~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>>}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
71 %Equal.sym(Array<Nat> & Nat, 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)), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rt(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
72 %Equal.sym(Array<Nat> & Nat, 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)), NF.left_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rl(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.ntag(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
73 %Equal.sym(Array<Nat> & Nat, 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)), NF.right_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rr(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.ntag(~K, y), M.nleft(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
74 %Equal.sym(Array<Nat> & Nat, 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)), NF.parent_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rp(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), U32.from_nat(i), M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
75 %Equal.sym(Array<Maybe<&2, K>> & Maybe<&2, 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)), NF.key_get(~K, l, d, xs, hl, hd, hc, i, y, hy)) : {M.ns_rk(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), M.nparent(~K, y), _) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
76 %Equal.sym(M.Node<K>, M.mk_node(~K, M.ntag(~K, y), M.nleft(~K, y), M.nright(~K, y), M.nparent(~K, y), M.nkey(~K, y)), y, mk_enc(~K, y)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))}, Done{_}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, Some{y})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
77 {==}
78
79def gs(~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, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, mv)) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
80 match mv:
81 case None{}:
82 Empty.absurd({M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, None{})) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
83 case Some{+y}:
84 get_some(~K, l, d, xs, hl, hd, hc, i, y, hmv)
85
86def gc(~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, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, SC.nth(M.Node<K>, xs, i))) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
87 match b:
88 case True{}:
89 gs(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
90 case False{}:
91 %Equal.sym(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), None{}, LL.nth_none(M.Node<K>, xs, i, N.not_lt_le(i, SC.length(M.Node<K>, xs), hb))) : {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, _)) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}
92 {==}
93
94# a read returns the list's node (IndexOutOfRange past the length)
95def ns_get_ok(~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) -> {M.ns_get(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), DA.item(M.Node<K>, SC.nth(M.Node<K>, xs, i))) : M.NodeStore<K> & Result<&2, &2, DE.Error, M.Node<K>>}:
96 gc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
97
98# ---- write ----
99
100
101def set_some(~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, +x: M.Node<K>, +y0: M.Node<K>, +hy0: {SC.nth(M.Node<K>, xs, i) == Some{y0} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, True{}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
102 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.tag_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), M.nleft(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), 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, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
103 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), M.nleft(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.left_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, x)), Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), 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, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
104 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), M.nright(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.right_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), 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, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
105 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), M.nparent(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), NF.parent_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _, 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, x))}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
106 %Equal.sym(Array<Maybe<&2, 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, x)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, x)), None{})), NF.key_set(~K, l, d, xs, hl, hd, hc, i, y0, hy0, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), _}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
107 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, x)), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, x)), None{}))}, Done{Unit{}}) == (M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, x)), None{}))}, Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
108 {==}
109
110def ws(~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, +x: M.Node<K>, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, True{}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
111 match mv:
112 case None{}:
113 Empty.absurd({M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, True{}) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
114 case Some{+y0}:
115 set_some(~K, l, d, xs, hl, hd, hc, i, x, y0, hmv)
116
117# a write below the length updates the list
118def ns_set_in(~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, +x: M.Node<K>, +h: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_set(~K, NR.real(~K, l, d, xs), i, x) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
119 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, h) : {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, _) == (NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
120 ws(~K, l, d, xs, hl, hd, hc, i, x, SC.nth(M.Node<K>, xs, i), {==}, h)
121
122# a write past the length changes nothing
123def ns_set_out(~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, +x: M.Node<K>, +h: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == False{} : Bool}) -> {M.ns_set(~K, NR.real(~K, l, d, xs), i, x) == (NR.real(~K, l, d, xs), Fail{DE.IndexOutOfRange{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
124 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), False{}, h) : {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, x, _) == (NR.real(~K, l, d, xs), Fail{DE.IndexOutOfRange{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
125 {==}
126
127# ---- append ----
128
129
130def push_at(~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}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_put(~K, l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), 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)), x) == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}:
131 %Equal.sym(Array<Nat>, 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, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.tag_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), _, 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, x)), 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, x)), 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, x)), 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, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
132 %Equal.sym(Array<Nat>, 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, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.left_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _, 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, x)), 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, x)), 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, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
133 %Equal.sym(Array<Nat>, 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, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.right_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _, 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, x)), 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, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
134 %Equal.sym(Array<Nat>, 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, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), NF.parent_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _, 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, x))} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
135 %Equal.sym(Array<Maybe<&2, 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(SC.length(M.Node<K>, xs)), M.nkey(~K, x)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, x)), None{})), NF.key_push(~K, l, d, xs, hl, hd, hc, x, hn)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), _} == NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)) : M.NodeStore<K>}
136 %Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, xs, x)), 1n+SC.length(M.Node<K>, xs), LL.length_snoc(M.Node<K>, xs, x)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, x)), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node<K>, xs, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node<K>, xs, x)), None{}))} : M.NodeStore<K>}
137 {==}
138
139# with room: the node appended
140def ns_push_room(~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}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_push(~K, NR.real(~K, l, d, xs), x) == (NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
141 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)), True{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, _, Nat.is_lt(d, l)) == (NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
142 Equal.cong(M.NodeStore<K>, M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, z => (z, Done{Unit{}}), M.ns_put(~K, l, d, SC.pow2(d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), 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)), x), NR.real(~K, l, d, SC.snoc(M.Node<K>, xs, x)), push_at(~K, l, d, xs, hl, hd, hc, x, hn))
143
144# full and below the limit: the blocks doubled, then the node appended
145def ns_push_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}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == False{} : Bool}, +hdl: {Nat.is_lt(d, l) == True{} : Bool}) -> {M.ns_push(~K, NR.real(~K, l, d, xs), x) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
146 +hd1 = N.lt_succ_le_succ(d, l, hdl)
147 +hc1 = N.le_trans(SC.length(M.Node<K>, xs), SC.pow2(d), SC.pow2(1n+d), hc, N.lt_le(SC.pow2(d), SC.pow2(1n+d), N.pow2_lt_succ(d)))
148 +hn1 = N.le_lt_trans(SC.length(M.Node<K>, xs), SC.pow2(d), SC.pow2(1n+d), hc, N.pow2_lt_succ(d))
149 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)), False{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, _, Nat.is_lt(d, l)) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
150 %Equal.sym(Bool, Nat.is_lt(d, l), True{}, hdl) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, False{}, _) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
151 %Equal.sym(Array<Nat>, 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)), NF.tag_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), _, M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n))), M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n))), M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n))), M.ns_grow_keys(~K, d, 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)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
152 %Equal.sym(Array<Nat>, 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)), NF.left_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), _, M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n))), M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n))), M.ns_grow_keys(~K, d, 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)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
153 %Equal.sym(Array<Nat>, 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)), NF.right_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), _, M.ns_grow_nats(d, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n))), M.ns_grow_keys(~K, d, 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)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
154 %Equal.sym(Array<Nat>, 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)), NF.parent_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)), _, M.ns_grow_keys(~K, d, 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)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
155 %Equal.sym(Array<Maybe<&2, K>>, 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{})), NF.key_grow(~K, l, d, xs, hl, hd, hc)) : {(M.ns_put(~K, l, 1n+d, Nat.double(SC.pow2(d)), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.parents(~K, xs), 0n)), _, U32.from_nat(SC.length(M.Node<K>, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), Done{Unit{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
156 Equal.cong(M.NodeStore<K>, M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>, z => (z, Done{Unit{}}), M.ns_put(~K, l, 1n+d, SC.pow2(1n+d), 1n+SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, 1n+d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, 1n+d, NR.keys(~K, xs), None{})), U32.from_nat(SC.length(M.Node<K>, xs)), x), NR.real(~K, l, 1n+d, SC.snoc(M.Node<K>, xs, x)), push_at(~K, l, 1n+d, xs, hl, hd1, hc1, x, hn1))
157
158# full at the limit: nothing changes
159def ns_push_full(~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}, +x: M.Node<K>, +hn: {Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)) == False{} : Bool}, +hdl: {Nat.is_lt(d, l) == False{} : Bool}) -> {M.ns_push(~K, NR.real(~K, l, d, xs), x) == (NR.real(~K, l, d, xs), Fail{DE.CapacityExceeded{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}:
160 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node<K>, xs), SC.pow2(d)), False{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, _, Nat.is_lt(d, l)) == (NR.real(~K, l, d, xs), Fail{DE.CapacityExceeded{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
161 %Equal.sym(Bool, Nat.is_lt(d, l), False{}, hdl) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), x, False{}, _) == (NR.real(~K, l, d, xs), Fail{DE.CapacityExceeded{}}) : M.NodeStore<K> & Result<&2, &2, DE.Error, Unit>}
162 {==}
163
164# ---- clear ----
165
166
167def drop_some(~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>>}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}:
168 %Equal.sym(Array<Nat>, 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)), NF.tag_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, _, 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})), 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})), 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})), 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}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
169 %Equal.sym(Array<Nat>, 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)), NF.left_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), _, 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})), 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})), 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}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
170 %Equal.sym(Array<Nat>, 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)), NF.right_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), _, 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})), 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}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
171 %Equal.sym(Array<Nat>, 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)), NF.parent_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), _, 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}))} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
172 %Equal.sym(Array<Maybe<&2, 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{})), NF.key_drop(~K, l, d, xs, hl, hd, hc, m, hm, y0, hy0)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)), _} == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}
173 %Equal.sym(Nat, SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), m, len_init(M.Node<K>, xs, m, hm)) : {M.NS{l, d, SC.pow2(d), m, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node<K>, xs)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node<K>, xs)), None{}))} : M.NodeStore<K>}
174 {==}
175
176def dr(~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}, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, m) == mv : Maybe<&2, M.Node<K>>}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}:
177 match mv:
178 case None{}:
179 +hi = L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, 1n+m, SC.length(M.Node<K>, xs), Equal.sym(Nat, SC.length(M.Node<K>, xs), 1n+m, hm), N.lt_succ(m))
180 Empty.absurd({M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, m), None{}, hmv, nth_isj(M.Node<K>, xs, m, hi))))
181 case Some{+y0}:
182 drop_some(~K, l, d, xs, hl, hd, hc, m, hm, y0, hmv)
183
184# dropping the last live slot: the list without its last node
185def ns_drop_ok(~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}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node<K>, xs)) : M.NodeStore<K>}:
186 dr(~K, l, d, xs, hl, hd, hc, m, hm, SC.nth(M.Node<K>, xs, m), {==})
187
188def clr(~K: Data, +k: Nat, +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}, +hk: {SC.length(M.Node<K>, xs) == k : Nat}) -> {M.ns_clear_go(~K, k, NR.real(~K, l, d, xs)) == NR.real(~K, l, d, Nil{}) : M.NodeStore<K>}:
189 match k:
190 case 0n:
191 Equal.cong(List<&2, M.Node<K>>, M.NodeStore<K>, z => NR.real(~K, l, d, z), xs, Nil{}, LL.length_zero_nil(M.Node<K>, xs, hk))
192 case 1n+ +m:
193 +hm2 = len_init(M.Node<K>, xs, m, hk)
194 %Equal.sym(M.NodeStore<K>, M.ns_drop(~K, NR.real(~K, l, d, xs), m), NR.real(~K, l, d, SC.init(M.Node<K>, xs)), ns_drop_ok(~K, l, d, xs, hl, hd, hc, m, hk)) : {M.ns_clear_go(~K, m, _) == NR.real(~K, l, d, Nil{}) : M.NodeStore<K>}
195 clr(~K, m, l, d, SC.init(M.Node<K>, xs), hl, hd, N.le_trans(SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), 1n+m, SC.pow2(d), L.subst(Nat, z => {Nat.is_le(z, 1n+m) == True{} : Bool}, m, SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), Equal.sym(Nat, SC.length(M.Node<K>, SC.init(M.Node<K>, xs)), m, hm2), N.le_succ(m)), L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, xs), 1n+m, hk, hc)), hm2)
196
197# clear empties the list, keeping the capacity
198def ns_clear_ok(~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.ns_clear(~K, NR.real(~K, l, d, xs)) == NR.real(~K, l, d, Nil{}) : M.NodeStore<K>}:
199 clr(~K, SC.length(M.Node<K>, xs), l, d, xs, hl, hd, hc, {==})
200
201# ---- reading one field of a slot ----
202
203
204def ors(-X: Data, m: Maybe<&2, X>, +dv: X) -> X:
205 match m:
206 case None{}:
207 dv
208 case Some{x}:
209 x
210
211def nth_or_some(-X: Data, +xs: List<&2, X>, +i: Nat, +y: X, +dv: X, +h: {SC.nth(X, xs, i) == Some{y} : Maybe<&2, X>}) -> {ST.nth_or(X, xs, i, dv) == y : X}:
212 match xs i:
213 case Nil{} _:
214 Empty.absurd({dv == y : X}, L.false_true(Equal.cong(Maybe<&2, X>, Bool, z => isj(X, z), None{}, Some{y}, h)))
215 case Con{+x, r} 0n:
216 Equal.cong(Maybe<&2, X>, X, z => ors(X, z, x), Some{x}, Some{y}, h)
217 case Con{x, +r} 1n+q:
218 nth_or_some(X, r, q, y, dv, h)
219
220def nth_or_hi(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X, +h: {Nat.is_lt(i, SC.length(X, xs)) == False{} : Bool}) -> {ST.nth_or(X, xs, i, dv) == dv : X}:
221 match xs i:
222 case Nil{} _:
223 {==}
224 case Con{x, t} 0n:
225 Empty.absurd({x == dv : X}, L.true_false(h))
226 case Con{x, +t} 1n+q:
227 nth_or_hi(X, t, q, dv, h)
228
229def tag_ats(~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, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
230 match mv:
231 case None{}:
232 Empty.absurd({M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
233 case Some{+y}:
234 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.ntag(~K, _)) : M.NodeStore<K> & Nat}
235 %Equal.sym(Array<Nat> & Nat, 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)), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_tag_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.ntag(~K, y)) : M.NodeStore<K> & Nat}
236 {==}
237
238def tag_atc(~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, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
239 match b:
240 case True{}:
241 tag_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
242 case False{}:
243 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.ntag(~K, _)) : M.NodeStore<K> & Nat}
244 {==}
245
246# the field of the list's node (of Free{0} past the length)
247def tag_at_ok(~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) -> {M.ns_tag_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.ntag(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
248 tag_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
249
250def left_ats(~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, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
251 match mv:
252 case None{}:
253 Empty.absurd({M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
254 case Some{+y}:
255 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nleft(~K, _)) : M.NodeStore<K> & Nat}
256 %Equal.sym(Array<Nat> & Nat, 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)), NF.left_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_left_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.nleft(~K, y)) : M.NodeStore<K> & Nat}
257 {==}
258
259def left_atc(~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, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
260 match b:
261 case True{}:
262 left_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
263 case False{}:
264 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nleft(~K, _)) : M.NodeStore<K> & Nat}
265 {==}
266
267# the field of the list's node (of Free{0} past the length)
268def left_at_ok(~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) -> {M.ns_left_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nleft(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
269 left_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
270
271def right_ats(~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, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
272 match mv:
273 case None{}:
274 Empty.absurd({M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
275 case Some{+y}:
276 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nright(~K, _)) : M.NodeStore<K> & Nat}
277 %Equal.sym(Array<Nat> & Nat, 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)), NF.right_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_right_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.nright(~K, y)) : M.NodeStore<K> & Nat}
278 {==}
279
280def right_atc(~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, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
281 match b:
282 case True{}:
283 right_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
284 case False{}:
285 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nright(~K, _)) : M.NodeStore<K> & Nat}
286 {==}
287
288# the field of the list's node (of Free{0} past the length)
289def right_at_ok(~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) -> {M.ns_right_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nright(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
290 right_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
291
292def parent_ats(~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, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
293 match mv:
294 case None{}:
295 Empty.absurd({M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
296 case Some{+y}:
297 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nparent(~K, _)) : M.NodeStore<K> & Nat}
298 %Equal.sym(Array<Nat> & Nat, 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)), NF.parent_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_parent_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), _) == (NR.real(~K, l, d, xs), M.nparent(~K, y)) : M.NodeStore<K> & Nat}
299 {==}
300
301def parent_atc(~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, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
302 match b:
303 case True{}:
304 parent_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
305 case False{}:
306 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nparent(~K, _)) : M.NodeStore<K> & Nat}
307 {==}
308
309# the field of the list's node (of Free{0} past the length)
310def parent_at_ok(~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) -> {M.ns_parent_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nparent(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Nat}:
311 parent_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
312
313
314# ---- writing one field of a slot ----
315
316def isn(~K: Data, n: M.Node<K>) -> Bool:
317 match n:
318 case M.Free{x}:
319 False{}
320 case M.N{c, lf, rt, pa, k}:
321 True{}
322
323# a live node is below the length
324def nth_or_lt(~K: Data, +xs: List<&2, M.Node<K>>, +i: Nat, +y: M.Node<K>, +hn: {isn(~K, y) == True{} : Bool}, +h: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == y : M.Node<K>}) -> {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}:
325 match xs i:
326 case Nil{} _:
327 Empty.absurd({Nat.is_lt(i, 0n) == True{} : Bool}, L.false_true(L.subst(M.Node<K>, z => {isn(~K, z) == True{} : Bool}, y, M.Free{0n}, Equal.sym(M.Node<K>, M.Free{0n}, y, h), hn)))
328 case Con{x, r} 0n:
329 {==}
330 case Con{x, +r} 1n+q:
331 nth_or_lt(~K, r, q, y, hn, h)
332
333def nth_of_or(-X: Data, +xs: List<&2, X>, +i: Nat, +dv: X, +h: {Nat.is_lt(i, SC.length(X, xs)) == True{} : Bool}) -> {SC.nth(X, xs, i) == Some{ST.nth_or(X, xs, i, dv)} : Maybe<&2, X>}:
334 match xs i:
335 case Nil{} _:
336 Empty.absurd({SC.nth(X, Nil{}, i) == Some{dv} : Maybe<&2, X>}, N.lt_zero_absurd(i, h))
337 case Con{x, r} 0n:
338 {==}
339 case Con{x, +r} 1n+q:
340 nth_of_or(X, r, q, dv, h)
341
342def red_tag_eq(~K: Data, +v: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K) -> {M.ns_red_tag(v) == M.ntag(~K, M.N{v, lf, rt, q, k}) : Nat}:
343 match v:
344 case True{}:
345 {==}
346 case False{}:
347 {==}
348
349def left_set_c(~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, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore<K>}:
350 match c:
351 case True{}:
352 %Equal.sym(Array<Nat> & Nat, 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, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_left_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})) : M.NodeStore<K>}
353 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), NF.left_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{True{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})) : M.NodeStore<K>}
354 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
355 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
356 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
357 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
358 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
359 {==}
360 case False{}:
361 %Equal.sym(Array<Nat> & Nat, 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, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_left_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})) : M.NodeStore<K>}
362 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), NF.left_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{False{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})) : M.NodeStore<K>}
363 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
364 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
365 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore<K>}
366 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, v, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
367 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
368 {==}
369
370# writing the field of a live node: the list with that field replaced
371def left_set_node(~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, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_left(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore<K>}:
372 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
373 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
374 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore<K>}
375 left_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)
376
377def left_set_fc(~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, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
378 match b:
379 case False{}:
380 {==}
381 case True{}:
382 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
383 %Equal.sym(Array<Nat> & Nat, 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, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_left_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
384 {==}
385
386# writing the field of a free slot (or past the length) changes nothing
387def left_set_free(~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, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_left(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
388 left_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
389
390def right_set_c(~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, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore<K>}:
391 match c:
392 case True{}:
393 %Equal.sym(Array<Nat> & Nat, 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, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_right_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})) : M.NodeStore<K>}
394 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), NF.right_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{True{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})) : M.NodeStore<K>}
395 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
396 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
397 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
398 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
399 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
400 {==}
401 case False{}:
402 %Equal.sym(Array<Nat> & Nat, 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, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_right_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})) : M.NodeStore<K>}
403 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), NF.right_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{False{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), _, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})) : M.NodeStore<K>}
404 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
405 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
406 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore<K>}
407 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, v, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
408 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
409 {==}
410
411# writing the field of a live node: the list with that field replaced
412def right_set_node(~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, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_right(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore<K>}:
413 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
414 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
415 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore<K>}
416 right_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)
417
418def right_set_fc(~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, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
419 match b:
420 case False{}:
421 {==}
422 case True{}:
423 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
424 %Equal.sym(Array<Nat> & Nat, 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, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_right_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
425 {==}
426
427# writing the field of a free slot (or past the length) changes nothing
428def right_set_free(~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, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_right(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
429 right_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
430
431def parent_set_c(~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, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore<K>}:
432 match c:
433 case True{}:
434 %Equal.sym(Array<Nat> & Nat, 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, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_parent_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})) : M.NodeStore<K>}
435 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), NF.parent_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{True{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), _, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})) : M.NodeStore<K>}
436 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
437 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
438 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
439 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{True{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
440 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
441 {==}
442 case False{}:
443 %Equal.sym(Array<Nat> & Nat, 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, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_parent_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})) : M.NodeStore<K>}
444 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(i), v), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), NF.parent_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{False{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), _, AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})) : M.NodeStore<K>}
445 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.tags(~K, xs), NF.tags_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
446 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
447 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore<K>}
448 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{False{}, lf, rt, v, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
449 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
450 {==}
451
452# writing the field of a live node: the list with that field replaced
453def parent_set_node(~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, +v: Nat, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_parent(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore<K>}:
454 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
455 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
456 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore<K>}
457 parent_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)
458
459def parent_set_fc(~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, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
460 match b:
461 case False{}:
462 {==}
463 case True{}:
464 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
465 %Equal.sym(Array<Nat> & Nat, 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, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_parent_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
466 {==}
467
468# writing the field of a free slot (or past the length) changes nothing
469def parent_set_free(~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, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_parent(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
470 parent_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
471
472def red_set_c(~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, +v: Bool, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy2: {SC.nth(M.Node<K>, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node<K>>}) -> {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, True{}) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}:
473 match c:
474 case True{}:
475 %Equal.sym(Array<Nat> & Nat, 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, M.N{True{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2)) : {M.ns_set_red_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
476 %Equal.sym(Nat, M.ns_red_tag(v), M.ntag(~K, M.N{v, lf, rt, q, k}), red_tag_eq(~K, v, lf, rt, q, k)) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), Array.set(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.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
477 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), NF.tag_set(~K, l, d, xs, hl, hd, hc, i, M.N{True{}, lf, rt, q, k}, hy2, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), _, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
478 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
479 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
480 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
481 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{True{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
482 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
483 {==}
484 case False{}:
485 %Equal.sym(Array<Nat> & Nat, 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, M.N{False{}, lf, rt, q, k})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2)) : {M.ns_set_red_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
486 %Equal.sym(Nat, M.ns_red_tag(v), M.ntag(~K, M.N{v, lf, rt, q, k}), red_tag_eq(~K, v, lf, rt, q, k)) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), Array.set(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.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
487 %Equal.sym(Array<Nat>, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(i), M.ntag(~K, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), NF.tag_set(~K, l, d, xs, hl, hd, hc, i, M.N{False{}, lf, rt, q, k}, hy2, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), _, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
488 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.lefts(~K, xs), NF.lefts_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
489 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.rights(~K, xs), NF.rights_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
490 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.parents(~K, xs), NF.parents_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, _, 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore<K>}
491 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), NR.keys(~K, xs), NF.keys_keep(~K, xs, i, M.N{False{}, lf, rt, q, k}, M.N{v, lf, rt, q, k}, hy2, {==})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore<K>}
492 %Equal.sym(Nat, SC.length(M.Node<K>, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), SC.length(M.Node<K>, xs), LL.length_update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{}))} : M.NodeStore<K>}
493 {==}
494
495# writing the field of a live node: the list with that field replaced
496def red_set_node(~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, +v: Bool, +c: Bool, +lf: Nat, +rt: Nat, +q: Nat, +k: K, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node<K>}) -> {M.ns_set_red(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}:
497 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy)
498 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, z => Some{z}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.N{c, lf, rt, q, k}, hy))
499 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node<K>, xs)), True{}, hlt) : {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, SC.update(M.Node<K>, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore<K>}
500 red_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2)
501
502def red_set_fc(~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, +v: Bool, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, b) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
503 match b:
504 case False{}:
505 {==}
506 case True{}:
507 +hy2 = Equal.trans(Maybe<&2, M.Node<K>>, SC.nth(M.Node<K>, xs, i), Some{ST.nth_or(M.Node<K>, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node<K>, xs, i, M.Free{0n}, hb), Equal.cong(M.Node<K>, Maybe<&2, M.Node<K>>, w => Some{w}, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{z}, hy))
508 %Equal.sym(Array<Nat> & Nat, 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, M.Free{z})), NF.tag_get(~K, l, d, xs, hl, hd, hc, i, M.Free{z}, hy2)) : {M.ns_set_red_tag(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, v, _) == NR.real(~K, l, d, xs) : M.NodeStore<K>}
509 {==}
510
511# writing the field of a free slot (or past the length) changes nothing
512def red_set_free(~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, +v: Bool, +z: Nat, +hy: {ST.nth_or(M.Node<K>, xs, i, M.Free{0n}) == M.Free{z} : M.Node<K>}) -> {M.ns_set_red(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore<K>}:
513 red_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})
514
515# ---- reading a slot's key ----
516
517def key_ats(~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, +mv: Maybe<&2, M.Node<K>>, +hmv: {SC.nth(M.Node<K>, xs, i) == mv : Maybe<&2, M.Node<K>>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == True{} : Bool}) -> {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}:
518 match mv:
519 case None{}:
520 Empty.absurd({M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}, L.false_true(L.subst(Maybe<&2, M.Node<K>>, z => {isj(M.Node<K>, z) == True{} : Bool}, SC.nth(M.Node<K>, xs, i), None{}, hmv, nth_isj(M.Node<K>, xs, i, hi))))
521 case Some{+y}:
522 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), y, nth_or_some(M.Node<K>, xs, i, y, M.Free{0n}, hmv)) : {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, True{}) == (NR.real(~K, l, d, xs), M.nkey(~K, _)) : M.NodeStore<K> & Maybe<&2, K>}
523 %Equal.sym(Array<Maybe<&2, K>> & Maybe<&2, 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)), NF.key_get(~K, l, d, xs, hl, hd, hc, i, y, hmv)) : {M.ns_key_fin(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), _) == (NR.real(~K, l, d, xs), M.nkey(~K, y)) : M.NodeStore<K> & Maybe<&2, K>}
524 {==}
525
526def key_atc(~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, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node<K>, xs)) == b : Bool}) -> {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, b) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}:
527 match b:
528 case True{}:
529 key_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node<K>, xs, i), {==}, hb)
530 case False{}:
531 %Equal.sym(M.Node<K>, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node<K>, xs, i, M.Free{0n}, hb)) : {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node<K>, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, xs), None{})), i, False{}) == (NR.real(~K, l, d, xs), M.nkey(~K, _)) : M.NodeStore<K> & Maybe<&2, K>}
532 {==}
533
534# the key of the list's node (None for a free slot or past the length)
535def key_at_ok(~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) -> {M.ns_key_at(~K, NR.real(~K, l, d, xs), i) == (NR.real(~K, l, d, xs), M.nkey(~K, ST.nth_or(M.Node<K>, xs, i, M.Free{0n}))) : M.NodeStore<K> & Maybe<&2, K>}:
536 key_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node<K>, xs)), {==})