Term Rewriting System R:
[x, y]
double(0) -> 0
double(s(x)) -> s(s(double(x)))
double(x) -> +(x, x)
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(s(x), y) -> s(+(x, y))

Termination of R to be shown.

R
Dependency Pair Analysis

R contains the following Dependency Pairs:

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

Furthermore, R contains two SCCs.

R
DPs
→DP Problem 1
Remaining Obligation(s)
→DP Problem 2
Remaining Obligation(s)

The following remains to be proven:
• Dependency Pairs:

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

Rules:

double(0) -> 0
double(s(x)) -> s(s(double(x)))
double(x) -> +(x, x)
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(s(x), y) -> s(+(x, y))

• Dependency Pair:

DOUBLE(s(x)) -> DOUBLE(x)

Rules:

double(0) -> 0
double(s(x)) -> s(s(double(x)))
double(x) -> +(x, x)
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(s(x), y) -> s(+(x, y))

R
DPs
→DP Problem 1
Remaining Obligation(s)
→DP Problem 2
Remaining Obligation(s)

The following remains to be proven:
• Dependency Pairs:

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

Rules:

double(0) -> 0
double(s(x)) -> s(s(double(x)))
double(x) -> +(x, x)
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(s(x), y) -> s(+(x, y))

• Dependency Pair:

DOUBLE(s(x)) -> DOUBLE(x)

Rules:

double(0) -> 0
double(s(x)) -> s(s(double(x)))
double(x) -> +(x, x)
+(x, 0) -> x
+(x, s(y)) -> s(+(x, y))
+(s(x), y) -> s(+(x, y))

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