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 (⇔, 12 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 QDP

        ↳6 UsableRulesProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 MRRProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 TransformationProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 DependencyGraphProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 TransformationProof (⇔, 0 ms)

        ↳15 QDP

        ↳16 DependencyGraphProof (⇔, 0 ms)

        ↳17 QDP

        ↳18 TransformationProof (⇔, 0 ms)

        ↳19 QDP

        ↳20 DependencyGraphProof (⇔, 0 ms)

        ↳21 QDP

        ↳22 SplitQDPProof (⇔, 0 ms)

        ↳23 AND

            ↳24 QDP

                ↳25 SemLabProof (⇒, 0 ms)

                ↳26 QDP

                ↳27 DependencyGraphProof (⇔, 0 ms)

                ↳28 QDP

                ↳29 UsableRulesReductionPairsProof (⇔, 0 ms)

                ↳30 QDP

                ↳31 MRRProof (⇔, 0 ms)

                ↳32 QDP

                ↳33 PisEmptyProof (⇒, 0 ms)

                ↳34 TRUE

            ↳35 QDP

                ↳36 UsableRulesReductionPairsProof (⇔, 0 ms)

                ↳37 QDP

                ↳38 RFCMatchBoundsDPProof (⇔, 0 ms)

                ↳39 YES

    ↳40 QDP

        ↳41 TransformationProof (⇔, 0 ms)

        ↳42 QDP

        ↳43 QDPOrderProof (⇔, 96 ms)

        ↳44 QDP

        ↳45 PisEmptyProof (⇔, 0 ms)

        ↳46 YES

(0) Obligation:

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

g(x, x) → g(a, b)
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))

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(x, x) → G(a, b)
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)

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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)

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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)

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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)

Used ordering: Polynomial interpretation [POLO]:

POL(G(x₁, x₂)) = x₁ + 2·x₂
POL(a) = 0
POL(b) = 0
POL(c) = 1
POL(d) = 1
POL(e) = 1
POL(g(x₁, x₂)) = 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))

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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

(10) 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, c)) → G(d, g(a, b)) → G(e, g(e, c)) → G(d, g(a, b))
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)))

(11) 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, c)) → G(d, g(a, b))
G(e, g(e, g(c, x0))) → G(d, g(e, g(d, x0)))

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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

(12) DependencyGraphProof (EQUIVALENT transformation)

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

(13) 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, g(c, x0))) → G(d, g(e, g(d, x0)))
G(d, g(d, x)) → G(c, g(e, x))

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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

(14) 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, d)) → G(e, g(a, b)) → G(c, g(c, d)) → G(e, g(a, b))
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)))

(15) 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, x)) → G(c, g(e, x))
G(c, g(c, d)) → G(e, g(a, b))
G(c, g(c, g(d, x0))) → G(e, g(c, g(e, x0)))

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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

(16) DependencyGraphProof (EQUIVALENT transformation)

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

(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, 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(x, x) → g(a, b)
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))

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, e)) → G(c, g(a, b)) → G(d, g(d, e)) → G(c, g(a, b))
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)))

(19) 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, e)) → G(c, g(a, b))
G(d, g(d, g(e, x0))) → G(c, g(d, g(c, x0)))

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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

(20) DependencyGraphProof (EQUIVALENT transformation)

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

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

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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

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

(23) Complex Obligation (AND)

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

The TRS R consists of the following rules:

g(x, x) → g(a, b)
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))

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

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

(26) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(27) DependencyGraphProof (EQUIVALENT transformation)

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

(28) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(29) 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, x) → g.0-0(a., b.)

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(G.1-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.1-0(x₁, x₂)) = x₁ + x₂
POL(g.1-1(x₁, x₂)) = x₁ + x₂

(30) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(31) MRRProof (EQUIVALENT transformation)

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

Used ordering: Polynomial interpretation [POLO]:

POL(G.1-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.1-0(x₁, x₂)) = x₁ + x₂
POL(g.1-1(x₁, x₂)) = 1 + x₁ + x₂

(32) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(33) PisEmptyProof (SOUND transformation)

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

(34) TRUE

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

(36) UsableRulesReductionPairsProof (EQUIVALENT transformation)

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

d1(d(e(x0))) → c1(d(c(x0)))
c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(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₁)) = x₁
POL(c1(x₁)) = 2 + x₁
POL(d(x₁)) = x₁
POL(d1(x₁)) = 2 + x₁
POL(e(x₁)) = x₁
POL(e1(x₁)) = 2 + x₁

(37) Obligation:

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

d1(d(e(x0))) → c1(d(c(x0)))
c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(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.

(38) 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:

d1(d(e(x0))) → c1(d(c(x0)))
c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(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))
d1(d(e(x0))) → c1(d(c(x0)))
c1(c(d(x0))) → e1(c(e(x0)))
e1(e(c(x0))) → d1(e(d(x0)))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

703, 704, 705, 706, 707, 708, 709, 710, 711, 712, 713

Node 703 is start node and node 704 is final node.

Those nodes are connected through the following edges:

703 to 705 labelled c1_1(0)
703 to 707 labelled e1_1(0)
703 to 709 labelled d1_1(0)
704 to 704 labelled #_1(0)
705 to 706 labelled d_1(0)
706 to 704 labelled c_1(0)
706 to 711 labelled e_1(1)
707 to 708 labelled c_1(0)
708 to 704 labelled e_1(0)
708 to 712 labelled d_1(1)
709 to 710 labelled e_1(0)
710 to 704 labelled d_1(0)
710 to 713 labelled c_1(1)
711 to 704 labelled d_1(1)
711 to 713 labelled c_1(1)
712 to 704 labelled c_1(1)
712 to 711 labelled e_1(1)
713 to 704 labelled e_1(1)
713 to 712 labelled d_1(1)

(39) YES

(40) 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(x, x) → g(a, b)
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))

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

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

(42) 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(x, x) → g(a, b)
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))

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

(43) 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₁)) = 0 +
[ 1, 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(b) =
/ 0 \

\ 0 /

POL(e) =
/ 0 \

\ 3 /

POL(d) =
/ 0 \

\ 3 /

POL(c) =
/ 0 \

\ 3 /

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(x, x) → g(a, b)
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))

(44) Obligation:

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

g(x, x) → g(a, b)
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))

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

(45) 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) TransformationProof (EQUIVALENT transformation)

(11) Obligation:

(12) DependencyGraphProof (EQUIVALENT transformation)

(13) Obligation:

(14) TransformationProof (EQUIVALENT transformation)

(15) Obligation:

(16) DependencyGraphProof (EQUIVALENT transformation)

(17) Obligation:

(18) TransformationProof (EQUIVALENT transformation)

(19) Obligation:

(20) DependencyGraphProof (EQUIVALENT transformation)

(21) Obligation:

(22) SplitQDPProof (EQUIVALENT transformation)

(23) Complex Obligation (AND)

(24) Obligation:

(25) SemLabProof (SOUND transformation)

(26) Obligation:

(27) DependencyGraphProof (EQUIVALENT transformation)

(28) Obligation:

(29) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(30) Obligation:

(31) MRRProof (EQUIVALENT transformation)

(32) Obligation:

(33) PisEmptyProof (SOUND transformation)

(34) TRUE

(35) Obligation:

(36) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(37) Obligation:

(38) RFCMatchBoundsDPProof (EQUIVALENT transformation)

(39) YES

(40) Obligation:

(41) TransformationProof (EQUIVALENT transformation)

(42) Obligation:

(43) QDPOrderProof (EQUIVALENT transformation)

(44) Obligation:

(45) PisEmptyProof (EQUIVALENT transformation)

(46) YES