~/bend-docscommunity

proofs/containers/hash_table/rebuild.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/rebuild.bend as Rebuild

5 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/array.bend as AR
import ./state.bend as ST
import ../../lib/nat_list.bend as NL

Templates

template good_vs source · line 10 · raw

@-V:Data -> @+n:U32 -> @+k:Nat -> @+td:U32 -> @+fresh:U32 -> @+sz:U32 -> @+sd:Nat -> @+sdU:U32 -> @+free:U32 -> @+tabT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+kl:List<&2, String> -> @+pk:Bool -> @+vsT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+nxT:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<U32> -> @+hg:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.goodF(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT, nxT) == True{} : Bool} -> @+vsT2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, V>> -> @+h_cpv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.cpv(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT2, nxT) == True{} : Bool} -> @+h_clive:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.clive(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT2, nxT) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/hash_table/state.goodF(V, n, k, td, fresh, sz, sd, sdU, free, tabT, kl, pk, vsT2, nxT) == True{} : Bool}