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 ../../../spec/lib/common.bend as SC 6 import ../../../src/containers/balanced_search_tree.bend as M 7 import ./state.bend as ST 8 import ./tree.bend as TR 9 import ../../lib/nat_list.bend as NL 10 11 # Paths into the ghost tree: the frames from a subtree up to the root (the 12 # parent's id, whether the subtree is its left child, the sibling), the ids 13 # before and after the subtree in key order, and the links each frame's 14 # parent has. A descent extends the path; the ids split around the subtree; 15 # with no repeated ids a subtree's root differs from every sibling's; the 16 # path is shorter than the ids. (source: tools/generators/tm_hand/path.src) 17 18 19 type Fr is Data: 20 FR{p: Nat, lft: Bool, sib: ST.Tr} 21 22 23 def fp(f: Fr) -> Nat: 24 match f: 25 case FR{+p, lft, s}: 26 p 27 28 def top(c: List<&2, Fr>) -> Nat: 29 match c: 30 case Nil{}: 31 0n 32 case Con{+f, t}: 33 fp(f) 34 35 def bef1(f: Fr, +b: List<&2, Nat>) -> List<&2, Nat>: 36 match f: 37 case FR{+p, lft, s}: 38 match lft: 39 case True{}: 40 b 41 case False{}: 42 SC.append(Nat, b, SC.append(Nat, ST.ids(s), Con{p, Nil{}})) 43 44 def aft1(f: Fr, +a: List<&2, Nat>) -> List<&2, Nat>: 45 match f: 46 case FR{+p, lft, s}: 47 match lft: 48 case True{}: 49 Con{p, SC.append(Nat, ST.ids(s), a)} 50 case False{}: 51 a 52 53 # the ids before and after the subtree the path leads to 54 def before(c: List<&2, Fr>) -> List<&2, Nat>: 55 match c: 56 case Nil{}: 57 Nil{} 58 case Con{+f, t}: 59 bef1(f, before(t)) 60 61 def after(c: List<&2, Fr>) -> List<&2, Nat>: 62 match c: 63 case Nil{}: 64 Nil{} 65 case Con{+f, t}: 66 aft1(f, after(t)) 67 68 # a frame's parent links to x on its side, to the sibling on the other, and 69 # to q above; the sibling hangs below it 70 def cok1(~K: Data, f: Fr, +x: Nat, +q: Nat, +nl: List<&2, M.Node>) -> Bool: 71 match f: 72 case FR{+p, +lft, +s}: 73 Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), q), ST.rep(~K, s, p, nl))) 74 75 def ctxok(~K: Data, c: List<&2, Fr>, +x: Nat, +nl: List<&2, M.Node>) -> Bool: 76 match c: 77 case Nil{}: 78 True{} 79 case Con{+f, +t}: 80 Bool.and(cok1(~K, f, x, top(t), nl), ctxok(~K, t, fp(f), nl)) 81 82 83 # ---- the ids around a descent ---- 84 85 def eq_l(+b: List<&2, Nat>, +a: List<&2, Nat>, +i: Nat, +x: List<&2, Nat>, +y: List<&2, Nat>) -> {SC.append(Nat, b, SC.append(Nat, SC.append(Nat, x, Con{i, y}), a)) == SC.append(Nat, b, SC.append(Nat, x, Con{i, SC.append(Nat, y, a)})) : List<&2, Nat>}: 86 %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, x, Con{i, y}), a), SC.append(Nat, x, SC.append(Nat, Con{i, y}, a)), LL.append_assoc(Nat, x, Con{i, y}, a)) : {SC.append(Nat, b, _) == SC.append(Nat, b, SC.append(Nat, x, Con{i, SC.append(Nat, y, a)})) : List<&2, Nat>} 87 {==} 88 89 def eq_r(+b: List<&2, Nat>, +a: List<&2, Nat>, +i: Nat, +x: List<&2, Nat>, +y: List<&2, Nat>) -> {SC.append(Nat, b, SC.append(Nat, SC.append(Nat, x, Con{i, y}), a)) == SC.append(Nat, SC.append(Nat, b, SC.append(Nat, x, Con{i, Nil{}})), SC.append(Nat, y, a)) : List<&2, Nat>}: 90 %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, b, SC.append(Nat, x, Con{i, Nil{}})), SC.append(Nat, y, a)), SC.append(Nat, b, SC.append(Nat, SC.append(Nat, x, Con{i, Nil{}}), SC.append(Nat, y, a))), LL.append_assoc(Nat, b, SC.append(Nat, x, Con{i, Nil{}}), SC.append(Nat, y, a))) : {SC.append(Nat, b, SC.append(Nat, SC.append(Nat, x, Con{i, y}), a)) == _ : List<&2, Nat>} 91 %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, x, Con{i, Nil{}}), SC.append(Nat, y, a)), SC.append(Nat, x, SC.append(Nat, Con{i, Nil{}}, SC.append(Nat, y, a))), LL.append_assoc(Nat, x, Con{i, Nil{}}, SC.append(Nat, y, a))) : {SC.append(Nat, b, SC.append(Nat, SC.append(Nat, x, Con{i, y}), a)) == SC.append(Nat, b, _) : List<&2, Nat>} 92 eq_l(b, a, i, x, y) 93 94 95 # the ids, split around a subtree, split around its left child 96 def ids_l(+c: List<&2, Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr) -> {SC.append(Nat, before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(c))) == SC.append(Nat, before(Con{FR{i, True{}, r}, c}), SC.append(Nat, ST.ids(l), after(Con{FR{i, True{}, r}, c}))) : List<&2, Nat>}: 97 eq_l(before(c), after(c), i, ST.ids(l), ST.ids(r)) 98 99 def ids_r(+c: List<&2, Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr) -> {SC.append(Nat, before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(c))) == SC.append(Nat, before(Con{FR{i, False{}, l}, c}), SC.append(Nat, ST.ids(r), after(Con{FR{i, False{}, l}, c}))) : List<&2, Nat>}: 100 eq_r(before(c), after(c), i, ST.ids(l), ST.ids(r)) 101 102 # the links along a descent 103 def ok_l(~K: Data, +nl: List<&2, M.Node>, +c: List<&2, Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +hr: {ST.rep(~K, ST.TN{i, l, r}, top(c), nl) == True{} : Bool}, +hc: {ctxok(~K, c, i, nl) == True{} : Bool}) -> {ctxok(~K, Con{FR{i, True{}, r}, c}, ST.rid(l), nl) == True{} : Bool} & {ST.rep(~K, l, i, nl) == True{} : Bool}: 104 +h2 = L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl))), hr) 105 +h3 = L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl)), h2) 106 +k1 = L.and_intro(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), ST.rep(~K, r, i, nl)), L.and_left(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl))), hr), L.and_intro(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), ST.rep(~K, r, i, nl), L.and_left(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl)), h2), L.and_right(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl), h3))) 107 (L.and_intro(cok1(~K, FR{i, True{}, r}, ST.rid(l), top(c), nl), ctxok(~K, c, i, nl), k1, hc), L.and_left(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl), h3)) 108 109 def ok_r(~K: Data, +nl: List<&2, M.Node>, +c: List<&2, Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +hr: {ST.rep(~K, ST.TN{i, l, r}, top(c), nl) == True{} : Bool}, +hc: {ctxok(~K, c, i, nl) == True{} : Bool}) -> {ctxok(~K, Con{FR{i, False{}, l}, c}, ST.rid(r), nl) == True{} : Bool} & {ST.rep(~K, r, i, nl) == True{} : Bool}: 110 +h2 = L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl))), hr) 111 +h3 = L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl)), h2) 112 +k1 = L.and_intro(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), ST.rep(~K, l, i, nl)), L.and_left(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl))), hr), L.and_intro(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), ST.rep(~K, l, i, nl), L.and_left(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), top(c)), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl)), h2), L.and_left(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl), h3))) 113 (L.and_intro(cok1(~K, FR{i, False{}, l}, ST.rid(r), top(c), nl), ctxok(~K, c, i, nl), k1, hc), L.and_right(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl), h3)) 114 115 # ---- siblings differ ---- 116 117 # the subtree's root is none of the frames' siblings (walking up) 118 def dist(c: List<&2, Fr>, +x: Nat) -> Bool: 119 match c: 120 case Nil{}: 121 True{} 122 case Con{+f, +t}: 123 match f: 124 case FR{+p, lft, +s}: 125 Bool.and(Bool.not(Nat.is_eq(x, ST.rid(s))), dist(t, p)) 126 127 128 def mem_self(+i: Nat, +y: List<&2, Nat>) -> {NL.memn(i, Con{i, y}) == True{} : Bool}: 129 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {Bool.or(_, NL.memn(i, y)) == True{} : Bool} 130 {==} 131 132 def mem_root(+i: Nat, +l: ST.Tr, +r: ST.Tr) -> {NL.memn(i, ST.ids(ST.TN{i, l, r})) == True{} : Bool}: 133 NL.mem_app_r(i, ST.ids(l), Con{i, ST.ids(r)}, mem_self(i, ST.ids(r))) 134 135 def mem_cons(+y: Nat, +p: Nat, +xs: List<&2, Nat>, +h: {NL.memn(y, xs) == True{} : Bool}) -> {NL.memn(y, Con{p, xs}) == True{} : Bool}: 136 %Equal.sym(Bool, NL.memn(y, xs), True{}, h) : {Bool.or(Nat.is_eq(p, y), _) == True{} : Bool} 137 NL.or_true_b(Nat.is_eq(p, y)) 138 139 def ne_c(+i: Nat, +j: Nat, +xs: List<&2, Nat>, +hi: {NL.memn(i, xs) == False{} : Bool}, +hj: {NL.memn(j, xs) == True{} : Bool}, +b: Bool, +hb: {Nat.is_eq(i, j) == b : Bool}) -> {Bool.not(b) == True{} : Bool}: 140 match b: 141 case True{}: 142 +e = N.eq_from_is_eq(i, j, hb) 143 Empty.absurd({Bool.not(True{}) == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, NL.memn(i, xs), False{}, Equal.sym(Bool, NL.memn(i, xs), True{}, L.subst(Nat, z => {NL.memn(z, xs) == True{} : Bool}, j, i, Equal.sym(Nat, i, j, e), hj)), hi))) 144 case False{}: 145 {==} 146 147 # an absent id differs from a present one 148 def ne_mem(+i: Nat, +j: Nat, +xs: List<&2, Nat>, +hi: {NL.memn(i, xs) == False{} : Bool}, +hj: {NL.memn(j, xs) == True{} : Bool}) -> {Bool.not(Nat.is_eq(i, j)) == True{} : Bool}: 149 ne_c(i, j, xs, hi, hj, Nat.is_eq(i, j), {==}) 150 151 def ne_zero(+i: Nat, +hi: {Nat.is_lt(0n, i) == True{} : Bool}) -> {Bool.not(Nat.is_eq(i, 0n)) == True{} : Bool}: 152 match i: 153 case 0n: 154 Empty.absurd({Bool.not(Nat.is_eq(0n, 0n)) == True{} : Bool}, L.false_true(hi)) 155 case 1n+j: 156 {==} 157 158 159 # the root differs from every sibling, when no id repeats 160 def nd_dist(~K: Data, +nl: List<&2, M.Node>, +c: List<&2, Fr>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +hi: {Nat.is_lt(0n, i) == True{} : Bool}, +hok: {ctxok(~K, c, i, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, before(c), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(c)))) == True{} : Bool}) -> {dist(c, i) == True{} : Bool}: 161 match c: 162 case Nil{}: 163 {==} 164 case Con{+f, +t}: 165 match f: 166 case FR{+p, +lft, +s}: 167 match lft: 168 case True{}: 169 match s: 170 case ST.TE{}: 171 +hk = L.and_left(cok1(~K, FR{p, True{}, ST.TE{}}, i, top(t), nl), ctxok(~K, t, p, nl), hok) 172 +hp = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), i, ST.rid(ST.TE{}), top(t)), ST.rep(~K, ST.TE{}, p, nl)), hk) 173 +hn = NL.nd_dj2(ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TE{}}, t}), NL.nd_r(before(t), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TE{}}, t})), hnd), i, mem_root(i, l, r)) 174 +hnd2 = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, before(Con{FR{p, True{}, ST.TE{}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TE{}}, t}))), SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{i, l, r}, ST.TE{}}), after(t))), Equal.sym(List<&2, Nat>, SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{i, l, r}, ST.TE{}}), after(t))), SC.append(Nat, before(Con{FR{p, True{}, ST.TE{}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TE{}}, t}))), ids_l(t, p, ST.TN{i, l, r}, ST.TE{})), hnd) 175 +rec = nd_dist(~K, nl, t, p, ST.TN{i, l, r}, ST.TE{}, hp, L.and_right(cok1(~K, FR{p, True{}, ST.TE{}}, i, top(t), nl), ctxok(~K, t, p, nl), hok), hnd2) 176 L.and_intro(Bool.not(Nat.is_eq(i, 0n)), dist(t, p), ne_zero(i, hi), rec) 177 case ST.TN{+j, +sl, +sr}: 178 +hk = L.and_left(cok1(~K, FR{p, True{}, ST.TN{j, sl, sr}}, i, top(t), nl), ctxok(~K, t, p, nl), hok) 179 +hp = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), i, ST.rid(ST.TN{j, sl, sr}), top(t)), ST.rep(~K, ST.TN{j, sl, sr}, p, nl)), hk) 180 +hn = NL.nd_dj2(ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TN{j, sl, sr}}, t}), NL.nd_r(before(t), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TN{j, sl, sr}}, t})), hnd), i, mem_root(i, l, r)) 181 +hnd2 = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, before(Con{FR{p, True{}, ST.TN{j, sl, sr}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TN{j, sl, sr}}, t}))), SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{i, l, r}, ST.TN{j, sl, sr}}), after(t))), Equal.sym(List<&2, Nat>, SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{i, l, r}, ST.TN{j, sl, sr}}), after(t))), SC.append(Nat, before(Con{FR{p, True{}, ST.TN{j, sl, sr}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, True{}, ST.TN{j, sl, sr}}, t}))), ids_l(t, p, ST.TN{i, l, r}, ST.TN{j, sl, sr})), hnd) 182 +rec = nd_dist(~K, nl, t, p, ST.TN{i, l, r}, ST.TN{j, sl, sr}, hp, L.and_right(cok1(~K, FR{p, True{}, ST.TN{j, sl, sr}}, i, top(t), nl), ctxok(~K, t, p, nl), hok), hnd2) 183 L.and_intro(Bool.not(Nat.is_eq(i, j)), dist(t, p), ne_mem(i, j, after(Con{FR{p, True{}, ST.TN{j, sl, sr}}, t}), hn, mem_cons(j, p, SC.append(Nat, ST.ids(ST.TN{j, sl, sr}), after(t)), NL.mem_app_l(j, ST.ids(ST.TN{j, sl, sr}), after(t), mem_root(j, sl, sr)))), rec) 184 case False{}: 185 match s: 186 case ST.TE{}: 187 +hk = L.and_left(cok1(~K, FR{p, False{}, ST.TE{}}, i, top(t), nl), ctxok(~K, t, p, nl), hok) 188 +hp = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(ST.TE{}), i, top(t)), ST.rep(~K, ST.TE{}, p, nl)), hk) 189 +hn = NL.nd_dj(before(Con{FR{p, False{}, ST.TE{}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(t)), hnd, i, NL.mem_app_l(i, ST.ids(ST.TN{i, l, r}), after(t), mem_root(i, l, r))) 190 +hnd2 = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, before(Con{FR{p, False{}, ST.TE{}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, False{}, ST.TE{}}, t}))), SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TE{}, ST.TN{i, l, r}}), after(t))), Equal.sym(List<&2, Nat>, SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TE{}, ST.TN{i, l, r}}), after(t))), SC.append(Nat, before(Con{FR{p, False{}, ST.TE{}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, False{}, ST.TE{}}, t}))), ids_r(t, p, ST.TE{}, ST.TN{i, l, r})), hnd) 191 +rec = nd_dist(~K, nl, t, p, ST.TE{}, ST.TN{i, l, r}, hp, L.and_right(cok1(~K, FR{p, False{}, ST.TE{}}, i, top(t), nl), ctxok(~K, t, p, nl), hok), hnd2) 192 L.and_intro(Bool.not(Nat.is_eq(i, 0n)), dist(t, p), ne_zero(i, hi), rec) 193 case ST.TN{+j, +sl, +sr}: 194 +hk = L.and_left(cok1(~K, FR{p, False{}, ST.TN{j, sl, sr}}, i, top(t), nl), ctxok(~K, t, p, nl), hok) 195 +hp = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(ST.TN{j, sl, sr}), i, top(t)), ST.rep(~K, ST.TN{j, sl, sr}, p, nl)), hk) 196 +hn = NL.nd_dj(before(Con{FR{p, False{}, ST.TN{j, sl, sr}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(t)), hnd, i, NL.mem_app_l(i, ST.ids(ST.TN{i, l, r}), after(t), mem_root(i, l, r))) 197 +hnd2 = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, before(Con{FR{p, False{}, ST.TN{j, sl, sr}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, False{}, ST.TN{j, sl, sr}}, t}))), SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{j, sl, sr}, ST.TN{i, l, r}}), after(t))), Equal.sym(List<&2, Nat>, SC.append(Nat, before(t), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{j, sl, sr}, ST.TN{i, l, r}}), after(t))), SC.append(Nat, before(Con{FR{p, False{}, ST.TN{j, sl, sr}}, t}), SC.append(Nat, ST.ids(ST.TN{i, l, r}), after(Con{FR{p, False{}, ST.TN{j, sl, sr}}, t}))), ids_r(t, p, ST.TN{j, sl, sr}, ST.TN{i, l, r})), hnd) 198 +rec = nd_dist(~K, nl, t, p, ST.TN{j, sl, sr}, ST.TN{i, l, r}, hp, L.and_right(cok1(~K, FR{p, False{}, ST.TN{j, sl, sr}}, i, top(t), nl), ctxok(~K, t, p, nl), hok), hnd2) 199 L.and_intro(Bool.not(Nat.is_eq(i, j)), dist(t, p), ne_mem(i, j, before(Con{FR{p, False{}, ST.TN{j, sl, sr}}, t}), hn, NL.mem_app_r(j, before(t), SC.append(Nat, ST.ids(ST.TN{j, sl, sr}), Con{p, Nil{}}), NL.mem_app_l(j, ST.ids(ST.TN{j, sl, sr}), Con{p, Nil{}}, mem_root(j, sl, sr)))), rec) 200 201 # ---- the path is shorter than the ids ---- 202 203 204 def cons_len(+x: List<&2, Nat>, +p: Nat, +y: List<&2, Nat>) -> {SC.length(Nat, SC.append(Nat, x, Con{p, y})) == 1n+SC.length(Nat, SC.append(Nat, x, y)) : Nat}: 205 match x: 206 case Nil{}: 207 {==} 208 case Con{+h, +t}: 209 %Equal.sym(Nat, SC.length(Nat, SC.append(Nat, t, Con{p, y})), 1n+SC.length(Nat, SC.append(Nat, t, y)), cons_len(t, p, y)) : {1n+_ == 1n+1n+SC.length(Nat, SC.append(Nat, t, y)) : Nat} 210 {==} 211 212 def ins_le(+x: List<&2, Nat>, +z: List<&2, Nat>, +y: List<&2, Nat>) -> {Nat.is_le(SC.length(Nat, SC.append(Nat, x, y)), SC.length(Nat, SC.append(Nat, x, SC.append(Nat, z, y)))) == True{} : Bool}: 213 match x: 214 case Nil{}: 215 %Equal.sym(Nat, SC.length(Nat, SC.append(Nat, z, y)), Nat.add(SC.length(Nat, z), SC.length(Nat, y)), LL.length_append(Nat, z, y)) : {Nat.is_le(SC.length(Nat, y), _) == True{} : Bool} 216 TR.le_add_l(SC.length(Nat, z), SC.length(Nat, y)) 217 case Con{+h, +t}: 218 ins_le(t, z, y) 219 220 def depth(+c: List<&2, Fr>) -> {Nat.is_le(SC.length(Fr, c), SC.length(Nat, SC.append(Nat, before(c), after(c)))) == True{} : Bool}: 221 match c: 222 case Nil{}: 223 {==} 224 case Con{+f, +t}: 225 match f: 226 case FR{+p, +lft, +s}: 227 match lft: 228 case True{}: 229 %Equal.sym(Nat, SC.length(Nat, SC.append(Nat, before(t), Con{p, SC.append(Nat, ST.ids(s), after(t))})), 1n+SC.length(Nat, SC.append(Nat, before(t), SC.append(Nat, ST.ids(s), after(t)))), cons_len(before(t), p, SC.append(Nat, ST.ids(s), after(t)))) : {Nat.is_le(1n+SC.length(Fr, t), _) == True{} : Bool} 230 N.le_trans(SC.length(Fr, t), SC.length(Nat, SC.append(Nat, before(t), after(t))), SC.length(Nat, SC.append(Nat, before(t), SC.append(Nat, ST.ids(s), after(t)))), depth(t), ins_le(before(t), ST.ids(s), after(t))) 231 case False{}: 232 %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, before(t), SC.append(Nat, ST.ids(s), Con{p, Nil{}})), after(t)), SC.append(Nat, before(t), SC.append(Nat, SC.append(Nat, ST.ids(s), Con{p, Nil{}}), after(t))), LL.append_assoc(Nat, before(t), SC.append(Nat, ST.ids(s), Con{p, Nil{}}), after(t))) : {Nat.is_le(1n+SC.length(Fr, t), SC.length(Nat, _)) == True{} : Bool} 233 %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, ST.ids(s), Con{p, Nil{}}), after(t)), SC.append(Nat, ST.ids(s), Con{p, after(t)}), LL.append_assoc(Nat, ST.ids(s), Con{p, Nil{}}, after(t))) : {Nat.is_le(1n+SC.length(Fr, t), SC.length(Nat, SC.append(Nat, before(t), _))) == True{} : Bool} 234 +x = L.subst(Nat, z => {Nat.is_le(1n+SC.length(Fr, t), z) == True{} : Bool}, 1n+SC.length(Nat, SC.append(Nat, before(t), after(t))), SC.length(Nat, SC.append(Nat, before(t), Con{p, after(t)})), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, before(t), Con{p, after(t)})), 1n+SC.length(Nat, SC.append(Nat, before(t), after(t))), cons_len(before(t), p, after(t))), depth(t)) 235 N.le_trans(1n+SC.length(Fr, t), SC.length(Nat, SC.append(Nat, before(t), Con{p, after(t)})), SC.length(Nat, SC.append(Nat, before(t), SC.append(Nat, ST.ids(s), Con{p, after(t)}))), x, ins_le(before(t), ST.ids(s), Con{p, after(t)}))