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

MAYBE H-Termination proof of ../tpdb/FP/full_haskell/List_groupBy_1.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ LR

mainModule Main

((List.groupBy :: (a -> a -> Bool) -> [a] -> [[a]]) :: (a -> a -> Bool) -> [a] -> [[a]])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

_ []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

(\(ys,_) ->ys) vv10

(\(_,zs) ->zs) vv10

module Main where

import qualified List
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified List
import qualified Main
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,zs)→zs

is transformed to

zs0 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys0 (ys,_) = ys

The following Lambda expression

\(_,zs)→zs

is transformed to

zs1 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys1 (ys,_) = ys

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Main

((List.groupBy :: (a -> a -> Bool) -> [a] -> [[a]]) :: (a -> a -> Bool) -> [a] -> [[a]])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

_ []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,_)

zs0 vv10

zs0

(_,zs)

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.
Binding Reductions:
The bind variable of the following binding Pattern

xs@(wu : wv)

is replaced by the following term

wu : wv

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Main

((List.groupBy :: (a -> a -> Bool) -> [a] -> [[a]]) :: (a -> a -> Bool) -> [a] -> [[a]])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

vw []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,vx)

zs0 vv10

zs0

(vy,zs)

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

span p [] = ([],[])

span p (wu : wv)

| p wu

= (wu : ys,zs)

| otherwise

= ([],wu : wv)

where

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

is transformed to

span p [] = span3 p []

span p (wu : wv) = span2 p (wu : wv)

span2 p (wu : wv) =

span1 p wu wv (p wu)

where

span0 p wu wv True = ([],wu : wv)

span1 p wu wv True = (wu : ys,zs)

span1 p wu wv False = span0 p wu wv otherwise

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

span3 p [] = ([],[])

span3 xv xw = span2 xv xw

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule Main

((List.groupBy :: (a -> a -> Bool) -> [a] -> [[a]]) :: (a -> a -> Bool) -> [a] -> [[a]])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy

vw []

[]

groupBy

eq (x : xs)

(x : ys) : groupBy eq zs

where

vv10

span (eq x) xs

ys0 vv10

ys0

(ys,vx)

zs0 vv10

zs0

(vy,zs)

module Main where

import qualified List
import qualified Maybe
import qualified Prelude

module Maybe where

import qualified List
import qualified Main
import qualified Prelude

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

(x : ys) : groupBy eq zs

where

vv10 = span (eq x) xs

ys = ys0 vv10

ys0 (ys,vx) = ys

zs = zs0 vv10

zs0 (vy,zs) = zs

are unpacked to the following functions on top level

groupByYs xx xy xz = groupByYs0 xx xy xz (groupByVv10 xx xy xz)

groupByVv10 xx xy xz = span (xx xy) xz

groupByZs0 xx xy xz (vy,zs) = zs

groupByZs xx xy xz = groupByZs0 xx xy xz (groupByVv10 xx xy xz)

groupByYs0 xx xy xz (ys,vx) = ys

The bindings of the following Let/Where expression

span1 p wu wv (p wu)

where

span0 p wu wv True = ([],wu : wv)

span1 p wu wv True = (wu : ys,zs)

span1 p wu wv False = span0 p wu wv otherwise

vu43 = span p wv

ys = ys1 vu43

ys1 (ys,wx) = ys

zs = zs1 vu43

zs1 (ww,zs) = zs

are unpacked to the following functions on top level

span2Span1 yu yv p wu wv True = (wu : span2Ys yu yv,span2Zs yu yv)

span2Span1 yu yv p wu wv False = span2Span0 yu yv p wu wv otherwise

span2Ys yu yv = span2Ys1 yu yv (span2Vu43 yu yv)

span2Ys1 yu yv (ys,wx) = ys

span2Zs1 yu yv (ww,zs) = zs

span2Zs yu yv = span2Zs1 yu yv (span2Vu43 yu yv)

