import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/u32alg.bend as A
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../lib/u32div.bend as UD
import ../../../src/containers/hash_table.bend as H
import ../../../src/containers/lru.bend as LR
import ../hash_table/probe_impl.bend as PI
import ./state.bend as ST
import ./idx.bend as ID
import ./dll.bend as DL
import ./trace.bend as TR
import ./unlink.bend as UL
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/u32_tree.bend as UT

# link_tail: attaching a slot as the newest.


def LtOK(~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, +sl: List<&2, Nat>, +s: Nat, r: LR.LRU<&2, V>) -> Type:
  Sigma<&1, &1, AR.Tree<U32>, t3 => Sigma<&1, &1, TR.Tr, tr => {r == LR.F{cap, n, LK.fst_or(SC.append(Nat, sl, Con{s, Nil{}}), 0), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), AR.thaw(U32, t3)} : LR.LRU<&2, V>} & ({AR.perfect(U32, 3n+sd, t3) == True{} : Bool} & ({AR.slots(U32, t3) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>} & ({TR.trlo(tr) == True{} : Bool} & ({TR.trin(tr, SC.append(Nat, sl, Con{s, Nil{}})) == True{} : Bool} & {ST.seg(AR.slots(U32, t3), SC.append(Nat, sl, Con{s, Nil{}}), 0, 0) == True{} : Bool}))))>>

# the written slots are all in xs, s is not: s is not written
def tr_single(+tr: TR.Tr, +xs: List<&2, Nat>, +s: Nat, +hin: {TR.trin(tr, xs) == True{} : Bool}, +hs: {NL.memn(s, xs) == False{} : Bool}) -> {TR.trout(tr, Con{s, Nil{}}) == True{} : Bool}:
  match tr:
    case TR.TNil{}:
      {==}
    case TR.TW{+y, +o, +v, +t}:
      +hy = L.and_left(NL.memn(y, xs), TR.trin(t, xs), hin)
      +ne = NL.ne_mem(s, y, xs, NL.not_f(NL.memn(s, xs), hs), hy)
      +e = L.subst(Bool, z => {Bool.or(z, False{}) == False{} : Bool}, False{}, Nat.is_eq(s, y), Equal.sym(Bool, Nat.is_eq(s, y), False{}, NL.ne_sym(y, s, ne)), {==})
      L.and_intro(Bool.not(NL.memn(y, Con{s, Nil{}})), TR.trout(t, Con{s, Nil{}}), NL.not_f(NL.memn(y, Con{s, Nil{}}), e), tr_single(t, xs, s, L.and_right(NL.memn(y, xs), TR.trin(t, xs), hin), hs))

def hd2(~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}, +sl: List<&2, Nat>, +s: Nat, +head: U32, +hh: {U32.is_eq(head, LK.fst_or(sl, 0)) == True{} : Bool}, +hb: {ST.sall(~V, ST.PLive{fr, el}, sl) == True{} : Bool}) -> {LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head) == LK.fst_or(SC.append(Nat, sl, Con{s, Nil{}}), 0) : U32}:
  match sl:
    case Nil{}:
      {==}
    case Con{+a0, +a2}:
      +z = NL.lastn(a2, a0)
      +hz = UL.bnd_of(~V, z, Con{a0, a2}, fr, el, sd, hfr, hb, NL.lastn_mem(a2, a0))
      +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)), UL.lnk_nz(one, h1, z, sd, hsd, hz))
      Equal.trans(U32, LR.pick(U32.is_eq(LK.last_or(a2, LK.lnk(a0)), 0), LK.lnk(s), head), head, LK.lnk(a0), UL.pick_f(U32.is_eq(LK.last_or(a2, LK.lnk(a0)), 0), hc, LK.lnk(s), head), A.eq_of(head, LK.lnk(a0), hh))


