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 (75ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor BackwardInstantiation (5ms).
| | – Problem 5 was processed with processor ForwardInstantiation (5ms).
| | | – Problem 6 was processed with processor BackwardInstantiation (5ms).
| | | | – Problem 7 was processed with processor ForwardInstantiation (12ms).
| | | | | – Problem 8 was processed with processor BackwardInstantiation (9ms).
| | | | | | – Problem 9 was processed with processor Propagation (8ms).
| | | | | | | – Problem 10 remains open; application of the following processors failed [].
| – Problem 4 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 3
Dependency Pairs
| sumList#(xs, y) | → | if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) |
| if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, cons, nil, isZero
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| sumList#(xs, y) | → | head#(xs) | | sumList#(xs, y) | → | p#(head(xs)) |
| sum#(xs) | → | sumList#(xs, 0) | | sumList#(xs, y) | → | inc#(y) |
| sumList#(xs, y) | → | if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | sumList#(xs, y) | → | tail#(xs) |
| inc#(s(x)) | → | inc#(x) | | if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) |
| if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) | | p#(s(s(x))) | → | p#(s(x)) |
| sumList#(xs, y) | → | isZero#(head(xs)) | | sumList#(xs, y) | → | isEmpty#(xs) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, isZero, nil, cons
Strategy
The following SCCs where found
| sumList#(xs, y) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | if#(false, true, y, xs, ys, x) → sumList#(xs, y) |
| if#(false, false, y, xs, ys, x) → sumList#(ys, x) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, isZero, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| sumList#(xs, y) | → | if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) |
| if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, isZero, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule sumList
#(
xs,
y) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) on dependency pair chains it holds that:
- sumList#(xs, y) matches r,
- all variables of sumList#(xs, y) are embedded in constructor contexts, i.e., each subterm of sumList#(xs, y), containing a variable is rooted by a constructor symbol.
Thus, sumList
#(
xs,
y) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) is replaced by instances determined through the above matching. These instances are:
| sumList#(ys, x) → if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) | sumList#(_xs, _y) → if#(isEmpty(_xs), isZero(head(_xs)), _y, tail(_xs), cons(p(head(_xs)), tail(_xs)), inc(_y)) |
Problem 5: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) | | if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) |
| sumList#(ys, x) | → | if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) | | sumList#(_xs, _y) | → | if#(isEmpty(_xs), isZero(head(_xs)), _y, tail(_xs), cons(p(head(_xs)), tail(_xs)), inc(_y)) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, cons, nil, isZero
Strategy
Instantiation
For all potential successors l → r of the rule if
#(false, true,
y,
xs,
ys,
x) → sumList
#(
xs,
y) on dependency pair chains it holds that:
- sumList#(xs, y) matches l,
- all variables of sumList#(xs, y) are embedded in constructor contexts, i.e., each subterm of sumList#(xs, y) containing a variable is rooted by a constructor symbol.
Thus, if
#(false, true,
y,
xs,
ys,
x) → sumList
#(
xs,
y) is replaced by instances determined through the above matching. These instances are:
| if#(false, true, y, xs, xs, y) → sumList#(xs, y) | if#(false, true, y, xs, ys, x) → sumList#(xs, y) |
Instantiation
For all potential successors l → r of the rule if
#(false, false,
y,
xs,
ys,
x) → sumList
#(
ys,
x) on dependency pair chains it holds that:
- sumList#(ys, x) matches l,
- all variables of sumList#(ys, x) are embedded in constructor contexts, i.e., each subterm of sumList#(ys, x) containing a variable is rooted by a constructor symbol.
Thus, if
#(false, false,
y,
xs,
ys,
x) → sumList
#(
ys,
x) is replaced by instances determined through the above matching. These instances are:
| if#(false, false, y, xs, ys, x) → sumList#(ys, x) |
Problem 6: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| if#(false, true, y, xs, xs, y) | → | sumList#(xs, y) | | if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) |
| if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) | | sumList#(ys, x) | → | if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) |
| sumList#(_xs, _y) | → | if#(isEmpty(_xs), isZero(head(_xs)), _y, tail(_xs), cons(p(head(_xs)), tail(_xs)), inc(_y)) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, isZero, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule sumList
#(
ys,
x) → if
#(isEmpty(
ys), isZero(head(
ys)),
x, tail(
ys), cons(p(head(
ys)), tail(
ys)), inc(
x)) on dependency pair chains it holds that:
- sumList#(ys, x) matches r,
- all variables of sumList#(ys, x) are embedded in constructor contexts, i.e., each subterm of sumList#(ys, x), containing a variable is rooted by a constructor symbol.
Thus, sumList
#(
ys,
x) → if
#(isEmpty(
ys), isZero(head(
ys)),
x, tail(
ys), cons(p(head(
ys)), tail(
ys)), inc(
x)) is replaced by instances determined through the above matching. These instances are:
| sumList#(_ys, _x) → if#(isEmpty(_ys), isZero(head(_ys)), _x, tail(_ys), cons(p(head(_ys)), tail(_ys)), inc(_x)) | sumList#(xs, y) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) |
Instantiation
For all potential predecessors l → r of the rule sumList
#(
_xs,
_y) → if
#(isEmpty(
_xs), isZero(head(
_xs)),
_y, tail(
_xs), cons(p(head(
_xs)), tail(
_xs)), inc(
_y)) on dependency pair chains it holds that:
- sumList#(_xs, _y) matches r,
- all variables of sumList#(_xs, _y) are embedded in constructor contexts, i.e., each subterm of sumList#(_xs, _y), containing a variable is rooted by a constructor symbol.
Thus, sumList
#(
_xs,
_y) → if
#(isEmpty(
_xs), isZero(head(
_xs)),
_y, tail(
_xs), cons(p(head(
_xs)), tail(
_xs)), inc(
_y)) is replaced by instances determined through the above matching. These instances are:
| sumList#(xs, y) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | sumList#(ys, x) → if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) |
Problem 7: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| sumList#(_ys, _x) | → | if#(isEmpty(_ys), isZero(head(_ys)), _x, tail(_ys), cons(p(head(_ys)), tail(_ys)), inc(_x)) | | sumList#(xs, y) | → | if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) |
| if#(false, true, y, xs, xs, y) | → | sumList#(xs, y) | | if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) |
| if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) | | sumList#(ys, x) | → | if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, cons, nil, isZero
Strategy
Instantiation
For all potential successors l → r of the rule if
#(false, true,
y,
xs,
xs,
y) → sumList
#(
xs,
y) on dependency pair chains it holds that:
- sumList#(xs, y) matches l,
- all variables of sumList#(xs, y) are embedded in constructor contexts, i.e., each subterm of sumList#(xs, y) containing a variable is rooted by a constructor symbol.
Thus, if
#(false, true,
y,
xs,
xs,
y) → sumList
#(
xs,
y) is replaced by instances determined through the above matching. These instances are:
| if#(false, true, y, xs, xs, y) → sumList#(xs, y) |
Instantiation
For all potential successors l → r of the rule if
#(false, false,
y,
xs,
ys,
x) → sumList
#(
ys,
x) on dependency pair chains it holds that:
- sumList#(ys, x) matches l,
- all variables of sumList#(ys, x) are embedded in constructor contexts, i.e., each subterm of sumList#(ys, x) containing a variable is rooted by a constructor symbol.
Thus, if
#(false, false,
y,
xs,
ys,
x) → sumList
#(
ys,
x) is replaced by instances determined through the above matching. These instances are:
| if#(false, false, x, ys, ys, x) → sumList#(ys, x) | if#(false, false, y, xs, ys, x) → sumList#(ys, x) |
Instantiation
For all potential successors l → r of the rule if
#(false, true,
y,
xs,
ys,
x) → sumList
#(
xs,
y) on dependency pair chains it holds that:
- sumList#(xs, y) matches l,
- all variables of sumList#(xs, y) are embedded in constructor contexts, i.e., each subterm of sumList#(xs, y) containing a variable is rooted by a constructor symbol.
Thus, if
#(false, true,
y,
xs,
ys,
x) → sumList
#(
xs,
y) is replaced by instances determined through the above matching. These instances are:
| if#(false, true, y, xs, xs, y) → sumList#(xs, y) | if#(false, true, y, xs, ys, x) → sumList#(xs, y) |
Problem 8: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| sumList#(xs, y) | → | if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | sumList#(_ys, _x) | → | if#(isEmpty(_ys), isZero(head(_ys)), _x, tail(_ys), cons(p(head(_ys)), tail(_ys)), inc(_x)) |
| if#(false, true, y, xs, xs, y) | → | sumList#(xs, y) | | if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) |
| if#(false, false, x, ys, ys, x) | → | sumList#(ys, x) | | if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) |
| sumList#(ys, x) | → | if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, isZero, nil, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule sumList
#(
_ys,
_x) → if
#(isEmpty(
_ys), isZero(head(
_ys)),
_x, tail(
_ys), cons(p(head(
_ys)), tail(
_ys)), inc(
_x)) on dependency pair chains it holds that:
- sumList#(_ys, _x) matches r,
- all variables of sumList#(_ys, _x) are embedded in constructor contexts, i.e., each subterm of sumList#(_ys, _x), containing a variable is rooted by a constructor symbol.
Thus, sumList
#(
_ys,
_x) → if
#(isEmpty(
_ys), isZero(head(
_ys)),
_x, tail(
_ys), cons(p(head(
_ys)), tail(
_ys)), inc(
_x)) is replaced by instances determined through the above matching. These instances are:
| sumList#(xs, y) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | sumList#(ys, x) → if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) |
Instantiation
For all potential predecessors l → r of the rule sumList
#(
xs,
y) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) on dependency pair chains it holds that:
- sumList#(xs, y) matches r,
- all variables of sumList#(xs, y) are embedded in constructor contexts, i.e., each subterm of sumList#(xs, y), containing a variable is rooted by a constructor symbol.
Thus, sumList
#(
xs,
y) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) is replaced by instances determined through the above matching. These instances are:
| sumList#(ys, x) → if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) | sumList#(_xs, _y) → if#(isEmpty(_xs), isZero(head(_xs)), _y, tail(_xs), cons(p(head(_xs)), tail(_xs)), inc(_y)) |
Instantiation
For all potential predecessors l → r of the rule sumList
#(
ys,
x) → if
#(isEmpty(
ys), isZero(head(
ys)),
x, tail(
ys), cons(p(head(
ys)), tail(
ys)), inc(
x)) on dependency pair chains it holds that:
- sumList#(ys, x) matches r,
- all variables of sumList#(ys, x) are embedded in constructor contexts, i.e., each subterm of sumList#(ys, x), containing a variable is rooted by a constructor symbol.
Thus, sumList
#(
ys,
x) → if
#(isEmpty(
ys), isZero(head(
ys)),
x, tail(
ys), cons(p(head(
ys)), tail(
ys)), inc(
x)) is replaced by instances determined through the above matching. These instances are:
| sumList#(_ys, _x) → if#(isEmpty(_ys), isZero(head(_ys)), _x, tail(_ys), cons(p(head(_ys)), tail(_ys)), inc(_x)) | sumList#(xs, y) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) |
Problem 9: Propagation
Dependency Pair Problem
Dependency Pairs
| sumList#(_ys, _x) | → | if#(isEmpty(_ys), isZero(head(_ys)), _x, tail(_ys), cons(p(head(_ys)), tail(_ys)), inc(_x)) | | sumList#(xs, y) | → | if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) |
| if#(false, true, y, xs, xs, y) | → | sumList#(xs, y) | | if#(false, false, y, xs, ys, x) | → | sumList#(ys, x) |
| if#(false, false, x, ys, ys, x) | → | sumList#(ys, x) | | if#(false, true, y, xs, ys, x) | → | sumList#(xs, y) |
| sumList#(ys, x) | → | if#(isEmpty(ys), isZero(head(ys)), x, tail(ys), cons(p(head(ys)), tail(ys)), inc(x)) | | sumList#(_xs, _y) | → | if#(isEmpty(_xs), isZero(head(_xs)), _y, tail(_xs), cons(p(head(_xs)), tail(_xs)), inc(_y)) |
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, cons, nil, isZero
Strategy
The dependency pairs if
#(false, true,
y,
xs,
xs,
y) → sumList
#(
xs,
y) and sumList
#(
xs,
y) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) are consolidated into the rule if
#(false, true,
y,
xs,
xs,
y) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) .
This is possible as
- all subterms of sumList#(xs, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in sumList#(xs, y), but non-replacing in both if#(false, true, y, xs, xs, y) and if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))
The dependency pairs if
#(false, true,
y,
xs,
ys,
x) → sumList
#(
xs,
y) and sumList
#(
xs,
y) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) are consolidated into the rule if
#(false, true,
y,
xs,
ys,
x) → if
#(isEmpty(
xs), isZero(head(
xs)),
y, tail(
xs), cons(p(head(
xs)), tail(
xs)), inc(
y)) .
This is possible as
- all subterms of sumList#(xs, y) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in sumList#(xs, y), but non-replacing in both if#(false, true, y, xs, ys, x) and if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| sumList#(xs, y) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | if#(false, true, y, xs, ys, x) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) |
| if#(false, true, y, xs, xs, y) → sumList#(xs, y) | if#(false, true, y, xs, xs, y) → if#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) |
| if#(false, true, y, xs, ys, x) → sumList#(xs, y) | |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| isEmpty(cons(x, xs)) | → | false | | isEmpty(nil) | → | true |
| isZero(0) | → | true | | isZero(s(x)) | → | false |
| head(cons(x, xs)) | → | x | | tail(cons(x, xs)) | → | xs |
| tail(nil) | → | nil | | p(s(s(x))) | → | s(p(s(x))) |
| p(s(0)) | → | 0 | | p(0) | → | 0 |
| inc(s(x)) | → | s(inc(x)) | | inc(0) | → | s(0) |
| sumList(xs, y) | → | if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) | | if(true, b, y, xs, ys, x) | → | y |
| if(false, true, y, xs, ys, x) | → | sumList(xs, y) | | if(false, false, y, xs, ys, x) | → | sumList(ys, x) |
| sum(xs) | → | sumList(xs, 0) |
Original Signature
Termination of terms over the following signature is verified: sumList, sum, true, tail, isEmpty, 0, s, inc, if, p, false, head, isZero, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed: