Module functions 

Auto-generated module

🤖 Generated with SplitRS

Constants

TRIE_ALPHABET

Functions

adjacency_list_ty

AdjacencyList : Nat → Type 0 — adjacency list graph representation.

adjacency_matrix_ty

AdjacencyMatrix : Nat → Type 0 — adjacency matrix graph representation.

app

app2

app3

arrow

avl_balance_factor

avl_balance_ty

avl_balance_invariant : ∀ (α : Type) (t : AVLTree α), BalanceFactor t ≤ 1

avl_contains

avl_height

avl_insert

avl_rebalance

avl_rotate_left

avl_rotate_right

avl_tree_ty

AVLTree α : Type 0 — AVL self-balancing binary search tree.

avl_update_height

bloom_filter_ds_ty

BloomFilterTy : Nat → Nat → Type 0 — Bloom filter with m bits and k hash functions.

bloom_filter_fpr_ty

BloomFilterFPR : Prop — false positive rate of Bloom filter is (1-e^{-kn/m})^k.

bool_ty

bootstrapped_heap_ty

BootstrappedHeap α : Type 0 — bootstrapped priority queue (Kaplan-Tarjan).

btree_insert_complexity_ty

BTreeInsertComplexity : Prop — B-tree insert runs in O(log_t n) I/Os.

btree_search_complexity_ty

BTreeSearchComplexity : Prop — B-tree search runs in O(log_t n) I/Os.

btree_ty

BTree : Nat → Type 0 — B-tree of order t (min t-1 keys, max 2t-1 keys per node).

buffer_tree_ty

BufferTree : Nat → Type 0 — buffer tree for batched external-memory operations.

build_data_structures_env

Register all data structure axioms into the given kernel environment.

build_extended_ds_env

Register extended data structure axioms into the given kernel environment.

bvar

cache_oblivious_btree_ty

CacheObliviousBTree : Nat → Type 0 — cache-oblivious B-tree.

cache_oblivious_matrix_ty

CacheObliviousMatrix : Nat → Type 0 — cache-oblivious matrix layout (Z-curve).

compressed_suffix_array_ty

CompressedSuffixArray : Nat → Type 0 — compressed suffix array (CSA/FM-index).

consistent_hashing_ty

ConsistentHashing : Nat → Prop — consistent hashing with O(1/n) key redistribution.

count_min_sketch_ty

CountMinSketchTy : Nat → Nat → Type 0 — count-min sketch with w columns, d rows.

crdt_ty

CRDT : Type 0 — conflict-free replicated data type.

cst

deque_ty

Deque α : Type 0 — double-ended queue.

disjoint_set_ty

DisjointSet n : Type 0 — union-find structure over n elements.

distributed_hash_table_ty

DistributedHashTable : Nat → Type 0 — distributed hash table (DHT).

dynamic_graph_ty

DynamicGraph : Nat → Type 0 — dynamic graph supporting edge insertions/deletions.

edge_weighted_graph_ty

EdgeWeightedGraph : Nat → Type 0 — edge-weighted graph.

fat_node_method_ty

FatNodeMethod : Nat → Prop — the fat node method overhead is O(1) per update.

fibonacci_heap_decrease_key_ty

FibonacciHeapDecreaseKey : Prop — decrease-key in Fibonacci heap is O(1) amortized.

fibonacci_heap_ty

FibonacciHeap α : Type 0 — Fibonacci heap with O(1) amortized decrease-key.

finger_tree_ty

FingerTree α : Type 0 — functional finger tree (Hinze-Paterson).

fm_index_ty

FMIndex : Nat → Type 0 — FM-index for compressed string matching.

fractional_cascading_ty

FractionalCascading : Nat → Prop — fractional cascading speedup for range queries.

functional_bst_invariant_ty

FunctionalBSTInvariant : Prop — a functional BST satisfies the BST ordering.

heap_pop_ty

heap_pop_returns_minimum : ∀ (α : Type) (h : Heap α), IsMinimum (pop h) h

heap_push_ty

