Term Rewriting System R:
[x, y, z]
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)
if(true, x, y) -> x
if(false, x, y) -> y
if(true, x, y) -> true
if(false, x, y) -> false
odd(0) -> false
odd(s(0)) -> true
odd(s(s(x))) -> odd(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
pow(x, y) -> f(x, y, s(0))
f(x, 0, z) -> z
f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))

Innermost Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

-'(s(x), s(y)) -> -'(x, y)
*'(x, s(y)) -> *'(x, y)
ODD(s(s(x))) -> ODD(x)
HALF(s(s(x))) -> HALF(x)
POW(x, y) -> F(x, y, s(0))
F(x, s(y), z) -> IF(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))
F(x, s(y), z) -> ODD(s(y))
F(x, s(y), z) -> F(x, y, *(x, z))
F(x, s(y), z) -> *'(x, z)
F(x, s(y), z) -> F(*(x, x), half(s(y)), z)
F(x, s(y), z) -> *'(x, x)
F(x, s(y), z) -> HALF(s(y))

Furthermore, R contains five SCCs.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Usable Rules (Innermost)`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

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

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)
if(true, x, y) -> x
if(false, x, y) -> y
if(true, x, y) -> true
if(false, x, y) -> false
odd(0) -> false
odd(s(0)) -> true
odd(s(s(x))) -> odd(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
pow(x, y) -> f(x, y, s(0))
f(x, 0, z) -> z
f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))

Strategy:

innermost

As we are in the innermost case, we can delete all 17 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`           →DP Problem 6`
`             ↳Size-Change Principle`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:
1. -'(s(x), s(y)) -> -'(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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳Usable Rules (Innermost)`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

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

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)
if(true, x, y) -> x
if(false, x, y) -> y
if(true, x, y) -> true
if(false, x, y) -> false
odd(0) -> false
odd(s(0)) -> true
odd(s(s(x))) -> odd(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
pow(x, y) -> f(x, y, s(0))
f(x, 0, z) -> z
f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))

Strategy:

innermost

As we are in the innermost case, we can delete all 17 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`           →DP Problem 7`
`             ↳Size-Change Principle`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:
1. *'(x, s(y)) -> *'(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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳Usable Rules (Innermost)`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

ODD(s(s(x))) -> ODD(x)

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)
if(true, x, y) -> x
if(false, x, y) -> y
if(true, x, y) -> true
if(false, x, y) -> false
odd(0) -> false
odd(s(0)) -> true
odd(s(s(x))) -> odd(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
pow(x, y) -> f(x, y, s(0))
f(x, 0, z) -> z
f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))

Strategy:

innermost

As we are in the innermost case, we can delete all 17 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`           →DP Problem 8`
`             ↳Size-Change Principle`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

ODD(s(s(x))) -> ODD(x)

Rule:

none

Strategy:

innermost

We number the DPs as follows:
1. ODD(s(s(x))) -> ODD(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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳Usable Rules (Innermost)`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

HALF(s(s(x))) -> HALF(x)

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)
if(true, x, y) -> x
if(false, x, y) -> y
if(true, x, y) -> true
if(false, x, y) -> false
odd(0) -> false
odd(s(0)) -> true
odd(s(s(x))) -> odd(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
pow(x, y) -> f(x, y, s(0))
f(x, 0, z) -> z
f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))

Strategy:

innermost

As we are in the innermost case, we can delete all 17 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`           →DP Problem 9`
`             ↳Size-Change Principle`
`       →DP Problem 5`
`         ↳UsableRules`

Dependency Pair:

HALF(s(s(x))) -> HALF(x)

Rule:

none

Strategy:

innermost

