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



↳ HASKELL
  ↳ LR

mainModule Main
  ((List.group :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]]) :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]])

module List where
  import qualified Main
import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = (\(ys,_) ->ys) vv10
zs = (\(_,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.group :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]]) :: (Eq b, Eq a) => [(b,a)]  ->  [[(b,a)]])

module List where
  import qualified Main
import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,_) = ys
zs = zs0 vv10
zs0 (_,zs) = 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@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR

mainModule Main
  ((List.group :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]]) :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]])

module List where
  import qualified Main
import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(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


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 (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

span3 p [] = ([],[])
span3 yz zu = span2 yz zu



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed

mainModule Main
  ((List.group :: (Eq a, Eq b) => [(a,b)]  ->  [[(a,b)]]) :: (Eq a, Eq b) => [(a,b)]  ->  [[(a,b)]])

module List where
  import qualified Main
import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(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


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
groupByVv10 zv zw zx = span (zv zw) zx

groupByZs zv zw zx = groupByZs0 zv zw zx (groupByVv10 zv zw zx)

groupByZs0 zv zw zx (vy,zs) = zs

groupByYs zv zw zx = groupByYs0 zv zw zx (groupByVv10 zv zw zx)

groupByYs0 zv zw zx (ys,vx) = ys

The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

are unpacked to the following functions on top level
span2Span1 zy zz p ww wx True = (ww : span2Ys zy zz,span2Zs zy zz)
span2Span1 zy zz p ww wx False = span2Span0 zy zz p ww wx otherwise

span2Zs1 zy zz (wy,zs) = zs

span2Vu43 zy zz = span zy zz

span2Span0 zy zz p ww wx True = ([],ww : wx)

span2Zs zy zz = span2Zs1 zy zz (span2Vu43 zy zz)

span2Ys zy zz = span2Ys1 zy zz (span2Vu43 zy zz)

span2Ys1 zy zz (ys,wz) = ys



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed

mainModule Main
  ((List.group :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]]) :: (Eq a, Eq b) => [(b,a)]  ->  [[(b,a)]])

module List where
  import qualified Main
import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

  
groupByVv10 zv zw zx = span (zv zw) zx

  
groupByYs zv zw zx = groupByYs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByYs0 zv zw zx (ys,vx) = ys

  
groupByZs zv zw zx = groupByZs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByZs0 zv zw zx (vy,zs) = 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.group :: (Eq a, Eq b) => [(a,b)]  ->  [[(a,b)]])

module List where
  import qualified Main
import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

  
groupByVv10 zv zw zx = span (zv zw) zx

  
groupByYs zv zw zx = groupByYs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByYs0 zv zw zx (ys,vx) = ys

  
groupByZs zv zw zx = groupByZs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByZs0 zv zw zx (vy,zs) = 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


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

new_primMulNat(Succ(vuu300100), Succ(vuu3100100)) → new_primMulNat(vuu300100, Succ(vuu3100100))

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: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

new_primPlusNat(Succ(vuu7500), Succ(vuu31001000)) → new_primPlusNat(vuu7500, vuu31001000)

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: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPOrderProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

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

new_groupBy(:(vuu30, vuu31), ba, bb) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba, bb), ba, bb)

The TRS R consists of the following rules:

