Term Rewriting System R:
[x, y]
minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))

Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

MINUS(+(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(y)
F(minus(x)) -> MINUS(minus(minus(f(x))))
F(minus(x)) -> MINUS(minus(f(x)))
F(minus(x)) -> MINUS(f(x))
F(minus(x)) -> F(x)

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:

MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(minus(minus(x)))

Rules:

minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))

• Dependency Pair:

F(minus(x)) -> F(x)

Rules:

minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))

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

The following remains to be proven:
• Dependency Pairs:

MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(minus(minus(x)))

Rules:

minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))

• Dependency Pair:

F(minus(x)) -> F(x)

Rules:

minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))

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