Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema

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

0 QTRS

↳1 FlatCCProof (⇔, 0 ms)

↳2 QTRS

↳3 RootLabelingProof (⇔, 0 ms)

↳4 QTRS

↳5 QTRSRRRProof (⇔, 117 ms)

↳6 QTRS

↳7 DependencyPairsProof (⇔, 143 ms)

↳8 QDP

↳9 QDPOrderProof (⇔, 687 ms)

↳10 QDP

↳11 DependencyGraphProof (⇔, 0 ms)

↳12 AND

    ↳13 QDP

        ↳14 QDPOrderProof (⇔, 69 ms)

        ↳15 QDP

        ↳16 DependencyGraphProof (⇔, 0 ms)

        ↳17 TRUE

    ↳18 QDP

        ↳19 UsableRulesProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

    ↳23 QDP

        ↳24 QDPOrderProof (⇔, 73 ms)

        ↳25 QDP

        ↳26 PisEmptyProof (⇔, 0 ms)

        ↳27 YES

    ↳28 QDP

        ↳29 QDPOrderProof (⇔, 77 ms)

        ↳30 QDP

        ↳31 PisEmptyProof (⇔, 0 ms)

        ↳32 YES

(0) Obligation:

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

s(b(x)) → b(s(s(s(x))))
s(b(s(x))) → b(t(x))
t(b(x)) → b(s(x))
t(b(s(x))) → u(t(b(x)))
b(u(x)) → b(s(x))
t(s(x)) → t(t(x))
t(u(x)) → u(t(x))
s(u(x)) → s(s(x))

Q is empty.

(1) FlatCCProof (EQUIVALENT transformation)

We used flat context closure [ROOTLAB] As Q is empty the flat context closure was sound AND complete.

(2) Obligation:

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

b(u(x)) → b(s(x))
t(s(x)) → t(t(x))
s(u(x)) → s(s(x))
s(s(b(x))) → s(b(s(s(s(x)))))
b(s(b(x))) → b(b(s(s(s(x)))))
t(s(b(x))) → t(b(s(s(s(x)))))
u(s(b(x))) → u(b(s(s(s(x)))))
s(s(b(s(x)))) → s(b(t(x)))
b(s(b(s(x)))) → b(b(t(x)))
t(s(b(s(x)))) → t(b(t(x)))
u(s(b(s(x)))) → u(b(t(x)))
s(t(b(x))) → s(b(s(x)))
b(t(b(x))) → b(b(s(x)))
t(t(b(x))) → t(b(s(x)))
u(t(b(x))) → u(b(s(x)))
s(t(b(s(x)))) → s(u(t(b(x))))
b(t(b(s(x)))) → b(u(t(b(x))))
t(t(b(s(x)))) → t(u(t(b(x))))
u(t(b(s(x)))) → u(u(t(b(x))))
s(t(u(x))) → s(u(t(x)))
b(t(u(x))) → b(u(t(x)))
t(t(u(x))) → t(u(t(x)))
u(t(u(x))) → u(u(t(x)))

Q is empty.

(3) RootLabelingProof (EQUIVALENT transformation)

We used plain root labeling [ROOTLAB] with the following heuristic: LabelAll: All function symbols get labeled
As Q is empty the root labeling was sound AND complete.

