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

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

↳ HASKELL

  ↳ CR

mainModule Main

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

lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b

lookupFM

EmptyFM key

Nothing

lookupFM

(Branch key elt _ fm_l fm_r) key_to_find

key_to_find < key

lookupFM fm_l key_to_find

key_to_find > key

lookupFM fm_r key_to_find

otherwise

Just elt

lookupWithDefaultFM :: Ord a => FiniteMap a b -> b -> a -> b

lookupWithDefaultFM

fm deflt key

case	lookupFM fm key of
	Nothing	->	deflt
	Just elt	->	elt

module Main where

import qualified FiniteMap
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified FiniteMap
import qualified Main
import qualified Prelude

Case Reductions:
The following Case expression

case lookupFM fm key of
Nothing → deflt

Just elt → elt

is transformed to

lookupWithDefaultFM0 deflt Nothing = deflt

lookupWithDefaultFM0 deflt (Just elt) = elt

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule Main

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

lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a

lookupFM

EmptyFM key

Nothing

lookupFM

(Branch key elt _ fm_l fm_r) key_to_find

key_to_find < key

lookupFM fm_l key_to_find

key_to_find > key

lookupFM fm_r key_to_find

otherwise

Just elt

lookupWithDefaultFM :: Ord b => FiniteMap b a -> a -> b -> a

lookupWithDefaultFM

fm deflt key

lookupWithDefaultFM0 deflt (lookupFM fm key)

lookupWithDefaultFM0	deflt Nothing	=	deflt
lookupWithDefaultFM0	deflt (Just elt)	=	elt

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

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

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

lookupFM :: Ord b => FiniteMap b a -> b -> Maybe a

lookupFM

EmptyFM key

Nothing

lookupFM

(Branch key elt vw fm_l fm_r) key_to_find

key_to_find < key

lookupFM fm_l key_to_find

key_to_find > key

lookupFM fm_r key_to_find

otherwise

Just elt

lookupWithDefaultFM :: Ord a => FiniteMap a b -> b -> a -> b

lookupWithDefaultFM

fm deflt key

lookupWithDefaultFM0 deflt (lookupFM fm key)

lookupWithDefaultFM0	deflt Nothing	=	deflt
lookupWithDefaultFM0	deflt (Just elt)	=	elt

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

lookupFM EmptyFM key = Nothing

lookupFM (Branch key elt vw fm_l fm_r) key_to_find

| key_to_find < key

= lookupFM fm_l key_to_find

| key_to_find > key

= lookupFM fm_r key_to_find

| otherwise

= Just elt

is transformed to

lookupFM EmptyFM key = lookupFM4 EmptyFM key

lookupFM (Branch key elt vw fm_l fm_r) key_to_find = lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find

lookupFM1 key elt vw fm_l fm_r key_to_find True = lookupFM fm_r key_to_find

lookupFM1 key elt vw fm_l fm_r key_to_find False = lookupFM0 key elt vw fm_l fm_r key_to_find otherwise

lookupFM0 key elt vw fm_l fm_r key_to_find True = Just elt

lookupFM2 key elt vw fm_l fm_r key_to_find True = lookupFM fm_l key_to_find

lookupFM2 key elt vw fm_l fm_r key_to_find False = lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key)

lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find = lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key)

lookupFM4 EmptyFM key = Nothing

lookupFM4 wv ww = lookupFM3 wv ww

The following Function with conditions

compare x y

| x == y

= EQ

| x <= y

= LT

| otherwise

= GT

is transformed to

compare x y = compare3 x y

compare2 x y True = EQ

compare2 x y False = compare1 x y (x <= y)

compare1 x y True = LT

compare1 x y False = compare0 x y otherwise

compare0 x y True = GT

compare3 x y = compare2 x y (x == y)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

mainModule Main

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

lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b

lookupFM	EmptyFM key	=	lookupFM4 EmptyFM key
lookupFM	(Branch key elt vw fm_l fm_r) key_to_find	=	lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find

lookupFM0

key elt vw fm_l fm_r key_to_find True

Just elt

lookupFM1	key elt vw fm_l fm_r key_to_find True	=	lookupFM fm_r key_to_find
lookupFM1	key elt vw fm_l fm_r key_to_find False	=	lookupFM0 key elt vw fm_l fm_r key_to_find otherwise

lookupFM2	key elt vw fm_l fm_r key_to_find True	=	lookupFM fm_l key_to_find
lookupFM2	key elt vw fm_l fm_r key_to_find False	=	lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key)

lookupFM3

(Branch key elt vw fm_l fm_r) key_to_find

lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key)

lookupFM4	EmptyFM key	=	Nothing
lookupFM4	wv ww	=	lookupFM3 wv ww

lookupWithDefaultFM :: Ord b => FiniteMap b a -> a -> b -> a

lookupWithDefaultFM

fm deflt key

