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

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

↳ HASKELL

  ↳ LR

mainModule Main

((Monad.ap :: IO (a -> b) -> IO a -> IO b) :: IO (a -> b) -> IO a -> IO b)

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

ap :: Monad a => a (c -> b) -> a c -> a b

liftM2 id

liftM2 :: Monad d => (c -> b -> a) -> d c -> d b -> d a

liftM2

f m1 m2

m1 >>= (\x1 ->m2 >>= (\x2 ->return (f x1 x2)))

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\x2→return (f x1 x2)

is transformed to

liftM20 f x1 x2 = return (f x1 x2)

The following Lambda expression

\x1→m2 >>= liftM20 f x1

is transformed to

liftM21 m2 f x1 = m2 >>= liftM20 f x1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

((Monad.ap :: IO (b -> a) -> IO b -> IO a) :: IO (b -> a) -> IO b -> 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

ap :: Monad a => a (b -> c) -> a b -> a c

liftM2 id

liftM2 :: Monad b => (c -> d -> a) -> b c -> b d -> b a

liftM2

f m1 m2

m1 >>= liftM21 m2 f

liftM20

f x1 x2

return (f x1 x2)

liftM21

m2 f x1

m2 >>= liftM20 f x1

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((Monad.ap :: IO (b -> a) -> IO b -> IO a) :: IO (b -> a) -> IO b -> IO a)

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

ap :: Monad c => c (b -> a) -> c b -> c a

liftM2 id

liftM2 :: Monad d => (c -> a -> b) -> d c -> d a -> d b

liftM2

f m1 m2

m1 >>= liftM21 m2 f

liftM20

f x1 x2

return (f x1 x2)

liftM21

m2 f x1

m2 >>= liftM20 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.ap :: IO (a -> b) -> IO a -> IO b)

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

ap :: Monad c => c (a -> b) -> c a -> c b

liftM2 id

liftM2 :: Monad c => (a -> b -> d) -> c a -> c b -> c d

liftM2

f m1 m2

m1 >>= liftM21 m2 f

liftM20

f x1 x2

return (f x1 x2)

liftM21

m2 f x1

m2 >>= liftM20 f x1

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="Monad.ap\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="Monad.ap vy3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="Monad.ap vy3 vy4\n",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="Monad.liftM2 id vy3 vy4\n",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="vy3 >>= Monad.liftM21 vy4 id\n",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="primbindIO vy3 (Monad.liftM21 vy4 id)\n",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="terminator vy3 (Monad.liftM21 vy4 id)\n",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="ter0m vy3 (Monad.liftM21 vy4 id)\n",fontsize=16,color="green",shape="box"];9 -> 10[label="",style="dashed", color="green", weight=3];
9 -> 11[label="",style="dashed", color="green", weight=3];
10[label="vy3\n",fontsize=16,color="green",shape="box"];11[label="Monad.liftM21 vy4 id\n",fontsize=16,color="grey",shape="box"];11 -> 12[label="",style="dashed", color="grey", weight=3];
12[label="Monad.liftM21 vy4 id vy5\n",fontsize=16,color="black",shape="triangle"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="vy4 >>= Monad.liftM20 id vy5\n",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="primbindIO vy4 (Monad.liftM20 id vy5)\n",fontsize=16,color="black",shape="box"];14 -> 15[label="",style="solid", color="black", weight=3];
15[label="terminator vy4 (Monad.liftM20 id vy5)\n",fontsize=16,color="black",shape="box"];15 -> 16[label="",style="solid", color="black", weight=3];
16[label="ter1m vy4 (Monad.liftM20 id vy5)\n",fontsize=16,color="green",shape="box"];16 -> 17[label="",style="dashed", color="green", weight=3];
16 -> 18[label="",style="dashed", color="green", weight=3];
17[label="vy4\n",fontsize=16,color="green",shape="box"];18[label="Monad.liftM20 id vy5\n",fontsize=16,color="grey",shape="box"];18 -> 19[label="",style="dashed", color="grey", weight=3];
19[label="Monad.liftM20 id vy5 vy6\n",fontsize=16,color="black",shape="triangle"];19 -> 20[label="",style="solid", color="black", weight=3];
20[label="return (id vy5 vy6)\n",fontsize=16,color="black",shape="box"];20 -> 21[label="",style="solid", color="black", weight=3];
21[label="primretIO (id vy5 vy6)\n",fontsize=16,color="black",shape="box"];21 -> 22[label="",style="solid", color="black", weight=3];
22[label="terminator (id vy5 vy6)\n",fontsize=16,color="black",shape="box"];22 -> 23[label="",style="solid", color="black", weight=3];
23[label="ter2m (id vy5 vy6)\n",fontsize=16,color="green",shape="box"];23 -> 24[label="",style="dashed", color="green", weight=3];
24[label="id vy5 vy6\n",fontsize=16,color="black",shape="box"];24 -> 25[label="",style="solid", color="black", weight=3];
25[label="vy5 vy6\n",fontsize=16,color="green",shape="box"];25 -> 26[label="",style="dashed", color="green", weight=3];
26[label="vy6\n",fontsize=16,color="green",shape="box"];}