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



↳ HASKELL
  ↳ BR

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

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

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

  
plus Z y = y
plus (S x) y = S (plus x y)



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

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

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

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

  
plus Z y = y
plus (S x) y = S (plus x y)



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
  ((mysum x) :: Main.Nat)

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

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

  
plus Z y = y
plus (S x) y = S (plus x y)



Haskell To QDPs


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

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

new_plus(S(x00), vx3) → new_plus(x00, vx3)

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: 



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

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

new_mysum(Cons(x0, x1)) → new_mysum(x1)

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: