Term Rewriting System R:

   [x, y, z]
   a(lambda(x), y) -> lambda(a(x, 1))
   a(lambda(x), y) -> lambda(a(x, a(y, t)))
   a(a(x, y), z) -> a(x, a(y, z))
   a(x, y) -> x
   a(x, y) -> y
   lambda(x) -> x

Termination of R to be shown.


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

   lambda(x) -> x

where the Polynomial interpretation:
POL(lambda(x_1)) = 1 + x_1
POL(1) = 0
POL(a(x_1, x_2)) = x_1 + x_2
POL(t) = 0
was used. 



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


R contains the following Dependency Pairs: 


   A(lambda(x), y) -> A(x, a(y, t))
   A(lambda(x), y) -> A(y, t)
   A(lambda(x), y) -> A(x, 1)
   A(a(x, y), z) -> A(x, a(y, z))
   A(a(x, y), z) -> A(y, z)

Furthermore, R contains one SCC.


SCC1:

A(a(x, y), z) -> A(y, z)
A(a(x, y), z) -> A(x, a(y, z))
A(lambda(x), y) -> A(x, 1)
A(lambda(x), y) -> A(y, t)
A(lambda(x), y) -> A(x, a(y, t))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(lambda(x_1)) = 1 + x_1
POL(1) = 0
POL(a(x_1, x_2)) = x_1 + x_2
POL(A(x_1, x_2)) = 1 + x_1 + x_2
POL(t) = 0

The following Dependency Pairs can be deleted:

   A(lambda(x), y) -> A(x, 1)
   A(lambda(x), y) -> A(y, t)
   A(lambda(x), y) -> A(x, a(y, t))

No rules of R can be deleted.


 This transformation is resulting in one new subcycle:


SCC1.MRR1:

A(a(x, y), z) -> A(x, a(y, z))
A(a(x, y), z) -> A(y, z)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(lambda(x_1)) = 0
POL(1) = 0
POL(a(x_1, x_2)) = 1 + x_1 + x_2
POL(A(x_1, x_2)) = x_1
POL(t) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.676 seconds.