Term Rewriting System R:
[x, y]
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 Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Usable Rules (Innermost)


Dependency Pairs:

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)


Rules:


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


Strategy:

innermost




As we are in the innermost case, we can delete all 9 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 2
             ↳A-Transformation


Dependency Pairs:

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)


Rule:

none


Strategy:

innermost




We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 2
             ↳ATrans
             ...
               →DP Problem 3
                 ↳Size-Change Principle


Dependency Pairs:

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)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. D'(pow(x, y)) -> D'(y)
  2. D'(pow(x, y)) -> D'(x)
  3. D'(ln(x)) -> D'(x)
  4. D'(div(x, y)) -> D'(y)
  5. D'(div(x, y)) -> D'(x)
  6. D'(minus(x)) -> D'(x)
  7. D'(-(x, y)) -> D'(y)
  8. D'(-(x, y)) -> D'(x)
  9. D'(*(x, y)) -> D'(y)
  10. D'(*(x, y)) -> D'(x)
  11. D'(+(x, y)) -> D'(y)
  12. D'(+(x, y)) -> D'(x)
and get the following Size-Change Graph(s):
{1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12} , {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12}
1>1

which lead(s) to this/these maximal multigraph(s):
{1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12} , {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
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)

We obtain no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:03 minutes