ratio.out

max expr size  =    5
  |- on ineqs  =    4
  |- on conds  =    4
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
  numerator (1 % denominator q) == 1
denominator (1 % denominator q) == denominator q
        denominator (q * abs r) == denominator (q * r)
                           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
    numerator q % denominator q == q
             q / negate (1 % 1) == negate q
  denominator q % denominator q == 1 % 1
                    abs (q * q) == q * q
                   q * negate r == negate (q * r)
                abs (q * abs r) == abs (q * r)
                   negate q + r == negate (q + negate r)
                  abs q * abs r == abs (q * r)
                abs (q + abs q) == q + abs q
                  abs q + abs q == abs (q + q)
            abs (1 % 1 + abs q) == 1 % 1 + abs q
        abs (1 % denominator q) == 1 % denominator q
        abs (denominator q % 1) == denominator q % 1
      recip (1 % denominator q) == denominator q % 1
      recip (denominator q % 1) == 1 % denominator q
 x % numerator (negate (1 % 1)) == negate (x % 1)
                    (q + r) + s == q + (r + s)
                    (q * r) * s == q * (r * s)
                    (q + q) * r == q * (r + r)
                q * (r + 1 % 1) == q + q * r
          numerator (abs q) % 1 == abs (numerator q % 1)
       numerator (negate q) % 1 == negate (numerator q % 1)

                         0 <= denominator q
                         1 <= denominator q
                         0 <= numerator (abs q)
               numerator q <= numerator (abs q)
                         0 <= numerator (q * q)
numerator (negate (abs q)) <= 0
               numerator q <= numerator (q * q)
             denominator q <= denominator (q * q)
       denominator (q + q) <= denominator q
               numerator q <= numerator (q + 1 % 1)
      numerator (negate q) <= numerator (abs q)
numerator (negate (abs q)) <= numerator q
         numerator (abs q) <= numerator (q * q)
numerator (negate (abs q)) <= numerator (negate 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
                         q <= q + abs r
                         q <= abs (q + q)
            negate (abs q) <= negate q
                         q <= 1 % 1 + abs q
                     0 % 1 <= q + abs q
            negate (q * q) <= 0 % 1
        q + negate (1 % 1) <= q
                     0 % 1 <= 1 % denominator q
                     0 % 1 <= denominator q % 1
                     1 % 1 <= denominator q % 1
         1 % denominator q <= 1 % 1
                     abs q <= abs (q + q)
        negate (q + 1 % 1) <= negate q
                     q + r <= q + abs r
                 q * abs q <= q * q
        negate (q + 1 % 1) <= q * q
            negate (q * q) <= q + 1 % 1
        q + negate (1 % 1) <= q * q
                 q * abs r <= abs (q * r)
              q + negate r <= q + abs r
         x % denominator q <= abs (x % 1)
                 q + abs q <= abs (q + q)
            negate (q * q) <= q * abs q
            negate (q * q) <= 1 % 1 + negate q
           abs (q + 1 % 1) <= 1 % 1 + abs q