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

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

↳ HASKELL

  ↳ BR

mainModule Main

((FiniteMap.foldFM_LE :: (Ordering -> b -> a -> a) -> a -> Ordering -> FiniteMap.FiniteMap Ordering b -> a) :: (Ordering -> b -> a -> a) -> a -> Ordering -> FiniteMap.FiniteMap Ordering b -> 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)

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

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

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((FiniteMap.foldFM_LE :: (Ordering -> a -> b -> b) -> b -> Ordering -> FiniteMap.FiniteMap Ordering a -> b) :: (Ordering -> a -> b -> b) -> b -> Ordering -> FiniteMap.FiniteMap Ordering 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)

foldFM_LE :: Ord a => (a -> b -> c -> c) -> c -> a -> FiniteMap a b -> 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

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((FiniteMap.foldFM_LE :: (Ordering -> b -> a -> a) -> a -> Ordering -> FiniteMap.FiniteMap Ordering b -> a) :: (Ordering -> b -> a -> a) -> a -> Ordering -> FiniteMap.FiniteMap Ordering 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)

foldFM_LE :: Ord a => (a -> c -> b -> b) -> b -> a -> FiniteMap a c -> 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

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(FiniteMap.foldFM_LE :: (Ordering -> b -> a -> a) -> a -> Ordering -> FiniteMap.FiniteMap Ordering 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)

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

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.foldFM_LE\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="FiniteMap.foldFM_LE wz3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="FiniteMap.foldFM_LE wz3 wz4\n",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="FiniteMap.foldFM_LE wz3 wz4 wz5\n",fontsize=16,color="grey",shape="box"];5 -> 6[label="",style="dashed", color="grey", weight=3];
6[label="FiniteMap.foldFM_LE wz3 wz4 wz5 wz6\n",fontsize=16,color="burlywood",shape="triangle"];103[label="wz6/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];6 -> 103[label="",style="solid", color="burlywood", weight=9];
103 -> 7[label="",style="solid", color="burlywood", weight=3];
104[label="wz6/FiniteMap.Branch wz60 wz61 wz62 wz63 wz64",fontsize=10,color="white",style="solid",shape="box"];6 -> 104[label="",style="solid", color="burlywood", weight=9];
104 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="FiniteMap.foldFM_LE wz3 wz4 wz5 FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="FiniteMap.foldFM_LE wz3 wz4 wz5 (FiniteMap.Branch wz60 wz61 wz62 wz63 wz64)\n",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="FiniteMap.foldFM_LE3 wz3 wz4 wz5 FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="FiniteMap.foldFM_LE2 wz3 wz4 wz5 (FiniteMap.Branch wz60 wz61 wz62 wz63 wz64)\n",fontsize=16,color="black",shape="box"];10 -> 12[label="",style="solid", color="black", weight=3];
11[label="wz4\n",fontsize=16,color="green",shape="box"];12[label="FiniteMap.foldFM_LE1 wz3 wz4 wz5 wz60 wz61 wz62 wz63 wz64 (wz60 <= wz5)\n",fontsize=16,color="burlywood",shape="box"];105[label="wz60/LT",fontsize=10,color="white",style="solid",shape="box"];12 -> 105[label="",style="solid", color="burlywood", weight=9];
105 -> 13[label="",style="solid", color="burlywood", weight=3];
106[label="wz60/EQ",fontsize=10,color="white",style="solid",shape="box"];12 -> 106[label="",style="solid", color="burlywood", weight=9];
106 -> 14[label="",style="solid", color="burlywood", weight=3];
107[label="wz60/GT",fontsize=10,color="white",style="solid",shape="box"];12 -> 107[label="",style="solid", color="burlywood", weight=9];
107 -> 15[label="",style="solid", color="burlywood", weight=3];
13[label="FiniteMap.foldFM_LE1 wz3 wz4 wz5 LT wz61 wz62 wz63 wz64 (LT <= wz5)\n",fontsize=16,color="burlywood",shape="box"];108[label="wz5/LT",fontsize=10,color="white",style="solid",shape="box"];13 -> 108[label="",style="solid", color="burlywood", weight=9];
108 -> 16[label="",style="solid", color="burlywood", weight=3];
109[label="wz5/EQ",fontsize=10,color="white",style="solid",shape="box"];13 -> 109[label="",style="solid", color="burlywood", weight=9];
109 -> 17[label="",style="solid", color="burlywood", weight=3];
110[label="wz5/GT",fontsize=10,color="white",style="solid",shape="box"];13 -> 110[label="",style="solid", color="burlywood", weight=9];
110 -> 18[label="",style="solid", color="burlywood", weight=3];
14[label="FiniteMap.foldFM_LE1 wz3 wz4 wz5 EQ wz61 wz62 wz63 wz64 (EQ <= wz5)\n",fontsize=16,color="burlywood",shape="box"];111[label="wz5/LT",fontsize=10,color="white",style="solid",shape="box"];14 -> 111[label="",style="solid", color="burlywood", weight=9];
111 -> 19[label="",style="solid", color="burlywood", weight=3];
112[label="wz5/EQ",fontsize=10,color="white",style="solid",shape="box"];14 -> 112[label="",style="solid", color="burlywood", weight=9];
112 -> 20[label="",style="solid", color="burlywood", weight=3];
113[label="wz5/GT",fontsize=10,color="white",style="solid",shape="box"];14 -> 113[label="",style="solid", color="burlywood", weight=9];
113 -> 21[label="",style="solid", color="burlywood", weight=3];
15[label="FiniteMap.foldFM_LE1 wz3 wz4 wz5 GT wz61 wz62 wz63 wz64 (GT <= wz5)\n",fontsize=16,color="burlywood",shape="box"];114[label="wz5/LT",fontsize=10,color="white",style="solid",shape="box"];15 -> 114[label="",style="solid", color="burlywood", weight=9];
114 -> 22[label="",style="solid", color="burlywood", weight=3];
115[label="wz5/EQ",fontsize=10,color="white",style="solid",shape="box"];15 -> 115[label="",style="solid", color="burlywood", weight=9];
115 -> 23[label="",style="solid", color="burlywood", weight=3];
116[label="wz5/GT",fontsize=10,color="white",style="solid",shape="box"];15 -> 116[label="",style="solid", color="burlywood", weight=9];
116 -> 24[label="",style="solid", color="burlywood", weight=3];
16[label="FiniteMap.foldFM_LE1 wz3 wz4 LT LT wz61 wz62 wz63 wz64 (LT <= LT)\n",fontsize=16,color="black",shape="box"];16 -> 25[label="",style="solid", color="black", weight=3];
17[label="FiniteMap.foldFM_LE1 wz3 wz4 EQ LT wz61 wz62 wz63 wz64 (LT <= EQ)\n",fontsize=16,color="black",shape="box"];17 -> 26[label="",style="solid", color="black", weight=3];
18[label="FiniteMap.foldFM_LE1 wz3 wz4 GT LT wz61 wz62 wz63 wz64 (LT <= GT)\n",fontsize=16,color="black",shape="box"];18 -> 27[label="",style="solid", color="black", weight=3];
19[label="FiniteMap.foldFM_LE1 wz3 wz4 LT EQ wz61 wz62 wz63 wz64 (EQ <= LT)\n",fontsize=16,color="black",shape="box"];19 -> 28[label="",style="solid", color="black", weight=3];
20[label="FiniteMap.foldFM_LE1 wz3 wz4 EQ EQ wz61 wz62 wz63 wz64 (EQ <= EQ)\n",fontsize=16,color="black",shape="box"];20 -> 29[label="",style="solid", color="black", weight=3];
21[label="FiniteMap.foldFM_LE1 wz3 wz4 GT EQ wz61 wz62 wz63 wz64 (EQ <= GT)\n",fontsize=16,color="black",shape="box"];21 -> 30[label="",style="solid", color="black", weight=3];
22[label="FiniteMap.foldFM_LE1 wz3 wz4 LT GT wz61 wz62 wz63 wz64 (GT <= LT)\n",fontsize=16,color="black",shape="box"];22 -> 31[label="",style="solid", color="black", weight=3];
23[label="FiniteMap.foldFM_LE1 wz3 wz4 EQ GT wz61 wz62 wz63 wz64 (GT <= EQ)\n",fontsize=16,color="black",shape="box"];23 -> 32[label="",style="solid", color="black", weight=3];
24[label="FiniteMap.foldFM_LE1 wz3 wz4 GT GT wz61 wz62 wz63 wz64 (GT <= GT)\n",fontsize=16,color="black",shape="box"];24 -> 33[label="",style="solid", color="black", weight=3];
25[label="FiniteMap.foldFM_LE1 wz3 wz4 LT LT wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];25 -> 34[label="",style="solid", color="black", weight=3];
26[label="FiniteMap.foldFM_LE1 wz3 wz4 EQ LT wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];26 -> 35[label="",style="solid", color="black", weight=3];
27[label="FiniteMap.foldFM_LE1 wz3 wz4 GT LT wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];27 -> 36[label="",style="solid", color="black", weight=3];
28[label="FiniteMap.foldFM_LE1 wz3 wz4 LT EQ wz61 wz62 wz63 wz64 False\n",fontsize=16,color="black",shape="box"];28 -> 37[label="",style="solid", color="black", weight=3];
29[label="FiniteMap.foldFM_LE1 wz3 wz4 EQ EQ wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];29 -> 38[label="",style="solid", color="black", weight=3];
30[label="FiniteMap.foldFM_LE1 wz3 wz4 GT EQ wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];30 -> 39[label="",style="solid", color="black", weight=3];
31[label="FiniteMap.foldFM_LE1 wz3 wz4 LT GT wz61 wz62 wz63 wz64 False\n",fontsize=16,color="black",shape="box"];31 -> 40[label="",style="solid", color="black", weight=3];
32[label="FiniteMap.foldFM_LE1 wz3 wz4 EQ GT wz61 wz62 wz63 wz64 False\n",fontsize=16,color="black",shape="box"];32 -> 41[label="",style="solid", color="black", weight=3];
33[label="FiniteMap.foldFM_LE1 wz3 wz4 GT GT wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];33 -> 42[label="",style="solid", color="black", weight=3];
34 -> 6[label="",style="dashed", color="red", weight=0];
34[label="FiniteMap.foldFM_LE wz3 (wz3 LT wz61 (FiniteMap.foldFM_LE wz3 wz4 LT wz63)) LT wz64\n",fontsize=16,color="magenta"];34 -> 43[label="",style="dashed", color="magenta", weight=3];
34 -> 44[label="",style="dashed", color="magenta", weight=3];
34 -> 45[label="",style="dashed", color="magenta", weight=3];
35 -> 6[label="",style="dashed", color="red", weight=0];
35[label="FiniteMap.foldFM_LE wz3 (wz3 LT wz61 (FiniteMap.foldFM_LE wz3 wz4 EQ wz63)) EQ wz64\n",fontsize=16,color="magenta"];35 -> 46[label="",style="dashed", color="magenta", weight=3];
35 -> 47[label="",style="dashed", color="magenta", weight=3];
35 -> 48[label="",style="dashed", color="magenta", weight=3];
36 -> 6[label="",style="dashed", color="red", weight=0];
36[label="FiniteMap.foldFM_LE wz3 (wz3 LT wz61 (FiniteMap.foldFM_LE wz3 wz4 GT wz63)) GT wz64\n",fontsize=16,color="magenta"];36 -> 49[label="",style="dashed", color="magenta", weight=3];
36 -> 50[label="",style="dashed", color="magenta", weight=3];
36 -> 51[label="",style="dashed", color="magenta", weight=3];
37[label="FiniteMap.foldFM_LE0 wz3 wz4 LT EQ wz61 wz62 wz63 wz64 otherwise\n",fontsize=16,color="black",shape="box"];37 -> 52[label="",style="solid", color="black", weight=3];
38 -> 6[label="",style="dashed", color="red", weight=0];
38[label="FiniteMap.foldFM_LE wz3 (wz3 EQ wz61 (FiniteMap.foldFM_LE wz3 wz4 EQ wz63)) EQ wz64\n",fontsize=16,color="magenta"];38 -> 53[label="",style="dashed", color="magenta", weight=3];
38 -> 54[label="",style="dashed", color="magenta", weight=3];
38 -> 55[label="",style="dashed", color="magenta", weight=3];
39 -> 6[label="",style="dashed", color="red", weight=0];
39[label="FiniteMap.foldFM_LE wz3 (wz3 EQ wz61 (FiniteMap.foldFM_LE wz3 wz4 GT wz63)) GT wz64\n",fontsize=16,color="magenta"];39 -> 56[label="",style="dashed", color="magenta", weight=3];
39 -> 57[label="",style="dashed", color="magenta", weight=3];
39 -> 58[label="",style="dashed", color="magenta", weight=3];
40[label="FiniteMap.foldFM_LE0 wz3 wz4 LT GT wz61 wz62 wz63 wz64 otherwise\n",fontsize=16,color="black",shape="box"];40 -> 59[label="",style="solid", color="black", weight=3];
41[label="FiniteMap.foldFM_LE0 wz3 wz4 EQ GT wz61 wz62 wz63 wz64 otherwise\n",fontsize=16,color="black",shape="box"];41 -> 60[label="",style="solid", color="black", weight=3];
42 -> 6[label="",style="dashed", color="red", weight=0];
42[label="FiniteMap.foldFM_LE wz3 (wz3 GT wz61 (FiniteMap.foldFM_LE wz3 wz4 GT wz63)) GT wz64\n",fontsize=16,color="magenta"];42 -> 61[label="",style="dashed", color="magenta", weight=3];
42 -> 62[label="",style="dashed", color="magenta", weight=3];
42 -> 63[label="",style="dashed", color="magenta", weight=3];
43[label="wz64\n",fontsize=16,color="green",shape="box"];44[label="wz3 LT wz61 (FiniteMap.foldFM_LE wz3 wz4 LT wz63)\n",fontsize=16,color="green",shape="box"];44 -> 64[label="",style="dashed", color="green", weight=3];
44 -> 65[label="",style="dashed", color="green", weight=3];
44 -> 66[label="",style="dashed", color="green", weight=3];
45[label="LT\n",fontsize=16,color="green",shape="box"];46[label="wz64\n",fontsize=16,color="green",shape="box"];47[label="wz3 LT wz61 (FiniteMap.foldFM_LE wz3 wz4 EQ wz63)\n",fontsize=16,color="green",shape="box"];47 -> 67[label="",style="dashed", color="green", weight=3];
47 -> 68[label="",style="dashed", color="green", weight=3];
47 -> 69[label="",style="dashed", color="green", weight=3];
48[label="EQ\n",fontsize=16,color="green",shape="box"];49[label="wz64\n",fontsize=16,color="green",shape="box"];50[label="wz3 LT wz61 (FiniteMap.foldFM_LE wz3 wz4 GT wz63)\n",fontsize=16,color="green",shape="box"];50 -> 70[label="",style="dashed", color="green", weight=3];
50 -> 71[label="",style="dashed", color="green", weight=3];
50 -> 72[label="",style="dashed", color="green", weight=3];
51[label="GT\n",fontsize=16,color="green",shape="box"];52[label="FiniteMap.foldFM_LE0 wz3 wz4 LT EQ wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];52 -> 73[label="",style="solid", color="black", weight=3];
53[label="wz64\n",fontsize=16,color="green",shape="box"];54[label="wz3 EQ wz61 (FiniteMap.foldFM_LE wz3 wz4 EQ wz63)\n",fontsize=16,color="green",shape="box"];54 -> 74[label="",style="dashed", color="green", weight=3];
54 -> 75[label="",style="dashed", color="green", weight=3];
54 -> 76[label="",style="dashed", color="green", weight=3];
55[label="EQ\n",fontsize=16,color="green",shape="box"];56[label="wz64\n",fontsize=16,color="green",shape="box"];57[label="wz3 EQ wz61 (FiniteMap.foldFM_LE wz3 wz4 GT wz63)\n",fontsize=16,color="green",shape="box"];57 -> 77[label="",style="dashed", color="green", weight=3];
57 -> 78[label="",style="dashed", color="green", weight=3];
57 -> 79[label="",style="dashed", color="green", weight=3];
58[label="GT\n",fontsize=16,color="green",shape="box"];59[label="FiniteMap.foldFM_LE0 wz3 wz4 LT GT wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];59 -> 80[label="",style="solid", color="black", weight=3];
60[label="FiniteMap.foldFM_LE0 wz3 wz4 EQ GT wz61 wz62 wz63 wz64 True\n",fontsize=16,color="black",shape="box"];60 -> 81[label="",style="solid", color="black", weight=3];
61[label="wz64\n",fontsize=16,color="green",shape="box"];62[label="wz3 GT wz61 (FiniteMap.foldFM_LE wz3 wz4 GT wz63)\n",fontsize=16,color="green",shape="box"];62 -> 82[label="",style="dashed", color="green", weight=3];
62 -> 83[label="",style="dashed", color="green", weight=3];
62 -> 84[label="",style="dashed", color="green", weight=3];
63[label="GT\n",fontsize=16,color="green",shape="box"];64[label="LT\n",fontsize=16,color="green",shape="box"];65[label="wz61\n",fontsize=16,color="green",shape="box"];66 -> 6[label="",style="dashed", color="red", weight=0];
66[label="FiniteMap.foldFM_LE wz3 wz4 LT wz63\n",fontsize=16,color="magenta"];66 -> 85[label="",style="dashed", color="magenta", weight=3];
66 -> 86[label="",style="dashed", color="magenta", weight=3];
67[label="LT\n",fontsize=16,color="green",shape="box"];68[label="wz61\n",fontsize=16,color="green",shape="box"];69 -> 6[label="",style="dashed", color="red", weight=0];
69[label="FiniteMap.foldFM_LE wz3 wz4 EQ wz63\n",fontsize=16,color="magenta"];69 -> 87[label="",style="dashed", color="magenta", weight=3];
69 -> 88[label="",style="dashed", color="magenta", weight=3];
70[label="LT\n",fontsize=16,color="green",shape="box"];71[label="wz61\n",fontsize=16,color="green",shape="box"];72 -> 6[label="",style="dashed", color="red", weight=0];
72[label="FiniteMap.foldFM_LE wz3 wz4 GT wz63\n",fontsize=16,color="magenta"];72 -> 89[label="",style="dashed", color="magenta", weight=3];
72 -> 90[label="",style="dashed", color="magenta", weight=3];
73 -> 6[label="",style="dashed", color="red", weight=0];
73[label="FiniteMap.foldFM_LE wz3 wz4 LT wz63\n",fontsize=16,color="magenta"];73 -> 91[label="",style="dashed", color="magenta", weight=3];
73 -> 92[label="",style="dashed", color="magenta", weight=3];
74[label="EQ\n",fontsize=16,color="green",shape="box"];75[label="wz61\n",fontsize=16,color="green",shape="box"];76 -> 6[label="",style="dashed", color="red", weight=0];
76[label="FiniteMap.foldFM_LE wz3 wz4 EQ wz63\n",fontsize=16,color="magenta"];76 -> 93[label="",style="dashed", color="magenta", weight=3];
76 -> 94[label="",style="dashed", color="magenta", weight=3];
77[label="EQ\n",fontsize=16,color="green",shape="box"];78[label="wz61\n",fontsize=16,color="green",shape="box"];79 -> 6[label="",style="dashed", color="red", weight=0];
79[label="FiniteMap.foldFM_LE wz3 wz4 GT wz63\n",fontsize=16,color="magenta"];79 -> 95[label="",style="dashed", color="magenta", weight=3];
79 -> 96[label="",style="dashed", color="magenta", weight=3];
80 -> 6[label="",style="dashed", color="red", weight=0];
80[label="FiniteMap.foldFM_LE wz3 wz4 LT wz63\n",fontsize=16,color="magenta"];80 -> 97[label="",style="dashed", color="magenta", weight=3];
80 -> 98[label="",style="dashed", color="magenta", weight=3];
81 -> 6[label="",style="dashed", color="red", weight=0];
81[label="FiniteMap.foldFM_LE wz3 wz4 EQ wz63\n",fontsize=16,color="magenta"];81 -> 99[label="",style="dashed", color="magenta", weight=3];
81 -> 100[label="",style="dashed", color="magenta", weight=3];
82[label="GT\n",fontsize=16,color="green",shape="box"];83[label="wz61\n",fontsize=16,color="green",shape="box"];84 -> 6[label="",style="dashed", color="red", weight=0];
84[label="FiniteMap.foldFM_LE wz3 wz4 GT wz63\n",fontsize=16,color="magenta"];84 -> 101[label="",style="dashed", color="magenta", weight=3];
84 -> 102[label="",style="dashed", color="magenta", weight=3];
85[label="wz63\n",fontsize=16,color="green",shape="box"];86[label="LT\n",fontsize=16,color="green",shape="box"];87[label="wz63\n",fontsize=16,color="green",shape="box"];88[label="EQ\n",fontsize=16,color="green",shape="box"];89[label="wz63\n",fontsize=16,color="green",shape="box"];90[label="GT\n",fontsize=16,color="green",shape="box"];91[label="wz63\n",fontsize=16,color="green",shape="box"];92[label="LT\n",fontsize=16,color="green",shape="box"];93[label="wz63\n",fontsize=16,color="green",shape="box"];94[label="EQ\n",fontsize=16,color="green",shape="box"];95[label="wz63\n",fontsize=16,color="green",shape="box"];96[label="GT\n",fontsize=16,color="green",shape="box"];97[label="wz63\n",fontsize=16,color="green",shape="box"];98[label="LT\n",fontsize=16,color="green",shape="box"];99[label="wz63\n",fontsize=16,color="green",shape="box"];100[label="EQ\n",fontsize=16,color="green",shape="box"];101[label="wz63\n",fontsize=16,color="green",shape="box"];102[label="GT\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

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

new_foldFM_LE(wz3, GT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
new_foldFM_LE(wz3, LT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)
new_foldFM_LE(wz3, EQ, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
new_foldFM_LE(wz3, GT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
new_foldFM_LE(wz3, LT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz64, h, ba)
new_foldFM_LE(wz3, GT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
new_foldFM_LE(wz3, GT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
new_foldFM_LE(wz3, GT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
new_foldFM_LE(wz3, LT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)
new_foldFM_LE(wz3, EQ, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz64, h, ba)
new_foldFM_LE(wz3, EQ, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
new_foldFM_LE(wz3, EQ, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz64, h, ba)
new_foldFM_LE(wz3, GT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
new_foldFM_LE(wz3, EQ, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
new_foldFM_LE(wz3, LT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)

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 3 SCCs.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

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

new_foldFM_LE(wz3, EQ, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
new_foldFM_LE(wz3, EQ, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
new_foldFM_LE(wz3, EQ, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz64, h, ba)
new_foldFM_LE(wz3, EQ, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz64, h, ba)
new_foldFM_LE(wz3, EQ, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)

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_LE(wz3, EQ, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz64, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, EQ, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, EQ, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, EQ, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz64, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, EQ, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, EQ, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

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

new_foldFM_LE(wz3, LT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)
new_foldFM_LE(wz3, LT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz64, h, ba)
new_foldFM_LE(wz3, LT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)
new_foldFM_LE(wz3, LT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)

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

new_foldFM_LE(wz3, LT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz64, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, LT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, LT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, LT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, LT, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 2, 3 > 3, 4 >= 4, 5 >= 5

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

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

new_foldFM_LE(wz3, GT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
new_foldFM_LE(wz3, GT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
new_foldFM_LE(wz3, GT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
new_foldFM_LE(wz3, GT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
new_foldFM_LE(wz3, GT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
new_foldFM_LE(wz3, GT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)

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

new_foldFM_LE(wz3, GT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, GT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, GT, Branch(LT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, GT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz64, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, GT, Branch(GT, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 2, 3 > 3, 4 >= 4, 5 >= 5
new_foldFM_LE(wz3, GT, Branch(EQ, wz61, wz62, wz63, wz64), h, ba) → new_foldFM_LE(wz3, GT, wz63, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5

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