proofs/containers/balanced_search_tree/path.bend
bend-collections-laws-containers@1.0.0.0 · 235 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/tree.bend as TR
9import bend-collections-laws-containers@1.0.0.0/proofs/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
19type Fr is Data:
20 FR{p: Nat, lft: Bool, sib: ST.Tr}
21
22
23def fp(f: Fr) -> Nat:
24 match f:
25 case FR{+p, lft, s}:
26 p
27
28def top(c: List<&2, Fr>) -> Nat:
29 match c:
30 case Nil{}:
31 0n
32 case Con{+f, t}:
33 fp(f)
34
35def 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
44def 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
54def 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
61def 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
70def cok1(~K: Data, f: Fr, +x: Nat, +q: Nat, +nl: List<&2, M.Node<K>>) -> 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
75def ctxok(~K: Data, c: List<&2, Fr>, +x: Nat, +nl: List<&2, M.Node<K>>) -> 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
85def 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
89def 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
96def 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
99def 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
103def ok_l(~K: Data, +nl: List<&2, M.Node<K>>, +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
109def ok_r(~K: Data, +nl: List<&2, M.Node<K>>, +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)
118def 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
128def 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
132def 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
135def 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
139def 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
148def 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
151def 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
160def nd_dist(~K: Data, +nl: List<&2, M.Node<K>>, +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
204def 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
212def 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
220def 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)}))