NO
The TRS could be proven non-terminating. The proof took 172 ms.
The following reduction sequence is a witness for non-termination:
f#(a) →* f#(a)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (11ms).
| – Problem 2 was processed with processor BackwardInstantiation (1ms).
| | – Problem 3 was processed with processor Propagation (1ms).
| | | – Problem 4 was processed with processor BackwardInstantiation (1ms).
| | | | – Problem 5 was processed with processor BackwardInstantiation (1ms).
| | | | | – Problem 6 remains open; application of the following processors failed [ForwardInstantiation (1ms), Propagation (1ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U41#(g(b), x) | → | T(x) | | f#(a) | → | c# |
| c# | → | a# | | f#(x) | → | U41#(f(x), x) |
| f#(x) | → | f#(x) | | c# | → | f#(a) |
Rewrite Rules
| a | → | b | | c | → | f(a) |
| f(a) | → | c | | c | → | g(b) |
| f(x) | → | U41(f(x), x) | | U41(g(b), x) | → | g(x) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = μ(a#) = ∅
μ(f) = μ(g) = μ(U41#) = μ(f#) = μ(U41) = {1}
The following SCCs where found
| f#(a) → c# | f#(x) → f#(x) |
| c# → f#(a) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(a) | → | c# | | f#(x) | → | f#(x) |
| c# | → | f#(a) |
Rewrite Rules
| a | → | b | | c | → | f(a) |
| f(a) | → | c | | c | → | g(b) |
| f(x) | → | U41(f(x), x) | | U41(g(b), x) | → | g(x) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = μ(a#) = ∅
μ(f) = μ(g) = μ(f#) = μ(U41#) = μ(U41) = {1}
Instantiation
For all potential predecessors l → r of the rule f
#(
x) → f
#(
x) on dependency pair chains it holds that:
- f#(x) matches r,
- all variables of f#(x) are embedded in constructor contexts, i.e., each subterm of f#(x), containing a variable is rooted by a constructor symbol.
Thus, f
#(
x) → f
#(
x) is replaced by instances determined through the above matching. These instances are:
| f#(_x) → f#(_x) | f#(a) → f#(a) |
Problem 3: Propagation
Dependency Pair Problem
Dependency Pairs
| f#(_x) | → | f#(_x) | | f#(a) | → | f#(a) |
| f#(a) | → | c# | | c# | → | f#(a) |
Rewrite Rules
| a | → | b | | c | → | f(a) |
| f(a) | → | c | | c | → | g(b) |
| f(x) | → | U41(f(x), x) | | U41(g(b), x) | → | g(x) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = μ(a#) = ∅
μ(f) = μ(g) = μ(U41#) = μ(f#) = μ(U41) = {1}
The dependency pairs f
#(
_x) → f
#(
_x) and f
#(
_x) → f
#(
_x) are consolidated into the rule f
#(
_x) → f
#(
_x) .
This is possible as
- all subterms of f#(_x) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in f#(_x), but non-replacing in both f#(_x) and f#(_x)
The dependency pairs f
#(a) → c
# and c
# → f
#(a) are consolidated into the rule f
#(a) → f
#(a) .
This is possible as
- all subterms of c# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in c#, but non-replacing in both f#(a) and f#(a)
The dependency pairs f
#(a) → c
# and c
# → f
#(a) are consolidated into the rule f
#(a) → f
#(a) .
This is possible as
- all subterms of c# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in c#, but non-replacing in both f#(a) and f#(a)
The dependency pairs f
#(a) → c
# and c
# → f
#(a) are consolidated into the rule f
#(a) → f
#(a) .
This is possible as
- all subterms of c# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in c#, but non-replacing in both f#(a) and f#(a)
The dependency pairs f
#(a) → c
# and c
# → f
#(a) are consolidated into the rule f
#(a) → f
#(a) .
This is possible as
- all subterms of c# containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in c#, but non-replacing in both f#(a) and f#(a)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| f#(_x) → f#(_x) | f#(_x) → f#(_x) |
| f#(a) → c# | f#(a) → f#(a) |
| c# → f#(a) | |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(_x) | → | f#(_x) | | f#(a) | → | f#(a) |
Rewrite Rules
| a | → | b | | c | → | f(a) |
| f(a) | → | c | | c | → | g(b) |
| f(x) | → | U41(f(x), x) | | U41(g(b), x) | → | g(x) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = μ(a#) = ∅
μ(f) = μ(g) = μ(f#) = μ(U41#) = μ(U41) = {1}
Instantiation
For all potential predecessors l → r of the rule f
#(
_x) → f
#(
_x) on dependency pair chains it holds that:
- f#(_x) matches r,
- all variables of f#(_x) are embedded in constructor contexts, i.e., each subterm of f#(_x), containing a variable is rooted by a constructor symbol.
Thus, f
#(
_x) → f
#(
_x) is replaced by instances determined through the above matching. These instances are:
| f#(a) → f#(a) | f#(__x) → f#(__x) |
Problem 5: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| f#(a) | → | f#(a) | | f#(__x) | → | f#(__x) |
Rewrite Rules
| a | → | b | | c | → | f(a) |
| f(a) | → | c | | c | → | g(b) |
| f(x) | → | U41(f(x), x) | | U41(g(b), x) | → | g(x) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, c, a
Strategy
Context-sensitive strategy:
μ(T) = μ(b) = μ(c) = μ(a) = μ(c#) = μ(a#) = ∅
μ(f) = μ(g) = μ(U41#) = μ(f#) = μ(U41) = {1}
Instantiation
For all potential predecessors l → r of the rule f
#(
__x) → f
#(
__x) on dependency pair chains it holds that:
- f#(__x) matches r,
- all variables of f#(__x) are embedded in constructor contexts, i.e., each subterm of f#(__x), containing a variable is rooted by a constructor symbol.
Thus, f
#(
__x) → f
#(
__x) is replaced by instances determined through the above matching. These instances are:
| f#(a) → f#(a) | f#(___x) → f#(___x) |