Termination w.r.t. Q proof of Secret_07_TRS

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

0 QTRS

↳1 DependencyPairsProof (⇔, 0 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 QDP

        ↳6 UsableRulesProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 MRRProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 DependencyGraphProof (⇔, 0 ms)

        ↳11 AND

            ↳12 QDP

                ↳13 TransformationProof (⇔, 0 ms)

                ↳14 QDP

                ↳15 DependencyGraphProof (⇔, 0 ms)

                ↳16 TRUE

            ↳17 QDP

                ↳18 TransformationProof (⇔, 0 ms)

                ↳19 QDP

                ↳20 TransformationProof (⇔, 0 ms)

                ↳21 QDP

                ↳22 TransformationProof (⇔, 0 ms)

                ↳23 QDP

                ↳24 TransformationProof (⇔, 0 ms)

                ↳25 QDP

                ↳26 DependencyGraphProof (⇔, 0 ms)

                ↳27 QDP

                ↳28 TransformationProof (⇔, 0 ms)

                ↳29 QDP

                ↳30 DependencyGraphProof (⇔, 0 ms)

                ↳31 QDP

                ↳32 TransformationProof (⇔, 0 ms)

                ↳33 QDP

                ↳34 DependencyGraphProof (⇔, 0 ms)

                ↳35 QDP

                ↳36 SplitQDPProof (⇔, 0 ms)

                ↳37 AND

                    ↳38 QDP

                        ↳39 SemLabProof (⇒, 0 ms)

                        ↳40 QDP

                        ↳41 DependencyGraphProof (⇔, 0 ms)

                        ↳42 QDP

                        ↳43 UsableRulesReductionPairsProof (⇔, 0 ms)

                        ↳44 QDP

                        ↳45 MRRProof (⇔, 0 ms)

                        ↳46 QDP

                        ↳47 PisEmptyProof (⇒, 0 ms)

                        ↳48 TRUE

                    ↳49 QDP

                        ↳50 UsableRulesReductionPairsProof (⇔, 0 ms)

                        ↳51 QDP

                        ↳52 RFCMatchBoundsDPProof (⇔, 5 ms)

                        ↳53 YES

    ↳54 QDP

        ↳55 TransformationProof (⇔, 0 ms)

        ↳56 QDP

        ↳57 SplitQDPProof (⇔, 0 ms)

        ↳58 AND

            ↳59 QDP

                ↳60 SemLabProof (⇒, 0 ms)

                ↳61 QDP

                ↳62 DependencyGraphProof (⇔, 0 ms)

                ↳63 QDP

                ↳64 UsableRulesReductionPairsProof (⇔, 0 ms)

                ↳65 QDP

                ↳66 PisEmptyProof (⇒, 0 ms)

                ↳67 TRUE

            ↳68 QDP

                ↳69 QDPOrderProof (⇔, 0 ms)

                ↳70 QDP

                ↳71 PisEmptyProof (⇔, 0 ms)

                ↳72 YES

(0) Obligation:

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

g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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:

G(c, g(c, x)) → G(e, g(d, x))
G(c, g(c, x)) → G(d, x)
G(d, g(d, x)) → G(c, g(e, x))
G(d, g(d, x)) → G(e, x)
G(e, g(e, x)) → G(d, g(c, x))
G(e, g(e, x)) → G(c, x)
F(g(x, y)) → G(y, g(f(f(x)), a))
F(g(x, y)) → G(f(f(x)), a)
F(g(x, y)) → F(f(x))
F(g(x, y)) → F(x)
G(x, g(y, g(x, y))) → G(a, g(x, g(y, b)))
G(x, g(y, g(x, y))) → G(x, g(y, b))
G(x, g(y, g(x, y))) → G(y, b)

The TRS R consists of the following rules:

g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

G(e, g(e, x)) → G(d, g(c, x))
G(d, g(d, x)) → G(c, g(e, x))
G(c, g(c, x)) → G(e, g(d, x))
G(e, g(e, x)) → G(c, x)
G(c, g(c, x)) → G(d, x)
G(d, g(d, x)) → G(e, x)
G(x, g(y, g(x, y))) → G(a, g(x, g(y, b)))
G(x, g(y, g(x, y))) → G(x, g(y, b))

The TRS R consists of the following rules:

g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(6) UsableRulesProof (EQUIVALENT transformation)

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

(7) Obligation:

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

G(e, g(e, x)) → G(d, g(c, x))
G(d, g(d, x)) → G(c, g(e, x))
G(c, g(c, x)) → G(e, g(d, x))
G(e, g(e, x)) → G(c, x)
G(c, g(c, x)) → G(d, x)
G(d, g(d, x)) → G(e, x)
G(x, g(y, g(x, y))) → G(a, g(x, g(y, b)))
G(x, g(y, g(x, y))) → G(x, g(y, b))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(8) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

G(e, g(e, x)) → G(c, x)
G(c, g(c, x)) → G(d, x)
G(d, g(d, x)) → G(e, x)
G(x, g(y, g(x, y))) → G(x, g(y, b))

Used ordering: Polynomial interpretation [POLO]:

POL(G(x₁, x₂)) = 2·x₁ + x₂
POL(a) = 0
POL(b) = 0
POL(c) = 2
POL(d) = 2
POL(e) = 2
POL(g(x₁, x₂)) = 1 + 2·x₁ + x₂

(9) Obligation:

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

G(e, g(e, x)) → G(d, g(c, x))
G(d, g(d, x)) → G(c, g(e, x))
G(c, g(c, x)) → G(e, g(d, x))
G(x, g(y, g(x, y))) → G(a, g(x, g(y, b)))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(10) DependencyGraphProof (EQUIVALENT transformation)

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

(11) Complex Obligation (AND)

(12) Obligation:

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

G(x, g(y, g(x, y))) → G(a, g(x, g(y, b)))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(13) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule G(x, g(y, g(x, y))) → G(a, g(x, g(y, b))) we obtained the following new rules [LPAR04]:

G(a, g(x1, g(a, x1))) → G(a, g(a, g(x1, b))) → G(a, g(x1, g(a, x1))) → G(a, g(a, g(x1, b)))

(14) Obligation:

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

G(a, g(x1, g(a, x1))) → G(a, g(a, g(x1, b)))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(15) DependencyGraphProof (EQUIVALENT transformation)

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

(16) TRUE

(17) Obligation:

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

G(d, g(d, x)) → G(c, g(e, x))
G(c, g(c, x)) → G(e, g(d, x))
G(e, g(e, x)) → G(d, g(c, x))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(18) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule G(d, g(d, x)) → G(c, g(e, x)) at position [1] we obtained the following new rules [LPAR04]:

G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0))) → G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(d, g(d, g(x1, g(e, x1)))) → G(c, g(a, g(e, g(x1, b)))) → G(d, g(d, g(x1, g(e, x1)))) → G(c, g(a, g(e, g(x1, b))))

