proofs/containers/hash_table/pop.bend source
proofs/containers/hash_table/pop.bend on the hub · documented module
import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/u32.bend as Uimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/math/hash.bend as HSimport ../../../src/containers/hash_table.bend as Himport ./keys.bend as Kimport ./table.bend as TBimport ./buckets.bend as Bimport ./cyc.bend as CYimport ./arr.bend as AXimport ./inv.bend as IVimport ./state.bend as STimport ./lookup.bend as LKimport ./size.bend as SZimport ./speclem.bend as SLimport ./get.bend as Gimport ./insm.bend as IMimport ./insa.bend as IAimport ./insert.bend as ISimport ./rehash.bend as RHimport ./delmv.bend as DMimport ./poplem.bend as PLimport ./delw.bend as DWimport ./probe_impl.bend as PIimport ./probe_all.bend as PAimport ../../lib/nat_list.bend as NLimport ../../lib/words32.bend as W32import ../../lib/links.bend as LKx# pop of a present key: the implementation's result is the specification's# lookup and remove.def PopOK(~V: Data, +sh: ST.Sh<V>, +key: String, r: H.HashMap<&2, V> & Maybe<&2, V>) -> Type: Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.lookup(~V, ST.model(~V, sh), key)) : H.HashMap<&2, V> & Maybe<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & ((@+q: String -> {S.lookup(~V, ST.model(~V, sh2), q) == S.lookup(~V, S.remove(~V, ST.model(~V, sh), key), q) : Maybe<&2, V>}) & {S.size(~V, ST.model(~V, sh2)) == S.size(~V, S.remove(~V, ST.model(~V, sh), key)) : Nat}))># ---- the slot of the removed entry ----def p_hoi(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}: B.hold_occ(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), hk)def p_esl(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == UD.v(H.slot(l)) : Nat}: Equal.cong(U32, Nat, z => UD.v(H.slot(z)), B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl)def p_bf(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {Bool.not(U32.is_eq(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), 0)) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), SC.pow2(sd)) == True{} : Bool} & {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i))))) == True{} : Bool}): G.bf_ok(sd, ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh), key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), B.all_inst(B.PWell{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), i, hi), B.all_inst(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh)}, SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), i, hi), hk)def live_lt(+lv: List<&2, Bool>, +fr: Nat, +b: B.Bk, +h: {B.live_b(lv, fr, b) == True{} : Bool}, +ho: {B.occ(b) == True{} : Bool}) -> {Nat.is_lt(UD.v(H.slot(B.lnk(b))), fr) == True{} : Bool}: match b: case B.BE{}: Empty.absurd({Nat.is_lt(UD.v(H.slot(B.lnk(B.BE{}))), fr) == True{} : Bool}, L.false_true(ho)) case B.BF{w, +l2, k2}: L.and_right(B.nthb(lv, UD.v(H.slot(l2))), Nat.is_lt(UD.v(H.slot(l2)), fr), h)def p_sf(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {Nat.is_lt(UD.v(H.slot(l)), UD.v(fresh)) == True{} : Bool}: L.subst(Nat, z => {Nat.is_lt(z, UD.v(fresh)) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), p_esl(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), live_lt(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh), B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), B.all_inst(B.PLive{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh)}, SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), i, hi), p_hoi(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))def p_hr_c(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, bf: {Bool.not(U32.is_eq(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), 0)) == True{} : Bool} & ({Nat.is_lt(UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), SC.pow2(sd)) == True{} : Bool} & {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i))))) == True{} : Bool})) -> {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool} & ({B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool} & {U32.is_eq(l, 0) == False{} : Bool}): match bf: case Tuple{nz, Tuple{hr0, hlv0}}: +hr = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), p_esl(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), hr0) +hlv = L.subst(Nat, z => {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), z) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), p_esl(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), hlv0) +nz2 = L.subst(U32, z => {Bool.not(U32.is_eq(z, 0)) == True{} : Bool}, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, hl, nz) (hr, (hlv, K.not_true_eq(U32.is_eq(l, 0), nz2)))def p_hr(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}: Pair.fst({Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool} & {U32.is_eq(l, 0) == False{} : Bool}, p_hr_c(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, p_bf(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))def p_hlv(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool}: Pair.fst({B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool}, {U32.is_eq(l, 0) == False{} : Bool}, Pair.snd({Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool} & {U32.is_eq(l, 0) == False{} : Bool}, p_hr_c(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, p_bf(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl))))def p_nz(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {U32.is_eq(l, 0) == False{} : Bool}: Pair.snd({B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool}, {U32.is_eq(l, 0) == False{} : Bool}, Pair.snd({Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, {B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))) == True{} : Bool} & {U32.is_eq(l, 0) == False{} : Bool}, p_hr_c(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, p_bf(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl))))def p_hlen(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {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)# no bucket but i used the removed slotdef ns0_b(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +b: B.Bk, +hb: {B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i) == b : B.Bk}) -> {ST.noslot(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), UD.v(H.slot(l)), SC.pow2(k)) == True{} : Bool}: match b: case B.BE{}: Empty.absurd({ST.noslot(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), UD.v(H.slot(l)), SC.pow2(k)) == True{} : Bool}, L.false_true(L.subst(B.Bk, y => {B.occ(y) == True{} : Bool}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), B.BE{}, hb, p_hoi(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))) case B.BF{+x, +l2, +kb}: +el = Equal.trans(U32, l2, B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)), l, Equal.cong(B.Bk, U32, y => B.lnk(y), B.BF{x, l2, kb}, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), Equal.sym(B.Bk, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), B.BF{x, l2, kb}, hb)), hl) L.subst(U32, z => {ST.noslot(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), UD.v(H.slot(z)), SC.pow2(k)) == True{} : Bool}, l2, l, el, DM.ns_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), x, l2, kb, hb, SC.pow2(k), N.le_refl(SC.pow2(k))))def p_ns0(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {ST.noslot(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), UD.v(H.slot(l)), SC.pow2(k)) == True{} : Bool}: ns0_b(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i), {==})def p_hem(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {Nat.is_lt(IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), SC.pow2(k)) == True{} : Bool}: L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(k)) == True{} : Bool}, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), 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, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), G.load_lt(UD.v(n), SC.pow2(k), N.succ_le_lt(0n, SC.pow2(k), N.pow2_pos(k)), ST.g_cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)))# v n = occn(V0) + 1def p_en(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {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)) : Nat}: 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)), 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, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), DM.occn_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), p_hoi(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))def p_en1(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {UD.v(U32.sub(n, 1)) == IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)) : Nat}: +hle = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), UD.v(n), Equal.sym(Nat, 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)), p_en(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), N.zero_le(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))) Equal.trans(Nat, UD.v(U32.sub(n, 1)), Nat.sub(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)), U.sub_nat(n, 1, hle), Equal.trans(Nat, Nat.sub(UD.v(n), 1n), Nat.sub(1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), 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)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), 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)), p_en(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), N.sub_zero(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))# ---- what the deletion left ----def d1(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {AR.perfect(U32, 1n+k, Tf) == True{} : Bool}: L.and_left(AR.perfect(U32, 1n+k, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {B.cluster(TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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 p_nsf(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {ST.noslot(TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), UD.v(H.slot(l)), SC.pow2(k)) == True{} : Bool}: RH.ns_from(TB.buckets(AR.slots(U32, Tf), 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, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), UD.v(H.slot(l)), p_ns0(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), SC.pow2(k), N.le_refl(SC.pow2(k)))# ---- the key cell ----def DropOK(+K2: AR.Tree<String>, +sd: Nat, +l: U32, +key: String, +bsf: List<&2, B.Bk>, +tbf: List<&2, U32>, +nn: Nat) -> Type: Sigma<&1, &1, AR.Tree<String>, KS3 => {H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))) == AR.thaw(String, KS3) : Array<String>} & ({AR.perfect(String, sd, KS3) == True{} : Bool} & {TB.buckets(tbf, AR.slots(String, KS3), nn) == bsf : List<&2, B.Bk>})>def drop_c(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +c: Bool, +hc: {H.is_short(K.kword(key)) == c : Bool}) -> DropOK(K2, sd, l, key, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), AR.slots(U32, Tf), SC.pow2(k)): match c: case True{}: (K2, (Equal.cong(Bool, Array<String>, b => H.drop_key(AR.thaw(String, K2), H.slot(l), b), H.is_short(K.kword(key)), True{}, hc), (pk2, Equal.cong(List<&2, String>, List<&2, B.Bk>, z => TB.buckets(AR.slots(U32, Tf), z, SC.pow2(k)), AR.slots(String, K2), AR.slots(String, ksT), hsl2)))) case False{}: +hr = p_hr(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl) +est = AR.set(String, sd, K2, H.slot(l), "", TB.nths(AR.slots(String, K2), UD.v(H.slot(l))), ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), hr, AX.nths_of(sd, K2, UD.v(H.slot(l)), hr, pk2), pk2) +esl = Equal.trans(List<&2, String>, AR.slots(String, AR.upd(String, sd, K2, UD.v(H.slot(l)), "")), SC.update(String, AR.slots(String, K2), UD.v(H.slot(l)), ""), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(l)), ""), AR.upd_slots(String, sd, K2, UD.v(H.slot(l)), "", hr, pk2), Equal.cong(List<&2, String>, List<&2, String>, z => SC.update(String, z, UD.v(H.slot(l)), ""), AR.slots(String, K2), AR.slots(String, ksT), hsl2)) (AR.upd(String, sd, K2, UD.v(H.slot(l)), ""), (Equal.trans(Array<String>, H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))), Array.set(String, AR.thaw(String, K2), H.slot(l), ""), AR.thaw(String, AR.upd(String, sd, K2, UD.v(H.slot(l)), "")), Equal.cong(Bool, Array<String>, b => H.drop_key(AR.thaw(String, K2), H.slot(l), b), H.is_short(K.kword(key)), False{}, hc), est), (AR.upd_perfect(String, sd, K2, UD.v(H.slot(l)), "", pk2), Equal.trans(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, AR.upd(String, sd, K2, UD.v(H.slot(l)), "")), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(l)), ""), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), Equal.cong(List<&2, String>, List<&2, B.Bk>, z => TB.buckets(AR.slots(U32, Tf), z, SC.pow2(k)), AR.slots(String, AR.upd(String, sd, K2, UD.v(H.slot(l)), "")), SC.update(String, AR.slots(String, ksT), UD.v(H.slot(l)), ""), esl), PL.bs_key(AR.slots(U32, Tf), AR.slots(String, ksT), UD.v(H.slot(l)), "", SC.pow2(k), p_nsf(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd))))))def p_vs2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})) == SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}) : List<&2, Maybe<&2, V>>}: AR.upd_slots(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}, p_hr(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), ST.g_cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))def p_nx2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)) == SC.update(U32, AR.slots(U32, nxT), UD.v(H.slot(l)), free) : List<&2, U32>}: AR.upd_slots(U32, sd, nxT, UD.v(H.slot(l)), free, p_hr(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))def p_esl2(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {UD.v(H.slot(H.link(H.slot(l)))) == UD.v(H.slot(l)) : Nat}: LKx.slot_link(one, h1, H.slot(l), W32.bound32(one, h1, UD.v(H.slot(l)), sd, N.lt_trans(sd, k, 31n, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))), p_hr(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))def p_live(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}) -> {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{})), UD.v(fresh)}, SC.pow2(k)) == True{} : Bool}: RH.live_from(TB.buckets(AR.slots(U32, Tf), 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, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), ST.lvs(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{})), UD.v(fresh), PL.live_rm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), UD.v(H.slot(l)), p_ns0(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(k), N.le_refl(SC.pow2(k)))def p_le1(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {Nat.is_le(UD.v(U32.sub(n, 1)), UD.v(n)) == True{} : Bool}: L.subst(Nat, z => {Nat.is_le(z, UD.v(n)) == True{} : Bool}, IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), UD.v(U32.sub(n, 1)), Equal.sym(Nat, UD.v(U32.sub(n, 1)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), p_en1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), L.subst(Nat, z => {Nat.is_le(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), z) == True{} : Bool}, 1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), UD.v(n), Equal.sym(Nat, 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)), p_en(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), N.le_succ(IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))# fresh - (n - 1) = (fresh - n) + 1def p_cnt(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {Nat.sub(UD.v(fresh), UD.v(U32.sub(n, 1))) == 1n+Nat.sub(UD.v(fresh), UD.v(n)) : Nat}: +cf = ST.g_cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg) +le0 = L.and_left(Nat.is_le(UD.v(n), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}), cf) +m = IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)) +efr = Equal.trans(Nat, UD.v(fresh), Nat.add(UD.v(n), Nat.sub(UD.v(fresh), UD.v(n))), 1n+Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), Equal.sym(Nat, Nat.add(UD.v(n), Nat.sub(UD.v(fresh), UD.v(n))), UD.v(fresh), N.sub_add(UD.v(fresh), UD.v(n), le0)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.sub(UD.v(fresh), UD.v(n))), UD.v(n), 1n+m, p_en(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl))) Equal.trans(Nat, Nat.sub(UD.v(fresh), UD.v(U32.sub(n, 1))), Nat.sub(1n+Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), m), 1n+Nat.sub(UD.v(fresh), UD.v(n)), Equal.trans(Nat, Nat.sub(UD.v(fresh), UD.v(U32.sub(n, 1))), Nat.sub(UD.v(fresh), m), Nat.sub(1n+Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), m), Equal.cong(Nat, Nat, z => Nat.sub(UD.v(fresh), z), UD.v(U32.sub(n, 1)), m, p_en1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), Equal.cong(Nat, Nat, z => Nat.sub(z, m), UD.v(fresh), 1n+Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), efr)), Equal.trans(Nat, Nat.sub(1n+Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), m), 1n+Nat.sub(Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), m), 1n+Nat.sub(UD.v(fresh), UD.v(n)), N.sub_succ_left(Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), m, N.le_add_right(m, Nat.sub(UD.v(fresh), UD.v(n)))), Equal.cong(Nat, Nat, z => 1n+z, Nat.sub(Nat.add(m, Nat.sub(UD.v(fresh), UD.v(n))), m), Nat.sub(UD.v(fresh), UD.v(n)), N.add_sub_cancel(m, Nat.sub(UD.v(fresh), UD.v(n))))))# THEOREM: the vacated slot heads a valid free listdef p_free(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +KS3: AR.Tree<String>, +pk3: {AR.perfect(String, sd, KS3) == True{} : Bool}, +ebs: {TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)) == TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}) -> {ST.cfree(~V, U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, AR.slots(String, KS3), AR.perfect(String, sd, KS3), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)) == True{} : Bool}: +cf = ST.g_cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg) +le0 = L.and_left(Nat.is_le(UD.v(n), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}), cf) +flo = L.and_right(Nat.is_le(UD.v(n), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}), cf) +le1 = N.le_trans(UD.v(U32.sub(n, 1)), UD.v(n), UD.v(fresh), p_le1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), le0) +hs32 = W32.bound32(one, h1, UD.v(H.slot(l)), sd, N.lt_trans(sd, k, 31n, ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))), p_hr(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)) +a1 = IM.not_f(U32.is_eq(H.link(H.slot(l)), 0), W32.link_nz(one, h1, H.slot(l), hs32)) +a2 = L.subst(Nat, z => {Nat.is_lt(z, UD.v(fresh)) == True{} : Bool}, UD.v(H.slot(l)), UD.v(H.slot(H.link(H.slot(l)))), Equal.sym(Nat, UD.v(H.slot(H.link(H.slot(l)))), UD.v(H.slot(l)), p_esl2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), p_sf(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)) +a3 = L.subst(Nat, z => {ST.noslot(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), z, SC.pow2(k)) == True{} : Bool}, UD.v(H.slot(l)), UD.v(H.slot(H.link(H.slot(l)))), Equal.sym(Nat, UD.v(H.slot(H.link(H.slot(l)))), UD.v(H.slot(l)), p_esl2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), L.subst(List<&2, B.Bk>, z => {ST.noslot(z, UD.v(H.slot(l)), SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs), p_nsf(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd))) +fp0 = PL.fl_pr(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), d4(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), p_hoi(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), AR.slots(U32, nxT), free, Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}, flo) +fp1 = L.subst(Nat, z => {ST.fl_ok(TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.update(U32, AR.slots(U32, nxT), z, free), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Con{z, Nil{}}) == True{} : Bool}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), p_esl(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), fp0) +fp2 = L.subst(List<&2, U32>, z => {ST.fl_ok(TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), z, Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Con{UD.v(H.slot(l)), Nil{}}) == True{} : Bool}, SC.update(U32, AR.slots(U32, nxT), UD.v(H.slot(l)), free), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), SC.update(U32, AR.slots(U32, nxT), UD.v(H.slot(l)), free), p_nx2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), fp1) +fp3 = L.subst(List<&2, B.Bk>, z => {ST.fl_ok(z, SC.pow2(k), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Con{UD.v(H.slot(l)), Nil{}}) == True{} : Bool} , TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs), fp2) +enx = Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), UD.v(H.slot(H.link(H.slot(l))))), W32.nth0(SC.update(U32, AR.slots(U32, nxT), UD.v(H.slot(l)), free), UD.v(H.slot(l))), free, Equal.trans(U32, W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), UD.v(H.slot(H.link(H.slot(l))))), W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), UD.v(H.slot(l))), W32.nth0(SC.update(U32, AR.slots(U32, nxT), UD.v(H.slot(l)), free), UD.v(H.slot(l))), Equal.cong(Nat, U32, z => W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), z), UD.v(H.slot(H.link(H.slot(l)))), UD.v(H.slot(l)), p_esl2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), Equal.cong(List<&2, U32>, U32, z => W32.nth0(z, UD.v(H.slot(l))), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), SC.update(U32, AR.slots(U32, nxT), UD.v(H.slot(l)), free), p_nx2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl))), W32.nth0_upd_same(AR.slots(U32, nxT), UD.v(H.slot(l)), free, IS.len_lt(U32, sd, nxT, ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), UD.v(H.slot(l)), p_hr(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))) +fp4 = L.subst(U32, g => {ST.fl_ok(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), Nat.sub(UD.v(fresh), UD.v(n)), g, UD.v(fresh), Con{UD.v(H.slot(l)), Nil{}}) == True{} : Bool}, free, W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), UD.v(H.slot(H.link(H.slot(l))))), Equal.sym(U32, W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), UD.v(H.slot(H.link(H.slot(l))))), free, enx), fp3) +a5 = L.subst(Nat, z => {ST.fl_ok(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), Nat.sub(UD.v(fresh), UD.v(n)), W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), UD.v(H.slot(H.link(H.slot(l))))), UD.v(fresh), Con{z, Nil{}}) == True{} : Bool}, UD.v(H.slot(l)), UD.v(H.slot(H.link(H.slot(l)))), Equal.sym(Nat, UD.v(H.slot(H.link(H.slot(l)))), UD.v(H.slot(l)), p_esl2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), fp4) +y2 = Bool.and(Nat.is_lt(UD.v(H.slot(H.link(H.slot(l)))), UD.v(fresh)), Bool.and(ST.noslot(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), UD.v(H.slot(H.link(H.slot(l)))), SC.pow2(k)), Bool.not(NL.memn(UD.v(H.slot(H.link(H.slot(l)))), Nil{})))) +tl2 = ST.fl_ok(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), Nat.sub(UD.v(fresh), UD.v(n)), W32.nth0(AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), UD.v(H.slot(H.link(H.slot(l))))), UD.v(fresh), Con{UD.v(H.slot(H.link(H.slot(l)))), Nil{}}) +fl1 = L.and_intro(Bool.not(U32.is_eq(H.link(H.slot(l)), 0)), Bool.and(y2, tl2), a1, L.and_intro(y2, tl2, L.and_intro(Nat.is_lt(UD.v(H.slot(H.link(H.slot(l)))), UD.v(fresh)), Bool.and(ST.noslot(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), UD.v(H.slot(H.link(H.slot(l)))), SC.pow2(k)), Bool.not(NL.memn(UD.v(H.slot(H.link(H.slot(l)))), Nil{}))), a2, L.and_intro(ST.noslot(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), UD.v(H.slot(H.link(H.slot(l)))), SC.pow2(k)), Bool.not(NL.memn(UD.v(H.slot(H.link(H.slot(l)))), Nil{})), a3, {==})), a5)) +fl2 = L.subst(Nat, c => {ST.fl_ok(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), c, H.link(H.slot(l)), UD.v(fresh), Nil{}) == True{} : Bool}, 1n+Nat.sub(UD.v(fresh), UD.v(n)), Nat.sub(UD.v(fresh), UD.v(U32.sub(n, 1))), Equal.sym(Nat, Nat.sub(UD.v(fresh), UD.v(U32.sub(n, 1))), 1n+Nat.sub(UD.v(fresh), UD.v(n)), p_cnt(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), fl1) L.and_intro(Nat.is_le(UD.v(U32.sub(n, 1)), UD.v(fresh)), ST.fl_ok(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), Nat.sub(UD.v(fresh), UD.v(U32.sub(n, 1))), H.link(H.slot(l)), UD.v(fresh), Nil{}), le1, fl2)# ---- the invariant after pop ----def p_good(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +KS3: AR.Tree<String>, +pk3: {AR.perfect(String, sd, KS3) == True{} : Bool}, +ebs: {TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)) == TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}) -> {ST.goodF(~V, U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, AR.slots(String, KS3), AR.perfect(String, sd, KS3), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)) == True{} : Bool}: +cn = IS.eq_is_eq(UD.v(U32.sub(n, 1)), IV.occn(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k)), Equal.trans(Nat, UD.v(U32.sub(n, 1)), 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, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k)), p_en1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), Equal.trans(Nat, 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, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), SC.pow2(k)), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, Tf), 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)), N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd))), Equal.cong(List<&2, B.Bk>, Nat, z => IV.occn(z, SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs))))) +cload = 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), p_le1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), ST.g_cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)) +cl1 = L.subst(List<&2, Maybe<&2, V>>, z => {B.all_lt(B.PLive{TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ST.lvs(~V, z), UD.v(fresh)}, SC.pow2(k)) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), p_vs2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)), p_live(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd)) +clive = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PLive{z, ST.lvs(~V, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}))), UD.v(fresh)}, SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs), cl1) +cwell = L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PWell{z, sd}, SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs), PL.well_from(TB.buckets(AR.slots(U32, Tf), 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, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), sd, PL.well_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), sd, ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(k), N.le_refl(SC.pow2(k)))) ST.good_intro(~V, U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, AR.slots(String, KS3), AR.perfect(String, sd, KS3), AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), d1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), pk3, AR.upd_perfect(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}, ST.g_cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), AR.upd_perfect(U32, sd, nxT, UD.v(H.slot(l)), free, ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), ST.g_ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), cwell, L.subst(List<&2, B.Bk>, z => {B.cluster(z, SC.pow2(k), CY.msk(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs), d2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd)), L.subst(List<&2, B.Bk>, z => {B.all_lt(B.PUniq{z}, SC.pow2(k)) == True{} : Bool} , TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), Equal.sym(List<&2, B.Bk>, TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs), d3(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd)), cn, cload, clive, ST.g_cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), p_free(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, KS3, pk3, ebs), ST.g_csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))# ---- the model after pop ----def p_m1(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +KS3: AR.Tree<String>, +pk3: {AR.perfect(String, sd, KS3) == True{} : Bool}, +ebs: {TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)) == TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}) -> {ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}) == ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n) : List<&2, S.Entry<V>>}: Equal.trans(List<&2, S.Entry<V>>, ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), SC.pow2(k), 0n), ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), Equal.cong(List<&2, B.Bk>, List<&2, S.Entry<V>>, z => ST.absm(~V, z, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), SC.pow2(k), 0n), TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)), TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), ebs), Equal.cong(List<&2, Maybe<&2, V>>, List<&2, S.Entry<V>>, z => ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), z, SC.pow2(k), 0n), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), p_vs2(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))def p_lk_c(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +q: String, +c: Bool, +hc: {S.str_eq(key, q) == c : Bool}) -> {S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), q) == S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q) : Maybe<&2, V>}: match c: case True{}: +pno = RH.pno_from(TB.buckets(AR.slots(U32, Tf), 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, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), q, IM.nohb_pno(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), q, SC.pow2(k), PL.pno_rmq(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), key, hk, q, hc, SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(k), N.le_refl(SC.pow2(k))) Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), q), None{}, S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q), LK.lookup_none(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), q, SC.pow2(k), pno), Equal.sym(Maybe<&2, V>, S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q), None{}, SL.lookup_remove_same(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, q, hc, PL.nodup_model(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))))) case False{}: +lr = L.subst(Nat, z => {S.lookup(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), z, None{}), SC.pow2(k), 0n), q) == S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), q) : Maybe<&2, V>}, UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), p_esl(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), PL.lk_rm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), key, hk, AR.slots(Maybe<&2, V>, vsT), None{}, q, hc)) Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), q), S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q), RH.lookup_copy(~V, TB.buckets(AR.slots(U32, Tf), 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, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), d5(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), d3(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), DM.uq_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), SC.pow2(k), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), SC.pow2(k), N.le_refl(SC.pow2(k))), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), q), Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), q), S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q), lr, Equal.sym(Maybe<&2, V>, S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), q), SL.lookup_remove_other(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, q, hc))))def p_lk(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +KS3: AR.Tree<String>, +pk3: {AR.perfect(String, sd, KS3) == True{} : Bool}, +ebs: {TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)) == TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}, +q: String) -> {S.lookup(~V, ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), q) == S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q) : Maybe<&2, V>}: Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), q), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), q), S.lookup(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), q), Equal.cong(List<&2, S.Entry<V>>, Maybe<&2, V>, z => S.lookup(~V, z, q), ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), p_m1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, KS3, pk3, ebs)), p_lk_c(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, q, S.str_eq(key, q), {==}))def p_lkk(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> {S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key) == ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))) : Maybe<&2, V>}: Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i))))), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), LK.lookup_hit(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), key, SC.pow2(k), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), i, hi, hk), Equal.cong(Nat, Maybe<&2, V>, z => ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), z), UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))), UD.v(H.slot(l)), p_esl(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))def p_sz_m(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +m: Maybe<&2, V>, +hm: {ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))) == m : Maybe<&2, V>}, +hs: {ST.some_b(~V, m) == True{} : Bool}) -> {S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n)) == S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : Nat}: match m: case None{}: Empty.absurd({S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n)) == S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : Nat}, L.false_true(hs)) case Some{+v0}: +e1 = SZ.size_absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), UD.v(fresh), SC.pow2(k), p_live(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd), SC.pow2(k), N.le_refl(SC.pow2(k))) +e2 = N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), 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, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd)) +er = SL.size_remove_old(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, v0, Equal.trans(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), Some{v0}, p_lkk(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), hm)) +e3 = Equal.trans(Nat, 1n+S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)), 1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), er, Equal.trans(Nat, S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)), 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)), SZ.size_absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), SC.pow2(k), N.le_refl(SC.pow2(k))), DM.occn_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, p_hlen(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), p_hoi(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))) Equal.trans(Nat, S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n)), IV.occn(TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), e1, Equal.trans(Nat, IV.occn(TB.buckets(AR.slots(U32, Tf), 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)), S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), e2, Equal.sym(Nat, S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), N.succ_inj(S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), e3))))def p_sz(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +KS3: AR.Tree<String>, +pk3: {AR.perfect(String, sd, KS3) == True{} : Bool}, +ebs: {TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)) == TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}) -> {S.size(~V, ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)})) == S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : Nat}: +hs = Equal.trans(Bool, ST.some_b(~V, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))), True{}, Equal.sym(Bool, B.nthb(ST.lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(H.slot(l))), ST.some_b(~V, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), ST.lvs_nth(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), p_hlv(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)) Equal.trans(Nat, S.size(~V, ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)})), S.size(~V, ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n)), S.size(~V, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), Equal.cong(List<&2, S.Entry<V>>, Nat, z => S.size(~V, z), ST.model(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), ST.absm(~V, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), None{}), SC.pow2(k), 0n), p_m1(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, KS3, pk3, ebs)), p_sz_m(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), {==}, hs))# ---- the implementation's pop of a present key ----def p_eq(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +KS3: AR.Tree<String>, +pk3: {AR.perfect(String, sd, KS3) == True{} : Bool}, +ebs: {TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)) == TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}, +edt: {H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)) == AR.thaw(U32, Tf) : Array<U32>}, +edk: {H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))) == AR.thaw(String, KS3) : Array<String>}) -> {H.pop_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), U32.is_eq(l, 0)) == (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)) : H.HashMap<&2, V> & Maybe<&2, V>}: +hr = p_hr(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl) +len = ST.nthm_some(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)), IS.len_lt(Maybe<&2, V>, sd, vsT, ST.g_cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), UD.v(H.slot(l)), hr)) +esw = AR.swap(Maybe<&2, V>, sd, vsT, H.slot(l), None{}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), hr, len, ST.g_cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)) +enx = AR.set(U32, sd, nxT, H.slot(l), free, W32.nth0(AR.slots(U32, nxT), UD.v(H.slot(l))), ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), hr, W32.nth_some(AR.slots(U32, nxT), UD.v(H.slot(l)), IS.len_lt(U32, sd, nxT, ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), UD.v(H.slot(l)), hr)), ST.g_cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)) +e1 = Equal.cong(Bool, H.HashMap<&2, V> & Maybe<&2, V>, b => H.pop_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), b), U32.is_eq(l, 0), False{}, p_nz(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)) +e2 = Equal.cong(Array<Maybe<&2, V>> & Maybe<&2, V>, H.HashMap<&2, V> & Maybe<&2, V>, r => H.pop_v(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), U32.from_nat(i), H.slot(l), K.kword(key), r), Array.swap(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l), None{}), (AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), esw) +e3 = Equal.cong(Array<U32>, H.HashMap<&2, V> & Maybe<&2, V>, DT => (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), DT, H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free)}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), AR.thaw(U32, Tf), edt) +e4 = Equal.cong(Array<String>, H.HashMap<&2, V> & Maybe<&2, V>, DK => (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), AR.thaw(U32, Tf), DK, AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free)}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))), AR.thaw(String, KS3), edk) +e5 = Equal.cong(Array<U32>, H.HashMap<&2, V> & Maybe<&2, V>, DN => (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), AR.thaw(U32, Tf), AR.thaw(String, KS3), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), DN}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free), AR.thaw(U32, AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)), enx) +e6 = Equal.cong(Maybe<&2, V>, H.HashMap<&2, V> & Maybe<&2, V>, DX => (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), DX), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))), p_lkk(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl))) Equal.trans(H.HashMap<&2, V> & Maybe<&2, V>, H.pop_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), U32.is_eq(l, 0)), H.pop_v(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), U32.from_nat(i), H.slot(l), K.kword(key), Array.swap(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l), None{})), (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), e1, Equal.trans(H.HashMap<&2, V> & Maybe<&2, V>, H.pop_v(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), U32.from_nat(i), H.slot(l), K.kword(key), Array.swap(Maybe<&2, V>, AR.thaw(Maybe<&2, V>, vsT), H.slot(l), None{})), H.pop_v(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(U32, nxT), U32.from_nat(i), H.slot(l), K.kword(key), (AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l))))), (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), e2, Equal.trans(H.HashMap<&2, V> & Maybe<&2, V>, (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)), H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free)}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), AR.thaw(U32, Tf), H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free)}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), e3, Equal.trans(H.HashMap<&2, V> & Maybe<&2, V>, (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), AR.thaw(U32, Tf), H.drop_key(AR.thaw(String, K2), H.slot(l), H.is_short(K.kword(key))), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free)}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), AR.thaw(U32, Tf), AR.thaw(String, KS3), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free)}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), e4, Equal.trans(H.HashMap<&2, V> & Maybe<&2, V>, (H.HM{U32.sub(n, 1), CY.msk(k), td, fresh, sz, sdU, H.link(H.slot(l)), AR.thaw(U32, Tf), AR.thaw(String, KS3), AR.thaw(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{})), Array.set(U32, AR.thaw(U32, nxT), H.slot(l), free)}, ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), ST.nthm(~V, AR.slots(Maybe<&2, V>, vsT), UD.v(H.slot(l)))), (ST.real(~V, ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}), S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key)), e5, e6)))))def ph_drop(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, +Tf: 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{}), Tf) == True{} : Bool}, +edt: {H.del_at(AR.thaw(U32, tabT), CY.msk(k), U32.from_nat(i)) == AR.thaw(U32, Tf) : Array<U32>}, dr: DropOK(K2, sd, l, key, TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)), AR.slots(U32, Tf), SC.pow2(k))) -> PopOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, H.pop_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), U32.is_eq(l, 0))): match dr: case Tuple{+KS3, Tuple{+edk, rest}}: (+pk3, ebs0) = rest +ebs = {ebs0 : {TB.buckets(AR.slots(U32, Tf), AR.slots(String, KS3), SC.pow2(k)) == TB.buckets(AR.slots(U32, Tf), AR.slots(String, ksT), SC.pow2(k)) : List<&2, B.Bk>}} (ST.HS{U32.sub(n, 1), k, td, fresh, sz, sd, sdU, H.link(H.slot(l)), Tf, KS3, AR.upd(Maybe<&2, V>, sd, vsT, UD.v(H.slot(l)), None{}), AR.upd(U32, sd, nxT, UD.v(H.slot(l)), free)}, (p_eq(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, KS3, pk3, ebs, edt, edk), (p_good(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, KS3, pk3, ebs), (q => p_lk(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, KS3, pk3, ebs, q), p_sz(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, KS3, pk3, ebs)))))def ph_del(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}, d: DW.DelAt2(AR.slots(String, ksT), k, tabT, i)) -> PopOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, H.pop_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), U32.is_eq(l, 0))): match d: case Tuple{+Tf, Tuple{+edt, +hd}}: ph_drop(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, edt, drop_c(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, Tf, hd, H.is_short(K.kword(key)), {==}))# THEOREM: popping a key held by bucket i returns its value and removes itdef pop_hit_ok(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +i: Nat, +l: U32, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hk: {B.hold(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hl: {B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == l : U32}) -> PopOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, H.pop_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(i), l, K.kword(key), U32.is_eq(l, 0))): ph_del(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl, DW.del_ok2(k, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), AR.slots(String, ksT), tabT, ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), i, hi, ST.g_cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), p_hoi(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl), p_hem(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl)))# ---- pop of an absent key ----def pop_absent_ok(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +e: Nat, +hno: {B.all_lt(B.PNo{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), key}, SC.pow2(k)) == True{} : Bool}) -> PopOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, H.pop_hit(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, K2), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), U32.from_nat(e), 0, K.kword(key), U32.is_eq(0, 0))): +kl = AR.slots(String, ksT) +pkT = ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg) +hgT = L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, b, vsT, nxT) == True{} : Bool}, AR.perfect(String, sd, ksT), True{}, pkT, hg) +g2 = L.subst(List<&2, String>, z => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, z, AR.perfect(String, sd, K2), vsT, nxT) == True{} : Bool}, kl, AR.slots(String, K2), Equal.sym(List<&2, String>, AR.slots(String, K2), kl, hsl2), L.subst(Bool, b => {ST.goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, b, vsT, nxT) == True{} : Bool}, True{}, AR.perfect(String, sd, K2), Equal.sym(Bool, AR.perfect(String, sd, K2), True{}, pk2), hgT)) +m2 = Equal.cong(List<&2, String>, List<&2, S.Entry<V>>, z => ST.absm(~V, TB.buckets(AR.slots(U32, tabT), z, SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), AR.slots(String, K2), kl, hsl2) +enone = LK.lookup_none(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), key, SC.pow2(k), hno) +erm = SL.remove_none(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key, enone) +mr = Equal.trans(List<&2, S.Entry<V>>, ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), m2, Equal.sym(List<&2, S.Entry<V>>, S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), erm)) (ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}, (Equal.cong(Maybe<&2, V>, H.HashMap<&2, V> & Maybe<&2, V>, x => (ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), x), None{}, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), None{}, enone)), (g2, (q => Equal.cong(List<&2, S.Entry<V>>, Maybe<&2, V>, z => S.lookup(~V, z, q), ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), mr), Equal.cong(List<&2, S.Entry<V>>, Nat, z => S.size(~V, z), ST.model(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, K2, vsT, nxT}), S.remove(~V, ST.absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n), key), mr)))))# ---- pop and del ----def pop_r(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +K2: AR.Tree<String>, +hsl2: {AR.slots(String, K2) == AR.slots(String, ksT) : List<&2, String>}, +pk2: {AR.perfect(String, sd, K2) == True{} : Bool}, +r: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r)) -> PopOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, H.pop_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)))): match r: case B.RHit{+i, +l}: (+hi, rest) = hres (+hk, hl) = rest pop_hit_ok(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, i, l, hi, hk, hl) case B.REnd{+e}: (he, rest) = hres (hz, rest2) = rest (hp, hno) = rest2 pop_absent_ok(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, e, hno)def pop_po(~V: Data, +one: Nat, +h1: {one == 1n : Nat}, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +hg: {ST.good(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}) == True{} : Bool}, +key: String, +r: B.Res, hres: B.ResOK(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), UD.v(HS.bucket(K.kword(key), CY.msk(k))), key, r), po: PA.ProbeOK(tabT, sd, AR.slots(String, ksT), PA.stored(key), K.kword(key), r, H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key))) -> PopOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, H.pop(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key)): match po: case Tuple{+K2, Tuple{+e, rest}}: (+hsl2, pk2) = rest +eq = Equal.cong(H.Found & U32, H.HashMap<&2, V> & Maybe<&2, V>, pr => H.pop_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), pr), H.probe(AR.thaw(U32, tabT), AR.thaw(String, ksT), CY.msk(k), key), (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key)), e) L.subst(H.HashMap<&2, V> & Maybe<&2, V>, rr => PopOK(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}, key, rr), H.pop_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), H.pop(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key), Equal.sym(H.HashMap<&2, V> & Maybe<&2, V>, H.pop(&2, V, ST.real(~V, ST.HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}), key), H.pop_f(&2, V, n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT), (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), PA.stored(key)), K.kword(key))), eq), pop_r(~V, one, h1, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, K2, hsl2, pk2, r, hres))# THEOREM: pop returns the specification's lookup and leaves its removedef pop_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> PopOK(~V, sh, key, H.pop(&2, V, ST.real(~V, sh), key)): match sh: case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}: +kl = AR.slots(String, ksT) +pk = AR.perfect(String, sd, ksT) pop_po(~V, 1n, {==}, n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT, hg, key, B.pf(key, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), UD.v(HS.bucket(K.kword(key), CY.msk(k))))), UD.v(HS.bucket(K.kword(key), CY.msk(k)))), G.res_of(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, hg, key), PA.probe_ok(1n, {==}, k, L.and_left(Nat.is_lt(k, 31n), Nat.is_lt(0n, k), ST.g_ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg)), tabT, ST.g_cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), sd, ST.g_csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), kl, ksT, {==}, ST.g_cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), key))def DelOK(~V: Data, +sh: ST.Sh<V>, +key: String, r: H.HashMap<&2, V>) -> Type: Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : H.HashMap<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & ((@+q: String -> {S.lookup(~V, ST.model(~V, sh2), q) == S.lookup(~V, S.remove(~V, ST.model(~V, sh), key), q) : Maybe<&2, V>}) & {S.size(~V, ST.model(~V, sh2)) == S.size(~V, S.remove(~V, ST.model(~V, sh), key)) : Nat}))>def del_p(~V: Data, +sh: ST.Sh<V>, +key: String, po: PopOK(~V, sh, key, H.pop(&2, V, ST.real(~V, sh), key))) -> DelOK(~V, sh, key, H.del(&2, V, ST.real(~V, sh), key)): match po: case Tuple{+sh2, Tuple{+e, rest}}: (sh2, (Equal.cong(H.HashMap<&2, V> & Maybe<&2, V>, H.HashMap<&2, V>, r => H.del_drop(&2, V, r), H.pop(&2, V, ST.real(~V, sh), key), (ST.real(~V, sh2), S.lookup(~V, ST.model(~V, sh), key)), e), rest))# THEOREM: del leaves the specification's removedef del_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> DelOK(~V, sh, key, H.del(&2, V, ST.real(~V, sh), key)): del_p(~V, sh, key, pop_ok(~V, sh, hg, key))