algebraic-graphs-s4.out

max expr size  =    4
max  #-tests   = 1080
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
_ :: Int
_ :: Nat3
_ :: Graph Nat3
0 :: Nat3
0 :: Int
True :: Bool
empty :: Graph Nat3
vertex :: Nat3 -> Graph Nat3
(+) :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
(*) :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
overlay :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
connect :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
edge :: Nat3 -> Nat3 -> Graph Nat3
size :: Graph Nat3 -> Int

size (vertex x) == size empty
size (edge x y) == size (edge z x')
 size (g1 * g2) == size (g1 + g2)
        g1 + g1 == g1
     g1 + empty == g1
     g1 * empty == g1
     empty * g1 == g1
        g1 + g2 == g2 + g1
  overlay g1 g2 == g1 + g2
  connect g1 g2 == g1 * g2

              0 <= size g1
     size empty <= size g1
        size g1 <= size (g1 + g2)
size (edge x x) <= size (g1 + g2)
          empty <= g1
             g1 <= g1 + g2
             g1 <= g1 * g2
             g1 <= g2 * g1
       vertex 0 <= vertex x
       vertex x <= edge x y
       vertex x <= edge y x
       edge x x <= edge x y
       edge x x <= edge y x
        g1 + g2 <= g1 * g2
       edge 0 0 <= edge x y
       edge 0 x <= edge x 0