(19) Obligation:

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

G(c, g(c, x)) → G(e, g(d, x))
G(e, g(e, x)) → G(d, g(c, x))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(d, g(d, g(x1, g(e, x1)))) → G(c, g(a, g(e, g(x1, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(20) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule G(c, g(c, x)) → G(e, g(d, x)) at position [1] we obtained the following new rules [LPAR04]:

G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0))) → G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(c, g(c, g(x1, g(d, x1)))) → G(e, g(a, g(d, g(x1, b)))) → G(c, g(c, g(x1, g(d, x1)))) → G(e, g(a, g(d, g(x1, b))))

(21) Obligation:

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

G(e, g(e, x)) → G(d, g(c, x))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(d, g(d, g(x1, g(e, x1)))) → G(c, g(a, g(e, g(x1, b))))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(c, g(c, g(x1, g(d, x1)))) → G(e, g(a, g(d, g(x1, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(22) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule G(e, g(e, x)) → G(d, g(c, x)) at position [1] we obtained the following new rules [LPAR04]:

G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0))) → G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b)))) → G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b))))

(23) Obligation:

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

G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(d, g(d, g(x1, g(e, x1)))) → G(c, g(a, g(e, g(x1, b))))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(c, g(c, g(x1, g(d, x1)))) → G(e, g(a, g(d, g(x1, b))))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(24) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule G(d, g(d, g(x1, g(e, x1)))) → G(c, g(a, g(e, g(x1, b)))) at position [1] we obtained the following new rules [LPAR04]:

