Term Rewriting System R:

   [x, y, z]
   app(app(., 1), x) -> x
   app(app(., x), 1) -> x
   app(app(., app(i, x)), x) -> 1
   app(app(., x), app(i, x)) -> 1
   app(app(., app(i, y)), app(app(., y), z)) -> z
   app(app(., y), app(app(., app(i, y)), z)) -> z
   app(app(., app(app(., x), y)), z) -> app(app(., x), app(app(., y), z))
   app(i, 1) -> 1
   app(i, app(i, x)) -> x
   app(i, app(app(., x), y)) -> app(app(., app(i, y)), app(i, x))

Termination of R to be shown.


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

   app(app(., 1), x) -> x
   app(app(., x), 1) -> x
   app(app(., app(i, x)), x) -> 1
   app(app(., x), app(i, x)) -> 1
   app(app(., app(i, y)), app(app(., y), z)) -> z
   app(app(., y), app(app(., app(i, y)), z)) -> z

where the Polynomial interpretation:
POL(1) = 0
POL(i) = 0
POL(app(x_1, x_2)) = x_1 + x_2
POL(.) = 1
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: 


   APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))
   APP(app(., app(app(., x), y)), z) -> APP(app(., y), z)
   APP(app(., app(app(., x), y)), z) -> APP(., y)
   APP(i, app(app(., x), y)) -> APP(app(., app(i, y)), app(i, x))
   APP(i, app(app(., x), y)) -> APP(., app(i, y))
   APP(i, app(app(., x), y)) -> APP(i, y)
   APP(i, app(app(., x), y)) -> APP(i, x)

Furthermore, R contains one SCC.


SCC1:

APP(i, app(app(., x), y)) -> APP(i, x)
APP(i, app(app(., x), y)) -> APP(i, y)
APP(i, app(app(., x), y)) -> APP(app(., app(i, y)), app(i, x))
APP(app(., app(app(., x), y)), z) -> APP(app(., y), z)
APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))

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(1) = 0
POL(APP(x_1, x_2)) = 1 + x_1 + x_2
POL(i) = 0
POL(app(x_1, x_2)) = x_1 + x_2
POL(.) = 1

The following Dependency Pairs can be deleted:

   APP(i, app(app(., x), y)) -> APP(i, x)
   APP(i, app(app(., x), y)) -> APP(i, y)
   APP(app(., app(app(., x), y)), z) -> APP(app(., y), z)

No rules of R can be deleted.


 This transformation is resulting in one new subcycle:


SCC1.MRR1:

APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))
APP(i, app(app(., x), y)) -> APP(app(., app(i, y)), app(i, x))

On this Scc, a Narrowing SCC transformation can be performed.
 
As a result of transforming the rule 

   APP(i, app(app(., x), y)) -> APP(app(., app(i, y)), app(i, x))
six new Dependency Pairs
are created:


   APP(i, app(app(., x), app(app(., x''), y''))) -> APP(app(., app(app(., app(i, y'')), app(i, x''))), app(i, x))
   APP(i, app(app(., x), app(i, x''))) -> APP(app(., x''), app(i, x))
   APP(i, app(app(., x), 1)) -> APP(app(., 1), app(i, x))
   APP(i, app(app(., app(app(., x''), y'')), y)) -> APP(app(., app(i, y)), app(app(., app(i, y'')), app(i, x'')))
   APP(i, app(app(., app(i, x'')), y)) -> APP(app(., app(i, y)), x'')
   APP(i, app(app(., 1), y)) -> APP(app(., app(i, y)), 1)

The transformation is resulting in one subcycle:


SCC1.MRR1.Nar1:

APP(i, app(app(., 1), y)) -> APP(app(., app(i, y)), 1)
APP(i, app(app(., app(i, x'')), y)) -> APP(app(., app(i, y)), x'')
APP(i, app(app(., app(app(., x''), y'')), y)) -> APP(app(., app(i, y)), app(app(., app(i, y'')), app(i, x'')))
APP(i, app(app(., x), 1)) -> APP(app(., 1), app(i, x))
APP(i, app(app(., x), app(i, x''))) -> APP(app(., x''), app(i, x))
APP(i, app(app(., x), app(app(., x''), y''))) -> APP(app(., app(app(., app(i, y'')), app(i, x''))), app(i, x))
APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))

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

Additionally, the following rules can be oriented: 

   app(app(., app(app(., x), y)), z) -> app(app(., x), app(app(., y), z))
   app(i, app(app(., x), y)) -> app(app(., app(i, y)), app(i, x))
   app(i, app(i, x)) -> x
   app(i, 1) -> 1


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(1) = 0
POL(APP(x_1, x_2)) = 1 + x_1
POL(i) = 1
POL(app(x_1, x_2)) = x_1*x_2
POL(.) = 0

 resulting in one subcycle.


SCC1.MRR1.Nar1.Polo1:

APP(app(., app(app(., x), y)), z) -> APP(app(., x), app(app(., y), z))

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

Additionally, the following rules can be oriented: 

   app(app(., app(app(., x), y)), z) -> app(app(., x), app(app(., y), z))
   app(i, app(app(., x), y)) -> app(app(., app(i, y)), app(i, x))
   app(i, app(i, x)) -> x
   app(i, 1) -> 1


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(1) = 0
POL(APP(x_1, x_2)) = 1 + x_1
POL(i) = 0
POL(app(x_1, x_2)) = x_1 + x_2
POL(.) = 1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 24.331 seconds.