Term Rewriting System R:
[X, Y, X1, X2, X3, Z]
aand(true, X) -> mark(X)
aand(false, Y) -> false
aand(X1, X2) -> and(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(add(X, Y))
aadd(X1, X2) -> add(X1, X2)
afirst(0, X) -> nil
afirst(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
afirst(X1, X2) -> first(X1, X2)
afrom(X) -> cons(X, from(s(X)))
afrom(X) -> from(X)
mark(and(X1, X2)) -> aand(mark(X1), X2)
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(add(X1, X2)) -> aadd(mark(X1), X2)
mark(first(X1, X2)) -> afirst(mark(X1), mark(X2))
mark(from(X)) -> afrom(X)
mark(true) -> true
mark(false) -> false
mark(0) -> 0
mark(s(X)) -> s(X)
mark(nil) -> nil
mark(cons(X1, X2)) -> cons(X1, X2)

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AAND(true, X) -> MARK(X)
AIF(true, X, Y) -> MARK(X)
AIF(false, X, Y) -> MARK(Y)
AADD(0, X) -> MARK(X)
MARK(and(X1, X2)) -> AAND(mark(X1), X2)
MARK(and(X1, X2)) -> MARK(X1)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
MARK(if(X1, X2, X3)) -> MARK(X1)
MARK(add(X1, X2)) -> AADD(mark(X1), X2)
MARK(add(X1, X2)) -> MARK(X1)
MARK(first(X1, X2)) -> AFIRST(mark(X1), mark(X2))
MARK(first(X1, X2)) -> MARK(X1)
MARK(first(X1, X2)) -> MARK(X2)
MARK(from(X)) -> AFROM(X)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Argument Filtering and Ordering


Dependency Pairs:

AIF(false, X, Y) -> MARK(Y)
MARK(first(X1, X2)) -> MARK(X2)
MARK(first(X1, X2)) -> MARK(X1)
MARK(add(X1, X2)) -> MARK(X1)
AADD(0, X) -> MARK(X)
MARK(add(X1, X2)) -> AADD(mark(X1), X2)
MARK(if(X1, X2, X3)) -> MARK(X1)
AIF(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
MARK(and(X1, X2)) -> MARK(X1)
MARK(and(X1, X2)) -> AAND(mark(X1), X2)
AAND(true, X) -> MARK(X)


Rules:


aand(true, X) -> mark(X)
aand(false, Y) -> false
aand(X1, X2) -> and(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(add(X, Y))
aadd(X1, X2) -> add(X1, X2)
afirst(0, X) -> nil
afirst(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
afirst(X1, X2) -> first(X1, X2)
afrom(X) -> cons(X, from(s(X)))
afrom(X) -> from(X)
mark(and(X1, X2)) -> aand(mark(X1), X2)
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(add(X1, X2)) -> aadd(mark(X1), X2)
mark(first(X1, X2)) -> afirst(mark(X1), mark(X2))
mark(from(X)) -> afrom(X)
mark(true) -> true
mark(false) -> false
mark(0) -> 0
mark(s(X)) -> s(X)
mark(nil) -> nil
mark(cons(X1, X2)) -> cons(X1, X2)


Strategy:

innermost




The following dependency pairs can be strictly oriented:

AIF(false, X, Y) -> MARK(Y)
MARK(first(X1, X2)) -> MARK(X2)
MARK(first(X1, X2)) -> MARK(X1)
MARK(add(X1, X2)) -> MARK(X1)
AADD(0, X) -> MARK(X)
MARK(add(X1, X2)) -> AADD(mark(X1), X2)
MARK(if(X1, X2, X3)) -> MARK(X1)
AIF(true, X, Y) -> MARK(X)
MARK(if(X1, X2, X3)) -> AIF(mark(X1), X2, X3)
MARK(and(X1, X2)) -> MARK(X1)
MARK(and(X1, X2)) -> AAND(mark(X1), X2)
AAND(true, X) -> MARK(X)


The following usable rules for innermost w.r.t. to the AFS can be oriented:

aand(true, X) -> mark(X)
aand(false, Y) -> false
aand(X1, X2) -> and(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
mark(and(X1, X2)) -> aand(mark(X1), X2)
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(add(X1, X2)) -> aadd(mark(X1), X2)
mark(first(X1, X2)) -> afirst(mark(X1), mark(X2))
mark(from(X)) -> afrom(X)
mark(true) -> true
mark(false) -> false
mark(0) -> 0
mark(s(X)) -> s(X)
mark(nil) -> nil
mark(cons(X1, X2)) -> cons(X1, X2)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(add(X, Y))
aadd(X1, X2) -> add(X1, X2)
afirst(0, X) -> nil
afirst(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
afirst(X1, X2) -> first(X1, X2)
afrom(X) -> cons(X, from(s(X)))
afrom(X) -> from(X)


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
{and, aand, AAND} > MARK
{afrom, from}
{add, aadd, AADD} > MARK
{add, aadd, AADD} > s
{afirst, first}
{aif, if} > AIF > MARK
{0, nil}

resulting in one new DP problem.
Used Argument Filtering System:
AAND(x1, x2) -> AAND(x1, x2)
MARK(x1) -> MARK(x1)
first(x1, x2) -> first(x1, x2)
add(x1, x2) -> add(x1, x2)
AADD(x1, x2) -> AADD(x1, x2)
mark(x1) -> x1
and(x1, x2) -> and(x1, x2)
if(x1, x2, x3) -> if(x1, x2, x3)
AIF(x1, x2, x3) -> AIF(x1, x2, x3)
aand(x1, x2) -> aand(x1, x2)
aif(x1, x2, x3) -> aif(x1, x2, x3)
aadd(x1, x2) -> aadd(x1, x2)
afirst(x1, x2) -> afirst(x1, x2)
from(x1) -> from(x1)
afrom(x1) -> afrom(x1)
s(x1) -> s(x1)
cons(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 2
Dependency Graph


Dependency Pair:


Rules:


aand(true, X) -> mark(X)
aand(false, Y) -> false
aand(X1, X2) -> and(X1, X2)
aif(true, X, Y) -> mark(X)
aif(false, X, Y) -> mark(Y)
aif(X1, X2, X3) -> if(X1, X2, X3)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(add(X, Y))
aadd(X1, X2) -> add(X1, X2)
afirst(0, X) -> nil
afirst(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))
afirst(X1, X2) -> first(X1, X2)
afrom(X) -> cons(X, from(s(X)))
afrom(X) -> from(X)
mark(and(X1, X2)) -> aand(mark(X1), X2)
mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)
mark(add(X1, X2)) -> aadd(mark(X1), X2)
mark(first(X1, X2)) -> afirst(mark(X1), mark(X2))
mark(from(X)) -> afrom(X)
mark(true) -> true
mark(false) -> false
mark(0) -> 0
mark(s(X)) -> s(X)
mark(nil) -> nil
mark(cons(X1, X2)) -> cons(X1, X2)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:05 minutes