G(d, g(d, g(e, g(e, e)))) → G(c, g(a, g(d, g(c, b)))) → G(d, g(d, g(e, g(e, e)))) → G(c, g(a, g(d, g(c, b))))

(25) Obligation:

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

G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(c, g(c, g(x1, g(d, x1)))) → G(e, g(a, g(d, g(x1, b))))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b))))
G(d, g(d, g(e, g(e, e)))) → G(c, g(a, g(d, g(c, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(26) DependencyGraphProof (EQUIVALENT transformation)

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

(27) Obligation:

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

G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(c, g(c, g(x1, g(d, x1)))) → G(e, g(a, g(d, g(x1, b))))
G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(28) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule G(c, g(c, g(x1, g(d, x1)))) → G(e, g(a, g(d, g(x1, b)))) at position [1] we obtained the following new rules [LPAR04]:

G(c, g(c, g(d, g(d, d)))) → G(e, g(a, g(c, g(e, b)))) → G(c, g(c, g(d, g(d, d)))) → G(e, g(a, g(c, g(e, b))))

(29) Obligation:

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

G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b))))
G(c, g(c, g(d, g(d, d)))) → G(e, g(a, g(c, g(e, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(30) DependencyGraphProof (EQUIVALENT transformation)

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

(31) Obligation:

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

G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(32) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule G(e, g(e, g(x1, g(c, x1)))) → G(d, g(a, g(c, g(x1, b)))) at position [1] we obtained the following new rules [LPAR04]:

G(e, g(e, g(c, g(c, c)))) → G(d, g(a, g(e, g(d, b)))) → G(e, g(e, g(c, g(c, c)))) → G(d, g(a, g(e, g(d, b))))

(33) Obligation:

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

G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(e, g(e, g(c, g(c, c)))) → G(d, g(a, g(e, g(d, b))))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(34) DependencyGraphProof (EQUIVALENT transformation)

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

(35) Obligation:

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

G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(36) SplitQDPProof (EQUIVALENT transformation)

We show in the first subproof that some pairs and rules can be removed, afterwards, we continue with the remaining DP-Problem

(37) Complex Obligation (AND)

(38) Obligation:

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

G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))

The TRS R consists of the following rules:

g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(39) 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.
a: 0
b: 1
c: 0
G: 0
d: 0
e: 0
g: 0
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.

(40) Obligation:

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

G.0-0(d., g.0-0(d., g.0-0(e., x0))) → G.0-0(c., g.0-0(d., g.0-0(c., x0)))
G.0-0(c., g.0-0(c., g.0-0(d., x0))) → G.0-0(e., g.0-0(c., g.0-0(e., x0)))
G.0-0(c., g.0-0(c., g.0-1(d., x0))) → G.0-0(e., g.0-0(c., g.0-1(e., x0)))
G.0-0(d., g.0-0(d., g.0-1(e., x0))) → G.0-0(c., g.0-0(d., g.0-1(c., x0)))
G.0-0(e., g.0-0(e., g.0-0(c., x0))) → G.0-0(d., g.0-0(e., g.0-0(d., x0)))
G.0-0(e., g.0-0(e., g.0-1(c., x0))) → G.0-0(d., g.0-0(e., g.0-1(d., x0)))

The TRS R consists of the following rules:

g.0-0(e., g.0-0(e., x)) → g.0-0(d., g.0-0(c., x))
g.0-0(e., g.0-1(e., x)) → g.0-0(d., g.0-1(c., x))
g.0-0(d., g.0-0(d., x)) → g.0-0(c., g.0-0(e., x))
g.0-0(d., g.0-1(d., x)) → g.0-0(c., g.0-1(e., x))
g.0-0(c., g.0-0(c., x)) → g.0-0(e., g.0-0(d., x))
g.0-0(c., g.0-1(c., x)) → g.0-0(e., g.0-1(d., x))
g.0-0(x, g.0-0(y, g.0-0(x, y))) → g.0-0(a., g.0-0(x, g.0-1(y, b.)))
g.0-0(x, g.1-0(y, g.0-1(x, y))) → g.0-0(a., g.0-0(x, g.1-1(y, b.)))
g.1-0(x, g.0-0(y, g.1-0(x, y))) → g.0-0(a., g.1-0(x, g.0-1(y, b.)))
g.1-0(x, g.1-0(y, g.1-1(x, y))) → g.0-0(a., g.1-0(x, g.1-1(y, b.)))

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

(41) DependencyGraphProof (EQUIVALENT transformation)

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

(42) Obligation:

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

G.0-0(c., g.0-0(c., g.0-0(d., x0))) → G.0-0(e., g.0-0(c., g.0-0(e., x0)))
G.0-0(e., g.0-0(e., g.0-0(c., x0))) → G.0-0(d., g.0-0(e., g.0-0(d., x0)))
G.0-0(d., g.0-0(d., g.0-0(e., x0))) → G.0-0(c., g.0-0(d., g.0-0(c., x0)))

The TRS R consists of the following rules:

g.0-0(e., g.0-0(e., x)) → g.0-0(d., g.0-0(c., x))
g.0-0(e., g.0-1(e., x)) → g.0-0(d., g.0-1(c., x))
g.0-0(d., g.0-0(d., x)) → g.0-0(c., g.0-0(e., x))
g.0-0(d., g.0-1(d., x)) → g.0-0(c., g.0-1(e., x))
g.0-0(c., g.0-0(c., x)) → g.0-0(e., g.0-0(d., x))
g.0-0(c., g.0-1(c., x)) → g.0-0(e., g.0-1(d., x))
g.0-0(x, g.0-0(y, g.0-0(x, y))) → g.0-0(a., g.0-0(x, g.0-1(y, b.)))
g.0-0(x, g.1-0(y, g.0-1(x, y))) → g.0-0(a., g.0-0(x, g.1-1(y, b.)))
g.1-0(x, g.0-0(y, g.1-0(x, y))) → g.0-0(a., g.1-0(x, g.0-1(y, b.)))
g.1-0(x, g.1-0(y, g.1-1(x, y))) → g.0-0(a., g.1-0(x, g.1-1(y, b.)))

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

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

No dependency pairs are removed.

The following rules are removed from R:

g.0-0(x, g.1-0(y, g.0-1(x, y))) → g.0-0(a., g.0-0(x, g.1-1(y, b.)))
g.1-0(x, g.0-0(y, g.1-0(x, y))) → g.0-0(a., g.1-0(x, g.0-1(y, b.)))
g.1-0(x, g.1-0(y, g.1-1(x, y))) → g.0-0(a., g.1-0(x, g.1-1(y, b.)))

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(G.0-0(x₁, x₂)) = x₁ + x₂
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(d.) = 0
POL(e.) = 0
POL(g.0-0(x₁, x₂)) = x₁ + x₂
POL(g.0-1(x₁, x₂)) = x₁ + x₂
POL(g.1-0(x₁, x₂)) = 1 + x₁ + x₂
POL(g.1-1(x₁, x₂)) = x₁ + x₂

(44) Obligation:

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

G.0-0(c., g.0-0(c., g.0-0(d., x0))) → G.0-0(e., g.0-0(c., g.0-0(e., x0)))
G.0-0(e., g.0-0(e., g.0-0(c., x0))) → G.0-0(d., g.0-0(e., g.0-0(d., x0)))
G.0-0(d., g.0-0(d., g.0-0(e., x0))) → G.0-0(c., g.0-0(d., g.0-0(c., x0)))

The TRS R consists of the following rules:

g.0-0(d., g.0-0(d., x)) → g.0-0(c., g.0-0(e., x))
g.0-0(c., g.0-0(c., x)) → g.0-0(e., g.0-0(d., x))
g.0-0(e., g.0-0(e., x)) → g.0-0(d., g.0-0(c., x))
g.0-0(c., g.0-1(c., x)) → g.0-0(e., g.0-1(d., x))
g.0-0(x, g.0-0(y, g.0-0(x, y))) → g.0-0(a., g.0-0(x, g.0-1(y, b.)))
g.0-0(d., g.0-1(d., x)) → g.0-0(c., g.0-1(e., x))
g.0-0(e., g.0-1(e., x)) → g.0-0(d., g.0-1(c., x))

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

(45) MRRProof (EQUIVALENT transformation)

g.0-0(x, g.0-0(y, g.0-0(x, y))) → g.0-0(a., g.0-0(x, g.0-1(y, b.)))

Used ordering: Polynomial interpretation [POLO]:

POL(G.0-0(x₁, x₂)) = x₁ + x₂
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(d.) = 0
POL(e.) = 0
POL(g.0-0(x₁, x₂)) = 1 + x₁ + x₂
POL(g.0-1(x₁, x₂)) = x₁ + x₂

(46) Obligation:

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

G.0-0(c., g.0-0(c., g.0-0(d., x0))) → G.0-0(e., g.0-0(c., g.0-0(e., x0)))
G.0-0(e., g.0-0(e., g.0-0(c., x0))) → G.0-0(d., g.0-0(e., g.0-0(d., x0)))
G.0-0(d., g.0-0(d., g.0-0(e., x0))) → G.0-0(c., g.0-0(d., g.0-0(c., x0)))

The TRS R consists of the following rules:

g.0-0(d., g.0-0(d., x)) → g.0-0(c., g.0-0(e., x))
g.0-0(c., g.0-0(c., x)) → g.0-0(e., g.0-0(d., x))
g.0-0(e., g.0-0(e., x)) → g.0-0(d., g.0-0(c., x))
g.0-0(c., g.0-1(c., x)) → g.0-0(e., g.0-1(d., x))
g.0-0(d., g.0-1(d., x)) → g.0-0(c., g.0-1(e., x))
g.0-0(e., g.0-1(e., x)) → g.0-0(d., g.0-1(c., x))

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

(47) PisEmptyProof (SOUND transformation)

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

(48) TRUE

(49) Obligation:

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

G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))

