proofs/containers/lru/unlink.bend

bend-collections-laws-containers@1.0.0.0 · 193 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/proofs/lib/list.bend as LL
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
10import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
11import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/lists.bend as LS
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dll.bend as DL
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/trace.bend as TR
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
19import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
20import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
21
22# unlink: detaching a slot from the middle of the recency list.
23
24
25# ---- bounds ----
26
27def sd1(+sd: Nat, +h: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}) -> {Nat.is_lt(1n+sd, 32n) == True{} : Bool}:
28  N.le_lt_trans(1n+sd, 3n+sd, 32n, N.le_trans(1n+sd, 2n+sd, 3n+sd, N.le_succ(1n+sd), N.le_succ(2n+sd)), h)
29
30def sd3(+sd: Nat, +h: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}) -> {Nat.is_le(3n+sd, 32n) == True{} : Bool}:
31  N.lt_le(3n+sd, 32n, h)
32
33def lnk_nz(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(sd)) == True{} : Bool}) -> {U32.is_eq(LK.lnk(b), 0) == False{} : Bool}:
34  +hk = N.lt_le(sd, 32n, N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), sd1(sd, hsd)))
35  +e1 = U.to_nat_from_nat(b, sd, hk, hb)
36  +hb2 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, b, UD.v(U32.from_nat(b)), Equal.sym(Nat, UD.v(U32.from_nat(b)), b, e1), hb)
37  W32.link_nz(one, h1, U32.from_nat(b), W32.bound32(one, h1, UD.v(U32.from_nat(b)), sd, sd1(sd, hsd), hb2))
38
39# the lk index of word o (< 8) of the slot of b's link
40def ix_o(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(sd)) == True{} : Bool}) -> {UD.v(H.slot(LK.lnk(b))) == b : Nat}:
41  LK.slot_lnk(one, h1, b, sd, sd1(sd, hsd), hb)
42
43def ix_p(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.pidx(H.slot(LK.lnk(b)))) == ST.off(b, 0n) : Nat}:
44  +e = ix_o(one, h1, b, sd, hsd, hb)
45  +hs = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, b, UD.v(H.slot(LK.lnk(b))), Equal.sym(Nat, UD.v(H.slot(LK.lnk(b))), b, e), hb)
46  Equal.trans(Nat, UD.v(LR.pidx(H.slot(LK.lnk(b)))), ST.off(UD.v(H.slot(LK.lnk(b))), 0n), ST.off(b, 0n), ID.w0(one, h1, H.slot(LK.lnk(b)), sd, sd3(sd, hsd), hs), Equal.cong(Nat, Nat, z => ST.off(z, 0n), UD.v(H.slot(LK.lnk(b))), b, e))
47
48def ix_n(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(sd)) == True{} : Bool}) -> {UD.v(LR.nidx(H.slot(LK.lnk(b)))) == ST.off(b, 1n) : Nat}:
49  +e = ix_o(one, h1, b, sd, hsd, hb)
50  +hs = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, b, UD.v(H.slot(LK.lnk(b))), Equal.sym(Nat, UD.v(H.slot(LK.lnk(b))), b, e), hb)
51  Equal.trans(Nat, UD.v(LR.nidx(H.slot(LK.lnk(b)))), ST.off(UD.v(H.slot(LK.lnk(b))), 1n), ST.off(b, 1n), ID.w1(one, h1, H.slot(LK.lnk(b)), sd, sd3(sd, hsd), hs), Equal.cong(Nat, Nat, z => ST.off(z, 1n), UD.v(H.slot(LK.lnk(b))), b, e))
52
53# a write of word o of slot b (b < 2^sd): the new tree, its slots, its trace
54def wr(+one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +i: U32, +b: Nat, +o: Nat, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(sd)) == True{} : Bool}, +hi: {UD.v(i) == ST.off(b, o) : Nat}, +x: U32) -> {Array.set(U32, AR.thaw(U32, lkT), i, x) == AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), x)) : Array<U32>}:
55  +hl = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(3n+sd)) == True{} : Bool}, ST.off(b, o), UD.v(i), Equal.sym(Nat, UD.v(i), ST.off(b, o), hi), ID.off_lt(b, sd, hb, o, ho))
56  UT.uset_a(3n+sd, hsd, lkT, hpl, i, hl, x)
57
58def wr_s(+lkT: AR.Tree<U32>, +sd: Nat, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +i: U32, +b: Nat, +o: Nat, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(sd)) == True{} : Bool}, +hi: {UD.v(i) == ST.off(b, o) : Nat}, +x: U32) -> {AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), x)) == SC.update(U32, AR.slots(U32, lkT), ST.off(b, o), x) : List<&2, U32>}:
59  +hl = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(3n+sd)) == True{} : Bool}, ST.off(b, o), UD.v(i), Equal.sym(Nat, UD.v(i), ST.off(b, o), hi), ID.off_lt(b, sd, hb, o, ho))
60  Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), x)), SC.update(U32, AR.slots(U32, lkT), UD.v(i), x), SC.update(U32, AR.slots(U32, lkT), ST.off(b, o), x), UT.uset_s(3n+sd, lkT, hpl, UD.v(i), hl, x), Equal.cong(Nat, List<&2, U32>, z => SC.update(U32, AR.slots(U32, lkT), z, x), UD.v(i), ST.off(b, o), hi))
61
62def len_ll(+lkT: AR.Tree<U32>, +sd: Nat, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +b: Nat, +o: Nat, +ho: {Nat.is_lt(o, 8n) == True{} : Bool}, +hb: {Nat.is_lt(b, SC.pow2(sd)) == True{} : Bool}) -> {Nat.is_lt(ST.off(b, o), SC.length(U32, AR.slots(U32, lkT))) == True{} : Bool}:
63  UT.len_of(U32, 3n+sd, lkT, hpl, ST.off(b, o), ID.off_lt(b, sd, hb, o, ho))
64
65# ---- the two writes ----
66
67def Step(+t0: AR.Tree<U32>, +sd: Nat, +xs: List<&2, Nat>, +p: U32, +q: U32, r: Array<U32>) -> Type:
68  Sigma<&1, &1, AR.Tree<U32>, t1 => Sigma<&1, &1, TR.Tr, tr => {r == AR.thaw(U32, t1) : Array<U32>} & ({AR.perfect(U32, 3n+sd, t1) == True{} : Bool} & ({AR.slots(U32, t1) == TR.app(AR.slots(U32, t0), tr) : List<&2, U32>} & ({TR.trlo(tr) == True{} : Bool} & ({TR.trin(tr, xs) == True{} : Bool} & {ST.seg(AR.slots(U32, t1), xs, p, q) == True{} : Bool}))))>>
69
70def self_in(+b: Nat, +t: List<&2, Nat>) -> {NL.memn(b, Con{b, t}) == True{} : Bool}:
71  NL.or_tl(Nat.is_eq(b, b), NL.memn(b, t), N.is_eq_refl(b))
72
73def bnd_of(~V: Data, +x: Nat, +xs: List<&2, Nat>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +sd: Nat, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +h: {ST.sall(~V, ST.PLive{fr, el}, xs) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {Nat.is_lt(x, SC.pow2(sd)) == True{} : Bool}:
74  N.lt_le_trans(x, fr, SC.pow2(sd), L.and_left(Nat.is_lt(x, fr), ST.live(~V, el, x), LS.sall_mem(~V, ST.PLive{fr, el}, x, xs, h, hm)), hfr)
75
76# the successor's prev becomes p
77def ul_q(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +p: U32, +s: Nat, +b: List<&2, Nat>, +hB: {ST.seg(AR.slots(U32, lkT), b, LK.lnk(s), 0) == True{} : Bool}, +hnB: {NL.nodupn(b) == True{} : Bool}, +hbB: {ST.sall(~V, ST.PLive{fr, el}, b) == True{} : Bool}) -> Step(lkT, sd, b, p, 0, LR.set_if(AR.thaw(U32, lkT), LR.pidx(H.slot(LK.fst_or(b, 0))), p, U32.is_eq(LK.fst_or(b, 0), 0))):
78  match b:
79    case Nil{}:
80      (lkT, (TR.TNil{}, ({==}, (hpl, ({==}, ({==}, ({==}, {==})))))))
81    case Con{+b0, +b2}:
82      +hb0 = bnd_of(~V, b0, Con{b0, b2}, fr, el, sd, hfr, hbB, self_in(b0, b2))
83      +ei = ix_p(one, h1, b0, sd, hsd, hb0)
84      +i = LR.pidx(H.slot(LK.lnk(b0)))
85      +ea = Equal.trans(Array<U32>, LR.set_if(AR.thaw(U32, lkT), i, p, U32.is_eq(LK.lnk(b0), 0)), LR.set_if(AR.thaw(U32, lkT), i, p, False{}), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), p)), Equal.cong(Bool, Array<U32>, z => LR.set_if(AR.thaw(U32, lkT), i, p, z), U32.is_eq(LK.lnk(b0), 0), False{}, lnk_nz(one, h1, b0, sd, hsd, hb0)), wr(one, h1, lkT, sd, hsd, hpl, i, b0, 0n, {==}, hb0, ei, p))
86      +es = wr_s(lkT, sd, hpl, i, b0, 0n, {==}, hb0, ei, p)
87      +hs = L.subst(List<&2, U32>, z => {ST.seg(z, Con{b0, b2}, p, 0) == True{} : Bool}, SC.update(U32, AR.slots(U32, lkT), ST.off(b0, 0n), p), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), p)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), p)), SC.update(U32, AR.slots(U32, lkT), ST.off(b0, 0n), p), es), DL.segp(AR.slots(U32, lkT), b0, b2, LK.lnk(s), 0, p, hB, hnB, len_ll(lkT, sd, hpl, b0, 0n, {==}, hb0)))
88      (AR.upd(U32, 3n+sd, lkT, UD.v(i), p), (TR.TW{b0, 0n, p, TR.TNil{}}, (ea, (UT.uset_p(3n+sd, lkT, hpl, UD.v(i), p), (es, ({==}, (L.and_intro(NL.memn(b0, Con{b0, b2}), True{}, self_in(b0, b2), {==}), hs)))))))
89
90# the predecessor's next becomes q
91def ul_p(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +q: U32, +x: U32, +a: List<&2, Nat>, +hA: {ST.seg(AR.slots(U32, lkT), a, 0, x) == True{} : Bool}, +hnA: {NL.nodupn(a) == True{} : Bool}, +hbA: {ST.sall(~V, ST.PLive{fr, el}, a) == True{} : Bool}) -> Step(lkT, sd, a, 0, q, LR.set_if(AR.thaw(U32, lkT), LR.nidx(H.slot(LK.last_or(a, 0))), q, U32.is_eq(LK.last_or(a, 0), 0))):
92  match a:
93    case Nil{}:
94      (lkT, (TR.TNil{}, ({==}, (hpl, ({==}, ({==}, ({==}, {==})))))))
95    case Con{+a0, +a2}:
96      +z = NL.lastn(a2, a0)
97      +hz = bnd_of(~V, z, Con{a0, a2}, fr, el, sd, hfr, hbA, NL.lastn_mem(a2, a0))
98      +ei = ix_n(one, h1, z, sd, hsd, hz)
99      +i = LR.nidx(H.slot(LK.lnk(z)))
100      +e0 = Equal.cong(U32, Array<U32>, w => LR.set_if(AR.thaw(U32, lkT), LR.nidx(H.slot(w)), q, U32.is_eq(w, 0)), LK.last_or(a2, LK.lnk(a0)), LK.lnk(z), LK.last_lnk(a2, a0))
101      +ea = Equal.trans(Array<U32>, LR.set_if(AR.thaw(U32, lkT), LR.nidx(H.slot(LK.last_or(a2, LK.lnk(a0)))), q, U32.is_eq(LK.last_or(a2, LK.lnk(a0)), 0)), LR.set_if(AR.thaw(U32, lkT), i, q, U32.is_eq(LK.lnk(z), 0)), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), q)), e0, Equal.trans(Array<U32>, LR.set_if(AR.thaw(U32, lkT), i, q, U32.is_eq(LK.lnk(z), 0)), LR.set_if(AR.thaw(U32, lkT), i, q, False{}), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), q)), Equal.cong(Bool, Array<U32>, w => LR.set_if(AR.thaw(U32, lkT), i, q, w), U32.is_eq(LK.lnk(z), 0), False{}, lnk_nz(one, h1, z, sd, hsd, hz)), wr(one, h1, lkT, sd, hsd, hpl, i, z, 1n, {==}, hz, ei, q)))
102      +es = wr_s(lkT, sd, hpl, i, z, 1n, {==}, hz, ei, q)
103      +hs = L.subst(List<&2, U32>, w => {ST.seg(w, Con{a0, a2}, 0, q) == True{} : Bool}, SC.update(U32, AR.slots(U32, lkT), ST.off(z, 1n), q), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), q)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(i), q)), SC.update(U32, AR.slots(U32, lkT), ST.off(z, 1n), q), es), DL.segq(AR.slots(U32, lkT), a2, a0, 0, x, q, hA, hnA, len_ll(lkT, sd, hpl, z, 1n, {==}, hz)))
104      (AR.upd(U32, 3n+sd, lkT, UD.v(i), q), (TR.TW{z, 1n, q, TR.TNil{}}, (ea, (UT.uset_p(3n+sd, lkT, hpl, UD.v(i), q), (es, ({==}, (L.and_intro(NL.memn(z, Con{a0, a2}), True{}, NL.lastn_mem(a2, a0), {==}), hs)))))))
105
106# ---- head and tail ----
107
108def pick_f(+c: Bool, +h: {c == False{} : Bool}, +x: U32, +y: U32) -> {LR.pick(c, x, y) == y : U32}:
109  L.subst(Bool, z => {LR.pick(z, x, y) == y : U32}, False{}, c, Equal.sym(Bool, c, False{}, h), {==})
110
111def hd_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +head: U32, +hh: {U32.is_eq(head, LK.fst_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}, +hbA: {ST.sall(~V, ST.PLive{fr, el}, a) == True{} : Bool}) -> {LR.pick(U32.is_eq(LK.last_or(a, 0), 0), LK.fst_or(b, 0), head) == LK.fst_or(SC.append(Nat, a, b), 0) : U32}:
112  match a:
113    case Nil{}:
114      {==}
115    case Con{+a0, +a2}:
116      +z = NL.lastn(a2, a0)
117      +hz = bnd_of(~V, z, Con{a0, a2}, fr, el, sd, hfr, hbA, NL.lastn_mem(a2, a0))
118      +hc = Equal.trans(Bool, U32.is_eq(LK.last_or(a2, LK.lnk(a0)), 0), U32.is_eq(LK.lnk(z), 0), False{}, Equal.cong(U32, Bool, w => U32.is_eq(w, 0), LK.last_or(a2, LK.lnk(a0)), LK.lnk(z), LK.last_lnk(a2, a0)), lnk_nz(one, h1, z, sd, hsd, hz))
119      Equal.trans(U32, LR.pick(U32.is_eq(LK.last_or(a2, LK.lnk(a0)), 0), LK.fst_or(b, 0), head), head, LK.lnk(a0), pick_f(U32.is_eq(LK.last_or(a2, LK.lnk(a0)), 0), hc, LK.fst_or(b, 0), head), A.eq_of(head, LK.lnk(a0), hh))
120
121def tl_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +tail: U32, +ht: {U32.is_eq(tail, LK.last_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}, +hbB: {ST.sall(~V, ST.PLive{fr, el}, b) == True{} : Bool}) -> {LR.pick(U32.is_eq(LK.fst_or(b, 0), 0), LK.last_or(a, 0), tail) == LK.last_or(SC.append(Nat, a, b), 0) : U32}:
122  match b:
123    case Nil{}:
124      Equal.cong(List<&2, Nat>, U32, w => LK.last_or(w, 0), a, SC.append(Nat, a, Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, a, Nil{}), a, LL.append_nil(Nat, a)))
125    case Con{+b0, +b2}:
126      +hb0 = bnd_of(~V, b0, Con{b0, b2}, fr, el, sd, hfr, hbB, self_in(b0, b2))
127      +et = Equal.trans(U32, tail, LK.last_or(SC.append(Nat, a, Con{s, Con{b0, b2}}), 0), LK.last_or(b2, LK.lnk(b0)), A.eq_of(tail, LK.last_or(SC.append(Nat, a, Con{s, Con{b0, b2}}), 0), ht), LK.last_app(a, Con{s, Con{b0, b2}}, 0))
128      Equal.trans(U32, LR.pick(U32.is_eq(LK.lnk(b0), 0), LK.last_or(a, 0), tail), tail, LK.last_or(SC.append(Nat, a, Con{b0, b2}), 0), pick_f(U32.is_eq(LK.lnk(b0), 0), lnk_nz(one, h1, b0, sd, hsd, hb0), LK.last_or(a, 0), tail), Equal.trans(U32, tail, LK.last_or(b2, LK.lnk(b0)), LK.last_or(SC.append(Nat, a, Con{b0, b2}), 0), et, Equal.sym(U32, LK.last_or(SC.append(Nat, a, Con{b0, b2}), 0), LK.last_or(b2, LK.lnk(b0)), LK.last_app(a, Con{b0, b2}, 0))))
129
130# ---- unlink ----
131
132
133def UnlOK(~V: Data, +cap: U32, +n: U32, +free: U32, +mT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sd: Nat, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, r: LR.LRU<&2, V>) -> Type:
134  Sigma<&1, &1, AR.Tree<U32>, t2 => Sigma<&1, &1, TR.Tr, tr => {r == LR.F{cap, n, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t2)} : LR.LRU<&2, V>} & ({AR.perfect(U32, 3n+sd, t2) == True{} : Bool} & ({AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>} & ({TR.trlo(tr) == True{} : Bool} & ({TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool} & {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}))))>>
135
136def f_eq(~V: Data, +cap: U32, +n: U32, +free: U32, +mT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +h: U32, +h2: U32, +t: U32, +t2: U32, +lk: AR.Tree<U32>, -x: Array<U32>, +eh: {h == h2 : U32}, +et: {t == t2 : U32}, +ex: {x == AR.thaw(U32, lk) : Array<U32>}) -> {LR.F{cap, n, h, t, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), x} == LR.F{cap, n, h2, t2, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lk)} : LR.LRU<&2, V>}:
137  +r1 = L.subst(U32, z => {LR.F{cap, n, h, t, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), x} == LR.F{cap, n, z, t, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), x} : LR.LRU<&2, V>}, h, h2, eh, {==})
138  +r2 = L.subst(U32, z => {LR.F{cap, n, h, t, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), x} == LR.F{cap, n, h2, z, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), x} : LR.LRU<&2, V>}, t, t2, et, r1)
139  L.subst(Array<U32>, z => {LR.F{cap, n, h, t, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), x} == LR.F{cap, n, h2, t2, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), z} : LR.LRU<&2, V>}, x, AR.thaw(U32, lk), ex, r2)
140
141def ul_b(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +cap: U32, +n: U32, +free: U32, +mT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +head: U32, +tail: U32, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hnd: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hbA: {ST.sall(~V, ST.PLive{fr, el}, a) == True{} : Bool}, +hbB: {ST.sall(~V, ST.PLive{fr, el}, b) == True{} : Bool}, +hh: {U32.is_eq(head, LK.fst_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}, +ht: {U32.is_eq(tail, LK.last_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}, +t1: AR.Tree<U32>, +tr1: TR.Tr, +ea1: {LR.set_if(AR.thaw(U32, lkT), LR.pidx(H.slot(LK.fst_or(b, 0))), LK.last_or(a, 0), U32.is_eq(LK.fst_or(b, 0), 0)) == AR.thaw(U32, t1) : Array<U32>}, +hs1: {AR.slots(U32, t1) == TR.app(AR.slots(U32, lkT), tr1) : List<&2, U32>}, +hl1: {TR.trlo(tr1) == True{} : Bool}, +hi1: {TR.trin(tr1, b) == True{} : Bool}, +hg1: {ST.seg(AR.slots(U32, t1), b, LK.last_or(a, 0), 0) == True{} : Bool}, st2: Step(t1, sd, a, 0, LK.fst_or(b, 0), LR.set_if(AR.thaw(U32, t1), LR.nidx(H.slot(LK.last_or(a, 0))), LK.fst_or(b, 0), U32.is_eq(LK.last_or(a, 0), 0)))) -> UnlOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), LK.fst_or(b, 0)))):
142  match st2:
143    case Tuple{+t2, Tuple{+tr2, Tuple{+ea2, Tuple{+hp2, Tuple{+hs2, Tuple{+hl2, Tuple{+hi2, hg2}}}}}}}:
144      +ex = Equal.trans(Array<U32>, LR.set_if(LR.set_if(AR.thaw(U32, lkT), LR.pidx(H.slot(LK.fst_or(b, 0))), LK.last_or(a, 0), U32.is_eq(LK.fst_or(b, 0), 0)), LR.nidx(H.slot(LK.last_or(a, 0))), LK.fst_or(b, 0), U32.is_eq(LK.last_or(a, 0), 0)), LR.set_if(AR.thaw(U32, t1), LR.nidx(H.slot(LK.last_or(a, 0))), LK.fst_or(b, 0), U32.is_eq(LK.last_or(a, 0), 0)), AR.thaw(U32, t2), Equal.cong(Array<U32>, Array<U32>, z => LR.set_if(z, LR.nidx(H.slot(LK.last_or(a, 0))), LK.fst_or(b, 0), U32.is_eq(LK.last_or(a, 0), 0)), LR.set_if(AR.thaw(U32, lkT), LR.pidx(H.slot(LK.fst_or(b, 0))), LK.last_or(a, 0), U32.is_eq(LK.fst_or(b, 0), 0)), AR.thaw(U32, t1), ea1), ea2)
145      +er = f_eq(~V, cap, n, free, mT, tabT, ksT, eT, LR.pick(U32.is_eq(LK.last_or(a, 0), 0), LK.fst_or(b, 0), head), LK.fst_or(SC.append(Nat, a, b), 0), LR.pick(U32.is_eq(LK.fst_or(b, 0), 0), LK.last_or(a, 0), tail), LK.last_or(SC.append(Nat, a, b), 0), t2, LR.set_if(LR.set_if(AR.thaw(U32, lkT), LR.pidx(H.slot(LK.fst_or(b, 0))), LK.last_or(a, 0), U32.is_eq(LK.fst_or(b, 0), 0)), LR.nidx(H.slot(LK.last_or(a, 0))), LK.fst_or(b, 0), U32.is_eq(LK.last_or(a, 0), 0)), hd_ok(~V, one, h1, sd, hsd, fr, el, hfr, a, s, b, head, hh, hbA), tl_ok(~V, one, h1, sd, hsd, fr, el, hfr, a, s, b, tail, ht, hbB), ex)
146      +tr = TR.tcat(tr2, tr1)
147      +hs = Equal.trans(List<&2, U32>, AR.slots(U32, t2), TR.app(AR.slots(U32, t1), tr2), TR.app(AR.slots(U32, lkT), tr), hs2, Equal.trans(List<&2, U32>, TR.app(AR.slots(U32, t1), tr2), TR.app(TR.app(AR.slots(U32, lkT), tr1), tr2), TR.app(AR.slots(U32, lkT), tr), Equal.cong(List<&2, U32>, List<&2, U32>, z => TR.app(z, tr2), AR.slots(U32, t1), TR.app(AR.slots(U32, lkT), tr1), hs1), Equal.sym(List<&2, U32>, TR.app(AR.slots(U32, lkT), tr), TR.app(TR.app(AR.slots(U32, lkT), tr1), tr2), TR.app_cat(AR.slots(U32, lkT), tr2, tr1))))
148      +hin = TR.in_cat(tr2, tr1, SC.append(Nat, a, Con{s, b}), TR.trin_l(tr2, a, Con{s, b}, hi2), TR.trin_r(tr1, a, Con{s, b}, TR.trin_cons(tr1, s, b, hi1)))
149      +out2 = TR.trout_tail(tr2, s, b, TR.trout_r(tr2, a, Con{s, b}, hi2, hnd))
150      +hgB = L.subst(Bool, z => {z == True{} : Bool}, ST.seg(AR.slots(U32, t1), b, LK.last_or(a, 0), 0), ST.seg(AR.slots(U32, t2), b, LK.last_or(a, 0), 0), Equal.sym(Bool, ST.seg(AR.slots(U32, t2), b, LK.last_or(a, 0), 0), ST.seg(AR.slots(U32, t1), b, LK.last_or(a, 0), 0), L.subst(List<&2, U32>, z => {ST.seg(z, b, LK.last_or(a, 0), 0) == ST.seg(AR.slots(U32, t1), b, LK.last_or(a, 0), 0) : Bool}, TR.app(AR.slots(U32, t1), tr2), AR.slots(U32, t2), Equal.sym(List<&2, U32>, AR.slots(U32, t2), TR.app(AR.slots(U32, t1), tr2), hs2), TR.seg_tr(AR.slots(U32, t1), tr2, hl2, b, LK.last_or(a, 0), 0, out2))), hg1)
151      +hg = L.subst(Bool, z => {z == True{} : Bool}, Bool.and(ST.seg(AR.slots(U32, t2), a, 0, LK.fst_or(b, 0)), ST.seg(AR.slots(U32, t2), b, LK.last_or(a, 0), 0)), ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0), Equal.sym(Bool, ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0), Bool.and(ST.seg(AR.slots(U32, t2), a, 0, LK.fst_or(b, 0)), ST.seg(AR.slots(U32, t2), b, LK.last_or(a, 0), 0)), DL.seg_app(AR.slots(U32, t2), a, b, 0, 0)), L.and_intro(ST.seg(AR.slots(U32, t2), a, 0, LK.fst_or(b, 0)), ST.seg(AR.slots(U32, t2), b, LK.last_or(a, 0), 0), hg2, hgB))
152      (t2, (tr, (er, (hp2, (hs, (TR.lo_cat(tr2, tr1, hl2, hl1), (hin, hg)))))))
153
154def ul_a(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +cap: U32, +n: U32, +free: U32, +mT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +head: U32, +tail: U32, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hnd: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hbA: {ST.sall(~V, ST.PLive{fr, el}, a) == True{} : Bool}, +hbB: {ST.sall(~V, ST.PLive{fr, el}, b) == True{} : Bool}, +hh: {U32.is_eq(head, LK.fst_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}, +ht: {U32.is_eq(tail, LK.last_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}, +hsA: {ST.seg(AR.slots(U32, lkT), a, 0, LK.lnk(s)) == True{} : Bool}, st1: Step(lkT, sd, b, LK.last_or(a, 0), 0, LR.set_if(AR.thaw(U32, lkT), LR.pidx(H.slot(LK.fst_or(b, 0))), LK.last_or(a, 0), U32.is_eq(LK.fst_or(b, 0), 0)))) -> UnlOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), LK.fst_or(b, 0)))):
155  match st1:
156    case Tuple{+t1, Tuple{+tr1, Tuple{+ea1, Tuple{+hp1, Tuple{+hs1, Tuple{+hl1, Tuple{+hi1, hg1}}}}}}}:
157      +out1 = TR.trout_l(tr1, a, Con{s, b}, TR.trin_cons(tr1, s, b, hi1), hnd)
158      +hsA1 = L.subst(Bool, z => {z == True{} : Bool}, ST.seg(AR.slots(U32, lkT), a, 0, LK.lnk(s)), ST.seg(AR.slots(U32, t1), a, 0, LK.lnk(s)), Equal.sym(Bool, ST.seg(AR.slots(U32, t1), a, 0, LK.lnk(s)), ST.seg(AR.slots(U32, lkT), a, 0, LK.lnk(s)), L.subst(List<&2, U32>, z => {ST.seg(z, a, 0, LK.lnk(s)) == ST.seg(AR.slots(U32, lkT), a, 0, LK.lnk(s)) : Bool}, TR.app(AR.slots(U32, lkT), tr1), AR.slots(U32, t1), Equal.sym(List<&2, U32>, AR.slots(U32, t1), TR.app(AR.slots(U32, lkT), tr1), hs1), TR.seg_tr(AR.slots(U32, lkT), tr1, hl1, a, 0, LK.lnk(s), out1))), hsA)
159      ul_b(~V, one, h1, lkT, sd, hsd, hpl, cap, n, free, mT, tabT, ksT, eT, fr, el, hfr, head, tail, a, s, b, hnd, hbA, hbB, hh, ht, t1, tr1, ea1, hs1, hl1, hi1, hg1, ul_p(~V, one, h1, t1, sd, hsd, hp1, fr, el, hfr, LK.fst_or(b, 0), LK.lnk(s), a, hsA1, NL.nd_l(a, Con{s, b}, hnd), hbA))
160
161
162# THEOREM (unlink): slot s, between a and b on the recency list, is
163# detached: the list a ++ b is linked, with its own head and tail; only link
164# words of listed slots are written.
165def unlink_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree<U32>, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hpl: {AR.perfect(U32, 3n+sd, lkT) == True{} : Bool}, +cap: U32, +n: U32, +free: U32, +mT: AR.Tree<U32>, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +fr: Nat, +el: List<&2, Maybe<&2, V>>, +hfr: {Nat.is_le(fr, SC.pow2(sd)) == True{} : Bool}, +head: U32, +tail: U32, +su: U32, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hsv: {UD.v(su) == s : Nat}, +hseg: {ST.seg(AR.slots(U32, lkT), SC.append(Nat, a, Con{s, b}), 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hsl: {ST.sall(~V, ST.PLive{fr, el}, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hh: {U32.is_eq(head, LK.fst_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}, +ht: {U32.is_eq(tail, LK.last_or(SC.append(Nat, a, Con{s, b}), 0)) == True{} : Bool}) -> UnlOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, LR.unlink(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su)):
166  +hsp = L.subst(Bool, z => {z == True{} : Bool}, ST.seg(AR.slots(U32, lkT), SC.append(Nat, a, Con{s, b}), 0, 0), Bool.and(ST.seg(AR.slots(U32, lkT), a, 0, LK.lnk(s)), ST.seg(AR.slots(U32, lkT), Con{s, b}, LK.last_or(a, 0), 0)), DL.seg_app(AR.slots(U32, lkT), a, Con{s, b}, 0, 0), hseg)
167  +hsA = L.and_left(ST.seg(AR.slots(U32, lkT), a, 0, LK.lnk(s)), ST.seg(AR.slots(U32, lkT), Con{s, b}, LK.last_or(a, 0), 0), hsp)
168  +hsS = L.and_right(ST.seg(AR.slots(U32, lkT), a, 0, LK.lnk(s)), ST.seg(AR.slots(U32, lkT), Con{s, b}, LK.last_or(a, 0), 0), hsp)
169  +hsS2 = L.and_right(U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 0n), LK.last_or(a, 0)), Bool.and(U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 1n), LK.fst_or(b, 0)), ST.seg(AR.slots(U32, lkT), b, LK.lnk(s), 0)), hsS)
170  +eP = A.eq_of(ST.lw(AR.slots(U32, lkT), s, 0n), LK.last_or(a, 0), L.and_left(U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 0n), LK.last_or(a, 0)), Bool.and(U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 1n), LK.fst_or(b, 0)), ST.seg(AR.slots(U32, lkT), b, LK.lnk(s), 0)), hsS))
171  +eQ = A.eq_of(ST.lw(AR.slots(U32, lkT), s, 1n), LK.fst_or(b, 0), L.and_left(U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 1n), LK.fst_or(b, 0)), ST.seg(AR.slots(U32, lkT), b, LK.lnk(s), 0), hsS2))
172  +hbs = L.subst(Bool, z => {z == True{} : Bool}, ST.sall(~V, ST.PLive{fr, el}, SC.append(Nat, a, Con{s, b})), Bool.and(ST.sall(~V, ST.PLive{fr, el}, a), ST.sall(~V, ST.PLive{fr, el}, Con{s, b})), LS.sall_app(~V, ST.PLive{fr, el}, a, Con{s, b}), hsl)
173  +hbA = L.and_left(ST.sall(~V, ST.PLive{fr, el}, a), ST.sall(~V, ST.PLive{fr, el}, Con{s, b}), hbs)
174  +hbS = L.and_right(ST.sall(~V, ST.PLive{fr, el}, a), ST.sall(~V, ST.PLive{fr, el}, Con{s, b}), hbs)
175  +hbB = L.and_right(ST.sev(~V, ST.PLive{fr, el}, s), ST.sall(~V, ST.PLive{fr, el}, b), hbS)
176  +hs0 = bnd_of(~V, s, Con{s, b}, fr, el, sd, hfr, hbS, self_in(s, b))
177  +hsu = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(su), Equal.sym(Nat, UD.v(su), s, hsv), hs0)
178  +iP = Equal.trans(Nat, UD.v(LR.pidx(su)), ST.off(UD.v(su), 0n), ST.off(s, 0n), ID.w0(one, h1, su, sd, sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 0n), UD.v(su), s, hsv))
179  +iN = Equal.trans(Nat, UD.v(LR.nidx(su)), ST.off(UD.v(su), 1n), ST.off(s, 1n), ID.w1(one, h1, su, sd, sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 1n), UD.v(su), s, hsv))
180  +hiP = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(3n+sd)) == True{} : Bool}, ST.off(s, 0n), UD.v(LR.pidx(su)), Equal.sym(Nat, UD.v(LR.pidx(su)), ST.off(s, 0n), iP), ID.off_lt(s, sd, hs0, 0n, {==}))
181  +hiN = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(3n+sd)) == True{} : Bool}, ST.off(s, 1n), UD.v(LR.nidx(su)), Equal.sym(Nat, UD.v(LR.nidx(su)), ST.off(s, 1n), iN), ID.off_lt(s, sd, hs0, 1n, {==}))
182  +P0 = W32.nth0(AR.slots(U32, lkT), UD.v(LR.pidx(su)))
183  +Q0 = W32.nth0(AR.slots(U32, lkT), UD.v(LR.nidx(su)))
184  +eP0 = Equal.trans(U32, P0, ST.lw(AR.slots(U32, lkT), s, 0n), LK.last_or(a, 0), Equal.cong(Nat, U32, z => W32.nth0(AR.slots(U32, lkT), z), UD.v(LR.pidx(su)), ST.off(s, 0n), iP), eP)
185  +eQ0 = Equal.trans(U32, Q0, ST.lw(AR.slots(U32, lkT), s, 1n), LK.fst_or(b, 0), Equal.cong(Nat, U32, z => W32.nth0(AR.slots(U32, lkT), z), UD.v(LR.nidx(su)), ST.off(s, 1n), iN), eQ)
186  +E1 = Equal.cong(Array<U32> & U32, LR.LRU<&2, V>, r => LR.ul_p(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), su, r), Array.get(U32, AR.thaw(U32, lkT), LR.pidx(su)), (AR.thaw(U32, lkT), P0), UT.uget(3n+sd, hsd, lkT, hpl, LR.pidx(su), hiP))
187  +E2 = Equal.cong(Array<U32> & U32, LR.LRU<&2, V>, r => LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), P0, r), Array.get(U32, AR.thaw(U32, lkT), LR.nidx(su)), (AR.thaw(U32, lkT), Q0), UT.uget(3n+sd, hsd, lkT, hpl, LR.nidx(su), hiN))
188  +E3 = Equal.cong(U32, LR.LRU<&2, V>, z => LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), z, (AR.thaw(U32, lkT), Q0)), P0, LK.last_or(a, 0), eP0)
189  +E4 = Equal.cong(U32, LR.LRU<&2, V>, z => LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), z)), Q0, LK.fst_or(b, 0), eQ0)
190  +E = Equal.trans(LR.LRU<&2, V>, LR.unlink(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su), LR.ul_p(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), su, (AR.thaw(U32, lkT), P0)), LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), LK.fst_or(b, 0))), E1, Equal.trans(LR.LRU<&2, V>, LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), P0, Array.get(U32, AR.thaw(U32, lkT), LR.nidx(su))), LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), P0, (AR.thaw(U32, lkT), Q0)), LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), LK.fst_or(b, 0))), E2, Equal.trans(LR.LRU<&2, V>, LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), P0, (AR.thaw(U32, lkT), Q0)), LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), Q0)), LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), LK.fst_or(b, 0))), E3, E4)))
191  +hnB = L.and_right(Bool.not(NL.memn(s, b)), NL.nodupn(b), NL.nd_r(a, Con{s, b}, hnd))
192  ok = ul_a(~V, one, h1, lkT, sd, hsd, hpl, cap, n, free, mT, tabT, ksT, eT, fr, el, hfr, head, tail, a, s, b, hnd, hbA, hbB, hh, ht, hsA, ul_q(~V, one, h1, lkT, sd, hsd, hpl, fr, el, hfr, LK.last_or(a, 0), s, b, L.and_right(U32.is_eq(ST.lw(AR.slots(U32, lkT), s, 1n), LK.fst_or(b, 0)), ST.seg(AR.slots(U32, lkT), b, LK.lnk(s), 0), hsS2), hnB, hbB))
193  L.subst(LR.LRU<&2, V>, r => UnlOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, r), LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), LK.fst_or(b, 0))), LR.unlink(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su), Equal.sym(LR.LRU<&2, V>, LR.unlink(&2, V, LR.F{cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, lkT)}, su), LR.ul_fin(&2, V, cap, n, head, tail, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LK.last_or(a, 0), (AR.thaw(U32, lkT), LK.fst_or(b, 0))), E), ok)