YES
H-Termination proof of ../tpdb/FP/full_haskell/Prelude_GTEQ_12.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ CR
mainModule Main
|
| (((>=) :: (Ord b, Ord a) => (b,a) -> (b,a) -> Bool) :: (Ord b, Ord a) => (b,a) -> (b,a) -> Bool) |
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
|
| (((>=) :: (Ord b, Ord a) => (b,a) -> (b,a) -> Bool) :: (Ord b, Ord a) => (b,a) -> (b,a) -> Bool) |
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
|
| (((>=) :: (Ord a, Ord b) => (a,b) -> (a,b) -> Bool) :: (Ord a, Ord b) => (a,b) -> (a,b) -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
|
| (((>=) :: (Ord a, Ord b) => (b,a) -> (b,a) -> Bool) :: (Ord b, Ord a) => (b,a) -> (b,a) -> Bool) |
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
| absReal0 | x True | = `negate` x |
| absReal1 | x True | = x |
| absReal1 | x False | = absReal0 x otherwise |
| 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 |
| compare1 | x y True | = LT |
| compare1 | x y False | = compare0 x y otherwise |
| compare2 | x y True | = EQ |
| compare2 | x y False | = compare1 x y (x <= y) |
| compare3 | x y | = compare2 x y (x == y) |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
|
| (((>=) :: (Ord b, Ord a) => (a,b) -> (a,b) -> Bool) :: (Ord a, Ord b) => (a,b) -> (a,b) -> Bool) |
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
| reduce2Reduce1 | vwv vww x y True | = error [] |
| reduce2Reduce1 | vwv vww x y False | = reduce2Reduce0 vwv vww x y otherwise |
| reduce2Reduce0 | vwv vww x y True | = x `quot` reduce2D vwv vww :% (y `quot` reduce2D vwv vww) |
| 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' | x zx | = gcd0Gcd'2 x zx |
| gcd0Gcd' | x y | = gcd0Gcd'0 x y |
| gcd0Gcd'2 | x zx | = gcd0Gcd'1 (zx == 0) x zx |
| gcd0Gcd'2 | vuv vuw | = gcd0Gcd'0 vuv vuw |
| gcd0Gcd'1 | True x zx | = x |
| gcd0Gcd'1 | zy zz vuu | = gcd0Gcd'0 zz vuu |
| gcd0Gcd'0 | x y | = gcd0Gcd' y (x `rem` y) |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
mainModule Main
|
| (((>=) :: (Ord b, Ord a) => (b,a) -> (b,a) -> Bool) :: (Ord a, Ord b) => (b,a) -> (b,a) -> Bool) |
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
|
| ((>=) :: (Ord a, Ord b) => (a,b) -> (a,b) -> Bool) |
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_primMulNat(Succ(vwx30100), Succ(vwx40100)) → new_primMulNat(vwx30100, Succ(vwx40100))
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(vwx30100), Succ(vwx40100)) → new_primMulNat(vwx30100, Succ(vwx40100))
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
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(vwx7400), Succ(vwx401000)) → new_primPlusNat(vwx7400, vwx401000)
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(vwx7400), Succ(vwx401000)) → new_primPlusNat(vwx7400, vwx401000)
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_esEs3(Just(vwx300), Just(vwx400), app(app(ty_@2, bdd), bde)) → new_esEs0(vwx300, vwx400, bdd, bde)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(app(ty_@3, ec), ed), ee), dg) → new_esEs2(vwx300, vwx400, ec, ed, ee)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(app(ty_@3, bac), bad), bae), hf, hg) → new_esEs2(vwx300, vwx400, bac, bad, bae)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_Either, hd), he), hf, hg) → new_esEs(vwx300, vwx400, hd, he)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(app(ty_@2, bbb), bbc), hg) → new_esEs0(vwx301, vwx401, bbb, bbc)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(app(app(ty_@3, ff), fg), fh)) → new_esEs2(vwx301, vwx401, ff, fg, fh)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(ty_Maybe, bbh), hg) → new_esEs3(vwx301, vwx401, bbh)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(app(ty_@2, bcc), bcd)) → new_esEs0(vwx302, vwx402, bcc, bcd)
new_esEs(Right(vwx300), Right(vwx400), cb, app(ty_Maybe, dd)) → new_esEs3(vwx300, vwx400, dd)
new_esEs(Right(vwx300), Right(vwx400), cb, app(ty_[], cg)) → new_esEs1(vwx300, vwx400, cg)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(ty_Maybe, bda)) → new_esEs3(vwx302, vwx402, bda)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), hc) → new_esEs1(vwx301, vwx401, hc)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(ty_[], bbd), hg) → new_esEs1(vwx301, vwx401, bbd)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_@2, hh), baa), hf, hg) → new_esEs0(vwx300, vwx400, hh, baa)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_[], eb), dg) → new_esEs1(vwx300, vwx400, eb)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(ty_[], gf)) → new_esEs1(vwx300, vwx400, gf)
new_esEs(Right(vwx300), Right(vwx400), cb, app(app(ty_@2, ce), cf)) → new_esEs0(vwx300, vwx400, ce, cf)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_Either, de), df), dg) → new_esEs(vwx300, vwx400, de, df)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(app(ty_Either, eh), fa)) → new_esEs(vwx301, vwx401, eh, fa)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(app(ty_Either, bah), bba), hg) → new_esEs(vwx301, vwx401, bah, bba)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(app(ty_Either, bca), bcb)) → new_esEs(vwx302, vwx402, bca, bcb)
new_esEs(Right(vwx300), Right(vwx400), cb, app(app(ty_Either, cc), cd)) → new_esEs(vwx300, vwx400, cc, cd)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(ty_Maybe, ga)) → new_esEs3(vwx301, vwx401, ga)
new_esEs(Left(vwx300), Left(vwx400), app(app(ty_@2, bc), bd), bb) → new_esEs0(vwx300, vwx400, bc, bd)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_Maybe, ef), dg) → new_esEs3(vwx300, vwx400, ef)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(app(app(ty_@3, bbe), bbf), bbg), hg) → new_esEs2(vwx301, vwx401, bbe, bbf, bbg)
new_esEs3(Just(vwx300), Just(vwx400), app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs2(vwx300, vwx400, bdg, bdh, bea)
new_esEs3(Just(vwx300), Just(vwx400), app(ty_Maybe, beb)) → new_esEs3(vwx300, vwx400, beb)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_Maybe, baf), hf, hg) → new_esEs3(vwx300, vwx400, baf)
new_esEs(Left(vwx300), Left(vwx400), app(ty_Maybe, ca), bb) → new_esEs3(vwx300, vwx400, ca)
new_esEs3(Just(vwx300), Just(vwx400), app(app(ty_Either, bdb), bdc)) → new_esEs(vwx300, vwx400, bdb, bdc)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_@2, dh), ea), dg) → new_esEs0(vwx300, vwx400, dh, ea)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(ty_[], bce)) → new_esEs1(vwx302, vwx402, bce)
new_esEs(Left(vwx300), Left(vwx400), app(ty_[], be), bb) → new_esEs1(vwx300, vwx400, be)
new_esEs(Left(vwx300), Left(vwx400), app(app(app(ty_@3, bf), bg), bh), bb) → new_esEs2(vwx300, vwx400, bf, bg, bh)
new_esEs(Right(vwx300), Right(vwx400), cb, app(app(app(ty_@3, da), db), dc)) → new_esEs2(vwx300, vwx400, da, db, dc)
new_esEs3(Just(vwx300), Just(vwx400), app(ty_[], bdf)) → new_esEs1(vwx300, vwx400, bdf)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(ty_[], fd)) → new_esEs1(vwx301, vwx401, fd)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_[], bab), hf, hg) → new_esEs1(vwx300, vwx400, bab)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(app(ty_@3, gg), gh), ha)) → new_esEs2(vwx300, vwx400, gg, gh, ha)
new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(app(ty_@2, fb), fc)) → new_esEs0(vwx301, vwx401, fb, fc)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_Either, gb), gc)) → new_esEs(vwx300, vwx400, gb, gc)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(ty_Maybe, hb)) → new_esEs3(vwx300, vwx400, hb)
new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_@2, gd), ge)) → new_esEs0(vwx300, vwx400, gd, ge)
new_esEs(Left(vwx300), Left(vwx400), app(app(ty_Either, h), ba), bb) → new_esEs(vwx300, vwx400, h, ba)
new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(app(app(ty_@3, bcf), bcg), bch)) → new_esEs2(vwx302, vwx402, bcf, bcg, bch)
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_esEs3(Just(vwx300), Just(vwx400), app(ty_Maybe, beb)) → new_esEs3(vwx300, vwx400, beb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(ty_Maybe, hb)) → new_esEs3(vwx300, vwx400, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(vwx300), Just(vwx400), app(app(ty_@2, bdd), bde)) → new_esEs0(vwx300, vwx400, bdd, bde)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_@2, gd), ge)) → new_esEs0(vwx300, vwx400, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(vwx300), Just(vwx400), app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs2(vwx300, vwx400, bdg, bdh, bea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(app(ty_@3, gg), gh), ha)) → new_esEs2(vwx300, vwx400, gg, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(vwx300), Just(vwx400), app(app(ty_Either, bdb), bdc)) → new_esEs(vwx300, vwx400, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(vwx300), Just(vwx400), app(ty_[], bdf)) → new_esEs1(vwx300, vwx400, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), app(app(ty_Either, gb), gc)) → new_esEs(vwx300, vwx400, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(ty_Maybe, ga)) → new_esEs3(vwx301, vwx401, ga)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_Maybe, ef), dg) → new_esEs3(vwx300, vwx400, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_@2, dh), ea), dg) → new_esEs0(vwx300, vwx400, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(app(ty_@2, fb), fc)) → new_esEs0(vwx301, vwx401, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(app(ty_@3, ec), ed), ee), dg) → new_esEs2(vwx300, vwx400, ec, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(app(app(ty_@3, ff), fg), fh)) → new_esEs2(vwx301, vwx401, ff, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_Either, de), df), dg) → new_esEs(vwx300, vwx400, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(app(ty_Either, eh), fa)) → new_esEs(vwx301, vwx401, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_[], eb), dg) → new_esEs1(vwx300, vwx400, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@2(vwx300, vwx301), @2(vwx400, vwx401), eg, app(ty_[], fd)) → new_esEs1(vwx301, vwx401, fd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(ty_Maybe, bbh), hg) → new_esEs3(vwx301, vwx401, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(ty_Maybe, bda)) → new_esEs3(vwx302, vwx402, bda)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_Maybe, baf), hf, hg) → new_esEs3(vwx300, vwx400, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(vwx300), Right(vwx400), cb, app(ty_Maybe, dd)) → new_esEs3(vwx300, vwx400, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Left(vwx300), Left(vwx400), app(ty_Maybe, ca), bb) → new_esEs3(vwx300, vwx400, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(app(ty_@2, bbb), bbc), hg) → new_esEs0(vwx301, vwx401, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(app(ty_@2, bcc), bcd)) → new_esEs0(vwx302, vwx402, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_@2, hh), baa), hf, hg) → new_esEs0(vwx300, vwx400, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(app(ty_@3, bac), bad), bae), hf, hg) → new_esEs2(vwx300, vwx400, bac, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(app(app(ty_@3, bbe), bbf), bbg), hg) → new_esEs2(vwx301, vwx401, bbe, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(app(app(ty_@3, bcf), bcg), bch)) → new_esEs2(vwx302, vwx402, bcf, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_Either, hd), he), hf, hg) → new_esEs(vwx300, vwx400, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(app(ty_Either, bah), bba), hg) → new_esEs(vwx301, vwx401, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(app(ty_Either, bca), bcb)) → new_esEs(vwx302, vwx402, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, app(ty_[], bbd), hg) → new_esEs1(vwx301, vwx401, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bag, hf, app(ty_[], bce)) → new_esEs1(vwx302, vwx402, bce)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_[], bab), hf, hg) → new_esEs1(vwx300, vwx400, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(vwx300), Right(vwx400), cb, app(app(ty_@2, ce), cf)) → new_esEs0(vwx300, vwx400, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(vwx300), Left(vwx400), app(app(ty_@2, bc), bd), bb) → new_esEs0(vwx300, vwx400, bc, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(vwx300), Right(vwx400), cb, app(app(app(ty_@3, da), db), dc)) → new_esEs2(vwx300, vwx400, da, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(Left(vwx300), Left(vwx400), app(app(app(ty_@3, bf), bg), bh), bb) → new_esEs2(vwx300, vwx400, bf, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Right(vwx300), Right(vwx400), cb, app(app(ty_Either, cc), cd)) → new_esEs(vwx300, vwx400, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(vwx300), Left(vwx400), app(app(ty_Either, h), ba), bb) → new_esEs(vwx300, vwx400, h, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(vwx300), Right(vwx400), cb, app(ty_[], cg)) → new_esEs1(vwx300, vwx400, cg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Left(vwx300), Left(vwx400), app(ty_[], be), bb) → new_esEs1(vwx300, vwx400, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(vwx300, vwx301), :(vwx400, vwx401), hc) → new_esEs1(vwx301, vwx401, hc)
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
↳ 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(vwx340000), Succ(vwx360000)) → new_primCmpNat(vwx340000, vwx360000)
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(vwx340000), Succ(vwx360000)) → new_primCmpNat(vwx340000, vwx360000)
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_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
↳ 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_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(app(ty_@2, ef), eg)), dg)) → new_ltEs3(vwx3410, vwx3610, ef, eg)
new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(ty_Maybe, fb))) → new_ltEs0(vwx3410, vwx3610, fb)
new_ltEs1(Left(vwx3410), Left(vwx3610), app(app(ty_Either, ea), eb), dg) → new_ltEs1(vwx3410, vwx3610, ea, eb)
new_ltEs1(Left(vwx3410), Left(vwx3610), app(ty_Maybe, dh), dg) → new_ltEs0(vwx3410, vwx3610, dh)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(ty_[], bda), bdb) → new_lt(vwx3410, vwx3610, bda)
new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(ty_[], df)), dg)) → new_ltEs(vwx3410, vwx3610, df)
new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(ty_[], fa)) → new_ltEs(vwx3410, vwx3610, fa)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(app(ty_Either, gg), gh), gd, ge) → new_lt1(vwx3410, vwx3610, gg, gh)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(app(app(ty_@3, bac), bad), bae), ge) → new_lt2(vwx3411, vwx3611, bac, bad, bae)
new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(app(ty_Either, bca), bcb), bfe) → new_compare21(vwx340, vwx360, new_esEs5(vwx340, vwx360, bca, bcb), bca, bcb)
new_ltEs0(Just(vwx3410), Just(vwx3610), app(ty_Maybe, ce)) → new_ltEs0(vwx3410, vwx3610, ce)
new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(ty_Maybe, dh)), dg)) → new_ltEs0(vwx3410, vwx3610, dh)
new_primCompAux(vwx3400, vwx3600, vwx101, app(ty_[], bb)) → new_compare(vwx3400, vwx3600, bb)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(app(ty_@2, hd), he)), gd), ge)) → new_lt3(vwx3410, vwx3610, hd, he)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(app(ty_Either, bdd), bde)), bdb)) → new_lt1(vwx3410, vwx3610, bdd, bde)
new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(app(app(ty_@3, da), db), dc))) → new_ltEs2(vwx3410, vwx3610, da, db, dc)
new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(ty_Maybe, cc), bfe) → new_compare20(vwx340, vwx360, new_esEs4(vwx340, vwx360, cc), cc)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(ty_[], bah))) → new_ltEs(vwx3412, vwx3612, bah)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(ty_Maybe, gf), gd, ge) → new_lt0(vwx3410, vwx3610, gf)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(app(ty_@2, bfc), bfd)) → new_ltEs3(vwx3411, vwx3611, bfc, bfd)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(ty_Maybe, hh)), ge)) → new_lt0(vwx3411, vwx3611, hh)
new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(ty_Maybe, fb)) → new_ltEs0(vwx3410, vwx3610, fb)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(app(ty_Either, bef), beg)) → new_ltEs1(vwx3411, vwx3611, bef, beg)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(app(ty_@2, bea), beb)), bdb)) → new_lt3(vwx3410, vwx3610, bea, beb)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(app(app(ty_@3, bbd), bbe), bbf))) → new_ltEs2(vwx3412, vwx3612, bbd, bbe, bbf)
new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(app(app(ty_@3, ff), fg), fh)) → new_ltEs2(vwx3410, vwx3610, ff, fg, fh)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(app(ty_Either, baa), bab)), ge)) → new_lt1(vwx3411, vwx3611, baa, bab)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(ty_[], bda)), bdb)) → new_lt(vwx3410, vwx3610, bda)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(app(app(ty_@3, beh), bfa), bfb))) → new_ltEs2(vwx3411, vwx3611, beh, bfa, bfb)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(app(app(ty_@3, bac), bad), bae)), ge)) → new_lt2(vwx3411, vwx3611, bac, bad, bae)
new_ltEs0(Just(vwx3410), Just(vwx3610), app(ty_[], cd)) → new_ltEs(vwx3410, vwx3610, cd)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(app(ty_@2, bea), beb), bdb) → new_lt3(vwx3410, vwx3610, bea, beb)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(app(ty_@2, bfc), bfd))) → new_ltEs3(vwx3411, vwx3611, bfc, bfd)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(ty_[], bah)) → new_ltEs(vwx3412, vwx3612, bah)
new_primCompAux(vwx3400, vwx3600, vwx101, app(ty_Maybe, bc)) → new_compare1(vwx3400, vwx3600, bc)
new_primCompAux(vwx3400, vwx3600, vwx101, app(app(app(ty_@3, bf), bg), bh)) → new_compare3(vwx3400, vwx3600, bf, bg, bh)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(ty_Maybe, bba))) → new_ltEs0(vwx3412, vwx3612, bba)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(app(ty_Either, gg), gh)), gd), ge)) → new_lt1(vwx3410, vwx3610, gg, gh)
new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(app(ty_Either, cf), cg))) → new_ltEs1(vwx3410, vwx3610, cf, cg)
new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(app(ty_Either, fc), fd)) → new_ltEs1(vwx3410, vwx3610, fc, fd)
new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(ty_[], cd))) → new_ltEs(vwx3410, vwx3610, cd)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(ty_Maybe, hh), ge) → new_lt0(vwx3411, vwx3611, hh)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(app(ty_@2, baf), bag)), ge)) → new_lt3(vwx3411, vwx3611, baf, bag)
new_ltEs(vwx341, vwx361, h) → new_compare(vwx341, vwx361, h)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(ty_Maybe, bdc)), bdb)) → new_lt0(vwx3410, vwx3610, bdc)
new_lt0(vwx340, vwx360, cc) → new_compare20(vwx340, vwx360, new_esEs4(vwx340, vwx360, cc), cc)
new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(app(ty_@2, dd), de))) → new_ltEs3(vwx3410, vwx3610, dd, de)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(app(ty_@2, baf), bag), ge) → new_lt3(vwx3411, vwx3611, baf, bag)
new_compare22(vwx340, vwx360, False, bcc, bcd, bce) → new_ltEs2(vwx340, vwx360, bcc, bcd, bce)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(app(ty_@2, bbg), bbh))) → new_ltEs3(vwx3412, vwx3612, bbg, bbh)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(ty_[], gc), gd, ge) → new_lt(vwx3410, vwx3610, gc)
new_lt(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_primCompAux(vwx3400, vwx3600, new_compare0(vwx3401, vwx3601, ba), ba)
new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(app(app(ty_@3, ff), fg), fh))) → new_ltEs2(vwx3410, vwx3610, ff, fg, fh)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(app(app(ty_@3, bbd), bbe), bbf)) → new_ltEs2(vwx3412, vwx3612, bbd, bbe, bbf)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(app(app(ty_@3, ha), hb), hc)), gd), ge)) → new_lt2(vwx3410, vwx3610, ha, hb, hc)
new_ltEs0(Just(vwx3410), Just(vwx3610), app(app(ty_@2, dd), de)) → new_ltEs3(vwx3410, vwx3610, dd, de)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(ty_Maybe, bee)) → new_ltEs0(vwx3411, vwx3611, bee)
new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(ty_Maybe, ce))) → new_ltEs0(vwx3410, vwx3610, ce)
new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(app(app(ty_@3, bcc), bcd), bce), bfe) → new_compare22(vwx340, vwx360, new_esEs6(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
new_compare2(vwx340, vwx360, bca, bcb) → new_compare21(vwx340, vwx360, new_esEs5(vwx340, vwx360, bca, bcb), bca, bcb)
new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(app(ty_Either, ea), eb)), dg)) → new_ltEs1(vwx3410, vwx3610, ea, eb)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(app(ty_Either, bbb), bbc)) → new_ltEs1(vwx3412, vwx3612, bbb, bbc)
new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(app(ty_Either, fc), fd))) → new_ltEs1(vwx3410, vwx3610, fc, fd)
new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(app(ty_@2, ga), gb))) → new_ltEs3(vwx3410, vwx3610, ga, gb)
new_ltEs0(Just(vwx3410), Just(vwx3610), app(app(app(ty_@3, da), db), dc)) → new_ltEs2(vwx3410, vwx3610, da, db, dc)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(app(ty_Either, baa), bab), ge) → new_lt1(vwx3411, vwx3611, baa, bab)
new_lt(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_compare(vwx3401, vwx3601, ba)
new_compare23(@2(:(vwx3400, vwx3401), vwx341), @2(:(vwx3600, vwx3601), vwx361), False, app(ty_[], ba), bfe) → new_compare(vwx3401, vwx3601, ba)
new_compare3(vwx340, vwx360, bcc, bcd, bce) → new_compare22(vwx340, vwx360, new_esEs6(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(ty_[], fa))) → new_ltEs(vwx3410, vwx3610, fa)
new_ltEs1(Left(vwx3410), Left(vwx3610), app(app(app(ty_@3, ec), ed), ee), dg) → new_ltEs2(vwx3410, vwx3610, ec, ed, ee)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(ty_[], gc)), gd), ge)) → new_lt(vwx3410, vwx3610, gc)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(ty_[], bed))) → new_ltEs(vwx3411, vwx3611, bed)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(app(ty_Either, bdd), bde), bdb) → new_lt1(vwx3410, vwx3610, bdd, bde)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(app(app(ty_@3, bdf), bdg), bdh)), bdb)) → new_lt2(vwx3410, vwx3610, bdf, bdg, bdh)
new_lt3(vwx340, vwx360, bcf, bcg) → new_compare23(vwx340, vwx360, new_esEs7(vwx340, vwx360, bcf, bcg), bcf, bcg)
new_ltEs1(Left(vwx3410), Left(vwx3610), app(ty_[], df), dg) → new_ltEs(vwx3410, vwx3610, df)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(ty_[], hg), ge) → new_lt(vwx3411, vwx3611, hg)
new_compare21(vwx340, vwx360, False, bca, bcb) → new_ltEs1(vwx340, vwx360, bca, bcb)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(app(ty_@2, bbg), bbh)) → new_ltEs3(vwx3412, vwx3612, bbg, bbh)
new_primCompAux(vwx3400, vwx3600, vwx101, app(app(ty_Either, bd), be)) → new_compare2(vwx3400, vwx3600, bd, be)
new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(app(app(ty_@3, ec), ed), ee)), dg)) → new_ltEs2(vwx3410, vwx3610, ec, ed, ee)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(app(ty_@2, hd), he), gd, ge) → new_lt3(vwx3410, vwx3610, hd, he)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(ty_Maybe, bdc), bdb) → new_lt0(vwx3410, vwx3610, bdc)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(app(app(ty_@3, beh), bfa), bfb)) → new_ltEs2(vwx3411, vwx3611, beh, bfa, bfb)
new_lt2(vwx340, vwx360, bcc, bcd, bce) → new_compare22(vwx340, vwx360, new_esEs6(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(ty_Maybe, bba)) → new_ltEs0(vwx3412, vwx3612, bba)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(ty_[], hg)), ge)) → new_lt(vwx3411, vwx3611, hg)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(app(app(ty_@3, bdf), bdg), bdh), bdb) → new_lt2(vwx3410, vwx3610, bdf, bdg, bdh)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(ty_Maybe, bee))) → new_ltEs0(vwx3411, vwx3611, bee)
new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(app(ty_@2, ga), gb)) → new_ltEs3(vwx3410, vwx3610, ga, gb)
new_compare(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_compare(vwx3401, vwx3601, ba)
new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, bch, app(ty_[], h)) → new_compare(vwx341, vwx361, h)
new_ltEs0(Just(vwx3410), Just(vwx3610), app(app(ty_Either, cf), cg)) → new_ltEs1(vwx3410, vwx3610, cf, cg)
new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(app(ty_Either, bef), beg))) → new_ltEs1(vwx3411, vwx3611, bef, beg)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(app(ty_Either, bbb), bbc))) → new_ltEs1(vwx3412, vwx3612, bbb, bbc)
new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(ty_Maybe, gf)), gd), ge)) → new_lt0(vwx3410, vwx3610, gf)
new_compare(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_primCompAux(vwx3400, vwx3600, new_compare0(vwx3401, vwx3601, ba), ba)
new_primCompAux(vwx3400, vwx3600, vwx101, app(app(ty_@2, ca), cb)) → new_compare4(vwx3400, vwx3600, ca, cb)
new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(app(app(ty_@3, ha), hb), hc), gd, ge) → new_lt2(vwx3410, vwx3610, ha, hb, hc)
new_compare1(vwx340, vwx360, cc) → new_compare20(vwx340, vwx360, new_esEs4(vwx340, vwx360, cc), cc)
new_compare23(@2(:(vwx3400, vwx3401), vwx341), @2(:(vwx3600, vwx3601), vwx361), False, app(ty_[], ba), bfe) → new_primCompAux(vwx3400, vwx3600, new_compare0(vwx3401, vwx3601, ba), ba)
new_lt1(vwx340, vwx360, bca, bcb) → new_compare21(vwx340, vwx360, new_esEs5(vwx340, vwx360, bca, bcb), bca, bcb)
new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(ty_[], bed)) → new_ltEs(vwx3411, vwx3611, bed)
new_compare4(vwx340, vwx360, bcf, bcg) → new_compare23(vwx340, vwx360, new_esEs7(vwx340, vwx360, bcf, bcg), bcf, bcg)
new_compare20(vwx340, vwx360, False, cc) → new_ltEs0(vwx340, vwx360, cc)
new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(app(ty_@2, bcf), bcg), bfe) → new_compare23(vwx340, vwx360, new_esEs7(vwx340, vwx360, bcf, bcg), bcf, bcg)
new_ltEs1(Left(vwx3410), Left(vwx3610), app(app(ty_@2, ef), eg), dg) → new_ltEs3(vwx3410, vwx3610, ef, eg)
The TRS R consists of the following rules:
new_esEs4(Just(vwx300), Just(vwx400), app(ty_Maybe, dac)) → new_esEs4(vwx300, vwx400, dac)
new_lt5(vwx3411, vwx3611, ty_Double) → new_lt18(vwx3411, vwx3611)
new_esEs25(vwx300, vwx400, ty_Char) → new_esEs19(vwx300, vwx400)
new_lt21(vwx340, vwx360, ty_Float) → new_lt13(vwx340, vwx360)
new_esEs24(vwx302, vwx402, app(app(ty_Either, cch), cda)) → new_esEs5(vwx302, vwx402, cch, cda)
new_esEs13(vwx3411, vwx3611, ty_Double) → new_esEs8(vwx3411, vwx3611)
new_ltEs19(vwx3411, vwx3611, ty_Char) → new_ltEs15(vwx3411, vwx3611)
new_ltEs20(vwx341, vwx361, app(ty_[], h)) → new_ltEs10(vwx341, vwx361, h)
new_esEs23(vwx301, vwx401, app(app(ty_Either, cbf), cbg)) → new_esEs5(vwx301, vwx401, cbf, cbg)
new_primCmpNat1(Zero, Succ(vwx360000)) → LT
new_ltEs6(vwx3412, vwx3612, ty_Integer) → new_ltEs9(vwx3412, vwx3612)
new_lt12(vwx340, vwx360, bca, bcb) → new_esEs10(new_compare7(vwx340, vwx360, bca, bcb), LT)
new_compare16(vwx340, vwx360, bcc, bcd, bce) → new_compare28(vwx340, vwx360, new_esEs6(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
new_esEs4(Just(vwx300), Nothing, cha) → False
new_esEs4(Nothing, Just(vwx400), cha) → False
new_esEs24(vwx302, vwx402, app(ty_Maybe, cdh)) → new_esEs4(vwx302, vwx402, cdh)
new_esEs29(vwx340, vwx360, ty_Int) → new_esEs9(vwx340, vwx360)
new_esEs20(vwx3410, vwx3610, ty_Int) → new_esEs9(vwx3410, vwx3610)
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_Bool) → new_ltEs11(vwx3410, vwx3610)
new_esEs23(vwx301, vwx401, ty_Float) → new_esEs17(vwx301, vwx401)
new_esEs26(vwx301, vwx401, ty_Float) → new_esEs17(vwx301, vwx401)
new_primMulNat0(Zero, Zero) → Zero
new_lt21(vwx340, vwx360, ty_@0) → new_lt17(vwx340, vwx360)
new_esEs5(Left(vwx300), Left(vwx400), ty_Bool, dbb) → new_esEs16(vwx300, vwx400)
new_compare14(vwx340, vwx360, cc) → new_compare24(vwx340, vwx360, new_esEs4(vwx340, vwx360, cc), cc)
new_esEs4(Just(vwx300), Just(vwx400), app(app(app(ty_@3, chh), daa), dab)) → new_esEs6(vwx300, vwx400, chh, daa, dab)
new_ltEs6(vwx3412, vwx3612, app(app(ty_Either, bbb), bbc)) → new_ltEs12(vwx3412, vwx3612, bbb, bbc)
new_compare26(vwx340, vwx360, False) → new_compare11(vwx340, vwx360, new_ltEs8(vwx340, vwx360))
new_ltEs6(vwx3412, vwx3612, app(app(app(ty_@3, bbd), bbe), bbf)) → new_ltEs5(vwx3412, vwx3612, bbd, bbe, bbf)
new_esEs20(vwx3410, vwx3610, app(ty_Maybe, bdc)) → new_esEs4(vwx3410, vwx3610, bdc)
new_esEs25(vwx300, vwx400, ty_Double) → new_esEs8(vwx300, vwx400)
new_esEs13(vwx3411, vwx3611, ty_Integer) → new_esEs14(vwx3411, vwx3611)
new_esEs18(:%(vwx300, vwx301), :%(vwx400, vwx401), cgg) → new_asAs(new_esEs27(vwx300, vwx400, cgg), new_esEs28(vwx301, vwx401, cgg))
new_esEs21(vwx300, vwx400, app(ty_[], bhc)) → new_esEs15(vwx300, vwx400, bhc)
new_lt20(vwx3410, vwx3610, app(app(ty_Either, bdd), bde)) → new_lt12(vwx3410, vwx3610, bdd, bde)
new_esEs25(vwx300, vwx400, app(ty_Ratio, cec)) → new_esEs18(vwx300, vwx400, cec)
new_lt21(vwx340, vwx360, app(ty_Ratio, dad)) → new_lt14(vwx340, vwx360, dad)
new_ltEs19(vwx3411, vwx3611, ty_Integer) → new_ltEs9(vwx3411, vwx3611)
new_esEs23(vwx301, vwx401, app(ty_Maybe, ccf)) → new_esEs4(vwx301, vwx401, ccf)
new_ltEs5(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, ge) → new_pePe(new_lt4(vwx3410, vwx3610, hf), new_asAs(new_esEs12(vwx3410, vwx3610, hf), new_pePe(new_lt5(vwx3411, vwx3611, gd), new_asAs(new_esEs13(vwx3411, vwx3611, gd), new_ltEs6(vwx3412, vwx3612, ge)))))
new_esEs26(vwx301, vwx401, ty_Ordering) → new_esEs10(vwx301, vwx401)
new_lt21(vwx340, vwx360, ty_Bool) → new_lt11(vwx340, vwx360)
new_ltEs20(vwx341, vwx361, app(app(ty_@2, bec), bdb)) → new_ltEs18(vwx341, vwx361, bec, bdb)
new_compare12(vwx83, vwx84, vwx85, vwx86, False, vwx88, bga, bgb) → new_compare13(vwx83, vwx84, vwx85, vwx86, vwx88, bga, bgb)
new_lt21(vwx340, vwx360, ty_Char) → new_lt16(vwx340, vwx360)
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_Double) → new_esEs8(vwx300, vwx400)
new_ltEs4(Just(vwx3410), Just(vwx3610), app(ty_[], cd)) → new_ltEs10(vwx3410, vwx3610, cd)
new_esEs26(vwx301, vwx401, ty_Double) → new_esEs8(vwx301, vwx401)
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_Integer) → new_esEs14(vwx300, vwx400)
new_primCmpNat1(Succ(vwx340000), Succ(vwx360000)) → new_primCmpNat1(vwx340000, vwx360000)
new_ltEs20(vwx341, vwx361, app(ty_Ratio, cgh)) → new_ltEs14(vwx341, vwx361, cgh)
new_ltEs8(EQ, EQ) → True
new_esEs23(vwx301, vwx401, ty_Ordering) → new_esEs10(vwx301, vwx401)
new_compare19(vwx340, vwx360) → new_compare27(vwx340, vwx360, new_esEs16(vwx340, vwx360))
new_esEs15(:(vwx300, vwx301), :(vwx400, vwx401), bge) → new_asAs(new_esEs21(vwx300, vwx400, bge), new_esEs15(vwx301, vwx401, bge))
new_ltEs6(vwx3412, vwx3612, app(ty_Maybe, bba)) → new_ltEs4(vwx3412, vwx3612, bba)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, app(ty_[], fa)) → new_ltEs10(vwx3410, vwx3610, fa)
new_ltEs19(vwx3411, vwx3611, app(ty_Maybe, bee)) → new_ltEs4(vwx3411, vwx3611, bee)
new_esEs26(vwx301, vwx401, ty_Integer) → new_esEs14(vwx301, vwx401)
new_ltEs14(vwx341, vwx361, cgh) → new_not(new_esEs10(new_compare18(vwx341, vwx361, cgh), GT))
new_esEs26(vwx301, vwx401, app(ty_Maybe, cgf)) → new_esEs4(vwx301, vwx401, cgf)
new_esEs5(Left(vwx300), Left(vwx400), ty_Char, dbb) → new_esEs19(vwx300, vwx400)
new_esEs4(Just(vwx300), Just(vwx400), app(ty_[], chg)) → new_esEs15(vwx300, vwx400, chg)
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_Double) → new_ltEs17(vwx3410, vwx3610)
new_esEs22(vwx300, vwx400, app(ty_Ratio, cac)) → new_esEs18(vwx300, vwx400, cac)
new_esEs13(vwx3411, vwx3611, app(ty_[], hg)) → new_esEs15(vwx3411, vwx3611, hg)
new_esEs12(vwx3410, vwx3610, app(ty_[], gc)) → new_esEs15(vwx3410, vwx3610, gc)
new_esEs5(Right(vwx300), Right(vwx400), dcd, app(app(app(ty_@3, ddc), ddd), dde)) → new_esEs6(vwx300, vwx400, ddc, ddd, dde)
new_ltEs6(vwx3412, vwx3612, ty_@0) → new_ltEs16(vwx3412, vwx3612)
new_pePe(False, vwx100) → vwx100
new_esEs25(vwx300, vwx400, app(app(ty_@2, cef), ceg)) → new_esEs7(vwx300, vwx400, cef, ceg)
new_lt20(vwx3410, vwx3610, ty_Bool) → new_lt11(vwx3410, vwx3610)
new_compare6(@0, @0) → EQ
new_compare32(vwx3400, vwx3600, ty_Double) → new_compare5(vwx3400, vwx3600)
new_ltEs12(Left(vwx3410), Left(vwx3610), app(ty_Maybe, dh), dg) → new_ltEs4(vwx3410, vwx3610, dh)
new_lt5(vwx3411, vwx3611, ty_@0) → new_lt17(vwx3411, vwx3611)
new_ltEs6(vwx3412, vwx3612, ty_Ordering) → new_ltEs8(vwx3412, vwx3612)
new_esEs13(vwx3411, vwx3611, app(ty_Maybe, hh)) → new_esEs4(vwx3411, vwx3611, hh)
new_esEs23(vwx301, vwx401, ty_Double) → new_esEs8(vwx301, vwx401)
new_ltEs16(vwx341, vwx361) → new_not(new_esEs10(new_compare6(vwx341, vwx361), GT))
new_ltEs4(Nothing, Just(vwx3610), dae) → True
new_esEs24(vwx302, vwx402, ty_@0) → new_esEs11(vwx302, vwx402)
new_esEs7(@2(vwx300, vwx301), @2(vwx400, vwx401), cea, ceb) → new_asAs(new_esEs25(vwx300, vwx400, cea), new_esEs26(vwx301, vwx401, ceb))
new_ltEs20(vwx341, vwx361, ty_Ordering) → new_ltEs8(vwx341, vwx361)
new_esEs5(Left(vwx300), Left(vwx400), ty_Double, dbb) → new_esEs8(vwx300, vwx400)
new_esEs20(vwx3410, vwx3610, ty_Ordering) → new_esEs10(vwx3410, vwx3610)
new_ltEs8(EQ, GT) → True
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, app(ty_Ratio, dah)) → new_ltEs14(vwx3410, vwx3610, dah)
new_ltEs11(False, True) → True
new_ltEs8(GT, GT) → True
new_ltEs18(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, bdb) → new_pePe(new_lt20(vwx3410, vwx3610, bec), new_asAs(new_esEs20(vwx3410, vwx3610, bec), new_ltEs19(vwx3411, vwx3611, bdb)))
new_compare111(vwx340, vwx360, False) → GT
new_esEs14(Integer(vwx300), Integer(vwx400)) → new_primEqInt(vwx300, vwx400)
new_compare111(vwx340, vwx360, True) → LT
new_compare10(vwx340, vwx360, True, cc) → LT
new_esEs26(vwx301, vwx401, ty_Char) → new_esEs19(vwx301, vwx401)
new_ltEs19(vwx3411, vwx3611, ty_Double) → new_ltEs17(vwx3411, vwx3611)
new_esEs5(Left(vwx300), Left(vwx400), app(ty_Maybe, dcc), dbb) → new_esEs4(vwx300, vwx400, dcc)
new_esEs20(vwx3410, vwx3610, ty_Bool) → new_esEs16(vwx3410, vwx3610)
new_ltEs19(vwx3411, vwx3611, ty_Int) → new_ltEs7(vwx3411, vwx3611)
new_esEs25(vwx300, vwx400, ty_Bool) → new_esEs16(vwx300, vwx400)
new_esEs25(vwx300, vwx400, app(app(ty_Either, ced), cee)) → new_esEs5(vwx300, vwx400, ced, cee)
new_lt5(vwx3411, vwx3611, ty_Integer) → new_lt8(vwx3411, vwx3611)
new_lt18(vwx340, vwx360) → new_esEs10(new_compare5(vwx340, vwx360), LT)
new_ltEs8(LT, EQ) → True
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_Float) → new_ltEs13(vwx3410, vwx3610)
new_esEs13(vwx3411, vwx3611, ty_Float) → new_esEs17(vwx3411, vwx3611)
new_esEs20(vwx3410, vwx3610, ty_@0) → new_esEs11(vwx3410, vwx3610)
new_esEs29(vwx340, vwx360, app(app(ty_@2, bcf), bcg)) → new_esEs7(vwx340, vwx360, bcf, bcg)
new_esEs10(LT, LT) → True
new_esEs10(EQ, GT) → False
new_esEs10(GT, EQ) → False
new_compare10(vwx340, vwx360, False, cc) → GT
new_ltEs4(Just(vwx3410), Just(vwx3610), app(ty_Ratio, daf)) → new_ltEs14(vwx3410, vwx3610, daf)
new_lt20(vwx3410, vwx3610, app(app(ty_@2, bea), beb)) → new_lt19(vwx3410, vwx3610, bea, beb)
new_esEs20(vwx3410, vwx3610, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs6(vwx3410, vwx3610, bdf, bdg, bdh)
new_compare0([], [], ba) → EQ
new_pePe(True, vwx100) → True
new_primEqNat0(Zero, Zero) → True
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_@0) → new_ltEs16(vwx3410, vwx3610)
new_lt11(vwx340, vwx360) → new_esEs10(new_compare19(vwx340, vwx360), LT)
new_compare26(vwx340, vwx360, True) → EQ
new_esEs23(vwx301, vwx401, ty_@0) → new_esEs11(vwx301, vwx401)
new_compare13(vwx83, vwx84, vwx85, vwx86, False, bga, bgb) → GT
new_esEs22(vwx300, vwx400, ty_@0) → new_esEs11(vwx300, vwx400)
new_lt16(vwx340, vwx360) → new_esEs10(new_compare30(vwx340, vwx360), LT)
new_esEs5(Left(vwx300), Left(vwx400), ty_Int, dbb) → new_esEs9(vwx300, vwx400)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_Char) → new_ltEs15(vwx3410, vwx3610)
new_lt20(vwx3410, vwx3610, app(ty_[], bda)) → new_lt9(vwx3410, vwx3610, bda)
new_lt6(vwx340, vwx360) → new_esEs10(new_compare8(vwx340, vwx360), LT)
new_esEs22(vwx300, vwx400, app(app(ty_@2, caf), cag)) → new_esEs7(vwx300, vwx400, caf, cag)
new_esEs12(vwx3410, vwx3610, ty_Float) → new_esEs17(vwx3410, vwx3610)
new_compare31(Float(vwx3400, vwx3401), Float(vwx3600, vwx3601)) → new_compare8(new_sr(vwx3400, vwx3600), new_sr(vwx3401, vwx3601))
new_ltEs4(Just(vwx3410), Just(vwx3610), app(app(ty_@2, dd), de)) → new_ltEs18(vwx3410, vwx3610, dd, de)
new_ltEs8(GT, EQ) → False
new_ltEs8(EQ, LT) → False
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_Integer, dg) → new_ltEs9(vwx3410, vwx3610)
new_lt4(vwx3410, vwx3610, ty_Bool) → new_lt11(vwx3410, vwx3610)
new_esEs26(vwx301, vwx401, ty_Bool) → new_esEs16(vwx301, vwx401)
new_esEs12(vwx3410, vwx3610, ty_Ordering) → new_esEs10(vwx3410, vwx3610)
new_compare32(vwx3400, vwx3600, app(app(ty_@2, ca), cb)) → new_compare29(vwx3400, vwx3600, ca, cb)
new_esEs12(vwx3410, vwx3610, app(app(ty_@2, hd), he)) → new_esEs7(vwx3410, vwx3610, hd, he)
new_sr(vwx301, vwx401) → new_primMulInt(vwx301, vwx401)
new_primCmpNat1(Zero, Zero) → EQ
new_esEs25(vwx300, vwx400, app(ty_[], ceh)) → new_esEs15(vwx300, vwx400, ceh)
new_esEs23(vwx301, vwx401, app(ty_[], ccb)) → new_esEs15(vwx301, vwx401, ccb)
new_esEs24(vwx302, vwx402, app(app(ty_@2, cdb), cdc)) → new_esEs7(vwx302, vwx402, cdb, cdc)
new_esEs13(vwx3411, vwx3611, app(app(app(ty_@3, bac), bad), bae)) → new_esEs6(vwx3411, vwx3611, bac, bad, bae)
new_esEs13(vwx3411, vwx3611, ty_Int) → new_esEs9(vwx3411, vwx3611)
new_lt5(vwx3411, vwx3611, app(ty_[], hg)) → new_lt9(vwx3411, vwx3611, hg)
new_esEs4(Just(vwx300), Just(vwx400), ty_Integer) → new_esEs14(vwx300, vwx400)
new_esEs24(vwx302, vwx402, ty_Char) → new_esEs19(vwx302, vwx402)
new_esEs5(Right(vwx300), Right(vwx400), dcd, app(ty_Ratio, dce)) → new_esEs18(vwx300, vwx400, dce)
new_compare32(vwx3400, vwx3600, ty_@0) → new_compare6(vwx3400, vwx3600)
new_esEs12(vwx3410, vwx3610, ty_Char) → new_esEs19(vwx3410, vwx3610)
new_primPlusNat0(Succ(vwx740), vwx40100) → Succ(Succ(new_primPlusNat1(vwx740, vwx40100)))
new_esEs20(vwx3410, vwx3610, ty_Double) → new_esEs8(vwx3410, vwx3610)
new_lt21(vwx340, vwx360, ty_Double) → new_lt18(vwx340, vwx360)
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_Float) → new_ltEs13(vwx3410, vwx3610)
new_esEs26(vwx301, vwx401, app(app(app(ty_@3, cgc), cgd), cge)) → new_esEs6(vwx301, vwx401, cgc, cgd, cge)
new_ltEs19(vwx3411, vwx3611, app(ty_Ratio, bgd)) → new_ltEs14(vwx3411, vwx3611, bgd)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, app(app(ty_@2, ga), gb)) → new_ltEs18(vwx3410, vwx3610, ga, gb)
new_ltEs7(vwx341, vwx361) → new_not(new_esEs10(new_compare8(vwx341, vwx361), GT))
new_primCmpNat1(Succ(vwx340000), Zero) → GT
new_ltEs6(vwx3412, vwx3612, ty_Double) → new_ltEs17(vwx3412, vwx3612)
new_compare17(vwx340, vwx360, True, bca, bcb) → LT
new_ltEs20(vwx341, vwx361, app(app(app(ty_@3, hf), gd), ge)) → new_ltEs5(vwx341, vwx361, hf, gd, ge)
new_esEs13(vwx3411, vwx3611, ty_Char) → new_esEs19(vwx3411, vwx3611)
new_esEs4(Just(vwx300), Just(vwx400), app(ty_Ratio, chb)) → new_esEs18(vwx300, vwx400, chb)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, app(app(app(ty_@3, ff), fg), fh)) → new_ltEs5(vwx3410, vwx3610, ff, fg, fh)
new_esEs10(EQ, EQ) → True
new_primEqInt(Neg(Succ(vwx3000)), Neg(Succ(vwx4000))) → new_primEqNat0(vwx3000, vwx4000)
new_esEs12(vwx3410, vwx3610, ty_Integer) → new_esEs14(vwx3410, vwx3610)
new_ltEs19(vwx3411, vwx3611, ty_Ordering) → new_ltEs8(vwx3411, vwx3611)
new_lt21(vwx340, vwx360, ty_Int) → new_lt6(vwx340, vwx360)
new_esEs22(vwx300, vwx400, app(app(app(ty_@3, cba), cbb), cbc)) → new_esEs6(vwx300, vwx400, cba, cbb, cbc)
new_lt19(vwx340, vwx360, bcf, bcg) → new_esEs10(new_compare29(vwx340, vwx360, bcf, bcg), LT)
new_esEs21(vwx300, vwx400, ty_Ordering) → new_esEs10(vwx300, vwx400)
new_primPlusNat1(Succ(vwx7400), Zero) → Succ(vwx7400)
new_primPlusNat1(Zero, Succ(vwx401000)) → Succ(vwx401000)
new_ltEs4(Nothing, Nothing, dae) → True
new_esEs29(vwx340, vwx360, app(app(ty_Either, bca), bcb)) → new_esEs5(vwx340, vwx360, bca, bcb)
new_ltEs12(Left(vwx3410), Left(vwx3610), app(app(app(ty_@3, ec), ed), ee), dg) → new_ltEs5(vwx3410, vwx3610, ec, ed, ee)
new_esEs16(True, False) → False
new_esEs16(False, True) → False
new_ltEs6(vwx3412, vwx3612, ty_Float) → new_ltEs13(vwx3412, vwx3612)
new_compare32(vwx3400, vwx3600, ty_Bool) → new_compare19(vwx3400, vwx3600)
new_esEs19(Char(vwx300), Char(vwx400)) → new_primEqInt(vwx300, vwx400)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_compare27(vwx340, vwx360, False) → new_compare111(vwx340, vwx360, new_ltEs11(vwx340, vwx360))
new_ltEs17(vwx341, vwx361) → new_not(new_esEs10(new_compare5(vwx341, vwx361), GT))
new_ltEs20(vwx341, vwx361, ty_Bool) → new_ltEs11(vwx341, vwx361)
new_esEs24(vwx302, vwx402, app(app(app(ty_@3, cde), cdf), cdg)) → new_esEs6(vwx302, vwx402, cde, cdf, cdg)
new_esEs21(vwx300, vwx400, ty_Double) → new_esEs8(vwx300, vwx400)
new_esEs21(vwx300, vwx400, app(app(ty_@2, bha), bhb)) → new_esEs7(vwx300, vwx400, bha, bhb)
new_lt20(vwx3410, vwx3610, ty_Ordering) → new_lt7(vwx3410, vwx3610)
new_primCmpNat0(Succ(vwx36000), vwx34000) → new_primCmpNat1(vwx36000, vwx34000)
new_compare8(vwx340, vwx360) → new_primCmpInt(vwx340, vwx360)
new_primEqInt(Neg(Succ(vwx3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vwx4000))) → False
new_primCompAux0(vwx106, GT) → GT
new_lt20(vwx3410, vwx3610, ty_Integer) → new_lt8(vwx3410, vwx3610)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_Ordering) → new_ltEs8(vwx3410, vwx3610)
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_@0, dg) → new_ltEs16(vwx3410, vwx3610)
new_lt20(vwx3410, vwx3610, ty_Char) → new_lt16(vwx3410, vwx3610)
new_compare28(vwx340, vwx360, False, bcc, bcd, bce) → new_compare110(vwx340, vwx360, new_ltEs5(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
new_esEs21(vwx300, vwx400, ty_Float) → new_esEs17(vwx300, vwx400)
new_lt21(vwx340, vwx360, app(ty_[], ba)) → new_lt9(vwx340, vwx360, ba)
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_Int) → new_esEs9(vwx300, vwx400)
new_esEs24(vwx302, vwx402, ty_Ordering) → new_esEs10(vwx302, vwx402)
new_esEs26(vwx301, vwx401, ty_@0) → new_esEs11(vwx301, vwx401)
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_esEs29(vwx340, vwx360, ty_Bool) → new_esEs16(vwx340, vwx360)
new_esEs23(vwx301, vwx401, ty_Integer) → new_esEs14(vwx301, vwx401)
new_compare32(vwx3400, vwx3600, app(ty_[], bb)) → new_compare0(vwx3400, vwx3600, bb)
new_compare12(vwx83, vwx84, vwx85, vwx86, True, vwx88, bga, bgb) → new_compare13(vwx83, vwx84, vwx85, vwx86, True, bga, bgb)
new_ltEs12(Left(vwx3410), Left(vwx3610), app(ty_Ratio, dag), dg) → new_ltEs14(vwx3410, vwx3610, dag)
new_compare7(vwx340, vwx360, bca, bcb) → new_compare25(vwx340, vwx360, new_esEs5(vwx340, vwx360, bca, bcb), bca, bcb)
new_esEs22(vwx300, vwx400, app(ty_Maybe, cbd)) → new_esEs4(vwx300, vwx400, cbd)
new_esEs22(vwx300, vwx400, ty_Double) → new_esEs8(vwx300, vwx400)
new_esEs25(vwx300, vwx400, app(ty_Maybe, cfd)) → new_esEs4(vwx300, vwx400, cfd)
new_ltEs9(vwx341, vwx361) → new_not(new_esEs10(new_compare15(vwx341, vwx361), GT))
new_primEqInt(Pos(Succ(vwx3000)), Pos(Succ(vwx4000))) → new_primEqNat0(vwx3000, vwx4000)
new_esEs12(vwx3410, vwx3610, ty_Double) → new_esEs8(vwx3410, vwx3610)
new_esEs13(vwx3411, vwx3611, ty_@0) → new_esEs11(vwx3411, vwx3611)
new_esEs29(vwx340, vwx360, ty_Double) → new_esEs8(vwx340, vwx360)
new_esEs25(vwx300, vwx400, ty_Int) → new_esEs9(vwx300, vwx400)
new_ltEs11(True, False) → False
new_esEs5(Left(vwx300), Left(vwx400), ty_@0, dbb) → new_esEs11(vwx300, vwx400)
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_@0) → new_ltEs16(vwx3410, vwx3610)
new_ltEs20(vwx341, vwx361, ty_@0) → new_ltEs16(vwx341, vwx361)
new_esEs5(Right(vwx300), Right(vwx400), dcd, app(app(ty_Either, dcf), dcg)) → new_esEs5(vwx300, vwx400, dcf, dcg)
new_primEqNat0(Succ(vwx30000), Succ(vwx40000)) → new_primEqNat0(vwx30000, vwx40000)
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_Ordering, dg) → new_ltEs8(vwx3410, vwx3610)
new_esEs24(vwx302, vwx402, app(ty_Ratio, ccg)) → new_esEs18(vwx302, vwx402, ccg)
new_primCompAux1(vwx3400, vwx3600, vwx101, ba) → new_primCompAux0(vwx101, new_compare32(vwx3400, vwx3600, ba))
new_lt17(vwx340, vwx360) → new_esEs10(new_compare6(vwx340, vwx360), LT)
new_esEs22(vwx300, vwx400, ty_Bool) → new_esEs16(vwx300, vwx400)
new_lt14(vwx340, vwx360, dad) → new_esEs10(new_compare18(vwx340, vwx360, dad), LT)
new_ltEs6(vwx3412, vwx3612, app(ty_Ratio, bfh)) → new_ltEs14(vwx3412, vwx3612, bfh)
new_lt13(vwx340, vwx360) → new_esEs10(new_compare31(vwx340, vwx360), LT)
new_esEs12(vwx3410, vwx3610, app(ty_Ratio, bff)) → new_esEs18(vwx3410, vwx3610, bff)
new_lt5(vwx3411, vwx3611, ty_Char) → new_lt16(vwx3411, vwx3611)
new_esEs15([], [], bge) → True
new_primEqInt(Pos(Succ(vwx3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vwx4000))) → False
new_esEs25(vwx300, vwx400, ty_Float) → new_esEs17(vwx300, vwx400)
new_lt4(vwx3410, vwx3610, app(ty_[], gc)) → new_lt9(vwx3410, vwx3610, gc)
new_compare18(:%(vwx3400, vwx3401), :%(vwx3600, vwx3601), ty_Int) → new_compare8(new_sr(vwx3400, vwx3601), new_sr(vwx3600, vwx3401))
new_esEs22(vwx300, vwx400, ty_Integer) → new_esEs14(vwx300, vwx400)
new_primCmpInt(Neg(Zero), Pos(Succ(vwx36000))) → LT
new_esEs4(Just(vwx300), Just(vwx400), app(app(ty_Either, chc), chd)) → new_esEs5(vwx300, vwx400, chc, chd)
new_esEs20(vwx3410, vwx3610, app(app(ty_Either, bdd), bde)) → new_esEs5(vwx3410, vwx3610, bdd, bde)
new_compare25(vwx340, vwx360, False, bca, bcb) → new_compare17(vwx340, vwx360, new_ltEs12(vwx340, vwx360, bca, bcb), bca, bcb)
new_compare32(vwx3400, vwx3600, app(app(app(ty_@3, bf), bg), bh)) → new_compare16(vwx3400, vwx3600, bf, bg, bh)
new_sr0(Integer(vwx34000), Integer(vwx36010)) → Integer(new_primMulInt(vwx34000, vwx36010))
new_lt21(vwx340, vwx360, ty_Integer) → new_lt8(vwx340, vwx360)
new_primPlusNat1(Succ(vwx7400), Succ(vwx401000)) → Succ(Succ(new_primPlusNat1(vwx7400, vwx401000)))
new_esEs29(vwx340, vwx360, app(ty_Ratio, dad)) → new_esEs18(vwx340, vwx360, dad)
new_lt21(vwx340, vwx360, app(ty_Maybe, cc)) → new_lt10(vwx340, vwx360, cc)
new_primEqInt(Pos(Succ(vwx3000)), Neg(vwx400)) → False
new_primEqInt(Neg(Succ(vwx3000)), Pos(vwx400)) → False
new_esEs5(Left(vwx300), Left(vwx400), app(ty_Ratio, dba), dbb) → new_esEs18(vwx300, vwx400, dba)
new_ltEs10(vwx341, vwx361, h) → new_not(new_esEs10(new_compare0(vwx341, vwx361, h), GT))
new_ltEs12(Left(vwx3410), Right(vwx3610), eh, dg) → True
new_esEs29(vwx340, vwx360, ty_Char) → new_esEs19(vwx340, vwx360)
new_ltEs12(Left(vwx3410), Left(vwx3610), app(ty_[], df), dg) → new_ltEs10(vwx3410, vwx3610, df)
new_esEs4(Just(vwx300), Just(vwx400), ty_Bool) → new_esEs16(vwx300, vwx400)
new_lt21(vwx340, vwx360, app(app(ty_Either, bca), bcb)) → new_lt12(vwx340, vwx360, bca, bcb)
new_esEs26(vwx301, vwx401, ty_Int) → new_esEs9(vwx301, vwx401)
new_primEqInt(Pos(Zero), Neg(Succ(vwx4000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vwx4000))) → False
new_primCmpNat0(Zero, vwx34000) → LT
new_ltEs6(vwx3412, vwx3612, ty_Bool) → new_ltEs11(vwx3412, vwx3612)
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_Int) → new_ltEs7(vwx3410, vwx3610)
new_ltEs8(GT, LT) → False
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_Bool) → new_ltEs11(vwx3410, vwx3610)
new_esEs20(vwx3410, vwx3610, ty_Char) → new_esEs19(vwx3410, vwx3610)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, app(ty_Maybe, fb)) → new_ltEs4(vwx3410, vwx3610, fb)
new_esEs4(Just(vwx300), Just(vwx400), ty_Int) → new_esEs9(vwx300, vwx400)
new_compare32(vwx3400, vwx3600, ty_Char) → new_compare30(vwx3400, vwx3600)
new_ltEs15(vwx341, vwx361) → new_not(new_esEs10(new_compare30(vwx341, vwx361), GT))
new_lt4(vwx3410, vwx3610, ty_Integer) → new_lt8(vwx3410, vwx3610)
new_lt4(vwx3410, vwx3610, ty_Float) → new_lt13(vwx3410, vwx3610)
new_compare17(vwx340, vwx360, False, bca, bcb) → GT
new_esEs5(Left(vwx300), Left(vwx400), app(ty_[], dbg), dbb) → new_esEs15(vwx300, vwx400, dbg)
new_esEs4(Just(vwx300), Just(vwx400), ty_Double) → new_esEs8(vwx300, vwx400)
new_compare5(Double(vwx3400, vwx3401), Double(vwx3600, vwx3601)) → new_compare8(new_sr(vwx3400, vwx3600), new_sr(vwx3401, vwx3601))
new_primCompAux0(vwx106, LT) → LT
new_esEs21(vwx300, vwx400, ty_Integer) → new_esEs14(vwx300, vwx400)
new_not(False) → True
new_esEs4(Just(vwx300), Just(vwx400), ty_@0) → new_esEs11(vwx300, vwx400)
new_esEs21(vwx300, vwx400, ty_Bool) → new_esEs16(vwx300, vwx400)
new_compare24(vwx340, vwx360, True, cc) → EQ
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_Ordering) → new_esEs10(vwx300, vwx400)
new_compare210(vwx34, vwx36, True, bch, bfe) → EQ
new_primPlusNat0(Zero, vwx40100) → Succ(vwx40100)
new_ltEs19(vwx3411, vwx3611, app(ty_[], bed)) → new_ltEs10(vwx3411, vwx3611, bed)
new_ltEs19(vwx3411, vwx3611, app(app(ty_Either, bef), beg)) → new_ltEs12(vwx3411, vwx3611, bef, beg)
new_esEs5(Left(vwx300), Left(vwx400), ty_Float, dbb) → new_esEs17(vwx300, vwx400)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, app(app(ty_Either, fc), fd)) → new_ltEs12(vwx3410, vwx3610, fc, fd)
new_esEs26(vwx301, vwx401, app(ty_Ratio, cfe)) → new_esEs18(vwx301, vwx401, cfe)
new_lt20(vwx3410, vwx3610, app(app(app(ty_@3, bdf), bdg), bdh)) → new_lt15(vwx3410, vwx3610, bdf, bdg, bdh)
new_ltEs12(Right(vwx3410), Left(vwx3610), eh, dg) → False
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_Double, dg) → new_ltEs17(vwx3410, vwx3610)
new_esEs13(vwx3411, vwx3611, app(app(ty_Either, baa), bab)) → new_esEs5(vwx3411, vwx3611, baa, bab)
new_lt9(vwx340, vwx360, ba) → new_esEs10(new_compare0(vwx340, vwx360, ba), LT)
new_lt20(vwx3410, vwx3610, app(ty_Ratio, bgc)) → new_lt14(vwx3410, vwx3610, bgc)
new_esEs5(Right(vwx300), Right(vwx400), dcd, app(ty_[], ddb)) → new_esEs15(vwx300, vwx400, ddb)
new_esEs24(vwx302, vwx402, ty_Float) → new_esEs17(vwx302, vwx402)
new_compare0(:(vwx3400, vwx3401), [], ba) → GT
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_Ordering) → new_ltEs8(vwx3410, vwx3610)
new_ltEs11(False, False) → True
new_lt15(vwx340, vwx360, bcc, bcd, bce) → new_esEs10(new_compare16(vwx340, vwx360, bcc, bcd, bce), LT)
new_lt20(vwx3410, vwx3610, ty_Int) → new_lt6(vwx3410, vwx3610)
new_esEs26(vwx301, vwx401, app(app(ty_Either, cff), cfg)) → new_esEs5(vwx301, vwx401, cff, cfg)
new_lt5(vwx3411, vwx3611, app(app(app(ty_@3, bac), bad), bae)) → new_lt15(vwx3411, vwx3611, bac, bad, bae)
new_primCmpInt(Pos(Succ(vwx34000)), Neg(vwx3600)) → GT
new_ltEs13(vwx341, vwx361) → new_not(new_esEs10(new_compare31(vwx341, vwx361), GT))
new_primCmpInt(Pos(Zero), Pos(Succ(vwx36000))) → new_primCmpNat0(Zero, vwx36000)
new_ltEs4(Just(vwx3410), Just(vwx3610), app(app(app(ty_@3, da), db), dc)) → new_ltEs5(vwx3410, vwx3610, da, db, dc)
new_ltEs19(vwx3411, vwx3611, ty_Float) → new_ltEs13(vwx3411, vwx3611)
new_esEs5(Left(vwx300), Left(vwx400), ty_Ordering, dbb) → new_esEs10(vwx300, vwx400)
new_primMulInt(Pos(vwx3010), Pos(vwx4010)) → Pos(new_primMulNat0(vwx3010, vwx4010))
new_esEs29(vwx340, vwx360, ty_Integer) → new_esEs14(vwx340, vwx360)
new_lt4(vwx3410, vwx3610, ty_Double) → new_lt18(vwx3410, vwx3610)
new_compare18(:%(vwx3400, vwx3401), :%(vwx3600, vwx3601), ty_Integer) → new_compare15(new_sr0(vwx3400, vwx3601), new_sr0(vwx3600, vwx3401))
new_compare210(@2(vwx340, vwx341), @2(vwx360, vwx361), False, bch, bfe) → new_compare12(vwx340, vwx341, vwx360, vwx361, new_lt21(vwx340, vwx360, bch), new_asAs(new_esEs29(vwx340, vwx360, bch), new_ltEs20(vwx341, vwx361, bfe)), bch, bfe)
new_esEs5(Left(vwx300), Right(vwx400), dcd, dbb) → False
new_esEs5(Right(vwx300), Left(vwx400), dcd, dbb) → False
new_primMulInt(Neg(vwx3010), Neg(vwx4010)) → Pos(new_primMulNat0(vwx3010, vwx4010))
new_esEs13(vwx3411, vwx3611, ty_Bool) → new_esEs16(vwx3411, vwx3611)
new_primEqNat0(Succ(vwx30000), Zero) → False
new_primEqNat0(Zero, Succ(vwx40000)) → False
new_esEs22(vwx300, vwx400, ty_Float) → new_esEs17(vwx300, vwx400)
new_esEs21(vwx300, vwx400, ty_Int) → new_esEs9(vwx300, vwx400)
new_lt4(vwx3410, vwx3610, app(app(app(ty_@3, ha), hb), hc)) → new_lt15(vwx3410, vwx3610, ha, hb, hc)
new_esEs26(vwx301, vwx401, app(app(ty_@2, cfh), cga)) → new_esEs7(vwx301, vwx401, cfh, cga)
new_esEs12(vwx3410, vwx3610, ty_@0) → new_esEs11(vwx3410, vwx3610)
new_esEs17(Float(vwx300, vwx301), Float(vwx400, vwx401)) → new_esEs9(new_sr(vwx300, vwx400), new_sr(vwx301, vwx401))
new_esEs5(Left(vwx300), Left(vwx400), ty_Integer, dbb) → new_esEs14(vwx300, vwx400)
new_compare25(vwx340, vwx360, True, bca, bcb) → EQ
new_ltEs20(vwx341, vwx361, ty_Char) → new_ltEs15(vwx341, vwx361)
new_lt20(vwx3410, vwx3610, ty_@0) → new_lt17(vwx3410, vwx3610)
new_lt20(vwx3410, vwx3610, app(ty_Maybe, bdc)) → new_lt10(vwx3410, vwx3610, bdc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(vwx301, vwx401, app(ty_Ratio, cbe)) → new_esEs18(vwx301, vwx401, cbe)
new_esEs4(Nothing, Nothing, cha) → True
new_ltEs20(vwx341, vwx361, ty_Int) → new_ltEs7(vwx341, vwx361)
new_esEs13(vwx3411, vwx3611, app(app(ty_@2, baf), bag)) → new_esEs7(vwx3411, vwx3611, baf, bag)
new_esEs11(@0, @0) → True
new_esEs12(vwx3410, vwx3610, app(app(ty_Either, gg), gh)) → new_esEs5(vwx3410, vwx3610, gg, gh)
new_esEs25(vwx300, vwx400, ty_@0) → new_esEs11(vwx300, vwx400)
new_esEs22(vwx300, vwx400, ty_Int) → new_esEs9(vwx300, vwx400)
new_ltEs12(Left(vwx3410), Left(vwx3610), app(app(ty_Either, ea), eb), dg) → new_ltEs12(vwx3410, vwx3610, ea, eb)
new_ltEs6(vwx3412, vwx3612, ty_Int) → new_ltEs7(vwx3412, vwx3612)
new_compare28(vwx340, vwx360, True, bcc, bcd, bce) → EQ
new_lt21(vwx340, vwx360, ty_Ordering) → new_lt7(vwx340, vwx360)
new_lt4(vwx3410, vwx3610, ty_Char) → new_lt16(vwx3410, vwx3610)
new_esEs12(vwx3410, vwx3610, ty_Int) → new_esEs9(vwx3410, vwx3610)
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_Bool) → new_esEs16(vwx300, vwx400)
new_primCmpInt(Neg(Zero), Neg(Succ(vwx36000))) → new_primCmpNat2(vwx36000, Zero)
new_ltEs20(vwx341, vwx361, ty_Double) → new_ltEs17(vwx341, vwx361)
new_esEs12(vwx3410, vwx3610, ty_Bool) → new_esEs16(vwx3410, vwx3610)
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_Char) → new_esEs19(vwx300, vwx400)
new_esEs24(vwx302, vwx402, ty_Int) → new_esEs9(vwx302, vwx402)
new_lt4(vwx3410, vwx3610, ty_Int) → new_lt6(vwx3410, vwx3610)
new_esEs16(True, True) → True
new_esEs22(vwx300, vwx400, app(ty_[], cah)) → new_esEs15(vwx300, vwx400, cah)
new_primCmpInt(Pos(Zero), Neg(Succ(vwx36000))) → GT
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_Float) → new_esEs17(vwx300, vwx400)
new_esEs6(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), bhh, caa, cab) → new_asAs(new_esEs22(vwx300, vwx400, bhh), new_asAs(new_esEs23(vwx301, vwx401, caa), new_esEs24(vwx302, vwx402, cab)))
new_esEs24(vwx302, vwx402, ty_Bool) → new_esEs16(vwx302, vwx402)
new_esEs25(vwx300, vwx400, ty_Integer) → new_esEs14(vwx300, vwx400)
new_compare0(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_primCompAux1(vwx3400, vwx3600, new_compare0(vwx3401, vwx3601, ba), ba)
new_ltEs20(vwx341, vwx361, ty_Float) → new_ltEs13(vwx341, vwx361)
new_lt20(vwx3410, vwx3610, ty_Double) → new_lt18(vwx3410, vwx3610)
new_esEs27(vwx300, vwx400, ty_Int) → new_esEs9(vwx300, vwx400)
new_ltEs4(Just(vwx3410), Just(vwx3610), app(app(ty_Either, cf), cg)) → new_ltEs12(vwx3410, vwx3610, cf, cg)
new_compare32(vwx3400, vwx3600, ty_Int) → new_compare8(vwx3400, vwx3600)
new_esEs20(vwx3410, vwx3610, app(ty_Ratio, bgc)) → new_esEs18(vwx3410, vwx3610, bgc)
new_esEs15([], :(vwx400, vwx401), bge) → False
new_esEs15(:(vwx300, vwx301), [], bge) → False
new_compare32(vwx3400, vwx3600, app(app(ty_Either, bd), be)) → new_compare7(vwx3400, vwx3600, bd, be)
new_esEs13(vwx3411, vwx3611, app(ty_Ratio, bfg)) → new_esEs18(vwx3411, vwx3611, bfg)
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_Bool, dg) → new_ltEs11(vwx3410, vwx3610)
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_Char, dg) → new_ltEs15(vwx3410, vwx3610)
new_esEs21(vwx300, vwx400, app(ty_Maybe, bhg)) → new_esEs4(vwx300, vwx400, bhg)
new_esEs22(vwx300, vwx400, ty_Char) → new_esEs19(vwx300, vwx400)
new_esEs4(Just(vwx300), Just(vwx400), ty_Ordering) → new_esEs10(vwx300, vwx400)
new_ltEs4(Just(vwx3410), Just(vwx3610), app(ty_Maybe, ce)) → new_ltEs4(vwx3410, vwx3610, ce)
new_esEs5(Left(vwx300), Left(vwx400), app(app(ty_@2, dbe), dbf), dbb) → new_esEs7(vwx300, vwx400, dbe, dbf)
new_primCmpNat2(vwx34000, Succ(vwx36000)) → new_primCmpNat1(vwx34000, vwx36000)
new_ltEs19(vwx3411, vwx3611, app(app(ty_@2, bfc), bfd)) → new_ltEs18(vwx3411, vwx3611, bfc, bfd)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_Int) → new_ltEs7(vwx3410, vwx3610)
new_ltEs20(vwx341, vwx361, app(app(ty_Either, eh), dg)) → new_ltEs12(vwx341, vwx361, eh, dg)
new_esEs12(vwx3410, vwx3610, app(ty_Maybe, gf)) → new_esEs4(vwx3410, vwx3610, gf)
new_asAs(False, vwx51) → False
new_ltEs11(True, True) → True
new_lt8(vwx340, vwx360) → new_esEs10(new_compare15(vwx340, vwx360), LT)
new_primMulInt(Neg(vwx3010), Pos(vwx4010)) → Neg(new_primMulNat0(vwx3010, vwx4010))
new_primMulInt(Pos(vwx3010), Neg(vwx4010)) → Neg(new_primMulNat0(vwx3010, vwx4010))
new_lt4(vwx3410, vwx3610, ty_Ordering) → new_lt7(vwx3410, vwx3610)
new_primMulNat0(Succ(vwx30100), Zero) → Zero
new_primMulNat0(Zero, Succ(vwx40100)) → Zero
new_esEs21(vwx300, vwx400, app(app(ty_Either, bgg), bgh)) → new_esEs5(vwx300, vwx400, bgg, bgh)
new_lt5(vwx3411, vwx3611, ty_Int) → new_lt6(vwx3411, vwx3611)
new_esEs23(vwx301, vwx401, app(app(app(ty_@3, ccc), ccd), cce)) → new_esEs6(vwx301, vwx401, ccc, ccd, cce)
new_lt5(vwx3411, vwx3611, app(app(ty_@2, baf), bag)) → new_lt19(vwx3411, vwx3611, baf, bag)
new_lt5(vwx3411, vwx3611, ty_Ordering) → new_lt7(vwx3411, vwx3611)
new_primCmpNat2(vwx34000, Zero) → GT
new_esEs5(Left(vwx300), Left(vwx400), app(app(app(ty_@3, dbh), dca), dcb), dbb) → new_esEs6(vwx300, vwx400, dbh, dca, dcb)
new_esEs25(vwx300, vwx400, ty_Ordering) → new_esEs10(vwx300, vwx400)
new_esEs10(GT, GT) → True
new_esEs23(vwx301, vwx401, ty_Int) → new_esEs9(vwx301, vwx401)
new_esEs23(vwx301, vwx401, app(app(ty_@2, cbh), cca)) → new_esEs7(vwx301, vwx401, cbh, cca)
new_lt5(vwx3411, vwx3611, ty_Float) → new_lt13(vwx3411, vwx3611)
new_compare110(vwx340, vwx360, True, bcc, bcd, bce) → LT
new_esEs20(vwx3410, vwx3610, app(ty_[], bda)) → new_esEs15(vwx3410, vwx3610, bda)
new_esEs25(vwx300, vwx400, app(app(app(ty_@3, cfa), cfb), cfc)) → new_esEs6(vwx300, vwx400, cfa, cfb, cfc)
new_lt20(vwx3410, vwx3610, ty_Float) → new_lt13(vwx3410, vwx3610)
new_ltEs6(vwx3412, vwx3612, app(ty_[], bah)) → new_ltEs10(vwx3412, vwx3612, bah)
new_compare27(vwx340, vwx360, True) → EQ
new_esEs29(vwx340, vwx360, ty_Ordering) → new_esEs10(vwx340, vwx360)
new_esEs20(vwx3410, vwx3610, ty_Integer) → new_esEs14(vwx3410, vwx3610)
new_ltEs8(LT, GT) → True
new_esEs16(False, False) → True
new_esEs26(vwx301, vwx401, app(ty_[], cgb)) → new_esEs15(vwx301, vwx401, cgb)
new_esEs24(vwx302, vwx402, ty_Integer) → new_esEs14(vwx302, vwx402)
new_esEs12(vwx3410, vwx3610, app(app(app(ty_@3, ha), hb), hc)) → new_esEs6(vwx3410, vwx3610, ha, hb, hc)
new_ltEs19(vwx3411, vwx3611, app(app(app(ty_@3, beh), bfa), bfb)) → new_ltEs5(vwx3411, vwx3611, beh, bfa, bfb)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_Double) → new_ltEs17(vwx3410, vwx3610)
new_ltEs6(vwx3412, vwx3612, ty_Char) → new_ltEs15(vwx3412, vwx3612)
new_compare29(vwx340, vwx360, bcf, bcg) → new_compare210(vwx340, vwx360, new_esEs7(vwx340, vwx360, bcf, bcg), bcf, bcg)
new_esEs24(vwx302, vwx402, ty_Double) → new_esEs8(vwx302, vwx402)
new_esEs20(vwx3410, vwx3610, ty_Float) → new_esEs17(vwx3410, vwx3610)
new_lt21(vwx340, vwx360, app(app(ty_@2, bcf), bcg)) → new_lt19(vwx340, vwx360, bcf, bcg)
new_esEs4(Just(vwx300), Just(vwx400), ty_Char) → new_esEs19(vwx300, vwx400)
new_esEs5(Right(vwx300), Right(vwx400), dcd, app(ty_Maybe, ddf)) → new_esEs4(vwx300, vwx400, ddf)
new_compare11(vwx340, vwx360, False) → GT
new_ltEs6(vwx3412, vwx3612, app(app(ty_@2, bbg), bbh)) → new_ltEs18(vwx3412, vwx3612, bbg, bbh)
new_esEs8(Double(vwx300, vwx301), Double(vwx400, vwx401)) → new_esEs9(new_sr(vwx300, vwx400), new_sr(vwx301, vwx401))
new_compare11(vwx340, vwx360, True) → LT
new_esEs23(vwx301, vwx401, ty_Char) → new_esEs19(vwx301, vwx401)
new_esEs5(Left(vwx300), Left(vwx400), app(app(ty_Either, dbc), dbd), dbb) → new_esEs5(vwx300, vwx400, dbc, dbd)
new_lt5(vwx3411, vwx3611, app(app(ty_Either, baa), bab)) → new_lt12(vwx3411, vwx3611, baa, bab)
new_primCmpInt(Neg(Succ(vwx34000)), Neg(vwx3600)) → new_primCmpNat0(vwx3600, vwx34000)
new_esEs23(vwx301, vwx401, ty_Bool) → new_esEs16(vwx301, vwx401)
new_lt10(vwx340, vwx360, cc) → new_esEs10(new_compare14(vwx340, vwx360, cc), LT)
new_esEs29(vwx340, vwx360, ty_@0) → new_esEs11(vwx340, vwx360)
new_esEs29(vwx340, vwx360, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs6(vwx340, vwx360, bcc, bcd, bce)
new_lt7(vwx340, vwx360) → new_esEs10(new_compare9(vwx340, vwx360), LT)
new_compare32(vwx3400, vwx3600, ty_Ordering) → new_compare9(vwx3400, vwx3600)
new_esEs28(vwx301, vwx401, ty_Int) → new_esEs9(vwx301, vwx401)
new_esEs4(Just(vwx300), Just(vwx400), app(app(ty_@2, che), chf)) → new_esEs7(vwx300, vwx400, che, chf)
new_esEs10(LT, GT) → False
new_esEs10(GT, LT) → False
new_esEs13(vwx3411, vwx3611, ty_Ordering) → new_esEs10(vwx3411, vwx3611)
new_lt21(vwx340, vwx360, app(app(app(ty_@3, bcc), bcd), bce)) → new_lt15(vwx340, vwx360, bcc, bcd, bce)
new_esEs4(Just(vwx300), Just(vwx400), ty_Float) → new_esEs17(vwx300, vwx400)
new_esEs10(LT, EQ) → False
new_esEs10(EQ, LT) → False
new_esEs20(vwx3410, vwx3610, app(app(ty_@2, bea), beb)) → new_esEs7(vwx3410, vwx3610, bea, beb)
new_esEs5(Right(vwx300), Right(vwx400), dcd, app(app(ty_@2, dch), dda)) → new_esEs7(vwx300, vwx400, dch, dda)
new_ltEs8(LT, LT) → True
new_esEs21(vwx300, vwx400, ty_@0) → new_esEs11(vwx300, vwx400)
new_compare15(Integer(vwx3400), Integer(vwx3600)) → new_primCmpInt(vwx3400, vwx3600)
new_compare0([], :(vwx3600, vwx3601), ba) → LT
new_lt5(vwx3411, vwx3611, app(ty_Maybe, hh)) → new_lt10(vwx3411, vwx3611, hh)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(vwx300, vwx400, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs6(vwx300, vwx400, bhd, bhe, bhf)
new_esEs27(vwx300, vwx400, ty_Integer) → new_esEs14(vwx300, vwx400)
new_asAs(True, vwx51) → vwx51
new_ltEs4(Just(vwx3410), Nothing, dae) → False
new_primMulNat0(Succ(vwx30100), Succ(vwx40100)) → new_primPlusNat0(new_primMulNat0(vwx30100, Succ(vwx40100)), vwx40100)
new_lt5(vwx3411, vwx3611, app(ty_Ratio, bfg)) → new_lt14(vwx3411, vwx3611, bfg)
new_ltEs12(Left(vwx3410), Left(vwx3610), app(app(ty_@2, ef), eg), dg) → new_ltEs18(vwx3410, vwx3610, ef, eg)
new_compare30(Char(vwx3400), Char(vwx3600)) → new_primCmpInt(vwx3400, vwx3600)
new_lt4(vwx3410, vwx3610, app(app(ty_@2, hd), he)) → new_lt19(vwx3410, vwx3610, hd, he)
new_ltEs20(vwx341, vwx361, app(ty_Maybe, dae)) → new_ltEs4(vwx341, vwx361, dae)
new_compare24(vwx340, vwx360, False, cc) → new_compare10(vwx340, vwx360, new_ltEs4(vwx340, vwx360, cc), cc)
new_esEs22(vwx300, vwx400, ty_Ordering) → new_esEs10(vwx300, vwx400)
new_lt5(vwx3411, vwx3611, ty_Bool) → new_lt11(vwx3411, vwx3611)
new_ltEs12(Right(vwx3410), Right(vwx3610), eh, ty_Integer) → new_ltEs9(vwx3410, vwx3610)
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_Int, dg) → new_ltEs7(vwx3410, vwx3610)
new_esEs29(vwx340, vwx360, app(ty_[], ba)) → new_esEs15(vwx340, vwx360, ba)
new_compare32(vwx3400, vwx3600, ty_Integer) → new_compare15(vwx3400, vwx3600)
new_lt4(vwx3410, vwx3610, app(ty_Maybe, gf)) → new_lt10(vwx3410, vwx3610, gf)
new_esEs29(vwx340, vwx360, ty_Float) → new_esEs17(vwx340, vwx360)
new_lt4(vwx3410, vwx3610, app(app(ty_Either, gg), gh)) → new_lt12(vwx3410, vwx3610, gg, gh)
new_esEs9(vwx30, vwx40) → new_primEqInt(vwx30, vwx40)
new_esEs29(vwx340, vwx360, app(ty_Maybe, cc)) → new_esEs4(vwx340, vwx360, cc)
new_compare32(vwx3400, vwx3600, app(ty_Ratio, ddg)) → new_compare18(vwx3400, vwx3600, ddg)
new_compare13(vwx83, vwx84, vwx85, vwx86, True, bga, bgb) → LT
new_compare110(vwx340, vwx360, False, bcc, bcd, bce) → GT
new_compare9(vwx340, vwx360) → new_compare26(vwx340, vwx360, new_esEs10(vwx340, vwx360))
new_esEs22(vwx300, vwx400, app(app(ty_Either, cad), cae)) → new_esEs5(vwx300, vwx400, cad, cae)
new_esEs28(vwx301, vwx401, ty_Integer) → new_esEs14(vwx301, vwx401)
new_ltEs20(vwx341, vwx361, ty_Integer) → new_ltEs9(vwx341, vwx361)
new_compare32(vwx3400, vwx3600, app(ty_Maybe, bc)) → new_compare14(vwx3400, vwx3600, bc)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_esEs5(Right(vwx300), Right(vwx400), dcd, ty_@0) → new_esEs11(vwx300, vwx400)
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_Char) → new_ltEs15(vwx3410, vwx3610)
new_primCompAux0(vwx106, EQ) → vwx106
new_ltEs12(Left(vwx3410), Left(vwx3610), ty_Float, dg) → new_ltEs13(vwx3410, vwx3610)
new_lt4(vwx3410, vwx3610, ty_@0) → new_lt17(vwx3410, vwx3610)
new_esEs24(vwx302, vwx402, app(ty_[], cdd)) → new_esEs15(vwx302, vwx402, cdd)
new_ltEs19(vwx3411, vwx3611, ty_@0) → new_ltEs16(vwx3411, vwx3611)
new_esEs21(vwx300, vwx400, ty_Char) → new_esEs19(vwx300, vwx400)
new_lt4(vwx3410, vwx3610, app(ty_Ratio, bff)) → new_lt14(vwx3410, vwx3610, bff)
new_compare32(vwx3400, vwx3600, ty_Float) → new_compare31(vwx3400, vwx3600)
new_primCmpInt(Pos(Succ(vwx34000)), Pos(vwx3600)) → new_primCmpNat2(vwx34000, vwx3600)
new_ltEs4(Just(vwx3410), Just(vwx3610), ty_Integer) → new_ltEs9(vwx3410, vwx3610)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(vwx300, vwx400, app(ty_Ratio, bgf)) → new_esEs18(vwx300, vwx400, bgf)
new_ltEs19(vwx3411, vwx3611, ty_Bool) → new_ltEs11(vwx3411, vwx3611)
new_primCmpInt(Neg(Succ(vwx34000)), Pos(vwx3600)) → LT
new_not(True) → False
The set Q consists of the following terms:
new_ltEs19(x0, x1, ty_Bool)
new_primMulInt(Neg(x0), Pos(x1))
new_primMulInt(Pos(x0), Neg(x1))
new_ltEs12(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_ltEs12(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs29(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_@0)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs15([], [], x0)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_compare32(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Char(x0), Char(x1))
new_ltEs4(Just(x0), Just(x1), ty_Float)
new_lt17(x0, x1)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs6(x0, x1, app(ty_Maybe, x2))
new_lt18(x0, x1)
new_ltEs8(EQ, EQ)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_lt5(x0, x1, ty_Float)
new_ltEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_ltEs4(Just(x0), Just(x1), ty_Int)
new_esEs26(x0, x1, ty_Int)
new_ltEs12(Right(x0), Right(x1), x2, ty_@0)
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_ltEs4(Just(x0), Just(x1), ty_Double)
new_esEs5(Left(x0), Left(x1), app(ty_[], x2), x3)
new_compare13(x0, x1, x2, x3, False, x4, x5)
new_ltEs12(Left(x0), Left(x1), app(ty_[], x2), x3)
new_lt21(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Bool)
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_ltEs5(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs29(x0, x1, ty_Integer)
new_esEs5(Right(x0), Right(x1), x2, ty_Ordering)
new_compare11(x0, x1, True)
new_compare27(x0, x1, False)
new_lt15(x0, x1, x2, x3, x4)
new_esEs5(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs10(EQ, GT)
new_esEs10(GT, EQ)
new_lt4(x0, x1, ty_Char)
new_ltEs19(x0, x1, ty_Integer)
new_ltEs4(Just(x0), Just(x1), ty_Bool)
new_esEs5(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(@0, @0)
new_compare32(x0, x1, ty_Int)
new_esEs10(LT, EQ)
new_esEs10(EQ, LT)
new_esEs24(x0, x1, ty_@0)
new_ltEs20(x0, x1, app(ty_[], x2))
new_ltEs12(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_compare26(x0, x1, True)
new_ltEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs12(Right(x0), Right(x1), x2, ty_Char)
new_compare5(Double(x0, x1), Double(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Char)
new_compare32(x0, x1, ty_Double)
new_lt4(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Bool)
new_compare18(:%(x0, x1), :%(x2, x3), ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_compare110(x0, x1, False, x2, x3, x4)
new_ltEs6(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs29(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_lt5(x0, x1, ty_Double)
new_ltEs17(x0, x1)
new_ltEs20(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(x0, x1, app(app(ty_@2, x2), x3))
new_lt21(x0, x1, ty_Ordering)
new_ltEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primMulInt(Pos(x0), Pos(x1))
new_esEs16(True, False)
new_esEs16(False, True)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_lt4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Left(x0), Left(x1), ty_Double, x2)
new_compare17(x0, x1, True, x2, x3)
new_ltEs12(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_primCmpNat1(Zero, Zero)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_lt12(x0, x1, x2, x3)
new_esEs13(x0, x1, app(ty_Maybe, x2))
new_esEs16(True, True)
new_esEs5(Right(x0), Left(x1), x2, x3)
new_esEs5(Left(x0), Right(x1), x2, x3)
new_lt4(x0, x1, ty_Ordering)
new_compare32(x0, x1, app(ty_[], x2))
new_lt13(x0, x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15([], :(x0, x1), x2)
new_esEs24(x0, x1, ty_Char)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_esEs21(x0, x1, ty_Char)
new_compare8(x0, x1)
new_pePe(True, x0)
new_ltEs12(Left(x0), Left(x1), ty_Float, x2)
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_lt20(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Zero)
new_esEs20(x0, x1, ty_Double)
new_primCmpNat1(Succ(x0), Succ(x1))
new_compare32(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs20(x0, x1, ty_Ordering)
new_esEs5(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_compare30(Char(x0), Char(x1))
new_esEs23(x0, x1, ty_Char)
new_compare29(x0, x1, x2, x3)
new_lt4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(x0, x1, ty_Ordering)
new_ltEs20(x0, x1, ty_Bool)
new_esEs13(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs12(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs12(x0, x1, app(ty_Maybe, x2))
new_lt16(x0, x1)
new_esEs25(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs5(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_lt5(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Int)
new_ltEs6(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Succ(x0), Succ(x1))
new_ltEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt5(x0, x1, ty_Ordering)
new_lt11(x0, x1)
new_esEs5(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs13(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs14(Integer(x0), Integer(x1))
new_esEs22(x0, x1, ty_@0)
new_ltEs20(x0, x1, ty_Double)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primCmpNat0(Succ(x0), x1)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt5(x0, x1, ty_Char)
new_ltEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_ltEs4(Nothing, Just(x0), x1)
new_ltEs9(x0, x1)
new_ltEs6(x0, x1, ty_Ordering)
new_esEs10(LT, GT)
new_esEs10(GT, LT)
new_primCmpNat1(Succ(x0), Zero)
new_compare32(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_Integer)
new_ltEs20(x0, x1, ty_@0)
new_esEs29(x0, x1, ty_Double)
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_esEs25(x0, x1, ty_Float)
new_lt20(x0, x1, ty_Bool)
new_esEs20(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Int)
new_ltEs15(x0, x1)
new_lt21(x0, x1, ty_Char)
new_ltEs4(Just(x0), Just(x1), ty_Char)
new_esEs13(x0, x1, ty_Char)
new_lt8(x0, x1)
new_lt9(x0, x1, x2)
new_primMulInt(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs21(x0, x1, ty_Float)
new_compare32(x0, x1, app(ty_Ratio, x2))
new_compare110(x0, x1, True, x2, x3, x4)
new_esEs29(x0, x1, ty_Bool)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primCompAux0(x0, EQ)
new_esEs22(x0, x1, ty_Integer)
new_compare0([], [], x0)
new_lt20(x0, x1, ty_@0)
new_ltEs20(x0, x1, ty_Integer)
new_ltEs12(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_lt21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs6(x0, x1, ty_Bool)
new_esEs21(x0, x1, ty_@0)
new_lt21(x0, x1, ty_Double)
new_lt4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs12(Right(x0), Right(x1), x2, ty_Integer)
new_compare31(Float(x0, x1), Float(x2, x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_lt5(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Zero)
new_esEs12(x0, x1, ty_Char)
new_esEs25(x0, x1, app(ty_[], x2))
new_compare0(:(x0, x1), :(x2, x3), x4)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(Right(x0), Right(x1), x2, app(ty_[], x3))
new_lt6(x0, x1)
new_esEs28(x0, x1, ty_Integer)
new_compare32(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_[], x2))
new_ltEs12(Right(x0), Right(x1), x2, ty_Bool)
new_esEs21(x0, x1, ty_Integer)
new_lt5(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs12(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs10(EQ, EQ)
new_ltEs6(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Bool)
new_esEs29(x0, x1, app(ty_Maybe, x2))
new_compare210(x0, x1, True, x2, x3)
new_ltEs20(x0, x1, app(ty_Ratio, x2))
new_compare13(x0, x1, x2, x3, True, x4, x5)
new_esEs23(x0, x1, ty_Double)
new_primCmpInt(Neg(Zero), Neg(Zero))
new_esEs13(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Int)
new_compare0([], :(x0, x1), x2)
new_compare18(:%(x0, x1), :%(x2, x3), ty_Int)
new_lt21(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs25(x0, x1, ty_Double)
new_esEs6(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_compare32(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs29(x0, x1, app(ty_Ratio, x2))
new_compare28(x0, x1, True, x2, x3, x4)
new_primMulNat0(Zero, Succ(x0))
new_ltEs12(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_@0)
new_esEs15(:(x0, x1), :(x2, x3), x4)
new_esEs29(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs13(x0, x1, ty_@0)
new_esEs26(x0, x1, ty_Bool)
new_asAs(False, x0)
new_esEs23(x0, x1, ty_Ordering)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(x0, x1, ty_Ordering)
new_esEs4(Just(x0), Nothing, x1)
new_ltEs19(x0, x1, ty_Ordering)
new_compare32(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_ltEs12(Left(x0), Left(x1), ty_@0, x2)
new_esEs21(x0, x1, ty_Bool)
new_ltEs4(Just(x0), Just(x1), ty_Integer)
new_ltEs4(Just(x0), Just(x1), ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs5(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primPlusNat0(Succ(x0), x1)
new_lt5(x0, x1, ty_Int)
new_lt21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs29(x0, x1, ty_Ordering)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Float)
new_esEs5(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs24(x0, x1, ty_Float)
new_ltEs19(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Int)
new_lt20(x0, x1, ty_Int)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_lt4(x0, x1, ty_Float)
new_esEs5(Right(x0), Right(x1), x2, ty_Bool)
new_primPlusNat0(Zero, x0)
new_ltEs19(x0, x1, ty_Int)
new_compare25(x0, x1, True, x2, x3)
new_esEs29(x0, x1, ty_Float)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Ordering)
new_ltEs11(False, False)
new_ltEs19(x0, x1, ty_Char)
new_lt4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt5(x0, x1, app(ty_[], x2))
new_compare0(:(x0, x1), [], x2)
new_esEs28(x0, x1, ty_Int)
new_ltEs12(Right(x0), Right(x1), x2, ty_Float)
new_ltEs8(EQ, LT)
new_lt20(x0, x1, app(ty_[], x2))
new_ltEs8(LT, EQ)
new_esEs25(x0, x1, ty_@0)
new_primMulNat0(Succ(x0), Zero)
new_esEs12(x0, x1, ty_Bool)
new_esEs12(x0, x1, app(ty_[], x2))
new_esEs12(x0, x1, app(ty_Ratio, x2))
new_lt7(x0, x1)
new_lt10(x0, x1, x2)
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs13(x0, x1, ty_Bool)
new_ltEs19(x0, x1, ty_Float)
new_ltEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Float)
new_ltEs12(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_lt14(x0, x1, x2)
new_lt20(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs22(x0, x1, ty_Double)
new_compare111(x0, x1, False)
new_primCmpNat0(Zero, x0)
new_compare32(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare7(x0, x1, x2, x3)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(x0, x1, ty_Integer)
new_esEs13(x0, x1, ty_Integer)
new_ltEs11(False, True)
new_ltEs11(True, False)
new_ltEs12(Left(x0), Left(x1), ty_Char, x2)
new_compare9(x0, x1)
new_esEs5(Right(x0), Right(x1), x2, ty_Char)
new_esEs12(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Integer)
new_lt21(x0, x1, ty_@0)
new_esEs4(Nothing, Just(x0), x1)
new_ltEs10(x0, x1, x2)
new_ltEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs4(Nothing, Nothing, x0)
new_esEs23(x0, x1, ty_Float)
new_ltEs14(x0, x1, x2)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs12(x0, x1, ty_Float)
new_lt5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs6(x0, x1, app(ty_Ratio, x2))
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_lt5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(LT, LT)
new_esEs12(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs6(x0, x1, ty_Int)
new_lt5(x0, x1, app(ty_Maybe, x2))
new_compare25(x0, x1, False, x2, x3)
new_ltEs12(Left(x0), Left(x1), ty_Bool, x2)
new_lt20(x0, x1, ty_Float)
new_compare6(@0, @0)
new_primEqNat0(Succ(x0), Zero)
new_lt5(x0, x1, ty_Integer)
new_compare111(x0, x1, True)
new_ltEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs9(x0, x1)
new_ltEs12(Left(x0), Left(x1), ty_Integer, x2)
new_lt21(x0, x1, ty_Float)
new_esEs5(Left(x0), Left(x1), ty_Ordering, x2)
new_ltEs13(x0, x1)
new_esEs12(x0, x1, ty_@0)
new_lt4(x0, x1, ty_Double)
new_ltEs8(LT, LT)
new_compare14(x0, x1, x2)
new_ltEs19(x0, x1, ty_Double)
new_lt4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs25(x0, x1, ty_Bool)
new_ltEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_ltEs8(GT, GT)
new_compare17(x0, x1, False, x2, x3)
new_ltEs12(Left(x0), Right(x1), x2, x3)
new_ltEs12(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_Ordering)
new_ltEs4(Just(x0), Nothing, x1)
new_compare32(x0, x1, ty_@0)
new_lt21(x0, x1, ty_Integer)
new_compare15(Integer(x0), Integer(x1))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs12(Right(x0), Right(x1), x2, app(ty_[], x3))
new_pePe(False, x0)
new_esEs5(Left(x0), Left(x1), ty_Bool, x2)
new_compare28(x0, x1, False, x2, x3, x4)
new_esEs15(:(x0, x1), [], x2)
new_esEs21(x0, x1, app(ty_[], x2))
new_lt4(x0, x1, app(ty_[], x2))
new_ltEs20(x0, x1, app(app(ty_Either, x2), x3))
new_lt4(x0, x1, ty_@0)
new_esEs10(GT, GT)
new_esEs26(x0, x1, ty_Char)
new_esEs5(Right(x0), Right(x1), x2, ty_Float)
new_esEs16(False, False)
new_ltEs12(Left(x0), Left(x1), ty_Double, x2)
new_sr0(Integer(x0), Integer(x1))
new_ltEs12(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_lt21(x0, x1, ty_Bool)
new_lt4(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Double)
new_ltEs12(Right(x0), Right(x1), x2, ty_Double)
new_ltEs8(LT, GT)
new_ltEs8(GT, LT)
new_esEs5(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primCmpNat2(x0, Zero)
new_ltEs19(x0, x1, app(ty_[], x2))
new_ltEs4(Nothing, Nothing, x0)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs5(Right(x0), Right(x1), x2, ty_@0)
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_lt5(x0, x1, ty_@0)
new_esEs5(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_compare26(x0, x1, False)
new_esEs27(x0, x1, ty_Integer)
new_compare32(x0, x1, ty_Bool)
new_primCompAux0(x0, LT)
new_not(True)
new_esEs5(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_ltEs6(x0, x1, ty_Float)
new_lt21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_ltEs16(x0, x1)
new_esEs20(x0, x1, ty_Ordering)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_compare10(x0, x1, False, x2)
new_not(False)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_compare12(x0, x1, x2, x3, True, x4, x5, x6)
new_esEs24(x0, x1, ty_Ordering)
new_compare10(x0, x1, True, x2)
new_ltEs6(x0, x1, ty_Char)
new_primCmpNat2(x0, Succ(x1))
new_esEs5(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs29(x0, x1, app(app(ty_Either, x2), x3))
new_esEs12(x0, x1, ty_Double)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_compare210(@2(x0, x1), @2(x2, x3), False, x4, x5)
new_ltEs7(x0, x1)
new_esEs13(x0, x1, ty_Double)
new_lt21(x0, x1, app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs5(Right(x0), Right(x1), x2, ty_Int)
new_sr(x0, x1)
new_esEs25(x0, x1, ty_Integer)
new_ltEs20(x0, x1, ty_Char)
new_ltEs20(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Succ(x0))
new_ltEs20(x0, x1, ty_Float)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs6(x0, x1, app(ty_[], x2))
new_lt21(x0, x1, app(ty_[], x2))
new_esEs13(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs4(Just(x0), Just(x1), ty_@0)
new_ltEs8(GT, EQ)
new_ltEs8(EQ, GT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_lt19(x0, x1, x2, x3)
new_esEs29(x0, x1, ty_Char)
new_ltEs12(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare27(x0, x1, True)
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs5(Left(x0), Left(x1), ty_Char, x2)
new_compare11(x0, x1, False)
new_esEs13(x0, x1, ty_Int)
new_esEs5(Left(x0), Left(x1), ty_Integer, x2)
new_compare16(x0, x1, x2, x3, x4)
new_esEs5(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(x0, x1, ty_Float)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_compare24(x0, x1, False, x2)
new_ltEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs22(x0, x1, app(ty_[], x2))
new_primCompAux1(x0, x1, x2, x3)
new_esEs20(x0, x1, ty_Float)
new_ltEs12(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs5(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(Just(x0), Just(x1), ty_Double)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_ltEs12(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs20(x0, x1, ty_Bool)
new_compare19(x0, x1)
new_lt4(x0, x1, ty_Bool)
new_lt20(x0, x1, ty_Ordering)
new_primCompAux0(x0, GT)
new_esEs5(Left(x0), Left(x1), ty_Int, x2)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_compare32(x0, x1, ty_Integer)
new_esEs29(x0, x1, ty_@0)
new_ltEs6(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Zero, Succ(x0))
new_ltEs11(True, True)
new_esEs20(x0, x1, ty_@0)
new_primCmpNat1(Zero, Succ(x0))
new_compare24(x0, x1, True, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs29(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, ty_Double)
new_asAs(True, x0)
new_ltEs6(x0, x1, ty_@0)
new_compare12(x0, x1, x2, x3, False, x4, x5, x6)
new_ltEs12(Left(x0), Left(x1), ty_Int, x2)
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_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(app(ty_Either, bef), beg)) → new_ltEs1(vwx3411, vwx3611, bef, beg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs0(Just(vwx3410), Just(vwx3610), app(app(ty_Either, cf), cg)) → new_ltEs1(vwx3410, vwx3610, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(app(ty_@2, bfc), bfd)) → new_ltEs3(vwx3411, vwx3611, bfc, bfd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs0(Just(vwx3410), Just(vwx3610), app(app(ty_@2, dd), de)) → new_ltEs3(vwx3410, vwx3610, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs(vwx341, vwx361, h) → new_compare(vwx341, vwx361, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(app(app(ty_@3, beh), bfa), bfb)) → new_ltEs2(vwx3411, vwx3611, beh, bfa, bfb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs0(Just(vwx3410), Just(vwx3610), app(app(app(ty_@3, da), db), dc)) → new_ltEs2(vwx3410, vwx3610, da, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_lt1(vwx340, vwx360, bca, bcb) → new_compare21(vwx340, vwx360, new_esEs5(vwx340, vwx360, bca, bcb), bca, bcb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_lt2(vwx340, vwx360, bcc, bcd, bce) → new_compare22(vwx340, vwx360, new_esEs6(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5, 5 >= 6
- new_compare21(vwx340, vwx360, False, bca, bcb) → new_ltEs1(vwx340, vwx360, bca, bcb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(ty_Maybe, bee)) → new_ltEs0(vwx3411, vwx3611, bee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs0(Just(vwx3410), Just(vwx3610), app(ty_Maybe, ce)) → new_ltEs0(vwx3410, vwx3610, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs0(Just(vwx3410), Just(vwx3610), app(ty_[], cd)) → new_ltEs(vwx3410, vwx3610, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_lt(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_primCompAux(vwx3400, vwx3600, new_compare0(vwx3401, vwx3601, ba), ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4
- new_lt(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_compare(vwx3401, vwx3601, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_compare(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_primCompAux(vwx3400, vwx3600, new_compare0(vwx3401, vwx3601, ba), ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4
- new_compare(:(vwx3400, vwx3401), :(vwx3600, vwx3601), ba) → new_compare(vwx3401, vwx3601, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_compare23(@2(:(vwx3400, vwx3401), vwx341), @2(:(vwx3600, vwx3601), vwx361), False, app(ty_[], ba), bfe) → new_primCompAux(vwx3400, vwx3600, new_compare0(vwx3401, vwx3601, ba), ba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4
- new_lt3(vwx340, vwx360, bcf, bcg) → new_compare23(vwx340, vwx360, new_esEs7(vwx340, vwx360, bcf, bcg), bcf, bcg)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(app(ty_Either, bbb), bbc)) → new_ltEs1(vwx3412, vwx3612, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(app(ty_@2, bbg), bbh)) → new_ltEs3(vwx3412, vwx3612, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(app(app(ty_@3, bbd), bbe), bbf)) → new_ltEs2(vwx3412, vwx3612, bbd, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(ty_Maybe, bba)) → new_ltEs0(vwx3412, vwx3612, bba)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare20(vwx340, vwx360, False, cc) → new_ltEs0(vwx340, vwx360, cc)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3
- new_lt0(vwx340, vwx360, cc) → new_compare20(vwx340, vwx360, new_esEs4(vwx340, vwx360, cc), cc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4
- new_compare1(vwx340, vwx360, cc) → new_compare20(vwx340, vwx360, new_esEs4(vwx340, vwx360, cc), cc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4
- new_compare3(vwx340, vwx360, bcc, bcd, bce) → new_compare22(vwx340, vwx360, new_esEs6(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5, 5 >= 6
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), bec, app(ty_[], bed)) → new_ltEs(vwx3411, vwx3611, bed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, gd, app(ty_[], bah)) → new_ltEs(vwx3412, vwx3612, bah)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(ty_Maybe, bdc), bdb) → new_lt0(vwx3410, vwx3610, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(app(app(ty_@3, bcc), bcd), bce), bfe) → new_compare22(vwx340, vwx360, new_esEs6(vwx340, vwx360, bcc, bcd, bce), bcc, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4, 4 > 5, 4 > 6
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(ty_[], bda), bdb) → new_lt(vwx3410, vwx3610, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_compare22(vwx340, vwx360, False, bcc, bcd, bce) → new_ltEs2(vwx340, vwx360, bcc, bcd, bce)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4, 6 >= 5
- new_primCompAux(vwx3400, vwx3600, vwx101, app(app(ty_Either, bd), be)) → new_compare2(vwx3400, vwx3600, bd, be)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_primCompAux(vwx3400, vwx3600, vwx101, app(app(app(ty_@3, bf), bg), bh)) → new_compare3(vwx3400, vwx3600, bf, bg, bh)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(app(ty_@2, bea), beb), bdb) → new_lt3(vwx3410, vwx3610, bea, beb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(app(ty_@2, bcf), bcg), bfe) → new_compare23(vwx340, vwx360, new_esEs7(vwx340, vwx360, bcf, bcg), bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4, 4 > 5
- new_compare4(vwx340, vwx360, bcf, bcg) → new_compare23(vwx340, vwx360, new_esEs7(vwx340, vwx360, bcf, bcg), bcf, bcg)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_compare2(vwx340, vwx360, bca, bcb) → new_compare21(vwx340, vwx360, new_esEs5(vwx340, vwx360, bca, bcb), bca, bcb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(app(ty_Either, bca), bcb), bfe) → new_compare21(vwx340, vwx360, new_esEs5(vwx340, vwx360, bca, bcb), bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4, 4 > 5
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(app(app(ty_@3, bdf), bdg), bdh), bdb) → new_lt2(vwx3410, vwx3610, bdf, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs3(@2(vwx3410, vwx3411), @2(vwx3610, vwx3611), app(app(ty_Either, bdd), bde), bdb) → new_lt1(vwx3410, vwx3610, bdd, bde)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_primCompAux(vwx3400, vwx3600, vwx101, app(ty_[], bb)) → new_compare(vwx3400, vwx3600, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3
- new_primCompAux(vwx3400, vwx3600, vwx101, app(ty_Maybe, bc)) → new_compare1(vwx3400, vwx3600, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3
- new_primCompAux(vwx3400, vwx3600, vwx101, app(app(ty_@2, ca), cb)) → new_compare4(vwx3400, vwx3600, ca, cb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, app(ty_Maybe, cc), bfe) → new_compare20(vwx340, vwx360, new_esEs4(vwx340, vwx360, cc), cc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 4
- new_ltEs1(Left(vwx3410), Left(vwx3610), app(app(ty_Either, ea), eb), dg) → new_ltEs1(vwx3410, vwx3610, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(app(ty_Either, fc), fd)) → new_ltEs1(vwx3410, vwx3610, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(app(ty_@2, ga), gb)) → new_ltEs3(vwx3410, vwx3610, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs1(Left(vwx3410), Left(vwx3610), app(app(ty_@2, ef), eg), dg) → new_ltEs3(vwx3410, vwx3610, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(app(app(ty_@3, ff), fg), fh)) → new_ltEs2(vwx3410, vwx3610, ff, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs1(Left(vwx3410), Left(vwx3610), app(app(app(ty_@3, ec), ed), ee), dg) → new_ltEs2(vwx3410, vwx3610, ec, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs1(Left(vwx3410), Left(vwx3610), app(ty_Maybe, dh), dg) → new_ltEs0(vwx3410, vwx3610, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(ty_Maybe, fb)) → new_ltEs0(vwx3410, vwx3610, fb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs1(Right(vwx3410), Right(vwx3610), eh, app(ty_[], fa)) → new_ltEs(vwx3410, vwx3610, fa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs1(Left(vwx3410), Left(vwx3610), app(ty_[], df), dg) → new_ltEs(vwx3410, vwx3610, df)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(app(ty_Either, cf), cg))) → new_ltEs1(vwx3410, vwx3610, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(app(ty_Either, ea), eb)), dg)) → new_ltEs1(vwx3410, vwx3610, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(app(ty_Either, fc), fd))) → new_ltEs1(vwx3410, vwx3610, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(app(ty_Either, bef), beg))) → new_ltEs1(vwx3411, vwx3611, bef, beg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(app(ty_Either, bbb), bbc))) → new_ltEs1(vwx3412, vwx3612, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(app(ty_@2, ef), eg)), dg)) → new_ltEs3(vwx3410, vwx3610, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(app(ty_@2, bfc), bfd))) → new_ltEs3(vwx3411, vwx3611, bfc, bfd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(app(ty_@2, dd), de))) → new_ltEs3(vwx3410, vwx3610, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(app(ty_@2, bbg), bbh))) → new_ltEs3(vwx3412, vwx3612, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(app(ty_@2, ga), gb))) → new_ltEs3(vwx3410, vwx3610, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(app(app(ty_@3, da), db), dc))) → new_ltEs2(vwx3410, vwx3610, da, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(app(app(ty_@3, bbd), bbe), bbf))) → new_ltEs2(vwx3412, vwx3612, bbd, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(app(app(ty_@3, beh), bfa), bfb))) → new_ltEs2(vwx3411, vwx3611, beh, bfa, bfb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(app(app(ty_@3, ff), fg), fh))) → new_ltEs2(vwx3410, vwx3610, ff, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(app(app(ty_@3, ec), ed), ee)), dg)) → new_ltEs2(vwx3410, vwx3610, ec, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(ty_Maybe, fb))) → new_ltEs0(vwx3410, vwx3610, fb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(ty_Maybe, dh)), dg)) → new_ltEs0(vwx3410, vwx3610, dh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(ty_Maybe, bba))) → new_ltEs0(vwx3412, vwx3612, bba)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(ty_Maybe, ce))) → new_ltEs0(vwx3410, vwx3610, ce)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(ty_Maybe, bee))) → new_ltEs0(vwx3411, vwx3611, bee)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(ty_Maybe, gf), gd, ge) → new_lt0(vwx3410, vwx3610, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(ty_Maybe, hh), ge) → new_lt0(vwx3411, vwx3611, hh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(ty_[], gc), gd, ge) → new_lt(vwx3410, vwx3610, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(ty_[], hg), ge) → new_lt(vwx3411, vwx3611, hg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(app(ty_@2, baf), bag), ge) → new_lt3(vwx3411, vwx3611, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(app(ty_@2, hd), he), gd, ge) → new_lt3(vwx3410, vwx3610, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(app(app(ty_@3, bac), bad), bae), ge) → new_lt2(vwx3411, vwx3611, bac, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(app(app(ty_@3, ha), hb), hc), gd, ge) → new_lt2(vwx3410, vwx3610, ha, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), app(app(ty_Either, gg), gh), gd, ge) → new_lt1(vwx3410, vwx3610, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs2(@3(vwx3410, vwx3411, vwx3412), @3(vwx3610, vwx3611, vwx3612), hf, app(app(ty_Either, baa), bab), ge) → new_lt1(vwx3411, vwx3611, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_compare23(@2(vwx340, Left(vwx3410)), @2(vwx360, Left(vwx3610)), False, bch, app(app(ty_Either, app(ty_[], df)), dg)) → new_ltEs(vwx3410, vwx3610, df)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), gd), app(ty_[], bah))) → new_ltEs(vwx3412, vwx3612, bah)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, Just(vwx3410)), @2(vwx360, Just(vwx3610)), False, bch, app(ty_Maybe, app(ty_[], cd))) → new_ltEs(vwx3410, vwx3610, cd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, Right(vwx3410)), @2(vwx360, Right(vwx3610)), False, bch, app(app(ty_Either, eh), app(ty_[], fa))) → new_ltEs(vwx3410, vwx3610, fa)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, bec), app(ty_[], bed))) → new_ltEs(vwx3411, vwx3611, bed)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(ty_Maybe, hh)), ge)) → new_lt0(vwx3411, vwx3611, hh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(ty_Maybe, bdc)), bdb)) → new_lt0(vwx3410, vwx3610, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(ty_Maybe, gf)), gd), ge)) → new_lt0(vwx3410, vwx3610, gf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(ty_[], bda)), bdb)) → new_lt(vwx3410, vwx3610, bda)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(ty_[], gc)), gd), ge)) → new_lt(vwx3410, vwx3610, gc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(ty_[], hg)), ge)) → new_lt(vwx3411, vwx3611, hg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(app(ty_@2, hd), he)), gd), ge)) → new_lt3(vwx3410, vwx3610, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(app(ty_@2, bea), beb)), bdb)) → new_lt3(vwx3410, vwx3610, bea, beb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(app(ty_@2, baf), bag)), ge)) → new_lt3(vwx3411, vwx3611, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(app(app(ty_@3, bac), bad), bae)), ge)) → new_lt2(vwx3411, vwx3611, bac, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(app(app(ty_@3, ha), hb), hc)), gd), ge)) → new_lt2(vwx3410, vwx3610, ha, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(app(app(ty_@3, bdf), bdg), bdh)), bdb)) → new_lt2(vwx3410, vwx3610, bdf, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_compare23(@2(:(vwx3400, vwx3401), vwx341), @2(:(vwx3600, vwx3601), vwx361), False, app(ty_[], ba), bfe) → new_compare(vwx3401, vwx3601, ba)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare23(@2(vwx340, vwx341), @2(vwx360, vwx361), False, bch, app(ty_[], h)) → new_compare(vwx341, vwx361, h)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_compare23(@2(vwx340, @2(vwx3410, vwx3411)), @2(vwx360, @2(vwx3610, vwx3611)), False, bch, app(app(ty_@2, app(app(ty_Either, bdd), bde)), bdb)) → new_lt1(vwx3410, vwx3610, bdd, bde)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, hf), app(app(ty_Either, baa), bab)), ge)) → new_lt1(vwx3411, vwx3611, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_compare23(@2(vwx340, @3(vwx3410, vwx3411, vwx3412)), @2(vwx360, @3(vwx3610, vwx3611, vwx3612)), False, bch, app(app(app(ty_@3, app(app(ty_Either, gg), gh)), gd), ge)) → new_lt1(vwx3410, vwx3610, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4