proofs/containers/lru/touchsh.bend source
proofs/containers/lru/touchsh.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32alg.bend as Aimport ../../lib/list.bend as LLimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../../spec/containers/lru.bend as SPimport ../../lib/u32div.bend as UDimport ../../../src/containers/hash_table.bend as Himport ../../../src/containers/lru.bend as LRimport ../hash_table/state.bend as HTimport ./state.bend as STimport ./trace.bend as TRimport ./unlink.bend as ULimport ./linktail.bend as LTimport ./rebuild.bend as RBimport ./touch.bend as TOimport ./perm.bend as PEimport ../hash_table/insf.bend as IFimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32# touch on the shadow: the slot holding key becomes the newest.def TouchOK(~V: Data, +spec: SP.Lru<V>, r: LR.LRU<&2, V>) -> Type: Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : LR.LRU<&2, V>} & ({ST.model(~V, sh2) == spec : SP.Lru<V>} & {ST.good(~V, sh2) == True{} : Bool})>def sd29(+k: Nat, +sd: Nat, +hk: {Nat.is_lt(k, 30n) == True{} : Bool}, +hs: {Nat.is_lt(sd, k) == True{} : Bool}) -> {Nat.is_lt(3n+sd, 32n) == True{} : Bool}: +h1 = N.lt_le_trans(sd, k, 29n, hs, N.lt_succ_le(k, 29n, hk)) N.lt_add_left(sd, 29n, 3n, h1)# the newest slot has nothing after itdef new_nil(~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, +b0: Nat, +b2: List<&2, Nat>, +su: U32, +hsv: {UD.v(su) == s : Nat}, +hs0: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}, +tail: U32, +ht: {U32.is_eq(tail, LK.last_or(SC.append(Nat, a, Con{s, Con{b0, b2}}), 0)) == True{} : Bool}, +hc: {U32.is_eq(H.link(su), tail) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, a, Con{s, Con{b0, b2}})) == True{} : Bool}, +hbB: {ST.sall(~V, ST.PLive{fr, el}, Con{b0, b2}) == True{} : Bool}) -> Empty: +z = NL.lastn(b2, b0) +hz = UL.bnd_of(~V, z, Con{b0, b2}, fr, el, sd, hfr, hbB, NL.lastn_mem(b2, b0)) +et = Equal.trans(U32, tail, LK.last_or(SC.append(Nat, a, Con{s, Con{b0, b2}}), 0), LK.lnk(z), A.eq_of(tail, LK.last_or(SC.append(Nat, a, Con{s, Con{b0, b2}}), 0), ht), Equal.trans(U32, LK.last_or(SC.append(Nat, a, Con{s, Con{b0, b2}}), 0), LK.last_or(b2, LK.lnk(b0)), LK.lnk(z), LK.last_app(a, Con{s, Con{b0, b2}}, 0), LK.last_lnk(b2, b0))) +el2 = Equal.trans(U32, LK.lnk(s), H.link(su), LK.lnk(z), Equal.sym(U32, H.link(su), LK.lnk(s), LT.lnk_su(su, s, sd, hsd, hsv, hs0)), Equal.trans(U32, H.link(su), tail, LK.lnk(z), A.eq_of(H.link(su), tail, hc), et)) +esz = Equal.trans(Nat, s, UD.v(H.slot(LK.lnk(s))), z, Equal.sym(Nat, UD.v(H.slot(LK.lnk(s))), s, UL.ix_o(one, h1, s, sd, hsd, hs0)), Equal.trans(Nat, UD.v(H.slot(LK.lnk(s))), UD.v(H.slot(LK.lnk(z))), z, Equal.cong(U32, Nat, w => UD.v(H.slot(w)), LK.lnk(s), LK.lnk(z), el2), UL.ix_o(one, h1, z, sd, hsd, hz))) +hin = L.subst(Nat, w => {NL.memn(w, Con{b0, b2}) == True{} : Bool}, z, s, Equal.sym(Nat, s, z, esz), NL.lastn_mem(b2, b0)) +hno = L.and_left(Bool.not(NL.memn(s, Con{b0, b2})), NL.nodupn(Con{b0, b2}), NL.nd_r(a, Con{s, Con{b0, b2}}, hnd)) L.false_true(L.subst(Bool, w => {Bool.not(w) == True{} : Bool}, NL.memn(s, Con{b0, b2}), True{}, hin, hno))def es_new(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +t3: AR.Tree<U32>, +tr: TR.Tr, +hsT: {AR.slots(U32, t3) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}) -> {ST.model(~V, ST.LS{cap, n, LK.fst_or(SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), 0), LK.lnk(s), free, mT, k, sd, tabT, ksT, eT, t3, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), fl}) == SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))} : SP.Lru<V>}: +e1 = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), ST.es(~V, TR.app(AR.slots(U32, lkT), tr), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), Equal.cong(List<&2, U32>, List<&2, SP.Ent<V>>, z => ST.es(~V, z, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), AR.slots(U32, t3), TR.app(AR.slots(U32, lkT), tr), hsT), TR.es_tr(~V, AR.slots(U32, lkT), tr, hlo, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}))) +e2 = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, t3), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), e1, Equal.sym(List<&2, SP.Ent<V>>, SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), TO.spec_touch(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, s, b, v, hm, key, hk, ST.g_ckeys(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)))) Equal.cong(List<&2, SP.Ent<V>>, SP.Lru<V>, z => SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, ST.ctr(AR.slots(U32, mT))}, ST.es(~V, AR.slots(U32, t3), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), e2)def tch_l(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +tr1: TR.Tr, +t2: AR.Tree<U32>, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr1) : List<&2, U32>}, +l1: {TR.trlo(tr1) == True{} : Bool}, +i1: {TR.trin(tr1, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, -r: LR.LRU<&2, V>, lt: LT.LtOK(~V, cap, n, free, mT, tabT, ksT, eT, t2, sd, SC.append(Nat, a, b), s, r)) -> TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, r): match lt: case Tuple{+t3, Tuple{+tr2, Tuple{+e2, Tuple{+p3, Tuple{+s3, Tuple{+l2, Tuple{+i2, g3}}}}}}}: +tr = TR.tcat(tr2, tr1) +hsT = Equal.trans(List<&2, U32>, AR.slots(U32, t3), TR.app(AR.slots(U32, t2), tr2), TR.app(AR.slots(U32, lkT), tr), s3, Equal.trans(List<&2, U32>, TR.app(AR.slots(U32, t2), 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, t2), TR.app(AR.slots(U32, lkT), tr1), hs2), 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)))) +hlo = TR.lo_cat(tr2, tr1, l2, l1) +hin = TR.in_cat(tr2, tr1, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), i2, PE.trin_sub(tr1, SC.append(Nat, a, Con{s, b}), SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), i1, PE.sub_xt(a, s, b))) +ht = L.subst(U32, z => {U32.is_eq(LK.lnk(s), z) == True{} : Bool}, LK.lnk(s), LK.last_or(SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), 0), Equal.sym(U32, LK.last_or(SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), 0), LK.lnk(s), LK.last_app(SC.append(Nat, a, b), Con{s, Nil{}}, 0)), LK.u_refl(LK.lnk(s))) +hkeys = PE.keys_xt(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, s, b, v, hm, ST.g_ckeys(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +g = RB.good_lk(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg, LK.fst_or(SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), 0), LK.lnk(s), t3, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), tr, p3, hsT, hlo, hin, g3, LK.u_refl(LK.fst_or(SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), 0)), ht, PE.sub_xt(a, s, b), PE.sub_tx(a, s, b), PE.nd_xt(a, s, b, ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)), PE.len_xt(a, s, b), hkeys) (ST.LS{cap, n, LK.fst_or(SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), 0), LK.lnk(s), free, mT, k, sd, tabT, ksT, eT, t3, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}}), fl}, (e2, (es_new(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, key, hk, v, hm, t3, tr, hsT, hlo), g)))def tch_u(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, -r1: LR.LRU<&2, V>, u: UL.UnlOK(~V, cap, n, free, mT, tabT, ksT, eT, lkT, sd, a, s, b, r1)) -> TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, LR.link_tail(&2, V, r1, su)): match u: case Tuple{+t2, Tuple{+tr1, Tuple{+e1, Tuple{+p2, Tuple{+s2, Tuple{+l1, Tuple{+i1, g2}}}}}}}: +hk2 = ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg) +hsd = sd29(k, sd, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), hk2), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +hfr = ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg) +sab = RB.subl_app(a, b, SC.append(Nat, a, Con{s, b}), RB.subl_ml(a, a, Con{s, b}, RB.subl_refl(a)), RB.subl_mr(b, a, Con{s, b}, IF.subl_cons(b, b, s, RB.subl_refl(b)))) +hbab = RB.sall_sub(~V, ST.PLive{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)}, SC.append(Nat, a, Con{s, b}), SC.append(Nat, a, b), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), sab) +hs0 = UL.bnd_of(~V, s, SC.append(Nat, a, Con{s, b}), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), sd, hfr, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), NL.mem_app_r(s, a, Con{s, b}, UL.self_in(s, b))) +hnm = L.subst(Bool, z => {z == True{} : Bool}, NL.nodupn(SC.append(Nat, a, Con{s, b})), Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b)))), NL.nd_mid(a, s, b), ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +hndab = L.and_left(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), hnm) +hsn = L.not_true(NL.memn(s, SC.append(Nat, a, b)), L.and_right(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), hnm)) lt = LT.link_tail_ok(~V, one, h1, t2, sd, hsd, p2, cap, n, free, mT, tabT, ksT, eT, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), hfr, LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), su, s, SC.append(Nat, a, b), hsv, hs0, hsn, g2, hndab, hbab, LK.u_refl(LK.fst_or(SC.append(Nat, a, b), 0)), LK.u_refl(LK.last_or(SC.append(Nat, a, b), 0))) ok = tch_l(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, key, hk, v, hm, tr1, t2, s2, l1, i1, LR.link_tail(&2, V, 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)}, su), lt) L.subst(LR.LRU<&2, V>, z => TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, LR.link_tail(&2, V, z, su)), 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)}, r1, Equal.sym(LR.LRU<&2, V>, r1, 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)}, e1), ok)def tch_new(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +hc: {U32.is_eq(H.link(su), tail) == True{} : Bool}) -> TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl})): match b: case Nil{}: +e1 = TO.spec_touch(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, s, Nil{}, v, hm, key, hk, ST.g_ckeys(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +e2 = Equal.cong(List<&2, Nat>, List<&2, SP.Ent<V>>, z => ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, z, Con{s, Nil{}})), SC.append(Nat, a, Nil{}), a, LL.append_nil(Nat, a)) +e3 = Equal.sym(List<&2, SP.Ent<V>>, SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), Equal.trans(List<&2, SP.Ent<V>>, SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, SC.append(Nat, a, Nil{}), Con{s, Nil{}})), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), e1, e2)) (ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}, ({==}, (Equal.cong(List<&2, SP.Ent<V>>, SP.Lru<V>, z => SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, ST.ctr(AR.slots(U32, mT))}, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), e3), hg))) case Con{+b0, +b2}: +hsd = sd29(k, sd, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) +hfr = ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg) +hs0 = UL.bnd_of(~V, s, SC.append(Nat, a, Con{s, b}), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), sd, hfr, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), NL.mem_app_r(s, a, Con{s, Con{b0, b2}}, UL.self_in(s, Con{b0, b2}))) +hbB = RB.sall_sub(~V, ST.PLive{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)}, SC.append(Nat, a, Con{s, b}), Con{b0, b2}, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), RB.subl_mr(Con{b0, b2}, a, Con{s, Con{b0, b2}}, IF.subl_cons(Con{b0, b2}, Con{b0, b2}, s, RB.subl_refl(Con{b0, b2})))) Empty.absurd(TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl})), new_nil(~V, one, h1, sd, hsd, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), hfr, a, s, b0, b2, su, hsv, hs0, tail, ST.g_ctail(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), hc, ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), hbB))def tch_c(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +c: Bool, +hc: {U32.is_eq(H.link(su), tail) == c : Bool}) -> TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, LR.touch_go(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}), su, c)): match c: case True{}: tch_new(~V, one, h1, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, su, hsv, key, hk, v, hm, hc) case False{}: +hsd = sd29(k, sd, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)) tch_u(~V, one, h1, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, su, hsv, key, hk, v, hm, LR.unlink(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}), su), UL.unlink_ok(~V, one, h1, lkT, sd, hsd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), cap, n, free, mT, tabT, ksT, eT, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), head, tail, su, a, s, b, hsv, ST.g_cdll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_chead(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_ctail(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)))def touch_sp(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +s: Nat, +su: U32, +hsv: {UD.v(su) == s : Nat}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, sp: NL.Split(s, sl)) -> TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su)): match sp: case Tuple{+a, Tuple{+b, +e}}: +hg2 = L.subst(List<&2, Nat>, z => {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, z, fl}) == True{} : Bool}, sl, SC.append(Nat, a, Con{s, b}), e, hg) L.subst(List<&2, Nat>, z => TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), z), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, z, fl}), su)), SC.append(Nat, a, Con{s, b}), sl, Equal.sym(List<&2, Nat>, sl, SC.append(Nat, a, Con{s, b}), e), tch_c(~V, one, h1, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg2, su, hsv, key, hk, v, hm, U32.is_eq(H.link(su), tail), {==}))# THEOREM (touch): the listed slot s, holding key with value v, becomes the# newest; the model is the specification's drop-and-append of its entry.def touch_sh(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +sl: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}) == True{} : Bool}, +s: Nat, +hmem: {NL.memn(s, sl) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> TouchOK(~V, SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.snoc(~V, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), sl), key), TO.ev(~V, AR.slots(U32, lkT), AR.slots(String, ksT), s, v)), ST.ctr(AR.slots(U32, mT))}, LR.touch(&2, V, ST.real(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl}), su)): touch_sp(~V, one, h1, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, sl, fl, hg, s, su, hsv, key, hk, v, hm, NL.split_mem(s, sl, hmem))