YES Termination w.r.t. Q proof of Zantema_05_z27.ari

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

0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 QDPOrderProof (⇔, 0 ms)
↳4 QDP
↳5 SemLabProof (⇒, 134 ms)
↳6 QDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 QDP
        ↳10 UsableRulesReductionPairsProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 PisEmptyProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesReductionPairsProof (⇔, 1 ms)
        ↳16 QDP
        ↳17 PisEmptyProof (⇔, 0 ms)
        ↳18 YES
    ↳19 QDP
        ↳20 UsableRulesReductionPairsProof (⇔, 0 ms)
        ↳21 QDP
        ↳22 PisEmptyProof (⇔, 0 ms)
        ↳23 YES
    ↳24 QDP
        ↳25 UsableRulesReductionPairsProof (⇔, 0 ms)
        ↳26 QDP
        ↳27 PisEmptyProof (⇔, 0 ms)
        ↳28 YES
    ↳29 QDP
        ↳30 UsableRulesReductionPairsProof (⇔, 0 ms)
        ↳31 QDP
        ↳32 PisEmptyProof (⇔, 0 ms)
        ↳33 YES
    ↳34 QDP
        ↳35 UsableRulesReductionPairsProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 PisEmptyProof (⇔, 0 ms)
        ↳38 YES
    ↳39 QDP
        ↳40 UsableRulesReductionPairsProof (⇔, 0 ms)
        ↳41 QDP
        ↳42 PisEmptyProof (⇔, 0 ms)
        ↳43 YES
    ↳44 QDP
        ↳45 UsableRulesReductionPairsProof (⇔, 0 ms)
        ↳46 QDP
        ↳47 PisEmptyProof (⇔, 0 ms)
        ↳48 YES

(0) Obligation:

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

f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))

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(0, 1, x) → F(g(x), g(x), x)
F(g(x), y, z) → F(x, y, z)
F(x, g(y), z) → F(x, y, z)
F(x, y, g(z)) → F(x, y, z)

The TRS R consists of the following rules:

f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))

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

(3) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


F(x, y, g(z)) → F(x, y, z)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
F(x1, x2, x3)  =  x3
g(x1)  =  g(x1)

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
g_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(4) Obligation:

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

F(0, 1, x) → F(g(x), g(x), x)
F(g(x), y, z) → F(x, y, z)
F(x, g(y), z) → F(x, y, z)

The TRS R consists of the following rules:

f(0, 1, x) → f(g(x), g(x), x)
f(g(x), y, z) → g(f(x, y, z))
f(x, g(y), z) → g(f(x, y, z))
f(x, y, g(z)) → g(f(x, y, z))

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

(5) SemLabProof (SOUND transformation)

We found the following model for the rules of the TRSs R and P. Interpretation over the domain with elements from 0 to 1.
f: 0
0: 0
1: 1
F: 0
g: x0
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.

(6) Obligation:

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