lookupWithDefaultFM0 deflt (lookupFM fm key)

lookupWithDefaultFM0	deflt Nothing	=	deflt
lookupWithDefaultFM0	deflt (Just elt)	=	elt

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

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

mainModule Main

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

lookupFM :: Ord a => FiniteMap a b -> a -> Maybe b

lookupFM	EmptyFM key	=	lookupFM4 EmptyFM key
lookupFM	(Branch key elt vw fm_l fm_r) key_to_find	=	lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find

lookupFM0

key elt vw fm_l fm_r key_to_find True

Just elt

lookupFM1	key elt vw fm_l fm_r key_to_find True	=	lookupFM fm_r key_to_find
lookupFM1	key elt vw fm_l fm_r key_to_find False	=	lookupFM0 key elt vw fm_l fm_r key_to_find otherwise

lookupFM2	key elt vw fm_l fm_r key_to_find True	=	lookupFM fm_l key_to_find
lookupFM2	key elt vw fm_l fm_r key_to_find False	=	lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key)

lookupFM3

(Branch key elt vw fm_l fm_r) key_to_find

lookupFM2 key elt vw fm_l fm_r key_to_find (key_to_find < key)

lookupFM4	EmptyFM key	=	Nothing
lookupFM4	wv ww	=	lookupFM3 wv ww

lookupWithDefaultFM :: Ord a => FiniteMap a b -> b -> a -> b

lookupWithDefaultFM

fm deflt key

lookupWithDefaultFM0 deflt (lookupFM fm key)

