YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z108-shift.srs

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

0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 46 ms)
↳4 QTRS
↳5 Overlay + Local Confluence (⇔, 0 ms)
↳6 QTRS
↳7 DependencyPairsProof (⇔, 18 ms)
↳8 QDP
↳9 DependencyGraphProof (⇔, 0 ms)
↳10 AND
    ↳11 QDP
        ↳12 UsableRulesProof (⇔, 0 ms)
        ↳13 QDP
        ↳14 QReductionProof (⇔, 0 ms)
        ↳15 QDP
        ↳16 QDPSizeChangeProof (⇔, 0 ms)
        ↳17 YES
    ↳18 QDP
        ↳19 UsableRulesProof (⇔, 0 ms)
        ↳20 QDP
        ↳21 QReductionProof (⇔, 0 ms)
        ↳22 QDP
        ↳23 QDPSizeChangeProof (⇔, 0 ms)
        ↳24 YES
    ↳25 QDP
        ↳26 UsableRulesProof (⇔, 0 ms)
        ↳27 QDP
        ↳28 QReductionProof (⇔, 0 ms)
        ↳29 QDP
        ↳30 QDPSizeChangeProof (⇔, 0 ms)
        ↳31 YES
    ↳32 QDP
        ↳33 UsableRulesProof (⇔, 0 ms)
        ↳34 QDP
        ↳35 QReductionProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 QDPSizeChangeProof (⇔, 0 ms)
        ↳38 YES
    ↳39 QDP
        ↳40 UsableRulesProof (⇔, 0 ms)
        ↳41 QDP
        ↳42 QReductionProof (⇔, 0 ms)
        ↳43 QDP
        ↳44 QDPSizeChangeProof (⇔, 0 ms)
        ↳45 YES

(0) Obligation:

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

B(x) → W(M(M(V(x))))
M(x) → x
M(V(a(x))) → V(Xa(x))
M(V(b(x))) → V(Xb(x))
M(V(c(x))) → V(Xc(x))
M(V(d(x))) → V(Xd(x))
Xa(a(x)) → a(Xa(x))
Xa(b(x)) → b(Xa(x))
Xa(c(x)) → c(Xa(x))
Xa(d(x)) → d(Xa(x))
Xb(a(x)) → a(Xb(x))
Xb(b(x)) → b(Xb(x))
Xb(c(x)) → c(Xb(x))
Xb(d(x)) → d(Xb(x))
Xc(a(x)) → a(Xc(x))
Xc(b(x)) → b(Xc(x))
Xc(c(x)) → c(Xc(x))
Xc(d(x)) → d(Xc(x))
Xd(a(x)) → a(Xd(x))
Xd(b(x)) → b(Xd(x))
Xd(c(x)) → c(Xd(x))
Xd(d(x)) → d(Xd(x))
Xa(E(x)) → a(E(x))
Xb(E(x)) → b(E(x))
Xc(E(x)) → c(E(x))
Xd(E(x)) → d(E(x))
W(V(x)) → R(L(x))
L(a(x)) → Ya(L(x))
L(b(x)) → Yb(L(x))
L(c(x)) → Yc(L(x))
L(d(x)) → Yd(L(x))
L(a(a(x))) → D(b(c(x)))
L(b(b(x))) → D(c(d(x)))
L(c(c(x))) → D(d(d(d(x))))
L(d(d(d(x)))) → D(a(c(x)))
Ya(D(x)) → D(a(x))
Yb(D(x)) → D(b(x))
Yc(D(x)) → D(c(x))
Yd(D(x)) → D(d(x))
R(D(x)) → B(x)

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

