YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/examples/collection/towerPhi.srs

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 QDP
↳5 QDPOrderProof (⇔, 33 ms)
↳6 QDP
↳7 QDPOrderProof (⇔, 92 ms)
↳8 QDP
↳9 PisEmptyProof (⇔, 0 ms)
↳10 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(c(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:

R1(Aa(x)) → A(R(x))
R1(Aa(x)) → R1(x)
R1(Ab(x)) → B(R(x))
R1(Ab(x)) → R1(x)
R1(Ac(x)) → C(R(x))
R1(Ac(x)) → R1(x)
A(b(L(x))) → B(c(a(R(x))))
A(b(L(x))) → C(a(R(x)))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R1(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))) → R1(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(c(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))) → C(a(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R1(x)
R1(Aa(x)) → A(R(x))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R1(x)
R1(Aa(x)) → R1(x)
R1(Ab(x)) → R1(x)
R1(Ac(x)) → C(R(x))
R1(Ac(x)) → R1(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(c(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.


A(b(L(x))) → R1(x)
R1(Aa(x)) → R1(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(A(x1)) = 1 + x1   
POL(Aa(x1)) = 1 + x1   
POL(Ab(x1)) = x1   
POL(Ac(x1)) = x1   
POL(C(x1)) = x1   
POL(E(x1)) = 1 + x1   
POL(L(x1)) = x1   
POL(R(x1)) = x1   
POL(R1(x1)) = x1   
POL(a(x1)) = 1 + x1   
POL(b(x1)) = x1   
POL(c(x1)) = x1   

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(c(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))) → C(a(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R1(x)
R1(Aa(x)) → A(R(x))
A(b(L(x))) → A(R(x))
R1(Ab(x)) → R1(x)
R1(Ac(x)) → C(R(x))
R1(Ac(x)) → R1(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(c(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) QDPOrderProof (EQUIVALENT transformation)

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


The following pairs can be oriented strictly and are deleted.


A(b(L(x))) → C(a(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R1(x)
R1(Aa(x)) → A(R(x))
A(b(L(x))) → A(R(x))
R1(Ab(x)) → R1(x)
R1(Ac(x)) → C(R(x))
R1(Ac(x)) → R1(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A(x1)  =  A(x1)
b(x1)  =  b(x1)
L(x1)  =  x1
C(x1)  =  C(x1)
a(x1)  =  a(x1)
R(x1)  =  x1
R1(x1)  =  R1(x1)
Aa(x1)  =  Aa(x1)
Ab(x1)  =  Ab(x1)
Ac(x1)  =  Ac(x1)
E(x1)  =  E(x1)
c(x1)  =  c(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
[A1, a1, Aa1] > [C1, R^11, Ac1, c1] > [b1, Ab1]

Status:
A1: [1]
b1: [1]
C1: [1]
a1: [1]
R^11: [1]
Aa1: [1]
Ab1: [1]
Ac1: [1]
E1: [1]
c1: [1]


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

(8) 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(c(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.

(9) PisEmptyProof (EQUIVALENT transformation)

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

(10) YES