The TRS R consists of the following rules:

g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(e, g(e, x)) → g(d, g(c, x))

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

(50) UsableRulesReductionPairsProof (EQUIVALENT transformation)

First, we A-transformed [FROCOS05] the QDP-Problem. Then we obtain the following A-transformed DP problem.
The pairs P are:

c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(x0)))
d1(d(e(x0))) → c1(d(c(x0)))

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

c(c(x)) → e(d(x))
e(e(x)) → d(c(x))
d(d(x)) → c(e(x))

Q is empty.

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.

No dependency pairs are removed.

The following rules are removed from R:

g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))
g(e, g(e, x)) → g(d, g(c, x))

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(c(x₁)) = 2·x₁
POL(c1(x₁)) = 2·x₁
POL(d(x₁)) = 2·x₁
POL(d1(x₁)) = 2·x₁
POL(e(x₁)) = 2·x₁
POL(e1(x₁)) = 2·x₁

(51) Obligation:

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

c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(x0)))
d1(d(e(x0))) → c1(d(c(x0)))

The TRS R consists of the following rules:

c(c(x)) → e(d(x))
e(e(x)) → d(c(x))
d(d(x)) → c(e(x))

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

(52) RFCMatchBoundsDPProof (EQUIVALENT transformation)

Finiteness of the DP problem can be shown by a matchbound of 1.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(x0)))
d1(d(e(x0))) → c1(d(c(x0)))

