R
↳Overlay and local confluence Check
R
↳OC
→TRS2
↳Dependency Pair Analysis
APP(D, app(app(+, x), y)) -> APP(app(+, app(D, x)), app(D, y))
APP(D, app(app(+, x), y)) -> APP(+, app(D, x))
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
APP(D, app(app(*, x), y)) -> APP(+, app(app(*, y), app(D, x)))
APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
APP(D, app(app(*, x), y)) -> APP(*, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(app(*, x), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
APP(D, app(app(-, x), y)) -> APP(-, app(D, x))
APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(minus, x)) -> APP(minus, app(D, x))
APP(D, app(minus, x)) -> APP(D, x)
APP(D, app(app(div, x), y)) -> APP(app(-, app(app(div, app(D, x)), y)), app(app(div, app(app(*, x), app(D, y))), app(app(pow, y), 2)))
APP(D, app(app(div, x), y)) -> APP(-, app(app(div, app(D, x)), y))
APP(D, app(app(div, x), y)) -> APP(app(div, app(D, x)), y)
APP(D, app(app(div, x), y)) -> APP(div, app(D, x))
APP(D, app(app(div, x), y)) -> APP(D, x)
APP(D, app(app(div, x), y)) -> APP(app(div, app(app(*, x), app(D, y))), app(app(pow, y), 2))
APP(D, app(app(div, x), y)) -> APP(div, app(app(*, x), app(D, y)))
APP(D, app(app(div, x), y)) -> APP(app(*, x), app(D, y))
APP(D, app(app(div, x), y)) -> APP(*, x)
APP(D, app(app(div, x), y)) -> APP(D, y)
APP(D, app(app(div, x), y)) -> APP(app(pow, y), 2)
APP(D, app(app(div, x), y)) -> APP(pow, y)
APP(D, app(ln, x)) -> APP(app(div, app(D, x)), x)
APP(D, app(ln, x)) -> APP(div, app(D, x))
APP(D, app(ln, x)) -> APP(D, x)
APP(D, app(app(pow, x), y)) -> APP(app(+, app(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x))), app(app(*, app(app(*, app(app(pow, x), y)), app(ln, x))), app(D, y)))
APP(D, app(app(pow, x), y)) -> APP(+, app(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x)))
APP(D, app(app(pow, x), y)) -> APP(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x))
APP(D, app(app(pow, x), y)) -> APP(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1))))
APP(D, app(app(pow, x), y)) -> APP(app(*, y), app(app(pow, x), app(app(-, y), 1)))
APP(D, app(app(pow, x), y)) -> APP(*, y)
APP(D, app(app(pow, x), y)) -> APP(app(pow, x), app(app(-, y), 1))
APP(D, app(app(pow, x), y)) -> APP(app(-, y), 1)
APP(D, app(app(pow, x), y)) -> APP(-, y)
APP(D, app(app(pow, x), y)) -> APP(D, x)
APP(D, app(app(pow, x), y)) -> APP(app(*, app(app(*, app(app(pow, x), y)), app(ln, x))), app(D, y))
APP(D, app(app(pow, x), y)) -> APP(*, app(app(*, app(app(pow, x), y)), app(ln, x)))
APP(D, app(app(pow, x), y)) -> APP(app(*, app(app(pow, x), y)), app(ln, x))
APP(D, app(app(pow, x), y)) -> APP(*, app(app(pow, x), y))
APP(D, app(app(pow, x), y)) -> APP(ln, x)
APP(D, app(app(pow, x), y)) -> APP(D, y)
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
APP(D, app(app(pow, x), y)) -> APP(D, y)
APP(D, app(app(pow, x), y)) -> APP(D, x)
APP(D, app(ln, x)) -> APP(D, x)
APP(D, app(app(div, x), y)) -> APP(D, y)
APP(D, app(app(div, x), y)) -> APP(D, x)
APP(D, app(minus, x)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
app(D, t) -> 1
app(D, constant) -> 0
app(D, app(app(+, x), y)) -> app(app(+, app(D, x)), app(D, y))
app(D, app(app(*, x), y)) -> app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) -> app(app(-, app(D, x)), app(D, y))
app(D, app(minus, x)) -> app(minus, app(D, x))
app(D, app(app(div, x), y)) -> app(app(-, app(app(div, app(D, x)), y)), app(app(div, app(app(*, x), app(D, y))), app(app(pow, y), 2)))
app(D, app(ln, x)) -> app(app(div, app(D, x)), x)
app(D, app(app(pow, x), y)) -> app(app(+, app(app(*, app(app(*, y), app(app(pow, x), app(app(-, y), 1)))), app(D, x))), app(app(*, app(app(*, app(app(pow, x), y)), app(ln, x))), app(D, y)))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 2
↳A-Transformation
APP(D, app(app(pow, x), y)) -> APP(D, y)
APP(D, app(app(pow, x), y)) -> APP(D, x)
APP(D, app(ln, x)) -> APP(D, x)
APP(D, app(app(div, x), y)) -> APP(D, y)
APP(D, app(app(div, x), y)) -> APP(D, x)
APP(D, app(minus, x)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
none
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 3
↳Size-Change Principle
D'(pow(x, y)) -> D'(y)
D'(pow(x, y)) -> D'(x)
D'(ln(x)) -> D'(x)
D'(div(x, y)) -> D'(y)
D'(div(x, y)) -> D'(x)
D'(minus(x)) -> D'(x)
D'(-(x, y)) -> D'(y)
D'(-(x, y)) -> D'(x)
D'(*(x, y)) -> D'(y)
D'(*(x, y)) -> D'(x)
D'(+(x, y)) -> D'(y)
D'(+(x, y)) -> D'(x)
none
innermost
|
|
trivial
pow(x1, x2) -> pow(x1, x2)
*(x1, x2) -> *(x1, x2)
minus(x1) -> minus(x1)
-(x1, x2) -> -(x1, x2)
+(x1, x2) -> +(x1, x2)
div(x1, x2) -> div(x1, x2)
ln(x1) -> ln(x1)