Termination Proof using AProVE

Term Rewriting System R:
[z, x, y]
app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

APP(app(h, z), app(e, x)) -> APP(app(h, app(c, z)), app(app(d, z), x))
APP(app(h, z), app(e, x)) -> APP(h, app(c, z))
APP(app(h, z), app(e, x)) -> APP(c, z)
APP(app(h, z), app(e, x)) -> APP(app(d, z), x)
APP(app(h, z), app(e, x)) -> APP(d, z)
APP(app(d, z), app(app(g, 0), 0)) -> APP(e, 0)
APP(app(d, z), app(app(g, x), y)) -> APP(app(g, app(e, x)), app(app(d, z), y))
APP(app(d, z), app(app(g, x), y)) -> APP(g, app(e, x))
APP(app(d, z), app(app(g, x), y)) -> APP(e, x)
APP(app(d, z), app(app(g, x), y)) -> APP(app(d, z), y)
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(g, app(app(d, app(c, z)), app(app(g, x), y)))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, app(c, z)), app(app(g, x), y))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, z), app(app(g, x), y))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(d, z)
APP(app(g, app(e, x)), app(e, y)) -> APP(e, app(app(g, x), y))
APP(app(g, app(e, x)), app(e, y)) -> APP(app(g, x), y)
APP(app(g, app(e, x)), app(e, y)) -> APP(g, x)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

Dependency Pairs:

APP(app(g, app(e, x)), app(e, y)) -> APP(app(g, x), y)
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, z), app(app(g, x), y))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, app(c, z)), app(app(g, x), y))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
APP(app(d, z), app(app(g, x), y)) -> APP(app(d, z), y)
APP(app(d, z), app(app(g, x), y)) -> APP(app(g, app(e, x)), app(app(d, z), y))
APP(app(h, z), app(e, x)) -> APP(app(d, z), x)
APP(app(h, z), app(e, x)) -> APP(app(h, app(c, z)), app(app(d, z), x))

Rules:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
APP(app(d, z), app(app(g, x), y)) -> APP(app(g, app(e, x)), app(app(d, z), y))

The following usable rules for innermost can be oriented:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

{d, h} > g > e

resulting in one new DP problem.
Used Argument Filtering System:

APP(x₁, x₂) -> x₁
app(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 2

             ↳Dependency Graph

Dependency Pairs:

Rules:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 2 DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 5

                 ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, z), app(app(g, x), y))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, app(c, z)), app(app(g, x), y))
APP(app(d, z), app(app(g, x), y)) -> APP(app(d, z), y)

Rules:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Strategy:
innermost
Dependency Pairs:
APP(app(h, z), app(e, x)) -> APP(app(h, app(c, z)), app(app(d, z), x))
APP(app(g, app(e, x)), app(e, y)) -> APP(app(g, x), y)

Rules:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Strategy:
innermost

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 4

                 ↳Argument Filtering and Ordering

Dependency Pairs:

APP(app(h, z), app(e, x)) -> APP(app(d, z), x)
APP(app(h, z), app(e, x)) -> APP(app(h, app(c, z)), app(app(d, z), x))
APP(app(g, app(e, x)), app(e, y)) -> APP(app(g, x), y)

Rules:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Strategy:

innermost

The following dependency pair can be strictly oriented:

APP(app(h, z), app(e, x)) -> APP(app(d, z), x)

The following usable rules for innermost can be oriented:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

h > d > g > e

resulting in one new DP problem.
Used Argument Filtering System:

APP(x₁, x₂) -> x₁
app(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 2

             ↳DGraph

...

               →DP Problem 5

                 ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, z), app(app(g, x), y))
APP(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> APP(app(d, app(c, z)), app(app(g, x), y))
APP(app(d, z), app(app(g, x), y)) -> APP(app(d, z), y)

Rules:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Strategy:
innermost
Dependency Pairs:
APP(app(h, z), app(e, x)) -> APP(app(h, app(c, z)), app(app(d, z), x))
APP(app(g, app(e, x)), app(e, y)) -> APP(app(g, x), y)

Rules:

app(app(h, z), app(e, x)) -> app(app(h, app(c, z)), app(app(d, z), x))
app(app(d, z), app(app(g, 0), 0)) -> app(e, 0)
app(app(d, z), app(app(g, x), y)) -> app(app(g, app(e, x)), app(app(d, z), y))
app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) -> app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) -> app(e, app(app(g, x), y))

Strategy:
innermost

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