MAYBE Termination proof of ../tpdb/TRS/CSR/Ex24_GM04.trs
Termination of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(X, g(X), Y) → f(Y, Y, Y)
g(b) → c
b → c

The replacement map contains the following entries:

f: empty set
g: {1}
b: empty set
c: empty set


↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

f(X, g(X), Y) → f(Y, Y, Y)
g(b) → c
b → c

The replacement map contains the following entries:

f: empty set
g: {1}
b: empty set
c: empty set

We applied the Lucas [26] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

f → f
g(b) → c
b → c

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

f → f
g(b) → c
b → c

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

g(b) → c
b → c
Used ordering:
Polynomial interpretation [25]:

POL(b) = 2   
POL(c) = 1   
POL(f) = 0   
POL(g(x1)) = 2 + 2·x1   




↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ AAECC Innermost
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

f → f

Q is empty.

We have applied [19,8] to switch to innermost. The TRS R 1 is none

The TRS R 2 is

f → f

The signature Sigma is {f}

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ AAECC Innermost
            ↳ QTRS
              ↳ DependencyPairsProof
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

f → f

The set Q consists of the following terms:

f


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F → F

The TRS R consists of the following rules:

f → f

The set Q consists of the following terms:

f

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

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ AAECC Innermost
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

F → F

The TRS R consists of the following rules:

f → f

The set Q consists of the following terms:

f

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.

↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ AAECC Innermost
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
                    ↳ QDP
                      ↳ QReductionProof
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

F → F

R is empty.
The set Q consists of the following terms:

f

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.

f



↳ CSR
  ↳ Lucas-Transformation
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ AAECC Innermost
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ UsableRulesProof
                    ↳ QDP
                      ↳ QReductionProof
                        ↳ QDP
                          ↳ NonTerminationProof
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

F → F

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 → F

The TRS R consists of the following rules:none


s = F evaluates to t =F

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from F to F.




We applied the Zantema [34] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(x1)

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:

F(X, gInact(X), Y) → F(a(Y), a(Y), a(Y))
A(gInact(x1)) → G(x1)
F(X, gInact(X), Y) → A(Y)

The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(x1)

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

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

F(X, gInact(X), Y) → F(a(Y), a(Y), a(Y))
A(gInact(x1)) → G(x1)
F(X, gInact(X), Y) → A(Y)

The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(x1)

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 2 less nodes.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

F(X, gInact(X), Y) → F(a(Y), a(Y), a(Y))

The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Incomplete Giesl Middeldorp [11] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, x3)
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(g(x1)) → gActive(mark(x1))
gActive(x1) → g(x1)
mark(b) → bActive
bActive → b
mark(c) → c
fActive(X, g(X), Y) → fActive(Y, Y, Y)
gActive(b) → c
bActive → c

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:

MARK(g(x1)) → GACTIVE(mark(x1))
MARK(b) → BACTIVE
MARK(g(x1)) → MARK(x1)
MARK(f(x1, x2, x3)) → FACTIVE(x1, x2, x3)
FACTIVE(X, g(X), Y) → FACTIVE(Y, Y, Y)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, x3)
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(g(x1)) → gActive(mark(x1))
gActive(x1) → g(x1)
mark(b) → bActive
bActive → b
mark(c) → c
fActive(X, g(X), Y) → fActive(Y, Y, Y)
gActive(b) → c
bActive → c

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

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

MARK(g(x1)) → GACTIVE(mark(x1))
MARK(b) → BACTIVE
MARK(g(x1)) → MARK(x1)
MARK(f(x1, x2, x3)) → FACTIVE(x1, x2, x3)
FACTIVE(X, g(X), Y) → FACTIVE(Y, Y, Y)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, x3)
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(g(x1)) → gActive(mark(x1))
gActive(x1) → g(x1)
mark(b) → bActive
bActive → b
mark(c) → c
fActive(X, g(X), Y) → fActive(Y, Y, Y)
gActive(b) → c
bActive → c

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 3 less nodes.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

FACTIVE(X, g(X), Y) → FACTIVE(Y, Y, Y)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, x3)
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(g(x1)) → gActive(mark(x1))
gActive(x1) → g(x1)
mark(b) → bActive
bActive → b
mark(c) → c
fActive(X, g(X), Y) → fActive(Y, Y, Y)
gActive(b) → c
bActive → c

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

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

MARK(g(x1)) → MARK(x1)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, x3)
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(g(x1)) → gActive(mark(x1))
gActive(x1) → g(x1)
mark(b) → bActive
bActive → b
mark(c) → c
fActive(X, g(X), Y) → fActive(Y, Y, Y)
gActive(b) → c
bActive → c

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.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QDPSizeChangeProof
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation

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