def lt_fin(~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, +su: U32, +s: Nat, +sl: List<&2, Nat>, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hsn: {NL.memn(s, sl) == False{} : Bool}, +hnd: {NL.nodupn(sl) == True{} : Bool}, +hb: {ST.sall(~V, ST.PLive{fr, el}, sl) == True{} : Bool}, +hh: {U32.is_eq(head, LK.fst_or(sl, 0)) == True{} : Bool}, +hp2: {AR.perfect(U32, 3n+sd, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)) == True{} : Bool}, +hs2: {AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)) == SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0) : List<&2, U32>}, +hg2: {ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), sl, 0, 0) == True{} : Bool}, st: UL.Step(AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0), sd, sl, 0, LK.lnk(s), LR.set_if(AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0)))) -> LtOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, sl, s, LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0))}):
  match st:
    case Tuple{+t3, Tuple{+tr3, Tuple{+ea3, Tuple{+hp3, Tuple{+hs3, Tuple{+hl3, Tuple{+hi3, hg3}}}}}}}:
      +tr0 = {TR.TW{s, 1n, 0, TR.TW{s, 0n, LK.last_or(sl, 0), TR.TNil{}}} : TR.Tr}
      +tr = TR.tcat(tr3, tr0)
      +hs = Equal.trans(List<&2, U32>, AR.slots(U32, t3), TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), tr3), TR.app(AR.slots(U32, lkT), tr), hs3, Equal.trans(List<&2, U32>, TR.app(AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), tr3), TR.app(TR.app(AR.slots(U32, lkT), tr0), tr3), TR.app(AR.slots(U32, lkT), tr), Equal.cong(List<&2, U32>, List<&2, U32>, z => TR.app(z, tr3), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), TR.app(AR.slots(U32, lkT), tr0), hs2), Equal.sym(List<&2, U32>, TR.app(AR.slots(U32, lkT), tr), TR.app(TR.app(AR.slots(U32, lkT), tr0), tr3), TR.app_cat(AR.slots(U32, lkT), tr3, tr0))))
      +out = tr_single(tr3, sl, s, hi3, hsn)
      +L2 = AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0))
      +len1 = UL.len_ll(lkT, sd, hpl, s, 1n, {==}, hs0)
      +len0 = UL.len_ll(lkT, sd, hpl, s, 0n, {==}, hs0)
      +r0 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 0n), ST.lw(L2, s, 0n), LK.last_or(sl, 0), Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 0n), ST.lw(TR.app(L2, tr3), s, 0n), ST.lw(L2, s, 0n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 0n), AR.slots(U32, t3), TR.app(L2, tr3), hs3), TR.lw_tr(L2, tr3, hl3, s, 0n, {==}, out)), Equal.trans(U32, ST.lw(L2, s, 0n), ST.lw(SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), s, 0n), LK.last_or(sl, 0), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 0n), L2, SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), hs2), Equal.trans(U32, ST.lw(SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), s, 0n), ST.lw(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), s, 0n), LK.last_or(sl, 0), DL.lw_other(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), s, 1n, 0, {==}, s, 0n, {==}, DL.ne_word(s, s, 1n, 0n, {==})), DL.lw_same(AR.slots(U32, lkT), s, 0n, LK.last_or(sl, 0), {==}, len0))))
      +len1b = L.subst(Nat, z => {Nat.is_lt(ST.off(s, 1n), z) == True{} : Bool}, SC.length(U32, AR.slots(U32, lkT)), SC.length(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0))), Equal.sym(Nat, SC.length(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0))), SC.length(U32, AR.slots(U32, lkT)), TR.len_tr(AR.slots(U32, lkT), TR.TW{s, 0n, LK.last_or(sl, 0), TR.TNil{}})), len1)
      +r1 = Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 1n), ST.lw(L2, s, 1n), 0, Equal.trans(U32, ST.lw(AR.slots(U32, t3), s, 1n), ST.lw(TR.app(L2, tr3), s, 1n), ST.lw(L2, s, 1n), Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 1n), AR.slots(U32, t3), TR.app(L2, tr3), hs3), TR.lw_tr(L2, tr3, hl3, s, 1n, {==}, out)), Equal.trans(U32, ST.lw(L2, s, 1n), ST.lw(SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), s, 1n), 0, Equal.cong(List<&2, U32>, U32, z => ST.lw(z, s, 1n), L2, SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), hs2), DL.lw_same(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), s, 1n, 0, {==}, len1b)))
      +hq0 = L.subst(U32, z => {U32.is_eq(z, LK.last_or(sl, 0)) == True{} : Bool}, LK.last_or(sl, 0), ST.lw(AR.slots(U32, t3), s, 0n), Equal.sym(U32, ST.lw(AR.slots(U32, t3), s, 0n), LK.last_or(sl, 0), r0), LK.u_refl(LK.last_or(sl, 0)))
      +hq1 = L.subst(U32, z => {U32.is_eq(z, 0) == True{} : Bool}, 0, ST.lw(AR.slots(U32, t3), s, 1n), Equal.sym(U32, ST.lw(AR.slots(U32, t3), s, 1n), 0, r1), {==})
      +hgs = L.and_intro(U32.is_eq(ST.lw(AR.slots(U32, t3), s, 0n), LK.last_or(sl, 0)), Bool.and(U32.is_eq(ST.lw(AR.slots(U32, t3), s, 1n), 0), True{}), hq0, L.and_intro(U32.is_eq(ST.lw(AR.slots(U32, t3), s, 1n), 0), True{}, hq1, {==}))
      +hg = L.subst(Bool, z => {z == True{} : Bool}, Bool.and(ST.seg(AR.slots(U32, t3), sl, 0, LK.lnk(s)), ST.seg(AR.slots(U32, t3), Con{s, Nil{}}, LK.last_or(sl, 0), 0)), ST.seg(AR.slots(U32, t3), SC.append(Nat, sl, Con{s, Nil{}}), 0, 0), Equal.sym(Bool, ST.seg(AR.slots(U32, t3), SC.append(Nat, sl, Con{s, Nil{}}), 0, 0), Bool.and(ST.seg(AR.slots(U32, t3), sl, 0, LK.lnk(s)), ST.seg(AR.slots(U32, t3), Con{s, Nil{}}, LK.last_or(sl, 0), 0)), DL.seg_app(AR.slots(U32, t3), sl, Con{s, Nil{}}, 0, 0)), L.and_intro(ST.seg(AR.slots(U32, t3), sl, 0, LK.lnk(s)), ST.seg(AR.slots(U32, t3), Con{s, Nil{}}, LK.last_or(sl, 0), 0), hg3, hgs))
      +hin0 = L.and_intro(NL.memn(s, SC.append(Nat, sl, Con{s, Nil{}})), Bool.and(NL.memn(s, SC.append(Nat, sl, Con{s, Nil{}})), True{}), NL.mem_app_r(s, sl, Con{s, Nil{}}, UL.self_in(s, Nil{})), L.and_intro(NL.memn(s, SC.append(Nat, sl, Con{s, Nil{}})), True{}, NL.mem_app_r(s, sl, Con{s, Nil{}}, UL.self_in(s, Nil{})), {==}))
      +hin = TR.in_cat(tr3, tr0, SC.append(Nat, sl, Con{s, Nil{}}), TR.trin_l(tr3, sl, Con{s, Nil{}}, hi3), hin0)
      +ef = UL.f_eq(~V, cap, n, free, mT, tabT, ksT, eT, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.fst_or(SC.append(Nat, sl, Con{s, Nil{}}), 0), LK.lnk(s), LK.lnk(s), t3, LR.set_if(AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0)), hd2(~V, one, h1, sd, hsd, fr, el, hfr, sl, s, head, hh, hb), {==}, ea3)
      (t3, (tr, (ef, (hp3, (hs, (TR.lo_cat(tr3, tr0, hl3, {==}), (hin, hg)))))))