B(x) → V(M(M(W(x))))
M(x) → x
a(V(M(x))) → Xa(V(x))
b(V(M(x))) → Xb(V(x))
c(V(M(x))) → Xc(V(x))
d(V(M(x))) → Xd(V(x))
a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
E(Xa(x)) → E(a(x))
E(Xb(x)) → E(b(x))
E(Xc(x)) → E(c(x))
E(Xd(x)) → E(d(x))
V(W(x)) → L(R(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
a(a(L(x))) → c(b(D(x)))
b(b(L(x))) → d(c(D(x)))
c(c(L(x))) → d(d(d(D(x))))
d(d(d(L(x)))) → c(a(D(x)))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))
D(R(x)) → B(x)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(B(x1)) = 6 + x1   
POL(D(x1)) = 7 + x1   
POL(E(x1)) = x1   
POL(L(x1)) = x1   
POL(M(x1)) = 2 + x1   
POL(R(x1)) = x1   
POL(V(x1)) = 1 + x1   
POL(W(x1)) = x1   
POL(Xa(x1)) = 241 + x1   
POL(Xb(x1)) = 217 + x1   
POL(Xc(x1)) = 257 + x1   
POL(Xd(x1)) = 169 + x1   
POL(Ya(x1)) = 240 + x1   
POL(Yb(x1)) = 216 + x1   
POL(Yc(x1)) = 256 + x1   
POL(Yd(x1)) = 168 + x1   
POL(a(x1)) = 240 + x1   
POL(b(x1)) = 216 + x1   
POL(c(x1)) = 256 + x1   
POL(d(x1)) = 168 + x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

B(x) → V(M(M(W(x))))
M(x) → x
a(V(M(x))) → Xa(V(x))
b(V(M(x))) → Xb(V(x))
c(V(M(x))) → Xc(V(x))
d(V(M(x))) → Xd(V(x))
E(Xa(x)) → E(a(x))
E(Xb(x)) → E(b(x))
E(Xc(x)) → E(c(x))
E(Xd(x)) → E(d(x))
V(W(x)) → L(R(x))
a(a(L(x))) → c(b(D(x)))
b(b(L(x))) → d(c(D(x)))
c(c(L(x))) → d(d(d(D(x))))
d(d(d(L(x)))) → c(a(D(x)))
D(R(x)) → B(x)


(4) Obligation:

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

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

Q is empty.

(5) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(6) Obligation:

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

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(8) Obligation:

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

A(Xa(x)) → A(x)
B(Xa(x)) → B(x)
C(Xa(x)) → C(x)
D1(Xa(x)) → D1(x)
A(Xb(x)) → A(x)
B(Xb(x)) → B(x)
C(Xb(x)) → C(x)
D1(Xb(x)) → D1(x)
A(Xc(x)) → A(x)
B(Xc(x)) → B(x)
C(Xc(x)) → C(x)
D1(Xc(x)) → D1(x)
A(Xd(x)) → A(x)
B(Xd(x)) → B(x)
C(Xd(x)) → C(x)
D1(Xd(x)) → D1(x)
D2(Ya(x)) → A(D(x))
D2(Ya(x)) → D2(x)
D2(Yb(x)) → B(D(x))
D2(Yb(x)) → D2(x)
D2(Yc(x)) → C(D(x))
D2(Yc(x)) → D2(x)
D2(Yd(x)) → D1(D(x))
D2(Yd(x)) → D2(x)

The TRS R consists of the following rules:

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Complex Obligation (AND)

(11) Obligation:

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

D1(Xb(x)) → D1(x)
D1(Xa(x)) → D1(x)
D1(Xc(x)) → D1(x)
D1(Xd(x)) → D1(x)

The TRS R consists of the following rules:

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(12) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

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

D1(Xb(x)) → D1(x)
D1(Xa(x)) → D1(x)
D1(Xc(x)) → D1(x)
D1(Xd(x)) → D1(x)

R is empty.
The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(14) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

(15) Obligation:

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

