1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/order.bend as O
5	import ../../../spec/lib/common.bend as SC
6	import ../../../spec/containers/balanced_search_tree/main.bend as S
7	import ../../../src/containers/balanced_search_tree.bend as M
8	import ./state.bend as ST
9	import ./prim.bend as PR
10	import ./path.bend as P
11	import ./ends.bend as EN
12	import ./frame.bend as FR
13	import ../../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	
22	def beq(+a: Bool, +b: Bool) -> Bool:
23	  match a:
24	    case True{}:
25	      b
26	    case False{}:
27	      Bool.not(b)
28	
29	def 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	
40	def beq_refl(+a: Bool) -> {beq(a, a) == True{} : Bool}:
41	  match a:
42	    case True{}:
43	      {==}
44	    case False{}:
45	      {==}
46	
47	def 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	
58	def 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	
67	def 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	
80	def 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	
101	def 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	
106	def 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	
114	def 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	
117	def 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	
124	def 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	
133	def 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	
140	def 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	
147	def 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	
154	def 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
162	def 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	
172	def 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	
184	def 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	
213	def 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	
222	def 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	
231	def 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	      {==}