TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60237 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (62ms).
| – Problem 2 was processed with processor BackwardInstantiation (5ms).
| | – Problem 6 remains open; application of the following processors failed [ForwardInstantiation (3ms), Propagation (1ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (3ms), Propagation (1ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
| – Problem 4 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (0ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| loop#(x, c, y) | → | if#(lt(x, c), x, c, y) | | if#(false, x, c, y) | → | loop#(x, s(c), times(y, s(c))) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | times(0, y) | → | 0 |
| times(s(x), y) | → | plus(y, times(x, y)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | fac(x) | → | loop(x, s(0), s(0)) |
| loop(x, c, y) | → | if(lt(x, c), x, c, y) | | if(false, x, c, y) | → | loop(x, s(c), times(y, s(c))) |
| if(true, x, c, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, if, fac, loop, false, true, lt
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | plus#(y, times(x, y)) | | fac#(x) | → | loop#(x, s(0), s(0)) |
| times#(s(x), y) | → | times#(x, y) | | plus#(s(x), y) | → | plus#(x, y) |
| loop#(x, c, y) | → | lt#(x, c) | | loop#(x, c, y) | → | if#(lt(x, c), x, c, y) |
| if#(false, x, c, y) | → | loop#(x, s(c), times(y, s(c))) | | lt#(s(x), s(y)) | → | lt#(x, y) |
| if#(false, x, c, y) | → | times#(y, s(c)) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | times(0, y) | → | 0 |
| times(s(x), y) | → | plus(y, times(x, y)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | fac(x) | → | loop(x, s(0), s(0)) |
| loop(x, c, y) | → | if(lt(x, c), x, c, y) | | if(false, x, c, y) | → | loop(x, s(c), times(y, s(c))) |
| if(true, x, c, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, if, fac, loop, true, false, lt
Strategy
The following SCCs where found
| times#(s(x), y) → times#(x, y) |
| if#(false, x, c, y) → loop#(x, s(c), times(y, s(c))) | loop#(x, c, y) → if#(lt(x, c), x, c, y) |
| plus#(s(x), y) → plus#(x, y) |
| lt#(s(x), s(y)) → lt#(x, y) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, x, c, y) | → | loop#(x, s(c), times(y, s(c))) | | loop#(x, c, y) | → | if#(lt(x, c), x, c, y) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | times(0, y) | → | 0 |
| times(s(x), y) | → | plus(y, times(x, y)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | fac(x) | → | loop(x, s(0), s(0)) |
| loop(x, c, y) | → | if(lt(x, c), x, c, y) | | if(false, x, c, y) | → | loop(x, s(c), times(y, s(c))) |
| if(true, x, c, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, if, fac, loop, true, false, lt
Strategy
Instantiation
For all potential predecessors l → r of the rule loop
#(
x,
c,
y) → if
#(lt(
x,
c),
x,
c,
y) on dependency pair chains it holds that:
- loop#(x, c, y) matches r,
- all variables of loop#(x, c, y) are embedded in constructor contexts, i.e., each subterm of loop#(x, c, y), containing a variable is rooted by a constructor symbol.
Thus, loop
#(
x,
c,
y) → if
#(lt(
x,
c),
x,
c,
y) is replaced by instances determined through the above matching. These instances are:
| loop#(_x, s(_c), times(_y, s(_c))) → if#(lt(_x, s(_c)), _x, s(_c), times(_y, s(_c))) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| times#(s(x), y) | → | times#(x, y) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | times(0, y) | → | 0 |
| times(s(x), y) | → | plus(y, times(x, y)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | fac(x) | → | loop(x, s(0), s(0)) |
| loop(x, c, y) | → | if(lt(x, c), x, c, y) | | if(false, x, c, y) | → | loop(x, s(c), times(y, s(c))) |
| if(true, x, c, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, if, fac, loop, true, false, lt
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| times#(s(x), y) | → | times#(x, y) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | times(0, y) | → | 0 |
| times(s(x), y) | → | plus(y, times(x, y)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | fac(x) | → | loop(x, s(0), s(0)) |
| loop(x, c, y) | → | if(lt(x, c), x, c, y) | | if(false, x, c, y) | → | loop(x, s(c), times(y, s(c))) |
| if(true, x, c, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, if, fac, loop, true, false, lt
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| plus#(s(x), y) | → | plus#(x, y) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| lt#(s(x), s(y)) | → | lt#(x, y) |
Rewrite Rules
| lt(0, s(x)) | → | true | | lt(x, 0) | → | false |
| lt(s(x), s(y)) | → | lt(x, y) | | times(0, y) | → | 0 |
| times(s(x), y) | → | plus(y, times(x, y)) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | fac(x) | → | loop(x, s(0), s(0)) |
| loop(x, c, y) | → | if(lt(x, c), x, c, y) | | if(false, x, c, y) | → | loop(x, s(c), times(y, s(c))) |
| if(true, x, c, y) | → | y |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, times, if, fac, loop, true, false, lt
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| lt#(s(x), s(y)) | → | lt#(x, y) |