MAYBE Termination proof of ../tpdb/TRS/CSR/Ex1_GM99.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(a, b, X) → f(X, X, X)
c → a
c → b

The replacement map contains the following entries:

f: {3}
a: empty set
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(a, b, X) → f(X, X, X)
c → a
c → b

The replacement map contains the following entries:

f: {3}
a: empty set
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(X) → f(X)
c → a
c → b

Q is empty.

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

f(X) → f(X)
c → a
c → b

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

c → a
c → b
Used ordering:
Polynomial interpretation [25]:

POL(a) = 1   
POL(b) = 1   
POL(c) = 2   
POL(f(x1)) = 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(X) → f(X)

Q is empty.

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

The TRS R 2 is

f(X) → f(X)

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(X) → f(X)

The set Q consists of the following terms:

f(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:

F(X) → F(X)

The TRS R consists of the following rules:

f(X) → f(X)

The set Q consists of the following terms:

f(x0)

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(X) → F(X)

The TRS R consists of the following rules:

f(X) → f(X)

The set Q consists of the following terms:

f(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
    ↳ 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(X) → F(X)

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

f(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.

f(x0)



↳ 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(X) → F(X)

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(X) → F(X)

The TRS R consists of the following rules:none


s = F(X) evaluates to t =F(X)

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(X) to F(X).




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(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a

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(aInact, bInact, X) → F(X, X, X)
A(bInact) → B
C → A
C → B
A(aInact) → A

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a

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(aInact, bInact, X) → F(X, X, X)
A(bInact) → B
C → A
C → B
A(aInact) → A

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → 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 4 less nodes.

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

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

F(aInact, bInact, X) → F(X, X, X)

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a

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 narrowing to the left:

The TRS P consists of the following rules:

F(aInact, bInact, X) → F(X, X, X)

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a


s = F(c, c, X) evaluates to t =F(X, X, X)

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



Rewriting sequence

F(c, c, c) → F(c, b, c)
with rule c → b at position [1] and matcher [ ]

F(c, b, c) → F(c, bInact, c)
with rule b → bInact at position [1] and matcher [ ]

F(c, bInact, c) → F(a, bInact, c)
with rule c → a at position [0] and matcher [ ]

F(a, bInact, c) → F(aInact, bInact, c)
with rule a → aInact at position [0] and matcher [ ]

F(aInact, bInact, c) → F(c, c, c)
with rule F(aInact, bInact, X) → F(X, X, X)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




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, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(X, X, mark(X))
cActive → a
cActive → b

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:

FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))
MARK(f(x1, x2, x3)) → FACTIVE(x1, x2, mark(x3))
MARK(c) → CACTIVE
FACTIVE(a, b, X) → MARK(X)
MARK(f(x1, x2, x3)) → MARK(x3)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(X, X, mark(X))
cActive → a
cActive → b

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:

FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))
MARK(f(x1, x2, x3)) → FACTIVE(x1, x2, mark(x3))
MARK(c) → CACTIVE
FACTIVE(a, b, X) → MARK(X)
MARK(f(x1, x2, x3)) → MARK(x3)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(X, X, mark(X))
cActive → a
cActive → b

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.

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

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

MARK(f(x1, x2, x3)) → FACTIVE(x1, x2, mark(x3))
FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))
MARK(f(x1, x2, x3)) → MARK(x3)
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(X, X, mark(X))
cActive → a
cActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


MARK(f(x1, x2, x3)) → FACTIVE(x1, x2, mark(x3))
MARK(f(x1, x2, x3)) → MARK(x3)
The remaining pairs can at least be oriented weakly.

FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))
FACTIVE(a, b, X) → MARK(X)
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
M( b ) =
/0\
\0/

M( mark(x1) ) =
/0\
\0/
+
/01\
\01/
·x1

M( a ) =
/0\
\0/

M( f(x1, ..., x3) ) =
/0\
\1/
+
/00\
\00/
·x1+
/00\
\00/
·x2+
/00\
\01/
·x3

M( cActive ) =
/1\
\1/

M( fActive(x1, ..., x3) ) =
/0\
\1/
+
/00\
\00/
·x1+
/00\
\00/
·x2+
/01\
\01/
·x3

M( c ) =
/0\
\1/

Tuple symbols:
M( FACTIVE(x1, ..., x3) ) = 0+
[0,0]
·x1+
[0,0]
·x2+
[0,1]
·x3

M( MARK(x1) ) = 0+
[0,1]
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

