YES
H-Termination proof of ../tpdb/FP/full_haskell/Prelude_compare_10.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ CR
mainModule Main
|
| ((compare :: (Ord b, Ord a) => Either a b -> Either a b -> Ordering) :: (Ord b, Ord a) => Either a b -> Either a b -> Ordering) |
module Main where
Case Reductions:
The following Case expression
| case | compare x y of |
| | EQ | → o |
| | LT | → LT |
| | GT | → GT |
is transformed to
| primCompAux0 | o EQ | = o |
| primCompAux0 | o LT | = LT |
| primCompAux0 | o GT | = GT |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule Main
|
| ((compare :: (Ord b, Ord a) => Either b a -> Either b a -> Ordering) :: (Ord a, Ord b) => Either b a -> Either b a -> Ordering) |
module Main where
If Reductions:
The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero
is transformed to
| primDivNatS0 | x y True | = Succ (primDivNatS (primMinusNatS x y) (Succ y)) |
| primDivNatS0 | x y False | = Zero |
The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x
is transformed to
| primModNatS0 | x y True | = primModNatS (primMinusNatS x y) (Succ y) |
| primModNatS0 | x y False | = Succ x |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule Main
|
| ((compare :: (Ord a, Ord b) => Either b a -> Either b a -> Ordering) :: (Ord a, Ord b) => Either b a -> Either b a -> Ordering) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
|
| ((compare :: (Ord a, Ord b) => Either a b -> Either a b -> Ordering) :: (Ord a, Ord b) => Either a b -> Either a b -> Ordering) |
module Main where
Cond Reductions:
The following Function with conditions
| gcd' | x 0 | = x |
| gcd' | x y | = gcd' y (x `rem` y) |
is transformed to
| gcd' | x zx | = gcd'2 x zx |
| gcd' | x y | = gcd'0 x y |
| gcd'0 | x y | = gcd' y (x `rem` y) |
| gcd'1 | True x zx | = x |
| gcd'1 | zy zz vuu | = gcd'0 zz vuu |
| gcd'2 | x zx | = gcd'1 (zx == 0) x zx |
| gcd'2 | vuv vuw | = gcd'0 vuv vuw |
The following Function with conditions
| gcd | 0 0 | = error [] |
| gcd | x y | =
| gcd' (abs x) (abs y) |
| where |
| gcd' | x 0 | = x |
| gcd' | x y | = gcd' y (x `rem` y) |
|
|
is transformed to
| gcd | vux vuy | = gcd3 vux vuy |
| gcd | x y | = gcd0 x y |
| gcd0 | x y | =
| gcd' (abs x) (abs y) |
| where |
| gcd' | x zx | = gcd'2 x zx |
| gcd' | x y | = gcd'0 x y |
|
|
| gcd'0 | x y | = gcd' y (x `rem` y) |
|
|
| gcd'1 | True x zx | = x |
| gcd'1 | zy zz vuu | = gcd'0 zz vuu |
|
|
| gcd'2 | x zx | = gcd'1 (zx == 0) x zx |
| gcd'2 | vuv vuw | = gcd'0 vuv vuw |
|
|
| gcd1 | True vux vuy | = error [] |
| gcd1 | vuz vvu vvv | = gcd0 vvu vvv |
| gcd2 | True vux vuy | = gcd1 (vuy == 0) vux vuy |
| gcd2 | vvw vvx vvy | = gcd0 vvx vvy |
| gcd3 | vux vuy | = gcd2 (vux == 0) vux vuy |
| gcd3 | vvz vwu | = gcd0 vvz vwu |
The following Function with conditions
is transformed to
| absReal1 | x True | = x |
| absReal1 | x False | = absReal0 x otherwise |
| absReal0 | x True | = `negate` x |
| absReal2 | x | = absReal1 x (x >= 0) |
The following Function with conditions
is transformed to
| undefined0 | True | = undefined |
| undefined1 | | = undefined0 False |
The following Function with conditions
| reduce | x y |
| | | y == 0 | |
| | | otherwise |
| = | x `quot` d :% (y `quot` d) |
|
|
| where | |
|
is transformed to
| reduce2 | x y | =
| reduce1 x y (y == 0) |
| where | |
|
| reduce0 | x y True | = x `quot` d :% (y `quot` d) |
|
|
| reduce1 | x y True | = error [] |
| reduce1 | x y False | = reduce0 x y otherwise |
|
|
The following Function with conditions
| compare | x y |
| | | x == y | |
| | | x <= y | |
| | | otherwise | |
|
is transformed to
| compare | x y | = compare3 x y |
| compare2 | x y True | = EQ |
| compare2 | x y False | = compare1 x y (x <= y) |
| compare1 | x y True | = LT |
| compare1 | x y False | = compare0 x y otherwise |
| compare3 | x y | = compare2 x y (x == y) |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
|
| ((compare :: (Ord b, Ord a) => Either b a -> Either b a -> Ordering) :: (Ord a, Ord b) => Either b a -> Either b a -> Ordering) |
module Main where
Let/Where Reductions:
The bindings of the following Let/Where expression
| reduce1 x y (y == 0) |
| where | |
|
| reduce0 | x y True | = x `quot` d :% (y `quot` d) |
|
|
| reduce1 | x y True | = error [] |
| reduce1 | x y False | = reduce0 x y otherwise |
|
are unpacked to the following functions on top level
| reduce2Reduce0 | vwv vww x y True | = x `quot` reduce2D vwv vww :% (y `quot` reduce2D vwv vww) |
| reduce2Reduce1 | vwv vww x y True | = error [] |
| reduce2Reduce1 | vwv vww x y False | = reduce2Reduce0 vwv vww x y otherwise |
| reduce2D | vwv vww | = gcd vwv vww |
The bindings of the following Let/Where expression
| gcd' (abs x) (abs y) |
| where |
| gcd' | x zx | = gcd'2 x zx |
| gcd' | x y | = gcd'0 x y |
|
|
| gcd'0 | x y | = gcd' y (x `rem` y) |
|
|
| gcd'1 | True x zx | = x |
| gcd'1 | zy zz vuu | = gcd'0 zz vuu |
|
|
| gcd'2 | x zx | = gcd'1 (zx == 0) x zx |
| gcd'2 | vuv vuw | = gcd'0 vuv vuw |
|
are unpacked to the following functions on top level
| gcd0Gcd'0 | x y | = gcd0Gcd' y (x `rem` y) |
| gcd0Gcd'1 | True x zx | = x |
| gcd0Gcd'1 | zy zz vuu | = gcd0Gcd'0 zz vuu |
| gcd0Gcd'2 | x zx | = gcd0Gcd'1 (zx == 0) x zx |
| gcd0Gcd'2 | vuv vuw | = gcd0Gcd'0 vuv vuw |
| gcd0Gcd' | x zx | = gcd0Gcd'2 x zx |
| gcd0Gcd' | x y | = gcd0Gcd'0 x y |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
mainModule Main
|
| ((compare :: (Ord a, Ord b) => Either a b -> Either a b -> Ordering) :: (Ord a, Ord b) => Either a b -> Either a b -> Ordering) |
module Main where
Num Reduction:All numbers are transformed to thier corresponding representation with Succ, Pred and Zero.
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
|
| (compare :: (Ord a, Ord b) => Either a b -> Either a b -> Ordering) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ 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_esEs3(Right(vwx300), Right(vwx400), bda, app(app(ty_@2, bdg), bdh)) → new_esEs2(vwx300, vwx400, bdg, bdh)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_[], fc), cb, df) → new_esEs1(vwx300, vwx400, fc)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(app(ty_Either, dc), dd)) → new_esEs3(vwx302, vwx402, dc, dd)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(app(ty_@2, baa), bab)) → new_esEs2(vwx301, vwx401, baa, bab)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(app(ty_@2, ec), ed), df) → new_esEs2(vwx301, vwx401, ec, ed)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(ty_Maybe, hd)) → new_esEs(vwx301, vwx401, hd)
new_esEs(Just(vwx300), Just(vwx400), app(app(app(ty_@3, ba), bb), bc)) → new_esEs0(vwx300, vwx400, ba, bb, bc)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_Maybe, bae), baf) → new_esEs(vwx300, vwx400, bae)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(ty_[], eb), df) → new_esEs1(vwx301, vwx401, eb)
new_esEs3(Right(vwx300), Right(vwx400), bda, app(app(ty_Either, bea), beb)) → new_esEs3(vwx300, vwx400, bea, beb)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), ga) → new_esEs1(vwx301, vwx401, ga)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_@2, bbc), bbd), baf) → new_esEs2(vwx300, vwx400, bbc, bbd)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(ty_[], gf)) → new_esEs1(vwx300, vwx400, gf)
new_esEs(Just(vwx300), Just(vwx400), app(ty_Maybe, h)) → new_esEs(vwx300, vwx400, h)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(app(app(ty_@3, dg), dh), ea), df) → new_esEs0(vwx301, vwx401, dg, dh, ea)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_@2, fd), ff), cb, df) → new_esEs2(vwx300, vwx400, fd, ff)
new_esEs3(Right(vwx300), Right(vwx400), bda, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs0(vwx300, vwx400, bdc, bdd, bde)
new_esEs3(Left(vwx300), Left(vwx400), app(app(ty_Either, bcg), bch), bbh) → new_esEs3(vwx300, vwx400, bcg, bch)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_[], bbb), baf) → new_esEs1(vwx300, vwx400, bbb)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(ty_[], cg)) → new_esEs1(vwx302, vwx402, cg)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_Either, ha), hb)) → new_esEs3(vwx300, vwx400, ha, hb)
new_esEs3(Left(vwx300), Left(vwx400), app(app(app(ty_@3, bca), bcb), bcc), bbh) → new_esEs0(vwx300, vwx400, bca, bcb, bcc)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(app(ty_@2, da), db)) → new_esEs2(vwx302, vwx402, da, db)
new_esEs(Just(vwx300), Just(vwx400), app(app(ty_@2, be), bf)) → new_esEs2(vwx300, vwx400, be, bf)
new_esEs3(Left(vwx300), Left(vwx400), app(app(ty_@2, bce), bcf), bbh) → new_esEs2(vwx300, vwx400, bce, bcf)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(app(app(ty_@3, he), hf), hg)) → new_esEs0(vwx301, vwx401, he, hf, hg)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(app(app(ty_@3, cd), ce), cf)) → new_esEs0(vwx302, vwx402, cd, ce, cf)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(app(ty_Either, bac), bad)) → new_esEs3(vwx301, vwx401, bac, bad)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(ty_Maybe, gb)) → new_esEs(vwx300, vwx400, gb)
new_esEs3(Right(vwx300), Right(vwx400), bda, app(ty_[], bdf)) → new_esEs1(vwx300, vwx400, bdf)
new_esEs(Just(vwx300), Just(vwx400), app(ty_[], bd)) → new_esEs1(vwx300, vwx400, bd)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_Either, fg), fh), cb, df) → new_esEs3(vwx300, vwx400, fg, fh)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(app(ty_@3, bag), bah), bba), baf) → new_esEs0(vwx300, vwx400, bag, bah, bba)
new_esEs(Just(vwx300), Just(vwx400), app(app(ty_Either, bg), bh)) → new_esEs3(vwx300, vwx400, bg, bh)
new_esEs3(Right(vwx300), Right(vwx400), bda, app(ty_Maybe, bdb)) → new_esEs(vwx300, vwx400, bdb)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(app(ty_@3, gc), gd), ge)) → new_esEs0(vwx300, vwx400, gc, gd, ge)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(ty_Maybe, de), df) → new_esEs(vwx301, vwx401, de)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_@2, gg), gh)) → new_esEs2(vwx300, vwx400, gg, gh)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(ty_[], hh)) → new_esEs1(vwx301, vwx401, hh)
new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_Either, bbe), bbf), baf) → new_esEs3(vwx300, vwx400, bbe, bbf)
new_esEs3(Left(vwx300), Left(vwx400), app(ty_[], bcd), bbh) → new_esEs1(vwx300, vwx400, bcd)
new_esEs3(Left(vwx300), Left(vwx400), app(ty_Maybe, bbg), bbh) → new_esEs(vwx300, vwx400, bbg)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(app(ty_Either, ee), ef), df) → new_esEs3(vwx301, vwx401, ee, ef)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(ty_Maybe, cc)) → new_esEs(vwx302, vwx402, cc)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(app(ty_@3, eh), fa), fb), cb, df) → new_esEs0(vwx300, vwx400, eh, fa, fb)
new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_Maybe, eg), cb, df) → new_esEs(vwx300, vwx400, eg)
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_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_Either, ha), hb)) → new_esEs3(vwx300, vwx400, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(app(ty_@3, gc), gd), ge)) → new_esEs0(vwx300, vwx400, gc, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_@2, gg), gh)) → new_esEs2(vwx300, vwx400, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(vwx300), Just(vwx400), app(app(ty_Either, bg), bh)) → new_esEs3(vwx300, vwx400, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(vwx300), Just(vwx400), app(app(app(ty_@3, ba), bb), bc)) → new_esEs0(vwx300, vwx400, ba, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Just(vwx300), Just(vwx400), app(app(ty_@2, be), bf)) → new_esEs2(vwx300, vwx400, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(ty_Maybe, gb)) → new_esEs(vwx300, vwx400, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(vwx300), Just(vwx400), app(ty_Maybe, h)) → new_esEs(vwx300, vwx400, h)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(vwx300), Just(vwx400), app(ty_[], bd)) → new_esEs1(vwx300, vwx400, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(app(ty_Either, bac), bad)) → new_esEs3(vwx301, vwx401, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_Either, bbe), bbf), baf) → new_esEs3(vwx300, vwx400, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(app(app(ty_@3, he), hf), hg)) → new_esEs0(vwx301, vwx401, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(app(ty_@3, bag), bah), bba), baf) → new_esEs0(vwx300, vwx400, bag, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(app(ty_@2, baa), bab)) → new_esEs2(vwx301, vwx401, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_@2, bbc), bbd), baf) → new_esEs2(vwx300, vwx400, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(ty_Maybe, hd)) → new_esEs(vwx301, vwx401, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_Maybe, bae), baf) → new_esEs(vwx300, vwx400, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_[], bbb), baf) → new_esEs1(vwx300, vwx400, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(vwx300, vwx301), @2(vwx400, vwx401), hc, app(ty_[], hh)) → new_esEs1(vwx301, vwx401, hh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Right(vwx300), Right(vwx400), bda, app(app(ty_Either, bea), beb)) → new_esEs3(vwx300, vwx400, bea, beb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(vwx300), Left(vwx400), app(app(ty_Either, bcg), bch), bbh) → new_esEs3(vwx300, vwx400, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(app(ty_Either, dc), dd)) → new_esEs3(vwx302, vwx402, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_Either, fg), fh), cb, df) → new_esEs3(vwx300, vwx400, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(app(ty_Either, ee), ef), df) → new_esEs3(vwx301, vwx401, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), ga) → new_esEs1(vwx301, vwx401, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(ty_[], gf)) → new_esEs1(vwx300, vwx400, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(vwx300), Right(vwx400), bda, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs0(vwx300, vwx400, bdc, bdd, bde)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(Left(vwx300), Left(vwx400), app(app(app(ty_@3, bca), bcb), bcc), bbh) → new_esEs0(vwx300, vwx400, bca, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(app(app(ty_@3, dg), dh), ea), df) → new_esEs0(vwx301, vwx401, dg, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(app(app(ty_@3, cd), ce), cf)) → new_esEs0(vwx302, vwx402, cd, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(app(ty_@3, eh), fa), fb), cb, df) → new_esEs0(vwx300, vwx400, eh, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Right(vwx300), Right(vwx400), bda, app(app(ty_@2, bdg), bdh)) → new_esEs2(vwx300, vwx400, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(vwx300), Left(vwx400), app(app(ty_@2, bce), bcf), bbh) → new_esEs2(vwx300, vwx400, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Right(vwx300), Right(vwx400), bda, app(ty_Maybe, bdb)) → new_esEs(vwx300, vwx400, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(vwx300), Left(vwx400), app(ty_Maybe, bbg), bbh) → new_esEs(vwx300, vwx400, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(vwx300), Right(vwx400), bda, app(ty_[], bdf)) → new_esEs1(vwx300, vwx400, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(vwx300), Left(vwx400), app(ty_[], bcd), bbh) → new_esEs1(vwx300, vwx400, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(app(ty_@2, ec), ed), df) → new_esEs2(vwx301, vwx401, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_@2, fd), ff), cb, df) → new_esEs2(vwx300, vwx400, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(app(ty_@2, da), db)) → new_esEs2(vwx302, vwx402, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(ty_Maybe, de), df) → new_esEs(vwx301, vwx401, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(ty_Maybe, cc)) → new_esEs(vwx302, vwx402, cc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_Maybe, eg), cb, df) → new_esEs(vwx300, vwx400, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_[], fc), cb, df) → new_esEs1(vwx300, vwx400, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, app(ty_[], eb), df) → new_esEs1(vwx301, vwx401, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), ca, cb, app(ty_[], cg)) → new_esEs1(vwx302, vwx402, cg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ 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_primMulNat(Succ(vwx30000), Succ(vwx40000)) → new_primMulNat(vwx30000, Succ(vwx40000))
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(vwx30000), Succ(vwx40000)) → new_primMulNat(vwx30000, Succ(vwx40000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(vwx5500), Succ(vwx400000)) → new_primPlusNat(vwx5500, vwx400000)
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(vwx5500), Succ(vwx400000)) → new_primPlusNat(vwx5500, vwx400000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ 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_primCmpNat(Succ(vwx9000), Succ(vwx10000)) → new_primCmpNat(vwx9000, vwx10000)
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_primCmpNat(Succ(vwx9000), Succ(vwx10000)) → new_primCmpNat(vwx9000, vwx10000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ 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_compare(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_primCompAux(vwx90, vwx100, new_compare1(vwx91, vwx101, eh), eh)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(app(ty_@2, ha), hb)) → new_ltEs1(vwx91, vwx101, ha, hb)
new_compare2(:(vwx90, vwx91), :(vwx100, vwx101), False, app(ty_[], eh), be) → new_compare(vwx91, vwx101, eh)
new_compare20(vwx90, vwx100, False, h, ba, bb) → new_ltEs(vwx90, vwx100, h, ba, bb)
new_ltEs2(Left(vwx90), Left(vwx100), app(app(ty_Either, bae), baf), baa) → new_ltEs2(vwx90, vwx100, bae, baf)
new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(ty_[], bbd)), be) → new_ltEs0(vwx90, vwx100, bbd)
new_lt2(vwx90, vwx100, ca, cb) → new_compare0(vwx90, vwx100, ca, cb)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(ty_[], eb)) → new_ltEs0(vwx92, vwx102, eb)
new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(app(ty_@2, bac), bad)), baa), be) → new_ltEs1(vwx90, vwx100, bac, bad)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(app(ty_Either, dd), de), bd) → new_lt2(vwx91, vwx101, dd, de)
new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(app(app(ty_@3, bcb), bcc), bcd)), be) → new_ltEs(vwx90, vwx100, bcb, bcc, bcd)
new_compare23(vwx16, vwx17, False, bef, app(app(ty_@2, bfc), bfd)) → new_ltEs1(vwx16, vwx17, bfc, bfd)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(app(ty_@2, ec), ed)) → new_ltEs1(vwx92, vwx102, ec, ed)
new_compare3(vwx90, vwx100, h, ba, bb) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(ty_Maybe, cc)), bc), bd), be) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(app(app(ty_@3, ce), cf), cg)), bd), be) → new_lt(vwx91, vwx101, ce, cf, cg)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(ty_[], bf)), bc), bd), be) → new_compare(vwx90, vwx100, bf)
new_primCompAux(vwx90, vwx100, vwx54, app(ty_[], bdf)) → new_compare(vwx90, vwx100, bdf)
new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(app(app(ty_@3, hf), hg), hh)), baa), be) → new_ltEs(vwx90, vwx100, hf, hg, hh)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(app(ty_Either, ee), ef)) → new_ltEs2(vwx92, vwx102, ee, ef)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(ty_Maybe, he)) → new_ltEs3(vwx91, vwx101, he)
new_lt0(vwx90, vwx100, bf) → new_compare(vwx90, vwx100, bf)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(app(ty_@2, ha), hb)), be) → new_ltEs1(vwx91, vwx101, ha, hb)
new_compare2(:(vwx90, vwx91), :(vwx100, vwx101), False, app(ty_[], eh), be) → new_primCompAux(vwx90, vwx100, new_compare1(vwx91, vwx101, eh), eh)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(ty_[], gh)), be) → new_ltEs0(vwx91, vwx101, gh)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(app(ty_Either, ee), ef)), be) → new_ltEs2(vwx92, vwx102, ee, ef)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(app(ty_Either, hc), hd)), be) → new_ltEs2(vwx91, vwx101, hc, hd)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(app(ty_Either, dd), de)), bd), be) → new_lt2(vwx91, vwx101, dd, de)
new_ltEs2(Left(vwx90), Left(vwx100), app(app(app(ty_@3, hf), hg), hh), baa) → new_ltEs(vwx90, vwx100, hf, hg, hh)
new_ltEs3(Just(vwx90), Just(vwx100), app(app(app(ty_@3, bcb), bcc), bcd)) → new_ltEs(vwx90, vwx100, bcb, bcc, bcd)
new_ltEs2(Right(vwx90), Right(vwx100), bah, app(ty_[], bbd)) → new_ltEs0(vwx90, vwx100, bbd)
new_compare5(vwx90, vwx100, cc) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(app(app(ty_@3, ge), gf), gg)) → new_ltEs(vwx91, vwx101, ge, gf, gg)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(ty_[], da)), bd), be) → new_lt0(vwx91, vwx101, da)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(ty_Maybe, df)), bd), be) → new_lt3(vwx91, vwx101, df)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(ty_[], da), bd) → new_lt0(vwx91, vwx101, da)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(app(ty_@2, db), dc), bd) → new_lt1(vwx91, vwx101, db, dc)
new_compare0(Left(vwx30), Left(vwx40), bed, bee) → new_compare2(vwx30, vwx40, new_esEs7(vwx30, vwx40, bed), bed, bee)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(app(app(ty_@3, ce), cf), cg), bd) → new_lt(vwx91, vwx101, ce, cf, cg)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(ty_Maybe, eg)) → new_ltEs3(vwx92, vwx102, eg)
new_ltEs3(Just(vwx90), Just(vwx100), app(ty_[], bce)) → new_ltEs0(vwx90, vwx100, bce)
new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(ty_Maybe, bag)), baa), be) → new_ltEs3(vwx90, vwx100, bag)
new_primCompAux(vwx90, vwx100, vwx54, app(app(app(ty_@3, bdc), bdd), bde)) → new_compare3(vwx90, vwx100, bdc, bdd, bde)
new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(app(ty_Either, bbg), bbh)), be) → new_ltEs2(vwx90, vwx100, bbg, bbh)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(app(ty_Either, ga), gb), fd) → new_lt2(vwx90, vwx100, ga, gb)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(ty_[], bf), bc, bd) → new_compare(vwx90, vwx100, bf)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(app(app(ty_@3, ge), gf), gg)), be) → new_ltEs(vwx91, vwx101, ge, gf, gg)
new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(ty_Maybe, bca)), be) → new_ltEs3(vwx90, vwx100, bca)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(app(app(ty_@3, dg), dh), ea)) → new_ltEs(vwx92, vwx102, dg, dh, ea)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(ty_Maybe, gc)), fd), be) → new_lt3(vwx90, vwx100, gc)
new_ltEs3(Just(vwx90), Just(vwx100), app(ty_Maybe, bdb)) → new_ltEs3(vwx90, vwx100, bdb)
new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(app(ty_@2, bcf), bcg)), be) → new_ltEs1(vwx90, vwx100, bcf, bcg)
new_ltEs2(Left(vwx90), Left(vwx100), app(ty_[], bab), baa) → new_ltEs0(vwx90, vwx100, bab)
new_ltEs0(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_compare(vwx91, vwx101, eh)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(ty_[], ff), fd) → new_lt0(vwx90, vwx100, ff)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(app(ty_Either, ga), gb)), fd), be) → new_lt2(vwx90, vwx100, ga, gb)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(app(ty_@2, fg), fh)), fd), be) → new_lt1(vwx90, vwx100, fg, fh)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(ty_Maybe, gc), fd) → new_lt3(vwx90, vwx100, gc)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(ty_[], eb)), be) → new_ltEs0(vwx92, vwx102, eb)
new_lt3(vwx90, vwx100, cc) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
new_ltEs2(Right(vwx90), Right(vwx100), bah, app(app(ty_@2, bbe), bbf)) → new_ltEs1(vwx90, vwx100, bbe, bbf)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(ty_[], ff)), fd), be) → new_lt0(vwx90, vwx100, ff)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(app(ty_Either, ca), cb)), bc), bd), be) → new_compare0(vwx90, vwx100, ca, cb)
new_primCompAux(vwx90, vwx100, vwx54, app(app(ty_Either, bea), beb)) → new_compare0(vwx90, vwx100, bea, beb)
new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(ty_[], bce)), be) → new_ltEs0(vwx90, vwx100, bce)
new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(app(ty_Either, bae), baf)), baa), be) → new_ltEs2(vwx90, vwx100, bae, baf)
new_ltEs2(Left(vwx90), Left(vwx100), app(ty_Maybe, bag), baa) → new_ltEs3(vwx90, vwx100, bag)
new_compare22(vwx90, vwx100, False, cc) → new_ltEs3(vwx90, vwx100, cc)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(app(app(ty_@3, dg), dh), ea)), be) → new_ltEs(vwx92, vwx102, dg, dh, ea)
new_ltEs3(Just(vwx90), Just(vwx100), app(app(ty_Either, bch), bda)) → new_ltEs2(vwx90, vwx100, bch, bda)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(app(app(ty_@3, fa), fb), fc)), fd), be) → new_lt(vwx90, vwx100, fa, fb, fc)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(app(ty_@2, db), dc)), bd), be) → new_lt1(vwx91, vwx101, db, dc)
new_ltEs3(Just(vwx90), Just(vwx100), app(app(ty_@2, bcf), bcg)) → new_ltEs1(vwx90, vwx100, bcf, bcg)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(app(ty_@2, ec), ed)), be) → new_ltEs1(vwx92, vwx102, ec, ed)
new_compare23(vwx16, vwx17, False, bef, app(app(ty_Either, bfe), bff)) → new_ltEs2(vwx16, vwx17, bfe, bff)
new_compare21(vwx90, vwx100, False, bg, bh) → new_ltEs1(vwx90, vwx100, bg, bh)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(ty_Maybe, cc), bc, bd) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
new_ltEs2(Right(vwx90), Right(vwx100), bah, app(app(app(ty_@3, bba), bbb), bbc)) → new_ltEs(vwx90, vwx100, bba, bbb, bbc)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(ty_[], gh)) → new_ltEs0(vwx91, vwx101, gh)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(ty_Maybe, eg)), be) → new_ltEs3(vwx92, vwx102, eg)
new_ltEs2(Right(vwx90), Right(vwx100), bah, app(app(ty_Either, bbg), bbh)) → new_ltEs2(vwx90, vwx100, bbg, bbh)
new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(app(ty_Either, bch), bda)), be) → new_ltEs2(vwx90, vwx100, bch, bda)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(app(ty_@2, fg), fh), fd) → new_lt1(vwx90, vwx100, fg, fh)
new_compare23(vwx16, vwx17, False, bef, app(ty_[], bfb)) → new_ltEs0(vwx16, vwx17, bfb)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(app(app(ty_@3, h), ba), bb)), bc), bd), be) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(app(app(ty_@3, bba), bbb), bbc)), be) → new_ltEs(vwx90, vwx100, bba, bbb, bbc)
new_compare(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_compare(vwx91, vwx101, eh)
new_ltEs0(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_primCompAux(vwx90, vwx100, new_compare1(vwx91, vwx101, eh), eh)
new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(ty_Maybe, bdb)), be) → new_ltEs3(vwx90, vwx100, bdb)
new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(app(ty_@2, bg), bh)), bc), bd), be) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
new_primCompAux(vwx90, vwx100, vwx54, app(app(ty_@2, bdg), bdh)) → new_compare4(vwx90, vwx100, bdg, bdh)
new_primCompAux(vwx90, vwx100, vwx54, app(ty_Maybe, bec)) → new_compare5(vwx90, vwx100, bec)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(app(app(ty_@3, fa), fb), fc), fd) → new_lt(vwx90, vwx100, fa, fb, fc)
new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(ty_[], bab)), baa), be) → new_ltEs0(vwx90, vwx100, bab)
new_compare23(vwx16, vwx17, False, bef, app(ty_Maybe, bfg)) → new_ltEs3(vwx16, vwx17, bfg)
new_lt1(vwx90, vwx100, bg, bh) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
new_ltEs2(Left(vwx90), Left(vwx100), app(app(ty_@2, bac), bad), baa) → new_ltEs1(vwx90, vwx100, bac, bad)
new_ltEs2(Right(vwx90), Right(vwx100), bah, app(ty_Maybe, bca)) → new_ltEs3(vwx90, vwx100, bca)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(ty_Maybe, df), bd) → new_lt3(vwx91, vwx101, df)
new_compare4(vwx90, vwx100, bg, bh) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(app(app(ty_@3, h), ba), bb), bc, bd) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(ty_Maybe, he)), be) → new_ltEs3(vwx91, vwx101, he)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(app(ty_@2, bg), bh), bc, bd) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
new_lt(vwx90, vwx100, h, ba, bb) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(app(ty_Either, ca), cb), bc, bd) → new_compare0(vwx90, vwx100, ca, cb)
new_compare0(Right(vwx30), Right(vwx40), bed, bee) → new_compare23(vwx30, vwx40, new_esEs8(vwx30, vwx40, bee), bed, bee)
new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(app(ty_@2, bbe), bbf)), be) → new_ltEs1(vwx90, vwx100, bbe, bbf)
new_compare23(vwx16, vwx17, False, bef, app(app(app(ty_@3, beg), beh), bfa)) → new_ltEs(vwx16, vwx17, beg, beh, bfa)
new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(app(ty_Either, hc), hd)) → new_ltEs2(vwx91, vwx101, hc, hd)
The TRS R consists of the following rules:
new_primCmpNat0(vwx900, Succ(vwx1000)) → new_primCmpNat2(vwx900, vwx1000)
new_esEs6(Just(vwx300), Just(vwx400), app(app(ty_@2, cfc), cfd)) → new_esEs5(vwx300, vwx400, cfc, cfd)
new_primCompAux0(vwx90, vwx100, vwx54, eh) → new_primCompAux00(vwx54, new_compare33(vwx90, vwx100, eh))
new_ltEs20(vwx16, vwx17, ty_Int) → new_ltEs9(vwx16, vwx17)
new_lt19(vwx90, vwx100, app(app(ty_Either, ca), cb)) → new_lt14(vwx90, vwx100, ca, cb)
new_lt6(vwx90, vwx100, app(app(app(ty_@3, fa), fb), fc)) → new_lt7(vwx90, vwx100, fa, fb, fc)
new_ltEs15(True, False) → False
new_esEs18(Right(vwx300), Right(vwx400), daf, app(ty_Ratio, dee)) → new_esEs19(vwx300, vwx400, dee)
new_esEs8(vwx30, vwx40, ty_Char) → new_esEs16(vwx30, vwx40)
new_esEs7(vwx30, vwx40, ty_Int) → new_esEs14(vwx30, vwx40)
new_esEs9(GT, LT) → False
new_esEs9(LT, GT) → False
new_esEs27(vwx301, vwx401, ty_Integer) → new_esEs20(vwx301, vwx401)
new_compare110(vwx23, vwx24, True, dcb, dcc) → LT
new_ltEs14(GT, GT) → True
new_ltEs8(vwx9, vwx10) → new_not(new_esEs9(new_compare6(vwx9, vwx10), GT))
new_compare10(vwx90, vwx100, True, bg, bh) → LT
new_compare33(vwx90, vwx100, ty_@0) → new_compare19(vwx90, vwx100)
new_esEs8(vwx30, vwx40, app(ty_Ratio, dah)) → new_esEs19(vwx30, vwx40, dah)
new_lt19(vwx90, vwx100, ty_Integer) → new_lt5(vwx90, vwx100)
new_esEs28(vwx300, vwx400, ty_Char) → new_esEs16(vwx300, vwx400)
new_lt19(vwx90, vwx100, app(app(ty_@2, bg), bh)) → new_lt10(vwx90, vwx100, bg, bh)
new_lt20(vwx91, vwx101, app(app(ty_Either, dd), de)) → new_lt14(vwx91, vwx101, dd, de)
new_ltEs16(Just(vwx90), Just(vwx100), ty_Char) → new_ltEs11(vwx90, vwx100)
new_ltEs20(vwx16, vwx17, app(ty_[], bfb)) → new_ltEs7(vwx16, vwx17, bfb)
new_esEs28(vwx300, vwx400, ty_Int) → new_esEs14(vwx300, vwx400)
new_ltEs16(Just(vwx90), Just(vwx100), ty_Ordering) → new_ltEs14(vwx90, vwx100)
new_esEs22(vwx302, vwx402, ty_Ordering) → new_esEs9(vwx302, vwx402)
new_esEs21(vwx300, vwx400, ty_Int) → new_esEs14(vwx300, vwx400)
new_esEs26(vwx90, vwx100, ty_Integer) → new_esEs20(vwx90, vwx100)
new_esEs26(vwx90, vwx100, ty_Float) → new_esEs13(vwx90, vwx100)
new_esEs21(vwx300, vwx400, ty_@0) → new_esEs17(vwx300, vwx400)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(vwx301, vwx401, app(ty_Ratio, cga)) → new_esEs19(vwx301, vwx401, cga)
new_lt16(vwx90, vwx100) → new_esEs9(new_compare17(vwx90, vwx100), LT)
new_lt20(vwx91, vwx101, ty_Float) → new_lt4(vwx91, vwx101)
new_lt20(vwx91, vwx101, app(ty_[], da)) → new_lt8(vwx91, vwx101, da)
new_esEs27(vwx301, vwx401, app(app(app(ty_@3, cgc), cgd), cge)) → new_esEs4(vwx301, vwx401, cgc, cgd, cge)
new_ltEs5(vwx91, vwx101, app(ty_Maybe, he)) → new_ltEs16(vwx91, vwx101, he)
new_compare31(vwx9, vwx10) → new_primCmpInt(vwx9, vwx10)
new_esEs8(vwx30, vwx40, ty_Int) → new_esEs14(vwx30, vwx40)
new_esEs18(Left(vwx300), Left(vwx400), ty_Int, dag) → new_esEs14(vwx300, vwx400)
new_lt7(vwx90, vwx100, h, ba, bb) → new_esEs9(new_compare30(vwx90, vwx100, h, ba, bb), LT)
new_esEs20(Integer(vwx300), Integer(vwx400)) → new_primEqInt(vwx300, vwx400)
new_ltEs21(vwx9, vwx10, ty_Float) → new_ltEs8(vwx9, vwx10)
new_esEs22(vwx302, vwx402, ty_@0) → new_esEs17(vwx302, vwx402)
new_lt13(vwx90, vwx100) → new_esEs9(new_compare19(vwx90, vwx100), LT)
new_esEs7(vwx30, vwx40, ty_Float) → new_esEs13(vwx30, vwx40)
new_compare1([], :(vwx100, vwx101), eh) → LT
new_ltEs16(Just(vwx90), Just(vwx100), ty_Int) → new_ltEs9(vwx90, vwx100)
new_esEs12([], [], bgf) → True
new_esEs22(vwx302, vwx402, ty_Bool) → new_esEs10(vwx302, vwx402)
new_lt6(vwx90, vwx100, ty_Char) → new_lt12(vwx90, vwx100)
new_esEs22(vwx302, vwx402, app(ty_Ratio, cad)) → new_esEs19(vwx302, vwx402, cad)
new_lt6(vwx90, vwx100, ty_@0) → new_lt13(vwx90, vwx100)
new_esEs6(Just(vwx300), Just(vwx400), ty_Char) → new_esEs16(vwx300, vwx400)
new_ltEs13(Right(vwx90), Right(vwx100), bah, app(ty_Maybe, bca)) → new_ltEs16(vwx90, vwx100, bca)
new_esEs22(vwx302, vwx402, app(app(ty_@2, cbb), cbc)) → new_esEs5(vwx302, vwx402, cbb, cbc)
new_esEs22(vwx302, vwx402, app(ty_Maybe, cae)) → new_esEs6(vwx302, vwx402, cae)
new_esEs24(vwx300, vwx400, app(app(ty_@2, cdf), cdg)) → new_esEs5(vwx300, vwx400, cdf, cdg)
new_esEs8(vwx30, vwx40, app(app(ty_Either, dbh), dca)) → new_esEs18(vwx30, vwx40, dbh, dca)
new_esEs27(vwx301, vwx401, ty_Bool) → new_esEs10(vwx301, vwx401)
new_esEs27(vwx301, vwx401, app(ty_Maybe, cgb)) → new_esEs6(vwx301, vwx401, cgb)
new_esEs8(vwx30, vwx40, app(app(app(ty_@3, dbb), dbc), dbd)) → new_esEs4(vwx30, vwx40, dbb, dbc, dbd)
new_esEs25(vwx91, vwx101, ty_Double) → new_esEs15(vwx91, vwx101)
new_compare33(vwx90, vwx100, ty_Char) → new_compare8(vwx90, vwx100)
new_ltEs21(vwx9, vwx10, app(app(ty_@2, gd), fd)) → new_ltEs4(vwx9, vwx10, gd, fd)
new_esEs24(vwx300, vwx400, ty_@0) → new_esEs17(vwx300, vwx400)
new_compare6(Float(vwx90, vwx91), Float(vwx100, vwx101)) → new_compare31(new_sr(vwx90, vwx100), new_sr(vwx91, vwx101))
new_esEs18(Right(vwx300), Right(vwx400), daf, app(ty_[], dfb)) → new_esEs12(vwx300, vwx400, dfb)
new_ltEs5(vwx91, vwx101, ty_Bool) → new_ltEs15(vwx91, vwx101)
new_lt20(vwx91, vwx101, ty_Ordering) → new_lt15(vwx91, vwx101)
new_compare211(vwx16, vwx17, False, bef, dch) → new_compare111(vwx16, vwx17, new_ltEs20(vwx16, vwx17, dch), bef, dch)
new_esEs19(:%(vwx300, vwx301), :%(vwx400, vwx401), dae) → new_asAs(new_esEs30(vwx300, vwx400, dae), new_esEs29(vwx301, vwx401, dae))
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_Integer) → new_esEs20(vwx300, vwx400)
new_esEs6(Just(vwx300), Just(vwx400), app(ty_[], cfb)) → new_esEs12(vwx300, vwx400, cfb)
new_esEs24(vwx300, vwx400, app(ty_[], cde)) → new_esEs12(vwx300, vwx400, cde)
new_esEs17(@0, @0) → True
new_ltEs20(vwx16, vwx17, app(app(ty_Either, bfe), bff)) → new_ltEs13(vwx16, vwx17, bfe, bff)
new_esEs25(vwx91, vwx101, ty_Float) → new_esEs13(vwx91, vwx101)
new_compare33(vwx90, vwx100, app(ty_Ratio, ddb)) → new_compare9(vwx90, vwx100, ddb)
new_pePe(False, vwx53) → vwx53
new_esEs26(vwx90, vwx100, ty_Bool) → new_esEs10(vwx90, vwx100)
new_esEs12(:(vwx300, vwx301), [], bgf) → False
new_esEs12([], :(vwx400, vwx401), bgf) → False
new_ltEs15(True, True) → True
new_esEs27(vwx301, vwx401, app(app(ty_Either, cha), chb)) → new_esEs18(vwx301, vwx401, cha, chb)
new_ltEs19(vwx92, vwx102, app(app(ty_@2, ec), ed)) → new_ltEs4(vwx92, vwx102, ec, ed)
new_lt12(vwx90, vwx100) → new_esEs9(new_compare8(vwx90, vwx100), LT)
new_ltEs14(GT, EQ) → False
new_esEs27(vwx301, vwx401, ty_Ordering) → new_esEs9(vwx301, vwx401)
new_lt19(vwx90, vwx100, app(ty_[], bf)) → new_lt8(vwx90, vwx100, bf)
new_esEs8(vwx30, vwx40, ty_@0) → new_esEs17(vwx30, vwx40)
new_ltEs15(False, True) → True
new_ltEs5(vwx91, vwx101, app(app(ty_@2, ha), hb)) → new_ltEs4(vwx91, vwx101, ha, hb)
new_esEs22(vwx302, vwx402, ty_Double) → new_esEs15(vwx302, vwx402)
new_ltEs5(vwx91, vwx101, ty_Float) → new_ltEs8(vwx91, vwx101)
new_compare30(vwx90, vwx100, h, ba, bb) → new_compare28(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
new_esEs21(vwx300, vwx400, app(ty_Ratio, bgg)) → new_esEs19(vwx300, vwx400, bgg)
new_esEs28(vwx300, vwx400, app(app(app(ty_@3, che), chf), chg)) → new_esEs4(vwx300, vwx400, che, chf, chg)
new_compare33(vwx90, vwx100, app(app(app(ty_@3, bdc), bdd), bde)) → new_compare30(vwx90, vwx100, bdc, bdd, bde)
new_esEs21(vwx300, vwx400, ty_Double) → new_esEs15(vwx300, vwx400)
new_ltEs21(vwx9, vwx10, ty_Int) → new_ltEs9(vwx9, vwx10)
new_ltEs13(Left(vwx90), Left(vwx100), ty_Int, baa) → new_ltEs9(vwx90, vwx100)
new_esEs9(GT, EQ) → False
new_esEs9(EQ, GT) → False
new_ltEs15(False, False) → True
new_compare26(vwx90, vwx100, False, cc) → new_compare12(vwx90, vwx100, new_ltEs16(vwx90, vwx100, cc), cc)
new_compare15(vwx90, vwx100, False, h, ba, bb) → GT
new_esEs22(vwx302, vwx402, ty_Integer) → new_esEs20(vwx302, vwx402)
new_ltEs20(vwx16, vwx17, app(app(ty_@2, bfc), bfd)) → new_ltEs4(vwx16, vwx17, bfc, bfd)
new_primCmpInt(Neg(Succ(vwx900)), Neg(vwx100)) → new_primCmpNat1(vwx100, vwx900)
new_esEs23(vwx301, vwx401, ty_Integer) → new_esEs20(vwx301, vwx401)
new_ltEs21(vwx9, vwx10, ty_Bool) → new_ltEs15(vwx9, vwx10)
new_ltEs13(Left(vwx90), Left(vwx100), ty_Double, baa) → new_ltEs10(vwx90, vwx100)
new_lt6(vwx90, vwx100, ty_Double) → new_lt11(vwx90, vwx100)
new_ltEs5(vwx91, vwx101, app(ty_[], gh)) → new_ltEs7(vwx91, vwx101, gh)
new_compare17(vwx90, vwx100) → new_compare25(vwx90, vwx100, new_esEs10(vwx90, vwx100))
new_compare29(Left(vwx30), Left(vwx40), bed, bee) → new_compare210(vwx30, vwx40, new_esEs7(vwx30, vwx40, bed), bed, bee)
new_ltEs16(Nothing, Nothing, bgd) → True
new_compare9(:%(vwx90, vwx91), :%(vwx100, vwx101), ty_Integer) → new_compare7(new_sr0(vwx90, vwx101), new_sr0(vwx100, vwx91))
new_esEs28(vwx300, vwx400, ty_Double) → new_esEs15(vwx300, vwx400)
new_ltEs10(vwx9, vwx10) → new_not(new_esEs9(new_compare16(vwx9, vwx10), GT))
new_ltEs21(vwx9, vwx10, ty_Ordering) → new_ltEs14(vwx9, vwx10)
new_esEs23(vwx301, vwx401, ty_Int) → new_esEs14(vwx301, vwx401)
new_ltEs13(Right(vwx90), Right(vwx100), bah, app(ty_Ratio, dcg)) → new_ltEs17(vwx90, vwx100, dcg)
new_pePe(True, vwx53) → True
new_primEqNat0(Zero, Zero) → True
new_ltEs19(vwx92, vwx102, ty_Integer) → new_ltEs18(vwx92, vwx102)
new_lt15(vwx90, vwx100) → new_esEs9(new_compare18(vwx90, vwx100), LT)
new_esEs26(vwx90, vwx100, app(ty_Maybe, cc)) → new_esEs6(vwx90, vwx100, cc)
new_ltEs21(vwx9, vwx10, app(ty_[], eh)) → new_ltEs7(vwx9, vwx10, eh)
new_compare111(vwx30, vwx31, False, dcd, dce) → GT
new_esEs18(Left(vwx300), Left(vwx400), app(app(ty_@2, dea), deb), dag) → new_esEs5(vwx300, vwx400, dea, deb)
new_lt6(vwx90, vwx100, app(ty_Ratio, bfh)) → new_lt18(vwx90, vwx100, bfh)
new_esEs29(vwx301, vwx401, ty_Int) → new_esEs14(vwx301, vwx401)
new_lt20(vwx91, vwx101, app(app(ty_@2, db), dc)) → new_lt10(vwx91, vwx101, db, dc)
new_ltEs11(vwx9, vwx10) → new_not(new_esEs9(new_compare8(vwx9, vwx10), GT))
new_ltEs13(Left(vwx90), Left(vwx100), app(ty_[], bab), baa) → new_ltEs7(vwx90, vwx100, bab)
new_esEs6(Just(vwx300), Just(vwx400), ty_Int) → new_esEs14(vwx300, vwx400)
new_ltEs20(vwx16, vwx17, ty_Float) → new_ltEs8(vwx16, vwx17)
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_Bool) → new_esEs10(vwx300, vwx400)
new_ltEs19(vwx92, vwx102, ty_Float) → new_ltEs8(vwx92, vwx102)
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_Float) → new_ltEs8(vwx90, vwx100)
new_esEs25(vwx91, vwx101, app(app(ty_Either, dd), de)) → new_esEs18(vwx91, vwx101, dd, de)
new_compare33(vwx90, vwx100, app(ty_Maybe, bec)) → new_compare14(vwx90, vwx100, bec)
new_esEs7(vwx30, vwx40, ty_Ordering) → new_esEs9(vwx30, vwx40)
new_ltEs16(Just(vwx90), Just(vwx100), ty_@0) → new_ltEs12(vwx90, vwx100)
new_lt6(vwx90, vwx100, ty_Int) → new_lt9(vwx90, vwx100)
new_lt6(vwx90, vwx100, ty_Integer) → new_lt5(vwx90, vwx100)
new_compare110(vwx23, vwx24, False, dcb, dcc) → GT
new_esEs11(vwx90, vwx100, ty_Char) → new_esEs16(vwx90, vwx100)
new_compare33(vwx90, vwx100, ty_Double) → new_compare16(vwx90, vwx100)
new_compare12(vwx90, vwx100, False, cc) → GT
new_esEs18(Left(vwx300), Right(vwx400), daf, dag) → False
new_esEs18(Right(vwx300), Left(vwx400), daf, dag) → False
new_ltEs14(EQ, LT) → False
new_sr(vwx300, vwx400) → new_primMulInt(vwx300, vwx400)
new_esEs6(Just(vwx300), Just(vwx400), ty_@0) → new_esEs17(vwx300, vwx400)
new_ltEs19(vwx92, vwx102, ty_@0) → new_ltEs12(vwx92, vwx102)
new_ltEs13(Left(vwx90), Left(vwx100), ty_Integer, baa) → new_ltEs18(vwx90, vwx100)
new_ltEs21(vwx9, vwx10, app(ty_Maybe, bgd)) → new_ltEs16(vwx9, vwx10, bgd)
new_ltEs7(vwx9, vwx10, eh) → new_not(new_esEs9(new_compare1(vwx9, vwx10, eh), GT))
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_Char) → new_esEs16(vwx300, vwx400)
new_primCmpInt(Neg(Zero), Neg(Succ(vwx1000))) → new_primCmpNat0(vwx1000, Zero)
new_esEs23(vwx301, vwx401, app(ty_Ratio, cbf)) → new_esEs19(vwx301, vwx401, cbf)
new_primPlusNat0(Succ(vwx550), vwx40000) → Succ(Succ(new_primPlusNat1(vwx550, vwx40000)))
new_primCmpInt(Pos(Zero), Pos(Succ(vwx1000))) → new_primCmpNat1(Zero, vwx1000)
new_esEs18(Left(vwx300), Left(vwx400), app(app(app(ty_@3, dde), ddf), ddg), dag) → new_esEs4(vwx300, vwx400, dde, ddf, ddg)
new_esEs7(vwx30, vwx40, ty_@0) → new_esEs17(vwx30, vwx40)
new_ltEs19(vwx92, vwx102, ty_Bool) → new_ltEs15(vwx92, vwx102)
new_esEs22(vwx302, vwx402, ty_Char) → new_esEs16(vwx302, vwx402)
new_esEs26(vwx90, vwx100, app(app(app(ty_@3, h), ba), bb)) → new_esEs4(vwx90, vwx100, h, ba, bb)
new_ltEs19(vwx92, vwx102, ty_Double) → new_ltEs10(vwx92, vwx102)
new_esEs21(vwx300, vwx400, ty_Ordering) → new_esEs9(vwx300, vwx400)
new_lt17(vwx90, vwx100, cc) → new_esEs9(new_compare14(vwx90, vwx100, cc), LT)
new_esEs18(Left(vwx300), Left(vwx400), ty_Double, dag) → new_esEs15(vwx300, vwx400)
new_esEs9(EQ, EQ) → True
new_lt10(vwx90, vwx100, bg, bh) → new_esEs9(new_compare32(vwx90, vwx100, bg, bh), LT)
new_esEs25(vwx91, vwx101, app(ty_[], da)) → new_esEs12(vwx91, vwx101, da)
new_esEs11(vwx90, vwx100, app(app(app(ty_@3, fa), fb), fc)) → new_esEs4(vwx90, vwx100, fa, fb, fc)
new_ltEs16(Nothing, Just(vwx100), bgd) → True
new_compare25(vwx90, vwx100, True) → EQ
new_primEqInt(Neg(Succ(vwx3000)), Neg(Succ(vwx4000))) → new_primEqNat0(vwx3000, vwx4000)
new_esEs8(vwx30, vwx40, app(app(ty_@2, dbf), dbg)) → new_esEs5(vwx30, vwx40, dbf, dbg)
new_esEs8(vwx30, vwx40, ty_Double) → new_esEs15(vwx30, vwx40)
new_primPlusNat1(Succ(vwx5500), Zero) → Succ(vwx5500)
new_primPlusNat1(Zero, Succ(vwx400000)) → Succ(vwx400000)
new_ltEs19(vwx92, vwx102, app(ty_Ratio, cec)) → new_ltEs17(vwx92, vwx102, cec)
new_compare13(vwx90, vwx100, False) → GT
new_esEs24(vwx300, vwx400, ty_Integer) → new_esEs20(vwx300, vwx400)
new_esEs28(vwx300, vwx400, ty_@0) → new_esEs17(vwx300, vwx400)
new_primCmpNat1(Zero, vwx900) → LT
new_esEs18(Right(vwx300), Right(vwx400), daf, app(ty_Maybe, def)) → new_esEs6(vwx300, vwx400, def)
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_Int) → new_ltEs9(vwx90, vwx100)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_ltEs16(Just(vwx90), Just(vwx100), app(ty_Maybe, bdb)) → new_ltEs16(vwx90, vwx100, bdb)
new_esEs24(vwx300, vwx400, ty_Bool) → new_esEs10(vwx300, vwx400)
new_ltEs20(vwx16, vwx17, ty_@0) → new_ltEs12(vwx16, vwx17)
new_ltEs20(vwx16, vwx17, app(ty_Ratio, dda)) → new_ltEs17(vwx16, vwx17, dda)
new_esEs6(Just(vwx300), Just(vwx400), ty_Float) → new_esEs13(vwx300, vwx400)
new_ltEs21(vwx9, vwx10, app(app(ty_Either, bah), baa)) → new_ltEs13(vwx9, vwx10, bah, baa)
new_primEqInt(Neg(Zero), Neg(Succ(vwx4000))) → False
new_primEqInt(Neg(Succ(vwx3000)), Neg(Zero)) → False
new_lt19(vwx90, vwx100, ty_Char) → new_lt12(vwx90, vwx100)
new_esEs25(vwx91, vwx101, ty_Ordering) → new_esEs9(vwx91, vwx101)
new_ltEs16(Just(vwx90), Just(vwx100), ty_Float) → new_ltEs8(vwx90, vwx100)
new_esEs16(Char(vwx300), Char(vwx400)) → new_primEqInt(vwx300, vwx400)
new_esEs22(vwx302, vwx402, ty_Float) → new_esEs13(vwx302, vwx402)
new_esEs23(vwx301, vwx401, app(app(app(ty_@3, cbh), cca), ccb)) → new_esEs4(vwx301, vwx401, cbh, cca, ccb)
new_compare24(vwx90, vwx100, True, bg, bh) → EQ
new_esEs5(@2(vwx300, vwx301), @2(vwx400, vwx401), cfg, cfh) → new_asAs(new_esEs28(vwx300, vwx400, cfg), new_esEs27(vwx301, vwx401, cfh))
new_esEs25(vwx91, vwx101, app(ty_Ratio, ceb)) → new_esEs19(vwx91, vwx101, ceb)
new_esEs10(False, False) → True
new_esEs7(vwx30, vwx40, app(app(app(ty_@3, caa), cab), cac)) → new_esEs4(vwx30, vwx40, caa, cab, cac)
new_esEs11(vwx90, vwx100, ty_Int) → new_esEs14(vwx90, vwx100)
new_esEs25(vwx91, vwx101, ty_Char) → new_esEs16(vwx91, vwx101)
new_lt9(vwx90, vwx100) → new_esEs9(new_compare31(vwx90, vwx100), LT)
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_Double) → new_ltEs10(vwx90, vwx100)
new_ltEs19(vwx92, vwx102, app(ty_Maybe, eg)) → new_ltEs16(vwx92, vwx102, eg)
new_ltEs5(vwx91, vwx101, app(ty_Ratio, bga)) → new_ltEs17(vwx91, vwx101, bga)
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_Double) → new_esEs15(vwx300, vwx400)
new_ltEs16(Just(vwx90), Just(vwx100), ty_Double) → new_ltEs10(vwx90, vwx100)
new_esEs25(vwx91, vwx101, ty_@0) → new_esEs17(vwx91, vwx101)
new_esEs23(vwx301, vwx401, ty_Char) → new_esEs16(vwx301, vwx401)
new_lt6(vwx90, vwx100, app(ty_[], ff)) → new_lt8(vwx90, vwx100, ff)
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_Ordering) → new_esEs9(vwx300, vwx400)
new_esEs6(Nothing, Nothing, ced) → True
new_ltEs20(vwx16, vwx17, app(ty_Maybe, bfg)) → new_ltEs16(vwx16, vwx17, bfg)
new_primEqInt(Pos(Succ(vwx3000)), Pos(Succ(vwx4000))) → new_primEqNat0(vwx3000, vwx4000)
new_esEs18(Left(vwx300), Left(vwx400), ty_Float, dag) → new_esEs13(vwx300, vwx400)
new_compare10(vwx90, vwx100, False, bg, bh) → GT
new_esEs21(vwx300, vwx400, app(ty_Maybe, bgh)) → new_esEs6(vwx300, vwx400, bgh)
new_esEs30(vwx300, vwx400, ty_Integer) → new_esEs20(vwx300, vwx400)
new_esEs23(vwx301, vwx401, app(ty_[], ccc)) → new_esEs12(vwx301, vwx401, ccc)
new_esEs6(Just(vwx300), Nothing, ced) → False
new_esEs6(Nothing, Just(vwx400), ced) → False
new_primEqNat0(Succ(vwx30000), Succ(vwx40000)) → new_primEqNat0(vwx30000, vwx40000)
new_lt19(vwx90, vwx100, ty_@0) → new_lt13(vwx90, vwx100)
new_ltEs16(Just(vwx90), Just(vwx100), app(ty_[], bce)) → new_ltEs7(vwx90, vwx100, bce)
new_ltEs19(vwx92, vwx102, app(app(ty_Either, ee), ef)) → new_ltEs13(vwx92, vwx102, ee, ef)
new_ltEs9(vwx9, vwx10) → new_not(new_esEs9(new_compare31(vwx9, vwx10), GT))
new_esEs27(vwx301, vwx401, ty_Char) → new_esEs16(vwx301, vwx401)
new_compare9(:%(vwx90, vwx91), :%(vwx100, vwx101), ty_Int) → new_compare31(new_sr(vwx90, vwx101), new_sr(vwx100, vwx91))
new_esEs8(vwx30, vwx40, ty_Integer) → new_esEs20(vwx30, vwx40)
new_esEs30(vwx300, vwx400, ty_Int) → new_esEs14(vwx300, vwx400)
new_primCompAux00(vwx64, LT) → LT
new_lt8(vwx90, vwx100, bf) → new_esEs9(new_compare1(vwx90, vwx100, bf), LT)
new_compare25(vwx90, vwx100, False) → new_compare11(vwx90, vwx100, new_ltEs15(vwx90, vwx100))
new_esEs23(vwx301, vwx401, ty_Double) → new_esEs15(vwx301, vwx401)
new_compare29(Left(vwx30), Right(vwx40), bed, bee) → LT
new_ltEs13(Left(vwx90), Left(vwx100), ty_@0, baa) → new_ltEs12(vwx90, vwx100)
new_ltEs20(vwx16, vwx17, ty_Ordering) → new_ltEs14(vwx16, vwx17)
new_compare24(vwx90, vwx100, False, bg, bh) → new_compare10(vwx90, vwx100, new_ltEs4(vwx90, vwx100, bg, bh), bg, bh)
new_compare33(vwx90, vwx100, ty_Int) → new_compare31(vwx90, vwx100)
new_compare1(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_primCompAux0(vwx90, vwx100, new_compare1(vwx91, vwx101, eh), eh)
new_compare18(vwx90, vwx100) → new_compare27(vwx90, vwx100, new_esEs9(vwx90, vwx100))
new_esEs25(vwx91, vwx101, ty_Integer) → new_esEs20(vwx91, vwx101)
new_primEqInt(Pos(Zero), Pos(Succ(vwx4000))) → False
new_primEqInt(Pos(Succ(vwx3000)), Pos(Zero)) → False
new_ltEs16(Just(vwx90), Just(vwx100), app(ty_Ratio, bge)) → new_ltEs17(vwx90, vwx100, bge)
new_compare19(@0, @0) → EQ
new_ltEs5(vwx91, vwx101, app(app(ty_Either, hc), hd)) → new_ltEs13(vwx91, vwx101, hc, hd)
new_esEs23(vwx301, vwx401, ty_@0) → new_esEs17(vwx301, vwx401)
new_esEs24(vwx300, vwx400, app(ty_Ratio, cch)) → new_esEs19(vwx300, vwx400, cch)
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_Char) → new_ltEs11(vwx90, vwx100)
new_esEs28(vwx300, vwx400, ty_Integer) → new_esEs20(vwx300, vwx400)
new_esEs23(vwx301, vwx401, app(app(ty_@2, ccd), cce)) → new_esEs5(vwx301, vwx401, ccd, cce)
new_ltEs21(vwx9, vwx10, app(ty_Ratio, bgc)) → new_ltEs17(vwx9, vwx10, bgc)
new_primCmpInt(Neg(Zero), Pos(Succ(vwx1000))) → LT
new_lt19(vwx90, vwx100, ty_Ordering) → new_lt15(vwx90, vwx100)
new_esEs21(vwx300, vwx400, ty_Char) → new_esEs16(vwx300, vwx400)
new_ltEs21(vwx9, vwx10, app(app(app(ty_@3, cd), bc), bd)) → new_ltEs6(vwx9, vwx10, cd, bc, bd)
new_ltEs13(Right(vwx90), Right(vwx100), bah, app(ty_[], bbd)) → new_ltEs7(vwx90, vwx100, bbd)
new_esEs23(vwx301, vwx401, ty_Float) → new_esEs13(vwx301, vwx401)
new_esEs28(vwx300, vwx400, app(ty_Ratio, chc)) → new_esEs19(vwx300, vwx400, chc)
new_compare13(vwx90, vwx100, True) → LT
new_sr0(Integer(vwx1000), Integer(vwx910)) → Integer(new_primMulInt(vwx1000, vwx910))
new_primPlusNat1(Succ(vwx5500), Succ(vwx400000)) → Succ(Succ(new_primPlusNat1(vwx5500, vwx400000)))
new_compare12(vwx90, vwx100, True, cc) → LT
new_primEqInt(Neg(Succ(vwx3000)), Pos(vwx400)) → False
new_primEqInt(Pos(Succ(vwx3000)), Neg(vwx400)) → False
new_esEs13(Float(vwx300, vwx301), Float(vwx400, vwx401)) → new_esEs14(new_sr(vwx300, vwx400), new_sr(vwx301, vwx401))
new_ltEs6(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, bd) → new_pePe(new_lt19(vwx90, vwx100, cd), new_asAs(new_esEs26(vwx90, vwx100, cd), new_pePe(new_lt20(vwx91, vwx101, bc), new_asAs(new_esEs25(vwx91, vwx101, bc), new_ltEs19(vwx92, vwx102, bd)))))
new_ltEs16(Just(vwx90), Just(vwx100), ty_Integer) → new_ltEs18(vwx90, vwx100)
new_esEs24(vwx300, vwx400, ty_Int) → new_esEs14(vwx300, vwx400)
new_esEs7(vwx30, vwx40, app(ty_Ratio, dae)) → new_esEs19(vwx30, vwx40, dae)
new_ltEs20(vwx16, vwx17, ty_Double) → new_ltEs10(vwx16, vwx17)
new_esEs18(Left(vwx300), Left(vwx400), app(app(ty_Either, dec), ded), dag) → new_esEs18(vwx300, vwx400, dec, ded)
new_primCmpNat2(Zero, Succ(vwx10000)) → LT
new_esEs28(vwx300, vwx400, app(ty_Maybe, chd)) → new_esEs6(vwx300, vwx400, chd)
new_ltEs20(vwx16, vwx17, ty_Integer) → new_ltEs18(vwx16, vwx17)
new_esEs24(vwx300, vwx400, app(app(ty_Either, cdh), cea)) → new_esEs18(vwx300, vwx400, cdh, cea)
new_primEqInt(Neg(Zero), Pos(Succ(vwx4000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vwx4000))) → False
new_compare33(vwx90, vwx100, ty_Integer) → new_compare7(vwx90, vwx100)
new_primCompAux00(vwx64, EQ) → vwx64
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_@0) → new_esEs17(vwx300, vwx400)
new_ltEs13(Left(vwx90), Left(vwx100), app(ty_Ratio, dcf), baa) → new_ltEs17(vwx90, vwx100, dcf)
new_lt6(vwx90, vwx100, app(app(ty_Either, ga), gb)) → new_lt14(vwx90, vwx100, ga, gb)
new_lt6(vwx90, vwx100, ty_Bool) → new_lt16(vwx90, vwx100)
new_esEs26(vwx90, vwx100, app(app(ty_@2, bg), bh)) → new_esEs5(vwx90, vwx100, bg, bh)
new_esEs6(Just(vwx300), Just(vwx400), ty_Bool) → new_esEs10(vwx300, vwx400)
new_esEs25(vwx91, vwx101, ty_Bool) → new_esEs10(vwx91, vwx101)
new_ltEs16(Just(vwx90), Nothing, bgd) → False
new_compare26(vwx90, vwx100, True, cc) → EQ
new_esEs22(vwx302, vwx402, app(app(ty_Either, cbd), cbe)) → new_esEs18(vwx302, vwx402, cbd, cbe)
new_esEs21(vwx300, vwx400, app(app(ty_@2, bhe), bhf)) → new_esEs5(vwx300, vwx400, bhe, bhf)
new_lt11(vwx90, vwx100) → new_esEs9(new_compare16(vwx90, vwx100), LT)
new_ltEs20(vwx16, vwx17, app(app(app(ty_@3, beg), beh), bfa)) → new_ltEs6(vwx16, vwx17, beg, beh, bfa)
new_not(False) → True
new_lt6(vwx90, vwx100, ty_Ordering) → new_lt15(vwx90, vwx100)
new_compare33(vwx90, vwx100, app(app(ty_@2, bdg), bdh)) → new_compare32(vwx90, vwx100, bdg, bdh)
new_ltEs13(Right(vwx90), Right(vwx100), bah, app(app(app(ty_@3, bba), bbb), bbc)) → new_ltEs6(vwx90, vwx100, bba, bbb, bbc)
new_esEs11(vwx90, vwx100, app(ty_Maybe, gc)) → new_esEs6(vwx90, vwx100, gc)
new_esEs8(vwx30, vwx40, app(ty_Maybe, dba)) → new_esEs6(vwx30, vwx40, dba)
new_primPlusNat0(Zero, vwx40000) → Succ(vwx40000)
new_esEs18(Left(vwx300), Left(vwx400), ty_Char, dag) → new_esEs16(vwx300, vwx400)
new_compare210(vwx9, vwx10, True, dfg, be) → EQ
new_esEs11(vwx90, vwx100, ty_Ordering) → new_esEs9(vwx90, vwx100)
new_esEs7(vwx30, vwx40, ty_Char) → new_esEs16(vwx30, vwx40)
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_Ordering) → new_ltEs14(vwx90, vwx100)
new_esEs9(GT, GT) → True
new_esEs6(Just(vwx300), Just(vwx400), ty_Ordering) → new_esEs9(vwx300, vwx400)
new_ltEs20(vwx16, vwx17, ty_Char) → new_ltEs11(vwx16, vwx17)
new_compare32(vwx90, vwx100, bg, bh) → new_compare24(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
new_esEs7(vwx30, vwx40, app(app(ty_@2, cfg), cfh)) → new_esEs5(vwx30, vwx40, cfg, cfh)
new_ltEs14(LT, LT) → True
new_esEs25(vwx91, vwx101, app(app(app(ty_@3, ce), cf), cg)) → new_esEs4(vwx91, vwx101, ce, cf, cg)
new_esEs28(vwx300, vwx400, app(app(ty_@2, daa), dab)) → new_esEs5(vwx300, vwx400, daa, dab)
new_lt20(vwx91, vwx101, app(ty_Maybe, df)) → new_lt17(vwx91, vwx101, df)
new_ltEs19(vwx92, vwx102, app(app(app(ty_@3, dg), dh), ea)) → new_ltEs6(vwx92, vwx102, dg, dh, ea)
new_esEs11(vwx90, vwx100, ty_Double) → new_esEs15(vwx90, vwx100)
new_lt20(vwx91, vwx101, app(app(app(ty_@3, ce), cf), cg)) → new_lt7(vwx91, vwx101, ce, cf, cg)
new_esEs22(vwx302, vwx402, app(app(app(ty_@3, caf), cag), cah)) → new_esEs4(vwx302, vwx402, caf, cag, cah)
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_Integer) → new_ltEs18(vwx90, vwx100)
new_lt19(vwx90, vwx100, app(ty_Ratio, bgb)) → new_lt18(vwx90, vwx100, bgb)
new_esEs6(Just(vwx300), Just(vwx400), app(app(ty_Either, cfe), cff)) → new_esEs18(vwx300, vwx400, cfe, cff)
new_esEs28(vwx300, vwx400, ty_Ordering) → new_esEs9(vwx300, vwx400)
new_ltEs13(Left(vwx90), Left(vwx100), app(ty_Maybe, bag), baa) → new_ltEs16(vwx90, vwx100, bag)
new_esEs7(vwx30, vwx40, ty_Integer) → new_esEs20(vwx30, vwx40)
new_primCmpInt(Pos(Succ(vwx900)), Neg(vwx100)) → GT
new_ltEs19(vwx92, vwx102, ty_Int) → new_ltEs9(vwx92, vwx102)
new_esEs7(vwx30, vwx40, app(app(ty_Either, daf), dag)) → new_esEs18(vwx30, vwx40, daf, dag)
new_esEs26(vwx90, vwx100, ty_@0) → new_esEs17(vwx90, vwx100)
new_esEs24(vwx300, vwx400, ty_Double) → new_esEs15(vwx300, vwx400)
new_ltEs13(Left(vwx90), Left(vwx100), app(app(ty_@2, bac), bad), baa) → new_ltEs4(vwx90, vwx100, bac, bad)
new_primMulInt(Pos(vwx3000), Pos(vwx4000)) → Pos(new_primMulNat0(vwx3000, vwx4000))
new_ltEs5(vwx91, vwx101, ty_Ordering) → new_ltEs14(vwx91, vwx101)
new_esEs10(True, True) → True
new_esEs27(vwx301, vwx401, ty_Double) → new_esEs15(vwx301, vwx401)
new_esEs23(vwx301, vwx401, ty_Ordering) → new_esEs9(vwx301, vwx401)
new_primMulInt(Neg(vwx3000), Neg(vwx4000)) → Pos(new_primMulNat0(vwx3000, vwx4000))
new_primCmpNat2(Zero, Zero) → EQ
new_compare8(Char(vwx90), Char(vwx100)) → new_primCmpInt(vwx90, vwx100)
new_ltEs5(vwx91, vwx101, app(app(app(ty_@3, ge), gf), gg)) → new_ltEs6(vwx91, vwx101, ge, gf, gg)
new_esEs11(vwx90, vwx100, ty_Integer) → new_esEs20(vwx90, vwx100)
new_esEs8(vwx30, vwx40, app(ty_[], dbe)) → new_esEs12(vwx30, vwx40, dbe)
new_primEqNat0(Succ(vwx30000), Zero) → False
new_primEqNat0(Zero, Succ(vwx40000)) → False
new_esEs24(vwx300, vwx400, ty_Char) → new_esEs16(vwx300, vwx400)
new_esEs6(Just(vwx300), Just(vwx400), app(ty_Ratio, cee)) → new_esEs19(vwx300, vwx400, cee)
new_esEs21(vwx300, vwx400, app(ty_[], bhd)) → new_esEs12(vwx300, vwx400, bhd)
new_esEs25(vwx91, vwx101, app(ty_Maybe, df)) → new_esEs6(vwx91, vwx101, df)
new_esEs18(Left(vwx300), Left(vwx400), ty_Bool, dag) → new_esEs10(vwx300, vwx400)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_ltEs16(Just(vwx90), Just(vwx100), app(app(app(ty_@3, bcb), bcc), bcd)) → new_ltEs6(vwx90, vwx100, bcb, bcc, bcd)
new_lt19(vwx90, vwx100, app(ty_Maybe, cc)) → new_lt17(vwx90, vwx100, cc)
new_primCmpNat2(Succ(vwx9000), Succ(vwx10000)) → new_primCmpNat2(vwx9000, vwx10000)
new_lt6(vwx90, vwx100, ty_Float) → new_lt4(vwx90, vwx100)
new_primCmpInt(Pos(Succ(vwx900)), Pos(vwx100)) → new_primCmpNat0(vwx900, vwx100)
new_ltEs5(vwx91, vwx101, ty_Int) → new_ltEs9(vwx91, vwx101)
new_esEs18(Right(vwx300), Right(vwx400), daf, app(app(ty_@2, dfc), dfd)) → new_esEs5(vwx300, vwx400, dfc, dfd)
new_esEs29(vwx301, vwx401, ty_Integer) → new_esEs20(vwx301, vwx401)
new_esEs27(vwx301, vwx401, app(app(ty_@2, cgg), cgh)) → new_esEs5(vwx301, vwx401, cgg, cgh)
new_compare28(vwx90, vwx100, True, h, ba, bb) → EQ
new_esEs6(Just(vwx300), Just(vwx400), ty_Double) → new_esEs15(vwx300, vwx400)
new_ltEs4(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, fd) → new_pePe(new_lt6(vwx90, vwx100, gd), new_asAs(new_esEs11(vwx90, vwx100, gd), new_ltEs5(vwx91, vwx101, fd)))
new_primCmpNat0(vwx900, Zero) → GT
new_esEs7(vwx30, vwx40, ty_Double) → new_esEs15(vwx30, vwx40)
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_Float) → new_esEs13(vwx300, vwx400)
new_esEs11(vwx90, vwx100, ty_Float) → new_esEs13(vwx90, vwx100)
new_lt20(vwx91, vwx101, ty_Double) → new_lt11(vwx91, vwx101)
new_ltEs17(vwx9, vwx10, bgc) → new_not(new_esEs9(new_compare9(vwx9, vwx10, bgc), GT))
new_primCmpInt(Pos(Zero), Neg(Succ(vwx1000))) → GT
new_ltEs18(vwx9, vwx10) → new_not(new_esEs9(new_compare7(vwx9, vwx10), GT))
new_ltEs19(vwx92, vwx102, app(ty_[], eb)) → new_ltEs7(vwx92, vwx102, eb)
new_esEs21(vwx300, vwx400, app(app(ty_Either, bhg), bhh)) → new_esEs18(vwx300, vwx400, bhg, bhh)
new_compare27(vwx90, vwx100, False) → new_compare13(vwx90, vwx100, new_ltEs14(vwx90, vwx100))
new_esEs18(Left(vwx300), Left(vwx400), ty_Ordering, dag) → new_esEs9(vwx300, vwx400)
new_esEs27(vwx301, vwx401, ty_@0) → new_esEs17(vwx301, vwx401)
new_esEs21(vwx300, vwx400, app(app(app(ty_@3, bha), bhb), bhc)) → new_esEs4(vwx300, vwx400, bha, bhb, bhc)
new_esEs11(vwx90, vwx100, app(app(ty_@2, fg), fh)) → new_esEs5(vwx90, vwx100, fg, fh)
new_esEs6(Just(vwx300), Just(vwx400), app(app(app(ty_@3, ceg), ceh), cfa)) → new_esEs4(vwx300, vwx400, ceg, ceh, cfa)
new_ltEs19(vwx92, vwx102, ty_Ordering) → new_ltEs14(vwx92, vwx102)
new_ltEs13(Left(vwx90), Left(vwx100), app(app(ty_Either, bae), baf), baa) → new_ltEs13(vwx90, vwx100, bae, baf)
new_esEs8(vwx30, vwx40, ty_Ordering) → new_esEs9(vwx30, vwx40)
new_esEs25(vwx91, vwx101, ty_Int) → new_esEs14(vwx91, vwx101)
new_lt6(vwx90, vwx100, app(ty_Maybe, gc)) → new_lt17(vwx90, vwx100, gc)
new_ltEs13(Right(vwx90), Right(vwx100), bah, app(app(ty_Either, bbg), bbh)) → new_ltEs13(vwx90, vwx100, bbg, bbh)
new_ltEs13(Left(vwx90), Left(vwx100), app(app(app(ty_@3, hf), hg), hh), baa) → new_ltEs6(vwx90, vwx100, hf, hg, hh)
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_@0) → new_ltEs12(vwx90, vwx100)
new_ltEs13(Left(vwx90), Left(vwx100), ty_Float, baa) → new_ltEs8(vwx90, vwx100)
new_esEs27(vwx301, vwx401, ty_Int) → new_esEs14(vwx301, vwx401)
new_esEs21(vwx300, vwx400, ty_Float) → new_esEs13(vwx300, vwx400)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_esEs27(vwx301, vwx401, ty_Float) → new_esEs13(vwx301, vwx401)
new_ltEs13(Left(vwx90), Left(vwx100), ty_Ordering, baa) → new_ltEs14(vwx90, vwx100)
new_lt20(vwx91, vwx101, ty_@0) → new_lt13(vwx91, vwx101)
new_compare15(vwx90, vwx100, True, h, ba, bb) → LT
new_esEs26(vwx90, vwx100, ty_Int) → new_esEs14(vwx90, vwx100)
new_asAs(False, vwx45) → False
new_lt20(vwx91, vwx101, ty_Bool) → new_lt16(vwx91, vwx101)
new_primMulInt(Neg(vwx3000), Pos(vwx4000)) → Neg(new_primMulNat0(vwx3000, vwx4000))
new_primMulInt(Pos(vwx3000), Neg(vwx4000)) → Neg(new_primMulNat0(vwx3000, vwx4000))
new_ltEs19(vwx92, vwx102, ty_Char) → new_ltEs11(vwx92, vwx102)
new_primMulNat0(Zero, Succ(vwx40000)) → Zero
new_primMulNat0(Succ(vwx30000), Zero) → Zero
new_ltEs13(Left(vwx90), Right(vwx100), bah, baa) → True
new_ltEs20(vwx16, vwx17, ty_Bool) → new_ltEs15(vwx16, vwx17)
new_esEs6(Just(vwx300), Just(vwx400), app(ty_Maybe, cef)) → new_esEs6(vwx300, vwx400, cef)
new_esEs26(vwx90, vwx100, app(ty_[], bf)) → new_esEs12(vwx90, vwx100, bf)
new_esEs11(vwx90, vwx100, app(ty_[], ff)) → new_esEs12(vwx90, vwx100, ff)
new_esEs18(Right(vwx300), Right(vwx400), daf, app(app(ty_Either, dfe), dff)) → new_esEs18(vwx300, vwx400, dfe, dff)
new_compare33(vwx90, vwx100, ty_Float) → new_compare6(vwx90, vwx100)
new_ltEs14(GT, LT) → False
new_primCmpNat1(Succ(vwx1000), vwx900) → new_primCmpNat2(vwx1000, vwx900)
new_primCmpNat2(Succ(vwx9000), Zero) → GT
new_lt19(vwx90, vwx100, ty_Bool) → new_lt16(vwx90, vwx100)
new_ltEs5(vwx91, vwx101, ty_Char) → new_ltEs11(vwx91, vwx101)
new_esEs4(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), caa, cab, cac) → new_asAs(new_esEs24(vwx300, vwx400, caa), new_asAs(new_esEs23(vwx301, vwx401, cab), new_esEs22(vwx302, vwx402, cac)))
new_esEs23(vwx301, vwx401, app(ty_Maybe, cbg)) → new_esEs6(vwx301, vwx401, cbg)
new_compare210(vwx9, vwx10, False, dfg, be) → new_compare110(vwx9, vwx10, new_ltEs21(vwx9, vwx10, dfg), dfg, be)
new_ltEs16(Just(vwx90), Just(vwx100), app(app(ty_Either, bch), bda)) → new_ltEs13(vwx90, vwx100, bch, bda)
new_esEs28(vwx300, vwx400, ty_Float) → new_esEs13(vwx300, vwx400)
new_esEs7(vwx30, vwx40, ty_Bool) → new_esEs10(vwx30, vwx40)
new_ltEs21(vwx9, vwx10, ty_@0) → new_ltEs12(vwx9, vwx10)
new_esEs8(vwx30, vwx40, ty_Bool) → new_esEs10(vwx30, vwx40)
new_lt14(vwx90, vwx100, ca, cb) → new_esEs9(new_compare29(vwx90, vwx100, ca, cb), LT)
new_lt20(vwx91, vwx101, app(ty_Ratio, ceb)) → new_lt18(vwx91, vwx101, ceb)
new_esEs11(vwx90, vwx100, app(ty_Ratio, bfh)) → new_esEs19(vwx90, vwx100, bfh)
new_esEs15(Double(vwx300, vwx301), Double(vwx400, vwx401)) → new_esEs14(new_sr(vwx300, vwx400), new_sr(vwx301, vwx401))
new_lt6(vwx90, vwx100, app(app(ty_@2, fg), fh)) → new_lt10(vwx90, vwx100, fg, fh)
new_esEs23(vwx301, vwx401, ty_Bool) → new_esEs10(vwx301, vwx401)
new_compare27(vwx90, vwx100, True) → EQ
new_esEs18(Left(vwx300), Left(vwx400), app(ty_Maybe, ddd), dag) → new_esEs6(vwx300, vwx400, ddd)
new_ltEs13(Right(vwx90), Left(vwx100), bah, baa) → False
new_ltEs21(vwx9, vwx10, ty_Double) → new_ltEs10(vwx9, vwx10)
new_esEs22(vwx302, vwx402, app(ty_[], cba)) → new_esEs12(vwx302, vwx402, cba)
new_compare29(Right(vwx30), Right(vwx40), bed, bee) → new_compare211(vwx30, vwx40, new_esEs8(vwx30, vwx40, bee), bed, bee)
new_compare211(vwx16, vwx17, True, bef, dch) → EQ
new_esEs14(vwx30, vwx40) → new_primEqInt(vwx30, vwx40)
new_ltEs13(Right(vwx90), Right(vwx100), bah, app(app(ty_@2, bbe), bbf)) → new_ltEs4(vwx90, vwx100, bbe, bbf)
new_lt19(vwx90, vwx100, app(app(app(ty_@3, h), ba), bb)) → new_lt7(vwx90, vwx100, h, ba, bb)
new_lt19(vwx90, vwx100, ty_Int) → new_lt9(vwx90, vwx100)
new_compare33(vwx90, vwx100, ty_Ordering) → new_compare18(vwx90, vwx100)
new_esEs8(vwx30, vwx40, ty_Float) → new_esEs13(vwx30, vwx40)
new_lt20(vwx91, vwx101, ty_Integer) → new_lt5(vwx91, vwx101)
new_ltEs12(vwx9, vwx10) → new_not(new_esEs9(new_compare19(vwx9, vwx10), GT))
new_compare11(vwx90, vwx100, False) → GT
new_ltEs13(Right(vwx90), Right(vwx100), bah, ty_Bool) → new_ltEs15(vwx90, vwx100)
new_ltEs14(LT, GT) → True
new_esEs25(vwx91, vwx101, app(app(ty_@2, db), dc)) → new_esEs5(vwx91, vwx101, db, dc)
new_esEs9(EQ, LT) → False
new_esEs9(LT, EQ) → False
new_compare33(vwx90, vwx100, app(app(ty_Either, bea), beb)) → new_compare29(vwx90, vwx100, bea, beb)
new_compare7(Integer(vwx90), Integer(vwx100)) → new_primCmpInt(vwx90, vwx100)
new_ltEs14(LT, EQ) → True
new_compare11(vwx90, vwx100, True) → LT
new_compare28(vwx90, vwx100, False, h, ba, bb) → new_compare15(vwx90, vwx100, new_ltEs6(vwx90, vwx100, h, ba, bb), h, ba, bb)
new_ltEs5(vwx91, vwx101, ty_Double) → new_ltEs10(vwx91, vwx101)
new_lt19(vwx90, vwx100, ty_Double) → new_lt11(vwx90, vwx100)
new_esEs23(vwx301, vwx401, app(app(ty_Either, ccf), ccg)) → new_esEs18(vwx301, vwx401, ccf, ccg)
new_lt20(vwx91, vwx101, ty_Char) → new_lt12(vwx91, vwx101)
new_lt19(vwx90, vwx100, ty_Float) → new_lt4(vwx90, vwx100)
new_esEs18(Left(vwx300), Left(vwx400), ty_Integer, dag) → new_esEs20(vwx300, vwx400)
new_esEs11(vwx90, vwx100, app(app(ty_Either, ga), gb)) → new_esEs18(vwx90, vwx100, ga, gb)
new_esEs28(vwx300, vwx400, ty_Bool) → new_esEs10(vwx300, vwx400)
new_esEs6(Just(vwx300), Just(vwx400), ty_Integer) → new_esEs20(vwx300, vwx400)
new_esEs22(vwx302, vwx402, ty_Int) → new_esEs14(vwx302, vwx402)
new_esEs24(vwx300, vwx400, ty_Ordering) → new_esEs9(vwx300, vwx400)
new_ltEs21(vwx9, vwx10, ty_Integer) → new_ltEs18(vwx9, vwx10)
new_esEs28(vwx300, vwx400, app(app(ty_Either, dac), dad)) → new_esEs18(vwx300, vwx400, dac, dad)
new_lt4(vwx90, vwx100) → new_esEs9(new_compare6(vwx90, vwx100), LT)
new_primPlusNat1(Zero, Zero) → Zero
new_compare111(vwx30, vwx31, True, dcd, dce) → LT
new_esEs26(vwx90, vwx100, ty_Ordering) → new_esEs9(vwx90, vwx100)
new_compare16(Double(vwx90, vwx91), Double(vwx100, vwx101)) → new_compare31(new_sr(vwx90, vwx100), new_sr(vwx91, vwx101))
new_ltEs14(EQ, EQ) → True
new_esEs12(:(vwx300, vwx301), :(vwx400, vwx401), bgf) → new_asAs(new_esEs21(vwx300, vwx400, bgf), new_esEs12(vwx301, vwx401, bgf))
new_esEs21(vwx300, vwx400, ty_Integer) → new_esEs20(vwx300, vwx400)
new_asAs(True, vwx45) → vwx45
new_esEs28(vwx300, vwx400, app(ty_[], chh)) → new_esEs12(vwx300, vwx400, chh)
new_esEs27(vwx301, vwx401, app(ty_[], cgf)) → new_esEs12(vwx301, vwx401, cgf)
new_compare29(Right(vwx30), Left(vwx40), bed, bee) → GT
new_lt18(vwx90, vwx100, bgb) → new_esEs9(new_compare9(vwx90, vwx100, bgb), LT)
new_primMulNat0(Succ(vwx30000), Succ(vwx40000)) → new_primPlusNat0(new_primMulNat0(vwx30000, Succ(vwx40000)), vwx40000)
new_compare33(vwx90, vwx100, app(ty_[], bdf)) → new_compare1(vwx90, vwx100, bdf)
new_ltEs5(vwx91, vwx101, ty_Integer) → new_ltEs18(vwx91, vwx101)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs18(Right(vwx300), Right(vwx400), daf, app(app(app(ty_@3, deg), deh), dfa)) → new_esEs4(vwx300, vwx400, deg, deh, dfa)
new_esEs26(vwx90, vwx100, ty_Double) → new_esEs15(vwx90, vwx100)
new_compare1(:(vwx90, vwx91), [], eh) → GT
new_ltEs13(Left(vwx90), Left(vwx100), ty_Char, baa) → new_ltEs11(vwx90, vwx100)
new_compare14(vwx90, vwx100, cc) → new_compare26(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
new_esEs24(vwx300, vwx400, ty_Float) → new_esEs13(vwx300, vwx400)
new_ltEs5(vwx91, vwx101, ty_@0) → new_ltEs12(vwx91, vwx101)
new_lt20(vwx91, vwx101, ty_Int) → new_lt9(vwx91, vwx101)
new_esEs26(vwx90, vwx100, ty_Char) → new_esEs16(vwx90, vwx100)
new_lt5(vwx90, vwx100) → new_esEs9(new_compare7(vwx90, vwx100), LT)
new_ltEs13(Left(vwx90), Left(vwx100), ty_Bool, baa) → new_ltEs15(vwx90, vwx100)
new_esEs7(vwx30, vwx40, app(ty_Maybe, ced)) → new_esEs6(vwx30, vwx40, ced)
new_esEs26(vwx90, vwx100, app(app(ty_Either, ca), cb)) → new_esEs18(vwx90, vwx100, ca, cb)
new_compare33(vwx90, vwx100, ty_Bool) → new_compare17(vwx90, vwx100)
new_ltEs21(vwx9, vwx10, ty_Char) → new_ltEs11(vwx9, vwx10)
new_esEs26(vwx90, vwx100, app(ty_Ratio, bgb)) → new_esEs19(vwx90, vwx100, bgb)
new_esEs24(vwx300, vwx400, app(ty_Maybe, cda)) → new_esEs6(vwx300, vwx400, cda)
new_esEs21(vwx300, vwx400, ty_Bool) → new_esEs10(vwx300, vwx400)
new_esEs7(vwx30, vwx40, app(ty_[], bgf)) → new_esEs12(vwx30, vwx40, bgf)
new_esEs24(vwx300, vwx400, app(app(app(ty_@3, cdb), cdc), cdd)) → new_esEs4(vwx300, vwx400, cdb, cdc, cdd)
new_esEs9(LT, LT) → True
new_primCompAux00(vwx64, GT) → GT
new_ltEs16(Just(vwx90), Just(vwx100), app(app(ty_@2, bcf), bcg)) → new_ltEs4(vwx90, vwx100, bcf, bcg)
new_ltEs16(Just(vwx90), Just(vwx100), ty_Bool) → new_ltEs15(vwx90, vwx100)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_ltEs14(EQ, GT) → True
new_esEs18(Left(vwx300), Left(vwx400), app(ty_[], ddh), dag) → new_esEs12(vwx300, vwx400, ddh)
new_esEs18(Left(vwx300), Left(vwx400), ty_@0, dag) → new_esEs17(vwx300, vwx400)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs18(Left(vwx300), Left(vwx400), app(ty_Ratio, ddc), dag) → new_esEs19(vwx300, vwx400, ddc)
new_esEs11(vwx90, vwx100, ty_Bool) → new_esEs10(vwx90, vwx100)
new_primCmpInt(Neg(Succ(vwx900)), Pos(vwx100)) → LT
new_esEs18(Right(vwx300), Right(vwx400), daf, ty_Int) → new_esEs14(vwx300, vwx400)
new_not(True) → False
new_esEs11(vwx90, vwx100, ty_@0) → new_esEs17(vwx90, vwx100)
new_compare1([], [], eh) → EQ
The set Q consists of the following terms:
new_compare26(x0, x1, False, x2)
new_lt19(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Integer)
new_compare33(x0, x1, ty_Bool)
new_ltEs5(x0, x1, ty_Char)
new_ltEs5(x0, x1, app(ty_Maybe, x2))
new_esEs6(Nothing, Just(x0), x1)
new_esEs23(x0, x1, ty_@0)
new_esEs11(x0, x1, ty_Double)
new_ltEs5(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Integer)
new_ltEs19(x0, x1, ty_Integer)
new_esEs7(x0, x1, ty_Integer)
new_esEs18(Right(x0), Right(x1), x2, ty_Float)
new_ltEs19(x0, x1, app(ty_[], x2))
new_ltEs5(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs16(Nothing, Just(x0), x1)
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Float)
new_compare33(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_compare29(Right(x0), Left(x1), x2, x3)
new_compare29(Left(x0), Right(x1), x2, x3)
new_ltEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs12(:(x0, x1), [], x2)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_asAs(False, x0)
new_lt7(x0, x1, x2, x3, x4)
new_ltEs5(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs18(x0, x1)
new_esEs29(x0, x1, ty_Integer)
new_esEs18(Right(x0), Right(x1), x2, ty_Bool)
new_compare33(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_[], x2))
new_lt15(x0, x1)
new_primMulInt(Neg(x0), Neg(x1))
new_esEs6(Nothing, Nothing, x0)
new_lt20(x0, x1, ty_Float)
new_compare11(x0, x1, False)
new_ltEs13(Right(x0), Right(x1), x2, ty_Int)
new_ltEs15(True, True)
new_primCompAux00(x0, GT)
new_lt19(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Zero)
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, ty_@0)
new_primCmpNat2(Zero, Succ(x0))
new_lt6(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_@0)
new_lt19(x0, x1, ty_Double)
new_ltEs16(Just(x0), Just(x1), ty_Int)
new_esEs24(x0, x1, ty_Ordering)
new_ltEs21(x0, x1, app(ty_[], x2))
new_ltEs20(x0, x1, ty_Char)
new_ltEs15(False, False)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, app(ty_Maybe, x2))
new_compare1(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primCmpNat2(Succ(x0), Zero)
new_esEs9(GT, LT)
new_esEs9(LT, GT)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_lt6(x0, x1, ty_Integer)
new_compare111(x0, x1, True, x2, x3)
new_ltEs10(x0, x1)
new_esEs21(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Int)
new_ltEs16(Just(x0), Just(x1), ty_@0)
new_esEs26(x0, x1, ty_Int)
new_ltEs5(x0, x1, ty_Double)
new_esEs18(Right(x0), Right(x1), x2, app(ty_[], x3))
new_compare25(x0, x1, True)
new_esEs28(x0, x1, ty_Double)
new_compare1([], :(x0, x1), x2)
new_esEs7(x0, x1, app(ty_[], x2))
new_lt19(x0, x1, ty_Integer)
new_esEs18(Left(x0), Left(x1), ty_@0, x2)
new_esEs9(GT, EQ)
new_esEs9(EQ, GT)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_ltEs19(x0, x1, ty_Bool)
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs28(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_ltEs20(x0, x1, ty_Bool)
new_lt20(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Bool)
new_ltEs21(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs18(Left(x0), Left(x1), ty_Char, x2)
new_compare33(x0, x1, app(app(ty_Either, x2), x3))
new_lt19(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_ltEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_sr(x0, x1)
new_esEs7(x0, x1, ty_Int)
new_esEs18(Left(x0), Left(x1), ty_Integer, x2)
new_ltEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs8(x0, x1, ty_Int)
new_compare33(x0, x1, app(ty_Maybe, x2))
new_compare27(x0, x1, False)
new_esEs21(x0, x1, ty_Char)
new_esEs18(Left(x0), Left(x1), ty_Ordering, x2)
new_ltEs14(EQ, EQ)
new_ltEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_ltEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs8(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_Integer)
new_esEs18(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_compare211(x0, x1, False, x2, x3)
new_compare1(:(x0, x1), [], x2)
new_ltEs13(Left(x0), Left(x1), ty_@0, x2)
new_esEs23(x0, x1, ty_Char)
new_lt6(x0, x1, ty_Ordering)
new_lt6(x0, x1, ty_Float)
new_primMulInt(Pos(x0), Pos(x1))
new_esEs11(x0, x1, ty_Int)
new_compare33(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Char)
new_ltEs5(x0, x1, ty_@0)
new_ltEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_pePe(False, x0)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_sr0(Integer(x0), Integer(x1))
new_ltEs5(x0, x1, ty_Float)
new_lt20(x0, x1, ty_Int)
new_ltEs13(Left(x0), Left(x1), ty_Bool, x2)
new_primMulNat0(Zero, Zero)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_ltEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs25(x0, x1, ty_Char)
new_esEs10(False, True)
new_esEs10(True, False)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_compare25(x0, x1, False)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_ltEs21(x0, x1, ty_Integer)
new_pePe(True, x0)
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_ltEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(Right(x0), Right(x1), x2, ty_Ordering)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs8(x0, x1, app(ty_[], x2))
new_ltEs21(x0, x1, ty_Bool)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_lt5(x0, x1)
new_compare110(x0, x1, True, x2, x3)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs18(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primPlusNat1(Succ(x0), Succ(x1))
new_ltEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs28(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs28(x0, x1, app(app(ty_@2, x2), x3))
new_compare27(x0, x1, True)
new_ltEs11(x0, x1)
new_ltEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_compare28(x0, x1, False, x2, x3, x4)
new_esEs4(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs20(Integer(x0), Integer(x1))
new_lt6(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs28(x0, x1, ty_Int)
new_esEs9(EQ, LT)
new_esEs9(LT, EQ)
new_primMulNat0(Zero, Succ(x0))
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt6(x0, x1, ty_Char)
new_ltEs13(Left(x0), Left(x1), ty_Double, x2)
new_lt20(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Char)
new_esEs12(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, ty_Int)
new_esEs8(x0, x1, ty_Float)
new_ltEs16(Nothing, Nothing, x0)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare14(x0, x1, x2)
new_primCompAux00(x0, LT)
new_lt19(x0, x1, ty_Bool)
new_esEs8(x0, x1, ty_Integer)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_ltEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_compare210(x0, x1, True, x2, x3)
new_esEs18(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, ty_Float)
new_ltEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs24(x0, x1, ty_Int)
new_esEs18(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs18(Right(x0), Right(x1), x2, ty_Double)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs5(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Double)
new_esEs15(Double(x0, x1), Double(x2, x3))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs21(x0, x1, ty_@0)
new_ltEs13(Right(x0), Right(x1), x2, ty_Double)
new_lt6(x0, x1, ty_@0)
new_lt12(x0, x1)
new_primPlusNat0(Zero, x0)
new_lt16(x0, x1)
new_lt20(x0, x1, ty_Ordering)
new_compare10(x0, x1, True, x2, x3)
new_compare9(:%(x0, x1), :%(x2, x3), ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_compare32(x0, x1, x2, x3)
new_ltEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_ltEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_primPlusNat1(Zero, Zero)
new_ltEs20(x0, x1, app(ty_[], x2))
new_primCmpNat2(Zero, Zero)
new_ltEs20(x0, x1, ty_Float)
new_ltEs9(x0, x1)
new_esEs10(True, True)
new_ltEs14(LT, LT)
new_esEs21(x0, x1, ty_Integer)
new_lt6(x0, x1, ty_Int)
new_lt13(x0, x1)
new_ltEs5(x0, x1, app(ty_Ratio, x2))
new_ltEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs18(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Double)
new_primCmpInt(Neg(Zero), Neg(Zero))
new_esEs28(x0, x1, ty_Char)
new_compare17(x0, x1)
new_esEs27(x0, x1, ty_Float)
new_esEs13(Float(x0, x1), Float(x2, x3))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs16(Char(x0), Char(x1))
new_compare8(Char(x0), Char(x1))
new_compare11(x0, x1, True)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(Right(x0), Right(x1), x2, ty_Char)
new_lt19(x0, x1, ty_@0)
new_esEs14(x0, x1)
new_ltEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(@0, @0)
new_ltEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(x0, x1, ty_@0)
new_esEs5(@2(x0, x1), @2(x2, x3), x4, x5)
new_lt19(x0, x1, ty_Float)
new_primCompAux00(x0, EQ)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_primCmpNat0(x0, Zero)
new_primCmpNat1(Succ(x0), x1)
new_compare15(x0, x1, True, x2, x3, x4)
new_ltEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_ltEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs23(x0, x1, ty_Ordering)
new_lt14(x0, x1, x2, x3)
new_lt6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Bool)
new_ltEs20(x0, x1, ty_Ordering)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_compare210(x0, x1, False, x2, x3)
new_ltEs8(x0, x1)
new_esEs30(x0, x1, ty_Integer)
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_esEs9(GT, GT)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_compare29(Right(x0), Right(x1), x2, x3)
new_ltEs15(True, False)
new_ltEs15(False, True)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_lt19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_compare111(x0, x1, False, x2, x3)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_compare1([], [], x0)
new_esEs6(Just(x0), Just(x1), ty_@0)
new_lt8(x0, x1, x2)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_esEs30(x0, x1, ty_Int)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_ltEs14(LT, EQ)
new_ltEs14(EQ, LT)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_ltEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs21(x0, x1, ty_Ordering)
new_compare33(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Double)
new_ltEs16(Just(x0), Just(x1), ty_Integer)
new_ltEs21(x0, x1, ty_Char)
new_ltEs5(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs18(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_compare12(x0, x1, True, x2)
new_esEs9(EQ, EQ)
new_ltEs21(x0, x1, ty_Float)
new_ltEs19(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_ltEs17(x0, x1, x2)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Ordering)
new_ltEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs11(x0, x1, ty_Char)
new_ltEs20(x0, x1, ty_@0)
new_esEs18(Left(x0), Left(x1), ty_Double, x2)
new_primMulInt(Neg(x0), Pos(x1))
new_primMulInt(Pos(x0), Neg(x1))
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt19(x0, x1, app(ty_Ratio, x2))
new_lt6(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Float)
new_ltEs5(x0, x1, ty_Int)
new_ltEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs12(x0, x1)
new_compare10(x0, x1, False, x2, x3)
new_esEs24(x0, x1, ty_Bool)
new_ltEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_ltEs21(x0, x1, app(app(ty_@2, x2), x3))
new_lt19(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1, ty_Char)
new_ltEs20(x0, x1, ty_Double)
new_esEs28(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Zero)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_asAs(True, x0)
new_ltEs16(Just(x0), Just(x1), app(ty_[], x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_[], x2))
new_compare24(x0, x1, True, x2, x3)
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_@0)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_ltEs19(x0, x1, ty_@0)
new_ltEs14(EQ, GT)
new_esEs22(x0, x1, ty_Char)
new_ltEs14(GT, EQ)
new_compare33(x0, x1, app(ty_Ratio, x2))
new_esEs12([], [], x0)
new_lt19(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs16(Just(x0), Just(x1), ty_Float)
new_compare18(x0, x1)
new_ltEs16(Just(x0), Nothing, x1)
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt11(x0, x1)
new_lt19(x0, x1, ty_Int)
new_esEs10(False, False)
new_compare24(x0, x1, False, x2, x3)
new_primCmpNat2(Succ(x0), Succ(x1))
new_lt4(x0, x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_ltEs21(x0, x1, ty_Ordering)
new_compare30(x0, x1, x2, x3, x4)
new_esEs26(x0, x1, ty_Char)
new_primCmpNat0(x0, Succ(x1))
new_lt18(x0, x1, x2)
new_esEs18(Right(x0), Right(x1), x2, ty_Integer)
new_esEs11(x0, x1, ty_Bool)
new_esEs7(x0, x1, ty_Bool)
new_esEs28(x0, x1, ty_Ordering)
new_ltEs16(Just(x0), Just(x1), ty_Double)
new_esEs28(x0, x1, ty_Integer)
new_ltEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs26(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs18(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primCompAux0(x0, x1, x2, x3)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs29(x0, x1, ty_Int)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs5(x0, x1, ty_Integer)
new_esEs18(Left(x0), Left(x1), ty_Float, x2)
new_compare12(x0, x1, False, x2)
new_esEs11(x0, x1, app(ty_[], x2))
new_ltEs21(x0, x1, ty_Int)
new_ltEs14(LT, GT)
new_ltEs14(GT, LT)
new_lt6(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primMulNat0(Succ(x0), Zero)
new_compare15(x0, x1, False, x2, x3, x4)
new_esEs27(x0, x1, ty_Bool)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Integer)
new_esEs11(x0, x1, ty_Float)
new_esEs12([], :(x0, x1), x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs28(x0, x1, app(ty_[], x2))
new_compare26(x0, x1, True, x2)
new_ltEs21(x0, x1, app(ty_Maybe, x2))
new_ltEs20(x0, x1, ty_Integer)
new_ltEs20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs18(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_lt20(x0, x1, ty_Integer)
new_lt10(x0, x1, x2, x3)
new_compare33(x0, x1, ty_Ordering)
new_esEs11(x0, x1, ty_Ordering)
new_ltEs14(GT, GT)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_ltEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_lt20(x0, x1, ty_@0)
new_ltEs20(x0, x1, app(ty_Ratio, x2))
new_not(True)
new_primCmpNat1(Zero, x0)
new_ltEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs28(x0, x1, ty_Float)
new_ltEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs25(x0, x1, ty_Double)
new_ltEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_compare9(:%(x0, x1), :%(x2, x3), ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_lt19(x0, x1, app(app(ty_Either, x2), x3))
new_compare16(Double(x0, x1), Double(x2, x3))
new_compare110(x0, x1, False, x2, x3)
new_compare31(x0, x1)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_not(False)
new_compare7(Integer(x0), Integer(x1))
new_ltEs20(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_ltEs19(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Bool)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs19(x0, x1, ty_Int)
new_ltEs21(x0, x1, ty_@0)
new_compare6(Float(x0, x1), Float(x2, x3))
new_ltEs20(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs13(Left(x0), Left(x1), ty_Char, x2)
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_lt17(x0, x1, x2)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_compare33(x0, x1, app(ty_[], x2))
new_compare29(Left(x0), Left(x1), x2, x3)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(Left(x0), Right(x1), x2, x3)
new_esEs18(Right(x0), Left(x1), x2, x3)
new_ltEs19(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_Double)
new_esEs18(Right(x0), Right(x1), x2, ty_Int)
new_ltEs21(x0, x1, ty_Double)
new_ltEs19(x0, x1, ty_Ordering)
new_primPlusNat0(Succ(x0), x1)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_compare19(@0, @0)
new_primEqNat0(Zero, Succ(x0))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_compare13(x0, x1, False)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_ltEs16(Just(x0), Just(x1), ty_Bool)
new_lt20(x0, x1, app(ty_[], x2))
new_ltEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs28(x0, x1, app(ty_Ratio, x2))
new_esEs18(Right(x0), Right(x1), x2, ty_@0)
new_compare33(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Double)
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_esEs18(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_compare28(x0, x1, True, x2, x3, x4)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_compare33(x0, x1, ty_Float)
new_lt6(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_lt6(x0, x1, ty_Bool)
new_esEs11(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs13(Right(x0), Left(x1), x2, x3)
new_ltEs13(Left(x0), Right(x1), x2, x3)
new_compare13(x0, x1, True)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs28(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs7(x0, x1, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs8(x0, x1, ty_Char)
new_esEs18(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs18(Left(x0), Left(x1), app(ty_[], x2), x3)
new_lt20(x0, x1, ty_Double)
new_primPlusNat1(Zero, Succ(x0))
new_compare33(x0, x1, ty_@0)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs7(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_@0)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, ty_Ordering)
new_compare33(x0, x1, ty_Integer)
new_compare211(x0, x1, True, x2, x3)
new_ltEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs9(LT, LT)
new_ltEs16(Just(x0), Just(x1), ty_Char)
new_esEs8(x0, x1, ty_Ordering)
new_lt9(x0, x1)
new_lt6(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
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_primCompAux(vwx90, vwx100, vwx54, app(ty_[], bdf)) → new_compare(vwx90, vwx100, bdf)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3
- new_compare(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_compare(vwx91, vwx101, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_compare(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_primCompAux(vwx90, vwx100, new_compare1(vwx91, vwx101, eh), eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4
- new_compare0(Left(vwx30), Left(vwx40), bed, bee) → new_compare2(vwx30, vwx40, new_esEs7(vwx30, vwx40, bed), bed, bee)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4, 4 >= 5
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(app(ty_@2, ha), hb)) → new_ltEs1(vwx91, vwx101, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(ty_[], bf), bc, bd) → new_compare(vwx90, vwx100, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(app(ty_@2, ec), ed)) → new_ltEs1(vwx92, vwx102, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(app(app(ty_@3, h), ba), bb), bc, bd) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 4, 3 > 5, 3 > 6
- new_ltEs0(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_compare(vwx91, vwx101, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_ltEs0(:(vwx90, vwx91), :(vwx100, vwx101), eh) → new_primCompAux(vwx90, vwx100, new_compare1(vwx91, vwx101, eh), eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(app(ty_Either, hc), hd)) → new_ltEs2(vwx91, vwx101, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(app(ty_Either, ee), ef)) → new_ltEs2(vwx92, vwx102, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(app(ty_Either, ga), gb), fd) → new_lt2(vwx90, vwx100, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(app(ty_Either, dd), de), bd) → new_lt2(vwx91, vwx101, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare0(Right(vwx30), Right(vwx40), bed, bee) → new_compare23(vwx30, vwx40, new_esEs8(vwx30, vwx40, bee), bed, bee)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4, 4 >= 5
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(app(app(ty_@3, ge), gf), gg)) → new_ltEs(vwx91, vwx101, ge, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(app(app(ty_@3, dg), dh), ea)) → new_ltEs(vwx92, vwx102, dg, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_lt2(vwx90, vwx100, ca, cb) → new_compare0(vwx90, vwx100, ca, cb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
- new_primCompAux(vwx90, vwx100, vwx54, app(app(app(ty_@3, bdc), bdd), bde)) → new_compare3(vwx90, vwx100, bdc, bdd, bde)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4, 4 > 5
- new_compare20(vwx90, vwx100, False, h, ba, bb) → new_ltEs(vwx90, vwx100, h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4, 6 >= 5
- new_compare22(vwx90, vwx100, False, cc) → new_ltEs3(vwx90, vwx100, cc)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3
- new_lt(vwx90, vwx100, h, ba, bb) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5, 5 >= 6
- new_compare2(:(vwx90, vwx91), :(vwx100, vwx101), False, app(ty_[], eh), be) → new_primCompAux(vwx90, vwx100, new_compare1(vwx91, vwx101, eh), eh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4
- new_ltEs3(Just(vwx90), Just(vwx100), app(app(ty_@2, bcf), bcg)) → new_ltEs1(vwx90, vwx100, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs3(Just(vwx90), Just(vwx100), app(app(ty_Either, bch), bda)) → new_ltEs2(vwx90, vwx100, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs3(Just(vwx90), Just(vwx100), app(app(app(ty_@3, bcb), bcc), bcd)) → new_ltEs(vwx90, vwx100, bcb, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(ty_[], ff), fd) → new_lt0(vwx90, vwx100, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(ty_[], da), bd) → new_lt0(vwx91, vwx101, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(ty_Maybe, he)) → new_ltEs3(vwx91, vwx101, he)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(ty_Maybe, eg)) → new_ltEs3(vwx92, vwx102, eg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_ltEs3(Just(vwx90), Just(vwx100), app(ty_Maybe, bdb)) → new_ltEs3(vwx90, vwx100, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs3(Just(vwx90), Just(vwx100), app(ty_[], bce)) → new_ltEs0(vwx90, vwx100, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_primCompAux(vwx90, vwx100, vwx54, app(ty_Maybe, bec)) → new_compare5(vwx90, vwx100, bec)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3
- new_lt0(vwx90, vwx100, bf) → new_compare(vwx90, vwx100, bf)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- new_lt3(vwx90, vwx100, cc) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4
- new_lt1(vwx90, vwx100, bg, bh) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_primCompAux(vwx90, vwx100, vwx54, app(app(ty_Either, bea), beb)) → new_compare0(vwx90, vwx100, bea, beb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_primCompAux(vwx90, vwx100, vwx54, app(app(ty_@2, bdg), bdh)) → new_compare4(vwx90, vwx100, bdg, bdh)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(app(ty_Either, ca), cb), bc, bd) → new_compare0(vwx90, vwx100, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(app(app(ty_@3, h), ba), bb)), bc), bd), be) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4, 4 > 5, 4 > 6
- new_compare3(vwx90, vwx100, h, ba, bb) → new_compare20(vwx90, vwx100, new_esEs4(vwx90, vwx100, h, ba, bb), h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5, 5 >= 6
- new_compare23(vwx16, vwx17, False, bef, app(app(ty_Either, bfe), bff)) → new_ltEs2(vwx16, vwx17, bfe, bff)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 > 3, 5 > 4
- new_compare23(vwx16, vwx17, False, bef, app(app(app(ty_@3, beg), beh), bfa)) → new_ltEs(vwx16, vwx17, beg, beh, bfa)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(vwx16, vwx17, False, bef, app(ty_Maybe, bfg)) → new_ltEs3(vwx16, vwx17, bfg)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 > 3
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(app(ty_Either, ca), cb)), bc), bd), be) → new_compare0(vwx90, vwx100, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), gd, app(ty_[], gh)) → new_ltEs0(vwx91, vwx101, gh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, bc, app(ty_[], eb)) → new_ltEs0(vwx92, vwx102, eb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(vwx16, vwx17, False, bef, app(ty_[], bfb)) → new_ltEs0(vwx16, vwx17, bfb)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 > 3
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(ty_Maybe, gc), fd) → new_lt3(vwx90, vwx100, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(ty_Maybe, df), bd) → new_lt3(vwx91, vwx101, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(ty_Maybe, cc), bc, bd) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 4
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(ty_Maybe, cc)), bc), bd), be) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4
- new_compare5(vwx90, vwx100, cc) → new_compare22(vwx90, vwx100, new_esEs6(vwx90, vwx100, cc), cc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4
- new_compare4(vwx90, vwx100, bg, bh) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), app(app(ty_@2, bg), bh), bc, bd) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 4, 3 > 5
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(app(ty_@2, bg), bh)), bc), bd), be) → new_compare21(vwx90, vwx100, new_esEs5(vwx90, vwx100, bg, bh), bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4, 4 > 5
- new_compare21(vwx90, vwx100, False, bg, bh) → new_ltEs1(vwx90, vwx100, bg, bh)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_compare23(vwx16, vwx17, False, bef, app(app(ty_@2, bfc), bfd)) → new_ltEs1(vwx16, vwx17, bfc, bfd)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 > 3, 5 > 4
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(app(ty_@2, fg), fh), fd) → new_lt1(vwx90, vwx100, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs1(@2(vwx90, vwx91), @2(vwx100, vwx101), app(app(app(ty_@3, fa), fb), fc), fd) → new_lt(vwx90, vwx100, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(app(ty_@2, db), dc), bd) → new_lt1(vwx91, vwx101, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), cd, app(app(app(ty_@3, ce), cf), cg), bd) → new_lt(vwx91, vwx101, ce, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_compare2(:(vwx90, vwx91), :(vwx100, vwx101), False, app(ty_[], eh), be) → new_compare(vwx91, vwx101, eh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, app(ty_[], bf)), bc), bd), be) → new_compare(vwx90, vwx100, bf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs2(Right(vwx90), Right(vwx100), bah, app(app(ty_@2, bbe), bbf)) → new_ltEs1(vwx90, vwx100, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs2(Left(vwx90), Left(vwx100), app(app(ty_@2, bac), bad), baa) → new_ltEs1(vwx90, vwx100, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(app(ty_@2, bac), bad)), baa), be) → new_ltEs1(vwx90, vwx100, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(app(ty_@2, ha), hb)), be) → new_ltEs1(vwx91, vwx101, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(app(ty_@2, bcf), bcg)), be) → new_ltEs1(vwx90, vwx100, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(app(ty_@2, ec), ed)), be) → new_ltEs1(vwx92, vwx102, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(app(ty_@2, bbe), bbf)), be) → new_ltEs1(vwx90, vwx100, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs2(Left(vwx90), Left(vwx100), app(app(ty_Either, bae), baf), baa) → new_ltEs2(vwx90, vwx100, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs2(Right(vwx90), Right(vwx100), bah, app(app(ty_Either, bbg), bbh)) → new_ltEs2(vwx90, vwx100, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs2(Left(vwx90), Left(vwx100), app(app(app(ty_@3, hf), hg), hh), baa) → new_ltEs(vwx90, vwx100, hf, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs2(Right(vwx90), Right(vwx100), bah, app(app(app(ty_@3, bba), bbb), bbc)) → new_ltEs(vwx90, vwx100, bba, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs2(Left(vwx90), Left(vwx100), app(ty_Maybe, bag), baa) → new_ltEs3(vwx90, vwx100, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs2(Right(vwx90), Right(vwx100), bah, app(ty_Maybe, bca)) → new_ltEs3(vwx90, vwx100, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs2(Right(vwx90), Right(vwx100), bah, app(ty_[], bbd)) → new_ltEs0(vwx90, vwx100, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs2(Left(vwx90), Left(vwx100), app(ty_[], bab), baa) → new_ltEs0(vwx90, vwx100, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(app(ty_Either, hc), hd)), be) → new_ltEs2(vwx91, vwx101, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(app(ty_Either, ee), ef)), be) → new_ltEs2(vwx92, vwx102, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(app(ty_Either, bbg), bbh)), be) → new_ltEs2(vwx90, vwx100, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(app(ty_Either, bae), baf)), baa), be) → new_ltEs2(vwx90, vwx100, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(app(ty_Either, bch), bda)), be) → new_ltEs2(vwx90, vwx100, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(app(ty_Either, dd), de)), bd), be) → new_lt2(vwx91, vwx101, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(app(ty_Either, ga), gb)), fd), be) → new_lt2(vwx90, vwx100, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(app(app(ty_@3, bcb), bcc), bcd)), be) → new_ltEs(vwx90, vwx100, bcb, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(app(app(ty_@3, hf), hg), hh)), baa), be) → new_ltEs(vwx90, vwx100, hf, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(app(app(ty_@3, ge), gf), gg)), be) → new_ltEs(vwx91, vwx101, ge, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(app(app(ty_@3, dg), dh), ea)), be) → new_ltEs(vwx92, vwx102, dg, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(app(app(ty_@3, bba), bbb), bbc)), be) → new_ltEs(vwx90, vwx100, bba, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(ty_[], da)), bd), be) → new_lt0(vwx91, vwx101, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(ty_[], ff)), fd), be) → new_lt0(vwx90, vwx100, ff)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(ty_Maybe, bag)), baa), be) → new_ltEs3(vwx90, vwx100, bag)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(ty_Maybe, bca)), be) → new_ltEs3(vwx90, vwx100, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(ty_Maybe, eg)), be) → new_ltEs3(vwx92, vwx102, eg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(ty_Maybe, bdb)), be) → new_ltEs3(vwx90, vwx100, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(ty_Maybe, he)), be) → new_ltEs3(vwx91, vwx101, he)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(Right(vwx90), Right(vwx100), False, app(app(ty_Either, bah), app(ty_[], bbd)), be) → new_ltEs0(vwx90, vwx100, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, gd), app(ty_[], gh)), be) → new_ltEs0(vwx91, vwx101, gh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), bc), app(ty_[], eb)), be) → new_ltEs0(vwx92, vwx102, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(Just(vwx90), Just(vwx100), False, app(ty_Maybe, app(ty_[], bce)), be) → new_ltEs0(vwx90, vwx100, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(Left(vwx90), Left(vwx100), False, app(app(ty_Either, app(ty_[], bab)), baa), be) → new_ltEs0(vwx90, vwx100, bab)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(ty_Maybe, df)), bd), be) → new_lt3(vwx91, vwx101, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(ty_Maybe, gc)), fd), be) → new_lt3(vwx90, vwx100, gc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(app(ty_@2, fg), fh)), fd), be) → new_lt1(vwx90, vwx100, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(app(ty_@2, db), dc)), bd), be) → new_lt1(vwx91, vwx101, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare2(@3(vwx90, vwx91, vwx92), @3(vwx100, vwx101, vwx102), False, app(app(app(ty_@3, cd), app(app(app(ty_@3, ce), cf), cg)), bd), be) → new_lt(vwx91, vwx101, ce, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_compare2(@2(vwx90, vwx91), @2(vwx100, vwx101), False, app(app(ty_@2, app(app(app(ty_@3, fa), fb), fc)), fd), be) → new_lt(vwx90, vwx100, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ 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_primEqNat(Succ(vwx30000), Succ(vwx40000)) → new_primEqNat(vwx30000, vwx40000)
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(vwx30000), Succ(vwx40000)) → new_primEqNat(vwx30000, vwx40000)
The graph contains the following edges 1 > 1, 2 > 2