lookupWithDefaultFM0	deflt Nothing	=	deflt
lookupWithDefaultFM0	deflt (Just elt)	=	elt

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.lookupWithDefaultFM\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="FiniteMap.lookupWithDefaultFM wx3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="FiniteMap.lookupWithDefaultFM wx3 wx4\n",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="FiniteMap.lookupWithDefaultFM wx3 wx4 wx5\n",fontsize=16,color="black",shape="triangle"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM wx3 wx5)\n",fontsize=16,color="burlywood",shape="triangle"];156[label="wx3/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];6 -> 156[label="",style="solid", color="burlywood", weight=9];
156 -> 7[label="",style="solid", color="burlywood", weight=3];
157[label="wx3/FiniteMap.Branch wx30 wx31 wx32 wx33 wx34",fontsize=10,color="white",style="solid",shape="box"];6 -> 157[label="",style="solid", color="burlywood", weight=9];
157 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM FiniteMap.EmptyFM wx5)\n",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM (FiniteMap.Branch wx30 wx31 wx32 wx33 wx34) wx5)\n",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM4 FiniteMap.EmptyFM wx5)\n",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM3 (FiniteMap.Branch wx30 wx31 wx32 wx33 wx34) wx5)\n",fontsize=16,color="black",shape="box"];10 -> 12[label="",style="solid", color="black", weight=3];
11[label="FiniteMap.lookupWithDefaultFM0 wx4 Nothing\n",fontsize=16,color="black",shape="box"];11 -> 13[label="",style="solid", color="black", weight=3];
12[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 wx30 wx31 wx32 wx33 wx34 wx5 (wx5 < wx30))\n",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="wx4\n",fontsize=16,color="green",shape="box"];14[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 wx30 wx31 wx32 wx33 wx34 wx5 (compare wx5 wx30 == LT))\n",fontsize=16,color="black",shape="box"];14 -> 15[label="",style="solid", color="black", weight=3];
15[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 wx30 wx31 wx32 wx33 wx34 wx5 (compare3 wx5 wx30 == LT))\n",fontsize=16,color="black",shape="box"];15 -> 16[label="",style="solid", color="black", weight=3];
16[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 wx30 wx31 wx32 wx33 wx34 wx5 (compare2 wx5 wx30 (wx5 == wx30) == LT))\n",fontsize=16,color="burlywood",shape="box"];158[label="wx5/LT",fontsize=10,color="white",style="solid",shape="box"];16 -> 158[label="",style="solid", color="burlywood", weight=9];
158 -> 17[label="",style="solid", color="burlywood", weight=3];
159[label="wx5/EQ",fontsize=10,color="white",style="solid",shape="box"];16 -> 159[label="",style="solid", color="burlywood", weight=9];
159 -> 18[label="",style="solid", color="burlywood", weight=3];
160[label="wx5/GT",fontsize=10,color="white",style="solid",shape="box"];16 -> 160[label="",style="solid", color="burlywood", weight=9];
160 -> 19[label="",style="solid", color="burlywood", weight=3];
17[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 wx30 wx31 wx32 wx33 wx34 LT (compare2 LT wx30 (LT == wx30) == LT))\n",fontsize=16,color="burlywood",shape="box"];161[label="wx30/LT",fontsize=10,color="white",style="solid",shape="box"];17 -> 161[label="",style="solid", color="burlywood", weight=9];
161 -> 20[label="",style="solid", color="burlywood", weight=3];
162[label="wx30/EQ",fontsize=10,color="white",style="solid",shape="box"];17 -> 162[label="",style="solid", color="burlywood", weight=9];
162 -> 21[label="",style="solid", color="burlywood", weight=3];
163[label="wx30/GT",fontsize=10,color="white",style="solid",shape="box"];17 -> 163[label="",style="solid", color="burlywood", weight=9];
163 -> 22[label="",style="solid", color="burlywood", weight=3];
18[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 wx30 wx31 wx32 wx33 wx34 EQ (compare2 EQ wx30 (EQ == wx30) == LT))\n",fontsize=16,color="burlywood",shape="box"];164[label="wx30/LT",fontsize=10,color="white",style="solid",shape="box"];18 -> 164[label="",style="solid", color="burlywood", weight=9];
164 -> 23[label="",style="solid", color="burlywood", weight=3];
165[label="wx30/EQ",fontsize=10,color="white",style="solid",shape="box"];18 -> 165[label="",style="solid", color="burlywood", weight=9];
165 -> 24[label="",style="solid", color="burlywood", weight=3];
166[label="wx30/GT",fontsize=10,color="white",style="solid",shape="box"];18 -> 166[label="",style="solid", color="burlywood", weight=9];
166 -> 25[label="",style="solid", color="burlywood", weight=3];
19[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 wx30 wx31 wx32 wx33 wx34 GT (compare2 GT wx30 (GT == wx30) == LT))\n",fontsize=16,color="burlywood",shape="box"];167[label="wx30/LT",fontsize=10,color="white",style="solid",shape="box"];19 -> 167[label="",style="solid", color="burlywood", weight=9];
167 -> 26[label="",style="solid", color="burlywood", weight=3];
168[label="wx30/EQ",fontsize=10,color="white",style="solid",shape="box"];19 -> 168[label="",style="solid", color="burlywood", weight=9];
168 -> 27[label="",style="solid", color="burlywood", weight=3];
169[label="wx30/GT",fontsize=10,color="white",style="solid",shape="box"];19 -> 169[label="",style="solid", color="burlywood", weight=9];
169 -> 28[label="",style="solid", color="burlywood", weight=3];
20[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 LT (compare2 LT LT (LT == LT) == LT))\n",fontsize=16,color="black",shape="box"];20 -> 29[label="",style="solid", color="black", weight=3];
21[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 LT (compare2 LT EQ (LT == EQ) == LT))\n",fontsize=16,color="black",shape="box"];21 -> 30[label="",style="solid", color="black", weight=3];
22[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 LT (compare2 LT GT (LT == GT) == LT))\n",fontsize=16,color="black",shape="box"];22 -> 31[label="",style="solid", color="black", weight=3];
23[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ (compare2 EQ LT (EQ == LT) == LT))\n",fontsize=16,color="black",shape="box"];23 -> 32[label="",style="solid", color="black", weight=3];
24[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 EQ (compare2 EQ EQ (EQ == EQ) == LT))\n",fontsize=16,color="black",shape="box"];24 -> 33[label="",style="solid", color="black", weight=3];
25[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 EQ (compare2 EQ GT (EQ == GT) == LT))\n",fontsize=16,color="black",shape="box"];25 -> 34[label="",style="solid", color="black", weight=3];
26[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT (compare2 GT LT (GT == LT) == LT))\n",fontsize=16,color="black",shape="box"];26 -> 35[label="",style="solid", color="black", weight=3];
27[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT (compare2 GT EQ (GT == EQ) == LT))\n",fontsize=16,color="black",shape="box"];27 -> 36[label="",style="solid", color="black", weight=3];
28[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 GT (compare2 GT GT (GT == GT) == LT))\n",fontsize=16,color="black",shape="box"];28 -> 37[label="",style="solid", color="black", weight=3];
29[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 LT (compare2 LT LT True == LT))\n",fontsize=16,color="black",shape="box"];29 -> 38[label="",style="solid", color="black", weight=3];
30[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 LT (compare2 LT EQ False == LT))\n",fontsize=16,color="black",shape="box"];30 -> 39[label="",style="solid", color="black", weight=3];
31[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 LT (compare2 LT GT False == LT))\n",fontsize=16,color="black",shape="box"];31 -> 40[label="",style="solid", color="black", weight=3];
32[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ (compare2 EQ LT False == LT))\n",fontsize=16,color="black",shape="box"];32 -> 41[label="",style="solid", color="black", weight=3];
33[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 EQ (compare2 EQ EQ True == LT))\n",fontsize=16,color="black",shape="box"];33 -> 42[label="",style="solid", color="black", weight=3];
34[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 EQ (compare2 EQ GT False == LT))\n",fontsize=16,color="black",shape="box"];34 -> 43[label="",style="solid", color="black", weight=3];
35[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT (compare2 GT LT False == LT))\n",fontsize=16,color="black",shape="box"];35 -> 44[label="",style="solid", color="black", weight=3];
36[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT (compare2 GT EQ False == LT))\n",fontsize=16,color="black",shape="box"];36 -> 45[label="",style="solid", color="black", weight=3];
37[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 GT (compare2 GT GT True == LT))\n",fontsize=16,color="black",shape="box"];37 -> 46[label="",style="solid", color="black", weight=3];
38[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 LT (EQ == LT))\n",fontsize=16,color="black",shape="box"];38 -> 47[label="",style="solid", color="black", weight=3];
39[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 LT (compare1 LT EQ (LT <= EQ) == LT))\n",fontsize=16,color="black",shape="box"];39 -> 48[label="",style="solid", color="black", weight=3];
40[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 LT (compare1 LT GT (LT <= GT) == LT))\n",fontsize=16,color="black",shape="box"];40 -> 49[label="",style="solid", color="black", weight=3];
41[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ (compare1 EQ LT (EQ <= LT) == LT))\n",fontsize=16,color="black",shape="box"];41 -> 50[label="",style="solid", color="black", weight=3];
42[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 EQ (EQ == LT))\n",fontsize=16,color="black",shape="box"];42 -> 51[label="",style="solid", color="black", weight=3];
43[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 EQ (compare1 EQ GT (EQ <= GT) == LT))\n",fontsize=16,color="black",shape="box"];43 -> 52[label="",style="solid", color="black", weight=3];
44[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT (compare1 GT LT (GT <= LT) == LT))\n",fontsize=16,color="black",shape="box"];44 -> 53[label="",style="solid", color="black", weight=3];
45[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT (compare1 GT EQ (GT <= EQ) == LT))\n",fontsize=16,color="black",shape="box"];45 -> 54[label="",style="solid", color="black", weight=3];
46[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 GT (EQ == LT))\n",fontsize=16,color="black",shape="box"];46 -> 55[label="",style="solid", color="black", weight=3];
47[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 LT False)\n",fontsize=16,color="black",shape="box"];47 -> 56[label="",style="solid", color="black", weight=3];
48[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 LT (compare1 LT EQ True == LT))\n",fontsize=16,color="black",shape="box"];48 -> 57[label="",style="solid", color="black", weight=3];
49[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 LT (compare1 LT GT True == LT))\n",fontsize=16,color="black",shape="box"];49 -> 58[label="",style="solid", color="black", weight=3];
50[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ (compare1 EQ LT False == LT))\n",fontsize=16,color="black",shape="box"];50 -> 59[label="",style="solid", color="black", weight=3];
51[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 EQ False)\n",fontsize=16,color="black",shape="box"];51 -> 60[label="",style="solid", color="black", weight=3];
52[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 EQ (compare1 EQ GT True == LT))\n",fontsize=16,color="black",shape="box"];52 -> 61[label="",style="solid", color="black", weight=3];
53[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT (compare1 GT LT False == LT))\n",fontsize=16,color="black",shape="box"];53 -> 62[label="",style="solid", color="black", weight=3];
54[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT (compare1 GT EQ False == LT))\n",fontsize=16,color="black",shape="box"];54 -> 63[label="",style="solid", color="black", weight=3];
55[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 GT False)\n",fontsize=16,color="black",shape="box"];55 -> 64[label="",style="solid", color="black", weight=3];
56[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 LT (LT > LT))\n",fontsize=16,color="black",shape="box"];56 -> 65[label="",style="solid", color="black", weight=3];
57[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 LT (LT == LT))\n",fontsize=16,color="black",shape="box"];57 -> 66[label="",style="solid", color="black", weight=3];
58[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 LT (LT == LT))\n",fontsize=16,color="black",shape="box"];58 -> 67[label="",style="solid", color="black", weight=3];
59[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ (compare0 EQ LT otherwise == LT))\n",fontsize=16,color="black",shape="box"];59 -> 68[label="",style="solid", color="black", weight=3];
60[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 EQ (EQ > EQ))\n",fontsize=16,color="black",shape="box"];60 -> 69[label="",style="solid", color="black", weight=3];
61[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 EQ (LT == LT))\n",fontsize=16,color="black",shape="box"];61 -> 70[label="",style="solid", color="black", weight=3];
62[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT (compare0 GT LT otherwise == LT))\n",fontsize=16,color="black",shape="box"];62 -> 71[label="",style="solid", color="black", weight=3];
63[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT (compare0 GT EQ otherwise == LT))\n",fontsize=16,color="black",shape="box"];63 -> 72[label="",style="solid", color="black", weight=3];
64[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 GT wx31 wx32 wx33 wx34 GT (GT > GT))\n",fontsize=16,color="black",shape="box"];64 -> 73[label="",style="solid", color="black", weight=3];
65[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 LT (compare LT LT == GT))\n",fontsize=16,color="black",shape="box"];65 -> 74[label="",style="solid", color="black", weight=3];
66[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 LT True)\n",fontsize=16,color="black",shape="box"];66 -> 75[label="",style="solid", color="black", weight=3];
67[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 LT True)\n",fontsize=16,color="black",shape="box"];67 -> 76[label="",style="solid", color="black", weight=3];
68[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ (compare0 EQ LT True == LT))\n",fontsize=16,color="black",shape="box"];68 -> 77[label="",style="solid", color="black", weight=3];
69[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 EQ (compare EQ EQ == GT))\n",fontsize=16,color="black",shape="box"];69 -> 78[label="",style="solid", color="black", weight=3];
70[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 GT wx31 wx32 wx33 wx34 EQ True)\n",fontsize=16,color="black",shape="box"];70 -> 79[label="",style="solid", color="black", weight=3];
71[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT (compare0 GT LT True == LT))\n",fontsize=16,color="black",shape="box"];71 -> 80[label="",style="solid", color="black", weight=3];
72[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT (compare0 GT EQ True == LT))\n",fontsize=16,color="black",shape="box"];72 -> 81[label="",style="solid", color="black", weight=3];
73[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 GT wx31 wx32 wx33 wx34 GT (compare GT GT == GT))\n",fontsize=16,color="black",shape="box"];73 -> 82[label="",style="solid", color="black", weight=3];
74[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 LT (compare3 LT LT == GT))\n",fontsize=16,color="black",shape="box"];74 -> 83[label="",style="solid", color="black", weight=3];
75 -> 6[label="",style="dashed", color="red", weight=0];
75[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM wx33 LT)\n",fontsize=16,color="magenta"];75 -> 84[label="",style="dashed", color="magenta", weight=3];
75 -> 85[label="",style="dashed", color="magenta", weight=3];
76 -> 6[label="",style="dashed", color="red", weight=0];
76[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM wx33 LT)\n",fontsize=16,color="magenta"];76 -> 86[label="",style="dashed", color="magenta", weight=3];
76 -> 87[label="",style="dashed", color="magenta", weight=3];
77[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ (GT == LT))\n",fontsize=16,color="black",shape="box"];77 -> 88[label="",style="solid", color="black", weight=3];
78[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 EQ (compare3 EQ EQ == GT))\n",fontsize=16,color="black",shape="box"];78 -> 89[label="",style="solid", color="black", weight=3];
79 -> 6[label="",style="dashed", color="red", weight=0];
79[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM wx33 EQ)\n",fontsize=16,color="magenta"];79 -> 90[label="",style="dashed", color="magenta", weight=3];
79 -> 91[label="",style="dashed", color="magenta", weight=3];
80[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT (GT == LT))\n",fontsize=16,color="black",shape="box"];80 -> 92[label="",style="solid", color="black", weight=3];
81[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT (GT == LT))\n",fontsize=16,color="black",shape="box"];81 -> 93[label="",style="solid", color="black", weight=3];
82[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 GT wx31 wx32 wx33 wx34 GT (compare3 GT GT == GT))\n",fontsize=16,color="black",shape="box"];82 -> 94[label="",style="solid", color="black", weight=3];
83[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 LT (compare2 LT LT (LT == LT) == GT))\n",fontsize=16,color="black",shape="box"];83 -> 95[label="",style="solid", color="black", weight=3];
84[label="wx33\n",fontsize=16,color="green",shape="box"];85[label="LT\n",fontsize=16,color="green",shape="box"];86[label="wx33\n",fontsize=16,color="green",shape="box"];87[label="LT\n",fontsize=16,color="green",shape="box"];88[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 EQ False)\n",fontsize=16,color="black",shape="box"];88 -> 96[label="",style="solid", color="black", weight=3];
89[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 EQ (compare2 EQ EQ (EQ == EQ) == GT))\n",fontsize=16,color="black",shape="box"];89 -> 97[label="",style="solid", color="black", weight=3];
90[label="wx33\n",fontsize=16,color="green",shape="box"];91[label="EQ\n",fontsize=16,color="green",shape="box"];92[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 LT wx31 wx32 wx33 wx34 GT False)\n",fontsize=16,color="black",shape="box"];92 -> 98[label="",style="solid", color="black", weight=3];
93[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM2 EQ wx31 wx32 wx33 wx34 GT False)\n",fontsize=16,color="black",shape="box"];93 -> 99[label="",style="solid", color="black", weight=3];
94[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 GT wx31 wx32 wx33 wx34 GT (compare2 GT GT (GT == GT) == GT))\n",fontsize=16,color="black",shape="box"];94 -> 100[label="",style="solid", color="black", weight=3];
95[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 LT (compare2 LT LT True == GT))\n",fontsize=16,color="black",shape="box"];95 -> 101[label="",style="solid", color="black", weight=3];
96[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (EQ > LT))\n",fontsize=16,color="black",shape="box"];96 -> 102[label="",style="solid", color="black", weight=3];
97[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 EQ (compare2 EQ EQ True == GT))\n",fontsize=16,color="black",shape="box"];97 -> 103[label="",style="solid", color="black", weight=3];
98[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (GT > LT))\n",fontsize=16,color="black",shape="box"];98 -> 104[label="",style="solid", color="black", weight=3];
99[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (GT > EQ))\n",fontsize=16,color="black",shape="box"];99 -> 105[label="",style="solid", color="black", weight=3];
100[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 GT wx31 wx32 wx33 wx34 GT (compare2 GT GT True == GT))\n",fontsize=16,color="black",shape="box"];100 -> 106[label="",style="solid", color="black", weight=3];
101[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 LT (EQ == GT))\n",fontsize=16,color="black",shape="box"];101 -> 107[label="",style="solid", color="black", weight=3];
102[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare EQ LT == GT))\n",fontsize=16,color="black",shape="box"];102 -> 108[label="",style="solid", color="black", weight=3];
103[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 EQ (EQ == GT))\n",fontsize=16,color="black",shape="box"];103 -> 109[label="",style="solid", color="black", weight=3];
104[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare GT LT == GT))\n",fontsize=16,color="black",shape="box"];104 -> 110[label="",style="solid", color="black", weight=3];
105[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare GT EQ == GT))\n",fontsize=16,color="black",shape="box"];105 -> 111[label="",style="solid", color="black", weight=3];
106[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 GT wx31 wx32 wx33 wx34 GT (EQ == GT))\n",fontsize=16,color="black",shape="box"];106 -> 112[label="",style="solid", color="black", weight=3];
107[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 LT False)\n",fontsize=16,color="black",shape="box"];107 -> 113[label="",style="solid", color="black", weight=3];
108[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare3 EQ LT == GT))\n",fontsize=16,color="black",shape="box"];108 -> 114[label="",style="solid", color="black", weight=3];
109[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 EQ False)\n",fontsize=16,color="black",shape="box"];109 -> 115[label="",style="solid", color="black", weight=3];
110[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare3 GT LT == GT))\n",fontsize=16,color="black",shape="box"];110 -> 116[label="",style="solid", color="black", weight=3];
111[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare3 GT EQ == GT))\n",fontsize=16,color="black",shape="box"];111 -> 117[label="",style="solid", color="black", weight=3];
112[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 GT wx31 wx32 wx33 wx34 GT False)\n",fontsize=16,color="black",shape="box"];112 -> 118[label="",style="solid", color="black", weight=3];
113[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM0 LT wx31 wx32 wx33 wx34 LT otherwise)\n",fontsize=16,color="black",shape="box"];113 -> 119[label="",style="solid", color="black", weight=3];
114[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare2 EQ LT (EQ == LT) == GT))\n",fontsize=16,color="black",shape="box"];114 -> 120[label="",style="solid", color="black", weight=3];
115[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM0 EQ wx31 wx32 wx33 wx34 EQ otherwise)\n",fontsize=16,color="black",shape="box"];115 -> 121[label="",style="solid", color="black", weight=3];
116[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare2 GT LT (GT == LT) == GT))\n",fontsize=16,color="black",shape="box"];116 -> 122[label="",style="solid", color="black", weight=3];
117[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare2 GT EQ (GT == EQ) == GT))\n",fontsize=16,color="black",shape="box"];117 -> 123[label="",style="solid", color="black", weight=3];
118[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM0 GT wx31 wx32 wx33 wx34 GT otherwise)\n",fontsize=16,color="black",shape="box"];118 -> 124[label="",style="solid", color="black", weight=3];
119[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM0 LT wx31 wx32 wx33 wx34 LT True)\n",fontsize=16,color="black",shape="box"];119 -> 125[label="",style="solid", color="black", weight=3];
120[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare2 EQ LT False == GT))\n",fontsize=16,color="black",shape="box"];120 -> 126[label="",style="solid", color="black", weight=3];
121[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM0 EQ wx31 wx32 wx33 wx34 EQ True)\n",fontsize=16,color="black",shape="box"];121 -> 127[label="",style="solid", color="black", weight=3];
122[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare2 GT LT False == GT))\n",fontsize=16,color="black",shape="box"];122 -> 128[label="",style="solid", color="black", weight=3];
123[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare2 GT EQ False == GT))\n",fontsize=16,color="black",shape="box"];123 -> 129[label="",style="solid", color="black", weight=3];
124[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM0 GT wx31 wx32 wx33 wx34 GT True)\n",fontsize=16,color="black",shape="box"];124 -> 130[label="",style="solid", color="black", weight=3];
125[label="FiniteMap.lookupWithDefaultFM0 wx4 (Just wx31)\n",fontsize=16,color="black",shape="triangle"];125 -> 131[label="",style="solid", color="black", weight=3];
126[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare1 EQ LT (EQ <= LT) == GT))\n",fontsize=16,color="black",shape="box"];126 -> 132[label="",style="solid", color="black", weight=3];
127 -> 125[label="",style="dashed", color="red", weight=0];
127[label="FiniteMap.lookupWithDefaultFM0 wx4 (Just wx31)\n",fontsize=16,color="magenta"];128[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare1 GT LT (GT <= LT) == GT))\n",fontsize=16,color="black",shape="box"];128 -> 133[label="",style="solid", color="black", weight=3];
129[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare1 GT EQ (GT <= EQ) == GT))\n",fontsize=16,color="black",shape="box"];129 -> 134[label="",style="solid", color="black", weight=3];
130 -> 125[label="",style="dashed", color="red", weight=0];
130[label="FiniteMap.lookupWithDefaultFM0 wx4 (Just wx31)\n",fontsize=16,color="magenta"];131[label="wx31\n",fontsize=16,color="green",shape="box"];132[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare1 EQ LT False == GT))\n",fontsize=16,color="black",shape="box"];132 -> 135[label="",style="solid", color="black", weight=3];
133[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare1 GT LT False == GT))\n",fontsize=16,color="black",shape="box"];133 -> 136[label="",style="solid", color="black", weight=3];
134[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare1 GT EQ False == GT))\n",fontsize=16,color="black",shape="box"];134 -> 137[label="",style="solid", color="black", weight=3];
135[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare0 EQ LT otherwise == GT))\n",fontsize=16,color="black",shape="box"];135 -> 138[label="",style="solid", color="black", weight=3];
136[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare0 GT LT otherwise == GT))\n",fontsize=16,color="black",shape="box"];136 -> 139[label="",style="solid", color="black", weight=3];
137[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare0 GT EQ otherwise == GT))\n",fontsize=16,color="black",shape="box"];137 -> 140[label="",style="solid", color="black", weight=3];
138[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (compare0 EQ LT True == GT))\n",fontsize=16,color="black",shape="box"];138 -> 141[label="",style="solid", color="black", weight=3];
139[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (compare0 GT LT True == GT))\n",fontsize=16,color="black",shape="box"];139 -> 142[label="",style="solid", color="black", weight=3];
140[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (compare0 GT EQ True == GT))\n",fontsize=16,color="black",shape="box"];140 -> 143[label="",style="solid", color="black", weight=3];
141[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ (GT == GT))\n",fontsize=16,color="black",shape="box"];141 -> 144[label="",style="solid", color="black", weight=3];
142[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT (GT == GT))\n",fontsize=16,color="black",shape="box"];142 -> 145[label="",style="solid", color="black", weight=3];
143[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT (GT == GT))\n",fontsize=16,color="black",shape="box"];143 -> 146[label="",style="solid", color="black", weight=3];
144[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 EQ True)\n",fontsize=16,color="black",shape="box"];144 -> 147[label="",style="solid", color="black", weight=3];
145[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 LT wx31 wx32 wx33 wx34 GT True)\n",fontsize=16,color="black",shape="box"];145 -> 148[label="",style="solid", color="black", weight=3];
146[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM1 EQ wx31 wx32 wx33 wx34 GT True)\n",fontsize=16,color="black",shape="box"];146 -> 149[label="",style="solid", color="black", weight=3];
147 -> 6[label="",style="dashed", color="red", weight=0];
147[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM wx34 EQ)\n",fontsize=16,color="magenta"];147 -> 150[label="",style="dashed", color="magenta", weight=3];
147 -> 151[label="",style="dashed", color="magenta", weight=3];
148 -> 6[label="",style="dashed", color="red", weight=0];
148[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM wx34 GT)\n",fontsize=16,color="magenta"];148 -> 152[label="",style="dashed", color="magenta", weight=3];
148 -> 153[label="",style="dashed", color="magenta", weight=3];
149 -> 6[label="",style="dashed", color="red", weight=0];
149[label="FiniteMap.lookupWithDefaultFM0 wx4 (FiniteMap.lookupFM wx34 GT)\n",fontsize=16,color="magenta"];149 -> 154[label="",style="dashed", color="magenta", weight=3];
149 -> 155[label="",style="dashed", color="magenta", weight=3];
150[label="wx34\n",fontsize=16,color="green",shape="box"];151[label="EQ\n",fontsize=16,color="green",shape="box"];152[label="wx34\n",fontsize=16,color="green",shape="box"];153[label="GT\n",fontsize=16,color="green",shape="box"];154[label="wx34\n",fontsize=16,color="green",shape="box"];155[label="GT\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ NumRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ QDP

                      ↳ DependencyGraphProof

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

new_lookupWithDefaultFM0(wx4, Branch(GT, wx31, wx32, wx33, wx34), LT, h) → new_lookupWithDefaultFM0(wx4, wx33, LT, h)
new_lookupWithDefaultFM0(wx4, Branch(LT, wx31, wx32, wx33, wx34), EQ, h) → new_lookupWithDefaultFM0(wx4, wx34, EQ, h)
new_lookupWithDefaultFM0(wx4, Branch(EQ, wx31, wx32, wx33, wx34), GT, h) → new_lookupWithDefaultFM0(wx4, wx34, GT, h)
new_lookupWithDefaultFM0(wx4, Branch(LT, wx31, wx32, wx33, wx34), GT, h) → new_lookupWithDefaultFM0(wx4, wx34, GT, h)
new_lookupWithDefaultFM0(wx4, Branch(EQ, wx31, wx32, wx33, wx34), LT, h) → new_lookupWithDefaultFM0(wx4, wx33, LT, h)
new_lookupWithDefaultFM0(wx4, Branch(GT, wx31, wx32, wx33, wx34), EQ, h) → new_lookupWithDefaultFM0(wx4, wx33, EQ, 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 3 SCCs.

↳ HASKELL

  ↳ CR

    ↳ 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_lookupWithDefaultFM0(wx4, Branch(EQ, wx31, wx32, wx33, wx34), GT, h) → new_lookupWithDefaultFM0(wx4, wx34, GT, h)
new_lookupWithDefaultFM0(wx4, Branch(LT, wx31, wx32, wx33, wx34), GT, h) → new_lookupWithDefaultFM0(wx4, wx34, GT, 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_lookupWithDefaultFM0(wx4, Branch(LT, wx31, wx32, wx33, wx34), GT, h) → new_lookupWithDefaultFM0(wx4, wx34, GT, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4
new_lookupWithDefaultFM0(wx4, Branch(EQ, wx31, wx32, wx33, wx34), GT, h) → new_lookupWithDefaultFM0(wx4, wx34, GT, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ CR

    ↳ 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_lookupWithDefaultFM0(wx4, Branch(LT, wx31, wx32, wx33, wx34), EQ, h) → new_lookupWithDefaultFM0(wx4, wx34, EQ, h)
new_lookupWithDefaultFM0(wx4, Branch(GT, wx31, wx32, wx33, wx34), EQ, h) → new_lookupWithDefaultFM0(wx4, wx33, EQ, h)

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

new_lookupWithDefaultFM0(wx4, Branch(GT, wx31, wx32, wx33, wx34), EQ, h) → new_lookupWithDefaultFM0(wx4, wx33, EQ, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4
new_lookupWithDefaultFM0(wx4, Branch(LT, wx31, wx32, wx33, wx34), EQ, h) → new_lookupWithDefaultFM0(wx4, wx34, EQ, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ CR

    ↳ 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_lookupWithDefaultFM0(wx4, Branch(GT, wx31, wx32, wx33, wx34), LT, h) → new_lookupWithDefaultFM0(wx4, wx33, LT, h)
new_lookupWithDefaultFM0(wx4, Branch(EQ, wx31, wx32, wx33, wx34), LT, h) → new_lookupWithDefaultFM0(wx4, wx33, LT, h)

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

new_lookupWithDefaultFM0(wx4, Branch(EQ, wx31, wx32, wx33, wx34), LT, h) → new_lookupWithDefaultFM0(wx4, wx33, LT, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4
new_lookupWithDefaultFM0(wx4, Branch(GT, wx31, wx32, wx33, wx34), LT, h) → new_lookupWithDefaultFM0(wx4, wx33, LT, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4

lookupWithDefaultFM0	deflt Nothing	= deflt
lookupWithDefaultFM0	deflt (Just elt)	= elt

lookupFM	EmptyFM key	= lookupFM4 EmptyFM key
lookupFM	(Branch key elt vw fm_l fm_r) key_to_find	= lookupFM3 (Branch key elt vw fm_l fm_r) key_to_find

lookupFM1	key elt vw fm_l fm_r key_to_find True	= lookupFM fm_r key_to_find
lookupFM1	key elt vw fm_l fm_r key_to_find False	= lookupFM0 key elt vw fm_l fm_r key_to_find otherwise

lookupFM2	key elt vw fm_l fm_r key_to_find True	= lookupFM fm_l key_to_find
lookupFM2	key elt vw fm_l fm_r key_to_find False	= lookupFM1 key elt vw fm_l fm_r key_to_find (key_to_find > key)

lookupFM4	EmptyFM key	= Nothing
lookupFM4	wv ww	= lookupFM3 wv ww

compare2	x y True	= EQ
compare2	x y False	= compare1 x y (x <= y)

compare1	x y True	= LT
compare1	x y False	= compare0 x y otherwise