MARK(g(x1)) → MARK(x1)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:


We applied the Improved Ferreira Ribeiro [5,11] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
  ↳ Complete Giesl Middeldorp-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(a(x1))

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:

F(X, gInact(X), Y) → F(a(Y), a(Y), a(Y))
A(gInact(x1)) → A(x1)
A(gInact(x1)) → G(a(x1))
F(X, gInact(X), Y) → A(Y)

The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(a(x1))

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

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
  ↳ Complete Giesl Middeldorp-Transformation

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

F(X, gInact(X), Y) → F(a(Y), a(Y), a(Y))
A(gInact(x1)) → A(x1)
A(gInact(x1)) → G(a(x1))
F(X, gInact(X), Y) → A(Y)

The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(a(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
  ↳ Complete Giesl Middeldorp-Transformation

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

A(gInact(x1)) → A(x1)

The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(a(x1))

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.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QDPSizeChangeProof
              ↳ QDP
  ↳ Complete Giesl Middeldorp-Transformation

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

A(gInact(x1)) → A(x1)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
  ↳ Complete Giesl Middeldorp-Transformation

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

F(X, gInact(X), Y) → F(a(Y), a(Y), a(Y))

The TRS R consists of the following rules:

f(X, gInact(X), Y) → f(a(Y), a(Y), a(Y))
g(b) → c
b → c
a(x) → x
g(x1) → gInact(x1)
a(gInact(x1)) → g(a(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Complete Giesl Middeldorp [11] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ACTIVE(g(x1)) → ACTIVE(x1)
TOP(mark(x)) → PROPER(x)
PROPER(f(x1, x2, x3)) → PROPER(x1)
PROPER(g(x1)) → G(proper(x1))
ACTIVE(f(X, g(X), Y)) → F(Y, Y, Y)
PROPER(g(x1)) → PROPER(x1)
PROPER(f(x1, x2, x3)) → PROPER(x3)
TOP(ok(x)) → ACTIVE(x)
G(mark(x1)) → G(x1)
ACTIVE(g(x1)) → G(active(x1))
TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))
PROPER(f(x1, x2, x3)) → PROPER(x2)
G(ok(x1)) → G(x1)
PROPER(f(x1, x2, x3)) → F(proper(x1), proper(x2), proper(x3))
F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)

The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof

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

ACTIVE(g(x1)) → ACTIVE(x1)
TOP(mark(x)) → PROPER(x)
PROPER(f(x1, x2, x3)) → PROPER(x1)
PROPER(g(x1)) → G(proper(x1))
ACTIVE(f(X, g(X), Y)) → F(Y, Y, Y)
PROPER(g(x1)) → PROPER(x1)
PROPER(f(x1, x2, x3)) → PROPER(x3)
TOP(ok(x)) → ACTIVE(x)
G(mark(x1)) → G(x1)
ACTIVE(g(x1)) → G(active(x1))
TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))
PROPER(f(x1, x2, x3)) → PROPER(x2)
G(ok(x1)) → G(x1)
PROPER(f(x1, x2, x3)) → F(proper(x1), proper(x2), proper(x3))
F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)

The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 5 SCCs with 6 less nodes.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

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

G(mark(x1)) → G(x1)
G(ok(x1)) → G(x1)

The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

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

G(mark(x1)) → G(x1)
G(ok(x1)) → G(x1)

R is empty.
The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

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

G(mark(x1)) → G(x1)
G(ok(x1)) → G(x1)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

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

F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)

The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

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

F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)

R is empty.
The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

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

F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP

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

PROPER(f(x1, x2, x3)) → PROPER(x1)
PROPER(g(x1)) → PROPER(x1)
PROPER(f(x1, x2, x3)) → PROPER(x3)
PROPER(f(x1, x2, x3)) → PROPER(x2)

The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
              ↳ QDP
              ↳ QDP

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

PROPER(f(x1, x2, x3)) → PROPER(x1)
PROPER(g(x1)) → PROPER(x1)
PROPER(f(x1, x2, x3)) → PROPER(x3)
PROPER(f(x1, x2, x3)) → PROPER(x2)

