~/bend-docscommunity

proofs/containers/hash_table/state.bend source

proofs/containers/hash_table/state.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/array.bend as ARimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/hash_table.bend as Simport ../../lib/u32div.bend as UDimport ../../../src/containers/hash_table.bend as Himport ./table.bend as TBimport ./buckets.bend as Bimport ./cyc.bend as CYimport ./inv.bend as IVimport ../../lib/nat_list.bend as NLimport ../../lib/words32.bend as W32# The hash map as a Data shadow: its U32 fields, the table and arena# exponents k (2^k buckets) and sd (2^sd slots), and a mirror tree for each# array. real(sh) is the HashMap<&2, V> the implementation holds.type Sh<-V: Data> is Data:  HS{n: U32, k: Nat, td: U32, fresh: U32, sz: U32, sd: Nat, sdU: U32, free: U32, tabT: AR.Tree<U32>, ksT: AR.Tree<String>, vsT: AR.Tree<Maybe<&2, V>>, nxT: AR.Tree<U32>}def real(~V: Data, sh: Sh<V>) -> H.HashMap<&2, V>:  match sh:    case HS{n, k, td, fresh, sz, sd, sdU, free, tabT, ksT, vsT, nxT}:      H.HM{n, CY.msk(k), td, fresh, sz, sdU, free, AR.thaw(U32, tabT), AR.thaw(String, ksT), AR.thaw(Maybe<&2, V>, vsT), AR.thaw(U32, nxT)}# ---- the abstraction ----def some_b(~V: Data, m: Maybe<&2, V>) -> Bool:  match m:    case None{}:      False{}    case Some{v}:      True{}def lvs(~V: Data, vsl: List<&2, Maybe<&2, V>>) -> List<&2, Bool>:  match vsl:    case Nil{}:      Nil{}    case Con{m, t}:      Con{some_b(~V, m), lvs(~V, t)}def nthm(~V: Data, vsl: List<&2, Maybe<&2, V>>, +i: Nat) -> Maybe<&2, V>:  match vsl i:    case Nil{} _:      None{}    case Con{m, t} 0n:      m    case Con{m, t} 1n+p:      nthm(~V, t, p)def ent_m(~V: Data, +k: String, m: Maybe<&2, V>) -> List<&2, S.Entry<V>>:  match m:    case None{}:      Nil{}    case Some{v}:      Con{S.E{k, v}, Nil{}}# the entry of a bucketdef ent(~V: Data, b: B.Bk, +vsl: List<&2, Maybe<&2, V>>) -> List<&2, S.Entry<V>>:  match b:    case B.BE{}:      Nil{}    case B.BF{w, +l, +k}:      ent_m(~V, k, nthm(~V, vsl, UD.v(H.slot(l))))# the entries of buckets j .. j + m - 1, in bucket orderdef absm(~V: Data, +bs: List<&2, B.Bk>, +vsl: List<&2, Maybe<&2, V>>, +m: Nat, +j: Nat) -> List<&2, S.Entry<V>>:  match m:    case 0n:      Nil{}    case 1n+p:      SC.append(S.Entry<V>, ent(~V, B.at(bs, j), vsl), absm(~V, bs, vsl, p, 1n+j))def bsof(~V: Data, sh: Sh<V>) -> List<&2, B.Bk>:  match sh:    case HS{n, +k, td, fresh, sz, sd, sdU, free, +tabT, +ksT, vsT, nxT}:      TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k))def model(~V: Data, sh: Sh<V>) -> List<&2, S.Entry<V>>:  match sh:    case HS{n, +k, td, fresh, sz, sd, sdU, free, +tabT, +ksT, +vsT, nxT}:      absm(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), SC.pow2(k), 0n)# ---- the invariant ----# stated over the stored keys' slot list kl and their tree's perfectness pk,# so that a read that swaps a key out and back keeps it# no full bucket among the first m uses slot sdef noslot(+bs: List<&2, B.Bk>, +s: Nat, +m: Nat) -> Bool:  match m:    case 0n:      True{}    case 1n+j:      Bool.and(Bool.not(Bool.and(B.occ(B.at(bs, j)), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), s))), noslot(bs, s, j))# the free list from link f has exactly cnt links: each slot on it is below# fresh, used by no bucket and not repeated, and the list ends after themdef fl_ok(+bs: List<&2, B.Bk>, +nb: Nat, +nxl: List<&2, U32>, +cnt: Nat, +f: U32, +fr: Nat, +seen: List<&2, Nat>) -> Bool:  match cnt:    case 0n:      U32.is_eq(f, 0)    case 1n+p:      Bool.and(Bool.not(U32.is_eq(f, 0)), Bool.and(Bool.and(Nat.is_lt(UD.v(H.slot(f)), fr), Bool.and(noslot(bs, UD.v(H.slot(f)), nb), Bool.not(NL.memn(UD.v(H.slot(f)), seen)))), fl_ok(bs, nb, nxl, p, W32.nth0(nxl, UD.v(H.slot(f))), fr, Con{UD.v(H.slot(f)), seen})))def ck(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(Nat.is_lt(k, 31n), Nat.is_lt(0n, k))def csd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_lt(sd, 32n)def cpt(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  AR.perfect(U32, 1n+k, tabT)def cpk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  pkdef cpv(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  AR.perfect(Maybe<&2, V>, sd, vsT)def cpn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  AR.perfect(U32, sd, nxT)def ctd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_eq(UD.v(td), 1n+k)def csz(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_eq(UD.v(sz), SC.pow2(sd))def csdu(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_eq(UD.v(sdU), sd)def cwell(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), sd}, SC.pow2(k))def cclus(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  B.cluster(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k))def cuniq(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k))}, SC.pow2(k))def cn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_eq(UD.v(n), IV.occn(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k)))def cload(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k))def clive(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  B.all_lt(B.PLive{TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), lvs(~V, AR.slots(Maybe<&2, V>, vsT)), UD.v(fresh)}, SC.pow2(k))def cfresh(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_le(UD.v(fresh), UD.v(sz))def cfree(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(Nat.is_le(UD.v(n), UD.v(fresh)), fl_ok(TB.buckets(AR.slots(U32, tabT), kl, SC.pow2(k)), SC.pow2(k), AR.slots(U32, nxT), Nat.sub(UD.v(fresh), UD.v(n)), free, UD.v(fresh), Nil{}))def csdk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Nat.is_lt(sd, k)def gr16(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr15(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr14(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr13(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr12(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr11(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr10(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr9(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr8(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr7(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr6(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr5(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr4(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr3(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr2(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def gr1(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def goodF(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>) -> Bool:  Bool.and(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT))def good(~V: Data, sh: Sh<V>) -> Bool:  match sh:    case HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:      goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT)def gp1(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), g)def gp2(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp3(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp4(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp5(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp6(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp7(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp8(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp9(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp10(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp11(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp12(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp13(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp14(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp15(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp16(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def gp17(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_right(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_ck(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), g)def g_csd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cpt(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cpk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cpv(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cpn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_ctd(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_csz(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_csdu(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cwell(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cclus(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cuniq(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cn(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cload(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_clive(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cfresh(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_cfree(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_left(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gp16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g))def g_csdk(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +g: {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  gp17(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT, g)# the invariant from its componentsdef good_intro(~V: Data, +n: U32, +k: Nat, +td: U32, +fresh: U32, +sz: U32, +sd: Nat, +sdU: U32, +free: U32, +tabT: AR.Tree<U32>, +kl: List<&2, String>, +pk: Bool, +vsT: AR.Tree<Maybe<&2, V>>, +nxT: AR.Tree<U32>, +h_ck: {ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csd: {csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpt: {cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpk: {cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpv: {cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cpn: {cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_ctd: {ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csz: {csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csdu: {csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cwell: {cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cclus: {cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cuniq: {cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cn: {cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cload: {cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_clive: {clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cfresh: {cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_cfree: {cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}, +h_csdk: {csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}) -> {goodF(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool}:  L.and_intro(ck(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr1(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_ck, L.and_intro(csd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr2(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csd, L.and_intro(cpt(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr3(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpt, L.and_intro(cpk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr4(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpk, L.and_intro(cpv(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr5(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpv, L.and_intro(cpn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr6(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cpn, L.and_intro(ctd(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr7(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_ctd, L.and_intro(csz(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr8(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csz, L.and_intro(csdu(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr9(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_csdu, L.and_intro(cwell(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr10(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cwell, L.and_intro(cclus(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr11(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cclus, L.and_intro(cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr12(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cuniq, L.and_intro(cn(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr13(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cn, L.and_intro(cload(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr14(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cload, L.and_intro(clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr15(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_clive, L.and_intro(cfresh(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), gr16(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cfresh, L.and_intro(cfree(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), csdk(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT), h_cfree, h_csdk)))))))))))))))))# ---- slot values ----def lvs_nth(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +i: Nat) -> {B.nthb(lvs(~V, vsl), i) == some_b(~V, nthm(~V, vsl, i)) : Bool}:  match vsl i:    case Nil{} _:      {==}    case Con{m, t} 0n:      {==}    case Con{m, t} 1n+p:      lvs_nth(~V, t, p)def nthm_some(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}) -> {SC.nth(Maybe<&2, V>, vsl, i) == Some{nthm(~V, vsl, i)} : Maybe<&2, Maybe<&2, V>>}:  match vsl i:    case Nil{} _:      Empty.absurd({SC.nth(Maybe<&2, V>, Nil{}, i) == Some{nthm(~V, Nil{}, i)} : Maybe<&2, Maybe<&2, V>>}, N.lt_zero_absurd(i, h))    case Con{m, t} 0n:      {==}    case Con{m, t} 1n+p:      nthm_some(~V, t, p, h)