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

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

↳ HASKELL

  ↳ BR

mainModule Main

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

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

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

genericIndex

(x : _) 0

genericIndex

(_ : xs) n

n > 0

genericIndex xs (n - 1)

otherwise

error []

genericIndex

_ _

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

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

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

genericIndex

(x : vw) 0

genericIndex

(vx : xs) n

n > 0

genericIndex xs (n - 1)

otherwise

error []

genericIndex

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

genericIndex (x : vw) 0 = x

genericIndex (vx : xs) n

| n > 0

= genericIndex xs (n - 1)

| otherwise

= error []

genericIndex vy vz = error []

is transformed to

genericIndex (x : vw) xw = genericIndex5 (x : vw) xw

genericIndex (vx : xs) n = genericIndex3 (vx : xs) n

genericIndex vy vz = genericIndex0 vy vz

genericIndex0 vy vz = error []

genericIndex2 vx xs n True = genericIndex xs (n - 1)

genericIndex2 vx xs n False = genericIndex1 vx xs n otherwise

genericIndex1 vx xs n True = error []

genericIndex1 vx xs n False = genericIndex0 (vx : xs) n

genericIndex3 (vx : xs) n = genericIndex2 vx xs n (n > 0)

genericIndex3 wz xu = genericIndex0 wz xu

genericIndex4 True (x : vw) xw = x

genericIndex4 xx xy xz = genericIndex3 xy xz

genericIndex5 (x : vw) xw = genericIndex4 (xw == 0) (x : vw) xw

genericIndex5 yu yv = genericIndex3 yu yv

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

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

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

genericIndex	(x : vw) xw	=	genericIndex5 (x : vw) xw
genericIndex	(vx : xs) n	=	genericIndex3 (vx : xs) n
genericIndex	vy vz	=	genericIndex0 vy vz

genericIndex0

vy vz

error []

genericIndex1	vx xs n True	=	error []
genericIndex1	vx xs n False	=	genericIndex0 (vx : xs) n

genericIndex2	vx xs n True	=	genericIndex xs (n - 1)
genericIndex2	vx xs n False	=	genericIndex1 vx xs n otherwise

genericIndex3	(vx : xs) n	=	genericIndex2 vx xs n (n > 0)
genericIndex3	wz xu	=	genericIndex0 wz xu

genericIndex4	True (x : vw) xw	=	x
genericIndex4	xx xy xz	=	genericIndex3 xy xz

genericIndex5	(x : vw) xw	=	genericIndex4 (xw == 0) (x : vw) xw
genericIndex5	yu yv	=	genericIndex3 yu yv

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

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

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

genericIndex	(x : vw) xw	=	genericIndex5 (x : vw) xw
genericIndex	(vx : xs) n	=	genericIndex3 (vx : xs) n
genericIndex	vy vz	=	genericIndex0 vy vz

genericIndex0

vy vz

error []

genericIndex1	vx xs n True	=	error []
genericIndex1	vx xs n False	=	genericIndex0 (vx : xs) n

genericIndex2	vx xs n True	=	genericIndex xs (n - fromInt (Pos (Succ Zero)))
genericIndex2	vx xs n False	=	genericIndex1 vx xs n otherwise

genericIndex3	(vx : xs) n	=	genericIndex2 vx xs n (n > fromInt (Pos Zero))
genericIndex3	wz xu	=	genericIndex0 wz xu

genericIndex4	True (x : vw) xw	=	x
genericIndex4	xx xy xz	=	genericIndex3 xy xz