R is empty.
The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
active(g(x0))
proper(g(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

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

PROPER(f(x1, x2, x3)) → PROPER(x1)
PROPER(g(x1)) → PROPER(x1)
PROPER(f(x1, x2, x3)) → PROPER(x2)
PROPER(f(x1, x2, x3)) → PROPER(x3)

R is empty.
The set Q consists of the following terms:

f(ok(x0), ok(x1), ok(x2))
g(mark(x0))
g(ok(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP

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

ACTIVE(g(x1)) → ACTIVE(x1)

The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
              ↳ QDP

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

ACTIVE(g(x1)) → ACTIVE(x1)

R is empty.
The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
proper(g(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ QDP

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

ACTIVE(g(x1)) → ACTIVE(x1)

R is empty.
The set Q consists of the following terms:

g(mark(x0))
g(ok(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof

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

TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))

The TRS R consists of the following rules:

active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(g(x1)) → g(active(x1))
g(mark(x1)) → mark(g(x1))
proper(g(x1)) → g(proper(x1))
g(ok(x1)) → ok(g(x1))
proper(b) → ok(b)
proper(c) → ok(c)
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof

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

TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))

The TRS R consists of the following rules:

proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
proper(g(x1)) → g(proper(x1))
proper(b) → ok(b)
proper(c) → ok(c)
g(mark(x1)) → mark(g(x1))
g(ok(x1)) → ok(g(x1))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
active(g(x1)) → g(active(x1))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)
top(mark(x0))
top(ok(x0))

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.

top(mark(x0))
top(ok(x0))



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing

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

TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))

The TRS R consists of the following rules:

proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
proper(g(x1)) → g(proper(x1))
proper(b) → ok(b)
proper(c) → ok(c)
g(mark(x1)) → mark(g(x1))
g(ok(x1)) → ok(g(x1))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
active(g(x1)) → g(active(x1))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(ok(x)) → TOP(active(x)) at position [0] we obtained the following new rules:

TOP(ok(b)) → TOP(mark(c))
TOP(ok(f(x0, g(x0), x1))) → TOP(mark(f(x1, x1, x1)))
TOP(ok(g(x0))) → TOP(g(active(x0)))
TOP(ok(g(b))) → TOP(mark(c))



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing

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

TOP(ok(g(b))) → TOP(mark(c))
TOP(ok(g(x0))) → TOP(g(active(x0)))
TOP(ok(b)) → TOP(mark(c))
TOP(mark(x)) → TOP(proper(x))
TOP(ok(f(x0, g(x0), x1))) → TOP(mark(f(x1, x1, x1)))

The TRS R consists of the following rules:

proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
proper(g(x1)) → g(proper(x1))
proper(b) → ok(b)
proper(c) → ok(c)
g(mark(x1)) → mark(g(x1))
g(ok(x1)) → ok(g(x1))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
active(g(x1)) → g(active(x1))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(mark(x)) → TOP(proper(x)) at position [0] we obtained the following new rules:

TOP(mark(g(x0))) → TOP(g(proper(x0)))
TOP(mark(b)) → TOP(ok(b))
TOP(mark(c)) → TOP(ok(c))
TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2)))



↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ DependencyGraphProof

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

TOP(mark(g(x0))) → TOP(g(proper(x0)))
TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2)))
TOP(ok(g(x0))) → TOP(g(active(x0)))
TOP(ok(g(b))) → TOP(mark(c))
TOP(ok(b)) → TOP(mark(c))
TOP(mark(b)) → TOP(ok(b))
TOP(mark(c)) → TOP(ok(c))
TOP(ok(f(x0, g(x0), x1))) → TOP(mark(f(x1, x1, x1)))

The TRS R consists of the following rules:

proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
proper(g(x1)) → g(proper(x1))
proper(b) → ok(b)
proper(c) → ok(c)
g(mark(x1)) → mark(g(x1))
g(ok(x1)) → ok(g(x1))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
active(g(x1)) → g(active(x1))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ CSR
  ↳ Lucas-Transformation
  ↳ Zantema-Transformation
  ↳ Incomplete Giesl Middeldorp-Transformation
  ↳ Improved Ferreira Ribeiro-Transformation
  ↳ Complete Giesl Middeldorp-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP

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

TOP(mark(g(x0))) → TOP(g(proper(x0)))
TOP(ok(g(x0))) → TOP(g(active(x0)))
TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2)))
TOP(ok(f(x0, g(x0), x1))) → TOP(mark(f(x1, x1, x1)))

The TRS R consists of the following rules:

proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
proper(g(x1)) → g(proper(x1))
proper(b) → ok(b)
proper(c) → ok(c)
g(mark(x1)) → mark(g(x1))
g(ok(x1)) → ok(g(x1))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(f(X, g(X), Y)) → mark(f(Y, Y, Y))
active(g(b)) → mark(c)
active(b) → mark(c)
active(g(x1)) → g(active(x1))

The set Q consists of the following terms:

active(f(x0, g(x0), x1))
active(b)
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
active(g(x0))
g(mark(x0))
proper(g(x0))
g(ok(x0))
proper(b)
proper(c)

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