TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60000 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (59ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| – Problem 3 was processed with processor BackwardInstantiation (1ms).
| | – Problem 6 was processed with processor BackwardInstantiation (1ms).
| | | – Problem 7 was processed with processor Propagation (3ms).
| | | | – Problem 8 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (0ms)].
| – 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 3
Dependency Pairs
| if#(true, sum, z) | → | aver#(sum, s(z)) | | aver#(sum, z) | → | if#(gt(sum, double(z)), sum, z) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, true, false, gt, double, average
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| if#(true, sum, z) | → | aver#(sum, s(z)) | | average#(x, y) | → | aver#(plus(x, y), 0) |
| gt#(s(x), s(y)) | → | gt#(x, y) | | plus#(s(x), y) | → | plus#(x, y) |
| average#(x, y) | → | plus#(x, y) | | aver#(sum, z) | → | if#(gt(sum, double(z)), sum, z) |
| aver#(sum, z) | → | double#(z) | | double#(s(x)) | → | double#(x) |
| aver#(sum, z) | → | gt#(sum, double(z)) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, false, true, gt, double, average
Strategy
The following SCCs where found
| plus#(s(x), y) → plus#(x, y) |
| gt#(s(x), s(y)) → gt#(x, y) |
| double#(s(x)) → double#(x) |
| if#(true, sum, z) → aver#(sum, s(z)) | aver#(sum, z) → if#(gt(sum, double(z)), sum, z) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| gt#(s(x), s(y)) | → | gt#(x, y) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, false, true, gt, double, average
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| gt#(s(x), s(y)) | → | gt#(x, y) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(true, sum, z) | → | aver#(sum, s(z)) | | aver#(sum, z) | → | if#(gt(sum, double(z)), sum, z) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, false, true, gt, double, average
Strategy
Instantiation
For all potential predecessors l → r of the rule aver
#(
sum,
z) → if
#(gt(
sum, double(
z)),
sum,
z) on dependency pair chains it holds that:
- aver#(sum, z) matches r,
- all variables of aver#(sum, z) are embedded in constructor contexts, i.e., each subterm of aver#(sum, z), containing a variable is rooted by a constructor symbol.
Thus, aver
#(
sum,
z) → if
#(gt(
sum, double(
z)),
sum,
z) is replaced by instances determined through the above matching. These instances are:
| aver#(_sum, s(_z)) → if#(gt(_sum, double(s(_z))), _sum, s(_z)) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| aver#(_sum, s(_z)) | → | if#(gt(_sum, double(s(_z))), _sum, s(_z)) | | if#(true, sum, z) | → | aver#(sum, s(z)) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, true, false, gt, double, average
Strategy
Instantiation
For all potential predecessors l → r of the rule aver
#(
_sum, s(
_z)) → if
#(gt(
_sum, double(s(
_z))),
_sum, s(
_z)) on dependency pair chains it holds that:
- aver#(_sum, s(_z)) matches r,
- all variables of aver#(_sum, s(_z)) are embedded in constructor contexts, i.e., each subterm of aver#(_sum, s(_z)), containing a variable is rooted by a constructor symbol.
Thus, aver
#(
_sum, s(
_z)) → if
#(gt(
_sum, double(s(
_z))),
_sum, s(
_z)) is replaced by instances determined through the above matching. These instances are:
| aver#(sum, s(z)) → if#(gt(sum, double(s(z))), sum, s(z)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| aver#(sum, s(z)) | → | if#(gt(sum, double(s(z))), sum, s(z)) | | if#(true, sum, z) | → | aver#(sum, s(z)) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, false, true, gt, double, average
Strategy
The dependency pairs if
#(true,
sum,
z) → aver
#(
sum, s(
z)) and aver
#(
sum, s(
z)) → if
#(gt(
sum, double(s(
z))),
sum, s(
z)) are consolidated into the rule if
#(true,
sum,
z) → if
#(gt(
sum, double(s(
z))),
sum, s(
z)) .
This is possible as
- all subterms of aver#(sum, s(z)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in aver#(sum, s(z)), but non-replacing in both if#(true, sum, z) and if#(gt(sum, double(s(z))), sum, s(z))
The dependency pairs if
#(true,
sum,
z) → aver
#(
sum, s(
z)) and aver
#(
sum, s(
z)) → if
#(gt(
sum, double(s(
z))),
sum, s(
z)) are consolidated into the rule if
#(true,
sum,
z) → if
#(gt(
sum, double(s(
z))),
sum, s(
z)) .
This is possible as
- all subterms of aver#(sum, s(z)) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in aver#(sum, s(z)), but non-replacing in both if#(true, sum, z) and if#(gt(sum, double(s(z))), sum, s(z))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| aver#(sum, s(z)) → if#(gt(sum, double(s(z))), sum, s(z)) | if#(true, sum, z) → if#(gt(sum, double(s(z))), sum, s(z)) |
| if#(true, sum, z) → aver#(sum, s(z)) | |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| plus#(s(x), y) | → | plus#(x, y) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, false, true, gt, double, average
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
| double#(s(x)) | → | double#(x) |
Rewrite Rules
| gt(0, y) | → | false | | gt(s(x), 0) | → | true |
| gt(s(x), s(y)) | → | gt(x, y) | | plus(0, y) | → | y |
| plus(s(x), y) | → | s(plus(x, y)) | | double(0) | → | 0 |
| double(s(x)) | → | s(s(double(x))) | | average(x, y) | → | aver(plus(x, y), 0) |
| aver(sum, z) | → | if(gt(sum, double(z)), sum, z) | | if(true, sum, z) | → | aver(sum, s(z)) |
| if(false, sum, z) | → | z |
Original Signature
Termination of terms over the following signature is verified: aver, plus, 0, s, if, false, true, gt, double, average
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| double#(s(x)) | → | double#(x) |