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

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)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation


Dependency Pairs:

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(app(-, app(D, x)), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(app(*, x), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
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(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(+, x), y)) -> APP(app(+, app(D, x)), app(D, y))


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





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(+, x), y)) -> APP(app(+, app(D, x)), app(D, y))
10 new Dependency Pairs are created:

APP(D, app(app(+, t), y)) -> APP(app(+, 1), app(D, y))
APP(D, app(app(+, constant), y)) -> APP(app(+, 0), app(D, y))
APP(D, app(app(+, app(app(+, x''), y'')), y)) -> APP(app(+, app(app(+, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, app(app(*, x''), y'')), y)) -> APP(app(+, app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y'')))), app(D, y))
APP(D, app(app(+, app(app(-, x''), y'')), y)) -> APP(app(+, app(app(-, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, x), t)) -> APP(app(+, app(D, x)), 1)
APP(D, app(app(+, x), constant)) -> APP(app(+, app(D, x)), 0)
APP(D, app(app(+, x), app(app(+, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, x), app(app(*, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(+, x), app(app(-, x''), y''))) -> APP(app(+, app(D, x)), app(app(-, app(D, x'')), app(D, y'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Narrowing Transformation


Dependency Pairs:

APP(D, app(app(+, x), app(app(-, x''), y''))) -> APP(app(+, app(D, x)), app(app(-, app(D, x'')), app(D, y'')))
APP(D, app(app(+, x), app(app(*, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(+, x), app(app(+, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, app(app(-, x''), y'')), y)) -> APP(app(+, app(app(-, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, app(app(*, x''), y'')), y)) -> APP(app(+, app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y'')))), app(D, y))
APP(D, app(app(+, app(app(+, x''), y'')), y)) -> APP(app(+, app(app(+, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, constant), y)) -> APP(app(+, 0), app(D, y))
APP(D, app(app(+, t), y)) -> APP(app(+, 1), app(D, y))
APP(D, app(app(-, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(app(*, x), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, x)
APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
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(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(-, x), y)) -> APP(D, y)


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





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(*, x), y)) -> APP(app(*, y), app(D, x))
five new Dependency Pairs are created:

APP(D, app(app(*, t), y)) -> APP(app(*, y), 1)
APP(D, app(app(*, constant), y)) -> APP(app(*, y), 0)
APP(D, app(app(*, app(app(+, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(*, app(app(*, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(*, app(app(-, x''), y'')), y)) -> APP(app(*, y), app(app(-, app(D, x'')), app(D, y'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Narrowing Transformation


Dependency Pairs:

APP(D, app(app(*, app(app(-, x''), y'')), y)) -> APP(app(*, y), app(app(-, app(D, x'')), app(D, y'')))
APP(D, app(app(*, app(app(*, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(*, app(app(+, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, x), app(app(*, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(+, x), app(app(+, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, app(app(-, x''), y'')), y)) -> APP(app(+, app(app(-, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, app(app(*, x''), y'')), y)) -> APP(app(+, app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y'')))), app(D, y))
APP(D, app(app(+, app(app(+, x''), y'')), y)) -> APP(app(+, app(app(+, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, constant), y)) -> APP(app(+, 0), app(D, y))
APP(D, app(app(+, t), y)) -> APP(app(+, 1), app(D, y))
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(app(-, app(D, x)), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(app(*, x), app(D, y))
APP(D, app(app(*, x), y)) -> APP(D, x)
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(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(+, x), app(app(-, x''), y''))) -> APP(app(+, app(D, x)), app(app(-, app(D, x'')), app(D, y'')))


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





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(*, x), y)) -> APP(app(*, x), app(D, y))
five new Dependency Pairs are created:

APP(D, app(app(*, x), t)) -> APP(app(*, x), 1)
APP(D, app(app(*, x), constant)) -> APP(app(*, x), 0)
APP(D, app(app(*, x), app(app(+, x''), y''))) -> APP(app(*, x), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(*, x), app(app(*, x''), y''))) -> APP(app(*, x), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(*, x), app(app(-, x''), y''))) -> APP(app(*, x), app(app(-, app(D, x'')), app(D, y'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 4
                 ↳Narrowing Transformation


Dependency Pairs:

APP(D, app(app(*, x), app(app(-, x''), y''))) -> APP(app(*, x), app(app(-, app(D, x'')), app(D, y'')))
APP(D, app(app(*, x), app(app(*, x''), y''))) -> APP(app(*, x), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(*, x), app(app(+, x''), y''))) -> APP(app(*, x), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(*, app(app(*, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(*, app(app(+, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, x), app(app(-, x''), y''))) -> APP(app(+, app(D, x)), app(app(-, app(D, x'')), app(D, y'')))
APP(D, app(app(+, x), app(app(*, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(+, x), app(app(+, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, app(app(-, x''), y'')), y)) -> APP(app(+, app(app(-, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, app(app(*, x''), y'')), y)) -> APP(app(+, app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y'')))), app(D, y))
APP(D, app(app(+, app(app(+, x''), y'')), y)) -> APP(app(+, app(app(+, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, constant), y)) -> APP(app(+, 0), app(D, y))
APP(D, app(app(+, t), y)) -> APP(app(+, 1), app(D, y))
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(app(-, app(D, x)), app(D, y))
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(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(*, app(app(-, x''), y'')), y)) -> APP(app(*, y), app(app(-, app(D, x'')), app(D, y'')))


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





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP(D, app(app(-, x), y)) -> APP(app(-, app(D, x)), app(D, y))
10 new Dependency Pairs are created:

APP(D, app(app(-, t), y)) -> APP(app(-, 1), app(D, y))
APP(D, app(app(-, constant), y)) -> APP(app(-, 0), app(D, y))
APP(D, app(app(-, app(app(+, x''), y'')), y)) -> APP(app(-, app(app(+, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(-, app(app(*, x''), y'')), y)) -> APP(app(-, app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y'')))), app(D, y))
APP(D, app(app(-, app(app(-, x''), y'')), y)) -> APP(app(-, app(app(-, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(-, x), t)) -> APP(app(-, app(D, x)), 1)
APP(D, app(app(-, x), constant)) -> APP(app(-, app(D, x)), 0)
APP(D, app(app(-, x), app(app(+, x''), y''))) -> APP(app(-, app(D, x)), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(-, x), app(app(*, x''), y''))) -> APP(app(-, app(D, x)), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(-, x), app(app(-, x''), y''))) -> APP(app(-, app(D, x)), app(app(-, app(D, x'')), app(D, y'')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 5
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

APP(D, app(app(-, x), app(app(-, x''), y''))) -> APP(app(-, app(D, x)), app(app(-, app(D, x'')), app(D, y'')))
APP(D, app(app(-, x), app(app(*, x''), y''))) -> APP(app(-, app(D, x)), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(-, x), app(app(+, x''), y''))) -> APP(app(-, app(D, x)), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(-, app(app(-, x''), y'')), y)) -> APP(app(-, app(app(-, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(-, app(app(*, x''), y'')), y)) -> APP(app(-, app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y'')))), app(D, y))
APP(D, app(app(-, app(app(+, x''), y'')), y)) -> APP(app(-, app(app(+, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(-, constant), y)) -> APP(app(-, 0), app(D, y))
APP(D, app(app(-, t), y)) -> APP(app(-, 1), app(D, y))
APP(D, app(app(*, x), app(app(*, x''), y''))) -> APP(app(*, x), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(*, x), app(app(+, x''), y''))) -> APP(app(*, x), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(*, app(app(-, x''), y'')), y)) -> APP(app(*, y), app(app(-, app(D, x'')), app(D, y'')))
APP(D, app(app(*, app(app(*, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(*, app(app(+, x''), y'')), y)) -> APP(app(*, y), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, x), app(app(-, x''), y''))) -> APP(app(+, app(D, x)), app(app(-, app(D, x'')), app(D, y'')))
APP(D, app(app(+, x), app(app(*, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y''))))
APP(D, app(app(+, x), app(app(+, x''), y''))) -> APP(app(+, app(D, x)), app(app(+, app(D, x'')), app(D, y'')))
APP(D, app(app(+, app(app(-, x''), y'')), y)) -> APP(app(+, app(app(-, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, app(app(*, x''), y'')), y)) -> APP(app(+, app(app(+, app(app(*, y''), app(D, x''))), app(app(*, x''), app(D, y'')))), app(D, y))
APP(D, app(app(+, app(app(+, x''), y'')), y)) -> APP(app(+, app(app(+, app(D, x'')), app(D, y''))), app(D, y))
APP(D, app(app(+, constant), y)) -> APP(app(+, 0), app(D, y))
APP(D, app(app(+, t), y)) -> APP(app(+, 1), app(D, y))
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(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)
APP(D, app(app(*, x), app(app(-, x''), y''))) -> APP(app(*, x), app(app(-, app(D, x'')), app(D, y'')))


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




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