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

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

↳ HASKELL

  ↳ LR

mainModule Main

((Monad.liftM5 :: (d -> f -> a -> b -> c -> e) -> IO d -> IO f -> IO a -> IO b -> IO c -> IO e) :: (d -> f -> a -> b -> c -> e) -> IO d -> IO f -> IO a -> IO b -> IO c -> IO e)

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

liftM5 :: Monad b => (f -> e -> d -> a -> g -> c) -> b f -> b e -> b d -> b a -> b g -> b c

liftM5

f m1 m2 m3 m4 m5

m1 >>= (\x1 ->m2 >>= (\x2 ->m3 >>= (\x3 ->m4 >>= (\x4 ->m5 >>= (\x5 ->return (f x1 x2 x3 x4 x5))))))

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\x5→return (f x1 x2 x3 x4 x5)

is transformed to

liftM50 f x1 x2 x3 x4 x5 = return (f x1 x2 x3 x4 x5)

The following Lambda expression

\x4→m5 >>= liftM50 f x1 x2 x3 x4

is transformed to

liftM51 m5 f x1 x2 x3 x4 = m5 >>= liftM50 f x1 x2 x3 x4

The following Lambda expression

\x3→m4 >>= liftM51 m5 f x1 x2 x3

is transformed to

liftM52 m4 m5 f x1 x2 x3 = m4 >>= liftM51 m5 f x1 x2 x3

The following Lambda expression

\x2→m3 >>= liftM52 m4 m5 f x1 x2

is transformed to

liftM53 m3 m4 m5 f x1 x2 = m3 >>= liftM52 m4 m5 f x1 x2

The following Lambda expression

\x1→m2 >>= liftM53 m3 m4 m5 f x1

is transformed to

liftM54 m2 m3 m4 m5 f x1 = m2 >>= liftM53 m3 m4 m5 f x1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

((Monad.liftM5 :: (b -> f -> e -> c -> d -> a) -> IO b -> IO f -> IO e -> IO c -> IO d -> IO a) :: (b -> f -> e -> c -> d -> a) -> IO b -> IO f -> IO e -> IO c -> IO d -> IO a)

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

liftM5 :: Monad g => (c -> f -> d -> e -> b -> a) -> g c -> g f -> g d -> g e -> g b -> g a

liftM5

f m1 m2 m3 m4 m5

m1 >>= liftM54 m2 m3 m4 m5 f

liftM50

f x1 x2 x3 x4 x5

return (f x1 x2 x3 x4 x5)

liftM51

m5 f x1 x2 x3 x4

m5 >>= liftM50 f x1 x2 x3 x4

liftM52

m4 m5 f x1 x2 x3

m4 >>= liftM51 m5 f x1 x2 x3

liftM53

m3 m4 m5 f x1 x2

m3 >>= liftM52 m4 m5 f x1 x2

liftM54

m2 m3 m4 m5 f x1

m2 >>= liftM53 m3 m4 m5 f x1

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((Monad.liftM5 :: (c -> f -> a -> e -> b -> d) -> IO c -> IO f -> IO a -> IO e -> IO b -> IO d) :: (c -> f -> a -> e -> b -> d) -> IO c -> IO f -> IO a -> IO e -> IO b -> IO d)

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

liftM5 :: Monad a => (b -> d -> e -> c -> g -> f) -> a b -> a d -> a e -> a c -> a g -> a f

liftM5

f m1 m2 m3 m4 m5

m1 >>= liftM54 m2 m3 m4 m5 f

liftM50

f x1 x2 x3 x4 x5

return (f x1 x2 x3 x4 x5)

liftM51

m5 f x1 x2 x3 x4

m5 >>= liftM50 f x1 x2 x3 x4

liftM52

m4 m5 f x1 x2 x3

m4 >>= liftM51 m5 f x1 x2 x3

liftM53

m3 m4 m5 f x1 x2

m3 >>= liftM52 m4 m5 f x1 x2

liftM54

m2 m3 m4 m5 f x1

m2 >>= liftM53 m3 m4 m5 f x1

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

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

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(Monad.liftM5 :: (b -> f -> e -> c -> d -> a) -> IO b -> IO f -> IO e -> IO c -> IO d -> IO a)

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

liftM5 :: Monad c => (d -> a -> g -> b -> f -> e) -> c d -> c a -> c g -> c b -> c f -> c e

liftM5

f m1 m2 m3 m4 m5

m1 >>= liftM54 m2 m3 m4 m5 f

liftM50

f x1 x2 x3 x4 x5

return (f x1 x2 x3 x4 x5)

liftM51

m5 f x1 x2 x3 x4

m5 >>= liftM50 f x1 x2 x3 x4

liftM52

m4 m5 f x1 x2 x3

