NO 1.733 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be disproven:



↳ HASKELL
  ↳ BR

mainModule Main
  ((getContents :: IO [Char]) :: IO [Char])

module Main where
  import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule Main
  ((getContents :: IO [Char]) :: IO [Char])

module Main where
  import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
          ↳ Narrow

mainModule Main
  (getContents :: IO [Char])

module Main where
  import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ NonTerminationProof
          ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_getContents → new_getContents

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_getContents → new_getContents

The TRS R consists of the following rules:none


s = new_getContents evaluates to t =new_getContents

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_getContents to new_getContents.




Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
          ↳ Narrow
            ↳ QDP
              ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

new_getContents([]) → new_getContents([])

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_getContents([]) → new_getContents([])

The TRS R consists of the following rules:none


s = new_getContents([]) evaluates to t =new_getContents([])

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_getContents([]) to new_getContents([]).