algebraic-graphs.out

max expr size  =    5
  |- on ineqs  =    4
  |- on conds  =    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 (g1 * g2) == size (g1 + g2)
size (g1 + vertex x) == size (g1 + vertex y)
             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
        g1 + g1 * g2 == g1 * g2
        g1 + g2 * g1 == g2 * g1
            edge x y == vertex x * vertex y
      (g1 + g2) + g3 == g1 + (g2 + g3)
      (g1 * g2) * g3 == g1 * (g2 * g3)
      g1 * (g1 * g2) == g1 * (g1 + g2)
      (g1 + g2) * g1 == g2 * (g1 * g1)

         0 <= size g1
size empty <= size g1
   size g1 <= size (g1 + g2)
     empty <= g1
        g1 <= g1 + g2
        g1 <= g1 * g2
        g1 <= g2 * g1
  vertex 0 <= vertex 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