Proof coverage
Browse proof obligations, exact target verification and reported external reproduction.
Weidner semidirect add/multiply: reordering and arbitrary history permutation
Cost: none
Weidner base52 alphabet: exact digit round trip and strict order
Cost: none
Weidner position labels: prefix-free path order separates arbitrary runs
Cost: none
Generated irreversible deletions of one item form a causal antichain
Sequence patches: bounded splice length is original minus deleted plus inserted
Cost: custom
Chunked sequences: concatenation, split round-trip and exact element measure
Cost: custom
Named partial patch replay concatenation law
Cost: none
A remote record's ordinal within a shared source gap is exact
Diff and patch correctness: a minimum-cost edit script reconstructs its target
Cost: edit count
Diff measurement: alignment edit cost equals source plus target length minus twice the keeps
Cost: edit count
Diff measurement: the LCS recurrence returns an attainable maximum common subsequence
Cost: custom
State-based CRDT convergence: equal delivered sets give equal joins despite duplicates
Cost: none
Patch replay: reversing per-operation inverses restores every successful execution
Cost: none
Patch replay: concatenation equals sequential application, including failures
Cost: none