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

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

↳ HASKELL

  ↳ CR

mainModule Main

((FiniteMap.minFM :: (Ord b, Ord a) => FiniteMap.FiniteMap (a,b) c -> Maybe (a,b)) :: (Ord a, Ord b) => FiniteMap.FiniteMap (a,b) c -> Maybe (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)

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

minFM

EmptyFM

Nothing

minFM

(Branch key _ _ fm_l _)

case	minFM fm_l of
	Nothing	->	Just key
	Just key1	->	Just key1

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 minFM fm_l of
Nothing → Just key

Just key1 → Just key1

is transformed to

minFM0 key Nothing = Just key

minFM0 key (Just key1) = Just key1

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule Main

((FiniteMap.minFM :: (Ord c, Ord b) => FiniteMap.FiniteMap (c,b) a -> Maybe (c,b)) :: (Ord c, Ord b) => FiniteMap.FiniteMap (c,b) a -> Maybe (c,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)

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

minFM	EmptyFM	=	Nothing
minFM	(Branch key _ _ fm_l _)	=	minFM0 key (minFM fm_l)

minFM0	key Nothing	=	Just key
minFM0	key (Just key1)	=	Just key1

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

          ↳ NumRed

mainModule Main

((FiniteMap.minFM :: (Ord b, Ord c) => FiniteMap.FiniteMap (b,c) a -> Maybe (b,c)) :: (Ord b, Ord c) => FiniteMap.FiniteMap (b,c) a -> Maybe (b,c))

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)

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

minFM	EmptyFM	=	Nothing
minFM	(Branch key vw vx fm_l vy)	=	minFM0 key (minFM fm_l)

minFM0	key Nothing	=	Just key
minFM0	key (Just key1)	=	Just key1

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

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(FiniteMap.minFM :: (Ord a, Ord b) => FiniteMap.FiniteMap (b,a) c -> Maybe (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)

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

minFM	EmptyFM	=	Nothing
minFM	(Branch key vw vx fm_l vy)	=	minFM0 key (minFM fm_l)

minFM0	key Nothing	=	Just key
minFM0	key (Just key1)	=	Just key1

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.minFM\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="FiniteMap.minFM wv3\n",fontsize=16,color="burlywood",shape="triangle"];15[label="wv3/FiniteMap.EmptyFM",fontsize=10,color="white",style="solid",shape="box"];3 -> 15[label="",style="solid", color="burlywood", weight=9];
15 -> 4[label="",style="solid", color="burlywood", weight=3];
16[label="wv3/FiniteMap.Branch wv30 wv31 wv32 wv33 wv34",fontsize=10,color="white",style="solid",shape="box"];3 -> 16[label="",style="solid", color="burlywood", weight=9];
16 -> 5[label="",style="solid", color="burlywood", weight=3];
4[label="FiniteMap.minFM FiniteMap.EmptyFM\n",fontsize=16,color="black",shape="box"];4 -> 6[label="",style="solid", color="black", weight=3];
5[label="FiniteMap.minFM (FiniteMap.Branch wv30 wv31 wv32 wv33 wv34)\n",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="Nothing\n",fontsize=16,color="green",shape="box"];7 -> 8[label="",style="dashed", color="red", weight=0];
7[label="FiniteMap.minFM0 wv30 (FiniteMap.minFM wv33)\n",fontsize=16,color="magenta"];7 -> 9[label="",style="dashed", color="magenta", weight=3];
9 -> 3[label="",style="dashed", color="red", weight=0];
9[label="FiniteMap.minFM wv33\n",fontsize=16,color="magenta"];9 -> 10[label="",style="dashed", color="magenta", weight=3];
8[label="FiniteMap.minFM0 wv30 wv4\n",fontsize=16,color="burlywood",shape="triangle"];19[label="wv4/Nothing",fontsize=10,color="white",style="solid",shape="box"];8 -> 19[label="",style="solid", color="burlywood", weight=9];
19 -> 11[label="",style="solid", color="burlywood", weight=3];
20[label="wv4/Just wv40",fontsize=10,color="white",style="solid",shape="box"];8 -> 20[label="",style="solid", color="burlywood", weight=9];
20 -> 12[label="",style="solid", color="burlywood", weight=3];
10[label="wv33\n",fontsize=16,color="green",shape="box"];11[label="FiniteMap.minFM0 wv30 Nothing\n",fontsize=16,color="black",shape="box"];11 -> 13[label="",style="solid", color="black", weight=3];
12[label="FiniteMap.minFM0 wv30 (Just wv40)\n",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="Just wv30\n",fontsize=16,color="green",shape="box"];14[label="Just wv40\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ QDPSizeChangeProof

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

new_minFM(Branch(wv30, wv31, wv32, wv33, wv34), h, ba, bb) → new_minFM(wv33, h, ba, bb)

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_minFM(Branch(wv30, wv31, wv32, wv33, wv34), h, ba, bb) → new_minFM(wv33, h, ba, bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4