YES
The TRS could be proven terminating. The proof took 163 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (4ms).
| – Problem 2 was processed with processor BackwardInstantiation (2ms).
| | – Problem 3 was processed with processor Propagation (1ms).
| | | – Problem 6 was processed with processor ForwardNarrowing (0ms).
| | – Problem 4 was processed with processor Propagation (1ms).
| | | – Problem 5 was processed with processor BackwardsNarrowing (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| h#(d) | → | g#(c) | | g#(X) | → | h#(X) |
| T(c) | → | c# |
Rewrite Rules
| g(X) | → | h(X) | | c | → | d |
| h(d) | → | g(c) |
Original Signature
Termination of terms over the following signature is verified: g, d, c, h
Strategy
Context-sensitive strategy:
μ(T) = μ(g) = μ(d) = μ(c) = μ(h#) = μ(c#) = μ(g#) = μ(h) = ∅
The following SCCs where found
| h#(d) → g#(c) | g#(X) → h#(X) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| h#(d) | → | g#(c) | | g#(X) | → | h#(X) |
Rewrite Rules
| g(X) | → | h(X) | | c | → | d |
| h(d) | → | g(c) |
Original Signature
Termination of terms over the following signature is verified: g, d, c, h
Strategy
Context-sensitive strategy:
μ(g) = μ(T) = μ(d) = μ(c) = μ(h#) = μ(c#) = μ(g#) = μ(h) = ∅
Instantiation
For all potential predecessors l → r of the rule g
#(
X) → h
#(
X) on dependency pair chains it holds that:
- g#(X) matches r,
- all variables of g#(X) are embedded in constructor contexts, i.e., each subterm of g#(X), containing a variable is rooted by a constructor symbol.
Thus, g
#(
X) → h
#(
X) is replaced by instances determined through the above matching. These instances are:
Problem 3: Propagation
Dependency Pair Problem
Dependency Pairs
| h#(d) | → | g#(c) | | g#(c) | → | h#(c) |
Rewrite Rules
| g(X) | → | h(X) | | c | → | d |
| h(d) | → | g(c) |
Original Signature
Termination of terms over the following signature is verified: g, d, c, h
Strategy
Context-sensitive strategy:
μ(T) = μ(g) = μ(d) = μ(c) = μ(h#) = μ(c#) = μ(g#) = μ(h) = ∅
The dependency pairs h
#(d) → g
#(c) and g
#(c) → h
#(c) are consolidated into the rule h
#(d) → h
#(c) .
This is possible as
- all subterms of g#(c) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#(c), but non-replacing in both h#(d) and h#(c)
The dependency pairs h
#(d) → g
#(c) and g
#(c) → h
#(c) are consolidated into the rule h
#(d) → h
#(c) .
This is possible as
- all subterms of g#(c) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#(c), but non-replacing in both h#(d) and h#(c)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| h#(d) → g#(c) | h#(d) → h#(c) |
| g#(c) → h#(c) | |
Problem 6: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| g(X) | → | h(X) | | c | → | d |
| h(d) | → | g(c) |
Original Signature
Termination of terms over the following signature is verified: g, d, c, h
Strategy
Context-sensitive strategy:
μ(g) = μ(T) = μ(d) = μ(c) = μ(h#) = μ(c#) = μ(g#) = μ(h) = ∅
The right-hand side of the rule h
#(d) → h
#(c) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule h
#(d) → h
#(c) is deleted.
Problem 4: Propagation
Dependency Pair Problem
Dependency Pairs
| h#(d) | → | g#(c) | | g#(c) | → | h#(c) |
Rewrite Rules
| g(X) | → | h(X) | | c | → | d |
| h(d) | → | g(c) |
Original Signature
Termination of terms over the following signature is verified: g, d, c, h
Strategy
Context-sensitive strategy:
μ(T) = μ(g) = μ(d) = μ(c) = μ(h#) = μ(c#) = μ(g#) = μ(h) = ∅
The dependency pairs h
#(d) → g
#(c) and g
#(c) → h
#(c) are consolidated into the rule h
#(d) → h
#(c) .
This is possible as
- all subterms of g#(c) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#(c), but non-replacing in both h#(d) and h#(c)
The dependency pairs h
#(d) → g
#(c) and g
#(c) → h
#(c) are consolidated into the rule h
#(d) → h
#(c) .
This is possible as
- all subterms of g#(c) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in g#(c), but non-replacing in both h#(d) and h#(c)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| h#(d) → g#(c) | h#(d) → h#(c) |
| g#(c) → h#(c) | |
Problem 5: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| g(X) | → | h(X) | | c | → | d |
| h(d) | → | g(c) |
Original Signature
Termination of terms over the following signature is verified: g, d, c, h
Strategy
Context-sensitive strategy:
μ(g) = μ(T) = μ(d) = μ(c) = μ(h#) = μ(c#) = μ(g#) = μ(h) = ∅
The left-hand side of the rule h
#(d) → h
#(c) is backward narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
Thus, the rule h
#(d) → h
#(c) is deleted.