YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z104-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 (⇔, 63 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 4 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 3 ms)
↳8 QTRS
↳9 Overlay + Local Confluence (⇔, 0 ms)
↳10 QTRS
↳11 DependencyPairsProof (⇔, 15 ms)
↳12 QDP
↳13 DependencyGraphProof (⇔, 0 ms)
↳14 AND
    ↳15 QDP
        ↳16 UsableRulesProof (⇔, 0 ms)
        ↳17 QDP
        ↳18 QReductionProof (⇔, 0 ms)
        ↳19 QDP
        ↳20 QDPSizeChangeProof (⇔, 0 ms)
        ↳21 YES
    ↳22 QDP
        ↳23 UsableRulesProof (⇔, 0 ms)
        ↳24 QDP
        ↳25 QReductionProof (⇔, 0 ms)
        ↳26 QDP
        ↳27 QDPSizeChangeProof (⇔, 0 ms)
        ↳28 YES
    ↳29 QDP
        ↳30 UsableRulesProof (⇔, 0 ms)
        ↳31 QDP
        ↳32 QReductionProof (⇔, 0 ms)
        ↳33 QDP
        ↳34 QDPSizeChangeProof (⇔, 0 ms)
        ↳35 YES
    ↳36 QDP
        ↳37 UsableRulesProof (⇔, 0 ms)
        ↳38 QDP
        ↳39 QReductionProof (⇔, 0 ms)
        ↳40 QDP
        ↳41 QDPSizeChangeProof (⇔, 0 ms)
        ↳42 YES
    ↳43 QDP
        ↳44 UsableRulesProof (⇔, 0 ms)
        ↳45 QDP
        ↳46 QReductionProof (⇔, 0 ms)
        ↳47 QDP
        ↳48 QDPSizeChangeProof (⇔, 0 ms)
        ↳49 YES

(0) Obligation:

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

B(x) → W(M(M(M(V(x)))))
M(x) → x
M(V(c(x))) → V(Xc(x))
M(V(a(x))) → V(Xa(x))
M(V(d(x))) → V(Xd(x))
M(V(b(x))) → V(Xb(x))
Xc(c(x)) → c(Xc(x))
Xc(a(x)) → a(Xc(x))
Xc(d(x)) → d(Xc(x))
Xc(b(x)) → b(Xc(x))
Xa(c(x)) → c(Xa(x))
Xa(a(x)) → a(Xa(x))
Xa(d(x)) → d(Xa(x))
Xa(b(x)) → b(Xa(x))
Xd(c(x)) → c(Xd(x))
Xd(a(x)) → a(Xd(x))
Xd(d(x)) → d(Xd(x))
Xd(b(x)) → b(Xd(x))
Xb(c(x)) → c(Xb(x))
Xb(a(x)) → a(Xb(x))
Xb(d(x)) → d(Xb(x))
Xb(b(x)) → b(Xb(x))
Xc(E(x)) → c(E(x))
Xa(E(x)) → a(E(x))
Xd(E(x)) → d(E(x))
Xb(E(x)) → b(E(x))
W(V(x)) → R(L(x))
L(c(x)) → Yc(L(x))
L(a(x)) → Ya(L(x))
L(d(x)) → Yd(L(x))
L(b(x)) → Yb(L(x))
L(c(c(c(a(x))))) → D(d(d(x)))
L(d(b(x))) → D(c(c(x)))
L(c(x)) → D(a(a(a(a(x)))))
L(d(x)) → D(b(b(b(b(x)))))
L(b(d(x))) → D(c(c(x)))
L(a(c(c(c(x))))) → D(d(d(x)))
Yc(D(x)) → D(c(x))
Ya(D(x)) → D(a(x))
Yd(D(x)) → D(d(x))
Yb(D(x)) → D(b(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(M(W(x)))))
M(x) → x
c(V(M(x))) → Xc(V(x))
a(V(M(x))) → Xa(V(x))
d(V(M(x))) → Xd(V(x))
b(V(M(x))) → Xb(V(x))
c(Xc(x)) → Xc(c(x))
a(Xc(x)) → Xc(a(x))
d(Xc(x)) → Xc(d(x))
b(Xc(x)) → Xc(b(x))
c(Xa(x)) → Xa(c(x))
a(Xa(x)) → Xa(a(x))
d(Xa(x)) → Xa(d(x))
b(Xa(x)) → Xa(b(x))
c(Xd(x)) → Xd(c(x))
a(Xd(x)) → Xd(a(x))
d(Xd(x)) → Xd(d(x))
b(Xd(x)) → Xd(b(x))
c(Xb(x)) → Xb(c(x))
a(Xb(x)) → Xb(a(x))
d(Xb(x)) → Xb(d(x))
b(Xb(x)) → Xb(b(x))
E(Xc(x)) → E(c(x))
E(Xa(x)) → E(a(x))
E(Xd(x)) → E(d(x))
E(Xb(x)) → E(b(x))
V(W(x)) → L(R(x))
c(L(x)) → L(Yc(x))
a(L(x)) → L(Ya(x))
d(L(x)) → L(Yd(x))
b(L(x)) → L(Yb(x))
a(c(c(c(L(x))))) → d(d(D(x)))
b(d(L(x))) → c(c(D(x)))
c(L(x)) → a(a(a(a(D(x)))))
d(L(x)) → b(b(b(b(D(x)))))
d(b(L(x))) → c(c(D(x)))
c(c(c(a(L(x))))) → d(d(D(x)))
D(Yc(x)) → c(D(x))
D(Ya(x)) → a(D(x))
D(Yd(x)) → d(D(x))
D(Yb(x)) → b(D(x))
D(R(x)) → B(x)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(B(x1)) = 8 + x1   
POL(D(x1)) = 9 + 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)) = 148 + x1   
POL(Xb(x1)) = 240 + x1   
POL(Xc(x1)) = 599 + x1   
POL(Xd(x1)) = 967 + x1   
POL(Ya(x1)) = 147 + x1   
POL(Yb(x1)) = 239 + x1   
POL(Yc(x1)) = 598 + x1   
POL(Yd(x1)) = 966 + x1   
POL(a(x1)) = 147 + x1   
POL(b(x1)) = 239 + x1   
POL(c(x1)) = 598 + x1   
POL(d(x1)) = 966 + 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(M(W(x)))))
M(x) → x
c(V(M(x))) → Xc(V(x))
a(V(M(x))) → Xa(V(x))
d(V(M(x))) → Xd(V(x))
b(V(M(x))) → Xb(V(x))
E(Xc(x)) → E(c(x))
E(Xa(x)) → E(a(x))
E(Xd(x)) → E(d(x))
E(Xb(x)) → E(b(x))
V(W(x)) → L(R(x))
c(L(x)) → a(a(a(a(D(x)))))
d(L(x)) → b(b(b(b(D(x)))))
D(R(x)) → B(x)


