YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z112-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 (⇔, 78 ms)
↳4 QTRS
↳5 Overlay + Local Confluence (⇔, 38 ms)
↳6 QTRS
↳7 DependencyPairsProof (⇔, 35 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
    ↳46 QDP
        ↳47 UsableRulesProof (⇔, 0 ms)
        ↳48 QDP
        ↳49 QReductionProof (⇔, 0 ms)
        ↳50 QDP
        ↳51 QDPSizeChangeProof (⇔, 0 ms)
        ↳52 YES
    ↳53 QDP
        ↳54 UsableRulesProof (⇔, 0 ms)
        ↳55 QDP
        ↳56 QReductionProof (⇔, 0 ms)
        ↳57 QDP
        ↳58 QDPSizeChangeProof (⇔, 0 ms)
        ↳59 YES

(0) Obligation:

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

B(x) → W(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))
M(V(f(x))) → V(Xf(x))
M(V(g(x))) → V(Xg(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))
Xa(f(x)) → f(Xa(x))
Xa(g(x)) → g(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))
Xb(f(x)) → f(Xb(x))
Xb(g(x)) → g(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))
Xc(f(x)) → f(Xc(x))
Xc(g(x)) → g(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))
Xd(f(x)) → f(Xd(x))
Xd(g(x)) → g(Xd(x))
Xf(a(x)) → a(Xf(x))
Xf(b(x)) → b(Xf(x))
Xf(c(x)) → c(Xf(x))
Xf(d(x)) → d(Xf(x))
Xf(f(x)) → f(Xf(x))
Xf(g(x)) → g(Xf(x))
Xg(a(x)) → a(Xg(x))
Xg(b(x)) → b(Xg(x))
Xg(c(x)) → c(Xg(x))
Xg(d(x)) → d(Xg(x))
Xg(f(x)) → f(Xg(x))
Xg(g(x)) → g(Xg(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))
Xf(E(x)) → f(E(x))
Xg(E(x)) → g(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(f(x)) → Yf(L(x))
L(g(x)) → Yg(L(x))
L(a(a(x))) → D(b(c(x)))
L(b(b(x))) → D(c(d(x)))
L(b(x)) → D(a(x))
L(c(c(x))) → D(d(f(x)))
L(d(d(x))) → D(f(f(f(x))))
L(d(x)) → D(b(x))
L(f(f(x))) → D(g(a(x)))
L(g(g(x))) → D(a(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))
Yf(D(x)) → D(f(x))
Yg(D(x)) → D(g(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(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))
f(V(M(x))) → Xf(V(x))
g(V(M(x))) → Xg(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
E(Xf(x)) → E(f(x))
E(Xg(x)) → E(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(x))
a(a(L(x))) → c(b(D(x)))
b(b(L(x))) → d(c(D(x)))
b(L(x)) → a(D(x))
c(c(L(x))) → f(d(D(x)))
d(d(L(x))) → f(f(f(D(x))))
d(L(x)) → b(D(x))
f(f(L(x))) → a(g(D(x)))
g(g(L(x))) → 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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))
D(R(x)) → B(x)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(B(x1)) = 4 + x1   
POL(D(x1)) = 5 + 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)) = 931 + x1   
POL(Xb(x1)) = 973 + x1   
POL(Xc(x1)) = 883 + x1   
POL(Xd(x1)) = 1057 + x1   
POL(Xf(x1)) = 703 + x1   
POL(Xg(x1)) = 469 + x1   
POL(Ya(x1)) = 930 + x1   
POL(Yb(x1)) = 972 + x1   
POL(Yc(x1)) = 882 + x1   
POL(Yd(x1)) = 1056 + x1   
POL(Yf(x1)) = 702 + x1   
POL(Yg(x1)) = 468 + x1   
POL(a(x1)) = 930 + x1   
POL(b(x1)) = 972 + x1   
POL(c(x1)) = 882 + x1   
POL(d(x1)) = 1056 + x1   
POL(f(x1)) = 702 + x1   
POL(g(x1)) = 468 + 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(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))
f(V(M(x))) → Xf(V(x))
g(V(M(x))) → Xg(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))
E(Xf(x)) → E(f(x))
E(Xg(x)) → E(g(x))
V(W(x)) → L(R(x))
a(a(L(x))) → c(b(D(x)))
b(b(L(x))) → d(c(D(x)))
b(L(x)) → a(D(x))
c(c(L(x))) → f(d(D(x)))
d(d(L(x))) → f(f(f(D(x))))
d(L(x)) → b(D(x))
f(f(L(x))) → a(g(D(x)))
g(g(L(x))) → 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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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)
F(Xa(x)) → F(x)
G(Xa(x)) → G(x)
A(Xb(x)) → A(x)
B(Xb(x)) → B(x)
C(Xb(x)) → C(x)
D1(Xb(x)) → D1(x)
F(Xb(x)) → F(x)
G(Xb(x)) → G(x)
A(Xc(x)) → A(x)
B(Xc(x)) → B(x)
C(Xc(x)) → C(x)
D1(Xc(x)) → D1(x)
F(Xc(x)) → F(x)
G(Xc(x)) → G(x)
A(Xd(x)) → A(x)
B(Xd(x)) → B(x)
C(Xd(x)) → C(x)
D1(Xd(x)) → D1(x)
F(Xd(x)) → F(x)
G(Xd(x)) → G(x)
A(Xf(x)) → A(x)
B(Xf(x)) → B(x)
C(Xf(x)) → C(x)
D1(Xf(x)) → D1(x)
F(Xf(x)) → F(x)
G(Xf(x)) → G(x)
A(Xg(x)) → A(x)
B(Xg(x)) → B(x)
C(Xg(x)) → C(x)
D1(Xg(x)) → D1(x)
F(Xg(x)) → F(x)
G(Xg(x)) → G(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)
D2(Yf(x)) → F(D(x))
D2(Yf(x)) → D2(x)
D2(Yg(x)) → G(D(x))
D2(Yg(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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 7 SCCs with 6 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

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

G(Xb(x)) → G(x)
G(Xa(x)) → G(x)
G(Xc(x)) → G(x)
G(Xd(x)) → G(x)
G(Xf(x)) → G(x)
G(Xg(x)) → G(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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:

G(Xb(x)) → G(x)
G(Xa(x)) → G(x)
G(Xc(x)) → G(x)
G(Xd(x)) → G(x)
G(Xf(x)) → G(x)
G(Xg(x)) → G(x)

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

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

(15) Obligation:

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

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

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

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

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

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

  • G(Xf(x)) → G(x)
    The graph contains the following edges 1 > 1

  • G(Xg(x)) → G(x)
    The graph contains the following edges 1 > 1

(17) YES

(18) Obligation:

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

F(Xb(x)) → F(x)
F(Xa(x)) → F(x)
F(Xc(x)) → F(x)
F(Xd(x)) → F(x)
F(Xf(x)) → F(x)
F(Xg(x)) → F(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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:

F(Xb(x)) → F(x)
F(Xa(x)) → F(x)
F(Xc(x)) → F(x)
F(Xd(x)) → F(x)
F(Xf(x)) → F(x)
F(Xg(x)) → F(x)

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

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

(22) Obligation:

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

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

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

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

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

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

  • F(Xf(x)) → F(x)
    The graph contains the following edges 1 > 1

  • F(Xg(x)) → F(x)
    The graph contains the following edges 1 > 1

(24) YES

(25) 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)
D1(Xf(x)) → D1(x)
D1(Xg(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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:

D1(Xb(x)) → D1(x)
D1(Xa(x)) → D1(x)
D1(Xc(x)) → D1(x)
D1(Xd(x)) → D1(x)
D1(Xf(x)) → D1(x)
D1(Xg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

(29) 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)
D1(Xf(x)) → D1(x)
D1(Xg(x)) → D1(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:

  • 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

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

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

(31) YES

(32) 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)
C(Xf(x)) → C(x)
C(Xg(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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:

C(Xb(x)) → C(x)
C(Xa(x)) → C(x)
C(Xc(x)) → C(x)
C(Xd(x)) → C(x)
C(Xf(x)) → C(x)
C(Xg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

(36) 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)
C(Xf(x)) → C(x)
C(Xg(x)) → C(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:

  • 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

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

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

(38) YES

(39) 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)
B(Xf(x)) → B(x)
B(Xg(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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:

B(Xb(x)) → B(x)
B(Xa(x)) → B(x)
B(Xc(x)) → B(x)
B(Xd(x)) → B(x)
B(Xf(x)) → B(x)
B(Xg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

(43) 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)
B(Xf(x)) → B(x)
B(Xg(x)) → B(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:

  • 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

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

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

(45) YES

(46) 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)
A(Xf(x)) → A(x)
A(Xg(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

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

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

(48) 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)
A(Xf(x)) → A(x)
A(Xg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

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

(49) 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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

(50) 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)
A(Xf(x)) → A(x)
A(Xg(x)) → A(x)

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

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

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

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

(52) YES

(53) 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)
D2(Yf(x)) → D2(x)
D2(Yg(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))
f(Xa(x)) → Xa(f(x))
g(Xa(x)) → Xa(g(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))
f(Xb(x)) → Xb(f(x))
g(Xb(x)) → Xb(g(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))
f(Xc(x)) → Xc(f(x))
g(Xc(x)) → Xc(g(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))
f(Xd(x)) → Xd(f(x))
g(Xd(x)) → Xd(g(x))
a(Xf(x)) → Xf(a(x))
b(Xf(x)) → Xf(b(x))
c(Xf(x)) → Xf(c(x))
d(Xf(x)) → Xf(d(x))
f(Xf(x)) → Xf(f(x))
g(Xf(x)) → Xf(g(x))
a(Xg(x)) → Xg(a(x))
b(Xg(x)) → Xg(b(x))
c(Xg(x)) → Xg(c(x))
d(Xg(x)) → Xg(d(x))
f(Xg(x)) → Xg(f(x))
g(Xg(x)) → Xg(g(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))
f(L(x)) → L(Yf(x))
g(L(x)) → L(Yg(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(Yf(x)) → f(D(x))
D(Yg(x)) → g(D(x))

The set Q consists of the following terms:

a(Xa(x0))
b(Xa(x0))
c(Xa(x0))
d(Xa(x0))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

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

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

(55) 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)
D2(Yf(x)) → D2(x)
D2(Yg(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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

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

(56) 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))
f(Xa(x0))
g(Xa(x0))
a(Xb(x0))
b(Xb(x0))
c(Xb(x0))
d(Xb(x0))
f(Xb(x0))
g(Xb(x0))
a(Xc(x0))
b(Xc(x0))
c(Xc(x0))
d(Xc(x0))
f(Xc(x0))
g(Xc(x0))
a(Xd(x0))
b(Xd(x0))
c(Xd(x0))
d(Xd(x0))
f(Xd(x0))
g(Xd(x0))
a(Xf(x0))
b(Xf(x0))
c(Xf(x0))
d(Xf(x0))
f(Xf(x0))
g(Xf(x0))
a(Xg(x0))
b(Xg(x0))
c(Xg(x0))
d(Xg(x0))
f(Xg(x0))
g(Xg(x0))
a(L(x0))
b(L(x0))
c(L(x0))
d(L(x0))
f(L(x0))
g(L(x0))
D(Ya(x0))
D(Yb(x0))
D(Yc(x0))
D(Yd(x0))
D(Yf(x0))
D(Yg(x0))

(57) 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)
D2(Yf(x)) → D2(x)
D2(Yg(x)) → D2(x)

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

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

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

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

(59) YES