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



↳ HASKELL
  ↳ BR

mainModule Main
  ((FiniteMap.emptyFM :: FiniteMap.FiniteMap a b) :: FiniteMap.FiniteMap a b)

module FiniteMap where
  import qualified Main
import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  emptyFM :: FiniteMap b a
emptyFM = EmptyFM


module Main where
  import qualified FiniteMap
import qualified Maybe
import qualified Prelude

module Maybe where
  import qualified FiniteMap
import qualified Main
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ NumRed

mainModule Main
  ((FiniteMap.emptyFM :: FiniteMap.FiniteMap b a) :: FiniteMap.FiniteMap b a)

module FiniteMap where
  import qualified Main
import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  emptyFM :: FiniteMap a b
emptyFM = EmptyFM


module Main where
  import qualified FiniteMap
import qualified Maybe
import qualified Prelude

module Maybe where
  import qualified FiniteMap
import qualified Main
import qualified Prelude


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

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ NumRed
        ↳ HASKELL
          ↳ Narrow

mainModule Main
  (FiniteMap.emptyFM :: FiniteMap.FiniteMap a b)

module FiniteMap where
  import qualified Main
import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  emptyFM :: FiniteMap a b
emptyFM = EmptyFM


module Main where
  import qualified FiniteMap
import qualified Maybe
import qualified Prelude

module Maybe where
  import qualified FiniteMap
import qualified Main
import qualified Prelude


Haskell To QDPs