NO
Termination w.r.t. Q proof of ../tpdb/TRS/TRCSR/Ex9_Luc06_FR.trs
Termination w.r.t. Q of the following Term Rewriting System could be disproven:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
B → A
F(n__a, X, X) → F(activate(X), b, n__b)
ACTIVATE(n__a) → A
F(n__a, X, X) → B
F(n__a, X, X) → ACTIVATE(X)
ACTIVATE(n__b) → B
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
B → A
F(n__a, X, X) → F(activate(X), b, n__b)
ACTIVATE(n__a) → A
F(n__a, X, X) → B
F(n__a, X, X) → ACTIVATE(X)
ACTIVATE(n__b) → B
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 5 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, X, X) → F(activate(X), b, n__b)
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
Q DP problem:
The TRS P consists of the following rules:
F(n__a, X, X) → F(activate(X), b, n__b)
The TRS R consists of the following rules:
activate(n__a) → a
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule F(n__a, X, X) → F(activate(X), b, n__b) we obtained the following new rules:
F(n__a, n__b, n__b) → F(activate(n__b), b, n__b)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(activate(n__b), b, n__b)
The TRS R consists of the following rules:
activate(n__a) → a
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(activate(n__b), b, n__b)
The TRS R consists of the following rules:
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(n__a, n__b, n__b) → F(activate(n__b), b, n__b) at position [0] we obtained the following new rules:
F(n__a, n__b, n__b) → F(n__b, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(n__b, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)
The TRS R consists of the following rules:
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, b, n__b)
The TRS R consists of the following rules:
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(n__a, n__b, n__b) → F(b, b, n__b) at position [1] we obtained the following new rules:
F(n__a, n__b, n__b) → F(b, n__b, n__b)
F(n__a, n__b, n__b) → F(b, a, n__b)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, a, n__b)
F(n__a, n__b, n__b) → F(b, n__b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(n__a, n__b, n__b) → F(b, a, n__b) at position [1] we obtained the following new rules:
F(n__a, n__b, n__b) → F(b, n__a, n__b)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, n__a, n__b)
F(n__a, n__b, n__b) → F(b, n__b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, n__b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
b → n__b
Used ordering: POLO with Polynomial interpretation [25]:
POL(F(x1, x2, x3)) = 2·x1 + x2 + x3
POL(a) = 1
POL(b) = 1
POL(n__a) = 1
POL(n__b) = 0
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, n__b, n__b)
The TRS R consists of the following rules:
b → a
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [15] to enlarge Q to all left-hand sides of R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
↳ QDP
↳ Rewriting
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, n__b, n__b)
The TRS R consists of the following rules:
b → a
a → n__a
The set Q consists of the following terms:
b
a
We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(n__a, n__b, n__b) → F(b, n__b, n__b) at position [0] we obtained the following new rules:
F(n__a, n__b, n__b) → F(a, n__b, n__b)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(a, n__b, n__b)
The TRS R consists of the following rules:
b → a
a → n__a
The set Q consists of the following terms:
b
a
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(a, n__b, n__b)
The TRS R consists of the following rules:
a → n__a
The set Q consists of the following terms:
b
a
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
b
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(a, n__b, n__b)
The TRS R consists of the following rules:
a → n__a
The set Q consists of the following terms:
a
We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(n__a, n__b, n__b) → F(a, n__b, n__b) at position [0] we obtained the following new rules:
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
The TRS R consists of the following rules:
a → n__a
The set Q consists of the following terms:
a
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
R is empty.
The set Q consists of the following terms:
a
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
a
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ MNOCProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ NonTerminationProof
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
The TRS R consists of the following rules:none
s = F(n__a, n__b, n__b) evaluates to t =F(n__a, n__b, n__b)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from F(n__a, n__b, n__b) to F(n__a, n__b, n__b).