Termination Proof using AProVE

Term Rewriting System R:
[x, y]
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

EVEN(s(s(x))) -> EVEN(x)
HALF(s(s(x))) -> HALF(x)
PLUS(s(x), y) -> PLUS(x, y)
TIMES(s(x), y) -> IF_TIMES(even(s(x)), s(x), y)
TIMES(s(x), y) -> EVEN(s(x))
IF_TIMES(true, s(x), y) -> PLUS(times(half(s(x)), y), times(half(s(x)), y))
IF_TIMES(true, s(x), y) -> TIMES(half(s(x)), y)
IF_TIMES(true, s(x), y) -> HALF(s(x))
IF_TIMES(false, s(x), y) -> PLUS(y, times(x, y))
IF_TIMES(false, s(x), y) -> TIMES(x, y)

Furthermore, R contains four 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)

The following remains to be proven:

Dependency Pair:
EVEN(s(s(x))) -> EVEN(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
HALF(s(s(x))) -> HALF(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
PLUS(s(x), y) -> PLUS(x, y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pairs:
IF_TIMES(false, s(x), y) -> TIMES(x, y)
IF_TIMES(true, s(x), y) -> TIMES(half(s(x)), y)
TIMES(s(x), y) -> IF_TIMES(even(s(x)), s(x), y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))

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

The following remains to be proven:

Dependency Pair:
EVEN(s(s(x))) -> EVEN(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
HALF(s(s(x))) -> HALF(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
PLUS(s(x), y) -> PLUS(x, y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pairs:
IF_TIMES(false, s(x), y) -> TIMES(x, y)
IF_TIMES(true, s(x), y) -> TIMES(half(s(x)), y)
TIMES(s(x), y) -> IF_TIMES(even(s(x)), s(x), y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))

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

The following remains to be proven:

Dependency Pair:
EVEN(s(s(x))) -> EVEN(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
HALF(s(s(x))) -> HALF(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
PLUS(s(x), y) -> PLUS(x, y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pairs:
IF_TIMES(false, s(x), y) -> TIMES(x, y)
IF_TIMES(true, s(x), y) -> TIMES(half(s(x)), y)
TIMES(s(x), y) -> IF_TIMES(even(s(x)), s(x), y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))

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

The following remains to be proven:

Dependency Pair:
EVEN(s(s(x))) -> EVEN(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
HALF(s(s(x))) -> HALF(x)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pair:
PLUS(s(x), y) -> PLUS(x, y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))
Dependency Pairs:
IF_TIMES(false, s(x), y) -> TIMES(x, y)
IF_TIMES(true, s(x), y) -> TIMES(half(s(x)), y)
TIMES(s(x), y) -> IF_TIMES(even(s(x)), s(x), y)

Rules:

even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> if_times(even(s(x)), s(x), y)
if_times(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
if_times(false, s(x), y) -> plus(y, times(x, y))

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