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