(4) Obligation:

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

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{s_1}(x)) → b_{s_1}(s_{s_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{s_1}(x)) → s_{s_1}(s_{s_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
u_{s_1}(s_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
u_{s_1}(s_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
u_{s_1}(s_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
u_{s_1}(s_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
u_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{b_1}(b_{t_1}(t_{b_1}(x)))
u_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{b_1}(b_{t_1}(t_{u_1}(x)))
u_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{b_1}(b_{t_1}(t_{s_1}(x)))
u_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{s_1}(x))) → s_{u_1}(u_{t_1}(t_{s_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{s_1}(x))) → b_{u_1}(u_{t_1}(t_{s_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{s_1}(x))) → t_{u_1}(u_{t_1}(t_{s_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{s_1}(x))) → u_{u_1}(u_{t_1}(t_{s_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(b_{b_1}(x₁)) = x₁
POL(b_{s_1}(x₁)) = x₁
POL(b_{t_1}(x₁)) = x₁
POL(b_{u_1}(x₁)) = x₁
POL(s_{b_1}(x₁)) = x₁
POL(s_{s_1}(x₁)) = x₁
POL(s_{t_1}(x₁)) = x₁
POL(s_{u_1}(x₁)) = x₁
POL(t_{b_1}(x₁)) = x₁
POL(t_{s_1}(x₁)) = x₁
POL(t_{t_1}(x₁)) = x₁
POL(t_{u_1}(x₁)) = x₁
POL(u_{b_1}(x₁)) = x₁
POL(u_{s_1}(x₁)) = 1 + x₁
POL(u_{t_1}(x₁)) = x₁
POL(u_{u_1}(x₁)) = x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

b_{u_1}(u_{s_1}(x)) → b_{s_1}(s_{s_1}(x))
s_{u_1}(u_{s_1}(x)) → s_{s_1}(s_{s_1}(x))
u_{s_1}(s_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
u_{s_1}(s_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
u_{s_1}(s_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
u_{s_1}(s_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
u_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{b_1}(b_{t_1}(t_{b_1}(x)))
u_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{b_1}(b_{t_1}(t_{u_1}(x)))
u_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{b_1}(b_{t_1}(t_{s_1}(x)))
u_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{u_1}(u_{s_1}(x))) → s_{u_1}(u_{t_1}(t_{s_1}(x)))
b_{t_1}(t_{u_1}(u_{s_1}(x))) → b_{u_1}(u_{t_1}(t_{s_1}(x)))
t_{t_1}(t_{u_1}(u_{s_1}(x))) → t_{u_1}(u_{t_1}(t_{s_1}(x)))
u_{t_1}(t_{u_1}(u_{s_1}(x))) → u_{u_1}(u_{t_1}(t_{s_1}(x)))

(6) Obligation:

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

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

Q is empty.

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

B_{U_1}(u_{b_1}(x)) → B_{S_1}(s_{b_1}(x))
B_{U_1}(u_{u_1}(x)) → B_{S_1}(s_{u_1}(x))
B_{U_1}(u_{u_1}(x)) → S_{U_1}(x)
B_{U_1}(u_{t_1}(x)) → B_{S_1}(s_{t_1}(x))
B_{U_1}(u_{t_1}(x)) → S_{T_1}(x)
T_{S_1}(s_{b_1}(x)) → T_{T_1}(t_{b_1}(x))
T_{S_1}(s_{u_1}(x)) → T_{T_1}(t_{u_1}(x))
T_{S_1}(s_{s_1}(x)) → T_{T_1}(t_{s_1}(x))
T_{S_1}(s_{s_1}(x)) → T_{S_1}(x)
T_{S_1}(s_{t_1}(x)) → T_{T_1}(t_{t_1}(x))
T_{S_1}(s_{t_1}(x)) → T_{T_1}(x)
S_{U_1}(u_{b_1}(x)) → S_{S_1}(s_{b_1}(x))
S_{U_1}(u_{u_1}(x)) → S_{S_1}(s_{u_1}(x))
S_{U_1}(u_{u_1}(x)) → S_{U_1}(x)
S_{U_1}(u_{t_1}(x)) → S_{S_1}(s_{t_1}(x))
S_{U_1}(u_{t_1}(x)) → S_{T_1}(x)
S_{S_1}(s_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{b_1}(x))))
S_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{s_1}(s_{b_1}(x)))
S_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{b_1}(x))
S_{S_1}(s_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{u_1}(x))))
S_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{s_1}(s_{u_1}(x)))
S_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{u_1}(x))
S_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
S_{S_1}(s_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{s_1}(x))))
S_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(s_{s_1}(x)))
S_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
S_{S_1}(s_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{t_1}(x))))
S_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{s_1}(s_{t_1}(x)))
S_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{t_1}(x))
S_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
B_{S_1}(s_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{b_1}(x))))
B_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{s_1}(s_{b_1}(x)))
B_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{b_1}(x))
B_{S_1}(s_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{u_1}(x))))
B_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{s_1}(s_{u_1}(x)))
B_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{u_1}(x))
B_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
B_{S_1}(s_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{s_1}(x))))
B_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(s_{s_1}(x)))
B_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
B_{S_1}(s_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{t_1}(x))))
B_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{s_1}(s_{t_1}(x)))
B_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{t_1}(x))
B_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
T_{S_1}(s_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{b_1}(x))))
T_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{s_1}(s_{b_1}(x)))
T_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{b_1}(x))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{u_1}(x))))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{s_1}(s_{u_1}(x)))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{u_1}(x))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
T_{S_1}(s_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{s_1}(x))))
T_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(s_{s_1}(x)))
T_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
T_{S_1}(s_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{t_1}(x))))
T_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{s_1}(s_{t_1}(x)))
T_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{t_1}(x))
T_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
S_{S_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{T_1}(t_{b_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{T_1}(t_{u_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{T_1}(t_{s_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → T_{S_1}(x)
S_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(t_{t_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → T_{T_1}(x)
B_{S_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{T_1}(t_{b_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{T_1}(t_{u_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{T_1}(t_{s_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → T_{S_1}(x)
B_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(t_{t_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → T_{T_1}(x)
T_{S_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{T_1}(t_{b_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{T_1}(t_{u_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{T_1}(t_{s_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → T_{S_1}(x)
T_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(t_{t_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → T_{T_1}(x)
S_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
S_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
S_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
S_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
S_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
S_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
B_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
B_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
B_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
B_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
B_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
B_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
T_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
T_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
T_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
T_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
T_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
T_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
T_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
U_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
U_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
U_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
U_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
U_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
U_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
U_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
T_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
T_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
T_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
U_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
U_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
U_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
S_{T_1}(t_{u_1}(u_{b_1}(x))) → S_{U_1}(u_{t_1}(t_{b_1}(x)))
S_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
S_{T_1}(t_{u_1}(u_{u_1}(x))) → S_{U_1}(u_{t_1}(t_{u_1}(x)))
S_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → S_{U_1}(u_{t_1}(t_{t_1}(x)))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)
B_{T_1}(t_{u_1}(u_{b_1}(x))) → B_{U_1}(u_{t_1}(t_{b_1}(x)))
B_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
B_{T_1}(t_{u_1}(u_{u_1}(x))) → B_{U_1}(u_{t_1}(t_{u_1}(x)))
B_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
B_{T_1}(t_{u_1}(u_{t_1}(x))) → B_{U_1}(u_{t_1}(t_{t_1}(x)))
B_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
B_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)
T_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
T_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
T_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
T_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)
U_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
U_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)

The TRS R consists of the following rules:

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(9) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

B_{U_1}(u_{b_1}(x)) → B_{S_1}(s_{b_1}(x))
B_{U_1}(u_{u_1}(x)) → B_{S_1}(s_{u_1}(x))
B_{U_1}(u_{t_1}(x)) → B_{S_1}(s_{t_1}(x))
T_{S_1}(s_{b_1}(x)) → T_{T_1}(t_{b_1}(x))
T_{S_1}(s_{u_1}(x)) → T_{T_1}(t_{u_1}(x))
T_{S_1}(s_{s_1}(x)) → T_{T_1}(t_{s_1}(x))
T_{S_1}(s_{t_1}(x)) → T_{T_1}(t_{t_1}(x))
T_{S_1}(s_{t_1}(x)) → T_{T_1}(x)
S_{U_1}(u_{b_1}(x)) → S_{S_1}(s_{b_1}(x))
S_{U_1}(u_{u_1}(x)) → S_{S_1}(s_{u_1}(x))
S_{U_1}(u_{t_1}(x)) → S_{S_1}(s_{t_1}(x))
S_{S_1}(s_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{b_1}(x))))
S_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{s_1}(s_{b_1}(x)))
S_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{b_1}(x))
S_{S_1}(s_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{u_1}(x))))
S_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{s_1}(s_{u_1}(x)))
S_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{u_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{s_1}(x))))
S_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(s_{s_1}(x)))
S_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
S_{S_1}(s_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{t_1}(x))))
S_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{s_1}(s_{t_1}(x)))
S_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{t_1}(x))
B_{S_1}(s_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{b_1}(x))))
B_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{s_1}(s_{b_1}(x)))
B_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{b_1}(x))
B_{S_1}(s_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{u_1}(x))))
B_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{s_1}(s_{u_1}(x)))
B_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{u_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{s_1}(x))))
B_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(s_{s_1}(x)))
B_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
B_{S_1}(s_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{t_1}(x))))
B_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{s_1}(s_{t_1}(x)))
B_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{t_1}(x))
T_{S_1}(s_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{b_1}(x))))
T_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{s_1}(s_{b_1}(x)))
T_{S_1}(s_{b_1}(b_{b_1}(x))) → S_{S_1}(s_{b_1}(x))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{u_1}(x))))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{s_1}(s_{u_1}(x)))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{S_1}(s_{u_1}(x))
T_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
T_{S_1}(s_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{s_1}(x))))
T_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(s_{s_1}(x)))
T_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(s_{s_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
T_{S_1}(s_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{s_1}(s_{s_1}(s_{t_1}(x))))
T_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{s_1}(s_{t_1}(x)))
T_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{S_1}(s_{t_1}(x))
T_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
S_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → T_{T_1}(x)
B_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → T_{T_1}(x)
T_{S_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{T_1}(t_{b_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{T_1}(t_{u_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{T_1}(t_{s_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → T_{S_1}(x)
T_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(t_{t_1}(x))
T_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → T_{T_1}(x)
S_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
S_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
S_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
S_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
S_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
S_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
B_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
B_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
B_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
B_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
B_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
B_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
T_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
T_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
T_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
T_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
T_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
U_{T_1}(t_{b_1}(b_{b_1}(x))) → B_{S_1}(s_{b_1}(x))
U_{T_1}(t_{b_1}(b_{u_1}(x))) → B_{S_1}(s_{u_1}(x))
U_{T_1}(t_{b_1}(b_{s_1}(x))) → B_{S_1}(s_{s_1}(x))
U_{T_1}(t_{b_1}(b_{s_1}(x))) → S_{S_1}(x)
U_{T_1}(t_{b_1}(b_{t_1}(x))) → B_{S_1}(s_{t_1}(x))
S_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
B_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
B_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
T_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
U_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{S_1}(x)
S_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
S_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)
B_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
B_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
B_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
B_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)

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

POL(B_{S_1}(x₁)) = x₁
POL(B_{T_1}(x₁)) = 1 + x₁
POL(B_{U_1}(x₁)) = 1 + x₁
POL(S_{S_1}(x₁)) = x₁
POL(S_{T_1}(x₁)) = 1 + x₁
POL(S_{U_1}(x₁)) = 1 + x₁
POL(T_{S_1}(x₁)) = 1 + x₁
POL(T_{T_1}(x₁)) = x₁
POL(U_{T_1}(x₁)) = x₁
POL(b_{b_1}(x₁)) = 1 + x₁
POL(b_{s_1}(x₁)) = x₁
POL(b_{t_1}(x₁)) = x₁
POL(b_{u_1}(x₁)) = x₁
POL(s_{b_1}(x₁)) = 1 + x₁
POL(s_{s_1}(x₁)) = x₁
POL(s_{t_1}(x₁)) = x₁
POL(s_{u_1}(x₁)) = x₁
POL(t_{b_1}(x₁)) = 1 + x₁
POL(t_{s_1}(x₁)) = x₁
POL(t_{t_1}(x₁)) = x₁
POL(t_{u_1}(x₁)) = x₁
POL(u_{b_1}(x₁)) = 1 + x₁
POL(u_{t_1}(x₁)) = x₁
POL(u_{u_1}(x₁)) = x₁

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

s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

(10) Obligation:

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

B_{U_1}(u_{u_1}(x)) → S_{U_1}(x)
B_{U_1}(u_{t_1}(x)) → S_{T_1}(x)
T_{S_1}(s_{s_1}(x)) → T_{S_1}(x)
S_{U_1}(u_{u_1}(x)) → S_{U_1}(x)
S_{U_1}(u_{t_1}(x)) → S_{T_1}(x)
S_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
S_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
B_{S_1}(s_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
B_{S_1}(s_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
S_{S_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{T_1}(t_{b_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{T_1}(t_{u_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{T_1}(t_{s_1}(x))
S_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → T_{S_1}(x)
S_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(t_{t_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{T_1}(t_{b_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{T_1}(t_{u_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{T_1}(t_{s_1}(x))
B_{S_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → T_{S_1}(x)
B_{S_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(t_{t_1}(x))
T_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
T_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
U_{T_1}(t_{b_1}(b_{u_1}(x))) → S_{U_1}(x)
U_{T_1}(t_{b_1}(b_{t_1}(x))) → S_{T_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
B_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{U_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
T_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
T_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
T_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
U_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → U_{T_1}(t_{b_1}(b_{b_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → B_{U_1}(x)
U_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → B_{T_1}(x)
S_{T_1}(t_{u_1}(u_{b_1}(x))) → S_{U_1}(u_{t_1}(t_{b_1}(x)))
S_{T_1}(t_{u_1}(u_{u_1}(x))) → S_{U_1}(u_{t_1}(t_{u_1}(x)))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → S_{U_1}(u_{t_1}(t_{t_1}(x)))
B_{T_1}(t_{u_1}(u_{b_1}(x))) → B_{U_1}(u_{t_1}(t_{b_1}(x)))
B_{T_1}(t_{u_1}(u_{u_1}(x))) → B_{U_1}(u_{t_1}(t_{u_1}(x)))
B_{T_1}(t_{u_1}(u_{t_1}(x))) → B_{U_1}(u_{t_1}(t_{t_1}(x)))
T_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
T_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
T_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
T_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)
U_{T_1}(t_{u_1}(u_{b_1}(x))) → U_{T_1}(t_{b_1}(x))
U_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)

The TRS R consists of the following rules:

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(11) DependencyGraphProof (EQUIVALENT transformation)

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

(12) Complex Obligation (AND)

(13) Obligation:

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

S_{U_1}(u_{t_1}(x)) → S_{T_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
S_{U_1}(u_{u_1}(x)) → S_{U_1}(x)
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
S_{T_1}(t_{u_1}(u_{b_1}(x))) → S_{U_1}(u_{t_1}(t_{b_1}(x)))
S_{T_1}(t_{u_1}(u_{u_1}(x))) → S_{U_1}(u_{t_1}(t_{u_1}(x)))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → S_{U_1}(u_{t_1}(t_{t_1}(x)))

The TRS R consists of the following rules:

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(14) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

S_{U_1}(u_{t_1}(x)) → S_{T_1}(x)
S_{U_1}(u_{u_1}(x)) → S_{U_1}(x)

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

POL(S_{T_1}(x₁)) = 1 + x₁
POL(S_{U_1}(x₁)) = 1 + x₁
POL(b_{b_1}(x₁)) = 0
POL(b_{s_1}(x₁)) = 1 + x₁
POL(b_{t_1}(x₁)) = 1 + x₁
POL(b_{u_1}(x₁)) = 1 + x₁
POL(s_{b_1}(x₁)) = 0
POL(s_{s_1}(x₁)) = 1 + x₁
POL(s_{t_1}(x₁)) = 1 + x₁
POL(s_{u_1}(x₁)) = 1 + x₁
POL(t_{b_1}(x₁)) = 1 + x₁
POL(t_{s_1}(x₁)) = 0
POL(t_{t_1}(x₁)) = 1 + x₁
POL(t_{u_1}(x₁)) = 1 + x₁
POL(u_{b_1}(x₁)) = 1 + x₁
POL(u_{t_1}(x₁)) = 1 + x₁
POL(u_{u_1}(x₁)) = 1 + x₁

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

u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))

(15) Obligation:

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

S_{T_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
S_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → S_{U_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
S_{T_1}(t_{u_1}(u_{b_1}(x))) → S_{U_1}(u_{t_1}(t_{b_1}(x)))
S_{T_1}(t_{u_1}(u_{u_1}(x))) → S_{U_1}(u_{t_1}(t_{u_1}(x)))
S_{T_1}(t_{u_1}(u_{t_1}(x))) → S_{U_1}(u_{t_1}(t_{t_1}(x)))

The TRS R consists of the following rules:

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(16) DependencyGraphProof (EQUIVALENT transformation)

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

(17) TRUE

(18) Obligation:

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

T_{S_1}(s_{s_1}(x)) → T_{S_1}(x)

The TRS R consists of the following rules:

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(19) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(20) Obligation:

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

T_{S_1}(s_{s_1}(x)) → T_{S_1}(x)

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

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

T_{S_1}(s_{s_1}(x)) → T_{S_1}(x)
The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

U_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))

The TRS R consists of the following rules:

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(24) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

U_{T_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → U_{T_1}(t_{b_1}(b_{s_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → U_{T_1}(t_{b_1}(b_{u_1}(x)))
U_{T_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → U_{T_1}(t_{b_1}(b_{t_1}(x)))

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

POL(U_{T_1}(x₁)) = x₁
POL(b_{b_1}(x₁)) = 0
POL(b_{s_1}(x₁)) = x₁
POL(b_{t_1}(x₁)) = x₁
POL(b_{u_1}(x₁)) = x₁
POL(s_{b_1}(x₁)) = 1
POL(s_{s_1}(x₁)) = 1 + x₁
POL(s_{t_1}(x₁)) = 1 + x₁
POL(s_{u_1}(x₁)) = 1 + x₁
POL(t_{b_1}(x₁)) = 1 + x₁
POL(t_{s_1}(x₁)) = 0
POL(t_{t_1}(x₁)) = 1 + x₁
POL(t_{u_1}(x₁)) = 1 + x₁
POL(u_{b_1}(x₁)) = 1 + x₁
POL(u_{t_1}(x₁)) = 1 + x₁
POL(u_{u_1}(x₁)) = 1 + x₁

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

b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))

(25) Obligation:

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

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(26) PisEmptyProof (EQUIVALENT transformation)

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

(27) YES

(28) Obligation:

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

T_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
U_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)
T_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
T_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)

The TRS R consists of the following rules:

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(29) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

T_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
U_{T_1}(t_{u_1}(u_{u_1}(x))) → U_{T_1}(t_{u_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
U_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)
T_{T_1}(t_{u_1}(u_{t_1}(x))) → U_{T_1}(t_{t_1}(x))
T_{T_1}(t_{u_1}(u_{t_1}(x))) → T_{T_1}(x)

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

POL(T_{T_1}(x₁)) = x₁
POL(U_{T_1}(x₁)) = x₁
POL(b_{b_1}(x₁)) = 0
POL(b_{s_1}(x₁)) = 1 + x₁
POL(b_{t_1}(x₁)) = 1 + x₁
POL(b_{u_1}(x₁)) = 1 + x₁
POL(s_{b_1}(x₁)) = 0
POL(s_{s_1}(x₁)) = 1 + x₁
POL(s_{t_1}(x₁)) = 1 + x₁
POL(s_{u_1}(x₁)) = 1 + x₁
POL(t_{b_1}(x₁)) = x₁
POL(t_{s_1}(x₁)) = 0
POL(t_{t_1}(x₁)) = 1 + x₁
POL(t_{u_1}(x₁)) = 1 + x₁
POL(u_{b_1}(x₁)) = x₁
POL(u_{t_1}(x₁)) = 1 + x₁
POL(u_{u_1}(x₁)) = 1 + x₁

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

t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

(30) Obligation:

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

b_{u_1}(u_{b_1}(x)) → b_{s_1}(s_{b_1}(x))
b_{u_1}(u_{u_1}(x)) → b_{s_1}(s_{u_1}(x))
b_{u_1}(u_{t_1}(x)) → b_{s_1}(s_{t_1}(x))
t_{s_1}(s_{b_1}(x)) → t_{t_1}(t_{b_1}(x))
t_{s_1}(s_{u_1}(x)) → t_{t_1}(t_{u_1}(x))
t_{s_1}(s_{s_1}(x)) → t_{t_1}(t_{s_1}(x))
t_{s_1}(s_{t_1}(x)) → t_{t_1}(t_{t_1}(x))
s_{u_1}(u_{b_1}(x)) → s_{s_1}(s_{b_1}(x))
s_{u_1}(u_{u_1}(x)) → s_{s_1}(s_{u_1}(x))
s_{u_1}(u_{t_1}(x)) → s_{s_1}(s_{t_1}(x))
s_{s_1}(s_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
s_{s_1}(s_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
s_{s_1}(s_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
b_{s_1}(s_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
b_{s_1}(s_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
b_{s_1}(s_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
b_{s_1}(s_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
t_{s_1}(s_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{b_1}(x)))))
t_{s_1}(s_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{u_1}(x)))))
t_{s_1}(s_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{s_1}(x)))))
t_{s_1}(s_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(s_{s_1}(s_{t_1}(x)))))
s_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{b_1}(b_{t_1}(t_{b_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{b_1}(b_{t_1}(t_{u_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{b_1}(b_{t_1}(t_{s_1}(x)))
s_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{b_1}(b_{t_1}(t_{t_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{b_1}(b_{t_1}(t_{b_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{b_1}(b_{t_1}(t_{u_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{b_1}(b_{t_1}(t_{s_1}(x)))
b_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{b_1}(b_{t_1}(t_{t_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{b_1}(b_{t_1}(t_{b_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{b_1}(b_{t_1}(t_{u_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{b_1}(b_{t_1}(t_{s_1}(x)))
t_{s_1}(s_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{b_1}(b_{t_1}(t_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{b_1}(x))) → s_{b_1}(b_{s_1}(s_{b_1}(x)))
s_{t_1}(t_{b_1}(b_{u_1}(x))) → s_{b_1}(b_{s_1}(s_{u_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(x))) → s_{b_1}(b_{s_1}(s_{s_1}(x)))
s_{t_1}(t_{b_1}(b_{t_1}(x))) → s_{b_1}(b_{s_1}(s_{t_1}(x)))
b_{t_1}(t_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{s_1}(s_{b_1}(x)))
b_{t_1}(t_{b_1}(b_{u_1}(x))) → b_{b_1}(b_{s_1}(s_{u_1}(x)))
b_{t_1}(t_{b_1}(b_{s_1}(x))) → b_{b_1}(b_{s_1}(s_{s_1}(x)))
b_{t_1}(t_{b_1}(b_{t_1}(x))) → b_{b_1}(b_{s_1}(s_{t_1}(x)))
t_{t_1}(t_{b_1}(b_{b_1}(x))) → t_{b_1}(b_{s_1}(s_{b_1}(x)))
t_{t_1}(t_{b_1}(b_{u_1}(x))) → t_{b_1}(b_{s_1}(s_{u_1}(x)))
t_{t_1}(t_{b_1}(b_{s_1}(x))) → t_{b_1}(b_{s_1}(s_{s_1}(x)))
t_{t_1}(t_{b_1}(b_{t_1}(x))) → t_{b_1}(b_{s_1}(s_{t_1}(x)))
u_{t_1}(t_{b_1}(b_{b_1}(x))) → u_{b_1}(b_{s_1}(s_{b_1}(x)))
u_{t_1}(t_{b_1}(b_{u_1}(x))) → u_{b_1}(b_{s_1}(s_{u_1}(x)))
u_{t_1}(t_{b_1}(b_{s_1}(x))) → u_{b_1}(b_{s_1}(s_{s_1}(x)))
u_{t_1}(t_{b_1}(b_{t_1}(x))) → u_{b_1}(b_{s_1}(s_{t_1}(x)))
s_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
s_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → s_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
b_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → b_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
t_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → t_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{b_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{b_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{u_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{u_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{s_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{s_1}(x))))
u_{t_1}(t_{b_1}(b_{s_1}(s_{t_1}(x)))) → u_{u_1}(u_{t_1}(t_{b_1}(b_{t_1}(x))))
s_{t_1}(t_{u_1}(u_{b_1}(x))) → s_{u_1}(u_{t_1}(t_{b_1}(x)))
s_{t_1}(t_{u_1}(u_{u_1}(x))) → s_{u_1}(u_{t_1}(t_{u_1}(x)))
s_{t_1}(t_{u_1}(u_{t_1}(x))) → s_{u_1}(u_{t_1}(t_{t_1}(x)))
b_{t_1}(t_{u_1}(u_{b_1}(x))) → b_{u_1}(u_{t_1}(t_{b_1}(x)))
b_{t_1}(t_{u_1}(u_{u_1}(x))) → b_{u_1}(u_{t_1}(t_{u_1}(x)))
b_{t_1}(t_{u_1}(u_{t_1}(x))) → b_{u_1}(u_{t_1}(t_{t_1}(x)))
t_{t_1}(t_{u_1}(u_{b_1}(x))) → t_{u_1}(u_{t_1}(t_{b_1}(x)))
t_{t_1}(t_{u_1}(u_{u_1}(x))) → t_{u_1}(u_{t_1}(t_{u_1}(x)))
t_{t_1}(t_{u_1}(u_{t_1}(x))) → t_{u_1}(u_{t_1}(t_{t_1}(x)))
u_{t_1}(t_{u_1}(u_{b_1}(x))) → u_{u_1}(u_{t_1}(t_{b_1}(x)))
u_{t_1}(t_{u_1}(u_{u_1}(x))) → u_{u_1}(u_{t_1}(t_{u_1}(x)))
u_{t_1}(t_{u_1}(u_{t_1}(x))) → u_{u_1}(u_{t_1}(t_{t_1}(x)))

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

(31) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) FlatCCProof (EQUIVALENT transformation)

(2) Obligation:

(3) RootLabelingProof (EQUIVALENT transformation)

(4) Obligation:

(5) QTRSRRRProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyPairsProof (EQUIVALENT transformation)

(8) Obligation:

(9) QDPOrderProof (EQUIVALENT transformation)

(10) Obligation:

(11) DependencyGraphProof (EQUIVALENT transformation)

(12) Complex Obligation (AND)

(13) Obligation:

(14) QDPOrderProof (EQUIVALENT transformation)

(15) Obligation:

(16) DependencyGraphProof (EQUIVALENT transformation)

(17) TRUE

(18) Obligation:

(19) UsableRulesProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) QDPOrderProof (EQUIVALENT transformation)

(25) Obligation:

(26) PisEmptyProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) QDPOrderProof (EQUIVALENT transformation)

(30) Obligation:

(31) PisEmptyProof (EQUIVALENT transformation)

(32) YES