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 (65ms).
| – Problem 2 was processed with processor BackwardInstantiation (2ms).
| | – Problem 4 was processed with processor ForwardInstantiation (2ms).
| | | – Problem 5 was processed with processor Propagation (3ms).
| | | | – Problem 6 remains open; application of the following processors failed [ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].
| – Problem 3 was processed with processor SubtermCriterion (1ms).
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| less_leaves#(u, v) | → | if1#(isLeaf(u), isLeaf(v), u, v) | | if1#(b, false, u, v) | → | if2#(b, u, v) |
| if2#(false, u, v) | → | less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) |
Rewrite Rules
| isLeaf(leaf) | → | true | | isLeaf(cons(u, v)) | → | false |
| left(cons(u, v)) | → | u | | right(cons(u, v)) | → | v |
| concat(leaf, y) | → | y | | concat(cons(u, v), y) | → | cons(u, concat(v, y)) |
| less_leaves(u, v) | → | if1(isLeaf(u), isLeaf(v), u, v) | | if1(b, true, u, v) | → | false |
| if1(b, false, u, v) | → | if2(b, u, v) | | if2(true, u, v) | → | true |
| if2(false, u, v) | → | less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) |
Original Signature
Termination of terms over the following signature is verified: isLeaf, false, true, if1, left, if2, leaf, less_leaves, concat, right, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| less_leaves#(u, v) | → | if1#(isLeaf(u), isLeaf(v), u, v) | | if2#(false, u, v) | → | concat#(left(v), right(v)) |
| if2#(false, u, v) | → | right#(v) | | if2#(false, u, v) | → | concat#(left(u), right(u)) |
| if2#(false, u, v) | → | left#(u) | | less_leaves#(u, v) | → | isLeaf#(u) |
| if1#(b, false, u, v) | → | if2#(b, u, v) | | if2#(false, u, v) | → | right#(u) |
| if2#(false, u, v) | → | left#(v) | | if2#(false, u, v) | → | less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) |
| concat#(cons(u, v), y) | → | concat#(v, y) | | less_leaves#(u, v) | → | isLeaf#(v) |
Rewrite Rules
| isLeaf(leaf) | → | true | | isLeaf(cons(u, v)) | → | false |
| left(cons(u, v)) | → | u | | right(cons(u, v)) | → | v |
| concat(leaf, y) | → | y | | concat(cons(u, v), y) | → | cons(u, concat(v, y)) |
| less_leaves(u, v) | → | if1(isLeaf(u), isLeaf(v), u, v) | | if1(b, true, u, v) | → | false |
| if1(b, false, u, v) | → | if2(b, u, v) | | if2(true, u, v) | → | true |
| if2(false, u, v) | → | less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) |
Original Signature
Termination of terms over the following signature is verified: isLeaf, true, false, left, if1, leaf, if2, right, concat, less_leaves, cons
Strategy
The following SCCs where found
| less_leaves#(u, v) → if1#(isLeaf(u), isLeaf(v), u, v) | if1#(b, false, u, v) → if2#(b, u, v) |
| if2#(false, u, v) → less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) |
| concat#(cons(u, v), y) → concat#(v, y) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| less_leaves#(u, v) | → | if1#(isLeaf(u), isLeaf(v), u, v) | | if1#(b, false, u, v) | → | if2#(b, u, v) |
| if2#(false, u, v) | → | less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) |
Rewrite Rules
| isLeaf(leaf) | → | true | | isLeaf(cons(u, v)) | → | false |
| left(cons(u, v)) | → | u | | right(cons(u, v)) | → | v |
| concat(leaf, y) | → | y | | concat(cons(u, v), y) | → | cons(u, concat(v, y)) |
| less_leaves(u, v) | → | if1(isLeaf(u), isLeaf(v), u, v) | | if1(b, true, u, v) | → | false |
| if1(b, false, u, v) | → | if2(b, u, v) | | if2(true, u, v) | → | true |
| if2(false, u, v) | → | less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) |
Original Signature
Termination of terms over the following signature is verified: isLeaf, true, false, left, if1, leaf, if2, right, concat, less_leaves, cons
Strategy
Instantiation
For all potential predecessors l → r of the rule less_leaves
#(
u,
v) → if1
#(isLeaf(
u), isLeaf(
v),
u,
v) on dependency pair chains it holds that:
- less_leaves#(u, v) matches r,
- all variables of less_leaves#(u, v) are embedded in constructor contexts, i.e., each subterm of less_leaves#(u, v), containing a variable is rooted by a constructor symbol.
Thus, less_leaves
#(
u,
v) → if1
#(isLeaf(
u), isLeaf(
v),
u,
v) is replaced by instances determined through the above matching. These instances are:
| less_leaves#(concat(left(_u), right(_u)), concat(left(_v), right(_v))) → if1#(isLeaf(concat(left(_u), right(_u))), isLeaf(concat(left(_v), right(_v))), concat(left(_u), right(_u)), concat(left(_v), right(_v))) |
Problem 4: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| less_leaves#(concat(left(_u), right(_u)), concat(left(_v), right(_v))) | → | if1#(isLeaf(concat(left(_u), right(_u))), isLeaf(concat(left(_v), right(_v))), concat(left(_u), right(_u)), concat(left(_v), right(_v))) | | if1#(b, false, u, v) | → | if2#(b, u, v) |
| if2#(false, u, v) | → | less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) |
Rewrite Rules
| isLeaf(leaf) | → | true | | isLeaf(cons(u, v)) | → | false |
| left(cons(u, v)) | → | u | | right(cons(u, v)) | → | v |
| concat(leaf, y) | → | y | | concat(cons(u, v), y) | → | cons(u, concat(v, y)) |
| less_leaves(u, v) | → | if1(isLeaf(u), isLeaf(v), u, v) | | if1(b, true, u, v) | → | false |
| if1(b, false, u, v) | → | if2(b, u, v) | | if2(true, u, v) | → | true |
| if2(false, u, v) | → | less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) |
Original Signature
Termination of terms over the following signature is verified: isLeaf, false, true, if1, left, if2, leaf, less_leaves, concat, right, cons
Strategy
Instantiation
For all potential successors l → r of the rule if1
#(
b, false,
u,
v) → if2
#(
b,
u,
v) on dependency pair chains it holds that:
- if2#(b, u, v) matches l,
- all variables of if2#(b, u, v) are embedded in constructor contexts, i.e., each subterm of if2#(b, u, v) containing a variable is rooted by a constructor symbol.
Thus, if1
#(
b, false,
u,
v) → if2
#(
b,
u,
v) is replaced by instances determined through the above matching. These instances are:
| if1#(false, false, u, v) → if2#(false, u, v) |
Problem 5: Propagation
Dependency Pair Problem
Dependency Pairs
| less_leaves#(concat(left(_u), right(_u)), concat(left(_v), right(_v))) | → | if1#(isLeaf(concat(left(_u), right(_u))), isLeaf(concat(left(_v), right(_v))), concat(left(_u), right(_u)), concat(left(_v), right(_v))) | | if1#(false, false, u, v) | → | if2#(false, u, v) |
| if2#(false, u, v) | → | less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) |
Rewrite Rules
| isLeaf(leaf) | → | true | | isLeaf(cons(u, v)) | → | false |
| left(cons(u, v)) | → | u | | right(cons(u, v)) | → | v |
| concat(leaf, y) | → | y | | concat(cons(u, v), y) | → | cons(u, concat(v, y)) |
| less_leaves(u, v) | → | if1(isLeaf(u), isLeaf(v), u, v) | | if1(b, true, u, v) | → | false |
| if1(b, false, u, v) | → | if2(b, u, v) | | if2(true, u, v) | → | true |
| if2(false, u, v) | → | less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) |
Original Signature
Termination of terms over the following signature is verified: isLeaf, true, false, left, if1, leaf, if2, right, concat, less_leaves, cons
Strategy
The dependency pairs if1
#(false, false,
u,
v) → if2
#(false,
u,
v) and if2
#(false,
u,
v) → less_leaves
#(concat(left(
u), right(
u)), concat(left(
v), right(
v))) are consolidated into the rule if1
#(false, false,
u,
v) → less_leaves
#(concat(left(
u), right(
u)), concat(left(
v), right(
v))) .
This is possible as
- all subterms of if2#(false, u, v) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, u, v), but non-replacing in both if1#(false, false, u, v) and less_leaves#(concat(left(u), right(u)), concat(left(v), right(v)))
The dependency pairs if1
#(false, false,
u,
v) → if2
#(false,
u,
v) and if2
#(false,
u,
v) → less_leaves
#(concat(left(
u), right(
u)), concat(left(
v), right(
v))) are consolidated into the rule if1
#(false, false,
u,
v) → less_leaves
#(concat(left(
u), right(
u)), concat(left(
v), right(
v))) .
This is possible as
- all subterms of if2#(false, u, v) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, u, v), but non-replacing in both if1#(false, false, u, v) and less_leaves#(concat(left(u), right(u)), concat(left(v), right(v)))
The dependency pairs if1
#(false, false,
u,
v) → if2
#(false,
u,
v) and if2
#(false,
u,
v) → less_leaves
#(concat(left(
u), right(
u)), concat(left(
v), right(
v))) are consolidated into the rule if1
#(false, false,
u,
v) → less_leaves
#(concat(left(
u), right(
u)), concat(left(
v), right(
v))) .
This is possible as
- all subterms of if2#(false, u, v) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in if2#(false, u, v), but non-replacing in both if1#(false, false, u, v) and less_leaves#(concat(left(u), right(u)), concat(left(v), right(v)))
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| if1#(false, false, u, v) → if2#(false, u, v) | if1#(false, false, u, v) → less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) |
| if2#(false, u, v) → less_leaves#(concat(left(u), right(u)), concat(left(v), right(v))) | |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| concat#(cons(u, v), y) | → | concat#(v, y) |
Rewrite Rules
| isLeaf(leaf) | → | true | | isLeaf(cons(u, v)) | → | false |
| left(cons(u, v)) | → | u | | right(cons(u, v)) | → | v |
| concat(leaf, y) | → | y | | concat(cons(u, v), y) | → | cons(u, concat(v, y)) |
| less_leaves(u, v) | → | if1(isLeaf(u), isLeaf(v), u, v) | | if1(b, true, u, v) | → | false |
| if1(b, false, u, v) | → | if2(b, u, v) | | if2(true, u, v) | → | true |
| if2(false, u, v) | → | less_leaves(concat(left(u), right(u)), concat(left(v), right(v))) |
Original Signature
Termination of terms over the following signature is verified: isLeaf, true, false, left, if1, leaf, if2, right, concat, less_leaves, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| concat#(cons(u, v), y) | → | concat#(v, y) |