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)
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(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`
`     ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

aand(true, X) -> mark(X)
aand(false, Y) -> false
mark(and(X1, X2)) -> aand(mark(X1), X2)

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  1 + x1 + x2 POL(a__and(x1, x2)) =  1 + x1 + 2·x2 POL(false) =  0 POL(true) =  0 POL(mark(x1)) =  2·x1 POL(a__from(x1)) =  2·x1 POL(a__add(x1, x2)) =  x1 + 2·x2 POL(a__first(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(first(x1, x2)) =  x1 + x2 POL(0) =  0 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  x1 + 2·x2 + 2·x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

afirst(0, X) -> nil
mark(0) -> 0
aadd(0, X) -> mark(X)

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(false) =  0 POL(true) =  0 POL(mark(x1)) =  2·x1 POL(a__add(x1, x2)) =  x1 + 2·x2 POL(a__from(x1)) =  2·x1 POL(a__first(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(0) =  1 POL(first(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  x1 + 2·x2 + 2·x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

aif(false, X, Y) -> mark(Y)
mark(false) -> false

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(false) =  1 POL(true) =  0 POL(mark(x1)) =  2·x1 POL(a__from(x1)) =  2·x1 POL(a__add(x1, x2)) =  x1 + x2 POL(a__first(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(first(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  x1 + 2·x2 + 2·x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS4`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

aif(X1, X2, X3) -> if(X1, X2, X3)
aif(true, X, Y) -> mark(X)

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(true) =  0 POL(mark(x1)) =  2·x1 POL(a__from(x1)) =  2·x1 POL(a__add(x1, x2)) =  x1 + x2 POL(a__first(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  1 + x1 + x2 + x3 POL(first(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  2 + x1 + 2·x2 + x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS5`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

afrom(X) -> cons(X, from(s(X)))
afrom(X) -> from(X)

where the Polynomial interpretation:
 POL(from(x1)) =  1 + x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(true) =  0 POL(mark(x1)) =  2·x1 POL(a__from(x1)) =  2 + 2·x1 POL(a__add(x1, x2)) =  x1 + x2 POL(a__first(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(first(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  x1 + x2 + x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS6`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

mark(first(X1, X2)) -> afirst(mark(X1), mark(X2))

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(true) =  0 POL(mark(x1)) =  2·x1 POL(a__from(x1)) =  x1 POL(a__add(x1, x2)) =  x1 + x2 POL(a__first(x1, x2)) =  1 + x1 + x2 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(first(x1, x2)) =  1 + x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  x1 + x2 + x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS7`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

afirst(X1, X2) -> first(X1, X2)
afirst(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(true) =  0 POL(mark(x1)) =  x1 POL(a__add(x1, x2)) =  x1 + x2 POL(a__from(x1)) =  x1 POL(a__first(x1, x2)) =  1 + x1 + x2 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(first(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  x1 + x2 + x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS8`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

mark(if(X1, X2, X3)) -> aif(mark(X1), X2, X3)

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(true) =  0 POL(mark(x1)) =  x1 POL(a__add(x1, x2)) =  x1 + x2 POL(a__from(x1)) =  x1 POL(add(x1, x2)) =  x1 + x2 POL(if(x1, x2, x3)) =  1 + x1 + x2 + x3 POL(cons(x1, x2)) =  x1 + x2 POL(a__if(x1, x2, x3)) =  x1 + x2 + x3 POL(nil) =  0 POL(s(x1)) =  x1
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS9`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

mark(true) -> true

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(nil) =  0 POL(true) =  1 POL(s(x1)) =  x1 POL(mark(x1)) =  2·x1 POL(a__add(x1, x2)) =  x1 + x2 POL(a__from(x1)) =  x1 POL(add(x1, x2)) =  x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS10`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(nil) =  0 POL(s(x1)) =  x1 POL(mark(x1)) =  2·x1 POL(a__from(x1)) =  x1 POL(a__add(x1, x2)) =  1 + x1 + x2 POL(add(x1, x2)) =  1 + x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS11`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

mark(nil) -> nil

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(nil) =  1 POL(s(x1)) =  x1 POL(mark(x1)) =  2·x1 POL(a__from(x1)) =  x1 POL(a__add(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS12`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

mark(s(X)) -> s(X)
mark(cons(X1, X2)) -> cons(X1, X2)
mark(from(X)) -> afrom(X)

where the Polynomial interpretation:
 POL(from(x1)) =  x1 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(cons(x1, x2)) =  x1 + x2 POL(s(x1)) =  x1 POL(mark(x1)) =  1 + x1 POL(a__from(x1)) =  x1 POL(a__add(x1, x2)) =  x1 + x2 POL(add(x1, x2)) =  x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS13`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

where the Polynomial interpretation:
 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  x1 + x2 POL(s(x1)) =  x1 POL(a__add(x1, x2)) =  1 + x1 + x2 POL(add(x1, x2)) =  x1 + x2
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS14`
`                 ↳Removing Redundant Rules`

Removing the following rules from R which fullfill a polynomial ordering:

aand(X1, X2) -> and(X1, X2)

where the Polynomial interpretation:
 POL(and(x1, x2)) =  x1 + x2 POL(a__and(x1, x2)) =  1 + x1 + x2
was used.

All Rules of R can be deleted.

`   R`
`     ↳RRRPolo`
`       →TRS2`
`         ↳RRRPolo`
`           →TRS3`
`             ↳RRRPolo`
`             ...`
`               →TRS15`
`                 ↳Dependency Pair Analysis`

R contains no Dependency Pairs and therefore no SCCs.

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