To find matches we regarded all rules of R and P:

c(c(x)) → e(d(x))
e(e(x)) → d(c(x))
d(d(x)) → c(e(x))
c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(x0)))
d1(d(e(x0))) → c1(d(c(x0)))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

573, 581, 582, 583, 584, 585, 586, 587, 588, 589, 590

Node 573 is start node and node 581 is final node.

Those nodes are connected through the following edges:

573 to 582 labelled e1_1(0)
573 to 584 labelled d1_1(0)
573 to 586 labelled c1_1(0)
581 to 581 labelled #_1(0)
582 to 583 labelled c_1(0)
583 to 581 labelled e_1(0)
583 to 588 labelled d_1(1)
584 to 585 labelled e_1(0)
585 to 581 labelled d_1(0)
585 to 589 labelled c_1(1)
586 to 587 labelled d_1(0)
587 to 581 labelled c_1(0)
587 to 590 labelled e_1(1)
588 to 581 labelled c_1(1)
588 to 590 labelled e_1(1)
589 to 581 labelled e_1(1)
589 to 588 labelled d_1(1)
590 to 581 labelled d_1(1)
590 to 589 labelled c_1(1)

(53) YES

(54) Obligation:

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

F(g(x, y)) → F(x)
F(g(x, y)) → F(f(x))

