proofs/containers/lru/rmrb.bend source

proofs/containers/lru/rmrb.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../lib/u32alg.bend as Aimport ../../lib/array.bend as ARimport ../../lib/list.bend as LLimport ../../../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/table.bend as TBimport ../hash_table/buckets.bend as Bimport ../hash_table/cyc.bend as CYimport ../hash_table/inv.bend as IVimport ../hash_table/state.bend as HTimport ../hash_table/insm.bend as IMimport ../hash_table/insa.bend as IAimport ../hash_table/tools.bend as TLimport ../hash_table/poplem.bend as PLimport ../hash_table/delmv.bend as DMimport ../hash_table/delw.bend as DWimport ./state.bend as STimport ./lists.bend as LSimport ./dll.bend as DLimport ./trace.bend as TRimport ./unlink.bend as ULimport ./linktail.bend as LTimport ./rebuild.bend as RBimport ./perm.bend as PEimport ./tabsl.bend as TSimport ./elfr.bend as EFimport ../hash_table/insf.bend as IFimport ./idx.bend as IDimport ./touchsh.bend as TSHimport ../../lib/nat_list.bend as NLimport ../../lib/links.bend as LKimport ../../lib/words32.bend as W32import ../../lib/u32_tree.bend as UT# The invariant after a removal: slot s's bucket is deleted from the table,# s is taken off the recency list, its value cell vacated and s pushed on the# free list.# ---- derived facts ----def f_sd(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(3n+sd, 32n) == True{} : Bool}:  TSH.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))def f_mid(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b)))) == True{} : Bool}:  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))def f_ndY(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}:  L.and_left(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), f_mid(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))def f_sn(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.memn(s, SC.append(Nat, a, b)) == False{} : Bool}:  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))), f_mid(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)))def f_sX(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.memn(s, SC.append(Nat, a, Con{s, b})) == True{} : Bool}:  NL.mem_app_r(s, a, Con{s, b}, UL.self_in(s, b))def f_sub(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {IF.subl(SC.append(Nat, a, b), SC.append(Nat, a, Con{s, b})) == True{} : Bool}:  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))))def f_bY(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.sall(~V, ST.PLive{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)}, SC.append(Nat, a, b)) == True{} : Bool}:  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), f_sub(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))def f_ls(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Bool.and(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s)) == True{} : Bool}:  LS.sall_mem(~V, ST.PLive{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)}, s, SC.append(Nat, a, Con{s, 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), f_sX(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))def f_s0(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}:  N.lt_le_trans(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), L.and_left(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s), f_ls(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), 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))def f_sf(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.memn(s, fl) == False{} : Bool}:  L.not_true(NL.memn(s, fl), TR.not_vac(~V, s, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), L.and_right(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s), f_ls(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cfl(~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.memn(s, fl), {==}))def f_su(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(UD.v(su), SC.pow2(sd)) == True{} : Bool}:  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), f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))def f_sd32(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(sd, 32n) == True{} : Bool}:  N.lt_trans(sd, 3n+sd, 32n, N.lt_le_trans(sd, 1n+sd, 3n+sd, N.lt_succ(sd), N.le_trans(1n+sd, 2n+sd, 3n+sd, N.le_succ(1n+sd), N.le_succ(2n+sd))), f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))# the vacated value cellsdef f_eu(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})) == SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}) : List<&2, Maybe<&2, V>>}:  Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su), None{}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), AR.upd_slots(Maybe<&2, V>, sd, eT, UD.v(su), None{}, f_su(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), ST.g_cpe(~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(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), z, None{}), UD.v(su), s, hsv))# the free-list pushdef f_lu(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)) == TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}) : List<&2, U32>}:  +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, f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), f_su(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), Equal.cong(Nat, Nat, z => ST.off(z, 1n), UD.v(su), s, hsv))  Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.update(U32, AR.slots(U32, t2), ST.off(s, 1n), free), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), UL.wr_s(t2, sd, hp2, LR.nidx(su), s, 1n, {==}, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), iN, free), Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, ST.off(s, 1n), free), AR.slots(U32, t2), TR.app(AR.slots(U32, lkT), tr), hs2))def f_tlo(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {TR.trlo(TR.TW{s, 1n, free, tr}) == True{} : Bool}:  L.and_intro(Nat.is_lt(1n, 2n), TR.trlo(tr), {==}, hlo)def f_len(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {SC.length(Nat, SC.append(Nat, a, Con{s, b})) == 1n+SC.length(Nat, SC.append(Nat, a, b)) : Nat}:  Equal.trans(Nat, SC.length(Nat, SC.append(Nat, a, Con{s, b})), Nat.add(SC.length(Nat, a), 1n+SC.length(Nat, b)), 1n+SC.length(Nat, SC.append(Nat, a, b)), LL.length_append(Nat, a, Con{s, b}), Equal.trans(Nat, Nat.add(SC.length(Nat, a), 1n+SC.length(Nat, b)), 1n+Nat.add(SC.length(Nat, a), SC.length(Nat, b)), 1n+SC.length(Nat, SC.append(Nat, a, b)), N.add_succ(SC.length(Nat, a), SC.length(Nat, b)), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(SC.length(Nat, a), SC.length(Nat, b)), SC.length(Nat, SC.append(Nat, a, b)), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, a, b)), Nat.add(SC.length(Nat, a), SC.length(Nat, b)), LL.length_append(Nat, a, b)))))# the count, one lowerdef f_n(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {UD.v(n) == 1n+SC.length(Nat, SC.append(Nat, a, b)) : Nat}:  Equal.trans(Nat, UD.v(n), SC.length(Nat, SC.append(Nat, a, Con{s, b})), 1n+SC.length(Nat, SC.append(Nat, a, b)), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, a, Con{s, b})), UD.v(n), N.eq_from_is_eq(SC.length(Nat, SC.append(Nat, a, Con{s, b})), UD.v(n), ST.g_clen(~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))), f_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))def f_n1(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {UD.v(U32.sub(n, 1)) == SC.length(Nat, SC.append(Nat, a, b)) : Nat}:  +en = f_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)  +hle = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+SC.length(Nat, SC.append(Nat, a, b)), UD.v(n), Equal.sym(Nat, UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), en), N.lt_succ_le_succ(0n, 1n+SC.length(Nat, SC.append(Nat, a, b)), {==}))  Equal.trans(Nat, UD.v(U32.sub(n, 1)), Nat.sub(UD.v(n), 1n), SC.length(Nat, SC.append(Nat, a, b)), U.sub_nat(n, 1, hle), Equal.trans(Nat, Nat.sub(UD.v(n), 1n), Nat.sub(1n+SC.length(Nat, SC.append(Nat, a, b)), 1n), SC.length(Nat, SC.append(Nat, a, b)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), en), N.sub_zero(SC.length(Nat, SC.append(Nat, a, b)))))# ---- the deleted bucket ----def d1(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {AR.perfect(U32, 1n+k, tabT2) == True{} : Bool}:  L.and_left(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)def d2(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}:  L.and_left(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd))def d3(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}:  L.and_left(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)))def d4(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)) == True{} : Bool}:  L.and_left(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd))))def d5(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)) == True{} : Bool}:  L.and_left(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))), L.and_right(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)))))def d6(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))) == True{} : Bool}:  L.and_right(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))), L.and_right(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)))))def f_blen(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(i, SC.length(B.Bk, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)))) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool}, SC.pow2(k), SC.length(B.Bk, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))), Equal.sym(Nat, SC.length(B.Bk, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))), SC.pow2(k), IA.len_dlist(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k), 0n)), hi)def c_well(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}:  PL.well_from(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k), SC.pow2(k), d4(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), sd, PL.well_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), sd, ST.g_cwell(~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), SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(k), N.le_refl(SC.pow2(k)))def c_n(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(UD.v(U32.sub(n, 1)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}:  +e1 = N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), d6(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))  +e2 = DM.occn_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), hoi)  +e3 = N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), ST.g_cn(~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))  +e4 = Equal.trans(Nat, 1n+SC.length(Nat, SC.append(Nat, a, b)), UD.v(n), 1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), Equal.sym(Nat, UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), f_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), Equal.trans(Nat, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), 1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), e3, e2))  +e5 = Equal.trans(Nat, UD.v(U32.sub(n, 1)), SC.length(Nat, SC.append(Nat, a, b)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), f_n1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, a, b)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), N.succ_inj(SC.length(Nat, SC.append(Nat, a, b)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), e4), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), e1)))  L.subst(Nat, z => {Nat.is_eq(UD.v(U32.sub(n, 1)), z) == True{} : Bool}, UD.v(U32.sub(n, 1)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), e5, N.is_eq_refl(UD.v(U32.sub(n, 1))))def f_n1le(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_le(UD.v(U32.sub(n, 1)), UD.v(n)) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_le(UD.v(U32.sub(n, 1)), z) == True{} : Bool}, 1n+UD.v(U32.sub(n, 1)), UD.v(n), Equal.sym(Nat, UD.v(n), 1n+UD.v(U32.sub(n, 1)), Equal.trans(Nat, UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), 1n+UD.v(U32.sub(n, 1)), f_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), Equal.cong(Nat, Nat, z => 1n+z, SC.length(Nat, SC.append(Nat, a, b)), UD.v(U32.sub(n, 1)), Equal.sym(Nat, UD.v(U32.sub(n, 1)), SC.length(Nat, SC.append(Nat, a, b)), f_n1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))))), N.le_succ(UD.v(U32.sub(n, 1))))def c_load(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_le(Nat.double(UD.v(U32.sub(n, 1))), SC.pow2(k)) == True{} : Bool}:  N.le_trans(Nat.double(UD.v(U32.sub(n, 1))), Nat.double(UD.v(n)), SC.pow2(k), N.double_le(UD.v(U32.sub(n, 1)), UD.v(n), f_n1le(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cload(~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))# ---- the slot correspondence ----def c_bsl(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.pow2(k)) == True{} : Bool}:  +b1 = TS.bsl_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), ST.g_cuniq(~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), i, hi, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), hoi, a, s, b, hsi, AR.slots(U32, lkT), ST.g_cbsl(~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), SC.pow2(k), N.le_refl(SC.pow2(k)))  +b2 = TS.bsl_from(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k), SC.pow2(k), d4(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), SC.append(Nat, a, b), AR.slots(U32, lkT), b1)  +b3 = RB.tr_eq_bool(ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), AR.slots(U32, lkT), SC.pow2(k)), TR.bsl_tr(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), SC.pow2(k)), b2)  L.subst(List<&2, U32>, z => {ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), z, SC.pow2(k)) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), b3)def c_has(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.append(Nat, a, b)) == True{} : Bool}:  +h0 = RB.sall_sub(~V, ST.PHas{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT)}, SC.append(Nat, a, Con{s, b}), SC.append(Nat, a, b), ST.g_chas(~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), f_sub(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))  +h1b = TS.has_rm(~V, one, h1, sd, f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), 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), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), s, hsi, AR.slots(U32, lkT), SC.append(Nat, a, b), f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), f_bY(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), h0)  +h2 = TS.has_to(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), d5(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), AR.slots(U32, lkT), SC.append(Nat, a, b), h1b)  +h3 = RB.tr_eq_bool(ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), SC.append(Nat, a, b)), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), SC.append(Nat, a, b)), TR.has_tr(~V, AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.append(Nat, a, b)), h2)  L.subst(List<&2, U32>, z => {ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), z, SC.append(Nat, a, b)) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), h3)# ---- lists ----def c_sl(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}))) == True{} : Bool}:  L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), f_eu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), RB.tr_eq_bool(ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{})), ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), EF.slok_el(~V, AR.slots(Maybe<&2, V>, eT), s, None{}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.append(Nat, a, b), f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), f_bY(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)))def c_len(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(SC.length(Nat, SC.append(Nat, a, b)), UD.v(U32.sub(n, 1))) == True{} : Bool}:  L.subst(Nat, z => {Nat.is_eq(SC.length(Nat, SC.append(Nat, a, b)), z) == True{} : Bool}, SC.length(Nat, SC.append(Nat, a, b)), UD.v(U32.sub(n, 1)), Equal.sym(Nat, UD.v(U32.sub(n, 1)), SC.length(Nat, SC.append(Nat, a, b)), f_n1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), N.is_eq_refl(SC.length(Nat, SC.append(Nat, a, b))))def c_dll(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.append(Nat, a, b), 0, 0) == True{} : Bool}:  +e = Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, ST.off(s, 1n), free), AR.slots(U32, t2), TR.app(AR.slots(U32, lkT), tr), hs2)  +l1 = RB.tr_eq_bool(ST.seg(SC.update(U32, AR.slots(U32, t2), ST.off(s, 1n), free), SC.append(Nat, a, b), 0, 0), ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0), DL.seg_fs(AR.slots(U32, t2), s, 1n, free, {==}, SC.append(Nat, a, b), 0, 0, f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), hseg)  L.subst(List<&2, U32>, z => {ST.seg(z, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), L.subst(List<&2, U32>, z => {ST.seg(z, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, SC.update(U32, AR.slots(U32, t2), ST.off(s, 1n), free), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), e, l1))# the new model's entries are the old ones of a ++ bdef f_es(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)) == ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)) : List<&2, SP.Ent<V>>}:  +e1 = Equal.cong(List<&2, U32>, List<&2, SP.Ent<V>>, z => ST.es(~V, z, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))  +e2 = Equal.cong(List<&2, Maybe<&2, V>>, List<&2, SP.Ent<V>>, z => ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), z, SC.append(Nat, a, b)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), f_eu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))  +e3 = TR.es_tr(~V, AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b))  +e4 = EF.es_el(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s, None{}, SC.append(Nat, a, b), f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))  Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), e1, Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), e2, Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), e3, e4)))def c_keys(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {S.nodup(SP.keys_of(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)))) == True{} : Bool}:  +KA = SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a))  +KB = SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b))  +SK = ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s)  +h1b = L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, SP.keys_of(~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}))), SC.append(String, KA, Con{SK, KB}), PE.keys_x(~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))  +h2 = L.and_left(S.nodup(SC.append(String, KA, KB)), Bool.not(S.mem(SK, SC.append(String, KA, KB))), L.subst(Bool, z => {z == True{} : Bool}, S.nodup(SC.append(String, KA, Con{SK, KB})), Bool.and(S.nodup(SC.append(String, KA, KB)), Bool.not(S.mem(SK, SC.append(String, KA, KB)))), LS.nd_mid_s(KA, SK, KB), h1b))  +ek = Equal.trans(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b))), SP.keys_of(~V, SC.append(SP.Ent<V>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b))), SC.append(String, KA, KB), Equal.cong(List<&2, SP.Ent<V>>, List<&2, String>, z => SP.keys_of(~V, z), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), SC.append(SP.Ent<V>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b)), LS.es_app(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, b)), LS.keys_app(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b)))  +h3 = L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, SC.append(String, KA, KB), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b))), Equal.sym(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b))), SC.append(String, KA, KB), ek), h2)  +ee = f_es(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)  L.subst(List<&2, SP.Ent<V>>, z => {S.nodup(SP.keys_of(~V, z)) == True{} : Bool}, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), Equal.sym(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ee), h3)# ---- the free list ----def c_free(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {U32.is_eq(H.link(su), LK.fst_or(Con{s, fl}, 0)) == True{} : Bool}:  L.subst(U32, z => {U32.is_eq(z, LK.lnk(s)) == True{} : Bool}, LK.lnk(s), H.link(su), Equal.sym(U32, H.link(su), LK.lnk(s), LT.lnk_su(su, s, sd, f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), hsv, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))), LK.u_refl(LK.lnk(s)))def c_fll(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Con{s, fl}) == True{} : Bool}:  +hl = L.subst(Nat, z => {Nat.is_lt(ST.off(s, 1n), z) == True{} : Bool}, SC.length(U32, AR.slots(U32, lkT)), SC.length(U32, TR.app(AR.slots(U32, lkT), tr)), Equal.sym(Nat, SC.length(U32, TR.app(AR.slots(U32, lkT), tr)), SC.length(U32, AR.slots(U32, lkT)), TR.len_tr(AR.slots(U32, lkT), tr)), UL.len_ll(lkT, sd, 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), s, 1n, {==}, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)))  +e0 = Equal.trans(U32, ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), free, LK.fst_or(fl, 0), DL.lw_same(TR.app(AR.slots(U32, lkT), tr), s, 1n, free, {==}, hl), A.eq_of(free, LK.fst_or(fl, 0), ST.g_cfree(~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)))  +h0 = L.subst(U32, z => {U32.is_eq(z, LK.fst_or(fl, 0)) == True{} : Bool}, LK.fst_or(fl, 0), ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), Equal.sym(U32, ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), LK.fst_or(fl, 0), e0), LK.u_refl(LK.fst_or(fl, 0)))  +out = L.and_intro(Bool.not(NL.memn(s, fl)), TR.trout(tr, fl), NL.not_f(NL.memn(s, fl), f_sf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), TR.out_of_in(~V, tr, SC.append(Nat, a, Con{s, b}), fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), hin, 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_cfl(~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)))  +h2 = RB.tr_eq_bool(ST.fll(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), fl), ST.fll(AR.slots(U32, lkT), fl), TR.fll_tr(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), fl, out), ST.g_cfll(~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))  L.subst(List<&2, U32>, z => {ST.fll(z, Con{s, fl}) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), L.and_intro(U32.is_eq(ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), LK.fst_or(fl, 0)), ST.fll(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), fl), h0, h2))def c_fl(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.flok(~V, Con{s, fl}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}))) == True{} : Bool}:  +hlen = UT.len_of(Maybe<&2, V>, sd, eT, ST.g_cpe(~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), s, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))  +hv = Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s), None{}, TL.nthm_upd_same(~V, AR.slots(Maybe<&2, V>, eT), s, None{}, hlen))  +hs = L.and_intro(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s)), L.and_left(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s), f_ls(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), NL.not_f(ST.live(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s), hv))  +hr = RB.tr_eq_bool(ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{})), ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), EF.flok_el(~V, AR.slots(Maybe<&2, V>, eT), s, None{}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), fl, f_sf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cfl(~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))  L.subst(List<&2, Maybe<&2, V>>, z => {ST.flok(~V, Con{s, fl}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), f_eu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), L.and_intro(Bool.and(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s))), ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{})), hs, hr))def c_fnd(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.nodupn(Con{s, fl}) == True{} : Bool}:  L.and_intro(Bool.not(NL.memn(s, fl)), NL.nodupn(fl), NL.not_f(NL.memn(s, fl), f_sf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cfnd(~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 c_fcnt(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(Nat.add(SC.length(Nat, SC.append(Nat, a, b)), SC.length(Nat, Con{s, fl})), UD.v(W32.nth0(AR.slots(U32, mT), 0n))) == True{} : Bool}:  +ly = SC.length(Nat, SC.append(Nat, a, b))  +lf = SC.length(Nat, fl)  +e = Equal.trans(Nat, Nat.add(ly, 1n+lf), 1n+Nat.add(ly, lf), Nat.add(SC.length(Nat, SC.append(Nat, a, Con{s, b})), lf), N.add_succ(ly, lf), Equal.cong(Nat, Nat, z => Nat.add(z, lf), 1n+ly, SC.length(Nat, SC.append(Nat, a, Con{s, b})), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, a, Con{s, b})), 1n+ly, f_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))))  L.subst(Nat, z => {Nat.is_eq(z, UD.v(W32.nth0(AR.slots(U32, mT), 0n))) == True{} : Bool}, Nat.add(SC.length(Nat, SC.append(Nat, a, Con{s, b})), lf), Nat.add(ly, 1n+lf), Equal.sym(Nat, Nat.add(ly, 1n+lf), Nat.add(SC.length(Nat, SC.append(Nat, a, Con{s, b})), lf), e), ST.g_cfcnt(~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))# THEOREM: the invariant after the removaldef good_rm(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.good(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}) == True{} : Bool}:  +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), None{}, ST.g_cpe(~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))  +pl = UT.uset_p(3n+sd, t2, hp2, UD.v(LR.nidx(su)), free)  ST.good_intro(~V, cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), 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, tabT2, AR.slots(String, ksT), AR.perfect(String, sd, ksT), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}, 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), d1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), ST.g_cpk(~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, pl, ST.g_cpm(~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_cmask(~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_cbits(~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_csize(~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_cdepth(~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_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), c_well(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), d2(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), d3(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_load(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), ST.g_ccap(~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), c_bsl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_has(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_sl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), f_ndY(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), LK.u_refl(LK.fst_or(SC.append(Nat, a, b), 0)), LK.u_refl(LK.last_or(SC.append(Nat, a, b), 0)), c_dll(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_keys(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_free(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fll(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fnd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fcnt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))# THEOREM: the model after the removal is the specification's drop of keydef model_rm(~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}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> {ST.model(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}) == SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), 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), ST.ctr(AR.slots(U32, mT))} : SP.Lru<V>}:  +e = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), 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), f_es(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), Equal.sym(List<&2, SP.Ent<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), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), EF.spec_drop(~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, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), 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), e)