Termination Proof using AProVE

Term Rewriting System R:
[x, y]
plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
times(0, y) -> 0
times(x, 0) -> 0
times(s(x), y) -> plus(times(x, y), y)
p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0
fac(s(x)) -> times(fac(p(s(x))), s(x))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

PLUS(x, s(y)) -> PLUS(x, y)
TIMES(s(x), y) -> PLUS(times(x, y), y)
TIMES(s(x), y) -> TIMES(x, y)
P(s(s(x))) -> P(s(x))
FAC(s(x)) -> TIMES(fac(p(s(x))), s(x))
FAC(s(x)) -> FAC(p(s(x)))
FAC(s(x)) -> P(s(x))

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Size-Change Principle

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳MRR

Dependency Pair:

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

Rules:

plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
times(0, y) -> 0
times(x, 0) -> 0
times(s(x), y) -> plus(times(x, y), y)
p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0
fac(s(x)) -> times(fac(p(s(x))), s(x))

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	=	1
2	>	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	=	1
2	>	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Size-Change Principle

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳MRR

Dependency Pair:

P(s(s(x))) -> P(s(x))

Rules:

plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
times(0, y) -> 0
times(x, 0) -> 0
times(s(x), y) -> plus(times(x, y), y)
p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0
fac(s(x)) -> times(fac(p(s(x))), s(x))

We number the DPs as follows:

P(s(s(x))) -> P(s(x))

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳Size-Change Principle

       →DP Problem 4

         ↳MRR

Dependency Pair:

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

Rules:

plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
times(0, y) -> 0
times(x, 0) -> 0
times(s(x), y) -> plus(times(x, y), y)
p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0
fac(s(x)) -> times(fac(p(s(x))), s(x))

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1
2	=	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1
2	=	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳Modular Removal of Rules

Dependency Pair:

FAC(s(x)) -> FAC(p(s(x)))

Rules:

plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
times(0, y) -> 0
times(x, 0) -> 0
times(s(x), y) -> plus(times(x, y), y)
p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0
fac(s(x)) -> times(fac(p(s(x))), s(x))

We have the following set of usable rules:

p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(0) = 0

POL(FAC(x₁)) = x₁

POL(s(x₁)) = x₁

POL(p(x₁)) = x₁

We have the following set D of usable symbols: {0, FAC, s, p}
No Dependency Pairs can be deleted.
6 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳MRR

           →DP Problem 5

             ↳Modular Removal of Rules

Dependency Pair:

FAC(s(x)) -> FAC(p(s(x)))

Rules:

p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0

We have the following set of usable rules:

p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(0) = 0

POL(FAC(x₁)) = 1 + x₁

POL(s(x₁)) = 1 + x₁

POL(p(x₁)) = x₁

We have the following set D of usable symbols: {0, FAC, s, p}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

p(s(0)) -> 0

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳MRR

           →DP Problem 5

             ↳MRR

...

               →DP Problem 6

                 ↳Non-Overlappingness Check

Dependency Pair:

FAC(s(x)) -> FAC(p(s(x)))

Rule:

p(s(s(x))) -> s(p(s(x)))

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle:

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳MRR

           →DP Problem 5

             ↳MRR

...

               →DP Problem 7

                 ↳Narrowing Transformation

Dependency Pair:

FAC(s(x)) -> FAC(p(s(x)))

Rule:

p(s(s(x))) -> s(p(s(x)))

Strategy:

innermost

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

FAC(s(x)) -> FAC(p(s(x)))

one new Dependency Pair is created:

FAC(s(s(x''))) -> FAC(s(p(s(x''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳MRR

           →DP Problem 5

             ↳MRR

...

               →DP Problem 8

                 ↳Negative Polynomial Order

Dependency Pair:

FAC(s(s(x''))) -> FAC(s(p(s(x''))))

Rule:

p(s(s(x))) -> s(p(s(x)))

Strategy:

innermost

The following Dependency Pair can be strictly oriented using the given order.

FAC(s(s(x''))) -> FAC(s(p(s(x''))))

Moreover, the following usable rules (regarding the implicit AFS) are oriented.

p(s(s(x))) -> s(p(s(x)))

Used ordering:
Polynomial Order with Interpretation:

POL( FAC(x₁) ) = max{0, x₁ - 1}

POL( s(x₁) ) = x₁ + 1

POL( p(x₁) ) = max{0, x₁ - 1}

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳MRR

           →DP Problem 5

             ↳MRR

...

               →DP Problem 9

                 ↳Dependency Graph

Dependency Pair:

Rule:

p(s(s(x))) -> s(p(s(x)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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

POL(0)	= 0
POL(FAC(x₁))	= x₁
POL(s(x₁))	= x₁
POL(p(x₁))	= x₁

POL(0)	= 0
POL(FAC(x₁))	= 1 + x₁
POL(s(x₁))	= 1 + x₁
POL(p(x₁))	= x₁