MAYBE
The TRS could not be proven terminating. The proof attempt took 2404 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (51ms).
| – Problem 2 was processed with processor BackwardInstantiation (1ms).
| | – Problem 4 was processed with processor Propagation (1ms).
| | | – Problem 8 was processed with processor BackwardInstantiation (0ms).
| | | | – Problem 13 was processed with processor Propagation (0ms).
| | | | | – Problem 16 was processed with processor ForwardInstantiation (1ms).
| | | | | | – Problem 20 remains open; application of the following processors failed [Propagation (0ms)].
| | – Problem 5 was processed with processor Propagation (1ms).
| | | – Problem 9 was processed with processor BackwardInstantiation (20ms).
| | | | – Problem 12 was processed with processor Propagation (0ms).
| | | | | – Problem 17 was processed with processor ForwardInstantiation (1ms).
| | | | | | – Problem 21 remains open; application of the following processors failed [Propagation (1ms)].
| – Problem 3 was processed with processor BackwardInstantiation (2ms).
| | – Problem 6 was processed with processor Propagation (1ms).
| | | – Problem 11 was processed with processor BackwardInstantiation (0ms).
| | | | – Problem 14 was processed with processor Propagation (1ms).
| | | | | – Problem 18 was processed with processor ForwardInstantiation (0ms).
| | | | | | – Problem 22 remains open; application of the following processors failed [Propagation (0ms)].
| | – Problem 7 was processed with processor Propagation (1ms).
| | | – Problem 10 was processed with processor BackwardInstantiation (0ms).
| | | | – Problem 15 was processed with processor Propagation (1ms).
| | | | | – Problem 19 was processed with processor ForwardInstantiation (21ms).
| | | | | | – Problem 23 remains open; application of the following processors failed [Propagation (0ms)].
The following open problems remain:
Open Dependency Pair Problem 20
Dependency Pairs
| x#(N, s(s(_M))) | → | x#(N, s(_M)) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Open Dependency Pair Problem 22
Dependency Pairs
| plus#(N, s(s(_M))) | → | plus#(N, s(_M)) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| U21#(tt, M, N) | → | U22#(tt, M, N) | | U22#(tt, M, N) | → | plus#(x(N, M), N) |
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U22#(tt, M, N) | → | T(M) |
| U22#(tt, M, N) | → | T(N) | | x#(N, s(M)) | → | U21#(tt, M, N) |
| U12#(tt, M, N) | → | T(M) | | U22#(tt, M, N) | → | x#(N, M) |
| U12#(tt, M, N) | → | plus#(N, M) | | U11#(tt, M, N) | → | U12#(tt, M, N) |
| U12#(tt, M, N) | → | T(N) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The following SCCs where found
| U21#(tt, M, N) → U22#(tt, M, N) | x#(N, s(M)) → U21#(tt, M, N) |
| U22#(tt, M, N) → x#(N, M) |
| plus#(N, s(M)) → U11#(tt, M, N) | U12#(tt, M, N) → plus#(N, M) |
| U11#(tt, M, N) → U12#(tt, M, N) |
Problem 2: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| U21#(tt, M, N) | → | U22#(tt, M, N) | | x#(N, s(M)) | → | U21#(tt, M, N) |
| U22#(tt, M, N) | → | x#(N, M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule
U21#(tt,
M,
N) →
U22#(tt,
M,
N) on dependency pair chains it holds that:
- U21#(tt, M, N) matches r,
- all variables of U21#(tt, M, N) are embedded in constructor contexts, i.e., each subterm of U21#(tt, M, N), containing a variable is rooted by a constructor symbol.
Thus,
U21#(tt,
M,
N) →
U22#(tt,
M,
N) is replaced by instances determined through the above matching. These instances are:
| U21#(tt, _M, _N) → U22#(tt, _M, _N) |
Instantiation
For all potential predecessors l → r of the rule
U22#(tt,
M,
N) → x
#(
N,
M) on dependency pair chains it holds that:
- U22#(tt, M, N) matches r,
- all variables of U22#(tt, M, N) are embedded in constructor contexts, i.e., each subterm of U22#(tt, M, N), containing a variable is rooted by a constructor symbol.
Thus,
U22#(tt,
M,
N) → x
#(
N,
M) is replaced by instances determined through the above matching. These instances are:
| U22#(tt, _M, _N) → x#(_N, _M) |
Problem 4: Propagation
Dependency Pair Problem
Dependency Pairs
| x#(N, s(M)) | → | U21#(tt, M, N) | | U22#(tt, _M, _N) | → | x#(_N, _M) |
| U21#(tt, _M, _N) | → | U22#(tt, _M, _N) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs
U21#(tt,
_M,
_N) →
U22#(tt,
_M,
_N) and
U22#(tt,
_M,
_N) → x
#(
_N,
_M) are consolidated into the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) .
This is possible as
- all subterms of U22#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U22#(tt, _M, _N), but non-replacing in both U21#(tt, _M, _N) and x#(_N, _M)
The dependency pairs
U21#(tt,
_M,
_N) →
U22#(tt,
_M,
_N) and
U22#(tt,
_M,
_N) → x
#(
_N,
_M) are consolidated into the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) .
This is possible as
- all subterms of U22#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U22#(tt, _M, _N), but non-replacing in both U21#(tt, _M, _N) and x#(_N, _M)
The dependency pairs
U21#(tt,
_M,
_N) →
U22#(tt,
_M,
_N) and
U22#(tt,
_M,
_N) → x
#(
_N,
_M) are consolidated into the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) .
This is possible as
- all subterms of U22#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U22#(tt, _M, _N), but non-replacing in both U21#(tt, _M, _N) and x#(_N, _M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| U22#(tt, _M, _N) → x#(_N, _M) | U21#(tt, _M, _N) → x#(_N, _M) |
| U21#(tt, _M, _N) → U22#(tt, _M, _N) | |
Problem 8: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| U21#(tt, _M, _N) | → | x#(_N, _M) | | x#(N, s(M)) | → | U21#(tt, M, N) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) on dependency pair chains it holds that:
- U21#(tt, _M, _N) matches r,
- all variables of U21#(tt, _M, _N) are embedded in constructor contexts, i.e., each subterm of U21#(tt, _M, _N), containing a variable is rooted by a constructor symbol.
Thus,
U21#(tt,
_M,
_N) → x
#(
_N,
_M) is replaced by instances determined through the above matching. These instances are:
| U21#(tt, M, N) → x#(N, M) |
Problem 13: Propagation
Dependency Pair Problem
Dependency Pairs
| x#(N, s(M)) | → | U21#(tt, M, N) | | U21#(tt, M, N) | → | x#(N, M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs x
#(
N, s(
M)) →
U21#(tt,
M,
N) and
U21#(tt,
M,
N) → x
#(
N,
M) are consolidated into the rule x
#(
N, s(
M)) → x
#(
N,
M) .
This is possible as
- all subterms of U21#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U21#(tt, M, N), but non-replacing in both x#(N, s(M)) and x#(N, M)
The dependency pairs x
#(
N, s(
M)) →
U21#(tt,
M,
N) and
U21#(tt,
M,
N) → x
#(
N,
M) are consolidated into the rule x
#(
N, s(
M)) → x
#(
N,
M) .
This is possible as
- all subterms of U21#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U21#(tt, M, N), but non-replacing in both x#(N, s(M)) and x#(N, M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| x#(N, s(M)) → U21#(tt, M, N) | x#(N, s(M)) → x#(N, M) |
| U21#(tt, M, N) → x#(N, M) | |
Problem 16: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential successors l → r of the rule x
#(
N, s(
M)) → x
#(
N,
M) on dependency pair chains it holds that:
- x#(N, M) matches l,
- all variables of x#(N, M) are embedded in constructor contexts, i.e., each subterm of x#(N, M) containing a variable is rooted by a constructor symbol.
Thus, x
#(
N, s(
M)) → x
#(
N,
M) is replaced by instances determined through the above matching. These instances are:
| x#(N, s(s(_M))) → x#(N, s(_M)) |
Problem 5: Propagation
Dependency Pair Problem
Dependency Pairs
| x#(N, s(M)) | → | U21#(tt, M, N) | | U22#(tt, _M, _N) | → | x#(_N, _M) |
| U21#(tt, _M, _N) | → | U22#(tt, _M, _N) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs
U21#(tt,
_M,
_N) →
U22#(tt,
_M,
_N) and
U22#(tt,
_M,
_N) → x
#(
_N,
_M) are consolidated into the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) .
This is possible as
- all subterms of U22#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U22#(tt, _M, _N), but non-replacing in both U21#(tt, _M, _N) and x#(_N, _M)
The dependency pairs
U21#(tt,
_M,
_N) →
U22#(tt,
_M,
_N) and
U22#(tt,
_M,
_N) → x
#(
_N,
_M) are consolidated into the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) .
This is possible as
- all subterms of U22#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U22#(tt, _M, _N), but non-replacing in both U21#(tt, _M, _N) and x#(_N, _M)
The dependency pairs
U21#(tt,
_M,
_N) →
U22#(tt,
_M,
_N) and
U22#(tt,
_M,
_N) → x
#(
_N,
_M) are consolidated into the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) .
This is possible as
- all subterms of U22#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U22#(tt, _M, _N), but non-replacing in both U21#(tt, _M, _N) and x#(_N, _M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| U22#(tt, _M, _N) → x#(_N, _M) | U21#(tt, _M, _N) → x#(_N, _M) |
| U21#(tt, _M, _N) → U22#(tt, _M, _N) | |
Problem 9: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| U21#(tt, _M, _N) | → | x#(_N, _M) | | x#(N, s(M)) | → | U21#(tt, M, N) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule
U21#(tt,
_M,
_N) → x
#(
_N,
_M) on dependency pair chains it holds that:
- U21#(tt, _M, _N) matches r,
- all variables of U21#(tt, _M, _N) are embedded in constructor contexts, i.e., each subterm of U21#(tt, _M, _N), containing a variable is rooted by a constructor symbol.
Thus,
U21#(tt,
_M,
_N) → x
#(
_N,
_M) is replaced by instances determined through the above matching. These instances are:
| U21#(tt, M, N) → x#(N, M) |
Problem 12: Propagation
Dependency Pair Problem
Dependency Pairs
| x#(N, s(M)) | → | U21#(tt, M, N) | | U21#(tt, M, N) | → | x#(N, M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs x
#(
N, s(
M)) →
U21#(tt,
M,
N) and
U21#(tt,
M,
N) → x
#(
N,
M) are consolidated into the rule x
#(
N, s(
M)) → x
#(
N,
M) .
This is possible as
- all subterms of U21#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U21#(tt, M, N), but non-replacing in both x#(N, s(M)) and x#(N, M)
The dependency pairs x
#(
N, s(
M)) →
U21#(tt,
M,
N) and
U21#(tt,
M,
N) → x
#(
N,
M) are consolidated into the rule x
#(
N, s(
M)) → x
#(
N,
M) .
This is possible as
- all subterms of U21#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U21#(tt, M, N), but non-replacing in both x#(N, s(M)) and x#(N, M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| x#(N, s(M)) → U21#(tt, M, N) | x#(N, s(M)) → x#(N, M) |
| U21#(tt, M, N) → x#(N, M) | |
Problem 17: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential successors l → r of the rule x
#(
N, s(
M)) → x
#(
N,
M) on dependency pair chains it holds that:
- x#(N, M) matches l,
- all variables of x#(N, M) are embedded in constructor contexts, i.e., each subterm of x#(N, M) containing a variable is rooted by a constructor symbol.
Thus, x
#(
N, s(
M)) → x
#(
N,
M) is replaced by instances determined through the above matching. These instances are:
| x#(N, s(s(_M))) → x#(N, s(_M)) |
Problem 3: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U12#(tt, M, N) | → | plus#(N, M) |
| U11#(tt, M, N) | → | U12#(tt, M, N) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule
U12#(tt,
M,
N) → plus
#(
N,
M) on dependency pair chains it holds that:
- U12#(tt, M, N) matches r,
- all variables of U12#(tt, M, N) are embedded in constructor contexts, i.e., each subterm of U12#(tt, M, N), containing a variable is rooted by a constructor symbol.
Thus,
U12#(tt,
M,
N) → plus
#(
N,
M) is replaced by instances determined through the above matching. These instances are:
| U12#(tt, _M, _N) → plus#(_N, _M) |
Instantiation
For all potential predecessors l → r of the rule
U11#(tt,
M,
N) →
U12#(tt,
M,
N) on dependency pair chains it holds that:
- U11#(tt, M, N) matches r,
- all variables of U11#(tt, M, N) are embedded in constructor contexts, i.e., each subterm of U11#(tt, M, N), containing a variable is rooted by a constructor symbol.
Thus,
U11#(tt,
M,
N) →
U12#(tt,
M,
N) is replaced by instances determined through the above matching. These instances are:
| U11#(tt, _M, _N) → U12#(tt, _M, _N) |
Problem 6: Propagation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U11#(tt, _M, _N) | → | U12#(tt, _M, _N) |
| U12#(tt, _M, _N) | → | plus#(_N, _M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs
U11#(tt,
_M,
_N) →
U12#(tt,
_M,
_N) and
U12#(tt,
_M,
_N) → plus
#(
_N,
_M) are consolidated into the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) .
This is possible as
- all subterms of U12#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _M, _N), but non-replacing in both U11#(tt, _M, _N) and plus#(_N, _M)
The dependency pairs
U11#(tt,
_M,
_N) →
U12#(tt,
_M,
_N) and
U12#(tt,
_M,
_N) → plus
#(
_N,
_M) are consolidated into the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) .
This is possible as
- all subterms of U12#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _M, _N), but non-replacing in both U11#(tt, _M, _N) and plus#(_N, _M)
The dependency pairs
U11#(tt,
_M,
_N) →
U12#(tt,
_M,
_N) and
U12#(tt,
_M,
_N) → plus
#(
_N,
_M) are consolidated into the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) .
This is possible as
- all subterms of U12#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _M, _N), but non-replacing in both U11#(tt, _M, _N) and plus#(_N, _M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| U11#(tt, _M, _N) → U12#(tt, _M, _N) | U11#(tt, _M, _N) → plus#(_N, _M) |
| U12#(tt, _M, _N) → plus#(_N, _M) | |
Problem 11: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U11#(tt, _M, _N) | → | plus#(_N, _M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) on dependency pair chains it holds that:
- U11#(tt, _M, _N) matches r,
- all variables of U11#(tt, _M, _N) are embedded in constructor contexts, i.e., each subterm of U11#(tt, _M, _N), containing a variable is rooted by a constructor symbol.
Thus,
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) is replaced by instances determined through the above matching. These instances are:
| U11#(tt, M, N) → plus#(N, M) |
Problem 14: Propagation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U11#(tt, M, N) | → | plus#(N, M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs plus
#(
N, s(
M)) →
U11#(tt,
M,
N) and
U11#(tt,
M,
N) → plus
#(
N,
M) are consolidated into the rule plus
#(
N, s(
M)) → plus
#(
N,
M) .
This is possible as
- all subterms of U11#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, M, N), but non-replacing in both plus#(N, s(M)) and plus#(N, M)
The dependency pairs plus
#(
N, s(
M)) →
U11#(tt,
M,
N) and
U11#(tt,
M,
N) → plus
#(
N,
M) are consolidated into the rule plus
#(
N, s(
M)) → plus
#(
N,
M) .
This is possible as
- all subterms of U11#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, M, N), but non-replacing in both plus#(N, s(M)) and plus#(N, M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| plus#(N, s(M)) → U11#(tt, M, N) | plus#(N, s(M)) → plus#(N, M) |
| U11#(tt, M, N) → plus#(N, M) | |
Problem 18: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | plus#(N, M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential successors l → r of the rule plus
#(
N, s(
M)) → plus
#(
N,
M) on dependency pair chains it holds that:
- plus#(N, M) matches l,
- all variables of plus#(N, M) are embedded in constructor contexts, i.e., each subterm of plus#(N, M) containing a variable is rooted by a constructor symbol.
Thus, plus
#(
N, s(
M)) → plus
#(
N,
M) is replaced by instances determined through the above matching. These instances are:
| plus#(N, s(s(_M))) → plus#(N, s(_M)) |
Problem 7: Propagation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U11#(tt, _M, _N) | → | U12#(tt, _M, _N) |
| U12#(tt, _M, _N) | → | plus#(_N, _M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs
U11#(tt,
_M,
_N) →
U12#(tt,
_M,
_N) and
U12#(tt,
_M,
_N) → plus
#(
_N,
_M) are consolidated into the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) .
This is possible as
- all subterms of U12#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _M, _N), but non-replacing in both U11#(tt, _M, _N) and plus#(_N, _M)
The dependency pairs
U11#(tt,
_M,
_N) →
U12#(tt,
_M,
_N) and
U12#(tt,
_M,
_N) → plus
#(
_N,
_M) are consolidated into the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) .
This is possible as
- all subterms of U12#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _M, _N), but non-replacing in both U11#(tt, _M, _N) and plus#(_N, _M)
The dependency pairs
U11#(tt,
_M,
_N) →
U12#(tt,
_M,
_N) and
U12#(tt,
_M,
_N) → plus
#(
_N,
_M) are consolidated into the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) .
This is possible as
- all subterms of U12#(tt, _M, _N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U12#(tt, _M, _N), but non-replacing in both U11#(tt, _M, _N) and plus#(_N, _M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| U11#(tt, _M, _N) → U12#(tt, _M, _N) | U11#(tt, _M, _N) → plus#(_N, _M) |
| U12#(tt, _M, _N) → plus#(_N, _M) | |
Problem 10: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U11#(tt, _M, _N) | → | plus#(_N, _M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) on dependency pair chains it holds that:
- U11#(tt, _M, _N) matches r,
- all variables of U11#(tt, _M, _N) are embedded in constructor contexts, i.e., each subterm of U11#(tt, _M, _N), containing a variable is rooted by a constructor symbol.
Thus,
U11#(tt,
_M,
_N) → plus
#(
_N,
_M) is replaced by instances determined through the above matching. These instances are:
| U11#(tt, M, N) → plus#(N, M) |
Problem 15: Propagation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | U11#(tt, M, N) | | U11#(tt, M, N) | → | plus#(N, M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, x, U22
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
The dependency pairs plus
#(
N, s(
M)) →
U11#(tt,
M,
N) and
U11#(tt,
M,
N) → plus
#(
N,
M) are consolidated into the rule plus
#(
N, s(
M)) → plus
#(
N,
M) .
This is possible as
- all subterms of U11#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, M, N), but non-replacing in both plus#(N, s(M)) and plus#(N, M)
The dependency pairs plus
#(
N, s(
M)) →
U11#(tt,
M,
N) and
U11#(tt,
M,
N) → plus
#(
N,
M) are consolidated into the rule plus
#(
N, s(
M)) → plus
#(
N,
M) .
This is possible as
- all subterms of U11#(tt, M, N) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in U11#(tt, M, N), but non-replacing in both plus#(N, s(M)) and plus#(N, M)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| plus#(N, s(M)) → U11#(tt, M, N) | plus#(N, s(M)) → plus#(N, M) |
| U11#(tt, M, N) → plus#(N, M) | |
Problem 19: ForwardInstantiation
Dependency Pair Problem
Dependency Pairs
| plus#(N, s(M)) | → | plus#(N, M) |
Rewrite Rules
| U11(tt, M, N) | → | U12(tt, M, N) | | U12(tt, M, N) | → | s(plus(N, M)) |
| U21(tt, M, N) | → | U22(tt, M, N) | | U22(tt, M, N) | → | plus(x(N, M), N) |
| plus(N, 0) | → | N | | plus(N, s(M)) | → | U11(tt, M, N) |
| x(N, 0) | → | 0 | | x(N, s(M)) | → | U21(tt, M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, 0, s, tt, U11, U12, U21, U22, x
Strategy
Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(s) = μ(U11) = μ(U12) = μ(U21) = μ(U22) = {1}
μ(plus) = μ(plus#) = μ(x#) = μ(x) = {1, 2}
Instantiation
For all potential successors l → r of the rule plus
#(
N, s(
M)) → plus
#(
N,
M) on dependency pair chains it holds that:
- plus#(N, M) matches l,
- all variables of plus#(N, M) are embedded in constructor contexts, i.e., each subterm of plus#(N, M) containing a variable is rooted by a constructor symbol.
Thus, plus
#(
N, s(
M)) → plus
#(
N,
M) is replaced by instances determined through the above matching. These instances are:
| plus#(N, s(s(_M))) → plus#(N, s(_M)) |