Termination Proof using AProVE

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))

Termination of R to be shown.

     ↳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.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

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))
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))
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))
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))
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))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

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))
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))
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))
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))
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))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

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))
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))
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))
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))
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))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

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))
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))
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))
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))
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))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

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))
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))
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))
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))
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))

Termination of R could not be shown.
Duration:
0:00 minutes