(4) Obligation:

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

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

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(D(x1)) = x1   
POL(L(x1)) = x1   
POL(Xa(x1)) = x1   
POL(Xb(x1)) = x1   
POL(Xc(x1)) = x1   
POL(Xd(x1)) = x1   
POL(Ya(x1)) = x1   
POL(Yb(x1)) = 1 + x1   
POL(Yc(x1)) = x1   
POL(Yd(x1)) = x1   
POL(a(x1)) = x1   
POL(b(x1)) = 1 + x1   
POL(c(x1)) = x1   
POL(d(x1)) = x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

b(d(L(x))) → c(c(D(x)))
d(b(L(x))) → c(c(D(x)))


(6) Obligation:

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

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

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(D(x1)) = x1   
POL(L(x1)) = 1 + x1   
POL(Xa(x1)) = x1   
POL(Xb(x1)) = x1   
POL(Xc(x1)) = x1   
POL(Xd(x1)) = x1   
POL(Ya(x1)) = x1   
POL(Yb(x1)) = x1   
POL(Yc(x1)) = x1   
POL(Yd(x1)) = x1   
POL(a(x1)) = x1   
POL(b(x1)) = x1   
POL(c(x1)) = x1   
POL(d(x1)) = x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

a(c(c(c(L(x))))) → d(d(D(x)))
c(c(c(a(L(x))))) → d(d(D(x)))


(8) Obligation:

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

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

Q is empty.

(9) Overlay + Local Confluence (EQUIVALENT transformation)

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

(10) Obligation:

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

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

The set Q consists of the following terms:

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

(11) DependencyPairsProof (EQUIVALENT transformation)

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

(12) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

(13) DependencyGraphProof (EQUIVALENT transformation)

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

(14) Complex Obligation (AND)

(15) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

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

(17) Obligation:

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

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

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

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

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

(18) 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].

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

(19) Obligation:

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

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

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

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

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

(21) YES

(22) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

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

(24) Obligation:

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

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

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

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

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

(25) 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].

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

(26) Obligation:

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

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

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

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

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

(28) YES

(29) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

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

(31) Obligation:

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

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

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

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

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

(32) 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].

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

(33) Obligation:

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

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

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

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

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

(35) YES

(36) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

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

(38) Obligation:

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

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

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

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

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

(39) 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].

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

(40) Obligation:

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

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

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

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

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

(42) YES

(43) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

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

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

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

(45) Obligation:

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

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

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

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

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

(46) 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].

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

(47) Obligation:

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

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

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

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

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

(49) YES