proofs/containers/balanced_search_tree/agree.bend
bend-collections-laws-containers@1.0.0.0 · 238 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/order.bend as O
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as P
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as EN
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/frame.bend as FR
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
14
15# Two node lists agreeing on a list of ids (a Bool, so the fact can be used
16# many times): nodes compared field by field, keys by the comparator, which
17# for a lawful one is equality. Agreement on a subtree's ids keeps its links,
18# on a list its entries, on a path its frames; a write agrees off its id;
19# agreement composes. (source: tools/generators/tm_hand/agree.src)
20
21
22def beq(+a: Bool, +b: Bool) -> Bool:
23 match a:
24 case True{}:
25 b
26 case False{}:
27 Bool.not(b)
28
29def ndeq(~K: Data, ~cmp: K -> K -> Cmp, x: M.Node<K>, y: M.Node<K>) -> Bool:
30 match x y:
31 case M.Free{+a} M.Free{+b}:
32 Nat.is_eq(a, b)
33 case M.Free{a} M.N{c2, a2, b2, q2, k2}:
34 False{}
35 case M.N{c, a, b, q, k} M.Free{f}:
36 False{}
37 case M.N{+c, +a, +b, +q, +k} M.N{+c2, +a2, +b2, +q2, +k2}:
38 Bool.and(beq(c, c2), Bool.and(Nat.is_eq(a, a2), Bool.and(Nat.is_eq(b, b2), Bool.and(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2))))))
39
40def beq_refl(+a: Bool) -> {beq(a, a) == True{} : Bool}:
41 match a:
42 case True{}:
43 {==}
44 case False{}:
45 {==}
46
47def beq_eq(+a: Bool, +b: Bool, +h: {beq(a, b) == True{} : Bool}) -> {a == b : Bool}:
48 match a b:
49 case True{} True{}:
50 {==}
51 case True{} False{}:
52 Empty.absurd({True{} == False{} : Bool}, L.false_true(h))
53 case False{} True{}:
54 Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
55 case False{} False{}:
56 {==}
57
58def iseq_eq(+c: Cmp, +h: {S.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
59 match c:
60 case LT{}:
61 Empty.absurd({LT{} == EQ{} : Cmp}, L.false_true(h))
62 case EQ{}:
63 {==}
64 case GT{}:
65 Empty.absurd({GT{} == EQ{} : Cmp}, L.false_true(h))
66
67def ndeq_refl(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +x: M.Node<K>) -> {ndeq(~K, ~cmp, x, x) == True{} : Bool}:
68 match x:
69 case M.Free{+a}:
70 N.is_eq_refl(a)
71 case M.N{+c, +a, +b, +q, +k}:
72 %Equal.sym(Bool, beq(c, c), True{}, beq_refl(c)) : {Bool.and(_, Bool.and(Nat.is_eq(a, a), Bool.and(Nat.is_eq(b, b), Bool.and(Nat.is_eq(q, q), S.is_eq(cmp(k, k)))))) == True{} : Bool}
73 %Equal.sym(Bool, Nat.is_eq(a, a), True{}, N.is_eq_refl(a)) : {Bool.and(True{}, Bool.and(_, Bool.and(Nat.is_eq(b, b), Bool.and(Nat.is_eq(q, q), S.is_eq(cmp(k, k)))))) == True{} : Bool}
74 %Equal.sym(Bool, Nat.is_eq(b, b), True{}, N.is_eq_refl(b)) : {Bool.and(True{}, Bool.and(True{}, Bool.and(_, Bool.and(Nat.is_eq(q, q), S.is_eq(cmp(k, k)))))) == True{} : Bool}
75 %Equal.sym(Bool, Nat.is_eq(q, q), True{}, N.is_eq_refl(q)) : {Bool.and(True{}, Bool.and(True{}, Bool.and(True{}, Bool.and(_, S.is_eq(cmp(k, k)))))) == True{} : Bool}
76 %Equal.sym(Cmp, cmp(k, k), EQ{}, O.refl(~K, ~cmp, ~o, k)) : {Bool.and(True{}, Bool.and(True{}, Bool.and(True{}, Bool.and(True{}, S.is_eq(_))))) == True{} : Bool}
77 {==}
78
79
80def ndeq_eq(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +x: M.Node<K>, +y: M.Node<K>, +h: {ndeq(~K, ~cmp, x, y) == True{} : Bool}) -> {x == y : M.Node<K>}:
81 match x y:
82 case M.Free{+a} M.Free{+b}:
83 %Equal.sym(Nat, a, b, N.eq_from_is_eq(a, b, h)) : {M.Free{_} == M.Free{b} : M.Node<K>}
84 {==}
85 case M.Free{a} M.N{c2, a2, b2, q2, k2}:
86 Empty.absurd({M.Free{a} == M.N{c2, a2, b2, q2, k2} : M.Node<K>}, L.false_true(h))
87 case M.N{c, a, b, q, k} M.Free{f}:
88 Empty.absurd({M.N{c, a, b, q, k} == M.Free{f} : M.Node<K>}, L.false_true(h))
89 case M.N{+c, +a, +b, +q, +k} M.N{+c2, +a2, +b2, +q2, +k2}:
90 +h2 = L.and_right(beq(c, c2), Bool.and(Nat.is_eq(a, a2), Bool.and(Nat.is_eq(b, b2), Bool.and(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2))))), h)
91 +h3 = L.and_right(Nat.is_eq(a, a2), Bool.and(Nat.is_eq(b, b2), Bool.and(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2)))), h2)
92 +h4 = L.and_right(Nat.is_eq(b, b2), Bool.and(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2))), h3)
93 +h5 = L.and_right(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2)), h4)
94 %Equal.sym(Bool, c, c2, beq_eq(c, c2, L.and_left(beq(c, c2), Bool.and(Nat.is_eq(a, a2), Bool.and(Nat.is_eq(b, b2), Bool.and(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2))))), h))) : {M.N{_, a, b, q, k} == M.N{c2, a2, b2, q2, k2} : M.Node<K>}
95 %Equal.sym(Nat, a, a2, N.eq_from_is_eq(a, a2, L.and_left(Nat.is_eq(a, a2), Bool.and(Nat.is_eq(b, b2), Bool.and(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2)))), h2))) : {M.N{c2, _, b, q, k} == M.N{c2, a2, b2, q2, k2} : M.Node<K>}
96 %Equal.sym(Nat, b, b2, N.eq_from_is_eq(b, b2, L.and_left(Nat.is_eq(b, b2), Bool.and(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2))), h3))) : {M.N{c2, a2, _, q, k} == M.N{c2, a2, b2, q2, k2} : M.Node<K>}
97 %Equal.sym(Nat, q, q2, N.eq_from_is_eq(q, q2, L.and_left(Nat.is_eq(q, q2), S.is_eq(cmp(k, k2)), h4))) : {M.N{c2, a2, b2, _, k} == M.N{c2, a2, b2, q2, k2} : M.Node<K>}
98 %Equal.sym(K, k, k2, O.antisym(~K, ~cmp, o, k, k2, iseq_eq(cmp(k, k2), h5))) : {M.N{c2, a2, b2, q2, _} == M.N{c2, a2, b2, q2, k2} : M.Node<K>}
99 {==}
100
101def ndeq_of_eq(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +x: M.Node<K>, +y: M.Node<K>, +e: {x == y : M.Node<K>}) -> {ndeq(~K, ~cmp, x, y) == True{} : Bool}:
102 L.subst(M.Node<K>, z => {ndeq(~K, ~cmp, x, z) == True{} : Bool}, x, y, e, ndeq_refl(~K, ~cmp, ~o, x))
103
104# ---- agreement on a list of ids ----
105
106def agr(~K: Data, ~cmp: K -> K -> Cmp, xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>) -> Bool:
107 match xs:
108 case Nil{}:
109 True{}
110 case Con{+j, t}:
111 Bool.and(ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, nl2, j)), agr(~K, ~cmp, t, nl, nl2))
112
113
114def agr_head(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +j: Nat, +t: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, Con{j, t}, nl, nl2) == True{} : Bool}) -> {ST.nd(K, nl, j) == ST.nd(K, nl2, j) : M.Node<K>}:
115 ndeq_eq(~K, ~cmp, ~o, ST.nd(K, nl, j), ST.nd(K, nl2, j), L.and_left(ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, nl2, j)), agr(~K, ~cmp, t, nl, nl2), h))
116
117def agr_refl(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>) -> {agr(~K, ~cmp, xs, nl, nl) == True{} : Bool}:
118 match xs:
119 case Nil{}:
120 {==}
121 case Con{+j, +t}:
122 L.and_intro(ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, nl, j)), agr(~K, ~cmp, t, nl, nl), ndeq_refl(~K, ~cmp, ~o, ST.nd(K, nl, j)), agr_refl(~K, ~cmp, ~o, t, nl))
123
124def agr_trans(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +a: List<&2, M.Node<K>>, +b: List<&2, M.Node<K>>, +c: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, xs, a, b) == True{} : Bool}, +h2: {agr(~K, ~cmp, xs, b, c) == True{} : Bool}) -> {agr(~K, ~cmp, xs, a, c) == True{} : Bool}:
125 match xs:
126 case Nil{}:
127 {==}
128 case Con{+j, +t}:
129 +e1 = ndeq_eq(~K, ~cmp, ~o, ST.nd(K, a, j), ST.nd(K, b, j), L.and_left(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, t, a, b), h))
130 +e2 = ndeq_eq(~K, ~cmp, ~o, ST.nd(K, b, j), ST.nd(K, c, j), L.and_left(ndeq(~K, ~cmp, ST.nd(K, b, j), ST.nd(K, c, j)), agr(~K, ~cmp, t, b, c), h2))
131 L.and_intro(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, c, j)), agr(~K, ~cmp, t, a, c), ndeq_of_eq(~K, ~cmp, ~o, ST.nd(K, a, j), ST.nd(K, c, j), Equal.trans(M.Node<K>, ST.nd(K, a, j), ST.nd(K, b, j), ST.nd(K, c, j), e1, e2)), agr_trans(~K, ~cmp, ~o, t, a, b, c, L.and_right(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, t, a, b), h), L.and_right(ndeq(~K, ~cmp, ST.nd(K, b, j), ST.nd(K, c, j)), agr(~K, ~cmp, t, b, c), h2)))
132
133def agr_sym(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +a: List<&2, M.Node<K>>, +b: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, xs, a, b) == True{} : Bool}) -> {agr(~K, ~cmp, xs, b, a) == True{} : Bool}:
134 match xs:
135 case Nil{}:
136 {==}
137 case Con{+j, +t}:
138 L.and_intro(ndeq(~K, ~cmp, ST.nd(K, b, j), ST.nd(K, a, j)), agr(~K, ~cmp, t, b, a), ndeq_of_eq(~K, ~cmp, ~o, ST.nd(K, b, j), ST.nd(K, a, j), Equal.sym(M.Node<K>, ST.nd(K, a, j), ST.nd(K, b, j), ndeq_eq(~K, ~cmp, ~o, ST.nd(K, a, j), ST.nd(K, b, j), L.and_left(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, t, a, b), h)))), agr_sym(~K, ~cmp, ~o, t, a, b, L.and_right(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, t, a, b), h)))
139
140def agr_l(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +ys: List<&2, Nat>, +a: List<&2, M.Node<K>>, +b: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, SC.append(Nat, xs, ys), a, b) == True{} : Bool}) -> {agr(~K, ~cmp, xs, a, b) == True{} : Bool}:
141 match xs:
142 case Nil{}:
143 {==}
144 case Con{+j, +t}:
145 L.and_intro(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, t, a, b), L.and_left(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, SC.append(Nat, t, ys), a, b), h), agr_l(~K, ~cmp, ~o, t, ys, a, b, L.and_right(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, SC.append(Nat, t, ys), a, b), h)))
146
147def agr_r(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +ys: List<&2, Nat>, +a: List<&2, M.Node<K>>, +b: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, SC.append(Nat, xs, ys), a, b) == True{} : Bool}) -> {agr(~K, ~cmp, ys, a, b) == True{} : Bool}:
148 match xs:
149 case Nil{}:
150 h
151 case Con{+j, +t}:
152 agr_r(~K, ~cmp, ~o, t, ys, a, b, L.and_right(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, SC.append(Nat, t, ys), a, b), h))
153
154def agr_app(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +ys: List<&2, Nat>, +a: List<&2, M.Node<K>>, +b: List<&2, M.Node<K>>, +hx: {agr(~K, ~cmp, xs, a, b) == True{} : Bool}, +hy: {agr(~K, ~cmp, ys, a, b) == True{} : Bool}) -> {agr(~K, ~cmp, SC.append(Nat, xs, ys), a, b) == True{} : Bool}:
155 match xs:
156 case Nil{}:
157 hy
158 case Con{+j, +t}:
159 L.and_intro(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, SC.append(Nat, t, ys), a, b), L.and_left(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, t, a, b), hx), agr_app(~K, ~cmp, ~o, t, ys, a, b, L.and_right(ndeq(~K, ~cmp, ST.nd(K, a, j), ST.nd(K, b, j)), agr(~K, ~cmp, t, a, b), hx), hy))
160
161# a write agrees off its id
162def agr_wr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {agr(~K, ~cmp, xs, nl, PR.wr_nl(K, nl, id, x)) == True{} : Bool}:
163 match xs:
164 case Nil{}:
165 {==}
166 case Con{+j, +t}:
167 L.and_intro(ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, PR.wr_nl(K, nl, id, x), j)), agr(~K, ~cmp, t, nl, PR.wr_nl(K, nl, id, x)), ndeq_of_eq(~K, ~cmp, ~o, ST.nd(K, nl, j), ST.nd(K, PR.wr_nl(K, nl, id, x), j), Equal.sym(M.Node<K>, ST.nd(K, PR.wr_nl(K, nl, id, x), j), ST.nd(K, nl, j), FR.nd_wr_other(K, nl, id, x, j, FR.ne_sym(j, id, FR.or_f_l(Nat.is_eq(j, id), NL.memn(id, t), hn))))), agr_wr(~K, ~cmp, ~o, t, nl, id, x, FR.or_f_r(Nat.is_eq(j, id), NL.memn(id, t), hn)))
168
169# ---- what agreement keeps ----
170
171
172def rep_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +t: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, ST.ids(t), nl, nl2) == True{} : Bool}) -> {ST.rep(~K, t, p, nl2) == ST.rep(~K, t, p, nl) : Bool}:
173 match t:
174 case ST.TE{}:
175 {==}
176 case ST.TN{+i, +l, +r}:
177 +hr = agr_r(~K, ~cmp, ~o, ST.ids(l), Con{i, ST.ids(r)}, nl, nl2, h)
178 %Equal.sym(M.Node<K>, ST.nd(K, nl2, i), ST.nd(K, nl, i), Equal.sym(M.Node<K>, ST.nd(K, nl, i), ST.nd(K, nl2, i), agr_head(~K, ~cmp, ~o, i, ST.ids(r), nl, nl2, hr))) : {Bool.and(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, _, ST.rid(l), ST.rid(r), p), Bool.and(ST.rep(~K, l, i, nl2), ST.rep(~K, r, i, nl2)))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}
179 %Equal.sym(Bool, ST.rep(~K, l, i, nl2), ST.rep(~K, l, i, nl), rep_agr(~K, ~cmp, ~o, l, i, nl, nl2, agr_l(~K, ~cmp, ~o, ST.ids(l), Con{i, ST.ids(r)}, nl, nl2, h))) : {Bool.and(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), Bool.and(_, ST.rep(~K, r, i, nl2)))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}
180 %Equal.sym(Bool, ST.rep(~K, r, i, nl2), ST.rep(~K, r, i, nl), rep_agr(~K, ~cmp, ~o, r, i, nl, nl2, L.and_right(ndeq(~K, ~cmp, ST.nd(K, nl, i), ST.nd(K, nl2, i)), agr(~K, ~cmp, ST.ids(r), nl, nl2), hr))) : {Bool.and(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), Bool.and(ST.rep(~K, l, i, nl), _))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}
181 {==}
182
183
184def ctx_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: List<&2, P.Fr>, +x: Nat, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, SC.append(Nat, P.before(c), P.after(c)), nl, nl2) == True{} : Bool}) -> {P.ctxok(~K, c, x, nl2) == P.ctxok(~K, c, x, nl) : Bool}:
185 match c:
186 case Nil{}:
187 {==}
188 case Con{P.FR{+p, +lft, +s}, +t}:
189 match lft:
190 case True{}:
191 +h1 = agr_r(~K, ~cmp, ~o, P.before(t), Con{p, SC.append(Nat, ST.ids(s), P.after(t))}, nl, nl2, h)
192 +hbt = agr_l(~K, ~cmp, ~o, P.before(t), Con{p, SC.append(Nat, ST.ids(s), P.after(t))}, nl, nl2, h)
193 +h2 = L.and_right(ndeq(~K, ~cmp, ST.nd(K, nl, p), ST.nd(K, nl2, p)), agr(~K, ~cmp, SC.append(Nat, ST.ids(s), P.after(t)), nl, nl2), h1)
194 +hs = agr_l(~K, ~cmp, ~o, ST.ids(s), P.after(t), nl, nl2, h2)
195 +hat = agr_r(~K, ~cmp, ~o, ST.ids(s), P.after(t), nl, nl2, h2)
196 %Equal.sym(M.Node<K>, ST.nd(K, nl2, p), ST.nd(K, nl, p), Equal.sym(M.Node<K>, ST.nd(K, nl, p), ST.nd(K, nl2, p), agr_head(~K, ~cmp, ~o, p, SC.append(Nat, ST.ids(s), P.after(t)), nl, nl2, h1))) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, _, x, ST.rid(s), P.top(t)), ST.rep(~K, s, p, nl2))), P.ctxok(~K, t, p, nl2)) == P.ctxok(~K, Con{P.FR{p, True{}, s}, t}, x, nl) : Bool}
197 %Equal.sym(Bool, ST.rep(~K, s, p, nl2), ST.rep(~K, s, p, nl), rep_agr(~K, ~cmp, ~o, s, p, nl, nl2, hs)) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), x, ST.rid(s), P.top(t)), _)), P.ctxok(~K, t, p, nl2)) == P.ctxok(~K, Con{P.FR{p, True{}, s}, t}, x, nl) : Bool}
198 %Equal.sym(Bool, P.ctxok(~K, t, p, nl2), P.ctxok(~K, t, p, nl), ctx_agr(~K, ~cmp, ~o, t, p, nl, nl2, agr_app(~K, ~cmp, ~o, P.before(t), P.after(t), nl, nl2, hbt, hat))) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), x, ST.rid(s), P.top(t)), ST.rep(~K, s, p, nl))), _) == P.ctxok(~K, Con{P.FR{p, True{}, s}, t}, x, nl) : Bool}
199 {==}
200 case False{}:
201 +h1 = agr_l(~K, ~cmp, ~o, SC.append(Nat, P.before(t), SC.append(Nat, ST.ids(s), Con{p, Nil{}})), P.after(t), nl, nl2, h)
202 +hat = agr_r(~K, ~cmp, ~o, SC.append(Nat, P.before(t), SC.append(Nat, ST.ids(s), Con{p, Nil{}})), P.after(t), nl, nl2, h)
203 +hbt = agr_l(~K, ~cmp, ~o, P.before(t), SC.append(Nat, ST.ids(s), Con{p, Nil{}}), nl, nl2, h1)
204 +h2 = agr_r(~K, ~cmp, ~o, P.before(t), SC.append(Nat, ST.ids(s), Con{p, Nil{}}), nl, nl2, h1)
205 +hs = agr_l(~K, ~cmp, ~o, ST.ids(s), Con{p, Nil{}}, nl, nl2, h2)
206 +hp = agr_r(~K, ~cmp, ~o, ST.ids(s), Con{p, Nil{}}, nl, nl2, h2)
207 %Equal.sym(M.Node<K>, ST.nd(K, nl2, p), ST.nd(K, nl, p), Equal.sym(M.Node<K>, ST.nd(K, nl, p), ST.nd(K, nl2, p), agr_head(~K, ~cmp, ~o, p, Nil{}, nl, nl2, hp))) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, _, ST.rid(s), x, P.top(t)), ST.rep(~K, s, p, nl2))), P.ctxok(~K, t, p, nl2)) == P.ctxok(~K, Con{P.FR{p, False{}, s}, t}, x, nl) : Bool}
208 %Equal.sym(Bool, ST.rep(~K, s, p, nl2), ST.rep(~K, s, p, nl), rep_agr(~K, ~cmp, ~o, s, p, nl, nl2, hs)) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), x, P.top(t)), _)), P.ctxok(~K, t, p, nl2)) == P.ctxok(~K, Con{P.FR{p, False{}, s}, t}, x, nl) : Bool}
209 %Equal.sym(Bool, P.ctxok(~K, t, p, nl2), P.ctxok(~K, t, p, nl), ctx_agr(~K, ~cmp, ~o, t, p, nl, nl2, agr_app(~K, ~cmp, ~o, P.before(t), P.after(t), nl, nl2, hbt, hat))) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.rid(s), x, P.top(t)), ST.rep(~K, s, p, nl))), _) == P.ctxok(~K, Con{P.FR{p, False{}, s}, t}, x, nl) : Bool}
210 {==}
211
212
213def ents_agr(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +h: {agr(~K, ~cmp, xs, nl, nl2) == True{} : Bool}) -> {ST.ents(~K, ~V, xs, nl2, pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
214 match xs:
215 case Nil{}:
216 {==}
217 case Con{+j, +t}:
218 %Equal.sym(M.Node<K>, ST.nd(K, nl2, j), ST.nd(K, nl, j), Equal.sym(M.Node<K>, ST.nd(K, nl, j), ST.nd(K, nl2, j), agr_head(~K, ~cmp, ~o, j, t, nl, nl2, h))) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, _, ST.pv(V, pl, j)), ST.ents(~K, ~V, t, nl2, pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
219 %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, nl2, pl), ST.ents(~K, ~V, t, nl, pl), ents_agr(~K, ~V, ~cmp, ~o, t, nl, nl2, pl, L.and_right(ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, nl2, j)), agr(~K, ~cmp, t, nl, nl2), h))) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
220 {==}
221
222def oks_agr(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +h: {agr(~K, ~cmp, xs, nl, nl2) == True{} : Bool}) -> {EN.oks(~K, ~V, xs, nl2, pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
223 match xs:
224 case Nil{}:
225 {==}
226 case Con{+j, +t}:
227 %Equal.sym(M.Node<K>, ST.nd(K, nl2, j), ST.nd(K, nl, j), Equal.sym(M.Node<K>, ST.nd(K, nl, j), ST.nd(K, nl2, j), agr_head(~K, ~cmp, ~o, j, t, nl, nl2, h))) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, _, ST.pv(V, pl, j))), EN.oks(~K, ~V, t, nl2, pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
228 %Equal.sym(Bool, EN.oks(~K, ~V, t, nl2, pl), EN.oks(~K, ~V, t, nl, pl), oks_agr(~K, ~V, ~cmp, ~o, t, nl, nl2, pl, L.and_right(ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, nl2, j)), agr(~K, ~cmp, t, nl, nl2), h))) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
229 {==}
230
231def fll_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>, +h: {agr(~K, ~cmp, fl, nl, nl2) == True{} : Bool}) -> {ST.fll(~K, nl2, fl) == ST.fll(~K, nl, fl) : Bool}:
232 match fl:
233 case Nil{}:
234 {==}
235 case Con{+f, +t}:
236 %Equal.sym(M.Node<K>, ST.nd(K, nl2, f), ST.nd(K, nl, f), Equal.sym(M.Node<K>, ST.nd(K, nl, f), ST.nd(K, nl2, f), agr_head(~K, ~cmp, ~o, f, t, nl, nl2, h))) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, nl2, t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
237 %Equal.sym(Bool, ST.fll(~K, nl2, t), ST.fll(~K, nl, t), fll_agr(~K, ~cmp, ~o, t, nl, nl2, L.and_right(ndeq(~K, ~cmp, ST.nd(K, nl, f), ST.nd(K, nl2, f)), agr(~K, ~cmp, t, nl, nl2), h))) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}
238 {==}