Term Rewriting System R:

   [x, y]
   p(0) -> 0
   p(s(x)) -> x
   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   minus(x, y) -> if(le(x, y), x, y)
   if(true, x, y) -> 0
   if(false, x, y) -> s(minus(p(x), y))

Innermost Termination of R to be shown.


R contains the following Dependency Pairs: 


   LE(s(x), s(y)) -> LE(x, y)
   IF(false, x, y) -> MINUS(p(x), y)
   IF(false, x, y) -> P(x)
   MINUS(x, y) -> IF(le(x, y), x, y)
   MINUS(x, y) -> LE(x, y)

Furthermore, R contains two SCCs.


SCC1:

LE(s(x), s(y)) -> LE(x, y)

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(LE(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   LE(s(x), s(y)) -> LE(x, y)



 This transformation is resulting in no new subcycles.


SCC2:

MINUS(x, y) -> IF(le(x, y), x, y)
IF(false, x, y) -> MINUS(p(x), y)

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

   MINUS(x, y) -> IF(le(x, y), x, y)
three new Dependency Pairs
are created:


   MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
   MINUS(0, y'') -> IF(true, 0, y'')
   MINUS(s(x''), 0) -> IF(false, s(x''), 0)

The transformation is resulting in one subcycle:


SCC2.Nar1:

MINUS(s(x''), 0) -> IF(false, s(x''), 0)
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
IF(false, x, y) -> MINUS(p(x), y)

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

   IF(false, x, y) -> MINUS(p(x), y)
two new Dependency Pairs
are created:


   IF(false, s(x''), y) -> MINUS(x'', y)
   IF(false, 0, y) -> MINUS(0, y)

The transformation is resulting in one subcycle:


SCC2.Nar1.Nar1:

MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
IF(false, s(x''), y) -> MINUS(x'', y)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)

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

   IF(false, s(x''), y) -> MINUS(x'', y)
two new Dependency Pairs
are created:


   IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
   IF(false, s(x''''), 0) -> MINUS(x'''', 0)

The transformation is resulting in two subcycles:


SCC2.Nar1.Nar1.Inst1:

IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))

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(s(x_1)) = 1 + x_1
POL(le(x_1, x_2)) = 0
POL(true) = 0
POL(MINUS(x_1, x_2)) = x_1
POL(0) = 0
POL(false) = 0
POL(IF(x_1, x_2, x_3)) = x_2

 resulting in no subcycles.


SCC2.Nar1.Nar1.Inst2:

IF(false, s(x''''), 0) -> MINUS(x'''', 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)

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(s(x_1)) = x_1
POL(MINUS(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(IF(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(false) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   le(s(x), s(y)) -> le(x, y)
   le(0, y) -> true
   le(s(x), 0) -> false
   p(s(x)) -> x
   p(0) -> 0


 This transformation is resulting in one new subcycle:


SCC2.Nar1.Nar1.Inst2.MRR1:

MINUS(s(x''), 0) -> IF(false, s(x''), 0)
IF(false, s(x''''), 0) -> MINUS(x'''', 0)

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(s(x_1)) = 1 + x_1
POL(MINUS(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(IF(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(false) = 0

The following Dependency Pairs can be deleted:

   IF(false, s(x''''), 0) -> MINUS(x'''', 0)



 This transformation is resulting in no new subcycles.




Innermost Termination of R successfully shown.


Duration: 10.840 seconds.