proofs/containers/doubly_linked_list/rel.bend
bend-collections-laws-containers@1.0.0.0 · 432 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/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as A
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/links.bend as LK
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LKx
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
16
17# Relinking: the writes of an insertion between two neighbours and of an
18# unlink, over the prev and next lists.
19
20
21# ---- writes at the first id of b / the last id of a ----
22
23# the first id of b is in xs
24def fstin(b: List<&2, Nat>, xs: List<&2, Nat>) -> Bool:
25 match b:
26 case Nil{}:
27 False{}
28 case Con{+b0, t}:
29 NL.memn(b0, xs)
30
31# the last id of a is in xs
32def lastin(a: List<&2, Nat>, xs: List<&2, Nat>) -> Bool:
33 match a:
34 case Nil{}:
35 False{}
36 case Con{+a0, +t}:
37 NL.memn(NL.lastn(t, a0), xs)
38
39def upd_first(+pl: List<&2, U32>, b: List<&2, Nat>, +v: U32) -> List<&2, U32>:
40 match b:
41 case Nil{}:
42 pl
43 case Con{+b0, t}:
44 SC.update(U32, pl, b0, v)
45
46def upd_last(+nl: List<&2, U32>, a: List<&2, Nat>, +v: U32) -> List<&2, U32>:
47 match a:
48 case Nil{}:
49 nl
50 case Con{+a0, +t}:
51 SC.update(U32, nl, NL.lastn(t, a0), v)
52
53def tu_first(+d: Nat, +tr: AR.Tree<U32>, b: List<&2, Nat>, +v: U32) -> AR.Tree<U32>:
54 match b:
55 case Nil{}:
56 tr
57 case Con{+b0, t}:
58 AR.upd(U32, d, tr, b0, v)
59
60def tu_last(+d: Nat, +tr: AR.Tree<U32>, a: List<&2, Nat>, +v: U32) -> AR.Tree<U32>:
61 match a:
62 case Nil{}:
63 tr
64 case Con{+a0, +t}:
65 AR.upd(U32, d, tr, NL.lastn(t, a0), v)
66
67# ---- bounds ----
68
69def hd1(+d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}) -> {Nat.is_lt(1n+d, 32n) == True{} : Bool}:
70 N.lt_trans(d, 30n, 31n, hd, {==})
71
72def hd0(+d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}) -> {Nat.is_lt(d, 32n) == True{} : Bool}:
73 N.lt_trans(d, 30n, 32n, hd, {==})
74
75def self_in(+b: Nat, +t: List<&2, Nat>) -> {NL.memn(b, Con{b, t}) == True{} : Bool}:
76 NL.or_tl(Nat.is_eq(b, b), NL.memn(b, t), N.is_eq_refl(b))
77
78
79def slok_c(~T: Data, +x: Nat, +y: Nat, +t: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hy: {Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hm2: {NL.memn(x, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}:
80 match c:
81 case True{}:
82 L.subst(Nat, z => {Bool.and(Nat.is_lt(z, fr), ST.live(T, vl, z)) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy)
83 case False{}:
84 rec(hm)
85
86# a member of a slok list is below fr and live
87def slok_mem(~T: Data, +x: Nat, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}:
88 match xs:
89 case Nil{}:
90 Empty.absurd({Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)) == True{} : Bool}, L.false_true(hm))
91 case Con{+y, +t}:
92 +hy = L.and_left(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h)
93 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h)
94 slok_c(~T, x, y, t, fr, vl, hy, Nat.is_eq(y, x), {==}, hm, hm2 => slok_mem(~T, x, t, fr, vl, ht, hm2))
95
96def flok_c(~T: Data, +x: Nat, +y: Nat, +t: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hy: {Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hm2: {NL.memn(x, t) == True{} : Bool} -> {Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}:
97 match c:
98 case True{}:
99 L.subst(Nat, z => {Bool.and(Nat.is_lt(z, fr), Bool.not(ST.live(T, vl, z))) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy)
100 case False{}:
101 rec(hm)
102
103# a member of a flok list is below fr and vacant
104def flok_mem(~T: Data, +x: Nat, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +h: {ST.flok(~T, xs, fr, vl) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}:
105 match xs:
106 case Nil{}:
107 Empty.absurd({Bool.and(Nat.is_lt(x, fr), Bool.not(ST.live(T, vl, x))) == True{} : Bool}, L.false_true(hm))
108 case Con{+y, +t}:
109 +hy = L.and_left(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h)
110 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h)
111 flok_c(~T, x, y, t, fr, vl, hy, Nat.is_eq(y, x), {==}, hm, hm2 => flok_mem(~T, x, t, fr, vl, ht, hm2))
112
113def slok_app(~T: Data, +a: List<&2, Nat>, +b: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>) -> {ST.slok(~T, SC.append(Nat, a, b), fr, vl) == Bool.and(ST.slok(~T, a, fr, vl), ST.slok(~T, b, fr, vl)) : Bool}:
114 match a:
115 case Nil{}:
116 {==}
117 case Con{+x, +t}:
118 +ih = slok_app(~T, t, b, fr, vl)
119 Equal.trans(Bool, Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, SC.append(Nat, t, b), fr, vl)), Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), Bool.and(ST.slok(~T, t, fr, vl), ST.slok(~T, b, fr, vl))), Bool.and(Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl)), ST.slok(~T, b, fr, vl)), Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), z), ST.slok(~T, SC.append(Nat, t, b), fr, vl), Bool.and(ST.slok(~T, t, fr, vl), ST.slok(~T, b, fr, vl)), ih), NL.and_assoc(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), ST.slok(~T, b, fr, vl)))
120
121# a live id is not on a vacant list
122def dj_c(~T: Data, +x: Nat, +y: Nat, +t: List<&2, Nat>, +vl: List<&2, Maybe<&2, T>>, +hx: {ST.live(T, vl, x) == True{} : Bool}, +hy: {Bool.not(ST.live(T, vl, y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +ih: {NL.memn(x, t) == False{} : Bool}) -> {Bool.or(c, NL.memn(x, t)) == False{} : Bool}:
123 match c:
124 case True{}:
125 +hy2 = L.subst(Nat, z => {Bool.not(ST.live(T, vl, z)) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy)
126 Empty.absurd({Bool.or(True{}, NL.memn(x, t)) == False{} : Bool}, L.true_not_false(ST.live(T, vl, x), hx, L.not_true(ST.live(T, vl, x), hy2)))
127 case False{}:
128 ih
129
130def live_nf(~T: Data, +x: Nat, +ys: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {ST.live(T, vl, x) == True{} : Bool}, +h: {ST.flok(~T, ys, fr, vl) == True{} : Bool}) -> {NL.memn(x, ys) == False{} : Bool}:
131 match ys:
132 case Nil{}:
133 {==}
134 case Con{+y, +t}:
135 +hy = L.and_right(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y)), L.and_left(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h))
136 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h)
137 dj_c(~T, x, y, t, vl, hx, hy, Nat.is_eq(y, x), {==}, live_nf(~T, x, t, fr, vl, hx, ht))
138
139# an id at or above fr is on no slok list
140def hi_c(+x: Nat, +y: Nat, +fr: Nat, +hy: {Nat.is_lt(y, fr) == True{} : Bool}, +hx: {Nat.is_le(fr, x) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +m: Bool, +ih: {m == False{} : Bool}) -> {Bool.or(c, m) == False{} : Bool}:
141 match c:
142 case True{}:
143 +hy2 = L.subst(Nat, z => {Nat.is_lt(z, fr) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy)
144 Empty.absurd({Bool.or(True{}, m) == False{} : Bool}, N.lt_ne(x, x, N.lt_le_trans(x, fr, x, hy2, hx), {==}))
145 case False{}:
146 ih
147
148def hi_ns(~T: Data, +x: Nat, +ys: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {Nat.is_le(fr, x) == True{} : Bool}, +h: {ST.slok(~T, ys, fr, vl) == True{} : Bool}) -> {NL.memn(x, ys) == False{} : Bool}:
149 match ys:
150 case Nil{}:
151 {==}
152 case Con{+y, +t}:
153 +hy = L.and_left(Nat.is_lt(y, fr), ST.live(T, vl, y), L.and_left(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h))
154 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), ST.live(T, vl, y)), ST.slok(~T, t, fr, vl), h)
155 hi_c(x, y, fr, hy, hx, Nat.is_eq(y, x), {==}, NL.memn(x, t), hi_ns(~T, x, t, fr, vl, hx, ht))
156
157def hi_nf(~T: Data, +x: Nat, +ys: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +hx: {Nat.is_le(fr, x) == True{} : Bool}, +h: {ST.flok(~T, ys, fr, vl) == True{} : Bool}) -> {NL.memn(x, ys) == False{} : Bool}:
158 match ys:
159 case Nil{}:
160 {==}
161 case Con{+y, +t}:
162 +hy = L.and_left(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y)), L.and_left(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h))
163 +ht = L.and_right(Bool.and(Nat.is_lt(y, fr), Bool.not(ST.live(T, vl, y))), ST.flok(~T, t, fr, vl), h)
164 hi_c(x, y, fr, hy, hx, Nat.is_eq(y, x), {==}, NL.memn(x, t), hi_nf(~T, x, t, fr, vl, hx, ht))
165
166# ---- first/last bounds ----
167
168def fstlt(b: List<&2, Nat>, +m: Nat) -> Bool:
169 match b:
170 case Nil{}:
171 True{}
172 case Con{+b0, t}:
173 Nat.is_lt(b0, m)
174
175def lastlt(a: List<&2, Nat>, +m: Nat) -> Bool:
176 match a:
177 case Nil{}:
178 True{}
179 case Con{+a0, +t}:
180 Nat.is_lt(NL.lastn(t, a0), m)
181
182def fstlt_of(~T: Data, +b: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +m: Nat, +hfr: {Nat.is_le(fr, m) == True{} : Bool}, +h: {ST.slok(~T, b, fr, vl) == True{} : Bool}) -> {fstlt(b, m) == True{} : Bool}:
183 match b:
184 case Nil{}:
185 {==}
186 case Con{+b0, +t}:
187 N.lt_le_trans(b0, fr, m, L.and_left(Nat.is_lt(b0, fr), ST.live(T, vl, b0), slok_mem(~T, b0, Con{b0, t}, fr, vl, h, self_in(b0, t))), hfr)
188
189def lastlt_of(~T: Data, +a: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +m: Nat, +hfr: {Nat.is_le(fr, m) == True{} : Bool}, +h: {ST.slok(~T, a, fr, vl) == True{} : Bool}) -> {lastlt(a, m) == True{} : Bool}:
190 match a:
191 case Nil{}:
192 {==}
193 case Con{+a0, +t}:
194 N.lt_le_trans(NL.lastn(t, a0), fr, m, L.and_left(Nat.is_lt(NL.lastn(t, a0), fr), ST.live(T, vl, NL.lastn(t, a0)), slok_mem(~T, NL.lastn(t, a0), Con{a0, t}, fr, vl, h, NL.lastn_mem(t, a0))), hfr)
195
196# ---- links of ids below 2^d ----
197
198def lnk_nz(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(d)) == True{} : Bool}) -> {U32.is_eq(LKx.lnk(b), 0) == False{} : Bool}:
199 +hk = N.lt_le(d, 32n, hd0(d, hd))
200 +e1 = U.to_nat_from_nat(b, d, hk, hb)
201 +hb2 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, b, UD.v(U32.from_nat(b)), Equal.sym(Nat, UD.v(U32.from_nat(b)), b, e1), hb)
202 W32.link_nz(one, h1, U32.from_nat(b), W32.bound32(one, h1, UD.v(U32.from_nat(b)), d, hd1(d, hd), hb2))
203
204def slot_lnk(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(d)) == True{} : Bool}) -> {UD.v(R.slot(LKx.lnk(b))) == b : Nat}:
205 LKx.slot_lnk(one, h1, b, d, hd1(d, hd), hb)
206
207
208# the write at the id of a link
209def sn_c(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +tr: AR.Tree<U32>, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b0: Nat, +hb: {Nat.is_lt(b0, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {R.set_next(AR.thaw(U32, tr), LKx.lnk(b0), v) == AR.thaw(U32, AR.upd(U32, d, tr, b0, v)) : Array<U32>}:
210 +i = R.slot(LKx.lnk(b0))
211 +es = slot_lnk(one, h1, b0, d, hd, hb)
212 +hi = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(d)) == True{} : Bool}, b0, UD.v(i), Equal.sym(Nat, UD.v(i), b0, es), hb)
213 +e1 = Equal.cong(Bool, Array<U32>, z => R.set_next_go(AR.thaw(U32, tr), LKx.lnk(b0), v, z), U32.is_eq(LKx.lnk(b0), 0), False{}, lnk_nz(one, h1, b0, d, hd, hb))
214 +e2 = UT.uset_a(d, hd0(d, hd), tr, pf, i, hi, v)
215 +e3 = Equal.cong(Nat, Array<U32>, z => AR.thaw(U32, AR.upd(U32, d, tr, z, v)), UD.v(i), b0, es)
216 Equal.trans(Array<U32>, R.set_next(AR.thaw(U32, tr), LKx.lnk(b0), v), Array.set(U32, AR.thaw(U32, tr), i, v), AR.thaw(U32, AR.upd(U32, d, tr, b0, v)), e1, Equal.trans(Array<U32>, Array.set(U32, AR.thaw(U32, tr), i, v), AR.thaw(U32, AR.upd(U32, d, tr, UD.v(i), v)), AR.thaw(U32, AR.upd(U32, d, tr, b0, v)), e2, e3))
217
218# set_next at b's first link
219def sn_first(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +tr: AR.Tree<U32>, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b: List<&2, Nat>, +hb: {fstlt(b, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {R.set_next(AR.thaw(U32, tr), LKx.fst_or(b, 0), v) == AR.thaw(U32, tu_first(d, tr, b, v)) : Array<U32>}:
220 match b:
221 case Nil{}:
222 {==}
223 case Con{+b0, +t}:
224 sn_c(one, h1, d, hd, tr, pf, b0, hb, v)
225
226# set_next at a's last link
227def sn_last(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 30n) == True{} : Bool}, +tr: AR.Tree<U32>, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +a: List<&2, Nat>, +ha: {lastlt(a, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {R.set_next(AR.thaw(U32, tr), LKx.last_or(a, 0), v) == AR.thaw(U32, tu_last(d, tr, a, v)) : Array<U32>}:
228 match a:
229 case Nil{}:
230 {==}
231 case Con{+a0, +t}:
232 +e0 = Equal.cong(U32, Array<U32>, w => R.set_next(AR.thaw(U32, tr), w, v), LKx.last_or(t, LKx.lnk(a0)), LKx.lnk(NL.lastn(t, a0)), LKx.last_lnk(t, a0))
233 Equal.trans(Array<U32>, R.set_next(AR.thaw(U32, tr), LKx.last_or(t, LKx.lnk(a0)), v), R.set_next(AR.thaw(U32, tr), LKx.lnk(NL.lastn(t, a0)), v), AR.thaw(U32, AR.upd(U32, d, tr, NL.lastn(t, a0), v)), e0, sn_c(one, h1, d, hd, tr, pf, NL.lastn(t, a0), ha, v))
234
235def tf_p(+d: Nat, +tr: AR.Tree<U32>, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b: List<&2, Nat>, +v: U32) -> {AR.perfect(U32, d, tu_first(d, tr, b, v)) == True{} : Bool}:
236 match b:
237 case Nil{}:
238 pf
239 case Con{+b0, +t}:
240 UT.uset_p(d, tr, pf, b0, v)
241
242def tl_p(+d: Nat, +tr: AR.Tree<U32>, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +a: List<&2, Nat>, +v: U32) -> {AR.perfect(U32, d, tu_last(d, tr, a, v)) == True{} : Bool}:
243 match a:
244 case Nil{}:
245 pf
246 case Con{+a0, +t}:
247 UT.uset_p(d, tr, pf, NL.lastn(t, a0), v)
248
249def tf_s(+d: Nat, +tr: AR.Tree<U32>, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +b: List<&2, Nat>, +hb: {fstlt(b, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {AR.slots(U32, tu_first(d, tr, b, v)) == upd_first(AR.slots(U32, tr), b, v) : List<&2, U32>}:
250 match b:
251 case Nil{}:
252 {==}
253 case Con{+b0, +t}:
254 UT.uset_s(d, tr, pf, b0, hb, v)
255
256def tl_s(+d: Nat, +tr: AR.Tree<U32>, +pf: {AR.perfect(U32, d, tr) == True{} : Bool}, +a: List<&2, Nat>, +ha: {lastlt(a, SC.pow2(d)) == True{} : Bool}, +v: U32) -> {AR.slots(U32, tu_last(d, tr, a, v)) == upd_last(AR.slots(U32, tr), a, v) : List<&2, U32>}:
257 match a:
258 case Nil{}:
259 {==}
260 case Con{+a0, +t}:
261 UT.uset_s(d, tr, pf, NL.lastn(t, a0), ha, v)
262
263# ---- frames ----
264
265def seg_ffp(+pl: List<&2, U32>, +nl: List<&2, U32>, +b: List<&2, Nat>, +v: U32, +xs: List<&2, Nat>, +p: U32, +q: U32, +h: {fstin(b, xs) == False{} : Bool}) -> {ST.seg(upd_first(pl, b, v), nl, xs, p, q) == ST.seg(pl, nl, xs, p, q) : Bool}:
266 match b:
267 case Nil{}:
268 {==}
269 case Con{+b0, +t}:
270 LK.seg_fp(pl, nl, b0, v, xs, p, q, h)
271
272def seg_lfn(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +v: U32, +xs: List<&2, Nat>, +p: U32, +q: U32, +h: {lastin(a, xs) == False{} : Bool}) -> {ST.seg(pl, upd_last(nl, a, v), xs, p, q) == ST.seg(pl, nl, xs, p, q) : Bool}:
273 match a:
274 case Nil{}:
275 {==}
276 case Con{+a0, +t}:
277 LK.seg_fn(pl, nl, NL.lastn(t, a0), v, xs, p, q, h)
278
279def fll_lfn(+nl: List<&2, U32>, +a: List<&2, Nat>, +v: U32, +fl: List<&2, Nat>, +h: {lastin(a, fl) == False{} : Bool}) -> {ST.fll(upd_last(nl, a, v), fl) == ST.fll(nl, fl) : Bool}:
280 match a:
281 case Nil{}:
282 {==}
283 case Con{+a0, +t}:
284 LK.fll_fn(nl, NL.lastn(t, a0), v, fl, h)
285
286def ne1(+n: Nat, +x: Nat, +h: {NL.memn(x, Con{n, Nil{}}) == False{} : Bool}) -> {Nat.is_eq(x, n) == False{} : Bool}:
287 NL.ne_sym(n, x, NL.or_ff_l(Nat.is_eq(n, x), False{}, h))
288
289def nth_uf(+pl: List<&2, U32>, +b: List<&2, Nat>, +v: U32, +n: Nat, +h: {fstin(b, Con{n, Nil{}}) == False{} : Bool}) -> {W32.nth0(upd_first(pl, b, v), n) == W32.nth0(pl, n) : U32}:
290 match b:
291 case Nil{}:
292 {==}
293 case Con{+b0, +t}:
294 W32.nth0_upd_other(pl, b0, n, v, ne1(n, b0, h))
295
296def nth_ul(+nl: List<&2, U32>, +a: List<&2, Nat>, +v: U32, +n: Nat, +h: {lastin(a, Con{n, Nil{}}) == False{} : Bool}) -> {W32.nth0(upd_last(nl, a, v), n) == W32.nth0(nl, n) : U32}:
297 match a:
298 case Nil{}:
299 {==}
300 case Con{+a0, +t}:
301 W32.nth0_upd_other(nl, NL.lastn(t, a0), n, v, ne1(n, NL.lastn(t, a0), h))
302
303# ---- re-targeting ----
304
305def seg_ufp(+pl: List<&2, U32>, +nl: List<&2, U32>, +b: List<&2, Nat>, +x: U32, +q: U32, +y: U32, +hs: {ST.seg(pl, nl, b, x, q) == True{} : Bool}, +hn: {NL.nodupn(b) == True{} : Bool}, +hl: {fstlt(b, SC.length(U32, pl)) == True{} : Bool}) -> {ST.seg(upd_first(pl, b, y), nl, b, y, q) == True{} : Bool}:
306 match b:
307 case Nil{}:
308 {==}
309 case Con{+b0, +t}:
310 LK.segp(pl, nl, b0, t, x, q, y, hs, hn, hl)
311
312def seg_ulq(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +p: U32, +x: U32, +y: U32, +hs: {ST.seg(pl, nl, a, p, x) == True{} : Bool}, +hn: {NL.nodupn(a) == True{} : Bool}, +hl: {lastlt(a, SC.length(U32, nl)) == True{} : Bool}) -> {ST.seg(pl, upd_last(nl, a, y), a, p, y) == True{} : Bool}:
313 match a:
314 case Nil{}:
315 {==}
316 case Con{+a0, +t}:
317 LK.segq(pl, nl, t, a0, p, x, y, hs, hn, hl)
318
319# ---- rewriting a truth ----
320
321# b1 is true when b1 == b2 and b2 is
322def by_eq(+b1: Bool, +b2: Bool, +e: {b1 == b2 : Bool}, +h: {b2 == True{} : Bool}) -> {b1 == True{} : Bool}:
323 L.subst(Bool, z => {z == True{} : Bool}, b2, b1, Equal.sym(Bool, b1, b2, e), h)
324
325# b2 is true when b1 == b2 and b1 is
326def to_eq(+b1: Bool, +b2: Bool, +e: {b1 == b2 : Bool}, +h: {b1 == True{} : Bool}) -> {b2 == True{} : Bool}:
327 L.subst(Bool, z => {z == True{} : Bool}, b1, b2, e, h)
328
329def u_is(+x: U32, +y: U32, +e: {x == y : U32}) -> {U32.is_eq(x, y) == True{} : Bool}:
330 L.subst(U32, z => {U32.is_eq(z, y) == True{} : Bool}, y, x, Equal.sym(U32, x, y, e), LKx.u_refl(y))
331
332# ---- disjointness of the parts of a list without repeats ----
333
334# a ++ s :: b: b's first id is not in a
335def fin_dj(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}) -> {fstin(b, a) == False{} : Bool}:
336 match b:
337 case Nil{}:
338 {==}
339 case Con{+b0, +t}:
340 NL.nd_dj(a, Con{s, Con{b0, t}}, hn, b0, NL.or_tr(Nat.is_eq(s, b0), NL.memn(b0, Con{b0, t}), self_in(b0, t)))
341
342# a ++ s :: b: a's last id is not in b
343def lin_dj(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}) -> {lastin(a, b) == False{} : Bool}:
344 match a:
345 case Nil{}:
346 {==}
347 case Con{+a0, +t}:
348 NL.or_ff_r(Nat.is_eq(s, NL.lastn(t, a0)), NL.memn(NL.lastn(t, a0), b), NL.nd_dj2(Con{a0, t}, Con{s, b}, hn, NL.lastn(t, a0), NL.lastn_mem(t, a0)))
349
350# a ++ b: b's first id is not in a
351def fin_dj2(+a: List<&2, Nat>, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}) -> {fstin(b, a) == False{} : Bool}:
352 match b:
353 case Nil{}:
354 {==}
355 case Con{+b0, +t}:
356 NL.nd_dj(a, Con{b0, t}, hn, b0, self_in(b0, t))
357
358# a ++ b: a's last id is not in b
359def lin_dj2(+a: List<&2, Nat>, +b: List<&2, Nat>, +hn: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}) -> {lastin(a, b) == False{} : Bool}:
360 match a:
361 case Nil{}:
362 {==}
363 case Con{+a0, +t}:
364 NL.nd_dj2(Con{a0, t}, b, hn, NL.lastn(t, a0), NL.lastn_mem(t, a0))
365
366def or_f(+x: Bool, +h: {x == False{} : Bool}) -> {Bool.or(x, False{}) == False{} : Bool}:
367 L.subst(Bool, z => {Bool.or(z, False{}) == False{} : Bool}, False{}, x, Equal.sym(Bool, x, False{}, h), {==})
368
369# n off b: b's first id is not n
370def fin1(+b: List<&2, Nat>, +n: Nat, +h: {NL.memn(n, b) == False{} : Bool}) -> {fstin(b, Con{n, Nil{}}) == False{} : Bool}:
371 match b:
372 case Nil{}:
373 {==}
374 case Con{+b0, +t}:
375 or_f(Nat.is_eq(n, b0), NL.ne_sym(b0, n, NL.or_ff_l(Nat.is_eq(b0, n), NL.memn(n, t), h)))
376
377# n off a: a's last id is not n
378def lin1(+a: List<&2, Nat>, +n: Nat, +h: {NL.memn(n, a) == False{} : Bool}) -> {lastin(a, Con{n, Nil{}}) == False{} : Bool}:
379 match a:
380 case Nil{}:
381 {==}
382 case Con{+a0, +t}:
383 or_f(Nat.is_eq(n, NL.lastn(t, a0)), NL.ne_sym(NL.lastn(t, a0), n, NL.ne_mem(n, NL.lastn(t, a0), Con{a0, t}, NL.not_f(NL.memn(n, Con{a0, t}), h), NL.lastn_mem(t, a0))))
384
385
386# THEOREM (unlink): s between a and b; b's first prev becomes a's last link
387# and a's last next becomes b's first link: a ++ b is linked
388def unl_seg(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hs: {ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0) == True{} : Bool}, +hn: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hlp: {fstlt(b, SC.length(U32, pl)) == True{} : Bool}, +hln: {lastlt(a, SC.length(U32, nl)) == True{} : Bool}) -> {ST.seg(upd_first(pl, b, LKx.last_or(a, 0)), upd_last(nl, a, LKx.fst_or(b, 0)), SC.append(Nat, a, b), 0, 0) == True{} : Bool}:
389 +pl2 = upd_first(pl, b, LKx.last_or(a, 0))
390 +nl2 = upd_last(nl, a, LKx.fst_or(b, 0))
391 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, Con{s, b}, 0, 0), hs)
392 +hsA = L.and_left(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp)
393 +hsS = L.and_right(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp)
394 +hsB = L.and_right(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0), L.and_right(U32.is_eq(W32.nth0(pl, s), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0)), hsS))
395 +hnS = NL.nd_r(a, Con{s, b}, hn)
396 +hA1 = seg_ulq(pl, nl, a, 0, LKx.lnk(s), LKx.fst_or(b, 0), hsA, NL.nd_l(a, Con{s, b}, hn), hln)
397 +hA = by_eq(ST.seg(pl2, nl2, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl2, a, 0, LKx.fst_or(b, 0)), seg_ffp(pl, nl2, b, LKx.last_or(a, 0), a, 0, LKx.fst_or(b, 0), fin_dj(a, s, b, hn)), hA1)
398 +hB1 = seg_ufp(pl, nl, b, LKx.lnk(s), 0, LKx.last_or(a, 0), hsB, L.and_right(Bool.not(NL.memn(s, b)), NL.nodupn(b), hnS), hlp)
399 +hB = by_eq(ST.seg(pl2, nl2, b, LKx.last_or(a, 0), 0), ST.seg(pl2, nl, b, LKx.last_or(a, 0), 0), seg_lfn(pl2, nl, a, LKx.fst_or(b, 0), b, LKx.last_or(a, 0), 0, lin_dj(a, s, b, hn)), hB1)
400 by_eq(ST.seg(pl2, nl2, SC.append(Nat, a, b), 0, 0), Bool.and(ST.seg(pl2, nl2, a, 0, LKx.fst_or(b, 0)), ST.seg(pl2, nl2, b, LKx.last_or(a, 0), 0)), LK.seg_app(pl2, nl2, a, b, 0, 0), L.and_intro(ST.seg(pl2, nl2, a, 0, LKx.fst_or(b, 0)), ST.seg(pl2, nl2, b, LKx.last_or(a, 0), 0), hA, hB))
401
402# ... and s's own links are a's last and b's first
403def unl_p(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hs: {ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0) == True{} : Bool}) -> {W32.nth0(pl, s) == LKx.last_or(a, 0) : U32}:
404 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, Con{s, b}, 0, 0), hs)
405 +hsS = L.and_right(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp)
406 A.eq_of(W32.nth0(pl, s), LKx.last_or(a, 0), L.and_left(U32.is_eq(W32.nth0(pl, s), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0)), hsS))
407
408def unl_n(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hs: {ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0) == True{} : Bool}) -> {W32.nth0(nl, s) == LKx.fst_or(b, 0) : U32}:
409 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, Con{s, b}), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, Con{s, b}, 0, 0), hs)
410 +hsS = L.and_right(ST.seg(pl, nl, a, 0, LKx.lnk(s)), ST.seg(pl, nl, Con{s, b}, LKx.last_or(a, 0), 0), hsp)
411 +hr = L.and_right(U32.is_eq(W32.nth0(pl, s), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0)), hsS)
412 A.eq_of(W32.nth0(nl, s), LKx.fst_or(b, 0), L.and_left(U32.is_eq(W32.nth0(nl, s), LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.lnk(s), 0), hr))
413
414
415# THEOREM (insert between): n off a ++ b takes a's last as prev and b's
416# first as next, and becomes their next and prev: a ++ n :: b is linked
417def ins_seg(+pl: List<&2, U32>, +nl: List<&2, U32>, +a: List<&2, Nat>, +b: List<&2, Nat>, +n: Nat, +hs: {ST.seg(pl, nl, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +hn: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +hna: {NL.memn(n, a) == False{} : Bool}, +hnb: {NL.memn(n, b) == False{} : Bool}, +hlp: {Nat.is_lt(n, SC.length(U32, pl)) == True{} : Bool}, +hlq: {Nat.is_lt(n, SC.length(U32, nl)) == True{} : Bool}, +hfp: {fstlt(b, SC.length(U32, SC.update(U32, pl, n, LKx.last_or(a, 0)))) == True{} : Bool}, +hfq: {lastlt(a, SC.length(U32, SC.update(U32, nl, n, LKx.fst_or(b, 0)))) == True{} : Bool}) -> {ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), SC.append(Nat, a, Con{n, b}), 0, 0) == True{} : Bool}:
418 +hsp = to_eq(ST.seg(pl, nl, SC.append(Nat, a, b), 0, 0), Bool.and(ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0)), LK.seg_app(pl, nl, a, b, 0, 0), hs)
419 +hsA = L.and_left(ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0), hsp)
420 +hsB = L.and_right(ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0), hsp)
421 +hA1 = by_eq(ST.seg(pl, SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, 0, LKx.fst_or(b, 0)), ST.seg(pl, nl, a, 0, LKx.fst_or(b, 0)), LK.seg_fn(pl, nl, n, LKx.fst_or(b, 0), a, 0, LKx.fst_or(b, 0), hna), hsA)
422 +hA2 = seg_ulq(pl, SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, 0, LKx.fst_or(b, 0), LKx.lnk(n), hA1, NL.nd_l(a, b, hn), hfq)
423 +hA3 = by_eq(ST.seg(SC.update(U32, pl, n, LKx.last_or(a, 0)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(pl, upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), LK.seg_fp(pl, upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n, LKx.last_or(a, 0), a, 0, LKx.lnk(n), hna), hA2)
424 +hA = by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(SC.update(U32, pl, n, LKx.last_or(a, 0)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), seg_ffp(SC.update(U32, pl, n, LKx.last_or(a, 0)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), a, 0, LKx.lnk(n), fin_dj2(a, b, hn)), hA3)
425 +ep = Equal.trans(U32, W32.nth0(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), n), W32.nth0(SC.update(U32, pl, n, LKx.last_or(a, 0)), n), LKx.last_or(a, 0), nth_uf(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n), n, fin1(b, n, hnb)), W32.nth0_upd_same(pl, n, LKx.last_or(a, 0), hlp))
426 +eq = Equal.trans(U32, W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), W32.nth0(SC.update(U32, nl, n, LKx.fst_or(b, 0)), n), LKx.fst_or(b, 0), nth_ul(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n), n, lin1(a, n, hna)), W32.nth0_upd_same(nl, n, LKx.fst_or(b, 0), hlq))
427 +hB1 = by_eq(ST.seg(SC.update(U32, pl, n, LKx.last_or(a, 0)), nl, b, LKx.last_or(a, 0), 0), ST.seg(pl, nl, b, LKx.last_or(a, 0), 0), LK.seg_fp(pl, nl, n, LKx.last_or(a, 0), b, LKx.last_or(a, 0), 0, hnb), hsB)
428 +hB2 = seg_ufp(SC.update(U32, pl, n, LKx.last_or(a, 0)), nl, b, LKx.last_or(a, 0), 0, LKx.lnk(n), hB1, NL.nd_r(a, b, hn), hfp)
429 +hB3 = by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), SC.update(U32, nl, n, LKx.fst_or(b, 0)), b, LKx.lnk(n), 0), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), nl, b, LKx.lnk(n), 0), LK.seg_fn(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), nl, n, LKx.fst_or(b, 0), b, LKx.lnk(n), 0, hnb), hB2)
430 +hB = by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), 0), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), SC.update(U32, nl, n, LKx.fst_or(b, 0)), b, LKx.lnk(n), 0), seg_lfn(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n), b, LKx.lnk(n), 0, lin_dj2(a, b, hn)), hB3)
431 +hN = L.and_intro(U32.is_eq(W32.nth0(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), n), LKx.last_or(a, 0)), Bool.and(U32.is_eq(W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), LKx.fst_or(b, 0)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), 0)), u_is(W32.nth0(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), n), LKx.last_or(a, 0), ep), L.and_intro(U32.is_eq(W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), LKx.fst_or(b, 0)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), b, LKx.lnk(n), 0), u_is(W32.nth0(upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), n), LKx.fst_or(b, 0), eq), hB))
432 by_eq(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), SC.append(Nat, a, Con{n, b}), 0, 0), Bool.and(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), Con{n, b}, LKx.last_or(a, 0), 0)), LK.seg_app(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, Con{n, b}, 0, 0), L.and_intro(ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), a, 0, LKx.lnk(n)), ST.seg(upd_first(SC.update(U32, pl, n, LKx.last_or(a, 0)), b, LKx.lnk(n)), upd_last(SC.update(U32, nl, n, LKx.fst_or(b, 0)), a, LKx.lnk(n)), Con{n, b}, LKx.last_or(a, 0), 0), hA, hN))