cActive → b
cActive → c
mark(f(x1, x2, x3)) → fActive(x1, x2, mark(x3))
mark(b) → b
cActive → a
mark(c) → cActive
fActive(x1, x2, x3) → f(x1, x2, x3)
fActive(a, b, X) → fActive(X, X, mark(X))
mark(a) → a



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

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

FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))
FACTIVE(a, b, X) → MARK(X)

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(X, X, mark(X))
cActive → a
cActive → b

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.

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

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

FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(X, X, mark(X))
cActive → a
cActive → b

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 narrowing to the left:

The TRS P consists of the following rules:

FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))

The TRS R consists of the following rules:

mark(f(x1, x2, x3)) → fActive(x1, x2, mark(x3))
fActive(x1, x2, x3) → f(x1, x2, x3)
mark(c) → cActive
cActive → c
mark(a) → a
mark(b) → b
fActive(a, b, X) → fActive(X, X, mark(X))
cActive → a
cActive → b


s = FACTIVE(mark(cActive), mark(cActive), mark(mark(cActive))) evaluates to t =FACTIVE(mark(cActive), mark(cActive), mark(mark(cActive)))

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



Rewriting sequence

FACTIVE(mark(cActive), mark(cActive), mark(mark(cActive))) → FACTIVE(mark(cActive), mark(cActive), mark(mark(c)))
with rule cActive → c at position [2,0,0] and matcher [ ]

FACTIVE(mark(cActive), mark(cActive), mark(mark(c))) → FACTIVE(mark(cActive), mark(cActive), mark(cActive))
with rule mark(c) → cActive at position [2,0] and matcher [ ]

FACTIVE(mark(cActive), mark(cActive), mark(cActive)) → FACTIVE(mark(cActive), mark(cActive), mark(c))
with rule cActive → c at position [2,0] and matcher [ ]

FACTIVE(mark(cActive), mark(cActive), mark(c)) → FACTIVE(mark(cActive), mark(cActive), cActive)
with rule mark(c) → cActive at position [2] and matcher [ ]

FACTIVE(mark(cActive), mark(cActive), cActive) → FACTIVE(mark(cActive), mark(b), cActive)
with rule cActive → b at position [1,0] and matcher [ ]

FACTIVE(mark(cActive), mark(b), cActive) → FACTIVE(mark(cActive), b, cActive)
with rule mark(b) → b at position [1] and matcher [ ]

FACTIVE(mark(cActive), b, cActive) → FACTIVE(mark(a), b, cActive)
with rule cActive → a at position [0,0] and matcher [ ]

FACTIVE(mark(a), b, cActive) → FACTIVE(a, b, cActive)
with rule mark(a) → a at position [0] and matcher [ ]

