Term Rewriting System R:

   [x, y]
   +(x, 0) -> x
   +(x, s(y)) -> s(+(x, y))
   *(x, 0) -> 0
   *(x, s(y)) -> +(*(x, y), x)
   ge(x, 0) -> true
   ge(0, s(y)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   -(x, 0) -> x
   -(s(x), s(y)) -> -(x, y)
   fact(x) -> iffact(x, ge(x, s(s(0))))
   iffact(x, true) -> *(x, fact(-(x, s(0))))
   iffact(x, false) -> s(0)

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   +'(x, s(y)) -> +'(x, y)
   GE(s(x), s(y)) -> GE(x, y)
   -'(s(x), s(y)) -> -'(x, y)
   IFFACT(x, true) -> *'(x, fact(-(x, s(0))))
   IFFACT(x, true) -> FACT(-(x, s(0)))
   IFFACT(x, true) -> -'(x, s(0))
   *'(x, s(y)) -> +'(*(x, y), x)
   *'(x, s(y)) -> *'(x, y)
   FACT(x) -> IFFACT(x, ge(x, s(s(0))))
   FACT(x) -> GE(x, s(s(0)))

Furthermore, R contains five SCCs.


SCC1:

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

The following Dependency Pairs can be deleted:

   +'(x, s(y)) -> +'(x, y)



 This transformation is resulting in no new subcycles.


SCC2:

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

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC3:

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

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC4:

*'(x, s(y)) -> *'(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(s(x_1)) = 1 + x_1
POL(*'(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   *'(x, s(y)) -> *'(x, y)



 This transformation is resulting in no new subcycles.


SCC5:

FACT(x) -> IFFACT(x, ge(x, s(s(0))))
IFFACT(x, true) -> FACT(-(x, s(0)))

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

   FACT(x) -> IFFACT(x, ge(x, s(s(0))))
two new Dependency Pairs
are created:


   FACT(0) -> IFFACT(0, false)
   FACT(s(x'')) -> IFFACT(s(x''), ge(x'', s(0)))

The transformation is resulting in one subcycle:


SCC5.Nar1:

FACT(s(x'')) -> IFFACT(s(x''), ge(x'', s(0)))
IFFACT(x, true) -> FACT(-(x, s(0)))

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

   IFFACT(x, true) -> FACT(-(x, s(0)))
one new Dependency Pair
is created:


   IFFACT(s(x''), true) -> FACT(-(x'', 0))

The transformation is resulting in one subcycle:


SCC5.Nar1.Nar1:

IFFACT(s(x''), true) -> FACT(-(x'', 0))
FACT(s(x'')) -> IFFACT(s(x''), ge(x'', s(0)))

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

   IFFACT(s(x''), true) -> FACT(-(x'', 0))
one new Dependency Pair
is created:


   IFFACT(s(x''), true) -> FACT(x'')

The transformation is resulting in one subcycle:


SCC5.Nar1.Nar1.Rewr1:

IFFACT(s(x''), true) -> FACT(x'')
FACT(s(x'')) -> IFFACT(s(x''), ge(x'', s(0)))

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(ge(x_1, x_2)) = 0
POL(true) = 0
POL(FACT(x_1)) = x_1
POL(0) = 0
POL(IFFACT(x_1, x_2)) = x_1
POL(false) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 10.909 seconds.