YES

The TRS could be proven terminating. The proof took 178 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (22ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (123ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 4 was processed with processor SubtermCriterion (0ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

plus#(x, s(s(y)))plus#(s(x), y)ack#(s(x), s(y))plus#(y, ack(s(x), y))
ack#(s(x), s(y))ack#(x, plus(y, ack(s(x), y)))ack#(s(x), s(y))ack#(s(x), y)
plus#(s(s(x)), y)plus#(x, s(y))ack#(s(x), 0)ack#(x, s(0))

Rewrite Rules

plus(s(s(x)), y)s(plus(x, s(y)))plus(x, s(s(y)))s(plus(s(x), y))
plus(s(0), y)s(y)plus(0, y)y
ack(0, y)s(y)ack(s(x), 0)ack(x, s(0))
ack(s(x), s(y))ack(x, plus(y, ack(s(x), y)))

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, ack

Strategy


The following SCCs where found

plus#(x, s(s(y))) → plus#(s(x), y)plus#(s(s(x)), y) → plus#(x, s(y))

ack#(s(x), s(y)) → ack#(x, plus(y, ack(s(x), y)))ack#(s(x), s(y)) → ack#(s(x), y)
ack#(s(x), 0) → ack#(x, s(0))

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

plus#(x, s(s(y)))plus#(s(x), y)plus#(s(s(x)), y)plus#(x, s(y))

Rewrite Rules

plus(s(s(x)), y)s(plus(x, s(y)))plus(x, s(s(y)))s(plus(s(x), y))
plus(s(0), y)s(y)plus(0, y)y
ack(0, y)s(y)ack(s(x), 0)ack(x, s(0))
ack(s(x), s(y))ack(x, plus(y, ack(s(x), y)))

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, ack

Strategy


Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

plus#(x, s(s(y)))plus#(s(x), y)plus#(s(s(x)), y)plus#(x, s(y))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

ack#(s(x), s(y))ack#(x, plus(y, ack(s(x), y)))ack#(s(x), s(y))ack#(s(x), y)
ack#(s(x), 0)ack#(x, s(0))

Rewrite Rules

plus(s(s(x)), y)s(plus(x, s(y)))plus(x, s(s(y)))s(plus(s(x), y))
plus(s(0), y)s(y)plus(0, y)y
ack(0, y)s(y)ack(s(x), 0)ack(x, s(0))
ack(s(x), s(y))ack(x, plus(y, ack(s(x), y)))

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, ack

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

ack#(s(x), s(y))ack#(x, plus(y, ack(s(x), y)))ack#(s(x), 0)ack#(x, s(0))

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

ack#(s(x), s(y))ack#(s(x), y)

Rewrite Rules

plus(s(s(x)), y)s(plus(x, s(y)))plus(x, s(s(y)))s(plus(s(x), y))
plus(s(0), y)s(y)plus(0, y)y
ack(0, y)s(y)ack(s(x), 0)ack(x, s(0))
ack(s(x), s(y))ack(x, plus(y, ack(s(x), y)))

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, ack

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

ack#(s(x), s(y))ack#(s(x), y)