The TRS R consists of the following rules:

g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(55) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(g(x, y)) → F(f(x)) at position [0] we obtained the following new rules [LPAR04]:

F(g(g(x0, x1), y1)) → F(g(x1, g(f(f(x0)), a))) → F(g(g(x0, x1), y1)) → F(g(x1, g(f(f(x0)), a)))

(56) Obligation:

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

F(g(x, y)) → F(x)
F(g(g(x0, x1), y1)) → F(g(x1, g(f(f(x0)), a)))

The TRS R consists of the following rules:

g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(57) SplitQDPProof (EQUIVALENT transformation)

We show in the first subproof that some pairs and rules can be removed, afterwards, we continue with the remaining DP-Problem

(58) Complex Obligation (AND)

(59) Obligation:

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

F(g(x, y)) → F(x)
F(g(g(x0, x1), y1)) → F(g(x1, g(f(f(x0)), a)))

The TRS R consists of the following rules:

g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))
g(x, g(y, g(x, y))) → g(a, g(x, g(y, b)))

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

(60) 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.
a: 1
b: 0
c: 0
d: 0
f: 0
F: 0
e: 0
g: 0
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.

(61) Obligation:

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

F.0(g.0-0(x, y)) → F.0(x)
F.0(g.0-1(x, y)) → F.0(x)
F.0(g.1-0(x, y)) → F.1(x)
F.0(g.1-1(x, y)) → F.1(x)
F.0(g.0-0(g.0-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-1(g.0-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-0(g.0-1(x0, x1), y1)) → F.0(g.1-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-1(g.0-1(x0, x1), y1)) → F.0(g.1-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-0(g.1-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.)))
F.0(g.0-1(g.1-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.)))
F.0(g.0-0(g.1-1(x0, x1), y1)) → F.0(g.1-0(x1, g.0-1(f.0(f.1(x0)), a.)))
F.0(g.0-1(g.1-1(x0, x1), y1)) → F.0(g.1-0(x1, g.0-1(f.0(f.1(x0)), a.)))

The TRS R consists of the following rules:

g.0-0(c., g.0-0(c., x)) → g.0-0(e., g.0-0(d., x))
g.0-0(c., g.0-1(c., x)) → g.0-0(e., g.0-1(d., x))
g.0-0(d., g.0-0(d., x)) → g.0-0(c., g.0-0(e., x))
g.0-0(d., g.0-1(d., x)) → g.0-0(c., g.0-1(e., x))
g.0-0(e., g.0-0(e., x)) → g.0-0(d., g.0-0(c., x))
g.0-0(e., g.0-1(e., x)) → g.0-0(d., g.0-1(c., x))
f.0(g.0-0(x, y)) → g.0-0(y, g.0-1(f.0(f.0(x)), a.))
f.0(g.0-1(x, y)) → g.1-0(y, g.0-1(f.0(f.0(x)), a.))
f.0(g.1-0(x, y)) → g.0-0(y, g.0-1(f.0(f.1(x)), a.))
f.0(g.1-1(x, y)) → g.1-0(y, g.0-1(f.0(f.1(x)), a.))
g.0-0(x, g.0-0(y, g.0-0(x, y))) → g.1-0(a., g.0-0(x, g.0-0(y, b.)))
g.0-0(x, g.1-0(y, g.0-1(x, y))) → g.1-0(a., g.0-0(x, g.1-0(y, b.)))
g.1-0(x, g.0-0(y, g.1-0(x, y))) → g.1-0(a., g.1-0(x, g.0-0(y, b.)))
g.1-0(x, g.1-0(y, g.1-1(x, y))) → g.1-0(a., g.1-0(x, g.1-0(y, b.)))

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

(62) DependencyGraphProof (EQUIVALENT transformation)

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

(63) Obligation:

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

