Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 UsableRulesProof (⇔)
↳6 QDP
↳7 Narrowing (⇔)
↳8 QDP
↳9 DependencyGraphProof (⇔)
↳10 QDP
↳11 UsableRulesProof (⇔)
↳12 QDP
↳13 Narrowing (⇔)
↳14 QDP
↳15 DependencyGraphProof (⇔)
↳16 QDP
↳17 Narrowing (⇔)
↳18 QDP
↳19 Narrowing (⇔)
↳20 QDP
↳21 Narrowing (⇔)
↳22 QDP
↳23 DependencyGraphProof (⇔)
↳24 QDP
↳25 Narrowing (⇔)
↳26 QDP
↳27 UsableRulesProof (⇔)
↳28 QDP
↳29 MNOCProof (⇔)
↳30 QDP
↳31 Rewriting (⇔)
↳32 QDP
↳33 DependencyGraphProof (⇔)
↳34 QDP
↳35 UsableRulesProof (⇔)
↳36 QDP
↳37 QReductionProof (⇔)
↳38 QDP
↳39 Instantiation (⇔)
↳40 QDP
↳41 DependencyGraphProof (⇔)
↳42 QDP
↳43 NonTerminationProof (⇔)
↳44 FALSE

(0) Obligation:

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.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, X, X) → F(activate(X), b, n__b)
F(n__a, X, X) → ACTIVATE(X)
F(n__a, X, X) → B
B → A
ACTIVATE(n__a) → A
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.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 5 less nodes.

(4) Obligation:

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.

(5) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(6) Obligation:

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.

(7) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(n__a, X, X) → F(activate(X), b, n__b) at position [0] we obtained the following new rules [LPAR04]:

F(n__a, n__a, n__a) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, b, n__b)

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, n__a, n__a) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, 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.

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, 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.

(11) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, 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.

(13) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(n__a, n__b, n__b) → F(b, b, n__b) at position [0] we obtained the following new rules [LPAR04]:

F(n__a, n__b, n__b) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(n__b, b, n__b)

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__b, n__b) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(n__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.

(15) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__b, n__b) → F(a, 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.

(17) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(n__a, x0, x0) → F(x0, b, n__b) at position [] we obtained the following new rules [LPAR04]:

F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, y0, y0) → F(y0, n__b, n__b)

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, n__b, n__b) → F(a, b, n__b)
F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, y0, y0) → F(y0, 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.

(19) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(n__a, n__b, n__b) → F(a, b, n__b) at position [0] we obtained the following new rules [LPAR04]:

F(n__a, n__b, n__b) → F(n__a, b, n__b)

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, 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.

(21) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(n__a, y0, y0) → F(y0, a, n__b) at position [] we obtained the following new rules [LPAR04]:

F(n__a, y0, y0) → F(y0, n__a, n__b)

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, b, n__b)
F(n__a, y0, y0) → F(y0, n__a, 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.

(23) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, 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.

(25) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(n__a, n__b, n__b) → F(n__a, b, n__b) at position [] we obtained the following new rules [LPAR04]:

F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, 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.

(27) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
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.

(31) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule F(n__a, n__b, n__b) → F(n__a, a, n__b) at position [1] we obtained the following new rules [LPAR04]:

F(n__a, n__b, n__b) → F(n__a, n__a, n__b)

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__a, 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.

(33) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
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.

(35) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
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.

(37) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(n__a, y0, y0) → F(y0, n__b, n__b)
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.

(39) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule F(n__a, y0, y0) → F(y0, n__b, n__b) we obtained the following new rules [LPAR04]:

F(n__a, n__b, n__b) → F(n__b, n__b, n__b)

(40) Obligation:

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)
F(n__a, n__b, n__b) → F(n__b, n__b, n__b)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(41) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(42) Obligation:

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.

(43) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

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:
  • Matcher: [ ]
  • Semiunifier: [ ]



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).



(44) FALSE