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
Polynomial Ordering

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

The following dependency pairs can be strictly oriented:

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

Additionally, the following usable rules using the Ce-refinement can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(t) =  0 POL(0) =  0 POL(1) =  0 POL(constant) =  0 POL(*) =  0 POL(D) =  1 POL(-) =  0 POL(app(x1, x2)) =  0 POL(+) =  0 POL(APP(x1, x2)) =  x1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polynomial Ordering

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

The following dependency pairs can be strictly oriented:

APP(D, app(app(-, x), y)) -> APP(D, y)
APP(D, app(app(-, x), y)) -> APP(D, x)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(*) =  0 POL(D) =  0 POL(-) =  1 POL(APP(x1, x2)) =  1 + x2 POL(app(x1, x2)) =  x1 + x2 POL(+) =  0

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
...
→DP Problem 3
Polynomial Ordering

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

The following dependency pairs can be strictly oriented:

APP(D, app(app(*, x), y)) -> APP(D, y)
APP(D, app(app(*, x), y)) -> APP(D, x)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(*) =  1 POL(D) =  0 POL(APP(x1, x2)) =  1 + x2 POL(app(x1, x2)) =  x1 + x2 POL(+) =  0

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
...
→DP Problem 4
Polynomial Ordering

Dependency Pairs:

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

The following dependency pairs can be strictly oriented:

APP(D, app(app(+, x), y)) -> APP(D, y)
APP(D, app(app(+, x), y)) -> APP(D, x)

There are no usable rules using the Ce-refinement that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(D) =  0 POL(APP(x1, x2)) =  1 + x2 POL(app(x1, x2)) =  x1 + x2 POL(+) =  1

resulting in one new DP problem.

R
DPs
→DP Problem 1
Polo
→DP Problem 2
Polo
...
→DP Problem 5
Dependency Graph

Dependency Pair:

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

Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:00 minutes