m4 >>= liftM51 m5 f x1 x2 x3

liftM53

m3 m4 m5 f x1 x2

m3 >>= liftM52 m4 m5 f x1 x2

liftM54

m2 m3 m4 m5 f x1

m2 >>= liftM53 m3 m4 m5 f x1

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="Monad.liftM5\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="Monad.liftM5 vy3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="Monad.liftM5 vy3 vy4\n",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="Monad.liftM5 vy3 vy4 vy5\n",fontsize=16,color="grey",shape="box"];5 -> 6[label="",style="dashed", color="grey", weight=3];
6[label="Monad.liftM5 vy3 vy4 vy5 vy6\n",fontsize=16,color="grey",shape="box"];6 -> 7[label="",style="dashed", color="grey", weight=3];
7[label="Monad.liftM5 vy3 vy4 vy5 vy6 vy7\n",fontsize=16,color="grey",shape="box"];7 -> 8[label="",style="dashed", color="grey", weight=3];
8[label="Monad.liftM5 vy3 vy4 vy5 vy6 vy7 vy8\n",fontsize=16,color="black",shape="triangle"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="vy4 >>= Monad.liftM54 vy5 vy6 vy7 vy8 vy3\n",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="primbindIO vy4 (Monad.liftM54 vy5 vy6 vy7 vy8 vy3)\n",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="terminator vy4 (Monad.liftM54 vy5 vy6 vy7 vy8 vy3)\n",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="ter0m vy4 (Monad.liftM54 vy5 vy6 vy7 vy8 vy3)\n",fontsize=16,color="green",shape="box"];12 -> 13[label="",style="dashed", color="green", weight=3];
12 -> 14[label="",style="dashed", color="green", weight=3];
13[label="vy4\n",fontsize=16,color="green",shape="box"];14[label="Monad.liftM54 vy5 vy6 vy7 vy8 vy3\n",fontsize=16,color="grey",shape="box"];14 -> 15[label="",style="dashed", color="grey", weight=3];
15[label="Monad.liftM54 vy5 vy6 vy7 vy8 vy3 vy9\n",fontsize=16,color="black",shape="triangle"];15 -> 16[label="",style="solid", color="black", weight=3];
16[label="vy5 >>= Monad.liftM53 vy6 vy7 vy8 vy3 vy9\n",fontsize=16,color="black",shape="box"];16 -> 17[label="",style="solid", color="black", weight=3];
17[label="primbindIO vy5 (Monad.liftM53 vy6 vy7 vy8 vy3 vy9)\n",fontsize=16,color="black",shape="box"];17 -> 18[label="",style="solid", color="black", weight=3];
18[label="terminator vy5 (Monad.liftM53 vy6 vy7 vy8 vy3 vy9)\n",fontsize=16,color="black",shape="box"];18 -> 19[label="",style="solid", color="black", weight=3];
19[label="ter1m vy5 (Monad.liftM53 vy6 vy7 vy8 vy3 vy9)\n",fontsize=16,color="green",shape="box"];19 -> 20[label="",style="dashed", color="green", weight=3];
19 -> 21[label="",style="dashed", color="green", weight=3];
20[label="vy5\n",fontsize=16,color="green",shape="box"];21[label="Monad.liftM53 vy6 vy7 vy8 vy3 vy9\n",fontsize=16,color="grey",shape="box"];21 -> 22[label="",style="dashed", color="grey", weight=3];
22[label="Monad.liftM53 vy6 vy7 vy8 vy3 vy9 vy10\n",fontsize=16,color="black",shape="triangle"];22 -> 23[label="",style="solid", color="black", weight=3];
23[label="vy6 >>= Monad.liftM52 vy7 vy8 vy3 vy9 vy10\n",fontsize=16,color="black",shape="box"];23 -> 24[label="",style="solid", color="black", weight=3];
24[label="primbindIO vy6 (Monad.liftM52 vy7 vy8 vy3 vy9 vy10)\n",fontsize=16,color="black",shape="box"];24 -> 25[label="",style="solid", color="black", weight=3];
25[label="terminator vy6 (Monad.liftM52 vy7 vy8 vy3 vy9 vy10)\n",fontsize=16,color="black",shape="box"];25 -> 26[label="",style="solid", color="black", weight=3];
26[label="ter2m vy6 (Monad.liftM52 vy7 vy8 vy3 vy9 vy10)\n",fontsize=16,color="green",shape="box"];26 -> 27[label="",style="dashed", color="green", weight=3];
26 -> 28[label="",style="dashed", color="green", weight=3];
27[label="vy6\n",fontsize=16,color="green",shape="box"];28[label="Monad.liftM52 vy7 vy8 vy3 vy9 vy10\n",fontsize=16,color="grey",shape="box"];28 -> 29[label="",style="dashed", color="grey", weight=3];
29[label="Monad.liftM52 vy7 vy8 vy3 vy9 vy10 vy11\n",fontsize=16,color="black",shape="triangle"];29 -> 30[label="",style="solid", color="black", weight=3];
30[label="vy7 >>= Monad.liftM51 vy8 vy3 vy9 vy10 vy11\n",fontsize=16,color="black",shape="box"];30 -> 31[label="",style="solid", color="black", weight=3];
31[label="primbindIO vy7 (Monad.liftM51 vy8 vy3 vy9 vy10 vy11)\n",fontsize=16,color="black",shape="box"];31 -> 32[label="",style="solid", color="black", weight=3];
32[label="terminator vy7 (Monad.liftM51 vy8 vy3 vy9 vy10 vy11)\n",fontsize=16,color="black",shape="box"];32 -> 33[label="",style="solid", color="black", weight=3];
33[label="ter3m vy7 (Monad.liftM51 vy8 vy3 vy9 vy10 vy11)\n",fontsize=16,color="green",shape="box"];33 -> 34[label="",style="dashed", color="green", weight=3];
33 -> 35[label="",style="dashed", color="green", weight=3];
34[label="vy7\n",fontsize=16,color="green",shape="box"];35[label="Monad.liftM51 vy8 vy3 vy9 vy10 vy11\n",fontsize=16,color="grey",shape="box"];35 -> 36[label="",style="dashed", color="grey", weight=3];
36[label="Monad.liftM51 vy8 vy3 vy9 vy10 vy11 vy12\n",fontsize=16,color="black",shape="triangle"];36 -> 37[label="",style="solid", color="black", weight=3];
37[label="vy8 >>= Monad.liftM50 vy3 vy9 vy10 vy11 vy12\n",fontsize=16,color="black",shape="box"];37 -> 38[label="",style="solid", color="black", weight=3];
38[label="primbindIO vy8 (Monad.liftM50 vy3 vy9 vy10 vy11 vy12)\n",fontsize=16,color="black",shape="box"];38 -> 39[label="",style="solid", color="black", weight=3];
39[label="terminator vy8 (Monad.liftM50 vy3 vy9 vy10 vy11 vy12)\n",fontsize=16,color="black",shape="box"];39 -> 40[label="",style="solid", color="black", weight=3];
40[label="ter4m vy8 (Monad.liftM50 vy3 vy9 vy10 vy11 vy12)\n",fontsize=16,color="green",shape="box"];40 -> 41[label="",style="dashed", color="green", weight=3];
40 -> 42[label="",style="dashed", color="green", weight=3];
41[label="vy8\n",fontsize=16,color="green",shape="box"];42[label="Monad.liftM50 vy3 vy9 vy10 vy11 vy12\n",fontsize=16,color="grey",shape="box"];42 -> 43[label="",style="dashed", color="grey", weight=3];
43[label="Monad.liftM50 vy3 vy9 vy10 vy11 vy12 vy13\n",fontsize=16,color="black",shape="triangle"];43 -> 44[label="",style="solid", color="black", weight=3];
44[label="return (vy3 vy9 vy10 vy11 vy12 vy13)\n",fontsize=16,color="black",shape="box"];44 -> 45[label="",style="solid", color="black", weight=3];
45[label="primretIO (vy3 vy9 vy10 vy11 vy12 vy13)\n",fontsize=16,color="black",shape="box"];45 -> 46[label="",style="solid", color="black", weight=3];
46[label="terminator (vy3 vy9 vy10 vy11 vy12 vy13)\n",fontsize=16,color="black",shape="box"];46 -> 47[label="",style="solid", color="black", weight=3];
47[label="ter5m (vy3 vy9 vy10 vy11 vy12 vy13)\n",fontsize=16,color="green",shape="box"];47 -> 48[label="",style="dashed", color="green", weight=3];
48[label="vy3 vy9 vy10 vy11 vy12 vy13\n",fontsize=16,color="green",shape="box"];48 -> 49[label="",style="dashed", color="green", weight=3];
48 -> 50[label="",style="dashed", color="green", weight=3];
48 -> 51[label="",style="dashed", color="green", weight=3];
48 -> 52[label="",style="dashed", color="green", weight=3];
48 -> 53[label="",style="dashed", color="green", weight=3];
49[label="vy9\n",fontsize=16,color="green",shape="box"];50[label="vy10\n",fontsize=16,color="green",shape="box"];51[label="vy11\n",fontsize=16,color="green",shape="box"];52[label="vy12\n",fontsize=16,color="green",shape="box"];53[label="vy13\n",fontsize=16,color="green",shape="box"];}