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

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

↳ HASKELL

  ↳ LR

mainModule Main

((Monad.zipWithM :: (a -> c -> Maybe b) -> [a] -> [c] -> Maybe [b]) :: (a -> c -> Maybe b) -> [a] -> [c] -> Maybe [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

zipWithM :: Monad a => (b -> d -> a c) -> [b] -> [d] -> a [c]

zipWithM

f xs ys

sequence (zipWith f xs ys)

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\xs→return (x : xs)

is transformed to

sequence0 x xs = return (x : xs)

The following Lambda expression

\x→sequence cs >>= sequence0 x

is transformed to

sequence1 cs x = sequence cs >>= sequence0 x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

((Monad.zipWithM :: (c -> a -> Maybe b) -> [c] -> [a] -> Maybe [b]) :: (c -> a -> Maybe b) -> [c] -> [a] -> Maybe [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

zipWithM :: Monad a => (b -> c -> a d) -> [b] -> [c] -> a [d]

zipWithM

f xs ys

sequence (zipWith f xs ys)

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((Monad.zipWithM :: (a -> b -> Maybe c) -> [a] -> [b] -> Maybe [c]) :: (a -> b -> Maybe c) -> [a] -> [b] -> Maybe [c])

module Main where

import qualified Maybe
import qualified Monad
import qualified Prelude

module Monad where

import qualified Main
import qualified Maybe
import qualified Prelude

zipWithM :: Monad d => (a -> b -> d c) -> [a] -> [b] -> d [c]

zipWithM

f xs ys

sequence (zipWith f xs ys)

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.zipWithM :: (c -> a -> Maybe b) -> [c] -> [a] -> Maybe [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

zipWithM :: Monad c => (b -> d -> c a) -> [b] -> [d] -> c [a]

zipWithM

f xs ys

sequence (zipWith f xs ys)

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="Monad.zipWithM\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="Monad.zipWithM wv3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="Monad.zipWithM wv3 wv4\n",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="Monad.zipWithM wv3 wv4 wv5\n",fontsize=16,color="black",shape="triangle"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="sequence (zipWith wv3 wv4 wv5)\n",fontsize=16,color="burlywood",shape="triangle"];38[label="wv4/wv40 : wv41",fontsize=10,color="white",style="solid",shape="box"];6 -> 38[label="",style="solid", color="burlywood", weight=9];
38 -> 7[label="",style="solid", color="burlywood", weight=3];
39[label="wv4/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 39[label="",style="solid", color="burlywood", weight=9];
39 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="sequence (zipWith wv3 (wv40 : wv41) wv5)\n",fontsize=16,color="burlywood",shape="box"];40[label="wv5/wv50 : wv51",fontsize=10,color="white",style="solid",shape="box"];7 -> 40[label="",style="solid", color="burlywood", weight=9];
40 -> 9[label="",style="solid", color="burlywood", weight=3];
41[label="wv5/[]",fontsize=10,color="white",style="solid",shape="box"];7 -> 41[label="",style="solid", color="burlywood", weight=9];
41 -> 10[label="",style="solid", color="burlywood", weight=3];
8[label="sequence (zipWith wv3 [] wv5)\n",fontsize=16,color="black",shape="box"];8 -> 11[label="",style="solid", color="black", weight=3];
9[label="sequence (zipWith wv3 (wv40 : wv41) (wv50 : wv51))\n",fontsize=16,color="black",shape="box"];9 -> 12[label="",style="solid", color="black", weight=3];
10[label="sequence (zipWith wv3 (wv40 : wv41) [])\n",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="sequence []\n",fontsize=16,color="black",shape="triangle"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="sequence (wv3 wv40 wv50 : zipWith wv3 wv41 wv51)\n",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13 -> 11[label="",style="dashed", color="red", weight=0];
13[label="sequence []\n",fontsize=16,color="magenta"];14[label="return []\n",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15 -> 17[label="",style="dashed", color="red", weight=0];
15[label="wv3 wv40 wv50 >>= sequence1 (zipWith wv3 wv41 wv51)\n",fontsize=16,color="magenta"];15 -> 18[label="",style="dashed", color="magenta", weight=3];
16[label="Just []\n",fontsize=16,color="green",shape="box"];18[label="wv3 wv40 wv50\n",fontsize=16,color="green",shape="box"];18 -> 23[label="",style="dashed", color="green", weight=3];
18 -> 24[label="",style="dashed", color="green", weight=3];
17[label="wv6 >>= sequence1 (zipWith wv3 wv41 wv51)\n",fontsize=16,color="burlywood",shape="triangle"];44[label="wv6/Nothing",fontsize=10,color="white",style="solid",shape="box"];17 -> 44[label="",style="solid", color="burlywood", weight=9];
44 -> 21[label="",style="solid", color="burlywood", weight=3];
45[label="wv6/Just wv60",fontsize=10,color="white",style="solid",shape="box"];17 -> 45[label="",style="solid", color="burlywood", weight=9];
45 -> 22[label="",style="solid", color="burlywood", weight=3];
23[label="wv40\n",fontsize=16,color="green",shape="box"];24[label="wv50\n",fontsize=16,color="green",shape="box"];21[label="Nothing >>= sequence1 (zipWith wv3 wv41 wv51)\n",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="Just wv60 >>= sequence1 (zipWith wv3 wv41 wv51)\n",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
25[label="Nothing\n",fontsize=16,color="green",shape="box"];26[label="sequence1 (zipWith wv3 wv41 wv51) wv60\n",fontsize=16,color="black",shape="box"];26 -> 27[label="",style="solid", color="black", weight=3];
27 -> 28[label="",style="dashed", color="red", weight=0];
27[label="sequence (zipWith wv3 wv41 wv51) >>= sequence0 wv60\n",fontsize=16,color="magenta"];27 -> 29[label="",style="dashed", color="magenta", weight=3];
29 -> 6[label="",style="dashed", color="red", weight=0];
29[label="sequence (zipWith wv3 wv41 wv51)\n",fontsize=16,color="magenta"];29 -> 30[label="",style="dashed", color="magenta", weight=3];
29 -> 31[label="",style="dashed", color="magenta", weight=3];
28[label="wv7 >>= sequence0 wv60\n",fontsize=16,color="burlywood",shape="triangle"];48[label="wv7/Nothing",fontsize=10,color="white",style="solid",shape="box"];28 -> 48[label="",style="solid", color="burlywood", weight=9];
48 -> 32[label="",style="solid", color="burlywood", weight=3];
49[label="wv7/Just wv70",fontsize=10,color="white",style="solid",shape="box"];28 -> 49[label="",style="solid", color="burlywood", weight=9];
49 -> 33[label="",style="solid", color="burlywood", weight=3];
30[label="wv51\n",fontsize=16,color="green",shape="box"];31[label="wv41\n",fontsize=16,color="green",shape="box"];32[label="Nothing >>= sequence0 wv60\n",fontsize=16,color="black",shape="box"];32 -> 34[label="",style="solid", color="black", weight=3];
33[label="Just wv70 >>= sequence0 wv60\n",fontsize=16,color="black",shape="box"];33 -> 35[label="",style="solid", color="black", weight=3];
34[label="Nothing\n",fontsize=16,color="green",shape="box"];35[label="sequence0 wv60 wv70\n",fontsize=16,color="black",shape="box"];35 -> 36[label="",style="solid", color="black", weight=3];
36[label="return (wv60 : wv70)\n",fontsize=16,color="black",shape="box"];36 -> 37[label="",style="solid", color="black", weight=3];
37[label="Just (wv60 : wv70)\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ QDPSizeChangeProof

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

new_sequence(wv3, :(wv40, wv41), :(wv50, wv51), h, ba, bb) → new_gtGtEs(wv3, wv41, wv51, h, ba, bb)
new_gtGtEs(wv3, wv41, wv51, h, ba, bb) → new_sequence(wv3, wv41, wv51, 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_gtGtEs(wv3, wv41, wv51, h, ba, bb) → new_sequence(wv3, wv41, wv51, h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6
new_sequence(wv3, :(wv40, wv41), :(wv50, wv51), h, ba, bb) → new_gtGtEs(wv3, wv41, wv51, h, ba, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6