new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(ty_Maybe, bdf)) → new_esEs15(vuu3000, vuu31000, bdf)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Double) → new_esEs18(vuu3001, vuu31001)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_primPlusNat1(Succ(vuu7500), Succ(vuu31001000)) → Succ(Succ(new_primPlusNat1(vuu7500, vuu31001000)))
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_esEs21(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Int) → new_esEs10(vuu3002, vuu31002)
new_esEs24(vuu3001, vuu31001, app(app(ty_@2, bfe), bff)) → new_esEs4(vuu3001, vuu31001, bfe, bff)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Char, bd) → new_esEs13(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Double) → new_esEs18(vuu300, vuu3100)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(ty_[], gh)) → new_esEs6(vuu3001, vuu31001, gh)
new_esEs7(vuu3000, vuu31000, app(app(app(ty_@3, he), hf), hg)) → new_esEs11(vuu3000, vuu31000, he, hf, hg)
new_esEs26(vuu300, vuu3100, app(ty_Ratio, cc)) → new_esEs16(vuu300, vuu3100, cc)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bec), bed)) → new_esEs4(vuu3000, vuu31000, bec, bed)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_[], bcf), bd) → new_esEs6(vuu3000, vuu31000, bcf)
new_esEs22(vuu3001, vuu31001, ty_Float) → new_esEs14(vuu3001, vuu31001)
new_esEs6(:(vuu3000, vuu3001), :(vuu31000, vuu31001), cd) → new_asAs(new_esEs7(vuu3000, vuu31000, cd), new_esEs6(vuu3001, vuu31001, cd))
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_esEs26(vuu300, vuu3100, ty_Int) → new_esEs10(vuu300, vuu3100)
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_esEs7(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs27(vuu301, vuu3101, ty_Bool) → new_esEs17(vuu301, vuu3101)
new_esEs27(vuu301, vuu3101, app(ty_Ratio, df)) → new_esEs16(vuu301, vuu3101, df)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(vuu301, vuu3101, app(app(app(ty_@3, db), dc), dd)) → new_esEs11(vuu301, vuu3101, db, dc, dd)
new_esEs24(vuu3001, vuu31001, ty_Char) → new_esEs13(vuu3001, vuu31001)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bcd), bd) → new_esEs15(vuu3000, vuu31000, bcd)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(app(ty_Either, bcg), bch)) → new_esEs9(vuu3000, vuu31000, bcg, bch)
new_esEs7(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(ty_Maybe, cb)) → new_esEs15(vuu300, vuu3100, cb)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(app(ty_@2, bgg), bgh)) → new_esEs4(vuu3002, vuu31002, bgg, bgh)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_primPlusNat0(Zero, vuu3100100) → Succ(vuu3100100)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bee), bef), beg)) → new_esEs11(vuu3000, vuu31000, bee, bef, beg)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(ty_[], bdh)) → new_esEs6(vuu3000, vuu31000, bdh)
new_esEs22(vuu3001, vuu31001, ty_Bool) → new_esEs17(vuu3001, vuu31001)
new_esEs19(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Bool) → new_esEs17(vuu3002, vuu31002)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, bca), bcb), bcc), bd) → new_esEs11(vuu3000, vuu31000, bca, bcb, bcc)
new_esEs25(vuu3002, vuu31002, app(ty_Ratio, bhe)) → new_esEs16(vuu3002, vuu31002, bhe)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, False, eb, ec) → []
new_esEs24(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_sr(Neg(vuu30010), Pos(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_sr(Pos(vuu30010), Neg(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_esEs17(True, True) → True
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, True, dh, ea) → new_span2Zs0(vuu57, vuu58, vuu61, dh, ea)
new_esEs24(vuu3001, vuu31001, app(ty_Maybe, bgb)) → new_esEs15(vuu3001, vuu31001, bgb)
new_esEs7(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_@0, bd) → new_esEs12(vuu3000, vuu31000)
new_esEs20(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(app(app(ty_@3, bha), bhb), bhc)) → new_esEs11(vuu3002, vuu31002, bha, bhb, bhc)
new_esEs24(vuu3001, vuu31001, app(ty_[], bgd)) → new_esEs6(vuu3001, vuu31001, bgd)
new_esEs22(vuu3001, vuu31001, ty_Double) → new_esEs18(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, app(app(ty_@2, ef), eg)) → new_esEs4(vuu3000, vuu31000, ef, eg)
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bag), bah), bba)) → new_esEs11(vuu3000, vuu31000, bag, bah, bba)
new_esEs12(@0, @0) → True
new_esEs21(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Char) → new_esEs13(vuu300, vuu3100)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(app(ty_@2, bda), bdb)) → new_esEs4(vuu3000, vuu31000, bda, bdb)
new_esEs7(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, beh)) → new_esEs15(vuu3000, vuu31000, beh)
new_esEs26(vuu300, vuu3100, app(app(ty_Either, bc), bd)) → new_esEs9(vuu300, vuu3100, bc, bd)
new_primEqNat0(Zero, Succ(vuu3100000)) → False
new_primEqNat0(Succ(vuu300000), Zero) → False
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bea), beb)) → new_esEs9(vuu3000, vuu31000, bea, beb)
new_esEs22(vuu3001, vuu31001, app(app(ty_Either, fg), fh)) → new_esEs9(vuu3001, vuu31001, fg, fh)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_groupByZs0(vuu30, [], ba, bb) → []
new_groupByZs0(@2(vuu300, vuu301), :(@2(vuu3100, vuu3101), vuu311), ba, bb) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_asAs(new_esEs26(vuu300, vuu3100, ba), new_esEs27(vuu301, vuu3101, bb)), ba, bb)
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bbg), bbh), bd) → new_esEs4(vuu3000, vuu31000, bbg, bbh)
new_esEs18(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs10(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs15(Nothing, Nothing, cb) → True
new_esEs27(vuu301, vuu3101, app(ty_Maybe, de)) → new_esEs15(vuu301, vuu3101, de)
new_esEs24(vuu3001, vuu31001, ty_Float) → new_esEs14(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(app(ty_@2, ga), gb)) → new_esEs4(vuu3001, vuu31001, ga, gb)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(app(app(ty_@3, bg), bh), ca)) → new_esEs11(vuu300, vuu3100, bg, bh, ca)
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs7(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, False, dh, ea) → :(vuu610, vuu611)
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, True, dh, ea) → new_span2Zs11(vuu57, vuu58, vuu610, vuu611, new_span2Ys0(vuu57, vuu58, vuu611, dh, ea), new_span2Zs0(vuu57, vuu58, vuu611, dh, ea), dh, ea)
new_esEs5(EQ, LT) → False
new_esEs5(LT, EQ) → False
new_esEs7(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs6([], :(vuu31000, vuu31001), cd) → False
new_esEs6(:(vuu3000, vuu3001), [], cd) → False
new_span2Ys11(vuu37, vuu38, vuu410, vuu411, vuu72, vuu71, eb, ec) → :(vuu410, vuu72)
new_esEs22(vuu3001, vuu31001, ty_@0) → new_esEs12(vuu3001, vuu31001)
new_esEs7(vuu3000, vuu31000, app(ty_[], bab)) → new_esEs6(vuu3000, vuu31000, bab)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, False, dh, ea) → :(@2(vuu59, vuu60), vuu61)
new_esEs21(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs7(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bfa)) → new_esEs16(vuu3000, vuu31000, bfa)
new_esEs22(vuu3001, vuu31001, app(ty_Ratio, gg)) → new_esEs16(vuu3001, vuu31001, gg)
new_esEs25(vuu3002, vuu31002, ty_Ordering) → new_esEs5(vuu3002, vuu31002)
new_esEs25(vuu3002, vuu31002, ty_@0) → new_esEs12(vuu3002, vuu31002)
new_esEs27(vuu301, vuu3101, ty_Double) → new_esEs18(vuu301, vuu3101)
new_esEs26(vuu300, vuu3100, app(ty_[], cd)) → new_esEs6(vuu300, vuu3100, cd)
new_sr(Neg(vuu30010), Neg(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_[], bbd)) → new_esEs6(vuu3000, vuu31000, bbd)
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bbc)) → new_esEs16(vuu3000, vuu31000, bbc)
new_esEs19(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_span2Ys0(vuu37, vuu38, [], eb, ec) → []
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_sr(Pos(vuu30010), Pos(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_asAs(False, vuu68) → False
new_primEqNat0(Zero, Zero) → True
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Float, bd) → new_esEs14(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300100), Zero) → Zero
new_primMulNat0(Zero, Succ(vuu3100100)) → Zero
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(ty_Ratio, bdg)) → new_esEs16(vuu3000, vuu31000, bdg)
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bae), baf)) → new_esEs4(vuu3000, vuu31000, bae, baf)
new_esEs25(vuu3002, vuu31002, ty_Integer) → new_esEs8(vuu3002, vuu31002)
new_esEs27(vuu301, vuu3101, ty_Char) → new_esEs13(vuu301, vuu3101)
new_esEs17(False, False) → True
new_esEs21(vuu3000, vuu31000, app(ty_Maybe, fc)) → new_esEs15(vuu3000, vuu31000, fc)
new_esEs17(True, False) → False
new_esEs17(False, True) → False
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(ty_Either, bbe), bbf), bd) → new_esEs9(vuu3000, vuu31000, bbe, bbf)
new_esEs8(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs13(Char(vuu3000), Char(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Ordering) → new_esEs5(vuu300, vuu3100)
new_esEs11(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), bg, bh, ca) → new_asAs(new_esEs23(vuu3000, vuu31000, bg), new_asAs(new_esEs24(vuu3001, vuu31001, bh), new_esEs25(vuu3002, vuu31002, ca)))
new_esEs24(vuu3001, vuu31001, ty_Bool) → new_esEs17(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(ty_Maybe, bhd)) → new_esEs15(vuu3002, vuu31002, bhd)
new_esEs14(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs10(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_primPlusNat0(Succ(vuu750), vuu3100100) → Succ(Succ(new_primPlusNat1(vuu750, vuu3100100)))
new_esEs26(vuu300, vuu3100, ty_Integer) → new_esEs8(vuu300, vuu3100)
new_esEs7(vuu3000, vuu31000, app(app(ty_@2, hc), hd)) → new_esEs4(vuu3000, vuu31000, hc, hd)
new_esEs5(EQ, EQ) → True
new_esEs7(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs27(vuu301, vuu3101, ty_Integer) → new_esEs8(vuu301, vuu3101)
new_esEs22(vuu3001, vuu31001, ty_Ordering) → new_esEs5(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, app(ty_Ratio, fd)) → new_esEs16(vuu3000, vuu31000, fd)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_Ratio, bce), bd) → new_esEs16(vuu3000, vuu31000, bce)
new_span2Zs0(vuu57, vuu58, [], dh, ea) → []
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Int, bd) → new_esEs10(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(ty_[], bhf)) → new_esEs6(vuu3002, vuu31002, bhf)
new_esEs4(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), be, bf) → new_asAs(new_esEs21(vuu3000, vuu31000, be), new_esEs22(vuu3001, vuu31001, bf))
new_esEs23(vuu3000, vuu31000, app(ty_[], bfb)) → new_esEs6(vuu3000, vuu31000, bfb)
new_esEs27(vuu301, vuu3101, app(app(ty_@2, cg), da)) → new_esEs4(vuu301, vuu3101, cg, da)
new_esEs6([], [], cd) → True
new_esEs7(vuu3000, vuu31000, app(ty_Maybe, hh)) → new_esEs15(vuu3000, vuu31000, hh)
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_Maybe, bbb)) → new_esEs15(vuu3000, vuu31000, bbb)
new_primPlusNat1(Succ(vuu7500), Zero) → Succ(vuu7500)
new_primPlusNat1(Zero, Succ(vuu31001000)) → Succ(vuu31001000)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, ty_Char) → new_esEs13(vuu3001, vuu31001)
new_esEs26(vuu300, vuu3100, ty_Bool) → new_esEs17(vuu300, vuu3100)
new_esEs22(vuu3001, vuu31001, app(ty_Maybe, gf)) → new_esEs15(vuu3001, vuu31001, gf)
new_esEs25(vuu3002, vuu31002, app(app(ty_Either, bge), bgf)) → new_esEs9(vuu3002, vuu31002, bge, bgf)
new_esEs25(vuu3002, vuu31002, ty_Double) → new_esEs18(vuu3002, vuu31002)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bac), bad)) → new_esEs9(vuu3000, vuu31000, bac, bad)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs11(vuu3000, vuu31000, bdc, bdd, bde)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Ordering, bd) → new_esEs5(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Ordering) → new_esEs5(vuu3001, vuu31001)
new_esEs5(GT, GT) → True
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_esEs21(vuu3000, vuu31000, app(ty_[], ff)) → new_esEs6(vuu3000, vuu31000, ff)
new_esEs22(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, vuu74, vuu73, dh, ea) → vuu73
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, True, eb, ec) → new_span2Ys11(vuu37, vuu38, vuu410, vuu411, new_span2Ys0(vuu37, vuu38, vuu411, eb, ec), new_span2Zs0(vuu37, vuu38, vuu411, eb, ec), eb, ec)
new_esEs7(vuu3000, vuu31000, app(app(ty_Either, ha), hb)) → new_esEs9(vuu3000, vuu31000, ha, hb)
new_esEs5(LT, LT) → True
new_primPlusNat1(Zero, Zero) → Zero
new_esEs27(vuu301, vuu3101, app(ty_[], dg)) → new_esEs6(vuu301, vuu3101, dg)
new_span2Ys0(vuu37, vuu38, :(vuu410, vuu411), eb, ec) → new_span2Ys10(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, eb, ec), eb, ec)
new_asAs(True, vuu68) → vuu68
new_esEs26(vuu300, vuu3100, ty_Float) → new_esEs14(vuu300, vuu3100)
new_esEs21(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300100), Succ(vuu3100100)) → new_primPlusNat0(new_primMulNat0(vuu300100, Succ(vuu3100100)), vuu3100100)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Double, bd) → new_esEs18(vuu3000, vuu31000)
new_esEs15(Just(vuu3000), Nothing, cb) → False
new_esEs15(Nothing, Just(vuu31000), cb) → False
new_esEs27(vuu301, vuu3101, app(app(ty_Either, ce), cf)) → new_esEs9(vuu301, vuu3101, ce, cf)
new_esEs16(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), cc) → new_asAs(new_esEs19(vuu3000, vuu31000, cc), new_esEs20(vuu3001, vuu31001, cc))
new_esEs27(vuu301, vuu3101, ty_Int) → new_esEs10(vuu301, vuu3101)
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Bool, bd) → new_esEs17(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs21(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(app(app(ty_@3, gc), gd), ge)) → new_esEs11(vuu3001, vuu31001, gc, gd, ge)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(ty_Ratio, bgc)) → new_esEs16(vuu3001, vuu31001, bgc)
new_esEs20(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_esEs27(vuu301, vuu3101, ty_Float) → new_esEs14(vuu301, vuu3101)
new_esEs24(vuu3001, vuu31001, app(app(app(ty_@3, bfg), bfh), bga)) → new_esEs11(vuu3001, vuu31001, bfg, bfh, bga)
new_primEqNat0(Succ(vuu300000), Succ(vuu3100000)) → new_primEqNat0(vuu300000, vuu3100000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Integer, bd) → new_esEs8(vuu3000, vuu31000)
new_esEs5(GT, EQ) → False
new_esEs5(GT, LT) → False
new_esEs5(EQ, GT) → False
new_esEs5(LT, GT) → False
new_esEs27(vuu301, vuu3101, ty_@0) → new_esEs12(vuu301, vuu3101)
new_esEs26(vuu300, vuu3100, ty_@0) → new_esEs12(vuu300, vuu3100)
new_esEs21(vuu3000, vuu31000, app(app(ty_Either, ed), ee)) → new_esEs9(vuu3000, vuu31000, ed, ee)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs11(vuu3000, vuu31000, eh, fa, fb)
new_esEs10(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs7(vuu3000, vuu31000, app(ty_Ratio, baa)) → new_esEs16(vuu3000, vuu31000, baa)
new_esEs25(vuu3002, vuu31002, ty_Float) → new_esEs14(vuu3002, vuu31002)
new_span2Zs0(vuu57, vuu58, :(vuu610, vuu611), dh, ea) → new_span2Zs10(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, dh, ea), dh, ea)
new_esEs26(vuu300, vuu3100, app(app(ty_@2, be), bf)) → new_esEs4(vuu300, vuu3100, be, bf)
new_esEs24(vuu3001, vuu31001, app(app(ty_Either, bfc), bfd)) → new_esEs9(vuu3001, vuu31001, bfc, bfd)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs27(vuu301, vuu3101, ty_Ordering) → new_esEs5(vuu301, vuu3101)
new_esEs24(vuu3001, vuu31001, ty_@0) → new_esEs12(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs9(Right(vuu3000), Left(vuu31000), bc, bd) → False
new_esEs9(Left(vuu3000), Right(vuu31000), bc, bd) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs21(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Char) → new_esEs13(vuu3002, vuu31002)

The set Q consists of the following terms:

new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs5(GT, EQ)
new_esEs5(EQ, GT)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_groupByZs00(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Ordering)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs15(Just(x0), Just(x1), ty_Int)
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs7(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Char)
new_esEs15(Just(x0), Just(x1), ty_Ordering)
new_esEs25(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(x0, x1, ty_Integer)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs7(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_@0)
new_asAs(False, x0)
new_esEs24(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Nothing, Nothing, x0)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Zs11(x0, x1, x2, x3, x4, x5, x6, x7)
new_esEs22(x0, x1, ty_Int)
new_esEs15(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, ty_Int)
new_span2Ys11(x0, x1, x2, x3, x4, x5, x6, x7)
new_esEs15(Just(x0), Just(x1), ty_Char)
new_esEs8(Integer(x0), Integer(x1))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs25(x0, x1, ty_Int)
new_esEs7(x0, x1, ty_Double)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_span2Zs0(x0, x1, :(x2, x3), x4, x5)
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(EQ, LT)
new_esEs5(LT, EQ)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Char)
new_esEs17(False, False)
new_esEs27(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, ty_Double)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs6([], [], x0)
new_esEs21(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Ordering)
new_esEs15(Just(x0), Just(x1), ty_Double)
new_esEs15(Nothing, Just(x0), x1)
new_esEs26(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs18(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs15(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_span2Zs0(x0, x1, [], x2, x3)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_span2Zs10(x0, x1, x2, x3, False, x4, x5)
new_primEqNat0(Zero, Zero)
new_esEs5(LT, LT)
new_esEs15(Just(x0), Just(x1), ty_Bool)
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs7(x0, x1, ty_Int)
new_span2Ys0(x0, x1, :(x2, x3), x4, x5)
new_esEs22(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs22(x0, x1, ty_Char)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_[], x2))
new_span2Ys10(x0, x1, x2, x3, True, x4, x5)
new_esEs6(:(x0, x1), [], x2)
new_groupByZs0(@2(x0, x1), :(@2(x2, x3), x4), x5, x6)
new_esEs12(@0, @0)
new_esEs21(x0, x1, ty_Char)
new_primEqNat0(Zero, Succ(x0))
new_esEs5(GT, GT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_primMulNat0(Zero, Zero)
new_esEs15(Just(x0), Just(x1), ty_Integer)
new_esEs13(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Bool)
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_[], x2))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs27(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_@0)
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6([], :(x0, x1), x2)
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primPlusNat1(Zero, Succ(x0))
new_esEs15(Just(x0), Just(x1), app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Float)
new_asAs(True, x0)
new_esEs15(Just(x0), Just(x1), ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs10(x0, x1)
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs26(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(EQ, EQ)
new_esEs7(x0, x1, ty_Ordering)
new_esEs15(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs15(Just(x0), Nothing, x1)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Ordering)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_span2Zs10(x0, x1, x2, x3, True, x4, x5)
new_esEs27(x0, x1, ty_@0)
new_span2Ys10(x0, x1, x2, x3, False, x4, x5)
new_esEs24(x0, x1, ty_Double)
new_esEs5(GT, LT)
new_esEs5(LT, GT)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_@0)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_groupByZs00(x0, x1, x2, x3, x4, True, x5, x6)
new_esEs25(x0, x1, ty_Ordering)
new_primPlusNat0(Succ(x0), x1)
new_esEs7(x0, x1, ty_@0)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_span2Ys0(x0, x1, [], x2, x3)
new_esEs17(False, True)
new_esEs17(True, False)
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Float)
new_esEs7(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Int)
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs15(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs17(True, True)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs6(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs21(x0, x1, ty_Double)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs15(Just(x0), Just(x1), ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_groupByZs0(x0, [], x1, x2)
new_esEs7(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Float)
new_esEs15(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_groupBy(:(vuu30, vuu31), ba, bb) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba, bb), ba, bb)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x1, x2)) = 1 + x2   
POL(:%(x1, x2)) = 0   
POL(@0) = 0   
POL(@2(x1, x2)) = 0   
POL(@3(x1, x2, x3)) = 0   
POL(Char(x1)) = 0   
POL(Double(x1, x2)) = 0   
POL(EQ) = 0   
POL(False) = 0   
POL(Float(x1, x2)) = 0   
POL(GT) = 0   
POL(Integer(x1)) = 0   
POL(Just(x1)) = 0   
POL(LT) = 0   
POL(Left(x1)) = 0   
POL(Neg(x1)) = 0   
POL(Nothing) = 0   
POL(Pos(x1)) = 0   
POL(Right(x1)) = 0   
POL(Succ(x1)) = 1 + x1   
POL(True) = 0   
POL(Zero) = 0   
POL([]) = 0   
POL(app(x1, x2)) = x1   
POL(new_asAs(x1, x2)) = 0   
POL(new_esEs10(x1, x2)) = 0   
POL(new_esEs11(x1, x2, x3, x4, x5)) = 0   
POL(new_esEs12(x1, x2)) = 0   
POL(new_esEs13(x1, x2)) = x2   
POL(new_esEs14(x1, x2)) = 0   
POL(new_esEs15(x1, x2, x3)) = 0   
POL(new_esEs16(x1, x2, x3)) = 0   
POL(new_esEs17(x1, x2)) = 0   
POL(new_esEs18(x1, x2)) = 0   
POL(new_esEs19(x1, x2, x3)) = 0   
POL(new_esEs20(x1, x2, x3)) = 0   
POL(new_esEs21(x1, x2, x3)) = 0   
POL(new_esEs22(x1, x2, x3)) = 0   
POL(new_esEs23(x1, x2, x3)) = 0   
POL(new_esEs24(x1, x2, x3)) = 0   
POL(new_esEs25(x1, x2, x3)) = 0   
POL(new_esEs26(x1, x2, x3)) = x1 + x2 + x3   
POL(new_esEs27(x1, x2, x3)) = 0   
POL(new_esEs4(x1, x2, x3, x4)) = 0   
POL(new_esEs5(x1, x2)) = 0   
POL(new_esEs6(x1, x2, x3)) = 0   
POL(new_esEs7(x1, x2, x3)) = 0   
POL(new_esEs8(x1, x2)) = 0   
POL(new_esEs9(x1, x2, x3, x4)) = 0   
POL(new_groupBy(x1, x2, x3)) = x1   
POL(new_groupByZs0(x1, x2, x3, x4)) = x2   
POL(new_groupByZs00(x1, x2, x3, x4, x5, x6, x7, x8)) = 1 + x5   
POL(new_primEqInt(x1, x2)) = 0   
POL(new_primEqNat0(x1, x2)) = 0   
POL(new_primMulNat0(x1, x2)) = 0   
POL(new_primPlusNat0(x1, x2)) = 0   
POL(new_primPlusNat1(x1, x2)) = x1 + x2   
POL(new_span2Ys0(x1, x2, x3, x4, x5)) = x3   
POL(new_span2Ys10(x1, x2, x3, x4, x5, x6, x7)) = 1 + x4   
POL(new_span2Ys11(x1, x2, x3, x4, x5, x6, x7, x8)) = 1 + x5   
POL(new_span2Zs0(x1, x2, x3, x4, x5)) = x3   
POL(new_span2Zs10(x1, x2, x3, x4, x5, x6, x7)) = 1 + x4   
POL(new_span2Zs11(x1, x2, x3, x4, x5, x6, x7, x8)) = x6   
POL(new_sr(x1, x2)) = 0   
POL(ty_@0) = 1   
POL(ty_@2) = 0   
POL(ty_@3) = 1   
POL(ty_Bool) = 0   
POL(ty_Char) = 0   
POL(ty_Double) = 0   
POL(ty_Either) = 1   
POL(ty_Float) = 1   
POL(ty_Int) = 0   
POL(ty_Integer) = 1   
POL(ty_Maybe) = 1   
POL(ty_Ordering) = 0   
POL(ty_Ratio) = 0   
POL(ty_[]) = 0   

The following usable rules [17] were oriented:

new_span2Zs0(vuu57, vuu58, [], dh, ea) → []
new_span2Ys0(vuu37, vuu38, [], eb, ec) → []
new_groupByZs0(@2(vuu300, vuu301), :(@2(vuu3100, vuu3101), vuu311), ba, bb) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_asAs(new_esEs26(vuu300, vuu3100, ba), new_esEs27(vuu301, vuu3101, bb)), ba, bb)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, True, dh, ea) → new_span2Zs0(vuu57, vuu58, vuu61, dh, ea)
new_groupByZs0(vuu30, [], ba, bb) → []
new_span2Ys11(vuu37, vuu38, vuu410, vuu411, vuu72, vuu71, eb, ec) → :(vuu410, vuu72)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, False, dh, ea) → :(@2(vuu59, vuu60), vuu61)
new_span2Zs0(vuu57, vuu58, :(vuu610, vuu611), dh, ea) → new_span2Zs10(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, dh, ea), dh, ea)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, vuu74, vuu73, dh, ea) → vuu73
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, True, eb, ec) → new_span2Ys11(vuu37, vuu38, vuu410, vuu411, new_span2Ys0(vuu37, vuu38, vuu411, eb, ec), new_span2Zs0(vuu37, vuu38, vuu411, eb, ec), eb, ec)
new_span2Ys0(vuu37, vuu38, :(vuu410, vuu411), eb, ec) → new_span2Ys10(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, eb, ec), eb, ec)
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, True, dh, ea) → new_span2Zs11(vuu57, vuu58, vuu610, vuu611, new_span2Ys0(vuu57, vuu58, vuu611, dh, ea), new_span2Zs0(vuu57, vuu58, vuu611, dh, ea), dh, ea)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, False, eb, ec) → []
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, False, dh, ea) → :(vuu610, vuu611)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPOrderProof
                              ↳ QDP
                                ↳ PisEmptyProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(ty_Maybe, bdf)) → new_esEs15(vuu3000, vuu31000, bdf)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Double) → new_esEs18(vuu3001, vuu31001)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_primPlusNat1(Succ(vuu7500), Succ(vuu31001000)) → Succ(Succ(new_primPlusNat1(vuu7500, vuu31001000)))
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_esEs21(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Int) → new_esEs10(vuu3002, vuu31002)
new_esEs24(vuu3001, vuu31001, app(app(ty_@2, bfe), bff)) → new_esEs4(vuu3001, vuu31001, bfe, bff)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Char, bd) → new_esEs13(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Double) → new_esEs18(vuu300, vuu3100)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(ty_[], gh)) → new_esEs6(vuu3001, vuu31001, gh)
new_esEs7(vuu3000, vuu31000, app(app(app(ty_@3, he), hf), hg)) → new_esEs11(vuu3000, vuu31000, he, hf, hg)
new_esEs26(vuu300, vuu3100, app(ty_Ratio, cc)) → new_esEs16(vuu300, vuu3100, cc)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bec), bed)) → new_esEs4(vuu3000, vuu31000, bec, bed)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_[], bcf), bd) → new_esEs6(vuu3000, vuu31000, bcf)
new_esEs22(vuu3001, vuu31001, ty_Float) → new_esEs14(vuu3001, vuu31001)
new_esEs6(:(vuu3000, vuu3001), :(vuu31000, vuu31001), cd) → new_asAs(new_esEs7(vuu3000, vuu31000, cd), new_esEs6(vuu3001, vuu31001, cd))
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_esEs26(vuu300, vuu3100, ty_Int) → new_esEs10(vuu300, vuu3100)
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_esEs7(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs27(vuu301, vuu3101, ty_Bool) → new_esEs17(vuu301, vuu3101)
new_esEs27(vuu301, vuu3101, app(ty_Ratio, df)) → new_esEs16(vuu301, vuu3101, df)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(vuu301, vuu3101, app(app(app(ty_@3, db), dc), dd)) → new_esEs11(vuu301, vuu3101, db, dc, dd)
new_esEs24(vuu3001, vuu31001, ty_Char) → new_esEs13(vuu3001, vuu31001)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bcd), bd) → new_esEs15(vuu3000, vuu31000, bcd)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(app(ty_Either, bcg), bch)) → new_esEs9(vuu3000, vuu31000, bcg, bch)
new_esEs7(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(ty_Maybe, cb)) → new_esEs15(vuu300, vuu3100, cb)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(app(ty_@2, bgg), bgh)) → new_esEs4(vuu3002, vuu31002, bgg, bgh)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_primPlusNat0(Zero, vuu3100100) → Succ(vuu3100100)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bee), bef), beg)) → new_esEs11(vuu3000, vuu31000, bee, bef, beg)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(ty_[], bdh)) → new_esEs6(vuu3000, vuu31000, bdh)
new_esEs22(vuu3001, vuu31001, ty_Bool) → new_esEs17(vuu3001, vuu31001)
new_esEs19(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Bool) → new_esEs17(vuu3002, vuu31002)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, bca), bcb), bcc), bd) → new_esEs11(vuu3000, vuu31000, bca, bcb, bcc)
new_esEs25(vuu3002, vuu31002, app(ty_Ratio, bhe)) → new_esEs16(vuu3002, vuu31002, bhe)
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, False, eb, ec) → []
new_esEs24(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_sr(Neg(vuu30010), Pos(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_sr(Pos(vuu30010), Neg(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_esEs17(True, True) → True
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, True, dh, ea) → new_span2Zs0(vuu57, vuu58, vuu61, dh, ea)
new_esEs24(vuu3001, vuu31001, app(ty_Maybe, bgb)) → new_esEs15(vuu3001, vuu31001, bgb)
new_esEs7(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_@0, bd) → new_esEs12(vuu3000, vuu31000)
new_esEs20(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(app(app(ty_@3, bha), bhb), bhc)) → new_esEs11(vuu3002, vuu31002, bha, bhb, bhc)
new_esEs24(vuu3001, vuu31001, app(ty_[], bgd)) → new_esEs6(vuu3001, vuu31001, bgd)
new_esEs22(vuu3001, vuu31001, ty_Double) → new_esEs18(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, app(app(ty_@2, ef), eg)) → new_esEs4(vuu3000, vuu31000, ef, eg)
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bag), bah), bba)) → new_esEs11(vuu3000, vuu31000, bag, bah, bba)
new_esEs12(@0, @0) → True
new_esEs21(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Char) → new_esEs13(vuu300, vuu3100)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(app(ty_@2, bda), bdb)) → new_esEs4(vuu3000, vuu31000, bda, bdb)
new_esEs7(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, beh)) → new_esEs15(vuu3000, vuu31000, beh)
new_esEs26(vuu300, vuu3100, app(app(ty_Either, bc), bd)) → new_esEs9(vuu300, vuu3100, bc, bd)
new_primEqNat0(Zero, Succ(vuu3100000)) → False
new_primEqNat0(Succ(vuu300000), Zero) → False
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bea), beb)) → new_esEs9(vuu3000, vuu31000, bea, beb)
new_esEs22(vuu3001, vuu31001, app(app(ty_Either, fg), fh)) → new_esEs9(vuu3001, vuu31001, fg, fh)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_groupByZs0(vuu30, [], ba, bb) → []
new_groupByZs0(@2(vuu300, vuu301), :(@2(vuu3100, vuu3101), vuu311), ba, bb) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_asAs(new_esEs26(vuu300, vuu3100, ba), new_esEs27(vuu301, vuu3101, bb)), ba, bb)
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bbg), bbh), bd) → new_esEs4(vuu3000, vuu31000, bbg, bbh)
new_esEs18(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs10(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs15(Nothing, Nothing, cb) → True
new_esEs27(vuu301, vuu3101, app(ty_Maybe, de)) → new_esEs15(vuu301, vuu3101, de)
new_esEs24(vuu3001, vuu31001, ty_Float) → new_esEs14(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(app(ty_@2, ga), gb)) → new_esEs4(vuu3001, vuu31001, ga, gb)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(app(app(ty_@3, bg), bh), ca)) → new_esEs11(vuu300, vuu3100, bg, bh, ca)
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs7(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, False, dh, ea) → :(vuu610, vuu611)
new_span2Zs10(vuu57, vuu58, vuu610, vuu611, True, dh, ea) → new_span2Zs11(vuu57, vuu58, vuu610, vuu611, new_span2Ys0(vuu57, vuu58, vuu611, dh, ea), new_span2Zs0(vuu57, vuu58, vuu611, dh, ea), dh, ea)
new_esEs5(EQ, LT) → False
new_esEs5(LT, EQ) → False
new_esEs7(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs6([], :(vuu31000, vuu31001), cd) → False
new_esEs6(:(vuu3000, vuu3001), [], cd) → False
new_span2Ys11(vuu37, vuu38, vuu410, vuu411, vuu72, vuu71, eb, ec) → :(vuu410, vuu72)
new_esEs22(vuu3001, vuu31001, ty_@0) → new_esEs12(vuu3001, vuu31001)
new_esEs7(vuu3000, vuu31000, app(ty_[], bab)) → new_esEs6(vuu3000, vuu31000, bab)
new_groupByZs00(vuu57, vuu58, vuu59, vuu60, vuu61, False, dh, ea) → :(@2(vuu59, vuu60), vuu61)
new_esEs21(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs7(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bfa)) → new_esEs16(vuu3000, vuu31000, bfa)
new_esEs22(vuu3001, vuu31001, app(ty_Ratio, gg)) → new_esEs16(vuu3001, vuu31001, gg)
new_esEs25(vuu3002, vuu31002, ty_Ordering) → new_esEs5(vuu3002, vuu31002)
new_esEs25(vuu3002, vuu31002, ty_@0) → new_esEs12(vuu3002, vuu31002)
new_esEs27(vuu301, vuu3101, ty_Double) → new_esEs18(vuu301, vuu3101)
new_esEs26(vuu300, vuu3100, app(ty_[], cd)) → new_esEs6(vuu300, vuu3100, cd)
new_sr(Neg(vuu30010), Neg(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_[], bbd)) → new_esEs6(vuu3000, vuu31000, bbd)
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bbc)) → new_esEs16(vuu3000, vuu31000, bbc)
new_esEs19(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_span2Ys0(vuu37, vuu38, [], eb, ec) → []
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_sr(Pos(vuu30010), Pos(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_asAs(False, vuu68) → False
new_primEqNat0(Zero, Zero) → True
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Float, bd) → new_esEs14(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300100), Zero) → Zero
new_primMulNat0(Zero, Succ(vuu3100100)) → Zero
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(ty_Ratio, bdg)) → new_esEs16(vuu3000, vuu31000, bdg)
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bae), baf)) → new_esEs4(vuu3000, vuu31000, bae, baf)
new_esEs25(vuu3002, vuu31002, ty_Integer) → new_esEs8(vuu3002, vuu31002)
new_esEs27(vuu301, vuu3101, ty_Char) → new_esEs13(vuu301, vuu3101)
new_esEs17(False, False) → True
new_esEs21(vuu3000, vuu31000, app(ty_Maybe, fc)) → new_esEs15(vuu3000, vuu31000, fc)
new_esEs17(True, False) → False
new_esEs17(False, True) → False
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(ty_Either, bbe), bbf), bd) → new_esEs9(vuu3000, vuu31000, bbe, bbf)
new_esEs8(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs13(Char(vuu3000), Char(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Ordering) → new_esEs5(vuu300, vuu3100)
new_esEs11(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), bg, bh, ca) → new_asAs(new_esEs23(vuu3000, vuu31000, bg), new_asAs(new_esEs24(vuu3001, vuu31001, bh), new_esEs25(vuu3002, vuu31002, ca)))
new_esEs24(vuu3001, vuu31001, ty_Bool) → new_esEs17(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(ty_Maybe, bhd)) → new_esEs15(vuu3002, vuu31002, bhd)
new_esEs14(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs10(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_primPlusNat0(Succ(vuu750), vuu3100100) → Succ(Succ(new_primPlusNat1(vuu750, vuu3100100)))
new_esEs26(vuu300, vuu3100, ty_Integer) → new_esEs8(vuu300, vuu3100)
new_esEs7(vuu3000, vuu31000, app(app(ty_@2, hc), hd)) → new_esEs4(vuu3000, vuu31000, hc, hd)
new_esEs5(EQ, EQ) → True
new_esEs7(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs27(vuu301, vuu3101, ty_Integer) → new_esEs8(vuu301, vuu3101)
new_esEs22(vuu3001, vuu31001, ty_Ordering) → new_esEs5(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, app(ty_Ratio, fd)) → new_esEs16(vuu3000, vuu31000, fd)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_Ratio, bce), bd) → new_esEs16(vuu3000, vuu31000, bce)
new_span2Zs0(vuu57, vuu58, [], dh, ea) → []
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Int, bd) → new_esEs10(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(ty_[], bhf)) → new_esEs6(vuu3002, vuu31002, bhf)
new_esEs4(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), be, bf) → new_asAs(new_esEs21(vuu3000, vuu31000, be), new_esEs22(vuu3001, vuu31001, bf))
new_esEs23(vuu3000, vuu31000, app(ty_[], bfb)) → new_esEs6(vuu3000, vuu31000, bfb)
new_esEs27(vuu301, vuu3101, app(app(ty_@2, cg), da)) → new_esEs4(vuu301, vuu3101, cg, da)
new_esEs6([], [], cd) → True
new_esEs7(vuu3000, vuu31000, app(ty_Maybe, hh)) → new_esEs15(vuu3000, vuu31000, hh)
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_Maybe, bbb)) → new_esEs15(vuu3000, vuu31000, bbb)
new_primPlusNat1(Succ(vuu7500), Zero) → Succ(vuu7500)
new_primPlusNat1(Zero, Succ(vuu31001000)) → Succ(vuu31001000)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, ty_Char) → new_esEs13(vuu3001, vuu31001)
new_esEs26(vuu300, vuu3100, ty_Bool) → new_esEs17(vuu300, vuu3100)
new_esEs22(vuu3001, vuu31001, app(ty_Maybe, gf)) → new_esEs15(vuu3001, vuu31001, gf)
new_esEs25(vuu3002, vuu31002, app(app(ty_Either, bge), bgf)) → new_esEs9(vuu3002, vuu31002, bge, bgf)
new_esEs25(vuu3002, vuu31002, ty_Double) → new_esEs18(vuu3002, vuu31002)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bac), bad)) → new_esEs9(vuu3000, vuu31000, bac, bad)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs11(vuu3000, vuu31000, bdc, bdd, bde)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Ordering, bd) → new_esEs5(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Ordering) → new_esEs5(vuu3001, vuu31001)
new_esEs5(GT, GT) → True
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_esEs21(vuu3000, vuu31000, app(ty_[], ff)) → new_esEs6(vuu3000, vuu31000, ff)
new_esEs22(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_span2Zs11(vuu57, vuu58, vuu610, vuu611, vuu74, vuu73, dh, ea) → vuu73
new_span2Ys10(vuu37, vuu38, vuu410, vuu411, True, eb, ec) → new_span2Ys11(vuu37, vuu38, vuu410, vuu411, new_span2Ys0(vuu37, vuu38, vuu411, eb, ec), new_span2Zs0(vuu37, vuu38, vuu411, eb, ec), eb, ec)
new_esEs7(vuu3000, vuu31000, app(app(ty_Either, ha), hb)) → new_esEs9(vuu3000, vuu31000, ha, hb)
new_esEs5(LT, LT) → True
new_primPlusNat1(Zero, Zero) → Zero
new_esEs27(vuu301, vuu3101, app(ty_[], dg)) → new_esEs6(vuu301, vuu3101, dg)
new_span2Ys0(vuu37, vuu38, :(vuu410, vuu411), eb, ec) → new_span2Ys10(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, eb, ec), eb, ec)
new_asAs(True, vuu68) → vuu68
new_esEs26(vuu300, vuu3100, ty_Float) → new_esEs14(vuu300, vuu3100)
new_esEs21(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300100), Succ(vuu3100100)) → new_primPlusNat0(new_primMulNat0(vuu300100, Succ(vuu3100100)), vuu3100100)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Double, bd) → new_esEs18(vuu3000, vuu31000)
new_esEs15(Just(vuu3000), Nothing, cb) → False
new_esEs15(Nothing, Just(vuu31000), cb) → False
new_esEs27(vuu301, vuu3101, app(app(ty_Either, ce), cf)) → new_esEs9(vuu301, vuu3101, ce, cf)
new_esEs16(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), cc) → new_asAs(new_esEs19(vuu3000, vuu31000, cc), new_esEs20(vuu3001, vuu31001, cc))
new_esEs27(vuu301, vuu3101, ty_Int) → new_esEs10(vuu301, vuu3101)
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Bool, bd) → new_esEs17(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs21(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(app(app(ty_@3, gc), gd), ge)) → new_esEs11(vuu3001, vuu31001, gc, gd, ge)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(ty_Ratio, bgc)) → new_esEs16(vuu3001, vuu31001, bgc)
new_esEs20(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_esEs27(vuu301, vuu3101, ty_Float) → new_esEs14(vuu301, vuu3101)
new_esEs24(vuu3001, vuu31001, app(app(app(ty_@3, bfg), bfh), bga)) → new_esEs11(vuu3001, vuu31001, bfg, bfh, bga)
new_primEqNat0(Succ(vuu300000), Succ(vuu3100000)) → new_primEqNat0(vuu300000, vuu3100000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Integer, bd) → new_esEs8(vuu3000, vuu31000)
new_esEs5(GT, EQ) → False
new_esEs5(GT, LT) → False
new_esEs5(EQ, GT) → False
new_esEs5(LT, GT) → False
new_esEs27(vuu301, vuu3101, ty_@0) → new_esEs12(vuu301, vuu3101)
new_esEs26(vuu300, vuu3100, ty_@0) → new_esEs12(vuu300, vuu3100)
new_esEs21(vuu3000, vuu31000, app(app(ty_Either, ed), ee)) → new_esEs9(vuu3000, vuu31000, ed, ee)
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs11(vuu3000, vuu31000, eh, fa, fb)
new_esEs10(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs7(vuu3000, vuu31000, app(ty_Ratio, baa)) → new_esEs16(vuu3000, vuu31000, baa)
new_esEs25(vuu3002, vuu31002, ty_Float) → new_esEs14(vuu3002, vuu31002)
new_span2Zs0(vuu57, vuu58, :(vuu610, vuu611), dh, ea) → new_span2Zs10(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, dh, ea), dh, ea)
new_esEs26(vuu300, vuu3100, app(app(ty_@2, be), bf)) → new_esEs4(vuu300, vuu3100, be, bf)
new_esEs24(vuu3001, vuu31001, app(app(ty_Either, bfc), bfd)) → new_esEs9(vuu3001, vuu31001, bfc, bfd)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_esEs9(Right(vuu3000), Right(vuu31000), bc, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs27(vuu301, vuu3101, ty_Ordering) → new_esEs5(vuu301, vuu3101)
new_esEs24(vuu3001, vuu31001, ty_@0) → new_esEs12(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs9(Right(vuu3000), Left(vuu31000), bc, bd) → False
new_esEs9(Left(vuu3000), Right(vuu31000), bc, bd) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs21(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Char) → new_esEs13(vuu3002, vuu31002)

The set Q consists of the following terms:

new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs5(GT, EQ)
new_esEs5(EQ, GT)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_groupByZs00(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Ordering)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs15(Just(x0), Just(x1), ty_Int)
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs7(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Char)
new_esEs15(Just(x0), Just(x1), ty_Ordering)
new_esEs25(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(x0, x1, ty_Integer)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Float)
new_esEs7(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_@0)
new_asAs(False, x0)
new_esEs24(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(Nothing, Nothing, x0)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Zs11(x0, x1, x2, x3, x4, x5, x6, x7)
new_esEs22(x0, x1, ty_Int)
new_esEs15(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, ty_Int)
new_span2Ys11(x0, x1, x2, x3, x4, x5, x6, x7)
new_esEs15(Just(x0), Just(x1), ty_Char)
new_esEs8(Integer(x0), Integer(x1))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs25(x0, x1, ty_Int)
new_esEs7(x0, x1, ty_Double)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_span2Zs0(x0, x1, :(x2, x3), x4, x5)
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(EQ, LT)
new_esEs5(LT, EQ)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Char)
new_esEs17(False, False)
new_esEs27(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, ty_Double)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs6([], [], x0)
new_esEs21(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Ordering)
new_esEs15(Just(x0), Just(x1), ty_Double)
new_esEs15(Nothing, Just(x0), x1)
new_esEs26(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs18(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs15(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_span2Zs0(x0, x1, [], x2, x3)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_span2Zs10(x0, x1, x2, x3, False, x4, x5)
new_primEqNat0(Zero, Zero)
new_esEs5(LT, LT)
new_esEs15(Just(x0), Just(x1), ty_Bool)
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs7(x0, x1, ty_Int)
new_span2Ys0(x0, x1, :(x2, x3), x4, x5)
new_esEs22(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs22(x0, x1, ty_Char)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_[], x2))
new_span2Ys10(x0, x1, x2, x3, True, x4, x5)
new_esEs6(:(x0, x1), [], x2)
new_groupByZs0(@2(x0, x1), :(@2(x2, x3), x4), x5, x6)
new_esEs12(@0, @0)
new_esEs21(x0, x1, ty_Char)
new_primEqNat0(Zero, Succ(x0))
new_esEs5(GT, GT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_primMulNat0(Zero, Zero)
new_esEs15(Just(x0), Just(x1), ty_Integer)
new_esEs13(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Bool)
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_[], x2))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs27(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_@0)
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6([], :(x0, x1), x2)
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primPlusNat1(Zero, Succ(x0))
new_esEs15(Just(x0), Just(x1), app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Float)
new_asAs(True, x0)
new_esEs15(Just(x0), Just(x1), ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs10(x0, x1)
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs26(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(EQ, EQ)
new_esEs7(x0, x1, ty_Ordering)
new_esEs15(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs15(Just(x0), Nothing, x1)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Ordering)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_span2Zs10(x0, x1, x2, x3, True, x4, x5)
new_esEs27(x0, x1, ty_@0)
new_span2Ys10(x0, x1, x2, x3, False, x4, x5)
new_esEs24(x0, x1, ty_Double)
new_esEs5(GT, LT)
new_esEs5(LT, GT)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_@0)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_groupByZs00(x0, x1, x2, x3, x4, True, x5, x6)
new_esEs25(x0, x1, ty_Ordering)
new_primPlusNat0(Succ(x0), x1)
new_esEs7(x0, x1, ty_@0)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_span2Ys0(x0, x1, [], x2, x3)
new_esEs17(False, True)
new_esEs17(True, False)
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Float)
new_esEs7(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Int)
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs15(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs17(True, True)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs6(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs21(x0, x1, ty_Double)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs15(Just(x0), Just(x1), ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_groupByZs0(x0, [], x1, x2)
new_esEs7(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Float)
new_esEs15(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP

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

new_primEqNat(Succ(vuu300000), Succ(vuu3100000)) → new_primEqNat(vuu300000, vuu3100000)

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: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP

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

new_span2Ys1(vuu37, vuu38, vuu410, vuu411, True, ba, bb) → new_span2Zs(vuu37, vuu38, vuu411, ba, bb)
new_span2Zs1(vuu57, vuu58, vuu610, vuu611, True, bc, bd) → new_span2Ys(vuu57, vuu58, vuu611, bc, bd)
new_span2Zs(vuu57, vuu58, :(vuu610, vuu611), bc, bd) → new_span2Zs1(vuu57, vuu58, vuu610, vuu611, new_esEs4(@2(vuu57, vuu58), vuu610, bc, bd), bc, bd)
new_span2Ys1(vuu37, vuu38, vuu410, vuu411, True, ba, bb) → new_span2Ys(vuu37, vuu38, vuu411, ba, bb)
new_span2Ys(vuu37, vuu38, :(vuu410, vuu411), ba, bb) → new_span2Ys1(vuu37, vuu38, vuu410, vuu411, new_esEs4(@2(vuu37, vuu38), vuu410, ba, bb), ba, bb)
new_span2Zs1(vuu57, vuu58, vuu610, vuu611, True, bc, bd) → new_span2Zs(vuu57, vuu58, vuu611, bc, bd)

The TRS R consists of the following rules:

new_esEs9(Right(vuu3000), Right(vuu31000), fh, app(ty_Maybe, gh)) → new_esEs15(vuu3000, vuu31000, gh)
new_esEs24(vuu3001, vuu31001, ty_Double) → new_esEs18(vuu3001, vuu31001)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_primPlusNat1(Succ(vuu7500), Succ(vuu31001000)) → Succ(Succ(new_primPlusNat1(vuu7500, vuu31001000)))
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_esEs25(vuu3002, vuu31002, ty_Int) → new_esEs10(vuu3002, vuu31002)
new_esEs21(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(ty_@2, bea), beb)) → new_esEs4(vuu3001, vuu31001, bea, beb)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Char, ed) → new_esEs13(vuu3000, vuu31000)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(ty_[], bca)) → new_esEs6(vuu3001, vuu31001, bca)
new_esEs7(vuu3000, vuu31000, app(app(app(ty_@3, cb), cc), cd)) → new_esEs11(vuu3000, vuu31000, cb, cc, cd)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bcg), bch)) → new_esEs4(vuu3000, vuu31000, bcg, bch)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_[], fg), ed) → new_esEs6(vuu3000, vuu31000, fg)
new_esEs22(vuu3001, vuu31001, ty_Float) → new_esEs14(vuu3001, vuu31001)
new_esEs6(:(vuu3000, vuu3001), :(vuu31000, vuu31001), be) → new_asAs(new_esEs7(vuu3000, vuu31000, be), new_esEs6(vuu3001, vuu31001, be))
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_esEs7(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs12(vuu3000, vuu31000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs24(vuu3001, vuu31001, ty_Char) → new_esEs13(vuu3001, vuu31001)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_Maybe, fd), ed) → new_esEs15(vuu3000, vuu31000, fd)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, app(app(ty_Either, ga), gb)) → new_esEs9(vuu3000, vuu31000, ga, gb)
new_esEs7(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(app(ty_@2, bfc), bfd)) → new_esEs4(vuu3002, vuu31002, bfc, bfd)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_primPlusNat0(Zero, vuu3100100) → Succ(vuu3100100)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bda), bdb), bdc)) → new_esEs11(vuu3000, vuu31000, bda, bdb, bdc)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, app(ty_[], hb)) → new_esEs6(vuu3000, vuu31000, hb)
new_esEs22(vuu3001, vuu31001, ty_Bool) → new_esEs17(vuu3001, vuu31001)
new_esEs19(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Bool) → new_esEs17(vuu3002, vuu31002)
new_esEs25(vuu3002, vuu31002, app(ty_Ratio, bga)) → new_esEs16(vuu3002, vuu31002, bga)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, fa), fb), fc), ed) → new_esEs11(vuu3000, vuu31000, fa, fb, fc)
new_esEs24(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_sr(Neg(vuu30010), Pos(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_sr(Pos(vuu30010), Neg(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_esEs17(True, True) → True
new_esEs24(vuu3001, vuu31001, app(ty_Maybe, bef)) → new_esEs15(vuu3001, vuu31001, bef)
new_esEs7(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_@0, ed) → new_esEs12(vuu3000, vuu31000)
new_esEs20(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(app(app(ty_@3, bfe), bff), bfg)) → new_esEs11(vuu3002, vuu31002, bfe, bff, bfg)
new_esEs24(vuu3001, vuu31001, app(ty_[], beh)) → new_esEs6(vuu3001, vuu31001, beh)
new_esEs22(vuu3001, vuu31001, ty_Double) → new_esEs18(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, app(app(ty_@2, hh), baa)) → new_esEs4(vuu3000, vuu31000, hh, baa)
new_esEs12(@0, @0) → True
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, df), dg), dh)) → new_esEs11(vuu3000, vuu31000, df, dg, dh)
new_esEs21(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, bdd)) → new_esEs15(vuu3000, vuu31000, bdd)
new_esEs22(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_esEs7(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, app(app(ty_@2, gc), gd)) → new_esEs4(vuu3000, vuu31000, gc, gd)
new_primEqNat0(Zero, Succ(vuu3100000)) → False
new_primEqNat0(Succ(vuu300000), Zero) → False
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bce), bcf)) → new_esEs9(vuu3000, vuu31000, bce, bcf)
new_esEs22(vuu3001, vuu31001, app(app(ty_Either, bah), bba)) → new_esEs9(vuu3001, vuu31001, bah, bba)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs18(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs10(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(ty_@2, eg), eh), ed) → new_esEs4(vuu3000, vuu31000, eg, eh)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs15(Nothing, Nothing, da) → True
new_esEs24(vuu3001, vuu31001, ty_Float) → new_esEs14(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(app(ty_@2, bbb), bbc)) → new_esEs4(vuu3001, vuu31001, bbb, bbc)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs7(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs5(LT, EQ) → False
new_esEs5(EQ, LT) → False
new_esEs7(vuu3000, vuu31000, ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs6([], :(vuu31000, vuu31001), be) → False
new_esEs6(:(vuu3000, vuu3001), [], be) → False
new_esEs22(vuu3001, vuu31001, ty_@0) → new_esEs12(vuu3001, vuu31001)
new_esEs7(vuu3000, vuu31000, app(ty_[], cg)) → new_esEs6(vuu3000, vuu31000, cg)
new_esEs21(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_esEs7(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bde)) → new_esEs16(vuu3000, vuu31000, bde)
new_esEs22(vuu3001, vuu31001, app(ty_Ratio, bbh)) → new_esEs16(vuu3001, vuu31001, bbh)
new_esEs25(vuu3002, vuu31002, ty_Ordering) → new_esEs5(vuu3002, vuu31002)
new_esEs25(vuu3002, vuu31002, ty_@0) → new_esEs12(vuu3002, vuu31002)
new_sr(Neg(vuu30010), Neg(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_Ratio, eb)) → new_esEs16(vuu3000, vuu31000, eb)
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_[], ec)) → new_esEs6(vuu3000, vuu31000, ec)
new_esEs24(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_esEs19(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_sr(Pos(vuu30010), Pos(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_asAs(False, vuu68) → False
new_primEqNat0(Zero, Zero) → True
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Float, ed) → new_esEs14(vuu3000, vuu31000)
new_primMulNat0(Zero, Succ(vuu3100100)) → Zero
new_primMulNat0(Succ(vuu300100), Zero) → Zero
new_esEs9(Right(vuu3000), Right(vuu31000), fh, app(ty_Ratio, ha)) → new_esEs16(vuu3000, vuu31000, ha)
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(ty_@2, dd), de)) → new_esEs4(vuu3000, vuu31000, dd, de)
new_esEs25(vuu3002, vuu31002, ty_Integer) → new_esEs8(vuu3002, vuu31002)
new_esEs21(vuu3000, vuu31000, app(ty_Maybe, bae)) → new_esEs15(vuu3000, vuu31000, bae)
new_esEs17(False, False) → True
new_esEs17(False, True) → False
new_esEs17(True, False) → False
new_esEs9(Left(vuu3000), Left(vuu31000), app(app(ty_Either, ee), ef), ed) → new_esEs9(vuu3000, vuu31000, ee, ef)
new_esEs8(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs13(Char(vuu3000), Char(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs11(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), bcb, bcc, bcd) → new_asAs(new_esEs23(vuu3000, vuu31000, bcb), new_asAs(new_esEs24(vuu3001, vuu31001, bcc), new_esEs25(vuu3002, vuu31002, bcd)))
new_esEs24(vuu3001, vuu31001, ty_Bool) → new_esEs17(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(ty_Maybe, bfh)) → new_esEs15(vuu3002, vuu31002, bfh)
new_esEs14(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs10(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_primPlusNat0(Succ(vuu750), vuu3100100) → Succ(Succ(new_primPlusNat1(vuu750, vuu3100100)))
new_esEs7(vuu3000, vuu31000, app(app(ty_@2, bh), ca)) → new_esEs4(vuu3000, vuu31000, bh, ca)
new_esEs5(EQ, EQ) → True
new_esEs7(vuu3000, vuu31000, ty_Ordering) → new_esEs5(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, ty_Ordering) → new_esEs5(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, app(ty_Ratio, baf)) → new_esEs16(vuu3000, vuu31000, baf)
new_esEs9(Left(vuu3000), Left(vuu31000), app(ty_Ratio, ff), ed) → new_esEs16(vuu3000, vuu31000, ff)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs25(vuu3002, vuu31002, app(ty_[], bgb)) → new_esEs6(vuu3002, vuu31002, bgb)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Int, ed) → new_esEs10(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bdf)) → new_esEs6(vuu3000, vuu31000, bdf)
new_esEs4(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), hd, he) → new_asAs(new_esEs21(vuu3000, vuu31000, hd), new_esEs22(vuu3001, vuu31001, he))
new_esEs6([], [], be) → True
new_esEs7(vuu3000, vuu31000, app(ty_Maybe, ce)) → new_esEs15(vuu3000, vuu31000, ce)
new_esEs15(Just(vuu3000), Just(vuu31000), app(ty_Maybe, ea)) → new_esEs15(vuu3000, vuu31000, ea)
new_primPlusNat1(Zero, Succ(vuu31001000)) → Succ(vuu31001000)
new_primPlusNat1(Succ(vuu7500), Zero) → Succ(vuu7500)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_Bool) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, ty_Char) → new_esEs13(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, ty_Double) → new_esEs18(vuu3002, vuu31002)
new_esEs25(vuu3002, vuu31002, app(app(ty_Either, bfa), bfb)) → new_esEs9(vuu3002, vuu31002, bfa, bfb)
new_esEs22(vuu3001, vuu31001, app(ty_Maybe, bbg)) → new_esEs15(vuu3001, vuu31001, bbg)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs15(Just(vuu3000), Just(vuu31000), app(app(ty_Either, db), dc)) → new_esEs9(vuu3000, vuu31000, db, dc)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs14(vuu3000, vuu31000)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, app(app(app(ty_@3, ge), gf), gg)) → new_esEs11(vuu3000, vuu31000, ge, gf, gg)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Ordering, ed) → new_esEs5(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Ordering) → new_esEs5(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Integer) → new_esEs8(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, app(ty_[], bag)) → new_esEs6(vuu3000, vuu31000, bag)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_esEs5(GT, GT) → True
new_esEs7(vuu3000, vuu31000, app(app(ty_Either, bf), bg)) → new_esEs9(vuu3000, vuu31000, bf, bg)
new_esEs5(LT, LT) → True
new_primPlusNat1(Zero, Zero) → Zero
new_asAs(True, vuu68) → vuu68
new_primMulNat0(Succ(vuu300100), Succ(vuu3100100)) → new_primPlusNat0(new_primMulNat0(vuu300100, Succ(vuu3100100)), vuu3100100)
new_esEs21(vuu3000, vuu31000, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs15(Nothing, Just(vuu31000), da) → False
new_esEs15(Just(vuu3000), Nothing, da) → False
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Double, ed) → new_esEs18(vuu3000, vuu31000)
new_esEs16(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), hc) → new_asAs(new_esEs19(vuu3000, vuu31000, hc), new_esEs20(vuu3001, vuu31001, hc))
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Bool, ed) → new_esEs17(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs21(vuu3000, vuu31000, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs22(vuu3001, vuu31001, app(app(app(ty_@3, bbd), bbe), bbf)) → new_esEs11(vuu3001, vuu31001, bbd, bbe, bbf)
new_esEs15(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs18(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(ty_Ratio, beg)) → new_esEs16(vuu3001, vuu31001, beg)
new_esEs20(vuu3001, vuu31001, ty_Int) → new_esEs10(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, app(app(app(ty_@3, bec), bed), bee)) → new_esEs11(vuu3001, vuu31001, bec, bed, bee)
new_primEqNat0(Succ(vuu300000), Succ(vuu3100000)) → new_primEqNat0(vuu300000, vuu3100000)
new_esEs5(LT, GT) → False
new_esEs5(EQ, GT) → False
new_esEs5(GT, LT) → False
new_esEs5(GT, EQ) → False
new_esEs9(Left(vuu3000), Left(vuu31000), ty_Integer, ed) → new_esEs8(vuu3000, vuu31000)
new_esEs21(vuu3000, vuu31000, app(app(ty_Either, hf), hg)) → new_esEs9(vuu3000, vuu31000, hf, hg)
new_esEs21(vuu3000, vuu31000, app(app(app(ty_@3, bab), bac), bad)) → new_esEs11(vuu3000, vuu31000, bab, bac, bad)
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_Int) → new_esEs10(vuu3000, vuu31000)
new_esEs10(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs7(vuu3000, vuu31000, app(ty_Ratio, cf)) → new_esEs16(vuu3000, vuu31000, cf)
new_esEs25(vuu3002, vuu31002, ty_Float) → new_esEs14(vuu3002, vuu31002)
new_esEs24(vuu3001, vuu31001, app(app(ty_Either, bdg), bdh)) → new_esEs9(vuu3001, vuu31001, bdg, bdh)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_esEs9(Right(vuu3000), Right(vuu31000), fh, ty_Integer) → new_esEs8(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_@0) → new_esEs12(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs13(vuu3000, vuu31000)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs9(Left(vuu3000), Right(vuu31000), fh, ed) → False
new_esEs9(Right(vuu3000), Left(vuu31000), fh, ed) → False
new_esEs21(vuu3000, vuu31000, ty_@0) → new_esEs12(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Char) → new_esEs13(vuu3002, vuu31002)

The set Q consists of the following terms:

new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs5(GT, EQ)
new_esEs5(EQ, GT)
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs15(Just(x0), Just(x1), ty_Int)
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs7(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs25(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_@0)
new_esEs15(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Integer)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Float)
new_esEs15(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs7(x0, x1, ty_Bool)
new_asAs(False, x0)
new_esEs22(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6([], [], x0)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs6(:(x0, x1), [], x2)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs15(Just(x0), Just(x1), ty_Char)
new_esEs8(Integer(x0), Integer(x1))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs7(x0, x1, ty_Double)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs6(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs25(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs15(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_esEs5(LT, EQ)
new_esEs5(EQ, LT)
new_esEs24(x0, x1, ty_Char)
new_esEs17(False, False)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs21(x0, x1, ty_Int)
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs15(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs15(Just(x0), Just(x1), ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs15(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs18(Double(x0, x1), Double(x2, x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_primEqNat0(Zero, Zero)
new_esEs5(LT, LT)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs15(Just(x0), Just(x1), ty_Bool)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs7(x0, x1, ty_Int)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs15(Nothing, Nothing, x0)
new_esEs12(@0, @0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Char)
new_primEqNat0(Zero, Succ(x0))
new_esEs5(GT, GT)
new_primMulNat0(Zero, Zero)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_esEs15(Just(x0), Just(x1), ty_Integer)
new_esEs13(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_Integer)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Bool)
new_esEs15(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs6([], :(x0, x1), x2)
new_primMulNat0(Zero, Succ(x0))
new_primEqNat0(Succ(x0), Zero)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_asAs(True, x0)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(Just(x0), Just(x1), ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs10(x0, x1)
new_esEs23(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs5(EQ, EQ)
new_esEs7(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Double)
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs5(GT, LT)
new_esEs5(LT, GT)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Ordering)
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs7(x0, x1, ty_@0)
new_esEs17(True, False)
new_esEs17(False, True)
new_primPlusNat1(Zero, Zero)
new_esEs14(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Float)
new_esEs7(x0, x1, ty_Float)
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs24(x0, x1, ty_Int)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs17(True, True)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs15(Nothing, Just(x0), x1)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs15(Just(x0), Just(x1), ty_Float)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs15(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))

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: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ NumRed
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof

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

new_esEs2(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs1(vuu3000, vuu31000, bce, bcf, bcg)
new_esEs3(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_Either, bdb), bdc)) → new_esEs(vuu3000, vuu31000, bdb, bdc)
new_esEs3(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_@2, bdd), bde)) → new_esEs0(vuu3000, vuu31000, bdd, bde)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, app(app(app(ty_@3, bac), bad), bae), gf) → new_esEs1(vuu3001, vuu31001, bac, bad, bae)
new_esEs3(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_[], beb)) → new_esEs3(vuu3000, vuu31000, beb)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, ge, app(ty_[], bbh)) → new_esEs3(vuu3002, vuu31002, bbh)
new_esEs2(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bca), bcb)) → new_esEs(vuu3000, vuu31000, bca, bcb)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), eh, app(app(app(ty_@3, ff), fg), fh)) → new_esEs1(vuu3001, vuu31001, ff, fg, fh)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, ge, app(app(app(ty_@3, bbd), bbe), bbf)) → new_esEs1(vuu3002, vuu31002, bbd, bbe, bbf)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(ty_@2, cf), cg)) → new_esEs0(vuu3000, vuu31000, cf, cg)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, ge, app(app(ty_@2, bbb), bbc)) → new_esEs0(vuu3002, vuu31002, bbb, bbc)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), eh, app(ty_[], gb)) → new_esEs3(vuu3001, vuu31001, gb)
new_esEs2(Just(vuu3000), Just(vuu31000), app(ty_Maybe, bch)) → new_esEs2(vuu3000, vuu31000, bch)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_[], eg), dh) → new_esEs3(vuu3000, vuu31000, eg)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_Either, df), dg), dh) → new_esEs(vuu3000, vuu31000, df, dg)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_@2, gg), gh), ge, gf) → new_esEs0(vuu3000, vuu31000, gg, gh)
new_esEs(Left(vuu3000), Left(vuu31000), app(ty_Maybe, ca), bc) → new_esEs2(vuu3000, vuu31000, ca)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), eh, app(app(ty_Either, fa), fb)) → new_esEs(vuu3001, vuu31001, fa, fb)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_[], he), ge, gf) → new_esEs3(vuu3000, vuu31000, he)
new_esEs3(:(vuu3000, vuu3001), :(vuu31000, vuu31001), bec) → new_esEs3(vuu3001, vuu31001, bec)
new_esEs(Left(vuu3000), Left(vuu31000), app(ty_[], cb), bc) → new_esEs3(vuu3000, vuu31000, cb)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, app(ty_[], bag), gf) → new_esEs3(vuu3001, vuu31001, bag)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(app(ty_@3, ha), hb), hc), ge, gf) → new_esEs1(vuu3000, vuu31000, ha, hb, hc)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(app(ty_@3, da), db), dc)) → new_esEs1(vuu3000, vuu31000, da, db, dc)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), eh, app(ty_Maybe, ga)) → new_esEs2(vuu3001, vuu31001, ga)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(ty_Either, cd), ce)) → new_esEs(vuu3000, vuu31000, cd, ce)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(ty_[], de)) → new_esEs3(vuu3000, vuu31000, de)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, app(ty_Maybe, baf), gf) → new_esEs2(vuu3001, vuu31001, baf)
new_esEs(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bd), be), bc) → new_esEs0(vuu3000, vuu31000, bd, be)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_Maybe, ef), dh) → new_esEs2(vuu3000, vuu31000, ef)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, ge, app(app(ty_Either, bah), bba)) → new_esEs(vuu3002, vuu31002, bah, bba)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, ge, app(ty_Maybe, bbg)) → new_esEs2(vuu3002, vuu31002, bbg)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, app(app(ty_Either, hg), hh), gf) → new_esEs(vuu3001, vuu31001, hg, hh)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_Either, gc), gd), ge, gf) → new_esEs(vuu3000, vuu31000, gc, gd)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(ty_Maybe, dd)) → new_esEs2(vuu3000, vuu31000, dd)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_@2, ea), eb), dh) → new_esEs0(vuu3000, vuu31000, ea, eb)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_Maybe, hd), ge, gf) → new_esEs2(vuu3000, vuu31000, hd)
new_esEs(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, bf), bg), bh), bc) → new_esEs1(vuu3000, vuu31000, bf, bg, bh)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(app(ty_@3, ec), ed), ee), dh) → new_esEs1(vuu3000, vuu31000, ec, ed, ee)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), hf, app(app(ty_@2, baa), bab), gf) → new_esEs0(vuu3001, vuu31001, baa, bab)
new_esEs0(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), eh, app(app(ty_@2, fc), fd)) → new_esEs0(vuu3001, vuu31001, fc, fd)
new_esEs3(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_Maybe, bea)) → new_esEs2(vuu3000, vuu31000, bea)
new_esEs3(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(vuu3000, vuu31000, bdf, bdg, bdh)
new_esEs(Left(vuu3000), Left(vuu31000), app(app(ty_Either, ba), bb), bc) → new_esEs(vuu3000, vuu31000, ba, bb)
new_esEs2(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bcc), bcd)) → new_esEs0(vuu3000, vuu31000, bcc, bcd)
new_esEs2(Just(vuu3000), Just(vuu31000), app(ty_[], bda)) → new_esEs3(vuu3000, vuu31000, bda)

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: