(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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, 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(h(del(max(cons(x, xs)), cons(x, xs))))
SORT(cons(x, xs)) → H(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)
H(cons(x, xs)) → H(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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, 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 6 SCCs with 5 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(cons(x, xs)) → H(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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, 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:
H(cons(x, xs)) → H(xs)
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))
h(nil)
h(cons(x0, 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))
h(nil)
h(cons(x0, x1))
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(cons(x, xs)) → H(xs)
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:
- H(cons(x, xs)) → H(xs)
The graph contains the following edges 1 > 1
(13) TRUE
(14) 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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, 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:
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))
h(nil)
h(cons(x0, 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))
h(nil)
h(cons(x0, x1))
(18) 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.
(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:
- GE(s(x), s(y)) → GE(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:
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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, 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:
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))
h(nil)
h(cons(x0, 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)
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))
h(nil)
h(cons(x0, x1))
(25) 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.
(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:
- EQ(s(x), s(y)) → EQ(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(27) TRUE
(28) 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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, 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:
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))
h(nil)
h(cons(x0, 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)
sort(nil)
sort(cons(x0, x1))
ge(0, 0)
ge(s(x0), 0)
ge(0, s(x0))
ge(s(x0), s(x1))
h(nil)
h(cons(x0, x1))
(32) 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.
(33) 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
(34) TRUE
(35) 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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(36) 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.
(37) 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))
h(nil)
h(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(38) 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))
h(nil)
h(cons(x0, x1))
(39) 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.
(40) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, 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
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x, y, xs) → MAX(cons(x, 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.
(42) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(43) TRUE
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SORT(cons(x, xs)) → SORT(h(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(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(xs))
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))
h(nil)
h(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(45) 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.
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SORT(cons(x, xs)) → SORT(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(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))
h(nil)
h(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(47) 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))
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SORT(cons(x, xs)) → SORT(h(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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(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))
h(nil)
h(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(49) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:SORT(
cons(
x,
xs)) →
SORT(
h(
del(
max(
cons(
x,
xs)),
cons(
x,
xs))))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 0
POL(SORT(x1)) = x1
POL(cons(x1, x2)) = 1 + 2·x1 + 2·x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = 1
POL(false) = 0
POL(ge(x1, x2)) = 1
POL(h(x1)) = x1
POL(if1(x1, x2, x3, x4)) = 1 + 2·x1 + 2·x2 + 2·x3 + 3·x4
POL(if2(x1, x2, x3, x4)) = 1 + 2·x3 + 2·x4
POL(max(x1)) = x1
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = 1
At least one of these decreasing rules is always used after the deleted DP:if2(
true,
x1609,
y1039,
xs809) →
xs809The following formula is valid:z0:sort[a36].(¬(
z0 =
nil)→
del'(
max(
z0 ),
z0 )=
true)
The transformed set:del'(
x58,
cons(
y37,
xs29)) →
if2'(
eq(
x58,
y37),
x58,
y37,
xs29)
if2'(
true,
x160,
y103,
xs80) →
trueif2'(
false,
x175,
y113,
xs88) →
del'(
x175,
xs88)
del'(
x190,
nil) →
falsemax(
cons(
x,
nil)) →
xmax(
cons(
x13,
cons(
y7,
xs5))) →
if1(
ge(
x13,
y7),
x13,
y7,
xs5)
if1(
true,
x28,
y17,
xs13) →
max(
cons(
x28,
xs13))
if1(
false,
x43,
y27,
xs21) →
max(
cons(
y27,
xs21))
del(
x58,
cons(
y37,
xs29)) →
if2(
eq(
x58,
y37),
x58,
y37,
xs29)
h(
nil) →
nilh(
cons(
x87,
xs44)) →
cons(
x87,
h(
xs44))
eq(
0,
0) →
trueeq(
0,
s(
y74)) →
falseeq(
s(
x130),
0) →
falseeq(
s(
x145),
s(
y93)) →
eq(
x145,
y93)
if2(
true,
x160,
y103,
xs80) →
xs80if2(
false,
x175,
y113,
xs88) →
cons(
y113,
del(
x175,
xs88))
del(
x190,
nil) →
nilge(
0,
0) →
truege(
s(
x219),
0) →
truege(
0,
s(
x234)) →
falsege(
s(
x249),
s(
y159)) →
ge(
x249,
y159)
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[a36](
cons(
x0,
x1),
cons(
x2,
x3)) →
and(
equal_sort[a36](
x0,
x2),
equal_sort[a36](
x1,
x3))
equal_sort[a36](
cons(
x0,
x1),
nil) →
falseequal_sort[a36](
nil,
cons(
x0,
x1)) →
falseequal_sort[a36](
nil,
nil) →
trueequal_sort[a64](
witness_sort[a64],
witness_sort[a64]) →
true
(50) Complex Obligation (AND)
(51) 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)
h(nil) → nil
h(cons(x, xs)) → cons(x, h(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))
h(nil)
h(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(52) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(53) TRUE
(54) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true
Q is empty.
(55) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(56) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(57) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
DEL'(x58, cons(y37, xs29)) → EQ(x58, y37)
IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
MAX(cons(x13, cons(y7, xs5))) → GE(x13, y7)
IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
DEL(x58, cons(y37, xs29)) → EQ(x58, y37)
H(cons(x87, xs44)) → H(xs44)
EQ(s(x145), s(y93)) → EQ(x145, y93)
IF2(false, x175, y113, xs88) → DEL(x175, xs88)
GE(s(x249), s(y159)) → GE(x249, y159)
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
We have to consider all minimal (P,Q,R)-chains.
(59) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 4 less nodes.
(60) Complex Obligation (AND)
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)
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[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x1, x3)
The graph contains the following edges 1 > 1, 2 > 2
- EQUAL_SORT[A36](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A36](x0, x2)
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:
EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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:
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(72) 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.
(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:
- EQUAL_SORT[A0](s(x0), s(x1)) → EQUAL_SORT[A0](x0, x1)
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:
GE(s(x249), s(y159)) → GE(x249, y159)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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:
GE(s(x249), s(y159)) → GE(x249, y159)
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(79) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x249), s(y159)) → GE(x249, y159)
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:
- GE(s(x249), s(y159)) → GE(x249, y159)
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:
EQ(s(x145), s(y93)) → EQ(x145, y93)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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:
EQ(s(x145), s(y93)) → EQ(x145, y93)
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x145), s(y93)) → EQ(x145, y93)
R is empty.
Q is empty.
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:
- EQ(s(x145), s(y93)) → EQ(x145, y93)
The graph contains the following edges 1 > 1, 2 > 2
(88) TRUE
(89) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(cons(x87, xs44)) → H(xs44)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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:
H(cons(x87, xs44)) → H(xs44)
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(93) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(cons(x87, xs44)) → H(xs44)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(94) 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:
- H(cons(x87, xs44)) → H(xs44)
The graph contains the following edges 1 > 1
(95) TRUE
(96) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x175, y113, xs88) → DEL(x175, xs88)
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
We have to consider all minimal (P,Q,R)-chains.
(97) 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.
(98) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x175, y113, xs88) → DEL(x175, xs88)
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
We have to consider all minimal (P,Q,R)-chains.
(99) 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))
h(nil)
h(cons(x0, 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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(100) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(false, x175, y113, xs88) → DEL(x175, xs88)
DEL(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
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.
(101) 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(x58, cons(y37, xs29)) → IF2(eq(x58, y37), x58, y37, xs29)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
- IF2(false, x175, y113, xs88) → DEL(x175, xs88)
The graph contains the following edges 2 >= 1, 4 >= 2
(102) TRUE
(103) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
We have to consider all minimal (P,Q,R)-chains.
(104) 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.
(105) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
We have to consider all minimal (P,Q,R)-chains.
(106) 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(107) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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.
(108) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MAX(cons(x13, cons(y7, xs5))) → IF1(ge(x13, y7), x13, y7, xs5)
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
(109) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, x28, y17, xs13) → MAX(cons(x28, xs13))
IF1(false, x43, y27, xs21) → MAX(cons(y27, xs21))
The TRS R consists of the following rules:
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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.
(110) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(111) TRUE
(112) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
The TRS R consists of the following rules:
del'(x58, cons(y37, xs29)) → if2'(eq(x58, y37), x58, y37, xs29)
if2'(true, x160, y103, xs80) → true
if2'(false, x175, y113, xs88) → del'(x175, xs88)
del'(x190, nil) → false
max(cons(x, nil)) → x
max(cons(x13, cons(y7, xs5))) → if1(ge(x13, y7), x13, y7, xs5)
if1(true, x28, y17, xs13) → max(cons(x28, xs13))
if1(false, x43, y27, xs21) → max(cons(y27, xs21))
del(x58, cons(y37, xs29)) → if2(eq(x58, y37), x58, y37, xs29)
h(nil) → nil
h(cons(x87, xs44)) → cons(x87, h(xs44))
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
if2(true, x160, y103, xs80) → xs80
if2(false, x175, y113, xs88) → cons(y113, del(x175, xs88))
del(x190, nil) → nil
ge(0, 0) → true
ge(s(x219), 0) → true
ge(0, s(x234)) → false
ge(s(x249), s(y159)) → ge(x249, y159)
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[a36](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a36](x0, x2), equal_sort[a36](x1, x3))
equal_sort[a36](cons(x0, x1), nil) → false
equal_sort[a36](nil, cons(x0, x1)) → false
equal_sort[a36](nil, nil) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → 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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
We have to consider all minimal (P,Q,R)-chains.
(113) 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.
(114) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
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))
h(nil)
h(cons(x0, x1))
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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
We have to consider all minimal (P,Q,R)-chains.
(115) 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))
h(nil)
h(cons(x0, 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[a36](cons(x0, x1), cons(x2, x3))
equal_sort[a36](cons(x0, x1), nil)
equal_sort[a36](nil, cons(x0, x1))
equal_sort[a36](nil, nil)
equal_sort[a64](witness_sort[a64], witness_sort[a64])
(116) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
DEL'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x130), 0) → false
eq(s(x145), s(y93)) → eq(x145, y93)
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.
(117) 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'(x58, cons(y37, xs29)) → IF2'(eq(x58, y37), x58, y37, xs29)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
- IF2'(false, x175, y113, xs88) → DEL'(x175, xs88)
The graph contains the following edges 2 >= 1, 4 >= 2
(118) TRUE