F.0(g.0-0(x, y)) → F.0(x)
F.0(g.0-1(x, y)) → F.0(x)
F.0(g.0-0(g.0-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-0(g.1-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.)))
F.0(g.0-1(g.0-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-1(g.1-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.)))

The TRS R consists of the following rules:

g.0-0(c., g.0-0(c., x)) → g.0-0(e., g.0-0(d., x))
g.0-0(c., g.0-1(c., x)) → g.0-0(e., g.0-1(d., x))
g.0-0(d., g.0-0(d., x)) → g.0-0(c., g.0-0(e., x))
g.0-0(d., g.0-1(d., x)) → g.0-0(c., g.0-1(e., x))
g.0-0(e., g.0-0(e., x)) → g.0-0(d., g.0-0(c., x))
g.0-0(e., g.0-1(e., x)) → g.0-0(d., g.0-1(c., x))
f.0(g.0-0(x, y)) → g.0-0(y, g.0-1(f.0(f.0(x)), a.))
f.0(g.0-1(x, y)) → g.1-0(y, g.0-1(f.0(f.0(x)), a.))
f.0(g.1-0(x, y)) → g.0-0(y, g.0-1(f.0(f.1(x)), a.))
f.0(g.1-1(x, y)) → g.1-0(y, g.0-1(f.0(f.1(x)), a.))
g.0-0(x, g.0-0(y, g.0-0(x, y))) → g.1-0(a., g.0-0(x, g.0-0(y, b.)))
g.0-0(x, g.1-0(y, g.0-1(x, y))) → g.1-0(a., g.0-0(x, g.1-0(y, b.)))
g.1-0(x, g.0-0(y, g.1-0(x, y))) → g.1-0(a., g.1-0(x, g.0-0(y, b.)))
g.1-0(x, g.1-0(y, g.1-1(x, y))) → g.1-0(a., g.1-0(x, g.1-0(y, b.)))

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

(64) UsableRulesReductionPairsProof (EQUIVALENT transformation)

g.0-0(c., g.0-0(c., x)) → g.0-0(e., g.0-0(d., x))
g.0-0(d., g.0-0(d., x)) → g.0-0(c., g.0-0(e., x))
g.0-0(e., g.0-0(e., x)) → g.0-0(d., g.0-0(c., x))
f.0(g.1-1(x, y)) → g.1-0(y, g.0-1(f.0(f.1(x)), a.))
g.0-0(x, g.0-0(y, g.0-0(x, y))) → g.1-0(a., g.0-0(x, g.0-0(y, b.)))
g.0-0(x, g.1-0(y, g.0-1(x, y))) → g.1-0(a., g.0-0(x, g.1-0(y, b.)))
g.1-0(x, g.0-0(y, g.1-0(x, y))) → g.1-0(a., g.1-0(x, g.0-0(y, b.)))
g.1-0(x, g.1-0(y, g.1-1(x, y))) → g.1-0(a., g.1-0(x, g.1-0(y, b.)))

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F.0(x₁)) = x₁
POL(a.) = 0
POL(c.) = 0
POL(d.) = 0
POL(e.) = 0
POL(f.0(x₁)) = x₁
POL(f.1(x₁)) = x₁
POL(g.0-0(x₁, x₂)) = x₁ + x₂
POL(g.0-1(x₁, x₂)) = x₁ + x₂
POL(g.1-0(x₁, x₂)) = x₁ + x₂
POL(g.1-1(x₁, x₂)) = x₁ + x₂

(65) Obligation:

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

F.0(g.0-0(x, y)) → F.0(x)
F.0(g.0-1(x, y)) → F.0(x)
F.0(g.0-0(g.0-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-0(g.1-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.)))
F.0(g.0-1(g.0-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.0(x0)), a.)))
F.0(g.0-1(g.1-0(x0, x1), y1)) → F.0(g.0-0(x1, g.0-1(f.0(f.1(x0)), a.)))

The TRS R consists of the following rules:

f.0(g.0-0(x, y)) → g.0-0(y, g.0-1(f.0(f.0(x)), a.))
f.0(g.0-1(x, y)) → g.1-0(y, g.0-1(f.0(f.0(x)), a.))
f.0(g.1-0(x, y)) → g.0-0(y, g.0-1(f.0(f.1(x)), a.))
g.0-0(c., g.0-1(c., x)) → g.0-0(e., g.0-1(d., x))
g.0-0(d., g.0-1(d., x)) → g.0-0(c., g.0-1(e., x))
g.0-0(e., g.0-1(e., x)) → g.0-0(d., g.0-1(c., x))

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