heap_push_preserves_invariant : ∀ (α : Type) (h : Heap α) (x : α), HeapInvariant (push h x)

heap_ty

Heap α : Type 0 — polymorphic binary min-heap type constructor.

hyperloglog_error_ty

HyperLogLogError : Prop — HyperLogLog relative error is 1.04/sqrt(m).

hyperloglog_ty

HyperLogLogTy : Nat → Type 0 — HyperLogLog cardinality estimator with b-bit registers.

impl_pi

interval_tree_ty

IntervalTree α : Type 0 — interval tree for overlap queries.

kd_tree_nn_complexity_ty

KDTreeNNComplexity : Prop — k-d tree nearest neighbor runs in O(sqrt(n)) expected.

kd_tree_ty

KDTree : Nat → Type 0 — k-d tree for k-dimensional range queries.

linearizability_ty

Linearizability : Prop — concurrent operations are linearizable.

lock_free_stack_ty

LockFreeStack α : Type 0 — lock-free Treiber stack.

nat_ty

pairing_heap_ty

PairingHeap α : Type 0 — pairing heap with O(log n) amortized delete-min.

path_copying_ty

PathCopying : Nat → Prop — path copying persistence for BSTs.

persistence_theorem_ty

PersistenceTheorem : Prop — all versions of a persistent structure coexist.

persistent_array_ty

PersistentArray α n : Type 0 — persistent immutable array.

persistent_queue_ty

PersistentQueue α : Type 0 — persistent queue (Hood-Melville or banker).

persistent_stack_ty

PersistentStack α : Type 0 — persistent (immutable-spine) stack.

pi

priority_queue_ty

PriorityQueue α : Type 0 — priority queue (backed by heap).

prop

range_tree_query_complexity_ty

RangeTreeQueryComplexity : Prop — range tree answers queries in O(log^d n + k).

range_tree_ty

RangeTree : Nat → Type 0 — range tree for orthogonal range queries.

rank_select_axiom_ty

RankSelectAxiom : Prop — rank(i) + select(rank(i)) = i on succinct bit vectors.

real_time_queue_ty

RealTimeQueue α : Type 0 — Hood-Melville real-time O(1) worst-case queue.

red_black_tree_ty

RedBlackTree α : Type 0 — red-black BST (Okasaki functional formulation).

replication_consistency_ty

ReplicationConsistency : Prop — eventual consistency of CRDT merges.

segment_tree_query_ty

segment_tree_query_log : ∀ n, QueryComplexity (segTree n) = O(log n)

segment_tree_ty

SegmentTree α n : Type 0 — segment tree over an array of size n.

skip_list_ty

SkipList α : Type 0 — probabilistic skip list.

splay_tree_amortized_ty

SplayTreeAmortized : Prop — splay tree access lemma and amortized O(log n).

splay_tree_ty

SplayTree α : Type 0 — splay tree with amortized O(log n) per operation.

succinct_bit_vector_ty

SuccinctBitVectorTy : Nat → Type 0 — compact bit vector with rank/select.

suffix_automaton_ty

SuffixAutomaton : Nat → Type 0 — suffix automaton (DAWG).

suffix_tree_linear_time_ty

SuffixTreeLinearTime : Prop — suffix tree can be built in O(n) time.

suffix_tree_ty

SuffixTree : Nat → Type 0 — compressed suffix tree (Ukkonen’s linear construction).

trie_ty

Trie α : Type 0 — trie (prefix tree) indexed by bit strings.

type0

union_find_amortized_ty

union_find_amortized : ∀ n ops, TotalCost (unionFind n) ops = O(ops * α(n))

van_emde_boas_ty

VanEmdeBoasTree n : Type 0 — van Emde Boas tree over universe [0,n).

wait_free_queue_ty

WaitFreeQueue α : Type 0 — wait-free queue (Kogan-Petrank).

wait_freedom_ty

WaitFreedom : Prop — every thread finishes in a bounded number of steps.

wavelet_tree_ty

WaveletTreeTy : Nat → Type 0 — wavelet tree for range queries on sequences.