# a slot's U32 is the U32 of its number
def lnk_su(+su: U32, +s: Nat, +sd: Nat, +hsd: {Nat.is_lt(3n+sd, 32n) == True{} : Bool}, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}) -> {H.link(su) == LK.lnk(s) : U32}:
  +hk = N.lt_le(sd, 32n, N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), UL.sd1(sd, hsd)))
  +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)
  +e = Equal.trans(U32, su, U32.from_nat(UD.v(su)), U32.from_nat(s), Equal.sym(U32, U32.from_nat(UD.v(su)), su, PI.from_v(su, sd, hk, hsu)), Equal.cong(Nat, U32, z => U32.from_nat(z), UD.v(su), s, hsv))
  Equal.cong(U32, U32, z => H.link(z), su, U32.from_nat(s), e)

# THEOREM (link_tail): a slot s off the recency list sl becomes its newest:
# the list sl ++ [s] is linked, with its head and tail.
def link_tail_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, +s: Nat, +sl: List<&2, Nat>, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +hsn: {NL.memn(s, sl) == False{} : Bool}, +hseg: {ST.seg(AR.slots(U32, lkT), sl, 0, 0) == True{} : Bool}, +hnd: {NL.nodupn(sl) == True{} : Bool}, +hb: {ST.sall(~V, ST.PLive{fr, el}, sl) == True{} : Bool}, +hh: {U32.is_eq(head, LK.fst_or(sl, 0)) == True{} : Bool}, +ht: {U32.is_eq(tail, LK.last_or(sl, 0)) == True{} : Bool}) -> LtOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, sl, s, LR.link_tail(&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)):
  +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)
  +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, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 0n), UD.v(su), s, hsv))
  +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, UL.sd3(sd, hsd), hsu), Equal.cong(Nat, Nat, z => ST.off(z, 1n), UD.v(su), s, hsv))
  +eL = lnk_su(su, s, sd, hsd, hsv, hs0)
  +etl = A.eq_of(tail, LK.last_or(sl, 0), ht)
  +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.pidx(su)), LK.last_or(sl, 0))
  +p2 = UT.uset_p(3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), p1, UD.v(LR.nidx(su)), 0)
  +a1 = UL.wr(one, h1, lkT, sd, hsd, hpl, LR.pidx(su), s, 0n, {==}, hs0, iP, LK.last_or(sl, 0))
  +a2 = UL.wr(one, h1, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), sd, hsd, p1, LR.nidx(su), s, 1n, {==}, hs0, iN, 0)
  +ea = Equal.trans(Array<U32>, Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), LK.last_or(sl, 0)), LR.nidx(su), 0), Array.set(U32, AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0))), LR.nidx(su), 0), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), Equal.cong(Array<U32>, Array<U32>, z => Array.set(U32, z, LR.nidx(su), 0), Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), LK.last_or(sl, 0)), AR.thaw(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0))), a1), a2)
  +s1 = UL.wr_s(lkT, sd, hpl, LR.pidx(su), s, 0n, {==}, hs0, iP, LK.last_or(sl, 0))
  +s2 = UL.wr_s(AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), sd, p1, LR.nidx(su), s, 1n, {==}, hs0, iN, 0)
  +hs2 = Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), SC.update(U32, AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0))), ST.off(s, 1n), 0), SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), s2, Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, ST.off(s, 1n), 0), AR.slots(U32, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0))), SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), s1))
  +g1 = Equal.trans(Bool, ST.seg(SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), sl, 0, 0), ST.seg(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), sl, 0, 0), ST.seg(AR.slots(U32, lkT), sl, 0, 0), DL.seg_fs(SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), s, 1n, 0, {==}, sl, 0, 0, hsn), DL.seg_fs(AR.slots(U32, lkT), s, 0n, LK.last_or(sl, 0), {==}, sl, 0, 0, hsn))
  +hg2 = L.subst(List<&2, U32>, z => {ST.seg(z, sl, 0, 0) == True{} : Bool}, SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), hs2), Equal.trans(Bool, ST.seg(SC.update(U32, SC.update(U32, AR.slots(U32, lkT), ST.off(s, 0n), LK.last_or(sl, 0)), ST.off(s, 1n), 0), sl, 0, 0), ST.seg(AR.slots(U32, lkT), sl, 0, 0), True{}, g1, hseg))
  ok = lt_fin(~V, one, h1, lkT, sd, hsd, hpl, cap, n, free, mT, tabT, ksT, eT, fr, el, hfr, head, su, s, sl, hsv, hs0, hsn, hnd, hb, hh, p2, hs2, hg2, UL.ul_p(~V, one, h1, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0), sd, hsd, p2, fr, el, hfr, LK.lnk(s), 0, sl, hg2, hnd, hb))
  +E1 = Equal.cong(U32, LR.LRU<&2, V>, z => LR.F{cap, n, LR.pick(U32.is_eq(z, 0), H.link(su), head), H.link(su), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), z), LR.nidx(su), 0), LR.nidx(H.slot(z)), H.link(su), U32.is_eq(z, 0))}, tail, LK.last_or(sl, 0), etl)
  +E2 = Equal.cong(U32, LR.LRU<&2, V>, z => LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), z, head), z, free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), LK.last_or(sl, 0)), LR.nidx(su), 0), LR.nidx(H.slot(LK.last_or(sl, 0))), z, U32.is_eq(LK.last_or(sl, 0), 0))}, H.link(su), LK.lnk(s), eL)
  +E3 = Equal.cong(Array<U32>, LR.LRU<&2, V>, z => LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(z, LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0))}, Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), LK.last_or(sl, 0)), LR.nidx(su), 0), AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), ea)
  +E = Equal.trans(LR.LRU<&2, V>, LR.F{cap, n, LR.pick(U32.is_eq(tail, 0), H.link(su), head), H.link(su), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), tail), LR.nidx(su), 0), LR.nidx(H.slot(tail)), H.link(su), U32.is_eq(tail, 0))}, LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), H.link(su), head), H.link(su), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), LK.last_or(sl, 0)), LR.nidx(su), 0), LR.nidx(H.slot(LK.last_or(sl, 0))), H.link(su), U32.is_eq(LK.last_or(sl, 0), 0))}, LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0))}, E1, Equal.trans(LR.LRU<&2, V>, LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), H.link(su), head), H.link(su), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), LK.last_or(sl, 0)), LR.nidx(su), 0), LR.nidx(H.slot(LK.last_or(sl, 0))), H.link(su), U32.is_eq(LK.last_or(sl, 0), 0))}, LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), LK.last_or(sl, 0)), LR.nidx(su), 0), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0))}, LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0))}, E2, E3))
  L.subst(LR.LRU<&2, V>, r => LtOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, sl, s, r), LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0))}, LR.F{cap, n, LR.pick(U32.is_eq(tail, 0), H.link(su), head), H.link(su), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), tail), LR.nidx(su), 0), LR.nidx(H.slot(tail)), H.link(su), U32.is_eq(tail, 0))}, Equal.sym(LR.LRU<&2, V>, LR.F{cap, n, LR.pick(U32.is_eq(tail, 0), H.link(su), head), H.link(su), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(Array.set(U32, Array.set(U32, AR.thaw(U32, lkT), LR.pidx(su), tail), LR.nidx(su), 0), LR.nidx(H.slot(tail)), H.link(su), U32.is_eq(tail, 0))}, LR.F{cap, n, LR.pick(U32.is_eq(LK.last_or(sl, 0), 0), LK.lnk(s), head), LK.lnk(s), free, AR.thaw(U32, mT), AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, eT), LR.set_if(AR.thaw(U32, AR.upd(U32, 3n+sd, AR.upd(U32, 3n+sd, lkT, UD.v(LR.pidx(su)), LK.last_or(sl, 0)), UD.v(LR.nidx(su)), 0)), LR.nidx(H.slot(LK.last_or(sl, 0))), LK.lnk(s), U32.is_eq(LK.last_or(sl, 0), 0))}, E), ok)