YES H-Termination proof of /tmp/aproveN7gh2V.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ BR

mainModule Main
  ((mylength x) :: Main.Nat)

module Main where
  import qualified Prelude
  data List a = Nil  | Cons a (List a) 

data Main.Nat = Z  | S Main.Nat 
  
mylength Nil = Z
mylength (Cons x xs) = S (mylength xs)



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule Main
  ((mylength x) :: Main.Nat)

module Main where
  import qualified Prelude
  data List a = Nil  | Cons a (List a) 

data Main.Nat = Z  | S Main.Nat 
  
mylength Nil = Z
mylength (Cons x xs) = S (mylength xs)



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

mainModule Main
  ((mylength x) :: Main.Nat)

module Main where
  import qualified Prelude
  data List a = Nil  | Cons a (List a) 

data Main.Nat = Z  | S Main.Nat 
  
mylength Nil = Z
mylength (Cons x xs) = S (mylength xs)



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ QDP
              ↳ QDPSizeChangeProof

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

new_mylength(Cons(x0, x1), h) → new_mylength(x1, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: