proofs/containers/lru/rmrb.bend

bend-collections-laws-containers@1.0.0.0 · 233 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as A
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
10import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
12import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
13import bend-collections-laws-containers@1.0.0.0/src/containers/lru.bend as LR
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as IV
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insa.bend as IA
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/tools.bend as TL
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/poplem.bend as PL
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/delmv.bend as DM
24import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/delw.bend as DW
25import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
26import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/lists.bend as LS
27import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/dll.bend as DL
28import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/trace.bend as TR
29import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/unlink.bend as UL
30import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/linktail.bend as LT
31import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/rebuild.bend as RB
32import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/perm.bend as PE
33import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/tabsl.bend as TS
34import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/elfr.bend as EF
35import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insf.bend as IF
36import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/idx.bend as ID
37import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/touchsh.bend as TSH
38import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
39import bend-collections-laws-containers@1.0.0.0/proofs/lib/links.bend as LK
40import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
41import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32_tree.bend as UT
42
43# The invariant after a removal: slot s's bucket is deleted from the table,
44# s is taken off the recency list, its value cell vacated and s pushed on the
45# free list.
46
47
48# ---- derived facts ----
49
50def f_sd(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(3n+sd, 32n) == True{} : Bool}:
51  TSH.sd29(k, sd, L.and_left(Nat.is_lt(k, 30n), Nat.is_lt(0n, k), ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
52
53def f_mid(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b)))) == True{} : Bool}:
54  L.subst(Bool, z => {z == True{} : Bool}, NL.nodupn(SC.append(Nat, a, Con{s, b})), Bool.and(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b)))), NL.nd_mid(a, s, b), ST.g_cnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
55
56def f_ndY(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}:
57  L.and_left(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), f_mid(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
58
59def f_sn(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.memn(s, SC.append(Nat, a, b)) == False{} : Bool}:
60  L.not_true(NL.memn(s, SC.append(Nat, a, b)), L.and_right(NL.nodupn(SC.append(Nat, a, b)), Bool.not(NL.memn(s, SC.append(Nat, a, b))), f_mid(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)))
61
62def f_sX(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.memn(s, SC.append(Nat, a, Con{s, b})) == True{} : Bool}:
63  NL.mem_app_r(s, a, Con{s, b}, UL.self_in(s, b))
64
65def f_sub(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {IF.subl(SC.append(Nat, a, b), SC.append(Nat, a, Con{s, b})) == True{} : Bool}:
66  RB.subl_app(a, b, SC.append(Nat, a, Con{s, b}), RB.subl_ml(a, a, Con{s, b}, RB.subl_refl(a)), RB.subl_mr(b, a, Con{s, b}, IF.subl_cons(b, b, s, RB.subl_refl(b))))
67
68def f_bY(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.sall(~V, ST.PLive{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)}, SC.append(Nat, a, b)) == True{} : Bool}:
69  RB.sall_sub(~V, ST.PLive{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)}, SC.append(Nat, a, Con{s, b}), SC.append(Nat, a, b), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), f_sub(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
70
71def f_ls(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Bool.and(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s)) == True{} : Bool}:
72  LS.sall_mem(~V, ST.PLive{UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)}, s, SC.append(Nat, a, Con{s, b}), ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), f_sX(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
73
74def f_s0(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}:
75  N.lt_le_trans(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.pow2(sd), L.and_left(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s), f_ls(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
76
77def f_sf(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.memn(s, fl) == False{} : Bool}:
78  L.not_true(NL.memn(s, fl), TR.not_vac(~V, s, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), L.and_right(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s), f_ls(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), NL.memn(s, fl), {==}))
79
80def f_su(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(UD.v(su), SC.pow2(sd)) == True{} : Bool}:
81  L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(su), Equal.sym(Nat, UD.v(su), s, hsv), f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
82
83def f_sd32(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(sd, 32n) == True{} : Bool}:
84  N.lt_trans(sd, 3n+sd, 32n, N.lt_le_trans(sd, 1n+sd, 3n+sd, N.lt_succ(sd), N.le_trans(1n+sd, 2n+sd, 3n+sd, N.le_succ(1n+sd), N.le_succ(2n+sd))), f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
85
86# the vacated value cells
87def f_eu(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})) == SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}) : List<&2, Maybe<&2, V>>}:
88  Equal.trans(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), UD.v(su), None{}), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), AR.upd_slots(Maybe<&2, V>, sd, eT, UD.v(su), None{}, f_su(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)), Equal.cong(Nat, List<&2, Maybe<&2, V>>, z => SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), z, None{}), UD.v(su), s, hsv))
89
90# the free-list push
91def f_lu(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)) == TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}) : List<&2, U32>}:
92  +iN = Equal.trans(Nat, UD.v(LR.nidx(su)), ST.off(UD.v(su), 1n), ST.off(s, 1n), ID.w1(one, h1, su, sd, UL.sd3(sd, f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), f_su(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), Equal.cong(Nat, Nat, z => ST.off(z, 1n), UD.v(su), s, hsv))
93  Equal.trans(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.update(U32, AR.slots(U32, t2), ST.off(s, 1n), free), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), UL.wr_s(t2, sd, hp2, LR.nidx(su), s, 1n, {==}, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), iN, free), Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, ST.off(s, 1n), free), AR.slots(U32, t2), TR.app(AR.slots(U32, lkT), tr), hs2))
94
95def f_tlo(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {TR.trlo(TR.TW{s, 1n, free, tr}) == True{} : Bool}:
96  L.and_intro(Nat.is_lt(1n, 2n), TR.trlo(tr), {==}, hlo)
97
98def f_len(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {SC.length(Nat, SC.append(Nat, a, Con{s, b})) == 1n+SC.length(Nat, SC.append(Nat, a, b)) : Nat}:
99  Equal.trans(Nat, SC.length(Nat, SC.append(Nat, a, Con{s, b})), Nat.add(SC.length(Nat, a), 1n+SC.length(Nat, b)), 1n+SC.length(Nat, SC.append(Nat, a, b)), LL.length_append(Nat, a, Con{s, b}), Equal.trans(Nat, Nat.add(SC.length(Nat, a), 1n+SC.length(Nat, b)), 1n+Nat.add(SC.length(Nat, a), SC.length(Nat, b)), 1n+SC.length(Nat, SC.append(Nat, a, b)), N.add_succ(SC.length(Nat, a), SC.length(Nat, b)), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(SC.length(Nat, a), SC.length(Nat, b)), SC.length(Nat, SC.append(Nat, a, b)), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, a, b)), Nat.add(SC.length(Nat, a), SC.length(Nat, b)), LL.length_append(Nat, a, b)))))
100
101# the count, one lower
102def f_n(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {UD.v(n) == 1n+SC.length(Nat, SC.append(Nat, a, b)) : Nat}:
103  Equal.trans(Nat, UD.v(n), SC.length(Nat, SC.append(Nat, a, Con{s, b})), 1n+SC.length(Nat, SC.append(Nat, a, b)), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, a, Con{s, b})), UD.v(n), N.eq_from_is_eq(SC.length(Nat, SC.append(Nat, a, Con{s, b})), UD.v(n), ST.g_clen(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))), f_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
104
105def f_n1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {UD.v(U32.sub(n, 1)) == SC.length(Nat, SC.append(Nat, a, b)) : Nat}:
106  +en = f_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)
107  +hle = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+SC.length(Nat, SC.append(Nat, a, b)), UD.v(n), Equal.sym(Nat, UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), en), N.lt_succ_le_succ(0n, 1n+SC.length(Nat, SC.append(Nat, a, b)), {==}))
108  Equal.trans(Nat, UD.v(U32.sub(n, 1)), Nat.sub(UD.v(n), 1n), SC.length(Nat, SC.append(Nat, a, b)), U.sub_nat(n, 1, hle), Equal.trans(Nat, Nat.sub(UD.v(n), 1n), Nat.sub(1n+SC.length(Nat, SC.append(Nat, a, b)), 1n), SC.length(Nat, SC.append(Nat, a, b)), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), en), N.sub_zero(SC.length(Nat, SC.append(Nat, a, b)))))
109
110# ---- the deleted bucket ----
111
112
113def d1(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {AR.perfect(U32, 1n+k, tabT2) == True{} : Bool}:
114  L.and_left(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)
115def d2(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}:
116  L.and_left(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd))
117def d3(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}:
118  L.and_left(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)))
119def d4(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)) == True{} : Bool}:
120  L.and_left(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd))))
121def d5(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)) == True{} : Bool}:
122  L.and_left(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))), L.and_right(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)))))
123def d6(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))) == True{} : Bool}:
124  L.and_right(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))), L.and_right(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))), L.and_right(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))), L.and_right(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), L.and_right(AR.perfect(U32, 1n+k, tabT2), Bool.and(B.cluster(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), hd)))))
125
126def f_blen(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_lt(i, SC.length(B.Bk, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)))) == True{} : Bool}:
127  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)
128
129def c_well(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}:
130  PL.well_from(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k), SC.pow2(k), d4(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), sd, PL.well_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), sd, ST.g_cwell(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), SC.pow2(k), N.le_refl(SC.pow2(k))), SC.pow2(k), N.le_refl(SC.pow2(k)))
131
132def c_n(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(UD.v(U32.sub(n, 1)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k))) == True{} : Bool}:
133  +e1 = N.eq_from_is_eq(IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), d6(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
134  +e2 = DM.occn_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, hi, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), hoi)
135  +e3 = N.eq_from_is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), ST.g_cn(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
136  +e4 = Equal.trans(Nat, 1n+SC.length(Nat, SC.append(Nat, a, b)), UD.v(n), 1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), Equal.sym(Nat, UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), f_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), Equal.trans(Nat, UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), 1n+IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), e3, e2))
137  +e5 = Equal.trans(Nat, UD.v(U32.sub(n, 1)), SC.length(Nat, SC.append(Nat, a, b)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), f_n1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, a, b)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), N.succ_inj(SC.length(Nat, SC.append(Nat, a, b)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), e4), Equal.sym(Nat, IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k)), e1)))
138  L.subst(Nat, z => {Nat.is_eq(UD.v(U32.sub(n, 1)), z) == True{} : Bool}, UD.v(U32.sub(n, 1)), IV.occn(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k)), e5, N.is_eq_refl(UD.v(U32.sub(n, 1))))
139
140def f_n1le(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_le(UD.v(U32.sub(n, 1)), UD.v(n)) == True{} : Bool}:
141  L.subst(Nat, z => {Nat.is_le(UD.v(U32.sub(n, 1)), z) == True{} : Bool}, 1n+UD.v(U32.sub(n, 1)), UD.v(n), Equal.sym(Nat, UD.v(n), 1n+UD.v(U32.sub(n, 1)), Equal.trans(Nat, UD.v(n), 1n+SC.length(Nat, SC.append(Nat, a, b)), 1n+UD.v(U32.sub(n, 1)), f_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), Equal.cong(Nat, Nat, z => 1n+z, SC.length(Nat, SC.append(Nat, a, b)), UD.v(U32.sub(n, 1)), Equal.sym(Nat, UD.v(U32.sub(n, 1)), SC.length(Nat, SC.append(Nat, a, b)), f_n1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))))), N.le_succ(UD.v(U32.sub(n, 1))))
142
143def c_load(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_le(Nat.double(UD.v(U32.sub(n, 1))), SC.pow2(k)) == True{} : Bool}:
144  N.le_trans(Nat.double(UD.v(U32.sub(n, 1))), Nat.double(UD.v(n)), SC.pow2(k), N.double_le(UD.v(U32.sub(n, 1)), UD.v(n), f_n1le(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cload(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
145
146
147# ---- the slot correspondence ----
148
149def c_bsl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.pow2(k)) == True{} : Bool}:
150  +b1 = TS.bsl_rm(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), ST.g_cuniq(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), i, hi, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), hoi, a, s, b, hsi, AR.slots(U32, lkT), ST.g_cbsl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), SC.pow2(k), N.le_refl(SC.pow2(k)))
151  +b2 = TS.bsl_from(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), SC.pow2(k), SC.pow2(k), d4(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), SC.append(Nat, a, b), AR.slots(U32, lkT), b1)
152  +b3 = RB.tr_eq_bool(ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), SC.pow2(k)), ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), AR.slots(U32, lkT), SC.pow2(k)), TR.bsl_tr(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), SC.pow2(k)), b2)
153  L.subst(List<&2, U32>, z => {ST.bsl(TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.append(Nat, a, b), z, SC.pow2(k)) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), b3)
154
155def c_has(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.append(Nat, a, b)) == True{} : Bool}:
156  +h0 = RB.sall_sub(~V, ST.PHas{TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT)}, SC.append(Nat, a, Con{s, b}), SC.append(Nat, a, b), ST.g_chas(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), f_sub(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
157  +h1b = TS.has_rm(~V, one, h1, sd, f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), i, f_blen(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), s, hsi, AR.slots(U32, lkT), SC.append(Nat, a, b), f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), f_bY(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), h0)
158  +h2 = TS.has_to(~V, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.pow2(k), d5(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), AR.slots(U32, lkT), SC.append(Nat, a, b), h1b)
159  +h3 = RB.tr_eq_bool(ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), SC.append(Nat, a, b)), ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), AR.slots(U32, lkT), SC.append(Nat, a, b)), TR.has_tr(~V, AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), SC.append(Nat, a, b)), h2)
160  L.subst(List<&2, U32>, z => {ST.hasall(~V, TB.buckets(AR.slots(U32, tabT2), AR.slots(String, ksT), SC.pow2(k)), SC.pow2(k), z, SC.append(Nat, a, b)) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), h3)
161
162# ---- lists ----
163
164
165def c_sl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}))) == True{} : Bool}:
166  L.subst(List<&2, Maybe<&2, V>>, z => {ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), f_eu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), RB.tr_eq_bool(ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{})), ST.slok(~V, SC.append(Nat, a, b), UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), EF.slok_el(~V, AR.slots(Maybe<&2, V>, eT), s, None{}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.append(Nat, a, b), f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), f_bY(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)))
167
168def c_len(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(SC.length(Nat, SC.append(Nat, a, b)), UD.v(U32.sub(n, 1))) == True{} : Bool}:
169  L.subst(Nat, z => {Nat.is_eq(SC.length(Nat, SC.append(Nat, a, b)), z) == True{} : Bool}, SC.length(Nat, SC.append(Nat, a, b)), UD.v(U32.sub(n, 1)), Equal.sym(Nat, UD.v(U32.sub(n, 1)), SC.length(Nat, SC.append(Nat, a, b)), f_n1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), N.is_eq_refl(SC.length(Nat, SC.append(Nat, a, b))))
170
171def c_dll(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.seg(AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), SC.append(Nat, a, b), 0, 0) == True{} : Bool}:
172  +e = Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.update(U32, z, ST.off(s, 1n), free), AR.slots(U32, t2), TR.app(AR.slots(U32, lkT), tr), hs2)
173  +l1 = RB.tr_eq_bool(ST.seg(SC.update(U32, AR.slots(U32, t2), ST.off(s, 1n), free), SC.append(Nat, a, b), 0, 0), ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0), DL.seg_fs(AR.slots(U32, t2), s, 1n, free, {==}, SC.append(Nat, a, b), 0, 0, f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), hseg)
174  L.subst(List<&2, U32>, z => {ST.seg(z, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), L.subst(List<&2, U32>, z => {ST.seg(z, SC.append(Nat, a, b), 0, 0) == True{} : Bool}, SC.update(U32, AR.slots(U32, t2), ST.off(s, 1n), free), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), e, l1))
175
176# the new model's entries are the old ones of a ++ b
177def f_es(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)) == ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)) : List<&2, SP.Ent<V>>}:
178  +e1 = Equal.cong(List<&2, U32>, List<&2, SP.Ent<V>>, z => ST.es(~V, z, AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
179  +e2 = Equal.cong(List<&2, Maybe<&2, V>>, List<&2, SP.Ent<V>>, z => ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), z, SC.append(Nat, a, b)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), f_eu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
180  +e3 = TR.es_tr(~V, AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b))
181  +e4 = EF.es_el(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), s, None{}, SC.append(Nat, a, b), f_sn(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
182  Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), e1, Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), e2, Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), e3, e4)))
183
184def c_keys(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {S.nodup(SP.keys_of(~V, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)))) == True{} : Bool}:
185  +KA = SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a))
186  +KB = SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b))
187  +SK = ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s)
188  +h1b = L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b}))), SC.append(String, KA, Con{SK, KB}), PE.keys_x(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, s, b, v, hm), ST.g_ckeys(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
189  +h2 = L.and_left(S.nodup(SC.append(String, KA, KB)), Bool.not(S.mem(SK, SC.append(String, KA, KB))), L.subst(Bool, z => {z == True{} : Bool}, S.nodup(SC.append(String, KA, Con{SK, KB})), Bool.and(S.nodup(SC.append(String, KA, KB)), Bool.not(S.mem(SK, SC.append(String, KA, KB)))), LS.nd_mid_s(KA, SK, KB), h1b))
190  +ek = Equal.trans(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b))), SP.keys_of(~V, SC.append(SP.Ent<V>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b))), SC.append(String, KA, KB), Equal.cong(List<&2, SP.Ent<V>>, List<&2, String>, z => SP.keys_of(~V, z), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), SC.append(SP.Ent<V>, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b)), LS.es_app(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, b)), LS.keys_app(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), b)))
191  +h3 = L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, SC.append(String, KA, KB), SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b))), Equal.sym(List<&2, String>, SP.keys_of(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b))), SC.append(String, KA, KB), ek), h2)
192  +ee = f_es(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)
193  L.subst(List<&2, SP.Ent<V>>, z => {S.nodup(SP.keys_of(~V, z)) == True{} : Bool}, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), Equal.sym(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), ee), h3)
194
195# ---- the free list ----
196
197def c_free(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {U32.is_eq(H.link(su), LK.fst_or(Con{s, fl}, 0)) == True{} : Bool}:
198  L.subst(U32, z => {U32.is_eq(z, LK.lnk(s)) == True{} : Bool}, LK.lnk(s), H.link(su), Equal.sym(U32, H.link(su), LK.lnk(s), LT.lnk_su(su, s, sd, f_sd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), hsv, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))), LK.u_refl(LK.lnk(s)))
199
200def c_fll(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.fll(AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Con{s, fl}) == True{} : Bool}:
201  +hl = L.subst(Nat, z => {Nat.is_lt(ST.off(s, 1n), z) == True{} : Bool}, SC.length(U32, AR.slots(U32, lkT)), SC.length(U32, TR.app(AR.slots(U32, lkT), tr)), Equal.sym(Nat, SC.length(U32, TR.app(AR.slots(U32, lkT), tr)), SC.length(U32, AR.slots(U32, lkT)), TR.len_tr(AR.slots(U32, lkT), tr)), UL.len_ll(lkT, sd, ST.g_cpl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), s, 1n, {==}, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)))
202  +e0 = Equal.trans(U32, ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), free, LK.fst_or(fl, 0), DL.lw_same(TR.app(AR.slots(U32, lkT), tr), s, 1n, free, {==}, hl), A.eq_of(free, LK.fst_or(fl, 0), ST.g_cfree(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)))
203  +h0 = L.subst(U32, z => {U32.is_eq(z, LK.fst_or(fl, 0)) == True{} : Bool}, LK.fst_or(fl, 0), ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), Equal.sym(U32, ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), LK.fst_or(fl, 0), e0), LK.u_refl(LK.fst_or(fl, 0)))
204  +out = L.and_intro(Bool.not(NL.memn(s, fl)), TR.trout(tr, fl), NL.not_f(NL.memn(s, fl), f_sf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), TR.out_of_in(~V, tr, SC.append(Nat, a, Con{s, b}), fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT), hin, ST.g_csl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg)))
205  +h2 = RB.tr_eq_bool(ST.fll(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), fl), ST.fll(AR.slots(U32, lkT), fl), TR.fll_tr(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}, f_tlo(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), fl, out), ST.g_cfll(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
206  L.subst(List<&2, U32>, z => {ST.fll(z, Con{s, fl}) == True{} : Bool}, TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), f_lu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), L.and_intro(U32.is_eq(ST.lw(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), s, 1n), LK.fst_or(fl, 0)), ST.fll(TR.app(AR.slots(U32, lkT), TR.TW{s, 1n, free, tr}), fl), h0, h2))
207
208def c_fl(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.flok(~V, Con{s, fl}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}))) == True{} : Bool}:
209  +hlen = UT.len_of(Maybe<&2, V>, sd, eT, ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), s, f_s0(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
210  +hv = Equal.cong(Maybe<&2, V>, Bool, z => HT.some_b(~V, z), HT.nthm(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s), None{}, TL.nthm_upd_same(~V, AR.slots(Maybe<&2, V>, eT), s, None{}, hlen))
211  +hs = L.and_intro(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s)), L.and_left(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), ST.live(~V, AR.slots(Maybe<&2, V>, eT), s), f_ls(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), NL.not_f(ST.live(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s), hv))
212  +hr = RB.tr_eq_bool(ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{})), ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), AR.slots(Maybe<&2, V>, eT)), EF.flok_el(~V, AR.slots(Maybe<&2, V>, eT), s, None{}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), fl, f_sf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cfl(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
213  L.subst(List<&2, Maybe<&2, V>>, z => {ST.flok(~V, Con{s, fl}, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), z) == True{} : Bool}, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), Equal.sym(List<&2, Maybe<&2, V>>, AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), f_eu(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), L.and_intro(Bool.and(Nat.is_lt(s, UD.v(W32.nth0(AR.slots(U32, mT), 0n))), Bool.not(ST.live(~V, SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{}), s))), ST.flok(~V, fl, UD.v(W32.nth0(AR.slots(U32, mT), 0n)), SC.update(Maybe<&2, V>, AR.slots(Maybe<&2, V>, eT), s, None{})), hs, hr))
214
215def c_fnd(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {NL.nodupn(Con{s, fl}) == True{} : Bool}:
216  L.and_intro(Bool.not(NL.memn(s, fl)), NL.nodupn(fl), NL.not_f(NL.memn(s, fl), f_sf(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm)), ST.g_cfnd(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
217
218def c_fcnt(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {Nat.is_eq(Nat.add(SC.length(Nat, SC.append(Nat, a, b)), SC.length(Nat, Con{s, fl})), UD.v(W32.nth0(AR.slots(U32, mT), 0n))) == True{} : Bool}:
219  +ly = SC.length(Nat, SC.append(Nat, a, b))
220  +lf = SC.length(Nat, fl)
221  +e = Equal.trans(Nat, Nat.add(ly, 1n+lf), 1n+Nat.add(ly, lf), Nat.add(SC.length(Nat, SC.append(Nat, a, Con{s, b})), lf), N.add_succ(ly, lf), Equal.cong(Nat, Nat, z => Nat.add(z, lf), 1n+ly, SC.length(Nat, SC.append(Nat, a, Con{s, b})), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, a, Con{s, b})), 1n+ly, f_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))))
222  L.subst(Nat, z => {Nat.is_eq(z, UD.v(W32.nth0(AR.slots(U32, mT), 0n))) == True{} : Bool}, Nat.add(SC.length(Nat, SC.append(Nat, a, Con{s, b})), lf), Nat.add(ly, 1n+lf), Equal.sym(Nat, Nat.add(ly, 1n+lf), Nat.add(SC.length(Nat, SC.append(Nat, a, Con{s, b})), lf), e), ST.g_cfcnt(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
223
224# THEOREM: the invariant after the removal
225def good_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}) -> {ST.good(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}) == True{} : Bool}:
226  +pe = AR.upd_perfect(Maybe<&2, V>, sd, eT, UD.v(su), None{}, ST.g_cpe(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))
227  +pl = UT.uset_p(3n+sd, t2, hp2, UD.v(LR.nidx(su)), free)
228  ST.good_intro(~V, cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT2, AR.slots(String, ksT), AR.perfect(String, sd, ksT), AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}, ST.g_ck(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_csdk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), d1(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), ST.g_cpk(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), pe, pl, ST.g_cpm(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cmask(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cbits(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_csize(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cdepth(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), ST.g_cfresh(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), c_well(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), d2(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), d3(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_n(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_load(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), ST.g_ccap(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg), c_bsl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_has(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_sl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), f_ndY(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_len(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), LK.u_refl(LK.fst_or(SC.append(Nat, a, b), 0)), LK.u_refl(LK.last_or(SC.append(Nat, a, b), 0)), c_dll(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_keys(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_free(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fll(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fl(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fnd(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), c_fcnt(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm))
229
230# THEOREM: the model after the removal is the specification's drop of key
231def model_rm(~V: Data, +cap: U32, +n: U32, +head: U32, +tail: U32, +free: U32, +mT: AR.Tree<U32>, +k: Nat, +sd: Nat, +tabT: AR.Tree<U32>, +ksT: AR.Tree<String>, +eT: AR.Tree<Maybe<&2, V>>, +lkT: AR.Tree<U32>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +fl: List<&2, Nat>, +hg: {ST.good(~V, ST.LS{cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, SC.append(Nat, a, Con{s, b}), fl}) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)) == True{} : Bool}, +hsi: {UD.v(H.slot(B.lnk(B.at(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i)))) == s : Nat}, +tabT2: AR.Tree<U32>, +hd: {DW.dfin2(AR.slots(String, ksT), k, IM.bupd(TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), i, B.BE{}), tabT2) == True{} : Bool}, +t2: AR.Tree<U32>, +tr: TR.Tr, +hp2: {AR.perfect(U32, 3n+sd, t2) == True{} : Bool}, +hs2: {AR.slots(U32, t2) == TR.app(AR.slots(U32, lkT), tr) : List<&2, U32>}, +hlo: {TR.trlo(tr) == True{} : Bool}, +hin: {TR.trin(tr, SC.append(Nat, a, Con{s, b})) == True{} : Bool}, +hseg: {ST.seg(AR.slots(U32, t2), SC.append(Nat, a, b), 0, 0) == True{} : Bool}, +su: U32, +hsv: {UD.v(su) == s : Nat}, +v: V, +hm: {HT.nthm(~V, AR.slots(Maybe<&2, V>, eT), s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(AR.slots(U32, lkT), AR.slots(String, ksT), s), key) == True{} : Bool}) -> {ST.model(~V, ST.LS{cap, U32.sub(n, 1), LK.fst_or(SC.append(Nat, a, b), 0), LK.last_or(SC.append(Nat, a, b), 0), H.link(su), mT, k, sd, tabT2, ksT, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{}), AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free), SC.append(Nat, a, b), Con{s, fl}}) == SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ST.ctr(AR.slots(U32, mT))} : SP.Lru<V>}:
232  +e = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), f_es(~V, cap, n, head, tail, free, mT, k, sd, tabT, ksT, eT, lkT, a, s, b, fl, hg, one, h1, i, hi, hoi, hsi, tabT2, hd, t2, tr, hp2, hs2, hlo, hin, hseg, su, hsv, v, hm), Equal.sym(List<&2, SP.Ent<V>>, SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, b)), EF.spec_drop(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), a, s, b, v, hm, key, hk, ST.g_ckeys(~V, cap, n, head, tail, free, W32.nth0(AR.slots(U32, mT), 0n), W32.nth0(AR.slots(U32, mT), 1n), W32.nth0(AR.slots(U32, mT), 2n), W32.nth0(AR.slots(U32, mT), 6n), W32.nth0(AR.slots(U32, mT), 7n), AR.perfect(U32, 5n, mT), k, sd, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), eT, lkT, SC.append(Nat, a, Con{s, b}), fl, hg))))
233  Equal.cong(List<&2, SP.Ent<V>>, SP.Lru<V>, z => SP.L{cap, W32.nth0(AR.slots(U32, mT), 3n), ST.w64(AR.slots(U32, mT), 4n), z, ST.ctr(AR.slots(U32, mT))}, ST.es(~V, AR.slots(U32, AR.upd(U32, 3n+sd, t2, UD.v(LR.nidx(su)), free)), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, AR.upd(Maybe<&2, V>, sd, eT, UD.v(su), None{})), SC.append(Nat, a, b)), SP.drop(~V, ST.es(~V, AR.slots(U32, lkT), AR.slots(String, ksT), AR.slots(Maybe<&2, V>, eT), SC.append(Nat, a, Con{s, b})), key), e)