YES
The TRS could be proven terminating. The proof took 50 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (24ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (3ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| fac#(s(x)) | → | fac#(x) | | floop#(s(x), y) | → | floop#(x, *(s(x), y)) |
| fac#(s(x)) | → | *#(s(x), fac(x)) | | *#(x, s(y)) | → | *#(x, y) |
| +#(x, s(y)) | → | +#(x, y) | | *#(x, s(y)) | → | +#(*(x, y), x) |
| fac#(0) | → | 1# | | floop#(s(x), y) | → | *#(s(x), y) |
Rewrite Rules
| fac(0) | → | 1 | | fac(s(x)) | → | *(s(x), fac(x)) |
| floop(0, y) | → | y | | floop(s(x), y) | → | floop(x, *(s(x), y)) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| +(x, 0) | → | x | | +(x, s(y)) | → | s(+(x, y)) |
| 1 | → | s(0) | | fac(0) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: 1, floop, 0, s, fac, *, +
Strategy
The following SCCs where found
| floop#(s(x), y) → floop#(x, *(s(x), y)) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| fac(0) | → | 1 | | fac(s(x)) | → | *(s(x), fac(x)) |
| floop(0, y) | → | y | | floop(s(x), y) | → | floop(x, *(s(x), y)) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| +(x, 0) | → | x | | +(x, s(y)) | → | s(+(x, y)) |
| 1 | → | s(0) | | fac(0) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: 1, floop, 0, s, fac, *, +
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| fac(0) | → | 1 | | fac(s(x)) | → | *(s(x), fac(x)) |
| floop(0, y) | → | y | | floop(s(x), y) | → | floop(x, *(s(x), y)) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| +(x, 0) | → | x | | +(x, s(y)) | → | s(+(x, y)) |
| 1 | → | s(0) | | fac(0) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: 1, floop, 0, s, fac, *, +
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| fac(0) | → | 1 | | fac(s(x)) | → | *(s(x), fac(x)) |
| floop(0, y) | → | y | | floop(s(x), y) | → | floop(x, *(s(x), y)) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| +(x, 0) | → | x | | +(x, s(y)) | → | s(+(x, y)) |
| 1 | → | s(0) | | fac(0) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: 1, floop, 0, s, fac, *, +
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| floop#(s(x), y) | → | floop#(x, *(s(x), y)) |
Rewrite Rules
| fac(0) | → | 1 | | fac(s(x)) | → | *(s(x), fac(x)) |
| floop(0, y) | → | y | | floop(s(x), y) | → | floop(x, *(s(x), y)) |
| *(x, 0) | → | 0 | | *(x, s(y)) | → | +(*(x, y), x) |
| +(x, 0) | → | x | | +(x, s(y)) | → | s(+(x, y)) |
| 1 | → | s(0) | | fac(0) | → | s(0) |
Original Signature
Termination of terms over the following signature is verified: 1, floop, 0, s, fac, *, +
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| floop#(s(x), y) | → | floop#(x, *(s(x), y)) |