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