1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32alg.bend as A 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../lib/u32div.bend as UD 8 import ../../../src/containers/hash_table.bend as H 9 import ../../../src/containers/lru.bend as LR 10 import ../hash_table/probe_impl.bend as PI 11 import ./state.bend as ST 12 import ./idx.bend as ID 13 import ./dll.bend as DL 14 import ./trace.bend as TR 15 import ./unlink.bend as UL 16 import ../../lib/nat_list.bend as NL 17 import ../../lib/links.bend as LK 18 import ../../lib/u32_tree.bend as UT 19 20 # link_tail: attaching a slot as the newest. 21 22 23 def LtOK(~V: Data, +cap: U32, +n: U32, +free: U32, +mT: AR.Tree, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +lkT: AR.Tree, +sd: Nat, +sl: List<&2, Nat>, +s: Nat, r: LR.LRU<&2, V>) -> Type: 24 Sigma<&1, &1, AR.Tree, 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}))))>> 25 26 # the written slots are all in xs, s is not: s is not written 27 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}: 28 match tr: 29 case TR.TNil{}: 30 {==} 31 case TR.TW{+y, +o, +v, +t}: 32 +hy = L.and_left(NL.memn(y, xs), TR.trin(t, xs), hin) 33 +ne = NL.ne_mem(s, y, xs, NL.not_f(NL.memn(s, xs), hs), hy) 34 +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)), {==}) 35 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)) 36 37 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}: 38 match sl: 39 case Nil{}: 40 {==} 41 case Con{+a0, +a2}: 42 +z = NL.lastn(a2, a0) 43 +hz = UL.bnd_of(~V, z, Con{a0, a2}, fr, el, sd, hfr, hb, NL.lastn_mem(a2, a0)) 44 +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)) 45 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)) 46 47 48 def lt_fin(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree, +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, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +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(L 49 match st: 50 case Tuple{+t3, Tuple{+tr3, Tuple{+ea3, Tuple{+hp3, Tuple{+hs3, Tuple{+hl3, Tuple{+hi3, hg3}}}}}}}: 51 +tr0 = {TR.TW{s, 1n, 0, TR.TW{s, 0n, LK.last_or(sl, 0), TR.TNil{}}} : TR.Tr} 52 +tr = TR.tcat(tr3, tr0) 53 +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)))) 54 +out = tr_single(tr3, sl, s, hi3, hsn) 55 +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)) 56 +len1 = UL.len_ll(lkT, sd, hpl, s, 1n, {==}, hs0) 57 +len0 = UL.len_ll(lkT, sd, hpl, s, 0n, {==}, hs0) 58 +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)))) 59 +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) 60 +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))) 61 +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))) 62 +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), {==}) 63 +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, {==})) 64 +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)) 65 +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{})), {==})) 66 +hin = TR.in_cat(tr3, tr0, SC.append(Nat, sl, Con{s, Nil{}}), TR.trin_l(tr3, sl, Con{s, Nil{}}, hi3), hin0) 67 +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) 68 (t3, (tr, (ef, (hp3, (hs, (TR.lo_cat(tr3, tr0, hl3, {==}), (hin, hg))))))) 69 70 71 # a slot's U32 is the U32 of its number 72 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}: 73 +hk = N.lt_le(sd, 32n, N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), UL.sd1(sd, hsd))) 74 +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) 75 +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)) 76 Equal.cong(U32, U32, z => H.link(z), su, U32.from_nat(s), e) 77 78 # THEOREM (link_tail): a slot s off the recency list sl becomes its newest: 79 # the list sl ++ [s] is linked, with its head and tail. 80 def link_tail_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +lkT: AR.Tree, +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, +tabT: AR.Tree, +ksT: AR.Tree, +eT: AR.Tree>, +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)): 81 +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) 82 +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)) 83 +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)) 84 +eL = lnk_su(su, s, sd, hsd, hsv, hs0) 85 +etl = A.eq_of(tail, LK.last_or(sl, 0), ht) 86 +p1 = UT.uset_p(3n+sd, lkT, hpl, UD.v(LR.pidx(su)), LK.last_or(sl, 0)) 87 +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) 88 +a1 = UL.wr(one, h1, lkT, sd, hsd, hpl, LR.pidx(su), s, 0n, {==}, hs0, iP, LK.last_or(sl, 0)) 89 +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) 90 +ea = Equal.trans(Array, 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, Array, 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) 91 +s1 = UL.wr_s(lkT, sd, hpl, LR.pidx(su), s, 0n, {==}, hs0, iP, LK.last_or(sl, 0)) 92 +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) 93 +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)) 94 +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)) 95 +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)) 96 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)) 97 +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) 98 +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) 99 +E3 = Equal.cong(Array, 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) 100 +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, tab 101 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)