FACTIVE(a, b, cActive) → FACTIVE(cActive, cActive, mark(cActive))
with rule FACTIVE(a, b, X') → FACTIVE(X', X', mark(X')) at position [] and matcher [X' / cActive]

FACTIVE(cActive, cActive, mark(cActive)) → FACTIVE(cActive, b, mark(cActive))
with rule cActive → b at position [1] and matcher [ ]

FACTIVE(cActive, b, mark(cActive)) → FACTIVE(a, b, mark(cActive))
with rule cActive → a at position [0] and matcher [ ]

FACTIVE(a, b, mark(cActive)) → FACTIVE(mark(cActive), mark(cActive), mark(mark(cActive)))
with rule FACTIVE(a, b, X) → FACTIVE(X, X, mark(X))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




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(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a

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(aInact, bInact, X) → F(X, X, X)
A(bInact) → B
C → A
C → B
A(aInact) → A

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a

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(aInact, bInact, X) → F(X, X, X)
A(bInact) → B
C → A
C → B
A(aInact) → A

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → 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 4 less nodes.

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

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

F(aInact, bInact, X) → F(X, X, X)

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a

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 narrowing to the left:

The TRS P consists of the following rules:

F(aInact, bInact, X) → F(X, X, X)

The TRS R consists of the following rules:

f(aInact, bInact, X) → f(X, X, X)
c → a
c → b
a(x) → x
b → bInact
a(bInact) → b
a → aInact
a(aInact) → a


s = F(c, c, X) evaluates to t =F(X, X, X)

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



Rewriting sequence

F(c, c, c) → F(c, b, c)
with rule c → b at position [1] and matcher [ ]

F(c, b, c) → F(c, bInact, c)
with rule b → bInact at position [1] and matcher [ ]

F(c, bInact, c) → F(a, bInact, c)
with rule c → a at position [0] and matcher [ ]

F(a, bInact, c) → F(aInact, bInact, c)
with rule a → aInact at position [0] and matcher [ ]

F(aInact, bInact, c) → F(c, c, c)
with rule F(aInact, bInact, X) → F(X, X, X)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




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(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
proper(a) → ok(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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(f(x1, x2, x3)) → ACTIVE(x3)
PROPER(f(x1, x2, x3)) → PROPER(x1)
TOP(mark(x)) → PROPER(x)
PROPER(f(x1, x2, x3)) → PROPER(x3)
ACTIVE(f(a, b, X)) → F(X, X, X)
TOP(ok(x)) → ACTIVE(x)
ACTIVE(f(x1, x2, x3)) → F(x1, x2, active(x3))
TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))
PROPER(f(x1, x2, x3)) → PROPER(x2)
PROPER(f(x1, x2, x3)) → F(proper(x1), proper(x2), proper(x3))
F(x1, x2, mark(x3)) → F(x1, x2, x3)
F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
proper(a) → ok(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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(f(x1, x2, x3)) → ACTIVE(x3)
PROPER(f(x1, x2, x3)) → PROPER(x1)
TOP(mark(x)) → PROPER(x)
PROPER(f(x1, x2, x3)) → PROPER(x3)
ACTIVE(f(a, b, X)) → F(X, X, X)
TOP(ok(x)) → ACTIVE(x)
ACTIVE(f(x1, x2, x3)) → F(x1, x2, active(x3))
TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))
PROPER(f(x1, x2, x3)) → PROPER(x2)
PROPER(f(x1, x2, x3)) → F(proper(x1), proper(x2), proper(x3))
F(x1, x2, mark(x3)) → F(x1, x2, x3)
F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
proper(a) → ok(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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 4 SCCs with 5 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

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

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

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
proper(a) → ok(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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

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

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

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

active(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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

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

F(ok(x1), ok(x2), ok(x3)) → F(x1, x2, x3)
F(x1, x2, mark(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
                ↳ UsableRulesProof
              ↳ QDP
              ↳ QDP

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

PROPER(f(x1, x2, x3)) → 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(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
proper(a) → ok(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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

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

PROPER(f(x1, x2, x3)) → 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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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(c)
active(f(x0, x1, x2))
proper(f(x0, x1, x2))
proper(a)
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

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

PROPER(f(x1, x2, x3)) → 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(x0, x1, mark(x2))
f(ok(x0), ok(x1), ok(x2))

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

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

ACTIVE(f(x1, x2, x3)) → ACTIVE(x3)

The TRS R consists of the following rules:

active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
proper(a) → ok(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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

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

ACTIVE(f(x1, x2, x3)) → ACTIVE(x3)

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

active(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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(c)
active(f(x0, x1, x2))
proper(f(x0, x1, x2))
proper(a)
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

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

ACTIVE(f(x1, x2, x3)) → ACTIVE(x3)

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

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

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

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(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
proper(f(x1, x2, x3)) → f(proper(x1), proper(x2), proper(x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
proper(a) → ok(a)
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(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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

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(a) → ok(a)
proper(b) → ok(b)
proper(c) → ok(c)
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))

The set Q consists of the following terms:

active(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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
                ↳ 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(a) → ok(a)
proper(b) → ok(b)
proper(c) → ok(c)
f(x1, x2, mark(x3)) → mark(f(x1, x2, x3))
f(ok(x1), ok(x2), ok(x3)) → ok(f(x1, x2, x3))
active(f(a, b, X)) → mark(f(X, X, X))
active(c) → mark(a)
active(c) → mark(b)
active(f(x1, x2, x3)) → f(x1, x2, active(x3))

The set Q consists of the following terms:

active(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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(f(x0, x1, x2))) → TOP(f(x0, x1, active(x2)))
TOP(ok(c)) → TOP(mark(b))
TOP(ok(f(a, b, x0))) → TOP(mark(f(x0, x0, x0)))
TOP(ok(c)) → TOP(mark(a))



↳ 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
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

active(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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(b)) → TOP(ok(b))
TOP(mark(c)) → TOP(ok(c))
TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2)))
TOP(mark(a)) → TOP(ok(a))



↳ 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
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ DependencyGraphProof

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

active(c)
active(f(x0, x1, x2))
f(x0, x1, mark(x2))
proper(f(x0, x1, x2))
f(ok(x0), ok(x1), ok(x2))
proper(a)
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 5 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
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ DependencyGraphProof
                                  ↳ QDP

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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