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

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

↳ HASKELL

  ↳ BR

mainModule Main

((List.genericTake :: Int -> [a] -> [a]) :: Int -> [a] -> [a])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

genericTake :: Integral b => b -> [a] -> [a]

genericTake

0 _

[]

genericTake

_ []

[]

genericTake

n (x : xs)

n > 0

x : genericTake (n - 1) xs

genericTake

_ _

error []

module Main where

import qualified List
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified List
import qualified Main
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((List.genericTake :: Int -> [a] -> [a]) :: Int -> [a] -> [a])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

genericTake :: Integral a => a -> [b] -> [b]

genericTake

0 vw

[]

genericTake

vx []

[]

genericTake

n (x : xs)

n > 0

x : genericTake (n - 1) xs

genericTake

vy vz

error []

module Main where

import qualified List
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified List
import qualified Main
import qualified Prelude

Cond Reductions:
The following Function with conditions

genericTake 0 vw = []

genericTake vx [] = []

genericTake n (x : xs)

| n > 0

= x : genericTake (n - 1) xs

genericTake vy vz = error []

is transformed to

genericTake xy vw = genericTake5 xy vw

genericTake vx [] = genericTake3 vx []

genericTake n (x : xs) = genericTake2 n (x : xs)

genericTake vy vz = genericTake0 vy vz

genericTake0 vy vz = error []

genericTake1 n x xs True = x : genericTake (n - 1) xs

genericTake1 n x xs False = genericTake0 n (x : xs)

genericTake2 n (x : xs) = genericTake1 n x xs (n > 0)

genericTake2 wz xu = genericTake0 wz xu

genericTake3 vx [] = []

genericTake3 xw xx = genericTake2 xw xx

genericTake4 True xy vw = []

genericTake4 xz yu yv = genericTake3 yu yv

genericTake5 xy vw = genericTake4 (xy == 0) xy vw

genericTake5 yw yx = genericTake3 yw yx

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((List.genericTake :: Int -> [a] -> [a]) :: Int -> [a] -> [a])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

genericTake :: Integral b => b -> [a] -> [a]

genericTake	xy vw	=	genericTake5 xy vw
genericTake	vx []	=	genericTake3 vx []
genericTake	n (x : xs)	=	genericTake2 n (x : xs)
genericTake	vy vz	=	genericTake0 vy vz

genericTake0

vy vz

error []

genericTake1	n x xs True	=	x : genericTake (n - 1) xs
genericTake1	n x xs False	=	genericTake0 n (x : xs)

genericTake2	n (x : xs)	=	genericTake1 n x xs (n > 0)
genericTake2	wz xu	=	genericTake0 wz xu

genericTake3	vx []	=	[]
genericTake3	xw xx	=	genericTake2 xw xx

genericTake4	True xy vw	=	[]
genericTake4	xz yu yv	=	genericTake3 yu yv

genericTake5	xy vw	=	genericTake4 (xy == 0) xy vw
genericTake5	yw yx	=	genericTake3 yw yx

module Main where

import qualified List
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified List
import qualified Main
import qualified Prelude

Num Reduction:All numbers are transformed to thier corresponding representation with Succ, Pred and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(List.genericTake :: Int -> [a] -> [a])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

genericTake :: Integral b => b -> [a] -> [a]

genericTake	xy vw	=	genericTake5 xy vw
genericTake	vx []	=	genericTake3 vx []
genericTake	n (x : xs)	=	genericTake2 n (x : xs)
genericTake	vy vz	=	genericTake0 vy vz

genericTake0

vy vz

error []

genericTake1	n x xs True	=	x : genericTake (n - fromInt (Pos (Succ Zero))) xs
genericTake1	n x xs False	=	genericTake0 n (x : xs)

genericTake2	n (x : xs)	=	genericTake1 n x xs (n > fromInt (Pos Zero))
genericTake2	wz xu	=	genericTake0 wz xu

genericTake3	vx []	=	[]
genericTake3	xw xx	=	genericTake2 xw xx

genericTake4	True xy vw	=	[]
genericTake4	xz yu yv	=	genericTake3 yu yv

genericTake5	xy vw	=	genericTake4 (xy == fromInt (Pos Zero)) xy vw
genericTake5	yw yx	=	genericTake3 yw yx

module Main where

