YES H-Termination proof of ../tpdb/FP/full_haskell/Prelude_DOT_1.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ BR

mainModule Main
  (((.) :: (b  ->  c)  ->  (a  ->  b)  ->  a  ->  c) :: (b  ->  c)  ->  (a  ->  b)  ->  a  ->  c)

module Main where
  import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ NumRed

mainModule Main
  (((.) :: (c  ->  a)  ->  (b  ->  c)  ->  b  ->  a) :: (c  ->  a)  ->  (b  ->  c)  ->  b  ->  a)

module Main where
  import qualified Prelude


Num Reduction:All numbers are transformed to thier corresponding representation with Succ, Pred and Zero.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ NumRed
        ↳ HASKELL
          ↳ Narrow

mainModule Main
  ((.) :: (a  ->  c)  ->  (b  ->  a)  ->  b  ->  c)

module Main where
  import qualified Prelude


Haskell To QDPs