The TRS could be proven terminating. The proof took 16 ms.
Problem 1 was processed with processor SubtermCriterion (1ms).
| g#(s(x)) | → | f#(x) | f#(s(x)) | → | g#(x) |
| g(s(x)) | → | f(x) | f(0) | → | s(0) | |
| f(s(x)) | → | s(s(g(x))) | g(0) | → | 0 |
Termination of terms over the following signature is verified: f, g, 0, s
The following projection was used:
Thus, the following dependency pairs are removed:
| g#(s(x)) | → | f#(x) | f#(s(x)) | → | g#(x) |