import Base
import ./lib.bend as U

law empty_find_is_singleton:
  { U.UnionFind.find(U.UnionFind.empty(), 7) == 7 : U32 }

law new_is_empty:
  { U.UnionFind.new() == U.UnionFind.empty() : U.UnionFind }

law connected_is_reflexive:
  { U.UnionFind.connected(U.UnionFind.empty(), 7, 7) == True{} : Bool }

law union_connects_arguments:
  {
    U.UnionFind.connected(U.UnionFind.union(U.UnionFind.empty(), 7, 11), 7, 11)
      == True{}
    : Bool
  }

law union_is_idempotent_for_connection:
  {
    U.UnionFind.connected(
      U.UnionFind.union(U.UnionFind.union(U.UnionFind.empty(), 7, 11), 7, 11),
      7, 11
    ) == True{}
    : Bool
  }

law union_preserves_root_of_first:
  {
    U.UnionFind.find(U.UnionFind.union(U.UnionFind.empty(), 7, 11), 7) == 7
    : U32
  }

law union_transitive_chain:
  {
    U.UnionFind.connected(
      U.UnionFind.union(U.UnionFind.union(U.UnionFind.empty(), 1, 2), 2, 3),
      1, 3
    ) == True{}
    : Bool
  }