F.0-1-0(0., 1., x) → F.0-0-0(g.0(x), g.0(x), x)
F.0-0-0(g.0(x), y, z) → F.0-0-0(x, y, z)
F.0-0-1(g.0(x), y, z) → F.0-0-1(x, y, z)
F.0-1-0(g.0(x), y, z) → F.0-1-0(x, y, z)
F.0-1-1(g.0(x), y, z) → F.0-1-1(x, y, z)
F.1-0-0(g.1(x), y, z) → F.1-0-0(x, y, z)
F.1-0-1(g.1(x), y, z) → F.1-0-1(x, y, z)
F.1-1-0(g.1(x), y, z) → F.1-1-0(x, y, z)
F.1-1-1(g.1(x), y, z) → F.1-1-1(x, y, z)
F.0-1-1(0., 1., x) → F.1-1-1(g.1(x), g.1(x), x)
F.0-0-0(x, g.0(y), z) → F.0-0-0(x, y, z)
F.0-0-1(x, g.0(y), z) → F.0-0-1(x, y, z)
F.0-1-0(x, g.1(y), z) → F.0-1-0(x, y, z)
F.0-1-1(x, g.1(y), z) → F.0-1-1(x, y, z)
F.1-0-0(x, g.0(y), z) → F.1-0-0(x, y, z)
F.1-0-1(x, g.0(y), z) → F.1-0-1(x, y, z)
F.1-1-0(x, g.1(y), z) → F.1-1-0(x, y, z)
F.1-1-1(x, g.1(y), z) → F.1-1-1(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 2 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

F.1-1-1(x, g.1(y), z) → F.1-1-1(x, y, z)
F.1-1-1(g.1(x), y, z) → F.1-1-1(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(10) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.1-1-1(x, g.1(y), z) → F.1-1-1(x, y, z)
F.1-1-1(g.1(x), y, z) → F.1-1-1(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.1-1-1(x1, x2, x3)) = x1 + x2 + x3   
POL(g.1(x1)) = x1   

(11) Obligation:

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

(12) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(13) YES

(14) Obligation:

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

F.1-1-0(x, g.1(y), z) → F.1-1-0(x, y, z)
F.1-1-0(g.1(x), y, z) → F.1-1-0(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(15) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.1-1-0(x, g.1(y), z) → F.1-1-0(x, y, z)
F.1-1-0(g.1(x), y, z) → F.1-1-0(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.1-1-0(x1, x2, x3)) = x1 + x2 + x3   
POL(g.1(x1)) = x1   

(16) Obligation:

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

(17) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(18) YES

(19) Obligation:

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

F.1-0-1(x, g.0(y), z) → F.1-0-1(x, y, z)
F.1-0-1(g.1(x), y, z) → F.1-0-1(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(20) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.1-0-1(x, g.0(y), z) → F.1-0-1(x, y, z)
F.1-0-1(g.1(x), y, z) → F.1-0-1(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.1-0-1(x1, x2, x3)) = x1 + x2 + x3   
POL(g.0(x1)) = x1   
POL(g.1(x1)) = x1   

(21) Obligation:

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

(22) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(23) YES

(24) Obligation:

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

F.1-0-0(x, g.0(y), z) → F.1-0-0(x, y, z)
F.1-0-0(g.1(x), y, z) → F.1-0-0(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(25) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.1-0-0(x, g.0(y), z) → F.1-0-0(x, y, z)
F.1-0-0(g.1(x), y, z) → F.1-0-0(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.1-0-0(x1, x2, x3)) = x1 + x2 + x3   
POL(g.0(x1)) = x1   
POL(g.1(x1)) = x1   

(26) Obligation:

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

(27) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(28) YES

(29) Obligation:

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

F.0-1-1(x, g.1(y), z) → F.0-1-1(x, y, z)
F.0-1-1(g.0(x), y, z) → F.0-1-1(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(30) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.0-1-1(x, g.1(y), z) → F.0-1-1(x, y, z)
F.0-1-1(g.0(x), y, z) → F.0-1-1(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.0-1-1(x1, x2, x3)) = x1 + x2 + x3   
POL(g.0(x1)) = x1   
POL(g.1(x1)) = x1   

(31) Obligation:

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

(32) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(33) YES

(34) Obligation:

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

F.0-0-1(x, g.0(y), z) → F.0-0-1(x, y, z)
F.0-0-1(g.0(x), y, z) → F.0-0-1(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(35) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.0-0-1(x, g.0(y), z) → F.0-0-1(x, y, z)
F.0-0-1(g.0(x), y, z) → F.0-0-1(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.0-0-1(x1, x2, x3)) = x1 + x2 + x3   
POL(g.0(x1)) = x1   

(36) Obligation:

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

(37) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(38) YES

(39) Obligation:

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

F.0-0-0(x, g.0(y), z) → F.0-0-0(x, y, z)
F.0-0-0(g.0(x), y, z) → F.0-0-0(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(40) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.0-0-0(x, g.0(y), z) → F.0-0-0(x, y, z)
F.0-0-0(g.0(x), y, z) → F.0-0-0(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.0-0-0(x1, x2, x3)) = x1 + x2 + x3   
POL(g.0(x1)) = x1   

(41) Obligation:

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

(42) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(43) YES

(44) Obligation:

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

F.0-1-0(x, g.1(y), z) → F.0-1-0(x, y, z)
F.0-1-0(g.0(x), y, z) → F.0-1-0(x, y, z)

The TRS R consists of the following rules:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))

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

(45) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F.0-1-0(x, g.1(y), z) → F.0-1-0(x, y, z)
F.0-1-0(g.0(x), y, z) → F.0-1-0(x, y, z)
The following rules are removed from R:

f.0-1-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(g.0(x), y, z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(g.0(x), y, z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, g.0(y), z) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, g.0(y), z) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, g.0(z)) → g.0(f.0-1-0(x, y, z))
f.0-1-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.0-1-0(x1, x2, x3)) = x1 + x2 + x3   
POL(g.0(x1)) = x1   
POL(g.1(x1)) = x1   

(46) Obligation:

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

(47) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(48) YES