span2Vu43 yu yv = span yu yv

span2Span0 yu yv p wu wv True = ([],wu : wv)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

mainModule Main

((List.groupBy :: (a -> a -> Bool) -> [a] -> [[a]]) :: (a -> a -> Bool) -> [a] -> [[a]])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy	vw []	=	[]
groupBy	eq (x : xs)	=	(x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

groupByVv10

xx xy xz

span (xx xy) xz

groupByYs

xx xy xz

groupByYs0 xx xy xz (groupByVv10 xx xy xz)

groupByYs0

xx xy xz (ys,vx)

groupByZs

xx xy xz

groupByZs0 xx xy xz (groupByVv10 xx xy xz)

groupByZs0

xx xy xz (vy,zs)

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

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

mainModule Main

(List.groupBy :: (a -> a -> Bool) -> [a] -> [[a]])

module List where

import qualified Main
import qualified Maybe
import qualified Prelude

groupBy :: (a -> a -> Bool) -> [a] -> [[a]]

groupBy	vw []	=	[]
groupBy	eq (x : xs)	=	(x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

groupByVv10

xx xy xz

span (xx xy) xz

groupByYs

xx xy xz

groupByYs0 xx xy xz (groupByVv10 xx xy xz)

groupByYs0

xx xy xz (ys,vx)

groupByZs

xx xy xz

groupByZs0 xx xy xz (groupByVv10 xx xy xz)

groupByZs0

xx xy xz (vy,zs)

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.groupBy\n",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="List.groupBy yw3\n",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="List.groupBy yw3 yw4\n",fontsize=16,color="burlywood",shape="triangle"];113[label="yw4/yw40 : yw41",fontsize=10,color="white",style="solid",shape="box"];4 -> 113[label="",style="solid", color="burlywood", weight=9];
113 -> 5[label="",style="solid", color="burlywood", weight=3];
114[label="yw4/[]",fontsize=10,color="white",style="solid",shape="box"];4 -> 114[label="",style="solid", color="burlywood", weight=9];
114 -> 6[label="",style="solid", color="burlywood", weight=3];
5[label="List.groupBy yw3 (yw40 : yw41)\n",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="List.groupBy yw3 []\n",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="(yw40 : List.groupByYs yw3 yw40 yw41) : List.groupBy yw3 (List.groupByZs yw3 yw40 yw41)\n",fontsize=16,color="green",shape="box"];7 -> 9[label="",style="dashed", color="green", weight=3];
7 -> 10[label="",style="dashed", color="green", weight=3];
8[label="[]\n",fontsize=16,color="green",shape="box"];9[label="List.groupByYs yw3 yw40 yw41\n",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10 -> 4[label="",style="dashed", color="red", weight=0];
10[label="List.groupBy yw3 (List.groupByZs yw3 yw40 yw41)\n",fontsize=16,color="magenta"];10 -> 12[label="",style="dashed", color="magenta", weight=3];
11[label="List.groupByYs0 yw3 yw40 yw41 (List.groupByVv10 yw3 yw40 yw41)\n",fontsize=16,color="black",shape="box"];11 -> 13[label="",style="solid", color="black", weight=3];
12[label="List.groupByZs yw3 yw40 yw41\n",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="List.groupByYs0 yw3 yw40 yw41 (span (yw3 yw40) yw41)\n",fontsize=16,color="burlywood",shape="box"];116[label="yw41/yw410 : yw411",fontsize=10,color="white",style="solid",shape="box"];13 -> 116[label="",style="solid", color="burlywood", weight=9];
116 -> 15[label="",style="solid", color="burlywood", weight=3];
117[label="yw41/[]",fontsize=10,color="white",style="solid",shape="box"];13 -> 117[label="",style="solid", color="burlywood", weight=9];
117 -> 16[label="",style="solid", color="burlywood", weight=3];
14[label="List.groupByZs0 yw3 yw40 yw41 (List.groupByVv10 yw3 yw40 yw41)\n",fontsize=16,color="black",shape="box"];14 -> 17[label="",style="solid", color="black", weight=3];
15[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span (yw3 yw40) (yw410 : yw411))\n",fontsize=16,color="black",shape="box"];15 -> 18[label="",style="solid", color="black", weight=3];
16[label="List.groupByYs0 yw3 yw40 [] (span (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];16 -> 19[label="",style="solid", color="black", weight=3];
17[label="List.groupByZs0 yw3 yw40 yw41 (span (yw3 yw40) yw41)\n",fontsize=16,color="burlywood",shape="box"];118[label="yw41/yw410 : yw411",fontsize=10,color="white",style="solid",shape="box"];17 -> 118[label="",style="solid", color="burlywood", weight=9];
118 -> 20[label="",style="solid", color="burlywood", weight=3];
119[label="yw41/[]",fontsize=10,color="white",style="solid",shape="box"];17 -> 119[label="",style="solid", color="burlywood", weight=9];
119 -> 21[label="",style="solid", color="burlywood", weight=3];
18[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span2 (yw3 yw40) (yw410 : yw411))\n",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="List.groupByYs0 yw3 yw40 [] (span3 (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span (yw3 yw40) (yw410 : yw411))\n",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="List.groupByZs0 yw3 yw40 [] (span (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22 -> 26[label="",style="dashed", color="red", weight=0];
22[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 (yw3 yw40 yw410))\n",fontsize=16,color="magenta"];22 -> 27[label="",style="dashed", color="magenta", weight=3];
23[label="List.groupByYs0 yw3 yw40 [] ([],[])\n",fontsize=16,color="black",shape="box"];23 -> 28[label="",style="solid", color="black", weight=3];
24[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span2 (yw3 yw40) (yw410 : yw411))\n",fontsize=16,color="black",shape="box"];24 -> 29[label="",style="solid", color="black", weight=3];
25[label="List.groupByZs0 yw3 yw40 [] (span3 (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];25 -> 30[label="",style="solid", color="black", weight=3];
27[label="yw3 yw40 yw410\n",fontsize=16,color="green",shape="box"];27 -> 35[label="",style="dashed", color="green", weight=3];
27 -> 36[label="",style="dashed", color="green", weight=3];
26[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 yw5)\n",fontsize=16,color="burlywood",shape="triangle"];121[label="yw5/False",fontsize=10,color="white",style="solid",shape="box"];26 -> 121[label="",style="solid", color="burlywood", weight=9];
121 -> 33[label="",style="solid", color="burlywood", weight=3];
122[label="yw5/True",fontsize=10,color="white",style="solid",shape="box"];26 -> 122[label="",style="solid", color="burlywood", weight=9];
122 -> 34[label="",style="solid", color="burlywood", weight=3];
28[label="[]\n",fontsize=16,color="green",shape="box"];29 -> 37[label="",style="dashed", color="red", weight=0];
29[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 (yw3 yw40 yw410))\n",fontsize=16,color="magenta"];29 -> 38[label="",style="dashed", color="magenta", weight=3];
30[label="List.groupByZs0 yw3 yw40 [] ([],[])\n",fontsize=16,color="black",shape="box"];30 -> 39[label="",style="solid", color="black", weight=3];
35[label="yw40\n",fontsize=16,color="green",shape="box"];36[label="yw410\n",fontsize=16,color="green",shape="box"];33[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 False)\n",fontsize=16,color="black",shape="box"];33 -> 40[label="",style="solid", color="black", weight=3];
34[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 True)\n",fontsize=16,color="black",shape="box"];34 -> 41[label="",style="solid", color="black", weight=3];
38[label="yw3 yw40 yw410\n",fontsize=16,color="green",shape="box"];38 -> 46[label="",style="dashed", color="green", weight=3];
38 -> 47[label="",style="dashed", color="green", weight=3];
37[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 yw6)\n",fontsize=16,color="burlywood",shape="triangle"];124[label="yw6/False",fontsize=10,color="white",style="solid",shape="box"];37 -> 124[label="",style="solid", color="burlywood", weight=9];
124 -> 44[label="",style="solid", color="burlywood", weight=3];
125[label="yw6/True",fontsize=10,color="white",style="solid",shape="box"];37 -> 125[label="",style="solid", color="burlywood", weight=9];
125 -> 45[label="",style="solid", color="burlywood", weight=3];
39[label="[]\n",fontsize=16,color="green",shape="box"];40[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span2Span0 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 otherwise)\n",fontsize=16,color="black",shape="box"];40 -> 48[label="",style="solid", color="black", weight=3];
41[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (yw410 : span2Ys (yw3 yw40) yw411,span2Zs (yw3 yw40) yw411)\n",fontsize=16,color="black",shape="box"];41 -> 49[label="",style="solid", color="black", weight=3];
46[label="yw40\n",fontsize=16,color="green",shape="box"];47[label="yw410\n",fontsize=16,color="green",shape="box"];44[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 False)\n",fontsize=16,color="black",shape="box"];44 -> 50[label="",style="solid", color="black", weight=3];
45[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span2Span1 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 True)\n",fontsize=16,color="black",shape="box"];45 -> 51[label="",style="solid", color="black", weight=3];
48[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) (span2Span0 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 True)\n",fontsize=16,color="black",shape="box"];48 -> 52[label="",style="solid", color="black", weight=3];
49[label="yw410 : span2Ys (yw3 yw40) yw411\n",fontsize=16,color="green",shape="box"];49 -> 53[label="",style="dashed", color="green", weight=3];
50[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span2Span0 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 otherwise)\n",fontsize=16,color="black",shape="box"];50 -> 54[label="",style="solid", color="black", weight=3];
51[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (yw410 : span2Ys (yw3 yw40) yw411,span2Zs (yw3 yw40) yw411)\n",fontsize=16,color="black",shape="box"];51 -> 55[label="",style="solid", color="black", weight=3];
52[label="List.groupByYs0 yw3 yw40 (yw410 : yw411) ([],yw410 : yw411)\n",fontsize=16,color="black",shape="box"];52 -> 56[label="",style="solid", color="black", weight=3];
53[label="span2Ys (yw3 yw40) yw411\n",fontsize=16,color="black",shape="triangle"];53 -> 57[label="",style="solid", color="black", weight=3];
54[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) (span2Span0 (yw3 yw40) yw411 (yw3 yw40) yw410 yw411 True)\n",fontsize=16,color="black",shape="box"];54 -> 58[label="",style="solid", color="black", weight=3];
55[label="span2Zs (yw3 yw40) yw411\n",fontsize=16,color="black",shape="triangle"];55 -> 59[label="",style="solid", color="black", weight=3];
56[label="[]\n",fontsize=16,color="green",shape="box"];57[label="span2Ys1 (yw3 yw40) yw411 (span2Vu43 (yw3 yw40) yw411)\n",fontsize=16,color="black",shape="box"];57 -> 60[label="",style="solid", color="black", weight=3];
58[label="List.groupByZs0 yw3 yw40 (yw410 : yw411) ([],yw410 : yw411)\n",fontsize=16,color="black",shape="box"];58 -> 61[label="",style="solid", color="black", weight=3];
59[label="span2Zs1 (yw3 yw40) yw411 (span2Vu43 (yw3 yw40) yw411)\n",fontsize=16,color="black",shape="box"];59 -> 62[label="",style="solid", color="black", weight=3];
60[label="span2Ys1 (yw3 yw40) yw411 (span (yw3 yw40) yw411)\n",fontsize=16,color="burlywood",shape="box"];126[label="yw411/yw4110 : yw4111",fontsize=10,color="white",style="solid",shape="box"];60 -> 126[label="",style="solid", color="burlywood", weight=9];
126 -> 63[label="",style="solid", color="burlywood", weight=3];
127[label="yw411/[]",fontsize=10,color="white",style="solid",shape="box"];60 -> 127[label="",style="solid", color="burlywood", weight=9];
127 -> 64[label="",style="solid", color="burlywood", weight=3];
61[label="yw410 : yw411\n",fontsize=16,color="green",shape="box"];62[label="span2Zs1 (yw3 yw40) yw411 (span (yw3 yw40) yw411)\n",fontsize=16,color="burlywood",shape="box"];128[label="yw411/yw4110 : yw4111",fontsize=10,color="white",style="solid",shape="box"];62 -> 128[label="",style="solid", color="burlywood", weight=9];
128 -> 65[label="",style="solid", color="burlywood", weight=3];
129[label="yw411/[]",fontsize=10,color="white",style="solid",shape="box"];62 -> 129[label="",style="solid", color="burlywood", weight=9];
129 -> 66[label="",style="solid", color="burlywood", weight=3];
63[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span (yw3 yw40) (yw4110 : yw4111))\n",fontsize=16,color="black",shape="box"];63 -> 67[label="",style="solid", color="black", weight=3];
64[label="span2Ys1 (yw3 yw40) [] (span (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];64 -> 68[label="",style="solid", color="black", weight=3];
65[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span (yw3 yw40) (yw4110 : yw4111))\n",fontsize=16,color="black",shape="box"];65 -> 69[label="",style="solid", color="black", weight=3];
66[label="span2Zs1 (yw3 yw40) [] (span (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];66 -> 70[label="",style="solid", color="black", weight=3];
67[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span2 (yw3 yw40) (yw4110 : yw4111))\n",fontsize=16,color="black",shape="box"];67 -> 71[label="",style="solid", color="black", weight=3];
68[label="span2Ys1 (yw3 yw40) [] (span3 (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];68 -> 72[label="",style="solid", color="black", weight=3];
69[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span2 (yw3 yw40) (yw4110 : yw4111))\n",fontsize=16,color="black",shape="box"];69 -> 73[label="",style="solid", color="black", weight=3];
70[label="span2Zs1 (yw3 yw40) [] (span3 (yw3 yw40) [])\n",fontsize=16,color="black",shape="box"];70 -> 74[label="",style="solid", color="black", weight=3];
71 -> 75[label="",style="dashed", color="red", weight=0];
71[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 (yw3 yw40 yw4110))\n",fontsize=16,color="magenta"];71 -> 76[label="",style="dashed", color="magenta", weight=3];
72[label="span2Ys1 (yw3 yw40) [] ([],[])\n",fontsize=16,color="black",shape="box"];72 -> 77[label="",style="solid", color="black", weight=3];
73 -> 78[label="",style="dashed", color="red", weight=0];
73[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 (yw3 yw40 yw4110))\n",fontsize=16,color="magenta"];73 -> 79[label="",style="dashed", color="magenta", weight=3];
74[label="span2Zs1 (yw3 yw40) [] ([],[])\n",fontsize=16,color="black",shape="box"];74 -> 80[label="",style="solid", color="black", weight=3];
76[label="yw3 yw40 yw4110\n",fontsize=16,color="green",shape="box"];76 -> 81[label="",style="dashed", color="green", weight=3];
76 -> 82[label="",style="dashed", color="green", weight=3];
75[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 yw7)\n",fontsize=16,color="burlywood",shape="triangle"];132[label="yw7/False",fontsize=10,color="white",style="solid",shape="box"];75 -> 132[label="",style="solid", color="burlywood", weight=9];
132 -> 83[label="",style="solid", color="burlywood", weight=3];
133[label="yw7/True",fontsize=10,color="white",style="solid",shape="box"];75 -> 133[label="",style="solid", color="burlywood", weight=9];
133 -> 84[label="",style="solid", color="burlywood", weight=3];
77[label="[]\n",fontsize=16,color="green",shape="box"];79[label="yw3 yw40 yw4110\n",fontsize=16,color="green",shape="box"];79 -> 89[label="",style="dashed", color="green", weight=3];
79 -> 90[label="",style="dashed", color="green", weight=3];
78[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 yw8)\n",fontsize=16,color="burlywood",shape="triangle"];134[label="yw8/False",fontsize=10,color="white",style="solid",shape="box"];78 -> 134[label="",style="solid", color="burlywood", weight=9];
134 -> 87[label="",style="solid", color="burlywood", weight=3];
135[label="yw8/True",fontsize=10,color="white",style="solid",shape="box"];78 -> 135[label="",style="solid", color="burlywood", weight=9];
135 -> 88[label="",style="solid", color="burlywood", weight=3];
80[label="[]\n",fontsize=16,color="green",shape="box"];81[label="yw40\n",fontsize=16,color="green",shape="box"];82[label="yw4110\n",fontsize=16,color="green",shape="box"];83[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 False)\n",fontsize=16,color="black",shape="box"];83 -> 91[label="",style="solid", color="black", weight=3];
84[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 True)\n",fontsize=16,color="black",shape="box"];84 -> 92[label="",style="solid", color="black", weight=3];
89[label="yw40\n",fontsize=16,color="green",shape="box"];90[label="yw4110\n",fontsize=16,color="green",shape="box"];87[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 False)\n",fontsize=16,color="black",shape="box"];87 -> 93[label="",style="solid", color="black", weight=3];
88[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span2Span1 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 True)\n",fontsize=16,color="black",shape="box"];88 -> 94[label="",style="solid", color="black", weight=3];
91[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span2Span0 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 otherwise)\n",fontsize=16,color="black",shape="box"];91 -> 95[label="",style="solid", color="black", weight=3];
92 -> 96[label="",style="dashed", color="red", weight=0];
92[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (yw4110 : span2Ys (yw3 yw40) yw4111,span2Zs (yw3 yw40) yw4111)\n",fontsize=16,color="magenta"];92 -> 97[label="",style="dashed", color="magenta", weight=3];
92 -> 98[label="",style="dashed", color="magenta", weight=3];
93[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span2Span0 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 otherwise)\n",fontsize=16,color="black",shape="box"];93 -> 99[label="",style="solid", color="black", weight=3];
94 -> 100[label="",style="dashed", color="red", weight=0];
94[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (yw4110 : span2Ys (yw3 yw40) yw4111,span2Zs (yw3 yw40) yw4111)\n",fontsize=16,color="magenta"];94 -> 101[label="",style="dashed", color="magenta", weight=3];
94 -> 102[label="",style="dashed", color="magenta", weight=3];
95[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (span2Span0 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 True)\n",fontsize=16,color="black",shape="box"];95 -> 103[label="",style="solid", color="black", weight=3];
97 -> 55[label="",style="dashed", color="red", weight=0];
97[label="span2Zs (yw3 yw40) yw4111\n",fontsize=16,color="magenta"];97 -> 104[label="",style="dashed", color="magenta", weight=3];
98 -> 53[label="",style="dashed", color="red", weight=0];
98[label="span2Ys (yw3 yw40) yw4111\n",fontsize=16,color="magenta"];98 -> 105[label="",style="dashed", color="magenta", weight=3];
96[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) (yw4110 : yw10,yw9)\n",fontsize=16,color="black",shape="triangle"];96 -> 106[label="",style="solid", color="black", weight=3];
99[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (span2Span0 (yw3 yw40) yw4111 (yw3 yw40) yw4110 yw4111 True)\n",fontsize=16,color="black",shape="box"];99 -> 107[label="",style="solid", color="black", weight=3];
101 -> 53[label="",style="dashed", color="red", weight=0];
101[label="span2Ys (yw3 yw40) yw4111\n",fontsize=16,color="magenta"];101 -> 108[label="",style="dashed", color="magenta", weight=3];
102 -> 55[label="",style="dashed", color="red", weight=0];
102[label="span2Zs (yw3 yw40) yw4111\n",fontsize=16,color="magenta"];102 -> 109[label="",style="dashed", color="magenta", weight=3];
100[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) (yw4110 : yw12,yw11)\n",fontsize=16,color="black",shape="triangle"];100 -> 110[label="",style="solid", color="black", weight=3];
103[label="span2Ys1 (yw3 yw40) (yw4110 : yw4111) ([],yw4110 : yw4111)\n",fontsize=16,color="black",shape="box"];103 -> 111[label="",style="solid", color="black", weight=3];
104[label="yw4111\n",fontsize=16,color="green",shape="box"];105[label="yw4111\n",fontsize=16,color="green",shape="box"];106[label="yw4110 : yw10\n",fontsize=16,color="green",shape="box"];107[label="span2Zs1 (yw3 yw40) (yw4110 : yw4111) ([],yw4110 : yw4111)\n",fontsize=16,color="black",shape="box"];107 -> 112[label="",style="solid", color="black", weight=3];
108[label="yw4111\n",fontsize=16,color="green",shape="box"];109[label="yw4111\n",fontsize=16,color="green",shape="box"];110[label="yw11\n",fontsize=16,color="green",shape="box"];111[label="[]\n",fontsize=16,color="green",shape="box"];112[label="yw4110 : yw4111\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_span2Zs1(yw3, yw40, yw4110, yw4111, ba) → new_span2Ys(yw3, yw40, yw4111, ba)
new_span2Ys1(yw3, yw40, yw4110, yw4111, ba) → new_span2Ys(yw3, yw40, yw4111, ba)
new_span2Zs1(yw3, yw40, yw4110, yw4111, ba) → new_span2Zs(yw3, yw40, yw4111, ba)
new_span2Ys(yw3, yw40, :(yw4110, yw4111), ba) → new_span2Ys1(yw3, yw40, yw4110, yw4111, ba)
new_span2Zs(yw3, yw40, :(yw4110, yw4111), ba) → new_span2Zs1(yw3, yw40, yw4110, yw4111, ba)
new_span2Ys1(yw3, yw40, yw4110, yw4111, ba) → new_span2Zs(yw3, yw40, yw4111, ba)

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_span2Ys(yw3, yw40, :(yw4110, yw4111), ba) → new_span2Ys1(yw3, yw40, yw4110, yw4111, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 5
new_span2Zs(yw3, yw40, :(yw4110, yw4111), ba) → new_span2Zs1(yw3, yw40, yw4110, yw4111, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 5
new_span2Ys1(yw3, yw40, yw4110, yw4111, ba) → new_span2Ys(yw3, yw40, yw4111, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
new_span2Ys1(yw3, yw40, yw4110, yw4111, ba) → new_span2Zs(yw3, yw40, yw4111, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
new_span2Zs1(yw3, yw40, yw4110, yw4111, ba) → new_span2Ys(yw3, yw40, yw4111, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
new_span2Zs1(yw3, yw40, yw4110, yw4111, ba) → new_span2Zs(yw3, yw40, yw4111, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ NumRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ NonTerminationProof

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

new_groupBy(yw3, ba) → new_groupBy(yw3, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_groupBy(yw3, ba) → new_groupBy(yw3, ba)

The TRS R consists of the following rules:none

s = new_groupBy(yw3, ba) evaluates to t =new_groupBy(yw3, ba)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_groupBy(yw3, ba) to new_groupBy(yw3, ba).

span2Span1	yu yv p wu wv True	= (wu : span2Ys yu yv,span2Zs yu yv)
span2Span1	yu yv p wu wv False	= span2Span0 yu yv p wu wv otherwise