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

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 c => (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

Lambda Reductions:
The following Lambda expression

\_→q

is transformed to

gtGt0 q _ = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

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

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 => (c -> b -> a d) -> [c] -> [b] -> a ()

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

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

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 d => (a -> b -> d c) -> [a] -> [b] -> d ()

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_ ww3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="Monad.zipWithM_ ww3 ww4\n",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="Monad.zipWithM_ ww3 ww4 ww5\n",fontsize=16,color="black",shape="triangle"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="sequence_ (zipWith ww3 ww4 ww5)\n",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="foldr (>>) (return ()) (zipWith ww3 ww4 ww5)\n",fontsize=16,color="burlywood",shape="triangle"];34[label="ww4/ww40 : ww41",fontsize=10,color="white",style="solid",shape="box"];7 -> 34[label="",style="solid", color="burlywood", weight=9];
34 -> 8[label="",style="solid", color="burlywood", weight=3];
35[label="ww4/[]",fontsize=10,color="white",style="solid",shape="box"];7 -> 35[label="",style="solid", color="burlywood", weight=9];
35 -> 9[label="",style="solid", color="burlywood", weight=3];
8[label="foldr (>>) (return ()) (zipWith ww3 (ww40 : ww41) ww5)\n",fontsize=16,color="burlywood",shape="box"];36[label="ww5/ww50 : ww51",fontsize=10,color="white",style="solid",shape="box"];8 -> 36[label="",style="solid", color="burlywood", weight=9];
36 -> 10[label="",style="solid", color="burlywood", weight=3];
37[label="ww5/[]",fontsize=10,color="white",style="solid",shape="box"];8 -> 37[label="",style="solid", color="burlywood", weight=9];
37 -> 11[label="",style="solid", color="burlywood", weight=3];
9[label="foldr (>>) (return ()) (zipWith ww3 [] ww5)\n",fontsize=16,color="black",shape="box"];9 -> 12[label="",style="solid", color="black", weight=3];
10[label="foldr (>>) (return ()) (zipWith ww3 (ww40 : ww41) (ww50 : ww51))\n",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="foldr (>>) (return ()) (zipWith ww3 (ww40 : ww41) [])\n",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="foldr (>>) (return ()) []\n",fontsize=16,color="black",shape="triangle"];12 -> 15[label="",style="solid", color="black", weight=3];
13[label="foldr (>>) (return ()) (ww3 ww40 ww50 : zipWith ww3 ww41 ww51)\n",fontsize=16,color="black",shape="box"];13 -> 16[label="",style="solid", color="black", weight=3];
14 -> 12[label="",style="dashed", color="red", weight=0];
14[label="foldr (>>) (return ()) []\n",fontsize=16,color="magenta"];15[label="return ()\n",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16 -> 18[label="",style="dashed", color="red", weight=0];
16[label="(>>) ww3 ww40 ww50 foldr (>>) (return ()) (zipWith ww3 ww41 ww51)\n",fontsize=16,color="magenta"];16 -> 19[label="",style="dashed", color="magenta", weight=3];
17[label="Just ()\n",fontsize=16,color="green",shape="box"];19 -> 7[label="",style="dashed", color="red", weight=0];
19[label="foldr (>>) (return ()) (zipWith ww3 ww41 ww51)\n",fontsize=16,color="magenta"];19 -> 20[label="",style="dashed", color="magenta", weight=3];
19 -> 21[label="",style="dashed", color="magenta", weight=3];
18[label="(>>) ww3 ww40 ww50 ww6\n",fontsize=16,color="black",shape="triangle"];18 -> 22[label="",style="solid", color="black", weight=3];
20[label="ww41\n",fontsize=16,color="green",shape="box"];21[label="ww51\n",fontsize=16,color="green",shape="box"];22 -> 23[label="",style="dashed", color="red", weight=0];
22[label="ww3 ww40 ww50 >>= gtGt0 ww6\n",fontsize=16,color="magenta"];22 -> 24[label="",style="dashed", color="magenta", weight=3];
24[label="ww3 ww40 ww50\n",fontsize=16,color="green",shape="box"];24 -> 29[label="",style="dashed", color="green", weight=3];
24 -> 30[label="",style="dashed", color="green", weight=3];
23[label="ww8 >>= gtGt0 ww6\n",fontsize=16,color="burlywood",shape="triangle"];42[label="ww8/Nothing",fontsize=10,color="white",style="solid",shape="box"];23 -> 42[label="",style="solid", color="burlywood", weight=9];
42 -> 27[label="",style="solid", color="burlywood", weight=3];
43[label="ww8/Just ww80",fontsize=10,color="white",style="solid",shape="box"];23 -> 43[label="",style="solid", color="burlywood", weight=9];
43 -> 28[label="",style="solid", color="burlywood", weight=3];
29[label="ww40\n",fontsize=16,color="green",shape="box"];30[label="ww50\n",fontsize=16,color="green",shape="box"];27[label="Nothing >>= gtGt0 ww6\n",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="Just ww80 >>= gtGt0 ww6\n",fontsize=16,color="black",shape="box"];28 -> 32[label="",style="solid", color="black", weight=3];
31[label="Nothing\n",fontsize=16,color="green",shape="box"];32[label="gtGt0 ww6 ww80\n",fontsize=16,color="black",shape="box"];32 -> 33[label="",style="solid", color="black", weight=3];
33[label="ww6\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_foldr(ww3, :(ww40, ww41), :(ww50, ww51), h, ba, bb) → new_foldr(ww3, ww41, ww51, 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_foldr(ww3, :(ww40, ww41), :(ww50, ww51), h, ba, bb) → new_foldr(ww3, ww41, ww51, h, ba, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6