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



↳ HASKELL
  ↳ LR

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude


Lambda Reductions:
The following Lambda expression
\_→q

is transformed to
gtGt0 q _ = q



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude


If Reductions:
The following If expression
if b then (showChar '(') . p . showChar ')' else p

is transformed to
showParen0 p True = (showChar '(') . p . showChar ')'
showParen0 p False = p



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ NumRed

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude


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

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ NumRed
                ↳ HASKELL
                  ↳ Narrow

mainModule Main
  (print :: Ordering  ->  IO ())

module Main where
  import qualified Prelude


Haskell To QDPs