(66) PisEmptyProof (SOUND transformation)

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

(67) TRUE

(68) Obligation:

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

F(g(x, y)) → F(x)
F(g(g(x0, x1), y1)) → F(g(x1, g(f(f(x0)), a)))

The TRS R consists of the following rules:

f(g(x, y)) → g(y, g(f(f(x)), a))
g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))

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

(69) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

F(g(x, y)) → F(x)
F(g(g(x0, x1), y1)) → F(g(x1, g(f(f(x0)), a)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(F(x₁)) = 1 +
[ 2, 0 ]

· x₁

POL(g(x₁, x₂)) =
/ 1 \

\ 1 /

+
/ 1 1 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 1 1 /

· x₂

POL(f(x₁)) =
/ 0 \

\ 0 /

+
/ 0 1 \

\ 3 0 /

· x₁

POL(a) =
/ 0 \

\ 0 /

POL(e) =
/ 0 \

\ 0 /

POL(d) =
/ 0 \

\ 0 /

POL(c) =
/ 0 \

\ 0 /

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

f(g(x, y)) → g(y, g(f(f(x)), a))
g(e, g(e, x)) → g(d, g(c, x))
g(d, g(d, x)) → g(c, g(e, x))
g(c, g(c, x)) → g(e, g(d, x))

(70) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f(g(x, y)) → g(y, g(f(f(x)), a))
g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))

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

(71) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) UsableRulesProof (EQUIVALENT transformation)

(7) Obligation:

(8) MRRProof (EQUIVALENT transformation)

(9) Obligation:

(10) DependencyGraphProof (EQUIVALENT transformation)

(11) Complex Obligation (AND)

(12) Obligation:

(13) TransformationProof (EQUIVALENT transformation)

(14) Obligation:

(15) DependencyGraphProof (EQUIVALENT transformation)

(16) TRUE

(17) Obligation:

(18) TransformationProof (EQUIVALENT transformation)

(19) Obligation:

(20) TransformationProof (EQUIVALENT transformation)

(21) Obligation:

(22) TransformationProof (EQUIVALENT transformation)

(23) Obligation:

(24) TransformationProof (EQUIVALENT transformation)

(25) Obligation:

(26) DependencyGraphProof (EQUIVALENT transformation)

(27) Obligation:

(28) TransformationProof (EQUIVALENT transformation)

(29) Obligation:

(30) DependencyGraphProof (EQUIVALENT transformation)

(31) Obligation:

(32) TransformationProof (EQUIVALENT transformation)

(33) Obligation:

(34) DependencyGraphProof (EQUIVALENT transformation)

(35) Obligation:

(36) SplitQDPProof (EQUIVALENT transformation)

(37) Complex Obligation (AND)

(38) Obligation:

(39) SemLabProof (SOUND transformation)

(40) Obligation:

(41) DependencyGraphProof (EQUIVALENT transformation)

(42) Obligation:

(43) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(44) Obligation:

(45) MRRProof (EQUIVALENT transformation)

(46) Obligation:

(47) PisEmptyProof (SOUND transformation)

(48) TRUE

(49) Obligation:

(50) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(51) Obligation:

(52) RFCMatchBoundsDPProof (EQUIVALENT transformation)

(53) YES

(54) Obligation:

(55) TransformationProof (EQUIVALENT transformation)

(56) Obligation:

(57) SplitQDPProof (EQUIVALENT transformation)

(58) Complex Obligation (AND)

(59) Obligation:

(60) SemLabProof (SOUND transformation)

(61) Obligation:

(62) DependencyGraphProof (EQUIVALENT transformation)

(63) Obligation:

(64) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(65) Obligation:

(66) PisEmptyProof (SOUND transformation)

(67) TRUE

(68) Obligation:

(69) QDPOrderProof (EQUIVALENT transformation)

(70) Obligation:

(71) PisEmptyProof (EQUIVALENT transformation)

(72) YES