D1(Xb(x)) → D1(x)
D1(Xa(x)) → D1(x)
D1(Xc(x)) → D1(x)
D1(Xd(x)) → D1(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:

  • D1(Xb(x)) → D1(x)
    The graph contains the following edges 1 > 1

  • D1(Xa(x)) → D1(x)
    The graph contains the following edges 1 > 1

  • D1(Xc(x)) → D1(x)
    The graph contains the following edges 1 > 1

  • D1(Xd(x)) → D1(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(Xb(x)) → C(x)
C(Xa(x)) → C(x)
C(Xc(x)) → C(x)
C(Xd(x)) → C(x)

The TRS R consists of the following rules:

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(19) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(20) Obligation:

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

C(Xb(x)) → C(x)
C(Xa(x)) → C(x)
C(Xc(x)) → C(x)
C(Xd(x)) → C(x)

R is empty.
The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(21) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

(22) Obligation:

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

C(Xb(x)) → C(x)
C(Xa(x)) → C(x)
C(Xc(x)) → C(x)
C(Xd(x)) → C(x)

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

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

  • C(Xb(x)) → C(x)
    The graph contains the following edges 1 > 1

  • C(Xa(x)) → C(x)
    The graph contains the following edges 1 > 1

  • C(Xc(x)) → C(x)
    The graph contains the following edges 1 > 1

  • C(Xd(x)) → C(x)
    The graph contains the following edges 1 > 1

(24) YES

(25) Obligation:

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

B(Xb(x)) → B(x)
B(Xa(x)) → B(x)
B(Xc(x)) → B(x)
B(Xd(x)) → B(x)

The TRS R consists of the following rules:

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(26) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(27) Obligation:

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

B(Xb(x)) → B(x)
B(Xa(x)) → B(x)
B(Xc(x)) → B(x)
B(Xd(x)) → B(x)

R is empty.
The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(28) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

(29) Obligation:

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

B(Xb(x)) → B(x)
B(Xa(x)) → B(x)
B(Xc(x)) → B(x)
B(Xd(x)) → B(x)

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

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

  • B(Xb(x)) → B(x)
    The graph contains the following edges 1 > 1

  • B(Xa(x)) → B(x)
    The graph contains the following edges 1 > 1

  • B(Xc(x)) → B(x)
    The graph contains the following edges 1 > 1

  • B(Xd(x)) → B(x)
    The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

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

A(Xb(x)) → A(x)
A(Xa(x)) → A(x)
A(Xc(x)) → A(x)
A(Xd(x)) → A(x)

The TRS R consists of the following rules:

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(33) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(34) Obligation:

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

A(Xb(x)) → A(x)
A(Xa(x)) → A(x)
A(Xc(x)) → A(x)
A(Xd(x)) → A(x)

R is empty.
The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(35) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

(36) Obligation:

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

A(Xb(x)) → A(x)
A(Xa(x)) → A(x)
A(Xc(x)) → A(x)
A(Xd(x)) → A(x)

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

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

  • A(Xb(x)) → A(x)
    The graph contains the following edges 1 > 1

  • A(Xa(x)) → A(x)
    The graph contains the following edges 1 > 1

  • A(Xc(x)) → A(x)
    The graph contains the following edges 1 > 1

  • A(Xd(x)) → A(x)
    The graph contains the following edges 1 > 1

(38) YES

(39) Obligation:

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

D2(Yb(x)) → D2(x)
D2(Ya(x)) → D2(x)
D2(Yc(x)) → D2(x)
D2(Yd(x)) → D2(x)

The TRS R consists of the following rules:

a(Xa(x)) → Xa(a(x))
b(Xa(x)) → Xa(b(x))
c(Xa(x)) → Xa(c(x))
d(Xa(x)) → Xa(d(x))
a(Xb(x)) → Xb(a(x))
b(Xb(x)) → Xb(b(x))
c(Xb(x)) → Xb(c(x))
d(Xb(x)) → Xb(d(x))
a(Xc(x)) → Xc(a(x))
b(Xc(x)) → Xc(b(x))
c(Xc(x)) → Xc(c(x))
d(Xc(x)) → Xc(d(x))
a(Xd(x)) → Xd(a(x))
b(Xd(x)) → Xd(b(x))
c(Xd(x)) → Xd(c(x))
d(Xd(x)) → Xd(d(x))
a(L(x)) → L(Ya(x))
b(L(x)) → L(Yb(x))
c(L(x)) → L(Yc(x))
d(L(x)) → L(Yd(x))
D(Ya(x)) → a(D(x))
D(Yb(x)) → b(D(x))
D(Yc(x)) → c(D(x))
D(Yd(x)) → d(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(40) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(41) Obligation:

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

D2(Yb(x)) → D2(x)
D2(Ya(x)) → D2(x)
D2(Yc(x)) → D2(x)
D2(Yd(x)) → D2(x)

R is empty.
The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

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

(42) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))

(43) Obligation:

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

D2(Yb(x)) → D2(x)
D2(Ya(x)) → D2(x)
D2(Yc(x)) → D2(x)
D2(Yd(x)) → D2(x)

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

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

  • D2(Yb(x)) → D2(x)
    The graph contains the following edges 1 > 1

  • D2(Ya(x)) → D2(x)
    The graph contains the following edges 1 > 1

  • D2(Yc(x)) → D2(x)
    The graph contains the following edges 1 > 1

  • D2(Yd(x)) → D2(x)
    The graph contains the following edges 1 > 1

(45) YES