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

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

↳ HASKELL

  ↳ IFR

mainModule Main

((Monad.when :: Bool -> IO () -> IO ()) :: Bool -> IO () -> IO ())

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

when :: Monad a => Bool -> a () -> a ()

when

p s

if p then s else return ()

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

If Reductions:
The following If expression

if p then s else return ()

is transformed to

when0 s True = s

when0 s False = return ()

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule Main

((Monad.when :: Bool -> IO () -> IO ()) :: Bool -> IO () -> IO ())

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

when :: Monad a => Bool -> a () -> a ()

when

p s

when0 s p

when0	s True	=	s
when0	s False	=	return ()

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((Monad.when :: Bool -> IO () -> IO ()) :: Bool -> IO () -> IO ())

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

when :: Monad a => Bool -> a () -> a ()

when

p s

when0 s p

when0	s True	=	s
when0	s False	=	return ()

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

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(Monad.when :: Bool -> IO () -> IO ())

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

when :: Monad a => Bool -> a () -> a ()

when

p s

when0 s p

when0	s True	=	s
when0	s False	=	return ()

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="Monad.when\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="Monad.when vy3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="Monad.when vy3 vy4\n",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="Monad.when0 vy4 vy3\n",fontsize=16,color="burlywood",shape="box"];14[label="vy3/False",fontsize=10,color="white",style="solid",shape="box"];5 -> 14[label="",style="solid", color="burlywood", weight=9];
14 -> 6[label="",style="solid", color="burlywood", weight=3];
15[label="vy3/True",fontsize=10,color="white",style="solid",shape="box"];5 -> 15[label="",style="solid", color="burlywood", weight=9];
15 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="Monad.when0 vy4 False\n",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="Monad.when0 vy4 True\n",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="return ()\n",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="vy4\n",fontsize=16,color="green",shape="box"];10[label="primretIO ()\n",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="terminator ()\n",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="ter0m ()\n",fontsize=16,color="green",shape="box"];12 -> 13[label="",style="dashed", color="green", weight=3];
13[label="()\n",fontsize=16,color="green",shape="box"];}