NO 1.72 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
  ((getChar :: 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
  ((getChar :: 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
  (getChar :: 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_getChar → new_getChar

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_getChar → new_getChar

The TRS R consists of the following rules:none


s = new_getChar evaluates to t =new_getChar

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_getChar to new_getChar.




Haskell To QDPs


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

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

new_getChar([]) → new_getChar([])

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_getChar([]) → new_getChar([])

The TRS R consists of the following rules:none


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

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_getChar([]) to new_getChar([]).