ratio-s4.out

max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   =  500
min  #-tests   =   25  (to consider p ==> q true)
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Integer
_ :: Ratio Integer
id :: Ratio Integer -> Ratio Integer
abs :: Ratio Integer -> Ratio Integer
negate :: Ratio Integer -> Ratio Integer
(+) :: Ratio Integer -> Ratio Integer -> Ratio Integer
(*) :: Ratio Integer -> Ratio Integer -> Ratio Integer
(/) :: Ratio Integer -> Ratio Integer -> Ratio Integer
(%) :: Integer -> Integer -> Ratio Integer
recip :: Ratio Integer -> Ratio Integer
numerator :: Ratio Integer -> Integer
denominator :: Ratio Integer -> Integer
0 % 1 :: Ratio Integer
1 % 1 :: Ratio Integer
0 :: Integer
1 :: Integer

    denominator (abs q) == denominator q
 denominator (negate q) == denominator q
      numerator (x % 1) == x
    denominator (x % 1) == 1
denominator (q + 1 % 1) == denominator q
                   id q == q
      negate (negate q) == q
              q + 0 % 1 == q
            q * (1 % 1) == q
            q / (1 % 1) == q
            q * (0 % 1) == 0 % 1
            abs (abs q) == abs q
         abs (negate q) == abs q
           q + negate q == 0 % 1
      0 % denominator q == 0 % 1
                  q + r == r + q
                  q * r == r * q
     q / negate (1 % 1) == negate q
            abs (q * q) == q * q
           q * negate r == negate (q * r)

                   0 <= denominator q
                   1 <= denominator q
                   0 <= numerator (abs q)
         numerator q <= numerator (abs q)
numerator (negate q) <= numerator (abs q)
                   q <= abs q
               0 % 1 <= abs q
                   q <= q + 1 % 1
               0 % 1 <= q * q
            negate q <= abs q
      negate (abs q) <= q
      negate (abs q) <= 0 % 1
      negate (abs q) <= negate q