import qualified List
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified List
import qualified Main
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="List.genericTake\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="List.genericTake yy3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="List.genericTake yy3 yy4\n",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="List.genericTake5 yy3 yy4\n",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="List.genericTake4 (yy3 == fromInt (Pos Zero)) yy3 yy4\n",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="List.genericTake4 (primEqInt yy3 (fromInt (Pos Zero))) yy3 yy4\n",fontsize=16,color="burlywood",shape="box"];62[label="yy3/Pos yy30",fontsize=10,color="white",style="solid",shape="box"];7 -> 62[label="",style="solid", color="burlywood", weight=9];
62 -> 8[label="",style="solid", color="burlywood", weight=3];
63[label="yy3/Neg yy30",fontsize=10,color="white",style="solid",shape="box"];7 -> 63[label="",style="solid", color="burlywood", weight=9];
63 -> 9[label="",style="solid", color="burlywood", weight=3];
8[label="List.genericTake4 (primEqInt (Pos yy30) (fromInt (Pos Zero))) (Pos yy30) yy4\n",fontsize=16,color="burlywood",shape="box"];64[label="yy30/Succ yy300",fontsize=10,color="white",style="solid",shape="box"];8 -> 64[label="",style="solid", color="burlywood", weight=9];
64 -> 10[label="",style="solid", color="burlywood", weight=3];
65[label="yy30/Zero",fontsize=10,color="white",style="solid",shape="box"];8 -> 65[label="",style="solid", color="burlywood", weight=9];
65 -> 11[label="",style="solid", color="burlywood", weight=3];
9[label="List.genericTake4 (primEqInt (Neg yy30) (fromInt (Pos Zero))) (Neg yy30) yy4\n",fontsize=16,color="burlywood",shape="box"];66[label="yy30/Succ yy300",fontsize=10,color="white",style="solid",shape="box"];9 -> 66[label="",style="solid", color="burlywood", weight=9];
66 -> 12[label="",style="solid", color="burlywood", weight=3];
67[label="yy30/Zero",fontsize=10,color="white",style="solid",shape="box"];9 -> 67[label="",style="solid", color="burlywood", weight=9];
67 -> 13[label="",style="solid", color="burlywood", weight=3];
10[label="List.genericTake4 (primEqInt (Pos (Succ yy300)) (fromInt (Pos Zero))) (Pos (Succ yy300)) yy4\n",fontsize=16,color="black",shape="box"];10 -> 14[label="",style="solid", color="black", weight=3];
11[label="List.genericTake4 (primEqInt (Pos Zero) (fromInt (Pos Zero))) (Pos Zero) yy4\n",fontsize=16,color="black",shape="box"];11 -> 15[label="",style="solid", color="black", weight=3];
12[label="List.genericTake4 (primEqInt (Neg (Succ yy300)) (fromInt (Pos Zero))) (Neg (Succ yy300)) yy4\n",fontsize=16,color="black",shape="box"];12 -> 16[label="",style="solid", color="black", weight=3];
13[label="List.genericTake4 (primEqInt (Neg Zero) (fromInt (Pos Zero))) (Neg Zero) yy4\n",fontsize=16,color="black",shape="box"];13 -> 17[label="",style="solid", color="black", weight=3];
14[label="List.genericTake4 (primEqInt (Pos (Succ yy300)) (Pos Zero)) (Pos (Succ yy300)) yy4\n",fontsize=16,color="black",shape="box"];14 -> 18[label="",style="solid", color="black", weight=3];
15[label="List.genericTake4 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero) yy4\n",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="List.genericTake4 (primEqInt (Neg (Succ yy300)) (Pos Zero)) (Neg (Succ yy300)) yy4\n",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="List.genericTake4 (primEqInt (Neg Zero) (Pos Zero)) (Neg Zero) yy4\n",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="List.genericTake4 False (Pos (Succ yy300)) yy4\n",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="List.genericTake4 True (Pos Zero) yy4\n",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="List.genericTake4 False (Neg (Succ yy300)) yy4\n",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="List.genericTake4 True (Neg Zero) yy4\n",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="List.genericTake3 (Pos (Succ yy300)) yy4\n",fontsize=16,color="burlywood",shape="box"];68[label="yy4/yy40 : yy41",fontsize=10,color="white",style="solid",shape="box"];22 -> 68[label="",style="solid", color="burlywood", weight=9];
68 -> 26[label="",style="solid", color="burlywood", weight=3];
69[label="yy4/[]",fontsize=10,color="white",style="solid",shape="box"];22 -> 69[label="",style="solid", color="burlywood", weight=9];
69 -> 27[label="",style="solid", color="burlywood", weight=3];
23[label="[]\n",fontsize=16,color="green",shape="box"];24[label="List.genericTake3 (Neg (Succ yy300)) yy4\n",fontsize=16,color="burlywood",shape="box"];70[label="yy4/yy40 : yy41",fontsize=10,color="white",style="solid",shape="box"];24 -> 70[label="",style="solid", color="burlywood", weight=9];
70 -> 28[label="",style="solid", color="burlywood", weight=3];
71[label="yy4/[]",fontsize=10,color="white",style="solid",shape="box"];24 -> 71[label="",style="solid", color="burlywood", weight=9];
71 -> 29[label="",style="solid", color="burlywood", weight=3];
25[label="[]\n",fontsize=16,color="green",shape="box"];26[label="List.genericTake3 (Pos (Succ yy300)) (yy40 : yy41)\n",fontsize=16,color="black",shape="box"];26 -> 30[label="",style="solid", color="black", weight=3];
27[label="List.genericTake3 (Pos (Succ yy300)) []\n",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="List.genericTake3 (Neg (Succ yy300)) (yy40 : yy41)\n",fontsize=16,color="black",shape="box"];28 -> 32[label="",style="solid", color="black", weight=3];
29[label="List.genericTake3 (Neg (Succ yy300)) []\n",fontsize=16,color="black",shape="box"];29 -> 33[label="",style="solid", color="black", weight=3];
30[label="List.genericTake2 (Pos (Succ yy300)) (yy40 : yy41)\n",fontsize=16,color="black",shape="box"];30 -> 34[label="",style="solid", color="black", weight=3];
31[label="[]\n",fontsize=16,color="green",shape="box"];32[label="List.genericTake2 (Neg (Succ yy300)) (yy40 : yy41)\n",fontsize=16,color="black",shape="box"];32 -> 35[label="",style="solid", color="black", weight=3];
33[label="[]\n",fontsize=16,color="green",shape="box"];34[label="List.genericTake1 (Pos (Succ yy300)) yy40 yy41 (Pos (Succ yy300) > fromInt (Pos Zero))\n",fontsize=16,color="black",shape="box"];34 -> 36[label="",style="solid", color="black", weight=3];
35[label="List.genericTake1 (Neg (Succ yy300)) yy40 yy41 (Neg (Succ yy300) > fromInt (Pos Zero))\n",fontsize=16,color="black",shape="box"];35 -> 37[label="",style="solid", color="black", weight=3];
36[label="List.genericTake1 (Pos (Succ yy300)) yy40 yy41 (compare (Pos (Succ yy300)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];36 -> 38[label="",style="solid", color="black", weight=3];
37[label="List.genericTake1 (Neg (Succ yy300)) yy40 yy41 (compare (Neg (Succ yy300)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];37 -> 39[label="",style="solid", color="black", weight=3];
38[label="List.genericTake1 (Pos (Succ yy300)) yy40 yy41 (primCmpInt (Pos (Succ yy300)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];38 -> 40[label="",style="solid", color="black", weight=3];
39[label="List.genericTake1 (Neg (Succ yy300)) yy40 yy41 (primCmpInt (Neg (Succ yy300)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];39 -> 41[label="",style="solid", color="black", weight=3];
40[label="List.genericTake1 (Pos (Succ yy300)) yy40 yy41 (primCmpInt (Pos (Succ yy300)) (Pos Zero) == GT)\n",fontsize=16,color="black",shape="box"];40 -> 42[label="",style="solid", color="black", weight=3];
41[label="List.genericTake1 (Neg (Succ yy300)) yy40 yy41 (primCmpInt (Neg (Succ yy300)) (Pos Zero) == GT)\n",fontsize=16,color="black",shape="box"];41 -> 43[label="",style="solid", color="black", weight=3];
42[label="List.genericTake1 (Pos (Succ yy300)) yy40 yy41 (primCmpNat (Succ yy300) Zero == GT)\n",fontsize=16,color="black",shape="box"];42 -> 44[label="",style="solid", color="black", weight=3];
43[label="List.genericTake1 (Neg (Succ yy300)) yy40 yy41 (LT == GT)\n",fontsize=16,color="black",shape="box"];43 -> 45[label="",style="solid", color="black", weight=3];
44[label="List.genericTake1 (Pos (Succ yy300)) yy40 yy41 (GT == GT)\n",fontsize=16,color="black",shape="box"];44 -> 46[label="",style="solid", color="black", weight=3];
45[label="List.genericTake1 (Neg (Succ yy300)) yy40 yy41 False\n",fontsize=16,color="black",shape="box"];45 -> 47[label="",style="solid", color="black", weight=3];
46[label="List.genericTake1 (Pos (Succ yy300)) yy40 yy41 True\n",fontsize=16,color="black",shape="box"];46 -> 48[label="",style="solid", color="black", weight=3];
47[label="List.genericTake0 (Neg (Succ yy300)) (yy40 : yy41)\n",fontsize=16,color="black",shape="box"];47 -> 49[label="",style="solid", color="black", weight=3];
48[label="yy40 : List.genericTake (Pos (Succ yy300) - fromInt (Pos (Succ Zero))) yy41\n",fontsize=16,color="green",shape="box"];48 -> 50[label="",style="dashed", color="green", weight=3];
49[label="error []\n",fontsize=16,color="black",shape="box"];49 -> 51[label="",style="solid", color="black", weight=3];
50 -> 4[label="",style="dashed", color="red", weight=0];
50[label="List.genericTake (Pos (Succ yy300) - fromInt (Pos (Succ Zero))) yy41\n",fontsize=16,color="magenta"];50 -> 52[label="",style="dashed", color="magenta", weight=3];
50 -> 53[label="",style="dashed", color="magenta", weight=3];
51[label="error []\n",fontsize=16,color="red",shape="box"];52[label="Pos (Succ yy300) - fromInt (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];52 -> 54[label="",style="solid", color="black", weight=3];
53[label="yy41\n",fontsize=16,color="green",shape="box"];54[label="primMinusInt (Pos (Succ yy300)) (fromInt (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];54 -> 55[label="",style="solid", color="black", weight=3];
55[label="primMinusInt (Pos (Succ yy300)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];55 -> 56[label="",style="solid", color="black", weight=3];
56[label="primMinusNat (Succ yy300) (Succ Zero)\n",fontsize=16,color="black",shape="box"];56 -> 57[label="",style="solid", color="black", weight=3];
57[label="primMinusNat yy300 Zero\n",fontsize=16,color="burlywood",shape="box"];73[label="yy300/Succ yy3000",fontsize=10,color="white",style="solid",shape="box"];57 -> 73[label="",style="solid", color="burlywood", weight=9];
73 -> 58[label="",style="solid", color="burlywood", weight=3];
74[label="yy300/Zero",fontsize=10,color="white",style="solid",shape="box"];57 -> 74[label="",style="solid", color="burlywood", weight=9];
74 -> 59[label="",style="solid", color="burlywood", weight=3];
58[label="primMinusNat (Succ yy3000) Zero\n",fontsize=16,color="black",shape="box"];58 -> 60[label="",style="solid", color="black", weight=3];
59[label="primMinusNat Zero Zero\n",fontsize=16,color="black",shape="box"];59 -> 61[label="",style="solid", color="black", weight=3];
60[label="Pos (Succ yy3000)\n",fontsize=16,color="green",shape="box"];61[label="Pos Zero\n",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ QDP

                  ↳ QDPSizeChangeProof

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

new_genericTake(Pos(Succ(yy300)), :(yy40, yy41), ba) → new_genericTake(new_primMinusNat(yy300), yy41, ba)

The TRS R consists of the following rules:

new_primMinusNat(Succ(yy3000)) → Pos(Succ(yy3000))
new_primMinusNat(Zero) → Pos(Zero)

The set Q consists of the following terms:

new_primMinusNat(Succ(x0))
new_primMinusNat(Zero)

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_genericTake(Pos(Succ(yy300)), :(yy40, yy41), ba) → new_genericTake(new_primMinusNat(yy300), yy41, ba)
The graph contains the following edges 2 > 2, 3 >= 3

genericTake	xy vw	= genericTake5 xy vw
genericTake	vx []	= genericTake3 vx []
genericTake	n (x : xs)	= genericTake2 n (x : xs)
genericTake	vy vz	= genericTake0 vy vz

genericTake1	n x xs True	= x : genericTake (n - 1) xs
genericTake1	n x xs False	= genericTake0 n (x : xs)

genericTake2	n (x : xs)	= genericTake1 n x xs (n > 0)
genericTake2	wz xu	= genericTake0 wz xu

genericTake4	True xy vw	= []
genericTake4	xz yu yv	= genericTake3 yu yv

genericTake5	xy vw	= genericTake4 (xy == 0) xy vw
genericTake5	yw yx	= genericTake3 yw yx