We number the DPs as follows:
1. HALF(s(s(x))) -> HALF(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

DP: empty set
Oriented Rules: none

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

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳Usable Rules (Innermost)`

Dependency Pairs:

F(x, s(y), z) -> F(*(x, x), half(s(y)), z)
F(x, s(y), z) -> F(x, y, *(x, z))

Rules:

-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)
if(true, x, y) -> x
if(false, x, y) -> y
if(true, x, y) -> true
if(false, x, y) -> false
odd(0) -> false
odd(s(0)) -> true
odd(s(s(x))) -> odd(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
pow(x, y) -> f(x, y, s(0))
f(x, 0, z) -> z
f(x, s(y), z) -> if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z))

Strategy:

innermost

As we are in the innermost case, we can delete all 12 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Negative Polynomial Order`

Dependency Pairs:

F(x, s(y), z) -> F(*(x, x), half(s(y)), z)
F(x, s(y), z) -> F(x, y, *(x, z))

Rules:

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Strategy:

innermost

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

F(x, s(y), z) -> F(x, y, *(x, z))

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

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Used ordering:
Polynomial Order with Interpretation:

POL( F(x1, ..., x3) ) = x2

POL( s(x1) ) = x1 + 1

POL( half(x1) ) = x1

POL( 0 ) = 0

POL( *(x1, x2) ) = 0

POL( +(x1, x2) ) = 0

This results in one new DP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Neg POLO`
`             ...`
`               →DP Problem 11`
`                 ↳Narrowing Transformation`

Dependency Pair:

F(x, s(y), z) -> F(*(x, x), half(s(y)), z)

Rules:

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Strategy:

innermost

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

F(x, s(y), z) -> F(*(x, x), half(s(y)), z)
four new Dependency Pairs are created:

F(0, s(y), z) -> F(0, half(s(y)), z)
F(s(y''), s(y), z) -> F(+(*(s(y''), y''), s(y'')), half(s(y)), z)
F(x, s(0), z) -> F(*(x, x), 0, z)
F(x, s(s(x'')), z) -> F(*(x, x), s(half(x'')), z)

The transformation is resulting in one new DP problem:

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Neg POLO`
`             ...`
`               →DP Problem 12`
`                 ↳Negative Polynomial Order`

Dependency Pairs:

F(s(y''), s(y), z) -> F(+(*(s(y''), y''), s(y'')), half(s(y)), z)
F(x, s(s(x'')), z) -> F(*(x, x), s(half(x'')), z)
F(0, s(y), z) -> F(0, half(s(y)), z)

Rules:

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Strategy:

innermost

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

F(s(y''), s(y), z) -> F(+(*(s(y''), y''), s(y'')), half(s(y)), z)

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

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Used ordering:
Polynomial Order with Interpretation:

POL( F(x1, ..., x3) ) = x1

POL( s(x1) ) = 1

POL( +(x1, x2) ) = 0

POL( 0 ) = 0

POL( *(x1, x2) ) = 0

POL( half(x1) ) = 1

This results in one new DP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Neg POLO`
`             ...`
`               →DP Problem 13`
`                 ↳Negative Polynomial Order`

Dependency Pairs:

F(x, s(s(x'')), z) -> F(*(x, x), s(half(x'')), z)
F(0, s(y), z) -> F(0, half(s(y)), z)

Rules:

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Strategy:

innermost

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

F(x, s(s(x'')), z) -> F(*(x, x), s(half(x'')), z)

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

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Used ordering:
Polynomial Order with Interpretation:

POL( F(x1, ..., x3) ) = x2

POL( s(x1) ) = x1 + 1

POL( half(x1) ) = x1

POL( 0 ) = 0

POL( *(x1, x2) ) = 0

POL( +(x1, x2) ) = 0

This results in one new DP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Neg POLO`
`             ...`
`               →DP Problem 14`
`                 ↳Usable Rules (Innermost)`

Dependency Pair:

F(0, s(y), z) -> F(0, half(s(y)), z)

Rules:

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
*(x, 0) -> 0
*(x, s(y)) -> +(*(x, y), x)

Strategy:

innermost

As we are in the innermost case, we can delete all 2 non-usable-rules.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Neg POLO`
`             ...`
`               →DP Problem 15`
`                 ↳Modular Removal of Rules`

Dependency Pair:

F(0, s(y), z) -> F(0, half(s(y)), z)

Rules:

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))

Strategy:

innermost

We have the following set of usable rules:

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
 POL(0) =  0 POL(s(x1)) =  1 + x1 POL(half(x1)) =  x1 POL(F(x1, x2, x3)) =  1 + x1 + x2 + x3

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

half(s(0)) -> 0
half(s(s(x))) -> s(half(x))

The result of this processor delivers one new DP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Neg POLO`
`             ...`
`               →DP Problem 16`
`                 ↳Modular Removal of Rules`

Dependency Pair:

F(0, s(y), z) -> F(0, half(s(y)), z)

Rule:

half(0) -> 0

Strategy:

innermost

We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
 POL(0) =  1 POL(s(x1)) =  x1 POL(half(x1)) =  x1 POL(F(x1, x2, x3)) =  x1 + x2 + x3

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

The result of this processor delivers one new DP problem.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳UsableRules`
`       →DP Problem 2`
`         ↳UsableRules`
`       →DP Problem 3`
`         ↳UsableRules`
`       →DP Problem 4`
`         ↳UsableRules`
`       →DP Problem 5`
`         ↳UsableRules`
`           →DP Problem 10`
`             ↳Neg POLO`
`             ...`
`               →DP Problem 17`
`                 ↳Dependency Graph`

Dependency Pair:

F(0, s(y), z) -> F(0, half(s(y)), z)

Rule:

none

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:08 minutes