~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0xa7cf27ec43eaf330fae4f6dc71a5f4aa/LAWS.bend as LAWS

2 imports
import Base
import ./lib.bend as U

Laws

law empty_find_is_singleton provedin PROOF.bendsource · line 4 · raw

{0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.find(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.empty, 7) == 7 : U32}

law new_is_empty provedin PROOF.bendsource · line 7 · raw

{0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.new == 0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.empty : 0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind}

law connected_is_reflexive provedin PROOF.bendsource · line 10 · raw

{0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.connected(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.empty, 7, 7) == True{} : Bool}

law union_connects_arguments provedin PROOF.bendsource · line 13 · raw

{0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.connected(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.union(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.empty, 7, 11), 7, 11) == True{} : Bool}

law union_is_idempotent_for_connection provedin PROOF.bendsource · line 20 · raw

{0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.connected(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.union(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.union(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.empty, 7, 11), 7, 11), 7, 11) == True{} : Bool}

law union_preserves_root_of_first provedin PROOF.bendsource · line 29 · raw

{0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.find(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.union(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.empty, 7, 11), 7) == 7 : U32}

law union_transitive_chain provedin PROOF.bendsource · line 35 · raw

{0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.connected(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.union(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.union(0xa7cf27ec43eaf330fae4f6dc71a5f4aa/lib.UnionFind.empty, 1, 2), 2, 3), 1, 3) == True{} : Bool}