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)

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:

mark(add(X1, X2)) -> aadd(mark(X1), X2)

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:

aadd(s(X), Y) -> s(add(X, Y))
aadd(X1, X2) -> add(X1, X2)

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
Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.


   R
RRRPolo
       →TRS2
RRRPolo
           →TRS3
RRRPolo
             ...
               →TRS16
Dependency Pair Analysis



R contains no Dependency Pairs and therefore no SCCs.

Termination of R successfully shown.
Duration:
0:00 minutes