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

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

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


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: Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] 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 TRS R. Interpretation over the domain with elements from 0 to 1.f: 0
g: x0
0: 1
1: 0
F: 0
By semantic labelling [SEMLAB] we obtain the following labelled TRS.

(6) Obligation:

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

F.1-0-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.1-0-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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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)
No rules are removed from R.

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

(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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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)
No rules are removed from R.

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

(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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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)
No rules are removed from R.

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

(24) 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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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.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)
No rules are removed from R.

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   

(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) TRUE

(29) 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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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-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)
No rules are removed from R.

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   

(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) TRUE

(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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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)
No rules are removed from R.

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

(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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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)
No rules are removed from R.

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

(44) 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-1(x, y, g.1(z)) → g.0(f.0-1-1(x, y, z))
f.0-1-0(g.0(x), y, z) → g.0(f.0-1-0(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(g.0(x), y, 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.1-0-1(g.1(x), y, z) → g.0(f.1-0-1(x, y, z))
f.0-1-1(x, g.1(y), z) → g.0(f.0-1-1(x, y, z))
f.1-1-0(g.1(x), y, z) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, g.0(y), z) → g.0(f.1-0-1(x, y, z))
f.0-0-0(x, y, g.0(z)) → g.0(f.0-0-0(x, y, z))
f.1-0-0(0., 1., x) → f.0-0-0(g.0(x), g.0(x), x)
f.0-1-1(g.0(x), 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.0-0-1(x, g.0(y), z) → g.0(f.0-0-1(x, y, z))
f.1-0-1(0., 1., x) → f.1-1-1(g.1(x), g.1(x), x)
f.1-1-1(x, g.1(y), z) → g.0(f.1-1-1(x, y, z))
f.0-0-0(g.0(x), y, z) → g.0(f.0-0-0(x, y, z))
f.1-0-0(x, y, g.0(z)) → g.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, g.0(z)) → g.0(f.1-1-0(x, y, z))
f.1-0-1(x, y, g.1(z)) → g.0(f.1-0-1(x, y, z))
f.0-0-1(x, y, g.1(z)) → g.0(f.0-0-1(x, y, z))
f.1-1-1(g.1(x), y, z) → g.0(f.1-1-1(x, y, z))
f.1-1-1(x, y, g.1(z)) → g.0(f.1-1-1(x, y, z))
f.0-1-0(x, g.1(y), z) → g.0(f.0-1-0(x, y, z))
f.1-1-0(x, g.1(y), z) → g.0(f.1-1-0(x, y, z))
f.1-0-0(g.1(x), y, z) → g.0(f.1-0-0(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.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)
No rules are removed from R.

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   

(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) TRUE