H-Termination proof of ../tpdb/FP/full_haskell/FiniteMap_eltsFM_LE

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

↳ HASKELL

  ↳ LR

mainModule Main

((FiniteMap.eltsFM_LE :: FiniteMap.FiniteMap Bool a -> Bool -> [a]) :: FiniteMap.FiniteMap Bool a -> Bool -> [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)

eltsFM_LE :: Ord a => FiniteMap a b -> a -> [b]

eltsFM_LE

fm fr

foldFM_LE (\key elt rest ->elt : rest) [] fr fm

foldFM_LE :: Ord a => (a -> c -> b -> b) -> b -> a -> FiniteMap a c -> b

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt _ fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

module Main where

import qualified FiniteMap
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified FiniteMap
import qualified Main
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\keyeltrest→elt : rest

is transformed to

eltsFM_LE0 key elt rest = elt : rest

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

((FiniteMap.eltsFM_LE :: FiniteMap.FiniteMap Bool a -> Bool -> [a]) :: FiniteMap.FiniteMap Bool a -> Bool -> [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)

eltsFM_LE :: Ord a => FiniteMap a b -> a -> [b]

eltsFM_LE

fm fr

foldFM_LE eltsFM_LE0 [] fr fm

eltsFM_LE0

key elt rest

elt : rest

foldFM_LE :: Ord b => (b -> c -> a -> a) -> a -> b -> FiniteMap b c -> a

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt _ fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

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

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

((FiniteMap.eltsFM_LE :: FiniteMap.FiniteMap Bool a -> Bool -> [a]) :: FiniteMap.FiniteMap Bool a -> Bool -> [a])

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)

eltsFM_LE :: Ord a => FiniteMap a b -> a -> [b]

eltsFM_LE

fm fr

foldFM_LE eltsFM_LE0 [] fr fm

eltsFM_LE0

key elt rest

elt : rest

foldFM_LE :: Ord b => (b -> a -> c -> c) -> c -> b -> FiniteMap b a -> c

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt vw fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

module Main where

import qualified FiniteMap
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified FiniteMap
import qualified Main
import qualified Prelude

Cond Reductions:
The following Function with conditions

foldFM_LE k z fr EmptyFM = z

foldFM_LE k z fr (Branch key elt vw fm_l fm_r)

| key <= fr

= foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

| otherwise

= foldFM_LE k z fr fm_l

is transformed to

foldFM_LE k z fr EmptyFM = foldFM_LE3 k z fr EmptyFM

foldFM_LE k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1 k z fr key elt vw fm_l fm_r True = foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

foldFM_LE1 k z fr key elt vw fm_l fm_r False = foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE0 k z fr key elt vw fm_l fm_r True = foldFM_LE k z fr fm_l

foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3 k z fr EmptyFM = z

foldFM_LE3 wv ww wx wy = foldFM_LE2 wv ww wx wy

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

mainModule Main

((FiniteMap.eltsFM_LE :: FiniteMap.FiniteMap Bool a -> Bool -> [a]) :: FiniteMap.FiniteMap Bool a -> Bool -> [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)

eltsFM_LE :: Ord a => FiniteMap a b -> a -> [b]

eltsFM_LE

fm fr

foldFM_LE eltsFM_LE0 [] fr fm

eltsFM_LE0

key elt rest

elt : rest

foldFM_LE :: Ord c => (c -> a -> b -> b) -> b -> c -> FiniteMap c a -> b

foldFM_LE	k z fr EmptyFM	=	foldFM_LE3 k z fr EmptyFM
foldFM_LE	k z fr (Branch key elt vw fm_l fm_r)	=	foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE0

k z fr key elt vw fm_l fm_r True

foldFM_LE k z fr fm_l

foldFM_LE1	k z fr key elt vw fm_l fm_r True	=	foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1	k z fr key elt vw fm_l fm_r False	=	foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE2

k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3	k z fr EmptyFM	=	z
foldFM_LE3	wv ww wx wy	=	foldFM_LE2 wv ww wx wy

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

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

mainModule Main

(FiniteMap.eltsFM_LE :: FiniteMap.FiniteMap Bool a -> Bool -> [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)

eltsFM_LE :: Ord b => FiniteMap b a -> b -> [a]

eltsFM_LE

fm fr

foldFM_LE eltsFM_LE0 [] fr fm

eltsFM_LE0

key elt rest

elt : rest

foldFM_LE :: Ord c => (c -> b -> a -> a) -> a -> c -> FiniteMap c b -> a

foldFM_LE	k z fr EmptyFM	=	foldFM_LE3 k z fr EmptyFM
foldFM_LE	k z fr (Branch key elt vw fm_l fm_r)	=	foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE0

k z fr key elt vw fm_l fm_r True

foldFM_LE k z fr fm_l

foldFM_LE1	k z fr key elt vw fm_l fm_r True	=	foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1	k z fr key elt vw fm_l fm_r False	=	foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE2

k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3	k z fr EmptyFM	=	z
foldFM_LE3	wv ww wx wy	=	foldFM_LE2 wv ww wx wy

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

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="FiniteMap.eltsFM_LE\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="FiniteMap.eltsFM_LE wz3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="FiniteMap.eltsFM_LE wz3 wz4\n",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] wz4 wz3\n",fontsize=16,color="burlywood",shape="triangle"];114[label="wz3/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];5 -> 114[label="",style="solid", color="burlywood", weight=9];
114 -> 6[label="",style="solid", color="burlywood", weight=3];
115[label="wz3/FiniteMap.Branch wz30 wz31 wz32 wz33 wz34",fontsize=10,color="white",style="solid",shape="box"];5 -> 115[label="",style="solid", color="burlywood", weight=9];
115 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] wz4 FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] wz4 (FiniteMap.Branch wz30 wz31 wz32 wz33 wz34)\n",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="FiniteMap.foldFM_LE3 FiniteMap.eltsFM_LE0 [] wz4 FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="FiniteMap.foldFM_LE2 FiniteMap.eltsFM_LE0 [] wz4 (FiniteMap.Branch wz30 wz31 wz32 wz33 wz34)\n",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="[]\n",fontsize=16,color="green",shape="box"];11[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (wz30 <= wz4)\n",fontsize=16,color="burlywood",shape="box"];116[label="wz30/False",fontsize=10,color="white",style="solid",shape="box"];11 -> 116[label="",style="solid", color="burlywood", weight=9];
116 -> 12[label="",style="solid", color="burlywood", weight=3];
117[label="wz30/True",fontsize=10,color="white",style="solid",shape="box"];11 -> 117[label="",style="solid", color="burlywood", weight=9];
117 -> 13[label="",style="solid", color="burlywood", weight=3];
12[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] wz4 False wz31 wz32 wz33 wz34 (False <= wz4)\n",fontsize=16,color="burlywood",shape="box"];118[label="wz4/False",fontsize=10,color="white",style="solid",shape="box"];12 -> 118[label="",style="solid", color="burlywood", weight=9];
118 -> 14[label="",style="solid", color="burlywood", weight=3];
119[label="wz4/True",fontsize=10,color="white",style="solid",shape="box"];12 -> 119[label="",style="solid", color="burlywood", weight=9];
119 -> 15[label="",style="solid", color="burlywood", weight=3];
13[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] wz4 True wz31 wz32 wz33 wz34 (True <= wz4)\n",fontsize=16,color="burlywood",shape="box"];120[label="wz4/False",fontsize=10,color="white",style="solid",shape="box"];13 -> 120[label="",style="solid", color="burlywood", weight=9];
120 -> 16[label="",style="solid", color="burlywood", weight=3];
121[label="wz4/True",fontsize=10,color="white",style="solid",shape="box"];13 -> 121[label="",style="solid", color="burlywood", weight=9];
121 -> 17[label="",style="solid", color="burlywood", weight=3];
14[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] False False wz31 wz32 wz33 wz34 (False <= False)\n",fontsize=16,color="black",shape="box"];14 -> 18[label="",style="solid", color="black", weight=3];
15[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] True False wz31 wz32 wz33 wz34 (False <= True)\n",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] False True wz31 wz32 wz33 wz34 (True <= False)\n",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] True True wz31 wz32 wz33 wz34 (True <= True)\n",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] False False wz31 wz32 wz33 wz34 True\n",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] True False wz31 wz32 wz33 wz34 True\n",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] False True wz31 wz32 wz33 wz34 False\n",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 [] True True wz31 wz32 wz33 wz34 True\n",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22 -> 26[label="",style="dashed", color="red", weight=0];
22[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 (FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] False wz33)) False wz34\n",fontsize=16,color="magenta"];22 -> 27[label="",style="dashed", color="magenta", weight=3];
23 -> 28[label="",style="dashed", color="red", weight=0];
23[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 (FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] True wz33)) True wz34\n",fontsize=16,color="magenta"];23 -> 29[label="",style="dashed", color="magenta", weight=3];
24[label="FiniteMap.foldFM_LE0 FiniteMap.eltsFM_LE0 [] False True wz31 wz32 wz33 wz34 otherwise\n",fontsize=16,color="black",shape="box"];24 -> 30[label="",style="solid", color="black", weight=3];
25 -> 31[label="",style="dashed", color="red", weight=0];
25[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz31 (FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] True wz33)) True wz34\n",fontsize=16,color="magenta"];25 -> 32[label="",style="dashed", color="magenta", weight=3];
27 -> 5[label="",style="dashed", color="red", weight=0];
27[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] False wz33\n",fontsize=16,color="magenta"];27 -> 33[label="",style="dashed", color="magenta", weight=3];
27 -> 34[label="",style="dashed", color="magenta", weight=3];
26[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz5) False wz34\n",fontsize=16,color="burlywood",shape="triangle"];126[label="wz34/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];26 -> 126[label="",style="solid", color="burlywood", weight=9];
126 -> 35[label="",style="solid", color="burlywood", weight=3];
127[label="wz34/FiniteMap.Branch wz340 wz341 wz342 wz343 wz344",fontsize=10,color="white",style="solid",shape="box"];26 -> 127[label="",style="solid", color="burlywood", weight=9];
127 -> 36[label="",style="solid", color="burlywood", weight=3];
29 -> 5[label="",style="dashed", color="red", weight=0];
29[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] True wz33\n",fontsize=16,color="magenta"];29 -> 37[label="",style="dashed", color="magenta", weight=3];
29 -> 38[label="",style="dashed", color="magenta", weight=3];
28[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz6) True wz34\n",fontsize=16,color="burlywood",shape="triangle"];129[label="wz34/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];28 -> 129[label="",style="solid", color="burlywood", weight=9];
129 -> 39[label="",style="solid", color="burlywood", weight=3];
130[label="wz34/FiniteMap.Branch wz340 wz341 wz342 wz343 wz344",fontsize=10,color="white",style="solid",shape="box"];28 -> 130[label="",style="solid", color="burlywood", weight=9];
130 -> 40[label="",style="solid", color="burlywood", weight=3];
30[label="FiniteMap.foldFM_LE0 FiniteMap.eltsFM_LE0 [] False True wz31 wz32 wz33 wz34 True\n",fontsize=16,color="black",shape="box"];30 -> 41[label="",style="solid", color="black", weight=3];
32 -> 5[label="",style="dashed", color="red", weight=0];
32[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] True wz33\n",fontsize=16,color="magenta"];32 -> 42[label="",style="dashed", color="magenta", weight=3];
32 -> 43[label="",style="dashed", color="magenta", weight=3];
31[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz31 wz7) True wz34\n",fontsize=16,color="burlywood",shape="triangle"];132[label="wz34/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];31 -> 132[label="",style="solid", color="burlywood", weight=9];
132 -> 44[label="",style="solid", color="burlywood", weight=3];
133[label="wz34/FiniteMap.Branch wz340 wz341 wz342 wz343 wz344",fontsize=10,color="white",style="solid",shape="box"];31 -> 133[label="",style="solid", color="burlywood", weight=9];
133 -> 45[label="",style="solid", color="burlywood", weight=3];
33[label="wz33\n",fontsize=16,color="green",shape="box"];34[label="False\n",fontsize=16,color="green",shape="box"];35[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz5) False FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];35 -> 46[label="",style="solid", color="black", weight=3];
36[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz5) False (FiniteMap.Branch wz340 wz341 wz342 wz343 wz344)\n",fontsize=16,color="black",shape="box"];36 -> 47[label="",style="solid", color="black", weight=3];
37[label="wz33\n",fontsize=16,color="green",shape="box"];38[label="True\n",fontsize=16,color="green",shape="box"];39[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz6) True FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];39 -> 48[label="",style="solid", color="black", weight=3];
40[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz6) True (FiniteMap.Branch wz340 wz341 wz342 wz343 wz344)\n",fontsize=16,color="black",shape="box"];40 -> 49[label="",style="solid", color="black", weight=3];
41 -> 5[label="",style="dashed", color="red", weight=0];
41[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 [] False wz33\n",fontsize=16,color="magenta"];41 -> 50[label="",style="dashed", color="magenta", weight=3];
41 -> 51[label="",style="dashed", color="magenta", weight=3];
42[label="wz33\n",fontsize=16,color="green",shape="box"];43[label="True\n",fontsize=16,color="green",shape="box"];44[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz31 wz7) True FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz31 wz7) True (FiniteMap.Branch wz340 wz341 wz342 wz343 wz344)\n",fontsize=16,color="black",shape="box"];45 -> 53[label="",style="solid", color="black", weight=3];
46[label="FiniteMap.foldFM_LE3 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz5) False FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];46 -> 54[label="",style="solid", color="black", weight=3];
47[label="FiniteMap.foldFM_LE2 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz5) False (FiniteMap.Branch wz340 wz341 wz342 wz343 wz344)\n",fontsize=16,color="black",shape="box"];47 -> 55[label="",style="solid", color="black", weight=3];
48[label="FiniteMap.foldFM_LE3 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz6) True FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];48 -> 56[label="",style="solid", color="black", weight=3];
49[label="FiniteMap.foldFM_LE2 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz6) True (FiniteMap.Branch wz340 wz341 wz342 wz343 wz344)\n",fontsize=16,color="black",shape="box"];49 -> 57[label="",style="solid", color="black", weight=3];
50[label="wz33\n",fontsize=16,color="green",shape="box"];51[label="False\n",fontsize=16,color="green",shape="box"];52[label="FiniteMap.foldFM_LE3 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz31 wz7) True FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];52 -> 58[label="",style="solid", color="black", weight=3];
53[label="FiniteMap.foldFM_LE2 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz31 wz7) True (FiniteMap.Branch wz340 wz341 wz342 wz343 wz344)\n",fontsize=16,color="black",shape="box"];53 -> 59[label="",style="solid", color="black", weight=3];
54[label="FiniteMap.eltsFM_LE0 False wz31 wz5\n",fontsize=16,color="black",shape="triangle"];54 -> 60[label="",style="solid", color="black", weight=3];
55 -> 61[label="",style="dashed", color="red", weight=0];
55[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz5) False wz340 wz341 wz342 wz343 wz344 (wz340 <= False)\n",fontsize=16,color="magenta"];55 -> 62[label="",style="dashed", color="magenta", weight=3];
56 -> 54[label="",style="dashed", color="red", weight=0];
56[label="FiniteMap.eltsFM_LE0 False wz31 wz6\n",fontsize=16,color="magenta"];56 -> 63[label="",style="dashed", color="magenta", weight=3];
57 -> 64[label="",style="dashed", color="red", weight=0];
57[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz31 wz6) True wz340 wz341 wz342 wz343 wz344 (wz340 <= True)\n",fontsize=16,color="magenta"];57 -> 65[label="",style="dashed", color="magenta", weight=3];
58[label="FiniteMap.eltsFM_LE0 True wz31 wz7\n",fontsize=16,color="black",shape="triangle"];58 -> 67[label="",style="solid", color="black", weight=3];
59 -> 64[label="",style="dashed", color="red", weight=0];
59[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz31 wz7) True wz340 wz341 wz342 wz343 wz344 (wz340 <= True)\n",fontsize=16,color="magenta"];59 -> 66[label="",style="dashed", color="magenta", weight=3];
60[label="wz31 : wz5\n",fontsize=16,color="green",shape="box"];62 -> 54[label="",style="dashed", color="red", weight=0];
62[label="FiniteMap.eltsFM_LE0 False wz31 wz5\n",fontsize=16,color="magenta"];61[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz8 False wz340 wz341 wz342 wz343 wz344 (wz340 <= False)\n",fontsize=16,color="burlywood",shape="triangle"];140[label="wz340/False",fontsize=10,color="white",style="solid",shape="box"];61 -> 140[label="",style="solid", color="burlywood", weight=9];
140 -> 68[label="",style="solid", color="burlywood", weight=3];
141[label="wz340/True",fontsize=10,color="white",style="solid",shape="box"];61 -> 141[label="",style="solid", color="burlywood", weight=9];
141 -> 69[label="",style="solid", color="burlywood", weight=3];
63[label="wz6\n",fontsize=16,color="green",shape="box"];65 -> 54[label="",style="dashed", color="red", weight=0];
65[label="FiniteMap.eltsFM_LE0 False wz31 wz6\n",fontsize=16,color="magenta"];65 -> 70[label="",style="dashed", color="magenta", weight=3];
64[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz9 True wz340 wz341 wz342 wz343 wz344 (wz340 <= True)\n",fontsize=16,color="burlywood",shape="triangle"];143[label="wz340/False",fontsize=10,color="white",style="solid",shape="box"];64 -> 143[label="",style="solid", color="burlywood", weight=9];
143 -> 71[label="",style="solid", color="burlywood", weight=3];
144[label="wz340/True",fontsize=10,color="white",style="solid",shape="box"];64 -> 144[label="",style="solid", color="burlywood", weight=9];
144 -> 72[label="",style="solid", color="burlywood", weight=3];
67[label="wz31 : wz7\n",fontsize=16,color="green",shape="box"];66 -> 58[label="",style="dashed", color="red", weight=0];
66[label="FiniteMap.eltsFM_LE0 True wz31 wz7\n",fontsize=16,color="magenta"];68[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz8 False False wz341 wz342 wz343 wz344 (False <= False)\n",fontsize=16,color="black",shape="box"];68 -> 73[label="",style="solid", color="black", weight=3];
69[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz8 False True wz341 wz342 wz343 wz344 (True <= False)\n",fontsize=16,color="black",shape="box"];69 -> 74[label="",style="solid", color="black", weight=3];
70[label="wz6\n",fontsize=16,color="green",shape="box"];71[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz9 True False wz341 wz342 wz343 wz344 (False <= True)\n",fontsize=16,color="black",shape="box"];71 -> 75[label="",style="solid", color="black", weight=3];
72[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz9 True True wz341 wz342 wz343 wz344 (True <= True)\n",fontsize=16,color="black",shape="box"];72 -> 76[label="",style="solid", color="black", weight=3];
73[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz8 False False wz341 wz342 wz343 wz344 True\n",fontsize=16,color="black",shape="box"];73 -> 77[label="",style="solid", color="black", weight=3];
74[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz8 False True wz341 wz342 wz343 wz344 False\n",fontsize=16,color="black",shape="box"];74 -> 78[label="",style="solid", color="black", weight=3];
75[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz9 True False wz341 wz342 wz343 wz344 True\n",fontsize=16,color="black",shape="box"];75 -> 79[label="",style="solid", color="black", weight=3];
76[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz9 True True wz341 wz342 wz343 wz344 True\n",fontsize=16,color="black",shape="box"];76 -> 80[label="",style="solid", color="black", weight=3];
77 -> 26[label="",style="dashed", color="red", weight=0];
77[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz341 (FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz8 False wz343)) False wz344\n",fontsize=16,color="magenta"];77 -> 81[label="",style="dashed", color="magenta", weight=3];
77 -> 82[label="",style="dashed", color="magenta", weight=3];
77 -> 83[label="",style="dashed", color="magenta", weight=3];
78[label="FiniteMap.foldFM_LE0 FiniteMap.eltsFM_LE0 wz8 False True wz341 wz342 wz343 wz344 otherwise\n",fontsize=16,color="black",shape="box"];78 -> 84[label="",style="solid", color="black", weight=3];
79 -> 28[label="",style="dashed", color="red", weight=0];
79[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 False wz341 (FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz9 True wz343)) True wz344\n",fontsize=16,color="magenta"];79 -> 85[label="",style="dashed", color="magenta", weight=3];
79 -> 86[label="",style="dashed", color="magenta", weight=3];
79 -> 87[label="",style="dashed", color="magenta", weight=3];
80 -> 31[label="",style="dashed", color="red", weight=0];
80[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 (FiniteMap.eltsFM_LE0 True wz341 (FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz9 True wz343)) True wz344\n",fontsize=16,color="magenta"];80 -> 88[label="",style="dashed", color="magenta", weight=3];
80 -> 89[label="",style="dashed", color="magenta", weight=3];
80 -> 90[label="",style="dashed", color="magenta", weight=3];
81[label="wz344\n",fontsize=16,color="green",shape="box"];82[label="wz341\n",fontsize=16,color="green",shape="box"];83[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz8 False wz343\n",fontsize=16,color="burlywood",shape="triangle"];149[label="wz343/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];83 -> 149[label="",style="solid", color="burlywood", weight=9];
149 -> 91[label="",style="solid", color="burlywood", weight=3];
150[label="wz343/FiniteMap.Branch wz3430 wz3431 wz3432 wz3433 wz3434",fontsize=10,color="white",style="solid",shape="box"];83 -> 150[label="",style="solid", color="burlywood", weight=9];
150 -> 92[label="",style="solid", color="burlywood", weight=3];
84[label="FiniteMap.foldFM_LE0 FiniteMap.eltsFM_LE0 wz8 False True wz341 wz342 wz343 wz344 True\n",fontsize=16,color="black",shape="box"];84 -> 93[label="",style="solid", color="black", weight=3];
85[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz9 True wz343\n",fontsize=16,color="burlywood",shape="triangle"];151[label="wz343/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];85 -> 151[label="",style="solid", color="burlywood", weight=9];
151 -> 94[label="",style="solid", color="burlywood", weight=3];
152[label="wz343/FiniteMap.Branch wz3430 wz3431 wz3432 wz3433 wz3434",fontsize=10,color="white",style="solid",shape="box"];85 -> 152[label="",style="solid", color="burlywood", weight=9];
152 -> 95[label="",style="solid", color="burlywood", weight=3];
86[label="wz344\n",fontsize=16,color="green",shape="box"];87[label="wz341\n",fontsize=16,color="green",shape="box"];88[label="wz344\n",fontsize=16,color="green",shape="box"];89[label="wz341\n",fontsize=16,color="green",shape="box"];90 -> 85[label="",style="dashed", color="red", weight=0];
90[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz9 True wz343\n",fontsize=16,color="magenta"];91[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz8 False FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];91 -> 96[label="",style="solid", color="black", weight=3];
92[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz8 False (FiniteMap.Branch wz3430 wz3431 wz3432 wz3433 wz3434)\n",fontsize=16,color="black",shape="box"];92 -> 97[label="",style="solid", color="black", weight=3];
93 -> 83[label="",style="dashed", color="red", weight=0];
93[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz8 False wz343\n",fontsize=16,color="magenta"];94[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz9 True FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];94 -> 98[label="",style="solid", color="black", weight=3];
95[label="FiniteMap.foldFM_LE FiniteMap.eltsFM_LE0 wz9 True (FiniteMap.Branch wz3430 wz3431 wz3432 wz3433 wz3434)\n",fontsize=16,color="black",shape="box"];95 -> 99[label="",style="solid", color="black", weight=3];
96[label="FiniteMap.foldFM_LE3 FiniteMap.eltsFM_LE0 wz8 False FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];96 -> 100[label="",style="solid", color="black", weight=3];
97[label="FiniteMap.foldFM_LE2 FiniteMap.eltsFM_LE0 wz8 False (FiniteMap.Branch wz3430 wz3431 wz3432 wz3433 wz3434)\n",fontsize=16,color="black",shape="box"];97 -> 101[label="",style="solid", color="black", weight=3];
98[label="FiniteMap.foldFM_LE3 FiniteMap.eltsFM_LE0 wz9 True FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];98 -> 102[label="",style="solid", color="black", weight=3];
99[label="FiniteMap.foldFM_LE2 FiniteMap.eltsFM_LE0 wz9 True (FiniteMap.Branch wz3430 wz3431 wz3432 wz3433 wz3434)\n",fontsize=16,color="black",shape="box"];99 -> 103[label="",style="solid", color="black", weight=3];
100[label="wz8\n",fontsize=16,color="green",shape="box"];101 -> 61[label="",style="dashed", color="red", weight=0];
101[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz8 False wz3430 wz3431 wz3432 wz3433 wz3434 (wz3430 <= False)\n",fontsize=16,color="magenta"];101 -> 104[label="",style="dashed", color="magenta", weight=3];
101 -> 105[label="",style="dashed", color="magenta", weight=3];
101 -> 106[label="",style="dashed", color="magenta", weight=3];
101 -> 107[label="",style="dashed", color="magenta", weight=3];
101 -> 108[label="",style="dashed", color="magenta", weight=3];
102[label="wz9\n",fontsize=16,color="green",shape="box"];103 -> 64[label="",style="dashed", color="red", weight=0];
103[label="FiniteMap.foldFM_LE1 FiniteMap.eltsFM_LE0 wz9 True wz3430 wz3431 wz3432 wz3433 wz3434 (wz3430 <= True)\n",fontsize=16,color="magenta"];103 -> 109[label="",style="dashed", color="magenta", weight=3];
103 -> 110[label="",style="dashed", color="magenta", weight=3];
103 -> 111[label="",style="dashed", color="magenta", weight=3];
103 -> 112[label="",style="dashed", color="magenta", weight=3];
103 -> 113[label="",style="dashed", color="magenta", weight=3];
104[label="wz3433\n",fontsize=16,color="green",shape="box"];105[label="wz3430\n",fontsize=16,color="green",shape="box"];106[label="wz3432\n",fontsize=16,color="green",shape="box"];107[label="wz3431\n",fontsize=16,color="green",shape="box"];108[label="wz3434\n",fontsize=16,color="green",shape="box"];109[label="wz3433\n",fontsize=16,color="green",shape="box"];110[label="wz3430\n",fontsize=16,color="green",shape="box"];111[label="wz3432\n",fontsize=16,color="green",shape="box"];112[label="wz3431\n",fontsize=16,color="green",shape="box"];113[label="wz3434\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

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

new_foldFM_LE11(wz8, False, wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE11(wz8, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE11(wz8, False, wz341, wz342, wz343, wz344, h) → new_foldFM_LE6(wz341, new_foldFM_LE7(wz8, wz343, h), wz344, h)
new_foldFM_LE6(wz31, wz5, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE11(new_eltsFM_LE0(wz31, wz5, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE8(wz8, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE11(wz8, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE11(wz8, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE8(wz8, wz343, h)

The TRS R consists of the following rules:

new_foldFM_LE9(wz31, wz5, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE12(new_eltsFM_LE0(wz31, wz5, h), wz340, wz341, wz342, wz343, wz344, h)
new_eltsFM_LE0(wz31, wz5, h) → :(wz31, wz5)
new_foldFM_LE12(wz8, False, wz341, wz342, wz343, wz344, h) → new_foldFM_LE9(wz341, new_foldFM_LE7(wz8, wz343, h), wz344, h)
new_foldFM_LE7(wz8, EmptyFM, h) → wz8
new_foldFM_LE12(wz8, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE7(wz8, wz343, h)
new_foldFM_LE7(wz8, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE12(wz8, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE9(wz31, wz5, EmptyFM, h) → new_eltsFM_LE0(wz31, wz5, h)

The set Q consists of the following terms:

new_foldFM_LE7(x0, EmptyFM, x1)
new_foldFM_LE7(x0, Branch(x1, x2, x3, x4, x5), x6)
new_foldFM_LE12(x0, True, x1, x2, x3, x4, x5)
new_foldFM_LE9(x0, x1, EmptyFM, x2)
new_foldFM_LE9(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE12(x0, False, x1, x2, x3, x4, x5)
new_eltsFM_LE0(x0, x1, x2)

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:

new_foldFM_LE11(wz8, False, wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE11(wz8, wz3430, wz3431, wz3432, wz3433, wz3434, h)
The graph contains the following edges 1 >= 1, 5 > 2, 5 > 3, 5 > 4, 5 > 5, 5 > 6, 7 >= 7
new_foldFM_LE6(wz31, wz5, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE11(new_eltsFM_LE0(wz31, wz5, h), wz340, wz341, wz342, wz343, wz344, h)
The graph contains the following edges 3 > 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 4 >= 7
new_foldFM_LE8(wz8, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE11(wz8, wz3430, wz3431, wz3432, wz3433, wz3434, h)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4, 2 > 5, 2 > 6, 3 >= 7
new_foldFM_LE11(wz8, False, wz341, wz342, wz343, wz344, h) → new_foldFM_LE6(wz341, new_foldFM_LE7(wz8, wz343, h), wz344, h)
The graph contains the following edges 3 >= 1, 6 >= 3, 7 >= 4
new_foldFM_LE11(wz8, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE8(wz8, wz343, h)
The graph contains the following edges 1 >= 1, 5 >= 2, 7 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

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

new_foldFM_LE1(wz9, False, wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE1(wz9, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE2(wz31, wz7, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_eltsFM_LE00(wz31, wz7, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE1(wz9, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE3(wz9, wz343, h)
new_foldFM_LE(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_eltsFM_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE3(wz9, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE1(wz9, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE1(wz9, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE2(wz341, new_foldFM_LE0(wz9, wz343, h), wz344, h)
new_foldFM_LE1(wz9, False, wz341, wz342, wz343, wz344, h) → new_foldFM_LE(wz341, new_foldFM_LE0(wz9, wz343, h), wz344, h)

The TRS R consists of the following rules:

new_foldFM_LE5(wz31, wz7, EmptyFM, h) → new_eltsFM_LE00(wz31, wz7, h)
new_eltsFM_LE00(wz31, wz7, h) → :(wz31, wz7)
new_eltsFM_LE0(wz31, wz5, h) → :(wz31, wz5)
new_foldFM_LE0(wz9, EmptyFM, h) → wz9
new_foldFM_LE5(wz31, wz7, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE10(new_eltsFM_LE00(wz31, wz7, h), wz340, wz341, wz342, wz343, wz344, h)
new_foldFM_LE10(wz9, False, wz341, wz342, wz343, wz344, h) → new_foldFM_LE4(wz341, new_foldFM_LE0(wz9, wz343, h), wz344, h)
new_foldFM_LE0(wz9, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE10(wz9, wz3430, wz3431, wz3432, wz3433, wz3434, h)
new_foldFM_LE4(wz31, wz6, EmptyFM, h) → new_eltsFM_LE0(wz31, wz6, h)
new_foldFM_LE10(wz9, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE5(wz341, new_foldFM_LE0(wz9, wz343, h), wz344, h)
new_foldFM_LE4(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE10(new_eltsFM_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)

The set Q consists of the following terms:

new_foldFM_LE10(x0, True, x1, x2, x3, x4, x5)
new_foldFM_LE0(x0, EmptyFM, x1)
new_eltsFM_LE00(x0, x1, x2)
new_foldFM_LE4(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE0(x0, Branch(x1, x2, x3, x4, x5), x6)
new_foldFM_LE5(x0, x1, Branch(x2, x3, x4, x5, x6), x7)
new_foldFM_LE10(x0, False, x1, x2, x3, x4, x5)
new_foldFM_LE5(x0, x1, EmptyFM, x2)
new_foldFM_LE4(x0, x1, EmptyFM, x2)
new_eltsFM_LE0(x0, x1, x2)

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:

new_foldFM_LE1(wz9, False, wz341, wz342, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), wz344, h) → new_foldFM_LE1(wz9, wz3430, wz3431, wz3432, wz3433, wz3434, h)
The graph contains the following edges 1 >= 1, 5 > 2, 5 > 3, 5 > 4, 5 > 5, 5 > 6, 7 >= 7
new_foldFM_LE1(wz9, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE2(wz341, new_foldFM_LE0(wz9, wz343, h), wz344, h)
The graph contains the following edges 3 >= 1, 6 >= 3, 7 >= 4
new_foldFM_LE3(wz9, Branch(wz3430, wz3431, wz3432, wz3433, wz3434), h) → new_foldFM_LE1(wz9, wz3430, wz3431, wz3432, wz3433, wz3434, h)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4, 2 > 5, 2 > 6, 3 >= 7
new_foldFM_LE1(wz9, True, wz341, wz342, wz343, wz344, h) → new_foldFM_LE3(wz9, wz343, h)
The graph contains the following edges 1 >= 1, 5 >= 2, 7 >= 3
new_foldFM_LE1(wz9, False, wz341, wz342, wz343, wz344, h) → new_foldFM_LE(wz341, new_foldFM_LE0(wz9, wz343, h), wz344, h)
The graph contains the following edges 3 >= 1, 6 >= 3, 7 >= 4
new_foldFM_LE2(wz31, wz7, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_eltsFM_LE00(wz31, wz7, h), wz340, wz341, wz342, wz343, wz344, h)
The graph contains the following edges 3 > 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 4 >= 7
new_foldFM_LE(wz31, wz6, Branch(wz340, wz341, wz342, wz343, wz344), h) → new_foldFM_LE1(new_eltsFM_LE0(wz31, wz6, h), wz340, wz341, wz342, wz343, wz344, h)
The graph contains the following edges 3 > 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 4 >= 7

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

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

new_foldFM_LE13(False, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(False, wz33, h)
new_foldFM_LE13(False, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(False, wz33, h)
new_foldFM_LE13(True, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(True, wz33, h)
new_foldFM_LE13(True, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(True, wz33, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                              ↳ QDPSizeChangeProof

                            ↳ QDP

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

new_foldFM_LE13(True, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(True, wz33, h)
new_foldFM_LE13(True, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(True, wz33, 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:

new_foldFM_LE13(True, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(True, wz33, h)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 3 >= 3
new_foldFM_LE13(True, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(True, wz33, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ AND

                            ↳ QDP

                            ↳ QDP

                              ↳ QDPSizeChangeProof

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

new_foldFM_LE13(False, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(False, wz33, h)
new_foldFM_LE13(False, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(False, wz33, h)

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

new_foldFM_LE13(False, Branch(True, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(False, wz33, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
new_foldFM_LE13(False, Branch(False, wz31, wz32, wz33, wz34), h) → new_foldFM_LE13(False, wz33, h)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 3 >= 3

foldFM_LE	k z fr EmptyFM	= foldFM_LE3 k z fr EmptyFM
foldFM_LE	k z fr (Branch key elt vw fm_l fm_r)	= foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1	k z fr key elt vw fm_l fm_r True	= foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1	k z fr key elt vw fm_l fm_r False	= foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise