YES
The TRS could be proven terminating. The proof took 38 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (16ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| | – Problem 3 was processed with processor DependencyGraph (4ms).
| | | – Problem 4 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| ack_in#(s(m), 0) | → | u11#(ack_in(m, s(0))) | | u21#(ack_out(n), m) | → | ack_in#(m, n) |
| ack_in#(s(m), s(n)) | → | ack_in#(s(m), n) | | ack_in#(s(m), 0) | → | ack_in#(m, s(0)) |
| ack_in#(s(m), s(n)) | → | u21#(ack_in(s(m), n), m) | | u21#(ack_out(n), m) | → | u22#(ack_in(m, n)) |
Rewrite Rules
| ack_in(0, n) | → | ack_out(s(n)) | | ack_in(s(m), 0) | → | u11(ack_in(m, s(0))) |
| u11(ack_out(n)) | → | ack_out(n) | | ack_in(s(m), s(n)) | → | u21(ack_in(s(m), n), m) |
| u21(ack_out(n), m) | → | u22(ack_in(m, n)) | | u22(ack_out(n)) | → | ack_out(n) |
Original Signature
Termination of terms over the following signature is verified: u11, u22, 0, u21, s, ack_in, ack_out
Strategy
The following SCCs where found
| u21#(ack_out(n), m) → ack_in#(m, n) | ack_in#(s(m), s(n)) → ack_in#(s(m), n) |
| ack_in#(s(m), 0) → ack_in#(m, s(0)) | ack_in#(s(m), s(n)) → u21#(ack_in(s(m), n), m) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| u21#(ack_out(n), m) | → | ack_in#(m, n) | | ack_in#(s(m), s(n)) | → | ack_in#(s(m), n) |
| ack_in#(s(m), 0) | → | ack_in#(m, s(0)) | | ack_in#(s(m), s(n)) | → | u21#(ack_in(s(m), n), m) |
Rewrite Rules
| ack_in(0, n) | → | ack_out(s(n)) | | ack_in(s(m), 0) | → | u11(ack_in(m, s(0))) |
| u11(ack_out(n)) | → | ack_out(n) | | ack_in(s(m), s(n)) | → | u21(ack_in(s(m), n), m) |
| u21(ack_out(n), m) | → | u22(ack_in(m, n)) | | u22(ack_out(n)) | → | ack_out(n) |
Original Signature
Termination of terms over the following signature is verified: u11, u22, 0, u21, s, ack_in, ack_out
Strategy
Projection
The following projection was used:
- π (u21#): 2
- π (ack_in#): 1
Thus, the following dependency pairs are removed:
| ack_in#(s(m), 0) | → | ack_in#(m, s(0)) | | ack_in#(s(m), s(n)) | → | u21#(ack_in(s(m), n), m) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| u21#(ack_out(n), m) | → | ack_in#(m, n) | | ack_in#(s(m), s(n)) | → | ack_in#(s(m), n) |
Rewrite Rules
| ack_in(0, n) | → | ack_out(s(n)) | | ack_in(s(m), 0) | → | u11(ack_in(m, s(0))) |
| u11(ack_out(n)) | → | ack_out(n) | | ack_in(s(m), s(n)) | → | u21(ack_in(s(m), n), m) |
| u21(ack_out(n), m) | → | u22(ack_in(m, n)) | | u22(ack_out(n)) | → | ack_out(n) |
Original Signature
Termination of terms over the following signature is verified: u11, u22, u21, 0, s, ack_in, ack_out
Strategy
The following SCCs where found
| ack_in#(s(m), s(n)) → ack_in#(s(m), n) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| ack_in#(s(m), s(n)) | → | ack_in#(s(m), n) |
Rewrite Rules
| ack_in(0, n) | → | ack_out(s(n)) | | ack_in(s(m), 0) | → | u11(ack_in(m, s(0))) |
| u11(ack_out(n)) | → | ack_out(n) | | ack_in(s(m), s(n)) | → | u21(ack_in(s(m), n), m) |
| u21(ack_out(n), m) | → | u22(ack_in(m, n)) | | u22(ack_out(n)) | → | ack_out(n) |
Original Signature
Termination of terms over the following signature is verified: u11, u22, u21, 0, s, ack_in, ack_out
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| ack_in#(s(m), s(n)) | → | ack_in#(s(m), n) |