Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/examples/collection/doubly-expPhi.srs

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

0 QTRS

↳1 DependencyPairsProof (⇔, 0 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 3 ms)

↳4 QDP

↳5 QDPOrderProof (⇔, 87 ms)

↳6 QDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 AND

    ↳9 QDP

        ↳10 MRRProof (⇔, 201 ms)

        ↳11 QDP

        ↳12 DependencyGraphProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 UsableRulesProof (⇔, 0 ms)

        ↳15 QDP

        ↳16 QDPSizeChangeProof (⇔, 0 ms)

        ↳17 YES

    ↳18 QDP

        ↳19 MRRProof (⇔, 176 ms)

        ↳20 QDP

        ↳21 PisEmptyProof (⇔, 0 ms)

        ↳22 YES

(0) Obligation:

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

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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:

R¹(Aa(x)) → A(R(x))
R¹(Aa(x)) → R¹(x)
R¹(Ab(x)) → B(R(x))
R¹(Ab(x)) → R¹(x)
R¹(Ac(x)) → C(R(x))
R¹(Ac(x)) → R¹(x)
A(b(L(x))) → B(a(a(R(x))))
A(b(L(x))) → A(a(R(x)))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R¹(x)
C(b(L(x))) → B(b(c(R(x))))
C(b(L(x))) → B(c(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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 1 SCC with 4 less nodes.

(4) Obligation:

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

A(b(L(x))) → A(a(R(x)))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R¹(x)
R¹(Aa(x)) → A(R(x))
R¹(Aa(x)) → R¹(x)
R¹(Ab(x)) → R¹(x)
R¹(Ac(x)) → C(R(x))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)
R¹(Ac(x)) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(5) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

R¹(Ac(x)) → C(R(x))
R¹(Ac(x)) → R¹(x)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(A(x₁)) = x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Ac(x₁)) = 1 + x₁
POL(C(x₁)) = x₁
POL(E(x₁)) = 1 + x₁
POL(L(x₁)) = x₁
POL(R(x₁)) = x₁
POL(R¹(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(c(x₁)) = 1 + x₁

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

R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))

(6) Obligation:

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

A(b(L(x))) → A(a(R(x)))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R¹(x)
R¹(Aa(x)) → A(R(x))
R¹(Aa(x)) → R¹(x)
R¹(Ab(x)) → R¹(x)
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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 2 SCCs with 1 less node.

(8) Complex Obligation (AND)

(9) Obligation:

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

A(b(L(x))) → A(R(x))
A(b(L(x))) → A(a(R(x)))
A(b(L(x))) → R¹(x)
R¹(Aa(x)) → A(R(x))
R¹(Aa(x)) → R¹(x)
R¹(Ab(x)) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

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

A(b(L(x))) → A(R(x))
A(b(L(x))) → A(a(R(x)))
A(b(L(x))) → R¹(x)
R¹(Ab(x)) → R¹(x)

Used ordering: Polynomial interpretation [POLO]:

POL(A(x₁)) = x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = 1 + x₁
POL(Ac(x₁)) = 2·x₁
POL(E(x₁)) = x₁
POL(L(x₁)) = 2·x₁
POL(R(x₁)) = 2·x₁
POL(R¹(x₁)) = 2·x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = 2 + x₁
POL(c(x₁)) = 2·x₁

(11) Obligation:

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

R¹(Aa(x)) → A(R(x))
R¹(Aa(x)) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(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:

R¹(Aa(x)) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

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

(15) Obligation:

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

R¹(Aa(x)) → R¹(x)

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

(16) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

R¹(Aa(x)) → R¹(x)
The graph contains the following edges 1 > 1

(17) YES

(18) Obligation:

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

C(b(L(x))) → C(R(x))

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(19) MRRProof (EQUIVALENT transformation)

C(b(L(x))) → C(R(x))

Used ordering: Polynomial interpretation [POLO]:

POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = 1 + x₁
POL(Ac(x₁)) = 2·x₁
POL(C(x₁)) = 3·x₁
POL(E(x₁)) = x₁
POL(L(x₁)) = 2·x₁
POL(R(x₁)) = 2·x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = 2 + x₁
POL(c(x₁)) = 2·x₁

(20) Obligation:

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

R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(a(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

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

(5) QDPOrderProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) MRRProof (EQUIVALENT transformation)

(11) Obligation:

(12) DependencyGraphProof (EQUIVALENT transformation)

(13) Obligation:

(14) UsableRulesProof (EQUIVALENT transformation)

(15) Obligation:

(16) QDPSizeChangeProof (EQUIVALENT transformation)

(17) YES

(18) Obligation:

(19) MRRProof (EQUIVALENT transformation)

(20) Obligation:

(21) PisEmptyProof (EQUIVALENT transformation)

(22) YES