YES
H-Termination proof of ../tpdb/FP/full_haskell/List_elemIndex_12.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule Main
|
| ((List.elemIndex :: (Eq b, Eq a) => (a,b) -> [(a,b)] -> Maybe Int) :: (Eq b, Eq a) => (a,b) -> [(a,b)] -> Maybe Int) |
module List where
| | import qualified Main
import qualified Maybe
import qualified Prelude
|
| | elemIndex :: Eq a => a -> [a] -> Maybe Int
| elemIndex | x | = | findIndex (== x) |
|
| | findIndex :: (a -> Bool) -> [a] -> Maybe Int
| findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| | findIndices :: (a -> Bool) -> [a] -> [Int]
| findIndices | p xs | = | concatMap (\vv1 ->
| case | vv1 of |
|
| (x,i) | -> | if p x then i : [] else [] |
|
| _ | -> | [] |
) (zip xs (enumFrom 0)) |
|
module Main where
| | import qualified List
import qualified Maybe
import qualified Prelude
|
module Maybe where
| | import qualified List
import qualified Main
import qualified Prelude
|
| | listToMaybe :: [a] -> Maybe a
| listToMaybe | [] | = | Nothing |
| listToMaybe | (a : _) | = | Just a |
|
Lambda Reductions:
The following Lambda expression
\vv1→
| case | vv1 of |
| | (x,i) | → if p x then i : [] else [] |
| | _ | → [] |
is transformed to
| findIndices0 | p vv1 | =
| case | vv1 of | | | (x,i) | → if p x then i : [] else [] |
| | _ | → [] |
|
The following Lambda expression
\ab→(a,b)
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule Main
|
| ((List.elemIndex :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> Maybe Int) :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> Maybe Int) |
module List where
| | import qualified Main
import qualified Maybe
import qualified Prelude
|
| | elemIndex :: Eq a => a -> [a] -> Maybe Int
| elemIndex | x | = | findIndex (== x) |
|
| | findIndex :: (a -> Bool) -> [a] -> Maybe Int
| findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| | findIndices :: (a -> Bool) -> [a] -> [Int]
| findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
| |
| findIndices0 | p vv1 | = |
| case | vv1 of |
|
| (x,i) | -> | if p x then i : [] else [] |
|
| _ | -> | [] |
|
|
module Main where
| | import qualified List
import qualified Maybe
import qualified Prelude
|
module Maybe where
| | import qualified List
import qualified Main
import qualified Prelude
|
| | listToMaybe :: [a] -> Maybe a
| listToMaybe | [] | = | Nothing |
| listToMaybe | (a : _) | = | Just a |
|
Case Reductions:
The following Case expression
| case | vv1 of |
| | (x,i) | → if p x then i : [] else [] |
| | _ | → [] |
is transformed to
| findIndices00 | p (x,i) | = if p x then i : [] else [] |
| findIndices00 | p _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule Main
|
| ((List.elemIndex :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> Maybe Int) :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> Maybe Int) |
module List where
| | import qualified Main
import qualified Maybe
import qualified Prelude
|
| | elemIndex :: Eq a => a -> [a] -> Maybe Int
| elemIndex | x | = | findIndex (== x) |
|
| | findIndex :: (a -> Bool) -> [a] -> Maybe Int
| findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| | findIndices :: (a -> Bool) -> [a] -> [Int]
| findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
| |
| findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
| |
| findIndices00 | p (x,i) | = | if p x then i : [] else [] |
| findIndices00 | p _ | = | [] |
|
module Main where
| | import qualified List
import qualified Maybe
import qualified Prelude
|
module Maybe where
| | import qualified List
import qualified Main
import qualified Prelude
|
| | listToMaybe :: [a] -> Maybe a
| listToMaybe | [] | = | Nothing |
| listToMaybe | (a : _) | = | Just a |
|
If Reductions:
The following If expression
if p x then i : [] else []
is transformed to
| findIndices000 | i True | = i : [] |
| findIndices000 | i False | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule Main
|
| ((List.elemIndex :: (Eq b, Eq a) => (b,a) -> [(b,a)] -> Maybe Int) :: (Eq a, Eq b) => (b,a) -> [(b,a)] -> Maybe Int) |
module List where
| | import qualified Main
import qualified Maybe
import qualified Prelude
|
| | elemIndex :: Eq a => a -> [a] -> Maybe Int
| elemIndex | x | = | findIndex (== x) |
|
| | findIndex :: (a -> Bool) -> [a] -> Maybe Int
| findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| | findIndices :: (a -> Bool) -> [a] -> [Int]
| findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
| |
| findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
| |
| findIndices00 | p (x,i) | = | findIndices000 i (p x) |
| findIndices00 | p _ | = | [] |
|
| |
| findIndices000 | i True | = | i : [] |
| findIndices000 | i False | = | [] |
|
module Main where
| | import qualified List
import qualified Maybe
import qualified Prelude
|
module Maybe where
| | import qualified List
import qualified Main
import qualified Prelude
|
| | listToMaybe :: [a] -> Maybe a
| listToMaybe | [] | = | Nothing |
| listToMaybe | (a : _) | = | Just a |
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ NumRed
mainModule Main
|
| ((List.elemIndex :: (Eq a, Eq b) => (b,a) -> [(b,a)] -> Maybe Int) :: (Eq b, Eq a) => (b,a) -> [(b,a)] -> Maybe Int) |
module List where
| | import qualified Main
import qualified Maybe
import qualified Prelude
|
| | elemIndex :: Eq a => a -> [a] -> Maybe Int
| elemIndex | x | = | findIndex (== x) |
|
| | findIndex :: (a -> Bool) -> [a] -> Maybe Int
| findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| | findIndices :: (a -> Bool) -> [a] -> [Int]
| findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom 0)) |
|
| |
| findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
| |
| findIndices00 | p (x,i) | = | findIndices000 i (p x) |
| findIndices00 | p vw | = | [] |
|
| |
| findIndices000 | i True | = | i : [] |
| findIndices000 | i False | = | [] |
|
module Main where
| | import qualified List
import qualified Maybe
import qualified Prelude
|
module Maybe where
| | import qualified List
import qualified Main
import qualified Prelude
|
| | listToMaybe :: [a] -> Maybe a
| listToMaybe | [] | = | Nothing |
| listToMaybe | (a : vx) | = | Just a |
|
Num Reduction:All numbers are transformed to thier corresponding representation with Succ, Pred and Zero.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
|
| (List.elemIndex :: (Eq a, Eq b) => (a,b) -> [(a,b)] -> Maybe Int) |
module List where
| | import qualified Main
import qualified Maybe
import qualified Prelude
|
| | elemIndex :: Eq a => a -> [a] -> Maybe Int
| elemIndex | x | = | findIndex (== x) |
|
| | findIndex :: (a -> Bool) -> [a] -> Maybe Int
| findIndex | p | = | Maybe.listToMaybe . findIndices p |
|
| | findIndices :: (a -> Bool) -> [a] -> [Int]
| findIndices | p xs | = | concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero))) |
|
| |
| findIndices0 | p vv1 | = | findIndices00 p vv1 |
|
| |
| findIndices00 | p (x,i) | = | findIndices000 i (p x) |
| findIndices00 | p vw | = | [] |
|
| |
| findIndices000 | i True | = | i : [] |
| findIndices000 | i False | = | [] |
|
module Main where
| | import qualified List
import qualified Maybe
import qualified Prelude
|
module Maybe where
| | import qualified List
import qualified Main
import qualified Prelude
|
| | listToMaybe :: [a] -> Maybe a
| listToMaybe | [] | = | Nothing |
| listToMaybe | (a : vx) | = | Just a |
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(yv30100), Succ(yv400100)) → new_primMulNat(yv30100, Succ(yv400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(yv30100), Succ(yv400100)) → new_primMulNat(yv30100, Succ(yv400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(yv5700), Succ(yv4001000)) → new_primPlusNat(yv5700, yv4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(yv5700), Succ(yv4001000)) → new_primPlusNat(yv5700, yv4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs1(Left(yv300), Left(yv4000), app(app(ty_@2, ee), ef), df) → new_esEs3(yv300, yv4000, ee, ef)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(app(ty_Either, bba), bbb)) → new_esEs1(yv302, yv4002, bba, bbb)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(app(ty_@3, gh), ha), hb), gc, gd) → new_esEs2(yv300, yv4000, gh, ha, hb)
new_esEs0(Just(yv300), Just(yv4000), app(app(app(ty_@3, cg), da), db)) → new_esEs2(yv300, yv4000, cg, da, db)
new_esEs1(Right(yv300), Right(yv4000), eg, app(ty_Maybe, fa)) → new_esEs0(yv300, yv4000, fa)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(ty_[], bag)) → new_esEs(yv302, yv4002, bag)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(app(ty_Either, bcc), bcd), bca) → new_esEs1(yv300, yv4000, bcc, bcd)
new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(app(app(ty_@3, be), bf), bg)) → new_esEs2(yv300, yv4000, be, bf, bg)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(ty_@2, hc), hd), gc, gd) → new_esEs3(yv300, yv4000, hc, hd)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs2(yv301, yv4001, bdg, bdh, bea)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(ty_[], gb), gc, gd) → new_esEs(yv300, yv4000, gb)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(ty_Maybe, hg), gd) → new_esEs0(yv301, yv4001, hg)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(ty_[], bbh), bca) → new_esEs(yv300, yv4000, bbh)
new_esEs0(Just(yv300), Just(yv4000), app(ty_Maybe, cd)) → new_esEs0(yv300, yv4000, cd)
new_esEs0(Just(yv300), Just(yv4000), app(ty_[], cc)) → new_esEs(yv300, yv4000, cc)
new_esEs1(Left(yv300), Left(yv4000), app(app(ty_Either, dh), ea), df) → new_esEs1(yv300, yv4000, dh, ea)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(app(ty_@2, bae), baf), gd) → new_esEs3(yv301, yv4001, bae, baf)
new_esEs1(Right(yv300), Right(yv4000), eg, app(app(ty_Either, fb), fc)) → new_esEs1(yv300, yv4000, fb, fc)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(ty_Maybe, bah)) → new_esEs0(yv302, yv4002, bah)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(ty_Maybe, ge), gc, gd) → new_esEs0(yv300, yv4000, ge)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(ty_[], bdc)) → new_esEs(yv301, yv4001, bdc)
new_esEs1(Left(yv300), Left(yv4000), app(ty_Maybe, dg), df) → new_esEs0(yv300, yv4000, dg)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(app(ty_@2, beb), bec)) → new_esEs3(yv301, yv4001, beb, bec)
new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(ty_Maybe, bb)) → new_esEs0(yv300, yv4000, bb)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(app(ty_Either, hh), baa), gd) → new_esEs1(yv301, yv4001, hh, baa)
new_esEs1(Left(yv300), Left(yv4000), app(app(app(ty_@3, eb), ec), ed), df) → new_esEs2(yv300, yv4000, eb, ec, ed)
new_esEs(:(yv300, yv301), :(yv4000, yv4001), cb) → new_esEs(yv301, yv4001, cb)
new_esEs1(Right(yv300), Right(yv4000), eg, app(app(app(ty_@3, fd), ff), fg)) → new_esEs2(yv300, yv4000, fd, ff, fg)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(ty_Maybe, bcb), bca) → new_esEs0(yv300, yv4000, bcb)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(app(ty_Either, bde), bdf)) → new_esEs1(yv301, yv4001, bde, bdf)
new_esEs0(Just(yv300), Just(yv4000), app(app(ty_Either, ce), cf)) → new_esEs1(yv300, yv4000, ce, cf)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(app(app(ty_@3, bab), bac), bad), gd) → new_esEs2(yv301, yv4001, bab, bac, bad)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(ty_[], hf), gd) → new_esEs(yv301, yv4001, hf)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(app(ty_@2, bch), bda), bca) → new_esEs3(yv300, yv4000, bch, bda)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(ty_Maybe, bdd)) → new_esEs0(yv301, yv4001, bdd)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(ty_Either, gf), gg), gc, gd) → new_esEs1(yv300, yv4000, gf, gg)
new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(app(ty_@2, bh), ca)) → new_esEs3(yv300, yv4000, bh, ca)
new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(app(app(ty_@3, bce), bcf), bcg), bca) → new_esEs2(yv300, yv4000, bce, bcf, bcg)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(app(ty_@2, bbf), bbg)) → new_esEs3(yv302, yv4002, bbf, bbg)
new_esEs1(Right(yv300), Right(yv4000), eg, app(ty_[], eh)) → new_esEs(yv300, yv4000, eh)
new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(app(ty_Either, bc), bd)) → new_esEs1(yv300, yv4000, bc, bd)
new_esEs1(Left(yv300), Left(yv4000), app(ty_[], de), df) → new_esEs(yv300, yv4000, de)
new_esEs1(Right(yv300), Right(yv4000), eg, app(app(ty_@2, fh), ga)) → new_esEs3(yv300, yv4000, fh, ga)
new_esEs0(Just(yv300), Just(yv4000), app(app(ty_@2, dc), dd)) → new_esEs3(yv300, yv4000, dc, dd)
new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(ty_[], ba)) → new_esEs(yv300, yv4000, ba)
new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs2(yv302, yv4002, bbc, bbd, bbe)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(app(app(ty_@3, be), bf), bg)) → new_esEs2(yv300, yv4000, be, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(yv300), Just(yv4000), app(app(app(ty_@3, cg), da), db)) → new_esEs2(yv300, yv4000, cg, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(app(ty_Either, bc), bd)) → new_esEs1(yv300, yv4000, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(yv300), Just(yv4000), app(app(ty_Either, ce), cf)) → new_esEs1(yv300, yv4000, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(ty_Maybe, bb)) → new_esEs0(yv300, yv4000, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(yv300), Just(yv4000), app(ty_Maybe, cd)) → new_esEs0(yv300, yv4000, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(app(ty_@2, bh), ca)) → new_esEs3(yv300, yv4000, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(yv300), Just(yv4000), app(app(ty_@2, dc), dd)) → new_esEs3(yv300, yv4000, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(yv300), Just(yv4000), app(ty_[], cc)) → new_esEs(yv300, yv4000, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(yv300), Left(yv4000), app(app(app(ty_@3, eb), ec), ed), df) → new_esEs2(yv300, yv4000, eb, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Right(yv300), Right(yv4000), eg, app(app(app(ty_@3, fd), ff), fg)) → new_esEs2(yv300, yv4000, fd, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(Left(yv300), Left(yv4000), app(app(ty_Either, dh), ea), df) → new_esEs1(yv300, yv4000, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(yv300), Right(yv4000), eg, app(app(ty_Either, fb), fc)) → new_esEs1(yv300, yv4000, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Right(yv300), Right(yv4000), eg, app(ty_Maybe, fa)) → new_esEs0(yv300, yv4000, fa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(yv300), Left(yv4000), app(ty_Maybe, dg), df) → new_esEs0(yv300, yv4000, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Left(yv300), Left(yv4000), app(app(ty_@2, ee), ef), df) → new_esEs3(yv300, yv4000, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(yv300), Right(yv4000), eg, app(app(ty_@2, fh), ga)) → new_esEs3(yv300, yv4000, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Right(yv300), Right(yv4000), eg, app(ty_[], eh)) → new_esEs(yv300, yv4000, eh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(yv300), Left(yv4000), app(ty_[], de), df) → new_esEs(yv300, yv4000, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs2(yv301, yv4001, bdg, bdh, bea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(app(app(ty_@3, bce), bcf), bcg), bca) → new_esEs2(yv300, yv4000, bce, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(app(ty_@3, gh), ha), hb), gc, gd) → new_esEs2(yv300, yv4000, gh, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(app(app(ty_@3, bab), bac), bad), gd) → new_esEs2(yv301, yv4001, bab, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs2(yv302, yv4002, bbc, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(app(ty_Either, bcc), bcd), bca) → new_esEs1(yv300, yv4000, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(app(ty_Either, bde), bdf)) → new_esEs1(yv301, yv4001, bde, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(ty_Maybe, bcb), bca) → new_esEs0(yv300, yv4000, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(ty_Maybe, bdd)) → new_esEs0(yv301, yv4001, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(app(ty_@2, beb), bec)) → new_esEs3(yv301, yv4001, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(app(ty_@2, bch), bda), bca) → new_esEs3(yv300, yv4000, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), app(ty_[], bbh), bca) → new_esEs(yv300, yv4000, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(yv300, yv301), @2(yv4000, yv4001), bdb, app(ty_[], bdc)) → new_esEs(yv301, yv4001, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(app(ty_Either, bba), bbb)) → new_esEs1(yv302, yv4002, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(app(ty_Either, hh), baa), gd) → new_esEs1(yv301, yv4001, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(ty_Either, gf), gg), gc, gd) → new_esEs1(yv300, yv4000, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(ty_Maybe, hg), gd) → new_esEs0(yv301, yv4001, hg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(ty_Maybe, bah)) → new_esEs0(yv302, yv4002, bah)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(ty_Maybe, ge), gc, gd) → new_esEs0(yv300, yv4000, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(ty_@2, hc), hd), gc, gd) → new_esEs3(yv300, yv4000, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(app(ty_@2, bae), baf), gd) → new_esEs3(yv301, yv4001, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(app(ty_@2, bbf), bbg)) → new_esEs3(yv302, yv4002, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, gc, app(ty_[], bag)) → new_esEs(yv302, yv4002, bag)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(ty_[], gb), gc, gd) → new_esEs(yv300, yv4000, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), he, app(ty_[], hf), gd) → new_esEs(yv301, yv4001, hf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(:(yv300, yv301), :(yv4000, yv4001), cb) → new_esEs(yv301, yv4001, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(yv300, yv301), :(yv4000, yv4001), app(ty_[], ba)) → new_esEs(yv300, yv4000, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_listToMaybe(yv41, False, yv22, yv23, :(yv24110, yv24111), ba, bb) → new_listToMaybe(new_primPlusNat0(yv41, Zero), new_esEs4(@2(yv22, yv23), yv24110, ba, bb), yv22, yv23, yv24111, ba, bb)
The TRS R consists of the following rules:
new_esEs12(Just(yv300), Just(yv4000), ty_Ordering) → new_esEs9(yv300, yv4000)
new_esEs25(yv302, yv4002, ty_Int) → new_esEs8(yv302, yv4002)
new_esEs23(yv300, yv4000, app(ty_Maybe, bcd)) → new_esEs12(yv300, yv4000, bcd)
new_esEs19(yv300, yv4000, ty_Int) → new_esEs8(yv300, yv4000)
new_primPlusNat1(Succ(yv5700), Succ(yv4001000)) → Succ(Succ(new_primPlusNat1(yv5700, yv4001000)))
new_primEqInt(Neg(Succ(yv3000)), Pos(yv4000)) → False
new_primEqInt(Pos(Succ(yv3000)), Neg(yv4000)) → False
new_esEs7(yv300, yv4000, app(ty_Maybe, be)) → new_esEs12(yv300, yv4000, be)
new_esEs24(yv301, yv4001, app(app(ty_@2, bee), bef)) → new_esEs4(yv301, yv4001, bee, bef)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs14(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), bbh, bca, bcb) → new_asAs(new_esEs23(yv300, yv4000, bbh), new_asAs(new_esEs24(yv301, yv4001, bca), new_esEs25(yv302, yv4002, bcb)))
new_esEs23(yv300, yv4000, app(app(ty_@2, bdc), bdd)) → new_esEs4(yv300, yv4000, bdc, bdd)
new_primEqInt(Neg(Zero), Pos(Succ(yv40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yv40000))) → False
new_esEs6(:(yv300, yv301), :(yv4000, yv4001), bc) → new_asAs(new_esEs7(yv300, yv4000, bc), new_esEs6(yv301, yv4001, bc))
new_esEs13(Left(yv300), Left(yv4000), app(app(ty_Either, hd), he), ha) → new_esEs13(yv300, yv4000, hd, he)
new_esEs12(Just(yv300), Just(yv4000), ty_Int) → new_esEs8(yv300, yv4000)
new_esEs23(yv300, yv4000, app(app(ty_Either, bce), bcf)) → new_esEs13(yv300, yv4000, bce, bcf)
new_esEs13(Left(yv300), Left(yv4000), ty_Ordering, ha) → new_esEs9(yv300, yv4000)
new_esEs13(Right(yv300), Right(yv4000), bad, ty_Double) → new_esEs15(yv300, yv4000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs19(yv300, yv4000, ty_Ordering) → new_esEs9(yv300, yv4000)
new_esEs20(yv301, yv4001, app(ty_Ratio, fb)) → new_esEs16(yv301, yv4001, fb)
new_esEs25(yv302, yv4002, app(app(ty_@2, bfg), bfh)) → new_esEs4(yv302, yv4002, bfg, bfh)
new_esEs21(yv300, yv4000, ty_Integer) → new_esEs5(yv300, yv4000)
new_primPlusNat0(Zero, yv400100) → Succ(yv400100)
new_esEs20(yv301, yv4001, ty_Bool) → new_esEs18(yv301, yv4001)
new_esEs9(GT, GT) → True
new_esEs13(Left(yv300), Left(yv4000), ty_Char, ha) → new_esEs11(yv300, yv4000)
new_esEs13(Right(yv300), Right(yv4000), bad, app(ty_[], bae)) → new_esEs6(yv300, yv4000, bae)
new_esEs25(yv302, yv4002, app(ty_Ratio, bff)) → new_esEs16(yv302, yv4002, bff)
new_esEs25(yv302, yv4002, ty_Float) → new_esEs10(yv302, yv4002)
new_sr(Pos(yv3010), Neg(yv40010)) → Neg(new_primMulNat0(yv3010, yv40010))
new_sr(Neg(yv3010), Pos(yv40010)) → Neg(new_primMulNat0(yv3010, yv40010))
new_esEs13(Left(yv300), Left(yv4000), app(ty_Maybe, hc), ha) → new_esEs12(yv300, yv4000, hc)
new_esEs13(Right(yv300), Right(yv4000), bad, ty_Char) → new_esEs11(yv300, yv4000)
new_esEs13(Left(yv300), Left(yv4000), app(app(ty_@2, bab), bac), ha) → new_esEs4(yv300, yv4000, bab, bac)
new_esEs5(Integer(yv300), Integer(yv4000)) → new_primEqInt(yv300, yv4000)
new_esEs24(yv301, yv4001, app(ty_[], bde)) → new_esEs6(yv301, yv4001, bde)
new_esEs24(yv301, yv4001, ty_Double) → new_esEs15(yv301, yv4001)
new_esEs25(yv302, yv4002, ty_Double) → new_esEs15(yv302, yv4002)
new_esEs13(Left(yv300), Left(yv4000), ty_Integer, ha) → new_esEs5(yv300, yv4000)
new_esEs20(yv301, yv4001, app(app(ty_Either, ee), ef)) → new_esEs13(yv301, yv4001, ee, ef)
new_esEs24(yv301, yv4001, ty_Int) → new_esEs8(yv301, yv4001)
new_esEs24(yv301, yv4001, ty_@0) → new_esEs17(yv301, yv4001)
new_esEs20(yv301, yv4001, ty_Char) → new_esEs11(yv301, yv4001)
new_esEs12(Just(yv300), Just(yv4000), ty_Bool) → new_esEs18(yv300, yv4000)
new_esEs12(Just(yv300), Just(yv4000), app(ty_Ratio, gf)) → new_esEs16(yv300, yv4000, gf)
new_esEs23(yv300, yv4000, ty_Ordering) → new_esEs9(yv300, yv4000)
new_primEqNat0(Succ(yv30000), Zero) → False
new_primEqNat0(Zero, Succ(yv400000)) → False
new_esEs17(@0, @0) → True
new_esEs7(yv300, yv4000, ty_Float) → new_esEs10(yv300, yv4000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs25(yv302, yv4002, ty_Char) → new_esEs11(yv302, yv4002)
new_esEs11(Char(yv300), Char(yv4000)) → new_primEqInt(yv300, yv4000)
new_esEs20(yv301, yv4001, ty_Integer) → new_esEs5(yv301, yv4001)
new_esEs13(Right(yv300), Right(yv4000), bad, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs14(yv300, yv4000, bba, bbb, bbc)
new_esEs7(yv300, yv4000, ty_Double) → new_esEs15(yv300, yv4000)
new_esEs15(Double(yv300, yv301), Double(yv4000, yv4001)) → new_esEs8(new_sr(yv300, yv4000), new_sr(yv301, yv4001))
new_esEs13(Right(yv300), Right(yv4000), bad, ty_Integer) → new_esEs5(yv300, yv4000)
new_esEs13(Left(yv300), Left(yv4000), ty_Float, ha) → new_esEs10(yv300, yv4000)
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_esEs13(Right(yv300), Right(yv4000), bad, ty_@0) → new_esEs17(yv300, yv4000)
new_esEs6([], :(yv4000, yv4001), bc) → False
new_esEs6(:(yv300, yv301), [], bc) → False
new_esEs13(Left(yv300), Left(yv4000), ty_@0, ha) → new_esEs17(yv300, yv4000)
new_esEs7(yv300, yv4000, app(ty_[], bd)) → new_esEs6(yv300, yv4000, bd)
new_esEs23(yv300, yv4000, app(ty_Ratio, bdb)) → new_esEs16(yv300, yv4000, bdb)
new_esEs13(Left(yv300), Left(yv4000), ty_Int, ha) → new_esEs8(yv300, yv4000)
new_esEs16(:%(yv300, yv301), :%(yv4000, yv4001), bbg) → new_asAs(new_esEs21(yv300, yv4000, bbg), new_esEs22(yv301, yv4001, bbg))
new_esEs7(yv300, yv4000, ty_Int) → new_esEs8(yv300, yv4000)
new_esEs19(yv300, yv4000, app(ty_Ratio, dh)) → new_esEs16(yv300, yv4000, dh)
new_sr(Neg(yv3010), Neg(yv40010)) → Pos(new_primMulNat0(yv3010, yv40010))
new_esEs24(yv301, yv4001, ty_Char) → new_esEs11(yv301, yv4001)
new_esEs12(Nothing, Just(yv4000), ff) → False
new_esEs12(Just(yv300), Nothing, ff) → False
new_asAs(False, yv56) → False
new_esEs7(yv300, yv4000, ty_Bool) → new_esEs18(yv300, yv4000)
new_sr(Pos(yv3010), Pos(yv40010)) → Pos(new_primMulNat0(yv3010, yv40010))
new_esEs19(yv300, yv4000, app(ty_Maybe, db)) → new_esEs12(yv300, yv4000, db)
new_esEs19(yv300, yv4000, ty_Float) → new_esEs10(yv300, yv4000)
new_primEqNat0(Zero, Zero) → True
new_esEs20(yv301, yv4001, app(ty_Maybe, ed)) → new_esEs12(yv301, yv4001, ed)
new_esEs12(Just(yv300), Just(yv4000), ty_@0) → new_esEs17(yv300, yv4000)
new_primMulNat0(Succ(yv30100), Zero) → Zero
new_primMulNat0(Zero, Succ(yv400100)) → Zero
new_esEs19(yv300, yv4000, app(app(ty_Either, dc), dd)) → new_esEs13(yv300, yv4000, dc, dd)
new_esEs25(yv302, yv4002, ty_Bool) → new_esEs18(yv302, yv4002)
new_esEs24(yv301, yv4001, ty_Float) → new_esEs10(yv301, yv4001)
new_esEs13(Right(yv300), Right(yv4000), bad, app(ty_Maybe, baf)) → new_esEs12(yv300, yv4000, baf)
new_esEs18(True, True) → True
new_esEs24(yv301, yv4001, ty_Integer) → new_esEs5(yv301, yv4001)
new_esEs12(Nothing, Nothing, ff) → True
new_esEs7(yv300, yv4000, ty_Ordering) → new_esEs9(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Integer) → new_esEs5(yv301, yv4001)
new_esEs19(yv300, yv4000, ty_Double) → new_esEs15(yv300, yv4000)
new_esEs12(Just(yv300), Just(yv4000), app(app(ty_@2, gg), gh)) → new_esEs4(yv300, yv4000, gg, gh)
new_esEs23(yv300, yv4000, ty_Integer) → new_esEs5(yv300, yv4000)
new_esEs13(Right(yv300), Right(yv4000), bad, ty_Int) → new_esEs8(yv300, yv4000)
new_esEs13(Left(yv300), Left(yv4000), app(ty_[], hb), ha) → new_esEs6(yv300, yv4000, hb)
new_esEs12(Just(yv300), Just(yv4000), app(app(ty_Either, ga), gb)) → new_esEs13(yv300, yv4000, ga, gb)
new_esEs13(Left(yv300), Left(yv4000), ty_Bool, ha) → new_esEs18(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Int) → new_esEs8(yv301, yv4001)
new_primPlusNat0(Succ(yv570), yv400100) → Succ(Succ(new_primPlusNat1(yv570, yv400100)))
new_esEs19(yv300, yv4000, app(ty_[], da)) → new_esEs6(yv300, yv4000, da)
new_esEs20(yv301, yv4001, app(app(ty_@2, fc), fd)) → new_esEs4(yv301, yv4001, fc, fd)
new_esEs7(yv300, yv4000, app(app(ty_@2, cd), ce)) → new_esEs4(yv300, yv4000, cd, ce)
new_esEs7(yv300, yv4000, ty_@0) → new_esEs17(yv300, yv4000)
new_esEs23(yv300, yv4000, ty_Bool) → new_esEs18(yv300, yv4000)
new_esEs20(yv301, yv4001, app(app(app(ty_@3, eg), eh), fa)) → new_esEs14(yv301, yv4001, eg, eh, fa)
new_esEs20(yv301, yv4001, ty_Ordering) → new_esEs9(yv301, yv4001)
new_esEs25(yv302, yv4002, app(ty_Maybe, beh)) → new_esEs12(yv302, yv4002, beh)
new_esEs9(EQ, EQ) → True
new_esEs12(Just(yv300), Just(yv4000), app(ty_[], fg)) → new_esEs6(yv300, yv4000, fg)
new_primEqInt(Neg(Succ(yv3000)), Neg(Succ(yv40000))) → new_primEqNat0(yv3000, yv40000)
new_esEs25(yv302, yv4002, app(ty_[], beg)) → new_esEs6(yv302, yv4002, beg)
new_esEs24(yv301, yv4001, ty_Bool) → new_esEs18(yv301, yv4001)
new_esEs7(yv300, yv4000, ty_Integer) → new_esEs5(yv300, yv4000)
new_esEs23(yv300, yv4000, app(ty_[], bcc)) → new_esEs6(yv300, yv4000, bcc)
new_esEs13(Right(yv300), Left(yv4000), bad, ha) → False
new_esEs13(Left(yv300), Right(yv4000), bad, ha) → False
new_esEs19(yv300, yv4000, ty_Integer) → new_esEs5(yv300, yv4000)
new_esEs13(Right(yv300), Right(yv4000), bad, app(app(ty_Either, bag), bah)) → new_esEs13(yv300, yv4000, bag, bah)
new_esEs7(yv300, yv4000, app(app(app(ty_@3, bh), ca), cb)) → new_esEs14(yv300, yv4000, bh, ca, cb)
new_esEs6([], [], bc) → True
new_esEs19(yv300, yv4000, ty_Bool) → new_esEs18(yv300, yv4000)
new_esEs24(yv301, yv4001, app(ty_Maybe, bdf)) → new_esEs12(yv301, yv4001, bdf)
new_primPlusNat1(Succ(yv5700), Zero) → Succ(yv5700)
new_primPlusNat1(Zero, Succ(yv4001000)) → Succ(yv4001000)
new_esEs12(Just(yv300), Just(yv4000), ty_Integer) → new_esEs5(yv300, yv4000)
new_esEs13(Right(yv300), Right(yv4000), bad, ty_Bool) → new_esEs18(yv300, yv4000)
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs13(Right(yv300), Right(yv4000), bad, ty_Ordering) → new_esEs9(yv300, yv4000)
new_esEs23(yv300, yv4000, ty_Char) → new_esEs11(yv300, yv4000)
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_primEqInt(Neg(Zero), Neg(Succ(yv40000))) → False
new_primEqInt(Neg(Succ(yv3000)), Neg(Zero)) → False
new_esEs25(yv302, yv4002, ty_Ordering) → new_esEs9(yv302, yv4002)
new_esEs24(yv301, yv4001, app(app(ty_Either, bdg), bdh)) → new_esEs13(yv301, yv4001, bdg, bdh)
new_esEs24(yv301, yv4001, ty_Ordering) → new_esEs9(yv301, yv4001)
new_esEs12(Just(yv300), Just(yv4000), app(ty_Maybe, fh)) → new_esEs12(yv300, yv4000, fh)
new_esEs10(Float(yv300, yv301), Float(yv4000, yv4001)) → new_esEs8(new_sr(yv300, yv4000), new_sr(yv301, yv4001))
new_esEs13(Left(yv300), Left(yv4000), ty_Double, ha) → new_esEs15(yv300, yv4000)
new_esEs20(yv301, yv4001, ty_@0) → new_esEs17(yv301, yv4001)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs7(yv300, yv4000, app(app(ty_Either, bf), bg)) → new_esEs13(yv300, yv4000, bf, bg)
new_esEs19(yv300, yv4000, ty_@0) → new_esEs17(yv300, yv4000)
new_esEs12(Just(yv300), Just(yv4000), app(app(app(ty_@3, gc), gd), ge)) → new_esEs14(yv300, yv4000, gc, gd, ge)
new_esEs20(yv301, yv4001, ty_Int) → new_esEs8(yv301, yv4001)
new_asAs(True, yv56) → yv56
new_esEs20(yv301, yv4001, ty_Double) → new_esEs15(yv301, yv4001)
new_primMulNat0(Succ(yv30100), Succ(yv400100)) → new_primPlusNat0(new_primMulNat0(yv30100, Succ(yv400100)), yv400100)
new_esEs25(yv302, yv4002, ty_@0) → new_esEs17(yv302, yv4002)
new_esEs23(yv300, yv4000, ty_Float) → new_esEs10(yv300, yv4000)
new_esEs25(yv302, yv4002, app(app(ty_Either, bfa), bfb)) → new_esEs13(yv302, yv4002, bfa, bfb)
new_esEs12(Just(yv300), Just(yv4000), ty_Float) → new_esEs10(yv300, yv4000)
new_esEs19(yv300, yv4000, ty_Char) → new_esEs11(yv300, yv4000)
new_esEs20(yv301, yv4001, app(ty_[], ec)) → new_esEs6(yv301, yv4001, ec)
new_primEqInt(Pos(Succ(yv3000)), Pos(Succ(yv40000))) → new_primEqNat0(yv3000, yv40000)
new_esEs4(@2(yv300, yv301), @2(yv4000, yv4001), cf, cg) → new_asAs(new_esEs19(yv300, yv4000, cf), new_esEs20(yv301, yv4001, cg))
new_esEs25(yv302, yv4002, ty_Integer) → new_esEs5(yv302, yv4002)
new_esEs13(Right(yv300), Right(yv4000), bad, app(app(ty_@2, bbe), bbf)) → new_esEs4(yv300, yv4000, bbe, bbf)
new_esEs24(yv301, yv4001, app(ty_Ratio, bed)) → new_esEs16(yv301, yv4001, bed)
new_primEqNat0(Succ(yv30000), Succ(yv400000)) → new_primEqNat0(yv30000, yv400000)
new_esEs25(yv302, yv4002, app(app(app(ty_@3, bfc), bfd), bfe)) → new_esEs14(yv302, yv4002, bfc, bfd, bfe)
new_esEs12(Just(yv300), Just(yv4000), ty_Double) → new_esEs15(yv300, yv4000)
new_esEs23(yv300, yv4000, app(app(app(ty_@3, bcg), bch), bda)) → new_esEs14(yv300, yv4000, bcg, bch, bda)
new_esEs13(Right(yv300), Right(yv4000), bad, app(ty_Ratio, bbd)) → new_esEs16(yv300, yv4000, bbd)
new_esEs7(yv300, yv4000, ty_Char) → new_esEs11(yv300, yv4000)
new_esEs19(yv300, yv4000, app(app(app(ty_@3, de), df), dg)) → new_esEs14(yv300, yv4000, de, df, dg)
new_esEs9(LT, LT) → True
new_esEs20(yv301, yv4001, ty_Float) → new_esEs10(yv301, yv4001)
new_esEs13(Left(yv300), Left(yv4000), app(ty_Ratio, baa), ha) → new_esEs16(yv300, yv4000, baa)
new_esEs7(yv300, yv4000, app(ty_Ratio, cc)) → new_esEs16(yv300, yv4000, cc)
new_esEs12(Just(yv300), Just(yv4000), ty_Char) → new_esEs11(yv300, yv4000)
new_esEs23(yv300, yv4000, ty_Double) → new_esEs15(yv300, yv4000)
new_esEs19(yv300, yv4000, app(app(ty_@2, ea), eb)) → new_esEs4(yv300, yv4000, ea, eb)
new_esEs24(yv301, yv4001, app(app(app(ty_@3, bea), beb), bec)) → new_esEs14(yv301, yv4001, bea, beb, bec)
new_esEs23(yv300, yv4000, ty_Int) → new_esEs8(yv300, yv4000)
new_esEs21(yv300, yv4000, ty_Int) → new_esEs8(yv300, yv4000)
new_primEqInt(Pos(Zero), Pos(Succ(yv40000))) → False
new_primEqInt(Pos(Succ(yv3000)), Pos(Zero)) → False
new_esEs13(Right(yv300), Right(yv4000), bad, ty_Float) → new_esEs10(yv300, yv4000)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs13(Left(yv300), Left(yv4000), app(app(app(ty_@3, hf), hg), hh), ha) → new_esEs14(yv300, yv4000, hf, hg, hh)
new_esEs8(yv30, yv400) → new_primEqInt(yv30, yv400)
new_esEs23(yv300, yv4000, ty_@0) → new_esEs17(yv300, yv4000)
new_esEs18(False, False) → True
The set Q consists of the following terms:
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs9(GT, GT)
new_esEs12(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, ty_Int)
new_esEs7(x0, x1, ty_Char)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_@0)
new_esEs12(Nothing, Just(x0), x1)
new_esEs12(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(x0, x1, ty_Bool)
new_esEs18(False, True)
new_esEs18(True, False)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs9(EQ, EQ)
new_esEs14(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs6(:(x0, x1), [], x2)
new_esEs7(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs6([], [], x0)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs20(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(True, True)
new_esEs6([], :(x0, x1), x2)
new_primPlusNat0(Zero, x0)
new_esEs21(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Bool)
new_esEs9(LT, GT)
new_esEs9(GT, LT)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs12(Just(x0), Just(x1), ty_Bool)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs7(x0, x1, ty_Bool)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Zero)
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs23(x0, x1, ty_Float)
new_esEs19(x0, x1, ty_Float)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs12(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_Double)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs7(x0, x1, ty_@0)
new_esEs7(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Ordering)
new_esEs12(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Int)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(x0, x1, ty_Int)
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs24(x0, x1, ty_Double)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs25(x0, x1, ty_Char)
new_esEs11(Char(x0), Char(x1))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Int)
new_esEs12(Just(x0), Just(x1), app(ty_[], x2))
new_primMulNat0(Zero, Zero)
new_esEs12(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs12(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs7(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Bool)
new_esEs8(x0, x1)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_esEs12(Just(x0), Just(x1), ty_@0)
new_esEs19(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs12(Just(x0), Just(x1), ty_Double)
new_esEs12(Just(x0), Just(x1), ty_Int)
new_asAs(False, x0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs9(LT, EQ)
new_esEs9(EQ, LT)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs25(x0, x1, ty_Float)
new_esEs12(Nothing, Nothing, x0)
new_esEs20(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_[], x2))
new_primMulNat0(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs18(False, False)
new_esEs19(x0, x1, ty_Ordering)
new_esEs20(x0, x1, ty_Integer)
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Just(x0), Just(x1), ty_Char)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs20(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Int)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Zero, Succ(x0))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs5(Integer(x0), Integer(x1))
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Zero)
new_esEs24(x0, x1, ty_Float)
new_esEs7(x0, x1, ty_Ordering)
new_esEs19(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Char)
new_primEqNat0(Zero, Succ(x0))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs12(Just(x0), Nothing, x1)
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs12(Just(x0), Just(x1), ty_Integer)
new_esEs23(x0, x1, ty_Bool)
new_asAs(True, x0)
new_esEs23(x0, x1, ty_Double)
new_esEs6(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_esEs17(@0, @0)
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs19(x0, x1, ty_@0)
new_esEs7(x0, x1, ty_Float)
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(Just(x0), Just(x1), ty_Ordering)
new_esEs9(LT, LT)
new_esEs10(Float(x0, x1), Float(x2, x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Succ(x0), Zero)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs15(Double(x0, x1), Double(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:
- new_listToMaybe(yv41, False, yv22, yv23, :(yv24110, yv24111), ba, bb) → new_listToMaybe(new_primPlusNat0(yv41, Zero), new_esEs4(@2(yv22, yv23), yv24110, ba, bb), yv22, yv23, yv24111, ba, bb)
The graph contains the following edges 3 >= 3, 4 >= 4, 5 > 5, 6 >= 6, 7 >= 7
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(yv30000), Succ(yv400000)) → new_primEqNat(yv30000, yv400000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(yv30000), Succ(yv400000)) → new_primEqNat(yv30000, yv400000)
The graph contains the following edges 1 > 1, 2 > 2