genericIndex5	(x : vw) xw	=	genericIndex4 (xw == fromInt (Pos Zero)) (x : vw) xw
genericIndex5	yu yv	=	genericIndex3 yu yv

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.genericIndex\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="List.genericIndex yw3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="List.genericIndex yw3 yw4\n",fontsize=16,color="burlywood",shape="triangle"];58[label="yw3/yw30 : yw31",fontsize=10,color="white",style="solid",shape="box"];4 -> 58[label="",style="solid", color="burlywood", weight=9];
58 -> 5[label="",style="solid", color="burlywood", weight=3];
59[label="yw3/[]",fontsize=10,color="white",style="solid",shape="box"];4 -> 59[label="",style="solid", color="burlywood", weight=9];
59 -> 6[label="",style="solid", color="burlywood", weight=3];
5[label="List.genericIndex (yw30 : yw31) yw4\n",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="List.genericIndex [] yw4\n",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="List.genericIndex5 (yw30 : yw31) yw4\n",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="List.genericIndex0 [] yw4\n",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="List.genericIndex4 (yw4 == fromInt (Pos Zero)) (yw30 : yw31) yw4\n",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="error []\n",fontsize=16,color="black",shape="triangle"];10 -> 12[label="",style="solid", color="black", weight=3];
11[label="List.genericIndex4 (primEqInt yw4 (fromInt (Pos Zero))) (yw30 : yw31) yw4\n",fontsize=16,color="burlywood",shape="box"];60[label="yw4/Pos yw40",fontsize=10,color="white",style="solid",shape="box"];11 -> 60[label="",style="solid", color="burlywood", weight=9];
60 -> 13[label="",style="solid", color="burlywood", weight=3];
61[label="yw4/Neg yw40",fontsize=10,color="white",style="solid",shape="box"];11 -> 61[label="",style="solid", color="burlywood", weight=9];
61 -> 14[label="",style="solid", color="burlywood", weight=3];
12[label="error []\n",fontsize=16,color="red",shape="box"];13[label="List.genericIndex4 (primEqInt (Pos yw40) (fromInt (Pos Zero))) (yw30 : yw31) (Pos yw40)\n",fontsize=16,color="burlywood",shape="box"];62[label="yw40/Succ yw400",fontsize=10,color="white",style="solid",shape="box"];13 -> 62[label="",style="solid", color="burlywood", weight=9];
62 -> 15[label="",style="solid", color="burlywood", weight=3];
63[label="yw40/Zero",fontsize=10,color="white",style="solid",shape="box"];13 -> 63[label="",style="solid", color="burlywood", weight=9];
63 -> 16[label="",style="solid", color="burlywood", weight=3];
14[label="List.genericIndex4 (primEqInt (Neg yw40) (fromInt (Pos Zero))) (yw30 : yw31) (Neg yw40)\n",fontsize=16,color="burlywood",shape="box"];64[label="yw40/Succ yw400",fontsize=10,color="white",style="solid",shape="box"];14 -> 64[label="",style="solid", color="burlywood", weight=9];
64 -> 17[label="",style="solid", color="burlywood", weight=3];
65[label="yw40/Zero",fontsize=10,color="white",style="solid",shape="box"];14 -> 65[label="",style="solid", color="burlywood", weight=9];
65 -> 18[label="",style="solid", color="burlywood", weight=3];
15[label="List.genericIndex4 (primEqInt (Pos (Succ yw400)) (fromInt (Pos Zero))) (yw30 : yw31) (Pos (Succ yw400))\n",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="List.genericIndex4 (primEqInt (Pos Zero) (fromInt (Pos Zero))) (yw30 : yw31) (Pos Zero)\n",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="List.genericIndex4 (primEqInt (Neg (Succ yw400)) (fromInt (Pos Zero))) (yw30 : yw31) (Neg (Succ yw400))\n",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="List.genericIndex4 (primEqInt (Neg Zero) (fromInt (Pos Zero))) (yw30 : yw31) (Neg Zero)\n",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="List.genericIndex4 (primEqInt (Pos (Succ yw400)) (Pos Zero)) (yw30 : yw31) (Pos (Succ yw400))\n",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="List.genericIndex4 (primEqInt (Pos Zero) (Pos Zero)) (yw30 : yw31) (Pos Zero)\n",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="List.genericIndex4 (primEqInt (Neg (Succ yw400)) (Pos Zero)) (yw30 : yw31) (Neg (Succ yw400))\n",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="List.genericIndex4 (primEqInt (Neg Zero) (Pos Zero)) (yw30 : yw31) (Neg Zero)\n",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="List.genericIndex4 False (yw30 : yw31) (Pos (Succ yw400))\n",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24[label="List.genericIndex4 True (yw30 : yw31) (Pos Zero)\n",fontsize=16,color="black",shape="box"];24 -> 28[label="",style="solid", color="black", weight=3];
25[label="List.genericIndex4 False (yw30 : yw31) (Neg (Succ yw400))\n",fontsize=16,color="black",shape="box"];25 -> 29[label="",style="solid", color="black", weight=3];
26[label="List.genericIndex4 True (yw30 : yw31) (Neg Zero)\n",fontsize=16,color="black",shape="box"];26 -> 30[label="",style="solid", color="black", weight=3];
27[label="List.genericIndex3 (yw30 : yw31) (Pos (Succ yw400))\n",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="yw30\n",fontsize=16,color="green",shape="box"];29[label="List.genericIndex3 (yw30 : yw31) (Neg (Succ yw400))\n",fontsize=16,color="black",shape="box"];29 -> 32[label="",style="solid", color="black", weight=3];
30[label="yw30\n",fontsize=16,color="green",shape="box"];31[label="List.genericIndex2 yw30 yw31 (Pos (Succ yw400)) (Pos (Succ yw400) > fromInt (Pos Zero))\n",fontsize=16,color="black",shape="box"];31 -> 33[label="",style="solid", color="black", weight=3];
32[label="List.genericIndex2 yw30 yw31 (Neg (Succ yw400)) (Neg (Succ yw400) > fromInt (Pos Zero))\n",fontsize=16,color="black",shape="box"];32 -> 34[label="",style="solid", color="black", weight=3];
33[label="List.genericIndex2 yw30 yw31 (Pos (Succ yw400)) (compare (Pos (Succ yw400)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];33 -> 35[label="",style="solid", color="black", weight=3];
34[label="List.genericIndex2 yw30 yw31 (Neg (Succ yw400)) (compare (Neg (Succ yw400)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];34 -> 36[label="",style="solid", color="black", weight=3];
35[label="List.genericIndex2 yw30 yw31 (Pos (Succ yw400)) (primCmpInt (Pos (Succ yw400)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];35 -> 37[label="",style="solid", color="black", weight=3];
36[label="List.genericIndex2 yw30 yw31 (Neg (Succ yw400)) (primCmpInt (Neg (Succ yw400)) (fromInt (Pos Zero)) == GT)\n",fontsize=16,color="black",shape="box"];36 -> 38[label="",style="solid", color="black", weight=3];
37[label="List.genericIndex2 yw30 yw31 (Pos (Succ yw400)) (primCmpInt (Pos (Succ yw400)) (Pos Zero) == GT)\n",fontsize=16,color="black",shape="box"];37 -> 39[label="",style="solid", color="black", weight=3];
38[label="List.genericIndex2 yw30 yw31 (Neg (Succ yw400)) (primCmpInt (Neg (Succ yw400)) (Pos Zero) == GT)\n",fontsize=16,color="black",shape="box"];38 -> 40[label="",style="solid", color="black", weight=3];
39[label="List.genericIndex2 yw30 yw31 (Pos (Succ yw400)) (primCmpNat (Succ yw400) Zero == GT)\n",fontsize=16,color="black",shape="box"];39 -> 41[label="",style="solid", color="black", weight=3];
40[label="List.genericIndex2 yw30 yw31 (Neg (Succ yw400)) (LT == GT)\n",fontsize=16,color="black",shape="box"];40 -> 42[label="",style="solid", color="black", weight=3];
41[label="List.genericIndex2 yw30 yw31 (Pos (Succ yw400)) (GT == GT)\n",fontsize=16,color="black",shape="box"];41 -> 43[label="",style="solid", color="black", weight=3];
42[label="List.genericIndex2 yw30 yw31 (Neg (Succ yw400)) False\n",fontsize=16,color="black",shape="box"];42 -> 44[label="",style="solid", color="black", weight=3];
43[label="List.genericIndex2 yw30 yw31 (Pos (Succ yw400)) True\n",fontsize=16,color="black",shape="box"];43 -> 45[label="",style="solid", color="black", weight=3];
44[label="List.genericIndex1 yw30 yw31 (Neg (Succ yw400)) otherwise\n",fontsize=16,color="black",shape="box"];44 -> 46[label="",style="solid", color="black", weight=3];
45 -> 4[label="",style="dashed", color="red", weight=0];
45[label="List.genericIndex yw31 (Pos (Succ yw400) - fromInt (Pos (Succ Zero)))\n",fontsize=16,color="magenta"];45 -> 47[label="",style="dashed", color="magenta", weight=3];
45 -> 48[label="",style="dashed", color="magenta", weight=3];
46[label="List.genericIndex1 yw30 yw31 (Neg (Succ yw400)) True\n",fontsize=16,color="black",shape="box"];46 -> 49[label="",style="solid", color="black", weight=3];
47[label="yw31\n",fontsize=16,color="green",shape="box"];48[label="Pos (Succ yw400) - fromInt (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];48 -> 50[label="",style="solid", color="black", weight=3];
49 -> 10[label="",style="dashed", color="red", weight=0];
49[label="error []\n",fontsize=16,color="magenta"];50[label="primMinusInt (Pos (Succ yw400)) (fromInt (Pos (Succ Zero)))\n",fontsize=16,color="black",shape="box"];50 -> 51[label="",style="solid", color="black", weight=3];
51[label="primMinusInt (Pos (Succ yw400)) (Pos (Succ Zero))\n",fontsize=16,color="black",shape="box"];51 -> 52[label="",style="solid", color="black", weight=3];
52[label="primMinusNat (Succ yw400) (Succ Zero)\n",fontsize=16,color="black",shape="box"];52 -> 53[label="",style="solid", color="black", weight=3];
53[label="primMinusNat yw400 Zero\n",fontsize=16,color="burlywood",shape="box"];68[label="yw400/Succ yw4000",fontsize=10,color="white",style="solid",shape="box"];53 -> 68[label="",style="solid", color="burlywood", weight=9];
68 -> 54[label="",style="solid", color="burlywood", weight=3];
69[label="yw400/Zero",fontsize=10,color="white",style="solid",shape="box"];53 -> 69[label="",style="solid", color="burlywood", weight=9];
69 -> 55[label="",style="solid", color="burlywood", weight=3];
54[label="primMinusNat (Succ yw4000) Zero\n",fontsize=16,color="black",shape="box"];54 -> 56[label="",style="solid", color="black", weight=3];
55[label="primMinusNat Zero Zero\n",fontsize=16,color="black",shape="box"];55 -> 57[label="",style="solid", color="black", weight=3];
56[label="Pos (Succ yw4000)\n",fontsize=16,color="green",shape="box"];57[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_genericIndex(:(yw30, yw31), Pos(Succ(yw400)), ba) → new_genericIndex(yw31, new_primMinusNat(yw400), ba)

The TRS R consists of the following rules:

new_primMinusNat(Succ(yw4000)) → Pos(Succ(yw4000))
new_primMinusNat(Zero) → Pos(Zero)

The set Q consists of the following terms:

new_primMinusNat(Zero)
new_primMinusNat(Succ(x0))

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_genericIndex(:(yw30, yw31), Pos(Succ(yw400)), ba) → new_genericIndex(yw31, new_primMinusNat(yw400), ba)
The graph contains the following edges 1 > 1, 3 >= 3

genericIndex	(x : vw) xw	= genericIndex5 (x : vw) xw
genericIndex	(vx : xs) n	= genericIndex3 (vx : xs) n
genericIndex	vy vz	= genericIndex0 vy vz

genericIndex2	vx xs n True	= genericIndex xs (n - 1)
genericIndex2	vx xs n False	= genericIndex1 vx xs n otherwise

genericIndex1	vx xs n True	= error []
genericIndex1	vx xs n False	= genericIndex0 (vx : xs) n

genericIndex3	(vx : xs) n	= genericIndex2 vx xs n (n > 0)
genericIndex3	wz xu	= genericIndex0 wz xu

genericIndex5	(x : vw) xw	= genericIndex4 (xw == 0) (x : vw) xw
genericIndex5	yu yv	= genericIndex3 yu yv