1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../../src/containers/balanced_search_tree.bend as M 8 import ../../../src/containers/types/dynamic_array.bend as DE 9 import ./bk.bend as BK 10 import ./nsr.bend as NR 11 import ./nsf.bend as NF 12 import ./da.bend as DA 13 import ./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 23 def 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 31 def 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 40 def 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 54 def mk_enc(~K: Data, +y: M.Node) -> {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}: 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 65 def ns_length_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs)) : M.NodeStore & Nat}: 66 {==} 67 68 # ---- read ---- 69 70 def get_some(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +y: M.Node, +hy: {SC.nth(M.Node, xs, i) == Some{y} : Maybe<&2, M.Node>}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, Some{y})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>}: 71 %Equal.sym(Array & 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, 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, Some{y})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>} 72 %Equal.sym(Array & 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, 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, Some{y})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>} 73 %Equal.sym(Array & 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, 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, Some{y})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>} 74 %Equal.sym(Array & 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, 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, Some{y})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>} 75 %Equal.sym(Array> & 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, 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, Some{y})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>} 76 %Equal.sym(M.Node, 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, 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, Some{y})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>} 77 {==} 78 79 def gs(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, i) == mv : Maybe<&2, M.Node>}, +hi: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, mv)) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>}: 80 match mv: 81 case None{}: 82 Empty.absurd({M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, None{})) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, i), None{}, hmv, nth_isj(M.Node, xs, i, hi)))) 83 case Some{+y}: 84 get_some(~K, l, d, xs, hl, hd, hc, i, y, hmv) 85 86 def gc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, SC.nth(M.Node, xs, i))) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>}: 87 match b: 88 case True{}: 89 gs(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node, xs, i), {==}, hb) 90 case False{}: 91 %Equal.sym(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), None{}, LL.nth_none(M.Node, xs, i, N.not_lt_le(i, SC.length(M.Node, xs), hb))) : {M.ns_get_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, _)) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>} 92 {==} 93 94 # a read returns the list's node (IndexOutOfRange past the length) 95 def ns_get_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, SC.nth(M.Node, xs, i))) : M.NodeStore & Result<&2, &2, DE.Error, M.Node>}: 96 gc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 97 98 # ---- write ---- 99 100 101 def set_some(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node, +y0: M.Node, +hy0: {SC.nth(M.Node, xs, i) == Some{y0} : Maybe<&2, M.Node>}) -> {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>}: 102 %Equal.sym(Array, 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, 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, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 103 %Equal.sym(Array, 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, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 104 %Equal.sym(Array, 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, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 105 %Equal.sym(Array, 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, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 106 %Equal.sym(Array>, 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, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, xs, i, x)), 0n)), _}, Done{Unit{}}) == (NR.real(~K, l, d, SC.update(M.Node, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 107 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, x)), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, x)) : {(M.NS{l, d, SC.pow2(d), SC.length(M.Node, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node, 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, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, xs, i, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.update(M.Node, xs, i, x)), None{}))}, Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 108 {==} 109 110 def ws(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, i) == mv : Maybe<&2, M.Node>}, +hi: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & 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, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, i), None{}, hmv, nth_isj(M.Node, 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 118 def ns_set_in(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node, +h: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_set(~K, NR.real(~K, l, d, xs), i, x) == (NR.real(~K, l, d, SC.update(M.Node, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>}: 119 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node, xs)), True{}, h) : {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 120 ws(~K, l, d, xs, hl, hd, hc, i, x, SC.nth(M.Node, xs, i), {==}, h) 121 122 # a write past the length changes nothing 123 def ns_set_out(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +x: M.Node, +h: {Nat.is_lt(i, SC.length(M.Node, 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 & Result<&2, &2, DE.Error, Unit>}: 124 %Equal.sym(Bool, Nat.is_lt(i, SC.length(M.Node, xs)), False{}, h) : {M.ns_set_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Result<&2, &2, DE.Error, Unit>} 125 {==} 126 127 # ---- append ---- 128 129 130 def push_at(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node, +hn: {Nat.is_lt(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_put(~K, l, d, SC.pow2(d), 1n+SC.length(M.Node, 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, xs)), x) == NR.real(~K, l, d, SC.snoc(M.Node, xs, x)) : M.NodeStore}: 131 %Equal.sym(Array, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, xs), 0n)), U32.from_nat(SC.length(M.Node, xs)), M.ntag(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node, 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, xs), _, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(SC.length(M.Node, 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, 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, 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, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node, xs, x)) : M.NodeStore} 132 %Equal.sym(Array, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, xs), 0n)), U32.from_nat(SC.length(M.Node, xs)), M.nleft(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node, 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, 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, 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, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node, xs, x)) : M.NodeStore} 133 %Equal.sym(Array, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, xs), 0n)), U32.from_nat(SC.length(M.Node, xs)), M.nright(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node, 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, 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, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node, xs, x)) : M.NodeStore} 134 %Equal.sym(Array, Array.set(Nat, AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, xs), 0n)), U32.from_nat(SC.length(M.Node, xs)), M.nparent(~K, x)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node, 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, xs)), M.nkey(~K, x))} == NR.real(~K, l, d, SC.snoc(M.Node, xs, x)) : M.NodeStore} 135 %Equal.sym(Array>, 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, xs)), M.nkey(~K, x)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node, xs, x)), 0n)), _} == NR.real(~K, l, d, SC.snoc(M.Node, xs, x)) : M.NodeStore} 136 %Equal.sym(Nat, SC.length(M.Node, SC.snoc(M.Node, xs, x)), 1n+SC.length(M.Node, xs), LL.length_snoc(M.Node, xs, x)) : {M.NS{l, d, SC.pow2(d), 1n+SC.length(M.Node, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node, xs, x)), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.snoc(M.Node, xs, x)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.snoc(M.Node, xs, x)), None{}))} : M.NodeStore} 137 {==} 138 139 # with room: the node appended 140 def ns_push_room(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node, +hn: {Nat.is_lt(SC.length(M.Node, 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, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>}: 141 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node, xs), SC.pow2(d)), True{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 142 Equal.cong(M.NodeStore, M.NodeStore & Result<&2, &2, DE.Error, Unit>, z => (z, Done{Unit{}}), M.ns_put(~K, l, d, SC.pow2(d), 1n+SC.length(M.Node, 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, xs)), x), NR.real(~K, l, d, SC.snoc(M.Node, 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 145 def ns_push_grow(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node, +hn: {Nat.is_lt(SC.length(M.Node, 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, xs, x)), Done{Unit{}}) : M.NodeStore & 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, 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, 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, xs), SC.pow2(d)), False{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, x)), Done{Unit{}}) : M.NodeStore & 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, 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, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 151 %Equal.sym(Array, 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, 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, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 152 %Equal.sym(Array, 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, 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, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 153 %Equal.sym(Array, 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, 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, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 154 %Equal.sym(Array, 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, 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, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 155 %Equal.sym(Array>, 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, 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, xs)), x), Done{Unit{}}) == (NR.real(~K, l, 1n+d, SC.snoc(M.Node, xs, x)), Done{Unit{}}) : M.NodeStore & Result<&2, &2, DE.Error, Unit>} 156 Equal.cong(M.NodeStore, M.NodeStore & 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, 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, xs)), x), NR.real(~K, l, 1n+d, SC.snoc(M.Node, xs, x)), push_at(~K, l, 1n+d, xs, hl, hd1, hc1, x, hn1)) 157 158 # full at the limit: nothing changes 159 def ns_push_full(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +x: M.Node, +hn: {Nat.is_lt(SC.length(M.Node, 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 & Result<&2, &2, DE.Error, Unit>}: 160 %Equal.sym(Bool, Nat.is_lt(SC.length(M.Node, xs), SC.pow2(d)), False{}, hn) : {M.ns_push_room(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & 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, 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 & Result<&2, &2, DE.Error, Unit>} 162 {==} 163 164 # ---- clear ---- 165 166 167 def drop_some(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node, xs) == 1n+m : Nat}, +y0: M.Node, +hy0: {SC.nth(M.Node, xs, m) == Some{y0} : Maybe<&2, M.Node>}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node, xs)) : M.NodeStore}: 168 %Equal.sym(Array, 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, 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, xs)) : M.NodeStore} 169 %Equal.sym(Array, 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, 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, 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, xs)) : M.NodeStore} 170 %Equal.sym(Array, 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, 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, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node, 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, xs)) : M.NodeStore} 171 %Equal.sym(Array, 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, 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, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node, 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, xs)) : M.NodeStore} 172 %Equal.sym(Array>, 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, 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, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node, xs)), 0n)), _} == NR.real(~K, l, d, SC.init(M.Node, xs)) : M.NodeStore} 173 %Equal.sym(Nat, SC.length(M.Node, SC.init(M.Node, xs)), m, len_init(M.Node, 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, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node, xs)), None{}))} == M.NS{l, d, SC.pow2(d), _, AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.lefts(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.init(M.Node, xs)), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, NR.keys(~K, SC.init(M.Node, xs)), None{}))} : M.NodeStore} 174 {==} 175 176 def dr(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node, xs) == 1n+m : Nat}, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, m) == mv : Maybe<&2, M.Node>}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node, xs)) : M.NodeStore}: 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, xs), Equal.sym(Nat, SC.length(M.Node, 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, xs)) : M.NodeStore}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, m), None{}, hmv, nth_isj(M.Node, 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 185 def ns_drop_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +m: Nat, +hm: {SC.length(M.Node, xs) == 1n+m : Nat}) -> {M.ns_drop(~K, NR.real(~K, l, d, xs), m) == NR.real(~K, l, d, SC.init(M.Node, xs)) : M.NodeStore}: 186 dr(~K, l, d, xs, hl, hd, hc, m, hm, SC.nth(M.Node, xs, m), {==}) 187 188 def clr(~K: Data, +k: Nat, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +hk: {SC.length(M.Node, xs) == k : Nat}) -> {M.ns_clear_go(~K, k, NR.real(~K, l, d, xs)) == NR.real(~K, l, d, Nil{}) : M.NodeStore}: 189 match k: 190 case 0n: 191 Equal.cong(List<&2, M.Node>, M.NodeStore, z => NR.real(~K, l, d, z), xs, Nil{}, LL.length_zero_nil(M.Node, xs, hk)) 192 case 1n+ +m: 193 +hm2 = len_init(M.Node, xs, m, hk) 194 %Equal.sym(M.NodeStore, M.ns_drop(~K, NR.real(~K, l, d, xs), m), NR.real(~K, l, d, SC.init(M.Node, 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} 195 clr(~K, m, l, d, SC.init(M.Node, xs), hl, hd, N.le_trans(SC.length(M.Node, SC.init(M.Node, xs)), 1n+m, SC.pow2(d), L.subst(Nat, z => {Nat.is_le(z, 1n+m) == True{} : Bool}, m, SC.length(M.Node, SC.init(M.Node, xs)), Equal.sym(Nat, SC.length(M.Node, SC.init(M.Node, xs)), m, hm2), N.le_succ(m)), L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node, xs), 1n+m, hk, hc)), hm2) 196 197 # clear empties the list, keeping the capacity 198 def ns_clear_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}) -> {M.ns_clear(~K, NR.real(~K, l, d, xs)) == NR.real(~K, l, d, Nil{}) : M.NodeStore}: 199 clr(~K, SC.length(M.Node, xs), l, d, xs, hl, hd, hc, {==}) 200 201 # ---- reading one field of a slot ---- 202 203 204 def 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 211 def 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 220 def 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 229 def tag_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, i) == mv : Maybe<&2, M.Node>}, +hi: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 230 match mv: 231 case None{}: 232 Empty.absurd({M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, i), None{}, hmv, nth_isj(M.Node, xs, i, hi)))) 233 case Some{+y}: 234 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), y, nth_or_some(M.Node, xs, i, y, M.Free{0n}, hmv)) : {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 235 %Equal.sym(Array & 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, 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 & Nat} 236 {==} 237 238 def tag_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 239 match b: 240 case True{}: 241 tag_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node, xs, i), {==}, hb) 242 case False{}: 243 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node, xs, i, M.Free{0n}, hb)) : {M.ns_tag_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 244 {==} 245 246 # the field of the list's node (of Free{0} past the length) 247 def tag_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 248 tag_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 249 250 def left_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, i) == mv : Maybe<&2, M.Node>}, +hi: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 251 match mv: 252 case None{}: 253 Empty.absurd({M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, i), None{}, hmv, nth_isj(M.Node, xs, i, hi)))) 254 case Some{+y}: 255 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), y, nth_or_some(M.Node, xs, i, y, M.Free{0n}, hmv)) : {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 256 %Equal.sym(Array & 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, 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 & Nat} 257 {==} 258 259 def left_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 260 match b: 261 case True{}: 262 left_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node, xs, i), {==}, hb) 263 case False{}: 264 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node, xs, i, M.Free{0n}, hb)) : {M.ns_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 265 {==} 266 267 # the field of the list's node (of Free{0} past the length) 268 def left_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 269 left_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 270 271 def right_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, i) == mv : Maybe<&2, M.Node>}, +hi: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 272 match mv: 273 case None{}: 274 Empty.absurd({M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, i), None{}, hmv, nth_isj(M.Node, xs, i, hi)))) 275 case Some{+y}: 276 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), y, nth_or_some(M.Node, xs, i, y, M.Free{0n}, hmv)) : {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 277 %Equal.sym(Array & 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, 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 & Nat} 278 {==} 279 280 def right_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 281 match b: 282 case True{}: 283 right_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node, xs, i), {==}, hb) 284 case False{}: 285 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node, xs, i, M.Free{0n}, hb)) : {M.ns_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 286 {==} 287 288 # the field of the list's node (of Free{0} past the length) 289 def right_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 290 right_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 291 292 def parent_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, i) == mv : Maybe<&2, M.Node>}, +hi: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 293 match mv: 294 case None{}: 295 Empty.absurd({M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, i), None{}, hmv, nth_isj(M.Node, xs, i, hi)))) 296 case Some{+y}: 297 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), y, nth_or_some(M.Node, xs, i, y, M.Free{0n}, hmv)) : {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 298 %Equal.sym(Array & 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, 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 & Nat} 299 {==} 300 301 def parent_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 302 match b: 303 case True{}: 304 parent_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node, xs, i), {==}, hb) 305 case False{}: 306 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node, xs, i, M.Free{0n}, hb)) : {M.ns_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Nat} 307 {==} 308 309 # the field of the list's node (of Free{0} past the length) 310 def parent_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Nat}: 311 parent_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 312 313 314 # ---- writing one field of a slot ---- 315 316 def isn(~K: Data, n: M.Node) -> 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 324 def nth_or_lt(~K: Data, +xs: List<&2, M.Node>, +i: Nat, +y: M.Node, +hn: {isn(~K, y) == True{} : Bool}, +h: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == y : M.Node}) -> {Nat.is_lt(i, SC.length(M.Node, 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, z => {isn(~K, z) == True{} : Bool}, y, M.Free{0n}, Equal.sym(M.Node, 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 333 def 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 342 def 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 349 def left_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node>}) -> {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore}: 350 match c: 351 case True{}: 352 %Equal.sym(Array & 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, 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, xs, i, M.N{True{}, v, rt, q, k})) : M.NodeStore} 353 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{True{}, v, rt, q, k})) : M.NodeStore} 354 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, M.N{True{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore} 355 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, 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, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore} 356 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, xs, i, M.N{True{}, v, rt, q, k})), None{}))} : M.NodeStore} 357 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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} 358 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{True{}, v, rt, q, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{True{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, 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, 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, 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} 359 {==} 360 case False{}: 361 %Equal.sym(Array & 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, 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, xs, i, M.N{False{}, v, rt, q, k})) : M.NodeStore} 362 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{False{}, v, rt, q, k})) : M.NodeStore} 363 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, M.N{False{}, v, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore} 364 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, 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, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore} 365 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, xs, i, M.N{False{}, v, rt, q, k})), None{}))} : M.NodeStore} 366 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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} 367 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{False{}, v, rt, q, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{False{}, v, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, 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, 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, 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} 368 {==} 369 370 # writing the field of a live node: the list with that field replaced 371 def left_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node}) -> {M.ns_set_left(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore}: 372 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy) 373 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node, Maybe<&2, M.Node>, z => Some{z}, ST.nth_or(M.Node, 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, xs)), True{}, hlt) : {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{c, v, rt, q, k})) : M.NodeStore} 375 left_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2) 376 377 def left_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_set_left_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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}: 378 match b: 379 case False{}: 380 {==} 381 case True{}: 382 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hb), Equal.cong(M.Node, Maybe<&2, M.Node>, w => Some{w}, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{z}, hy)) 383 %Equal.sym(Array & 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, 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} 384 {==} 385 386 # writing the field of a free slot (or past the length) changes nothing 387 def left_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}) -> {M.ns_set_left(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore}: 388 left_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 389 390 def right_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node>}) -> {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore}: 391 match c: 392 case True{}: 393 %Equal.sym(Array & 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, 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, xs, i, M.N{True{}, lf, v, q, k})) : M.NodeStore} 394 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{True{}, lf, v, q, k})) : M.NodeStore} 395 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore} 396 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore} 397 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, xs, i, M.N{True{}, lf, v, q, k})), None{}))} : M.NodeStore} 398 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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} 399 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{True{}, lf, v, q, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{True{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, 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, 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, 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} 400 {==} 401 case False{}: 402 %Equal.sym(Array & 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, 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, xs, i, M.N{False{}, lf, v, q, k})) : M.NodeStore} 403 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{False{}, lf, v, q, k})) : M.NodeStore} 404 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore} 405 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, v, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore} 406 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, xs, i, M.N{False{}, lf, v, q, k})), None{}))} : M.NodeStore} 407 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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} 408 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{False{}, lf, v, q, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{False{}, lf, v, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, 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, 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, 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} 409 {==} 410 411 # writing the field of a live node: the list with that field replaced 412 def right_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node}) -> {M.ns_set_right(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore}: 413 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy) 414 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node, Maybe<&2, M.Node>, z => Some{z}, ST.nth_or(M.Node, 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, xs)), True{}, hlt) : {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{c, lf, v, q, k})) : M.NodeStore} 416 right_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2) 417 418 def right_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_set_right_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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}: 419 match b: 420 case False{}: 421 {==} 422 case True{}: 423 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hb), Equal.cong(M.Node, Maybe<&2, M.Node>, w => Some{w}, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{z}, hy)) 424 %Equal.sym(Array & 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, 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} 425 {==} 426 427 # writing the field of a free slot (or past the length) changes nothing 428 def right_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}) -> {M.ns_set_right(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore}: 429 right_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 430 431 def parent_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node>}) -> {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore}: 432 match c: 433 case True{}: 434 %Equal.sym(Array & 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, 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, xs, i, M.N{True{}, lf, rt, v, k})) : M.NodeStore} 435 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{True{}, lf, rt, v, k})) : M.NodeStore} 436 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore} 437 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore} 438 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, xs, i, M.N{True{}, lf, rt, v, k})), None{}))} : M.NodeStore} 439 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{True{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore} 440 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{True{}, lf, rt, v, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{True{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, 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, 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, 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} 441 {==} 442 case False{}: 443 %Equal.sym(Array & 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, 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, xs, i, M.N{False{}, lf, rt, v, k})) : M.NodeStore} 444 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{False{}, lf, rt, v, k})) : M.NodeStore} 445 %Equal.sym(List<&2, Nat>, NR.tags(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.rights(~K, SC.update(M.Node, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore} 446 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore} 447 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, 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, xs, i, M.N{False{}, lf, rt, v, k})), None{}))} : M.NodeStore} 448 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, 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, 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, SC.update(M.Node, 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, xs, i, M.N{False{}, lf, rt, v, k})), 0n)), AR.thaw(Maybe<&2, K>, BK.bk(Maybe<&2, K>, d, _, None{}))} : M.NodeStore} 449 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{False{}, lf, rt, v, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{False{}, lf, rt, v, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, 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, 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, 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} 450 {==} 451 452 # writing the field of a live node: the list with that field replaced 453 def parent_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node}) -> {M.ns_set_parent(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore}: 454 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy) 455 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node, Maybe<&2, M.Node>, z => Some{z}, ST.nth_or(M.Node, 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, xs)), True{}, hlt) : {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{c, lf, rt, v, k})) : M.NodeStore} 457 parent_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2) 458 459 def parent_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_set_parent_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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}: 460 match b: 461 case False{}: 462 {==} 463 case True{}: 464 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hb), Equal.cong(M.Node, Maybe<&2, M.Node>, w => Some{w}, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{z}, hy)) 465 %Equal.sym(Array & 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, 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} 466 {==} 467 468 # writing the field of a free slot (or past the length) changes nothing 469 def parent_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Nat, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}) -> {M.ns_set_parent(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore}: 470 parent_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 471 472 def red_set_c(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i) == Some{M.N{c, lf, rt, q, k}} : Maybe<&2, M.Node>}) -> {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore}: 473 match c: 474 case True{}: 475 %Equal.sym(Array & 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, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore} 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, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore} 477 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore} 478 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore} 479 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, 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, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore} 480 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore} 481 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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} 482 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, 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} 483 {==} 484 case False{}: 485 %Equal.sym(Array & 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, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore} 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, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore} 487 %Equal.sym(Array, 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, 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, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore} 488 %Equal.sym(List<&2, Nat>, NR.lefts(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})), 0n)), AR.thaw(Nat, BK.bk(Nat, d, NR.parents(~K, SC.update(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore} 489 %Equal.sym(List<&2, Nat>, NR.rights(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, 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, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore} 490 %Equal.sym(List<&2, Nat>, NR.parents(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})), None{}))} : M.NodeStore} 491 %Equal.sym(List<&2, Maybe<&2, K>>, NR.keys(~K, SC.update(M.Node, 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, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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} 492 %Equal.sym(Nat, SC.length(M.Node, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})), SC.length(M.Node, xs), LL.length_update(M.Node, xs, i, M.N{v, lf, rt, q, k})) : {M.NS{l, d, SC.pow2(d), SC.length(M.Node, xs), AR.thaw(Nat, BK.bk(Nat, d, NR.tags(~K, SC.update(M.Node, 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, 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} 493 {==} 494 495 # writing the field of a live node: the list with that field replaced 496 def red_set_node(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}) == M.N{c, lf, rt, q, k} : M.Node}) -> {M.ns_set_red(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, SC.update(M.Node, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore}: 497 +hlt = nth_or_lt(~K, xs, i, M.N{c, lf, rt, q, k}, {==}, hy) 498 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.N{c, lf, rt, q, k}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hlt), Equal.cong(M.Node, Maybe<&2, M.Node>, z => Some{z}, ST.nth_or(M.Node, 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, xs)), True{}, hlt) : {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.N{v, lf, rt, q, k})) : M.NodeStore} 500 red_set_c(~K, l, d, xs, hl, hd, hc, i, v, c, lf, rt, q, k, hy2) 501 502 def red_set_fc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Bool, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_set_red_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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}: 503 match b: 504 case False{}: 505 {==} 506 case True{}: 507 +hy2 = Equal.trans(Maybe<&2, M.Node>, SC.nth(M.Node, xs, i), Some{ST.nth_or(M.Node, xs, i, M.Free{0n})}, Some{M.Free{z}}, nth_of_or(M.Node, xs, i, M.Free{0n}, hb), Equal.cong(M.Node, Maybe<&2, M.Node>, w => Some{w}, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{z}, hy)) 508 %Equal.sym(Array & 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, 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} 509 {==} 510 511 # writing the field of a free slot (or past the length) changes nothing 512 def red_set_free(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +v: Bool, +z: Nat, +hy: {ST.nth_or(M.Node, xs, i, M.Free{0n}) == M.Free{z} : M.Node}) -> {M.ns_set_red(~K, NR.real(~K, l, d, xs), i, v) == NR.real(~K, l, d, xs) : M.NodeStore}: 513 red_set_fc(~K, l, d, xs, hl, hd, hc, i, v, z, hy, Nat.is_lt(i, SC.length(M.Node, xs)), {==}) 514 515 # ---- reading a slot's key ---- 516 517 def key_ats(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +mv: Maybe<&2, M.Node>, +hmv: {SC.nth(M.Node, xs, i) == mv : Maybe<&2, M.Node>}, +hi: {Nat.is_lt(i, SC.length(M.Node, xs)) == True{} : Bool}) -> {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & 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, 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, xs, i, M.Free{0n}))) : M.NodeStore & Maybe<&2, K>}, L.false_true(L.subst(Maybe<&2, M.Node>, z => {isj(M.Node, z) == True{} : Bool}, SC.nth(M.Node, xs, i), None{}, hmv, nth_isj(M.Node, xs, i, hi)))) 521 case Some{+y}: 522 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), y, nth_or_some(M.Node, xs, i, y, M.Free{0n}, hmv)) : {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Maybe<&2, K>} 523 %Equal.sym(Array> & 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, 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 & Maybe<&2, K>} 524 {==} 525 526 def key_atc(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, xs), SC.pow2(d)) == True{} : Bool}, +i: Nat, +b: Bool, +hb: {Nat.is_lt(i, SC.length(M.Node, xs)) == b : Bool}) -> {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Maybe<&2, K>}: 527 match b: 528 case True{}: 529 key_ats(~K, l, d, xs, hl, hd, hc, i, SC.nth(M.Node, xs, i), {==}, hb) 530 case False{}: 531 %Equal.sym(M.Node, ST.nth_or(M.Node, xs, i, M.Free{0n}), M.Free{0n}, nth_or_hi(M.Node, xs, i, M.Free{0n}, hb)) : {M.ns_key_ok(~K, l, d, SC.pow2(d), SC.length(M.Node, 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 & Maybe<&2, K>} 532 {==} 533 534 # the key of the list's node (None for a free slot or past the length) 535 def key_at_ok(~K: Data, +l: Nat, +d: Nat, +xs: List<&2, M.Node>, +hl: {Nat.is_le(l, 31n) == True{} : Bool}, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hc: {Nat.is_le(SC.length(M.Node, 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, xs, i, M.Free{0n}))) : M.NodeStore & Maybe<&2, K>}: 536 key_atc(~K, l, d, xs, hl, hd, hc, i, Nat.is_lt(i, SC.length(M.Node, xs)), {==})