(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
Q is empty.
(1) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
MAX(cons(x, cons(y, xs))) → GE(x, y)
IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF2(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
SORT(cons(x, xs)) → MAX(cons(x, xs))
SORT(cons(x, xs)) → SORT(del(max(cons(x, xs)), cons(x, xs)))
SORT(cons(x, xs)) → DEL(max(cons(x, xs)), cons(x, xs))
GE(s(x), s(y)) → GE(x, y)
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(8) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
R is empty.
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(10) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(13) TRUE
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x), s(y)) → EQ(x, y)
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(15) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x), s(y)) → EQ(x, y)
R is empty.
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(17) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x), s(y)) → EQ(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- EQ(s(x), s(y)) → EQ(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(20) TRUE
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(22) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(24) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(26) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
- IF2(false, x, y, xs) → DEL(x, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
(27) TRUE
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(29) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(31) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(33) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(IF1(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(ge(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
none
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(35) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(36) TRUE
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SORT(cons(x, xs)) → SORT(del(max(cons(x, xs)), cons(x, xs)))
The TRS R consists of the following rules:
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(nil) → nil
sort(cons(x, xs)) → cons(max(cons(x, xs)), sort(del(max(cons(x, xs)), cons(x, xs))))
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(38) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SORT(cons(x, xs)) → SORT(del(max(cons(x, xs)), cons(x, xs)))
The TRS R consists of the following rules:
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(40) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
sort(nil)
sort(cons(x0, x1))
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SORT(cons(x, xs)) → SORT(del(max(cons(x, xs)), cons(x, xs)))
The TRS R consists of the following rules:
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(42) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:SORT(
cons(
x,
xs)) →
SORT(
del(
max(
cons(
x,
xs)),
cons(
x,
xs)))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 0
POL(SORT(x1)) = 2·x1
POL(cons(x1, x2)) = 1 + x1 + 2·x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = 1 + 2·x1
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(if1(x1, x2, x3, x4)) = 2 + x2 + x3 + 2·x4
POL(if2(x1, x2, x3, x4)) = 1 + x3 + 2·x4
POL(max(x1)) = x1
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
At least one of these decreasing rules is always used after the deleted DP:if2(
true,
x1227,
y857,
xs567) →
xs567The following formula is valid:z0:sort[a34].(¬(
z0 =
nil)→
del'(
max(
z0 ),
z0 )=
true)
The transformed set:del'(
x54,
cons(
y37,
xs25)) →
if2'(
eq(
x54,
y37),
x54,
y37,
xs25)
if2'(
true,
x122,
y85,
xs56) →
trueif2'(
false,
x136,
y95,
xs63) →
del'(
x136,
xs63)
del'(
x150,
nil) →
falsemax(
cons(
x,
nil)) →
xmax(
cons(
x12,
cons(
y7,
xs4))) →
if1(
ge(
x12,
y7),
x12,
y7,
xs4)
if1(
true,
x26,
y17,
xs11) →
max(
cons(
x26,
xs11))
if1(
false,
x40,
y27,
xs18) →
max(
cons(
y27,
xs18))
del(
x54,
cons(
y37,
xs25)) →
if2(
eq(
x54,
y37),
x54,
y37,
xs25)
eq(
0,
0) →
trueeq(
0,
s(
y56)) →
falseeq(
s(
x94),
0) →
falseeq(
s(
x108),
s(
y75)) →
eq(
x108,
y75)
if2(
true,
x122,
y85,
xs56) →
xs56if2(
false,
x136,
y95,
xs63) →
cons(
y95,
del(
x136,
xs63))
del(
x150,
nil) →
nilge(
0,
0) →
truege(
s(
x177),
0) →
truege(
0,
s(
x191)) →
falsege(
s(
x205),
s(
y141)) →
ge(
x205,
y141)
max(
nil) →
0equal_bool(
true,
false) →
falseequal_bool(
false,
true) →
falseequal_bool(
true,
true) →
trueequal_bool(
false,
false) →
trueand(
true,
x) →
xand(
false,
x) →
falseor(
true,
x) →
trueor(
false,
x) →
xnot(
false) →
truenot(
true) →
falseisa_true(
true) →
trueisa_true(
false) →
falseisa_false(
true) →
falseisa_false(
false) →
trueequal_sort[a0](
0,
0) →
trueequal_sort[a0](
0,
s(
x0)) →
falseequal_sort[a0](
s(
x0),
0) →
falseequal_sort[a0](
s(
x0),
s(
x1)) →
equal_sort[a0](
x0,
x1)
equal_sort[a34](
nil,
nil) →
trueequal_sort[a34](
nil,
cons(
x0,
x1)) →
falseequal_sort[a34](
cons(
x0,
x1),
nil) →
falseequal_sort[a34](
cons(
x0,
x1),
cons(
x2,
x3)) →
and(
equal_sort[a34](
x0,
x2),
equal_sort[a34](
x1,
x3))
equal_sort[a60](
witness_sort[a60],
witness_sort[a60]) →
true
(43) Complex Obligation (AND)
(44) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
ge(0, 0) → true
ge(s(x), 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(45) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(46) TRUE
(47) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
Q is empty.
(48) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(49) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(50) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DEL'(x54, cons(y37, xs25)) → IF2'(eq(x54, y37), x54, y37, xs25)
DEL'(x54, cons(y37, xs25)) → EQ(x54, y37)
IF2'(false, x136, y95, xs63) → DEL'(x136, xs63)
MAX(cons(x12, cons(y7, xs4))) → IF1(ge(x12, y7), x12, y7, xs4)
MAX(cons(x12, cons(y7, xs4))) → GE(x12, y7)
IF1(true, x26, y17, xs11) → MAX(cons(x26, xs11))
IF1(false, x40, y27, xs18) → MAX(cons(y27, xs18))
DEL(x54, cons(y37, xs25)) → IF2(eq(x54, y37), x54, y37, xs25)
DEL(x54, cons(y37, xs25)) → EQ(x54, y37)
EQ(s(x108), s(y75)) → EQ(x108, y75)
IF2(false, x136, y95, xs63) → DEL(x136, xs63)
GE(s(x205), s(y141)) → GE(x205, y141)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(52) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 7 SCCs with 4 less nodes.
(53) Complex Obligation (AND)
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(55) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
R is empty.
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(57) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(59) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
The graph contains the following edges 1 > 1, 2 > 2
- EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
The graph contains the following edges 1 > 1, 2 > 2
(60) TRUE
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(62) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
R is empty.
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(64) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(66) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
The graph contains the following edges 1 > 1, 2 > 2
(67) TRUE
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x205), s(y141)) → GE(x205, y141)
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(69) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x205), s(y141)) → GE(x205, y141)
R is empty.
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(71) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x205), s(y141)) → GE(x205, y141)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(73) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- GE(s(x205), s(y141)) → GE(x205, y141)
The graph contains the following edges 1 > 1, 2 > 2
(74) TRUE
(75) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x108), s(y75)) → EQ(x108, y75)
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(76) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(77) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x108), s(y75)) → EQ(x108, y75)
R is empty.
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(78) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(79) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x108), s(y75)) → EQ(x108, y75)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(80) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- EQ(s(x108), s(y75)) → EQ(x108, y75)
The graph contains the following edges 1 > 1, 2 > 2
(81) TRUE
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x136, y95, xs63) → DEL(x136, xs63)
DEL(x54, cons(y37, xs25)) → IF2(eq(x54, y37), x54, y37, xs25)
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(83) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x136, y95, xs63) → DEL(x136, xs63)
DEL(x54, cons(y37, xs25)) → IF2(eq(x54, y37), x54, y37, xs25)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(85) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x136, y95, xs63) → DEL(x136, xs63)
DEL(x54, cons(y37, xs25)) → IF2(eq(x54, y37), x54, y37, xs25)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(87) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- DEL(x54, cons(y37, xs25)) → IF2(eq(x54, y37), x54, y37, xs25)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
- IF2(false, x136, y95, xs63) → DEL(x136, xs63)
The graph contains the following edges 2 >= 1, 4 >= 2
(88) TRUE
(89) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x26, y17, xs11) → MAX(cons(x26, xs11))
MAX(cons(x12, cons(y7, xs4))) → IF1(ge(x12, y7), x12, y7, xs4)
IF1(false, x40, y27, xs18) → MAX(cons(y27, xs18))
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(90) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(91) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x26, y17, xs11) → MAX(cons(x26, xs11))
MAX(cons(x12, cons(y7, xs4))) → IF1(ge(x12, y7), x12, y7, xs4)
IF1(false, x40, y27, xs18) → MAX(cons(y27, xs18))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(92) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(93) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x26, y17, xs11) → MAX(cons(x26, xs11))
MAX(cons(x12, cons(y7, xs4))) → IF1(ge(x12, y7), x12, y7, xs4)
IF1(false, x40, y27, xs18) → MAX(cons(y27, xs18))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(94) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MAX(cons(x12, cons(y7, xs4))) → IF1(ge(x12, y7), x12, y7, xs4)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(IF1(x1, x2, x3, x4)) = 1 + x2 + x3 + x4
POL(MAX(x1)) = x1
POL(cons(x1, x2)) = 1 + x1 + x2
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(s(x1)) = 0
POL(true) = 0
The following usable rules [FROCOS05] were oriented:
none
(95) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x26, y17, xs11) → MAX(cons(x26, xs11))
IF1(false, x40, y27, xs18) → MAX(cons(y27, xs18))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
The set Q consists of the following terms:
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(96) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(97) TRUE
(98) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2'(false, x136, y95, xs63) → DEL'(x136, xs63)
DEL'(x54, cons(y37, xs25)) → IF2'(eq(x54, y37), x54, y37, xs25)
The TRS R consists of the following rules:
del'(x54, cons(y37, xs25)) → if2'(eq(x54, y37), x54, y37, xs25)
if2'(true, x122, y85, xs56) → true
if2'(false, x136, y95, xs63) → del'(x136, xs63)
del'(x150, nil) → false
max(cons(x, nil)) → x
max(cons(x12, cons(y7, xs4))) → if1(ge(x12, y7), x12, y7, xs4)
if1(true, x26, y17, xs11) → max(cons(x26, xs11))
if1(false, x40, y27, xs18) → max(cons(y27, xs18))
del(x54, cons(y37, xs25)) → if2(eq(x54, y37), x54, y37, xs25)
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
if2(true, x122, y85, xs56) → xs56
if2(false, x136, y95, xs63) → cons(y95, del(x136, xs63))
del(x150, nil) → nil
ge(0, 0) → true
ge(s(x177), 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
max(nil) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60]) → true
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(99) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(100) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2'(false, x136, y95, xs63) → DEL'(x136, xs63)
DEL'(x54, cons(y37, xs25)) → IF2'(eq(x54, y37), x54, y37, xs25)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
The set Q consists of the following terms:
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
We have to consider all minimal (P,Q,R)-chains.
(101) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
del'(x0, nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
del(x0, nil)
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
max(nil)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a0](0, 0)
equal_sort[a0](0, s(x0))
equal_sort[a0](s(x0), 0)
equal_sort[a0](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a60](witness_sort[a60], witness_sort[a60])
(102) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2'(false, x136, y95, xs63) → DEL'(x136, xs63)
DEL'(x54, cons(y37, xs25)) → IF2'(eq(x54, y37), x54, y37, xs25)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y56)) → false
eq(s(x94), 0) → false
eq(s(x108), s(y75)) → eq(x108, y75)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(103) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:
- DEL'(x54, cons(y37, xs25)) → IF2'(eq(x54, y37), x54, y37, xs25)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
- IF2'(false, x136, y95, xs63) → DEL'(x136, xs63)
The graph contains the following edges 2 >= 1, 4 >= 2
(104) TRUE