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

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

↳ HASKELL

  ↳ LR

mainModule Main

((Monad.replicateM_ :: Int -> [a] -> [()]) :: Int -> [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

replicateM_ :: Monad a => Int -> a b -> a ()

replicateM_

n x

sequence_ (replicate n x)

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.replicateM_ :: Int -> [a] -> [()]) :: Int -> [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

replicateM_ :: Monad b => Int -> b a -> b ()

replicateM_

n x

sequence_ (replicate n x)

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

((Monad.replicateM_ :: Int -> [a] -> [()]) :: Int -> [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

replicateM_ :: Monad b => Int -> b a -> b ()

replicateM_

n x

sequence_ (replicate n x)

module Maybe where

import qualified Main
import qualified Monad
import qualified Prelude

Cond Reductions:
The following Function with conditions

take n vw

| n <= 0

= []

take vx [] = []

take n (x : xs) = x : take (n - 1) xs

is transformed to

take n vw = take3 n vw

take vx [] = take1 vx []

take n (x : xs) = take0 n (x : xs)

take0 n (x : xs) = x : take (n - 1) xs

take1 vx [] = []

take1 wx wy = take0 wx wy

take2 n vw True = []

take2 n vw False = take1 n vw

take3 n vw = take2 n vw (n <= 0)

take3 wz xu = take1 wz xu

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule Main

((Monad.replicateM_ :: Int -> [a] -> [()]) :: Int -> [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

replicateM_ :: Monad a => Int -> a b -> a ()

replicateM_

n x

sequence_ (replicate n x)

Let/Where Reductions:
The bindings of the following Let/Where expression

xs

where

xs = x : xs

are unpacked to the following functions on top level

repeatXs xv = xv : repeatXs xv

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

mainModule Main

((Monad.replicateM_ :: Int -> [a] -> [()]) :: Int -> [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

replicateM_ :: Monad b => Int -> b a -> b ()

replicateM_

n x

sequence_ (replicate n x)

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

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

mainModule Main

(Monad.replicateM_ :: Int -> [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

replicateM_ :: Monad a => Int -> a b -> a ()

replicateM_

n x

sequence_ (replicate n x)

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="Monad.replicateM_\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="Monad.replicateM_ xw3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="Monad.replicateM_ xw3 xw4\n",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="sequence_ (replicate xw3 xw4)\n",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="foldr (>>) (return ()) (replicate xw3 xw4)\n",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="foldr (>>) (return ()) (take xw3 (repeat xw4))\n",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="foldr (>>) (return ()) (take3 xw3 (repeat xw4))\n",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="foldr (>>) (return ()) (take2 xw3 (repeat xw4) (xw3 <= Pos Zero))\n",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="foldr (>>) (return ()) (take2 xw3 (repeat xw4) (compare xw3 (Pos Zero) /= GT))\n",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="foldr (>>) (return ()) (take2 xw3 (repeat xw4) (not (compare xw3 (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="foldr (>>) (return ()) (take2 xw3 (repeat xw4) (not (primCmpInt xw3 (Pos Zero) == GT)))\n",fontsize=16,color="burlywood",shape="box"];159[label="xw3/Pos xw30",fontsize=10,color="white",style="solid",shape="box"];12 -> 159[label="",style="solid", color="burlywood", weight=9];
159 -> 13[label="",style="solid", color="burlywood", weight=3];
160[label="xw3/Neg xw30",fontsize=10,color="white",style="solid",shape="box"];12 -> 160[label="",style="solid", color="burlywood", weight=9];
160 -> 14[label="",style="solid", color="burlywood", weight=3];
13[label="foldr (>>) (return ()) (take2 (Pos xw30) (repeat xw4) (not (primCmpInt (Pos xw30) (Pos Zero) == GT)))\n",fontsize=16,color="burlywood",shape="box"];161[label="xw30/Succ xw300",fontsize=10,color="white",style="solid",shape="box"];13 -> 161[label="",style="solid", color="burlywood", weight=9];
161 -> 15[label="",style="solid", color="burlywood", weight=3];
162[label="xw30/Zero",fontsize=10,color="white",style="solid",shape="box"];13 -> 162[label="",style="solid", color="burlywood", weight=9];
162 -> 16[label="",style="solid", color="burlywood", weight=3];
14[label="foldr (>>) (return ()) (take2 (Neg xw30) (repeat xw4) (not (primCmpInt (Neg xw30) (Pos Zero) == GT)))\n",fontsize=16,color="burlywood",shape="box"];163[label="xw30/Succ xw300",fontsize=10,color="white",style="solid",shape="box"];14 -> 163[label="",style="solid", color="burlywood", weight=9];
163 -> 17[label="",style="solid", color="burlywood", weight=3];
164[label="xw30/Zero",fontsize=10,color="white",style="solid",shape="box"];14 -> 164[label="",style="solid", color="burlywood", weight=9];
164 -> 18[label="",style="solid", color="burlywood", weight=3];
15[label="foldr (>>) (return ()) (take2 (Pos (Succ xw300)) (repeat xw4) (not (primCmpInt (Pos (Succ xw300)) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="foldr (>>) (return ()) (take2 (Pos Zero) (repeat xw4) (not (primCmpInt (Pos Zero) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="foldr (>>) (return ()) (take2 (Neg (Succ xw300)) (repeat xw4) (not (primCmpInt (Neg (Succ xw300)) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="foldr (>>) (return ()) (take2 (Neg Zero) (repeat xw4) (not (primCmpInt (Neg Zero) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="foldr (>>) (return ()) (take2 (Pos (Succ xw300)) (repeat xw4) (not (primCmpNat (Succ xw300) Zero == GT)))\n",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="foldr (>>) (return ()) (take2 (Pos Zero) (repeat xw4) (not (EQ == GT)))\n",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="foldr (>>) (return ()) (take2 (Neg (Succ xw300)) (repeat xw4) (not (LT == GT)))\n",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="foldr (>>) (return ()) (take2 (Neg Zero) (repeat xw4) (not (EQ == GT)))\n",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="foldr (>>) (return ()) (take2 (Pos (Succ xw300)) (repeat xw4) (not (GT == GT)))\n",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24[label="foldr (>>) (return ()) (take2 (Pos Zero) (repeat xw4) (not False))\n",fontsize=16,color="black",shape="box"];24 -> 28[label="",style="solid", color="black", weight=3];
25[label="foldr (>>) (return ()) (take2 (Neg (Succ xw300)) (repeat xw4) (not False))\n",fontsize=16,color="black",shape="box"];25 -> 29[label="",style="solid", color="black", weight=3];
26[label="foldr (>>) (return ()) (take2 (Neg Zero) (repeat xw4) (not False))\n",fontsize=16,color="black",shape="box"];26 -> 30[label="",style="solid", color="black", weight=3];
27[label="foldr (>>) (return ()) (take2 (Pos (Succ xw300)) (repeat xw4) (not True))\n",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="foldr (>>) (return ()) (take2 (Pos Zero) (repeat xw4) True)\n",fontsize=16,color="black",shape="box"];28 -> 32[label="",style="solid", color="black", weight=3];
29[label="foldr (>>) (return ()) (take2 (Neg (Succ xw300)) (repeat xw4) True)\n",fontsize=16,color="black",shape="box"];29 -> 33[label="",style="solid", color="black", weight=3];
30[label="foldr (>>) (return ()) (take2 (Neg Zero) (repeat xw4) True)\n",fontsize=16,color="black",shape="box"];30 -> 34[label="",style="solid", color="black", weight=3];
31[label="foldr (>>) (return ()) (take2 (Pos (Succ xw300)) (repeat xw4) False)\n",fontsize=16,color="black",shape="box"];31 -> 35[label="",style="solid", color="black", weight=3];
32[label="foldr (>>) (return ()) []\n",fontsize=16,color="black",shape="triangle"];32 -> 36[label="",style="solid", color="black", weight=3];
33 -> 32[label="",style="dashed", color="red", weight=0];
33[label="foldr (>>) (return ()) []\n",fontsize=16,color="magenta"];34 -> 32[label="",style="dashed", color="red", weight=0];
34[label="foldr (>>) (return ()) []\n",fontsize=16,color="magenta"];35[label="foldr (>>) (return ()) (take1 (Pos (Succ xw300)) (repeat xw4))\n",fontsize=16,color="black",shape="box"];35 -> 37[label="",style="solid", color="black", weight=3];
36[label="return ()\n",fontsize=16,color="black",shape="triangle"];36 -> 38[label="",style="solid", color="black", weight=3];
37 -> 39[label="",style="dashed", color="red", weight=0];
37[label="foldr (>>) (return ()) (take1 (Pos (Succ xw300)) (repeatXs xw4))\n",fontsize=16,color="magenta"];37 -> 40[label="",style="dashed", color="magenta", weight=3];
38[label="() : []\n",fontsize=16,color="green",shape="box"];40 -> 36[label="",style="dashed", color="red", weight=0];
40[label="return ()\n",fontsize=16,color="magenta"];39[label="foldr (>>) xw5 (take1 (Pos (Succ xw300)) (repeatXs xw4))\n",fontsize=16,color="black",shape="triangle"];39 -> 41[label="",style="solid", color="black", weight=3];
41[label="foldr (>>) xw5 (take1 (Pos (Succ xw300)) (xw4 : repeatXs xw4))\n",fontsize=16,color="black",shape="box"];41 -> 42[label="",style="solid", color="black", weight=3];
42[label="foldr (>>) xw5 (take0 (Pos (Succ xw300)) (xw4 : repeatXs xw4))\n",fontsize=16,color="black",shape="box"];42 -> 43[label="",style="solid", color="black", weight=3];
43[label="foldr (>>) xw5 (xw4 : take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs xw4))\n",fontsize=16,color="black",shape="box"];43 -> 44[label="",style="solid", color="black", weight=3];
44[label="(>>) xw4 foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs xw4))\n",fontsize=16,color="black",shape="box"];44 -> 45[label="",style="solid", color="black", weight=3];
45[label="xw4 >>= gtGt0 (foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs xw4)))\n",fontsize=16,color="burlywood",shape="box"];169[label="xw4/xw40 : xw41",fontsize=10,color="white",style="solid",shape="box"];45 -> 169[label="",style="solid", color="burlywood", weight=9];
169 -> 46[label="",style="solid", color="burlywood", weight=3];
170[label="xw4/[]",fontsize=10,color="white",style="solid",shape="box"];45 -> 170[label="",style="solid", color="burlywood", weight=9];
170 -> 47[label="",style="solid", color="burlywood", weight=3];
46[label="xw40 : xw41 >>= gtGt0 (foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41))))\n",fontsize=16,color="black",shape="box"];46 -> 48[label="",style="solid", color="black", weight=3];
47[label="[] >>= gtGt0 (foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs [])))\n",fontsize=16,color="black",shape="box"];47 -> 49[label="",style="solid", color="black", weight=3];
48 -> 73[label="",style="dashed", color="red", weight=0];
48[label="gtGt0 (foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)))) xw40 ++ (xw41 >>= gtGt0 (foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)))))\n",fontsize=16,color="magenta"];48 -> 74[label="",style="dashed", color="magenta", weight=3];
48 -> 75[label="",style="dashed", color="magenta", weight=3];
49[label="[]\n",fontsize=16,color="green",shape="box"];74[label="foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)))\n",fontsize=16,color="black",shape="triangle"];74 -> 118[label="",style="solid", color="black", weight=3];
75 -> 119[label="",style="dashed", color="red", weight=0];
75[label="gtGt0 (foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)))) xw40\n",fontsize=16,color="magenta"];75 -> 120[label="",style="dashed", color="magenta", weight=3];
73[label="xw6 ++ (xw41 >>= gtGt0 xw7)\n",fontsize=16,color="burlywood",shape="triangle"];173[label="xw6/xw60 : xw61",fontsize=10,color="white",style="solid",shape="box"];73 -> 173[label="",style="solid", color="burlywood", weight=9];
173 -> 121[label="",style="solid", color="burlywood", weight=3];
174[label="xw6/[]",fontsize=10,color="white",style="solid",shape="box"];73 -> 174[label="",style="solid", color="burlywood", weight=9];
174 -> 122[label="",style="solid", color="burlywood", weight=3];
118[label="foldr (>>) xw5 (take3 (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)))\n",fontsize=16,color="black",shape="box"];118 -> 123[label="",style="solid", color="black", weight=3];
120 -> 74[label="",style="dashed", color="red", weight=0];
120[label="foldr (>>) xw5 (take (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)))\n",fontsize=16,color="magenta"];119[label="gtGt0 xw8 xw40\n",fontsize=16,color="black",shape="triangle"];119 -> 124[label="",style="solid", color="black", weight=3];
121[label="(xw60 : xw61) ++ (xw41 >>= gtGt0 xw7)\n",fontsize=16,color="black",shape="box"];121 -> 125[label="",style="solid", color="black", weight=3];
122[label="[] ++ (xw41 >>= gtGt0 xw7)\n",fontsize=16,color="black",shape="box"];122 -> 126[label="",style="solid", color="black", weight=3];
123[label="foldr (>>) xw5 (take2 (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)) (Pos (Succ xw300) - Pos (Succ Zero) <= Pos Zero))\n",fontsize=16,color="black",shape="box"];123 -> 127[label="",style="solid", color="black", weight=3];
124[label="xw8\n",fontsize=16,color="green",shape="box"];125[label="xw60 : xw61 ++ (xw41 >>= gtGt0 xw7)\n",fontsize=16,color="green",shape="box"];125 -> 128[label="",style="dashed", color="green", weight=3];
126[label="xw41 >>= gtGt0 xw7\n",fontsize=16,color="burlywood",shape="box"];176[label="xw41/xw410 : xw411",fontsize=10,color="white",style="solid",shape="box"];126 -> 176[label="",style="solid", color="burlywood", weight=9];
176 -> 129[label="",style="solid", color="burlywood", weight=3];
177[label="xw41/[]",fontsize=10,color="white",style="solid",shape="box"];126 -> 177[label="",style="solid", color="burlywood", weight=9];
177 -> 130[label="",style="solid", color="burlywood", weight=3];
127[label="foldr (>>) xw5 (take2 (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)) (compare (Pos (Succ xw300) - Pos (Succ Zero)) (Pos Zero) /= GT))\n",fontsize=16,color="black",shape="box"];127 -> 131[label="",style="solid", color="black", weight=3];
128 -> 73[label="",style="dashed", color="red", weight=0];
128[label="xw61 ++ (xw41 >>= gtGt0 xw7)\n",fontsize=16,color="magenta"];128 -> 132[label="",style="dashed", color="magenta", weight=3];
129[label="xw410 : xw411 >>= gtGt0 xw7\n",fontsize=16,color="black",shape="box"];129 -> 133[label="",style="solid", color="black", weight=3];
130[label="[] >>= gtGt0 xw7\n",fontsize=16,color="black",shape="box"];130 -> 134[label="",style="solid", color="black", weight=3];
131[label="foldr (>>) xw5 (take2 (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)) (not (compare (Pos (Succ xw300) - Pos (Succ Zero)) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];131 -> 135[label="",style="solid", color="black", weight=3];
132[label="xw61\n",fontsize=16,color="green",shape="box"];133 -> 73[label="",style="dashed", color="red", weight=0];
133[label="gtGt0 xw7 xw410 ++ (xw411 >>= gtGt0 xw7)\n",fontsize=16,color="magenta"];133 -> 136[label="",style="dashed", color="magenta", weight=3];
133 -> 137[label="",style="dashed", color="magenta", weight=3];
134[label="[]\n",fontsize=16,color="green",shape="box"];135[label="foldr (>>) xw5 (take2 (Pos (Succ xw300) - Pos (Succ Zero)) (repeatXs (xw40 : xw41)) (not (primCmpInt (Pos (Succ xw300) - Pos (Succ Zero)) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];135 -> 138[label="",style="solid", color="black", weight=3];
136[label="xw411\n",fontsize=16,color="green",shape="box"];137 -> 119[label="",style="dashed", color="red", weight=0];
137[label="gtGt0 xw7 xw410\n",fontsize=16,color="magenta"];137 -> 139[label="",style="dashed", color="magenta", weight=3];
137 -> 140[label="",style="dashed", color="magenta", weight=3];
138[label="foldr (>>) xw5 (take2 (primMinusInt (Pos (Succ xw300)) (Pos (Succ Zero))) (repeatXs (xw40 : xw41)) (not (primCmpInt (primMinusInt (Pos (Succ xw300)) (Pos (Succ Zero))) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];138 -> 141[label="",style="solid", color="black", weight=3];
139[label="xw7\n",fontsize=16,color="green",shape="box"];140[label="xw410\n",fontsize=16,color="green",shape="box"];141[label="foldr (>>) xw5 (take2 (primMinusNat (Succ xw300) (Succ Zero)) (repeatXs (xw40 : xw41)) (not (primCmpInt (primMinusNat (Succ xw300) (Succ Zero)) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];141 -> 142[label="",style="solid", color="black", weight=3];
142[label="foldr (>>) xw5 (take2 (primMinusNat xw300 Zero) (repeatXs (xw40 : xw41)) (not (primCmpInt (primMinusNat xw300 Zero) (Pos Zero) == GT)))\n",fontsize=16,color="burlywood",shape="box"];181[label="xw300/Succ xw3000",fontsize=10,color="white",style="solid",shape="box"];142 -> 181[label="",style="solid", color="burlywood", weight=9];
181 -> 143[label="",style="solid", color="burlywood", weight=3];
182[label="xw300/Zero",fontsize=10,color="white",style="solid",shape="box"];142 -> 182[label="",style="solid", color="burlywood", weight=9];
182 -> 144[label="",style="solid", color="burlywood", weight=3];
143[label="foldr (>>) xw5 (take2 (primMinusNat (Succ xw3000) Zero) (repeatXs (xw40 : xw41)) (not (primCmpInt (primMinusNat (Succ xw3000) Zero) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];143 -> 145[label="",style="solid", color="black", weight=3];
144[label="foldr (>>) xw5 (take2 (primMinusNat Zero Zero) (repeatXs (xw40 : xw41)) (not (primCmpInt (primMinusNat Zero Zero) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];144 -> 146[label="",style="solid", color="black", weight=3];
145[label="foldr (>>) xw5 (take2 (Pos (Succ xw3000)) (repeatXs (xw40 : xw41)) (not (primCmpInt (Pos (Succ xw3000)) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];145 -> 147[label="",style="solid", color="black", weight=3];
146[label="foldr (>>) xw5 (take2 (Pos Zero) (repeatXs (xw40 : xw41)) (not (primCmpInt (Pos Zero) (Pos Zero) == GT)))\n",fontsize=16,color="black",shape="box"];146 -> 148[label="",style="solid", color="black", weight=3];
147[label="foldr (>>) xw5 (take2 (Pos (Succ xw3000)) (repeatXs (xw40 : xw41)) (not (primCmpNat (Succ xw3000) Zero == GT)))\n",fontsize=16,color="black",shape="box"];147 -> 149[label="",style="solid", color="black", weight=3];
148[label="foldr (>>) xw5 (take2 (Pos Zero) (repeatXs (xw40 : xw41)) (not (EQ == GT)))\n",fontsize=16,color="black",shape="box"];148 -> 150[label="",style="solid", color="black", weight=3];
149[label="foldr (>>) xw5 (take2 (Pos (Succ xw3000)) (repeatXs (xw40 : xw41)) (not (GT == GT)))\n",fontsize=16,color="black",shape="box"];149 -> 151[label="",style="solid", color="black", weight=3];
150[label="foldr (>>) xw5 (take2 (Pos Zero) (repeatXs (xw40 : xw41)) (not False))\n",fontsize=16,color="black",shape="box"];150 -> 152[label="",style="solid", color="black", weight=3];
151[label="foldr (>>) xw5 (take2 (Pos (Succ xw3000)) (repeatXs (xw40 : xw41)) (not True))\n",fontsize=16,color="black",shape="box"];151 -> 153[label="",style="solid", color="black", weight=3];
152[label="foldr (>>) xw5 (take2 (Pos Zero) (repeatXs (xw40 : xw41)) True)\n",fontsize=16,color="black",shape="box"];152 -> 154[label="",style="solid", color="black", weight=3];
153[label="foldr (>>) xw5 (take2 (Pos (Succ xw3000)) (repeatXs (xw40 : xw41)) False)\n",fontsize=16,color="black",shape="box"];153 -> 155[label="",style="solid", color="black", weight=3];
154[label="foldr (>>) xw5 []\n",fontsize=16,color="black",shape="box"];154 -> 156[label="",style="solid", color="black", weight=3];
155 -> 39[label="",style="dashed", color="red", weight=0];
155[label="foldr (>>) xw5 (take1 (Pos (Succ xw3000)) (repeatXs (xw40 : xw41)))\n",fontsize=16,color="magenta"];155 -> 157[label="",style="dashed", color="magenta", weight=3];
155 -> 158[label="",style="dashed", color="magenta", weight=3];
156[label="xw5\n",fontsize=16,color="green",shape="box"];157[label="xw3000\n",fontsize=16,color="green",shape="box"];158[label="xw40 : xw41\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

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

new_psPs(:(xw60, xw61), xw41, xw7, h) → new_psPs(xw61, xw41, xw7, h)
new_psPs([], :(xw410, xw411), xw7, h) → new_psPs(new_gtGt0(xw7, xw410, h), xw411, xw7, h)

The TRS R consists of the following rules:

new_gtGt0(xw8, xw40, h) → xw8

The set Q consists of the following terms:

new_gtGt0(x0, x1, x2)

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_psPs(:(xw60, xw61), xw41, xw7, h) → new_psPs(xw61, xw41, xw7, h)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4
new_psPs([], :(xw410, xw411), xw7, h) → new_psPs(new_gtGt0(xw7, xw410, h), xw411, xw7, h)
The graph contains the following edges 2 > 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

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

new_foldr0(xw5, xw300, :(xw40, xw41), h) → new_foldr(xw5, xw300, xw40, xw41, h)
new_foldr(xw5, Succ(xw3000), xw40, xw41, h) → new_foldr0(xw5, xw3000, :(xw40, xw41), h)
new_foldr0(xw5, Succ(xw3000), :(xw40, xw41), h) → new_foldr0(xw5, xw3000, :(xw40, xw41), h)

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(xw5, Succ(xw3000), xw40, xw41, h) → new_foldr0(xw5, xw3000, :(xw40, xw41), h)
The graph contains the following edges 1 >= 1, 2 > 2, 5 >= 4
new_foldr0(xw5, Succ(xw3000), :(xw40, xw41), h) → new_foldr0(xw5, xw3000, :(xw40, xw41), h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4
new_foldr0(xw5, xw300, :(xw40, xw41), h) → new_foldr(xw5, xw300, xw40, xw41, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 5

take	n vw	= take3 n vw
take	vx []	= take1 vx []
take	n (x : xs)	= take0 n (x : xs)