Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/examples/collection/ab-baPhi-split.srs

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

0 QTRS

↳1 QTRS Reverse (⇔, 0 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 61 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 QDP

        ↳13 UsableRulesProof (⇔, 1 ms)

        ↳14 QDP

        ↳15 MRRProof (⇔, 150 ms)

        ↳16 QDP

        ↳17 PisEmptyProof (⇔, 0 ms)

        ↳18 YES

    ↳19 QDP

        ↳20 UsableRulesProof (⇔, 0 ms)

        ↳21 QDP

        ↳22 QDPSizeChangeProof (⇔, 0 ms)

        ↳23 YES

    ↳24 QDP

        ↳25 UsableRulesProof (⇔, 1 ms)

        ↳26 QDP

        ↳27 QDPOrderProof (⇔, 114 ms)

        ↳28 QDP

        ↳29 QDPOrderProof (⇔, 70 ms)

        ↳30 QDP

        ↳31 QDPOrderProof (⇔, 43 ms)

        ↳32 QDP

        ↳33 QDPOrderProof (⇔, 44 ms)

        ↳34 QDP

        ↳35 MRRProof (⇔, 125 ms)

        ↳36 QDP

        ↳37 MRRProof (⇔, 27 ms)

        ↳38 QDP

        ↳39 MRRProof (⇔, 32 ms)

        ↳40 QDP

        ↳41 MRRProof (⇔, 64 ms)

        ↳42 QDP

        ↳43 QDPOrderProof (⇔, 268 ms)

        ↳44 QDP

        ↳45 MRRProof (⇔, 43 ms)

        ↳46 QDP

        ↳47 MRRProof (⇔, 84 ms)

        ↳48 QDP

        ↳49 QDPOrderProof (⇔, 74 ms)

        ↳50 QDP

        ↳51 PisEmptyProof (⇔, 0 ms)

        ↳52 YES

(0) Obligation:

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

Begin(E(x)) → Wait(Right1(x))
Begin(L(x)) → Wait(Right2(x))
Begin(L(x)) → Wait(Right3(x))
Begin(Aa(x)) → Wait(Right4(x))
Begin(Ab(x)) → Wait(Right5(x))
Begin(b(L(x))) → Wait(Right6(x))
Begin(L(x)) → Wait(Right7(x))
Right1(R(End(x))) → Left(L(E(End(x))))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right4(R(End(x))) → Left(a(R(End(x))))
Right5(R(End(x))) → Left(b(R(End(x))))
Right6(a(End(x))) → Left(b(a(R(End(x)))))
Right7(a(b(End(x)))) → Left(b(a(R(End(x)))))
Right1(R(x)) → AR(Right1(x))
Right2(R(x)) → AR(Right2(x))
Right3(R(x)) → AR(Right3(x))
Right4(R(x)) → AR(Right4(x))
Right5(R(x)) → AR(Right5(x))
Right6(R(x)) → AR(Right6(x))
Right7(R(x)) → AR(Right7(x))
Right1(E(x)) → AE(Right1(x))
Right2(E(x)) → AE(Right2(x))
Right3(E(x)) → AE(Right3(x))
Right4(E(x)) → AE(Right4(x))
Right5(E(x)) → AE(Right5(x))
Right6(E(x)) → AE(Right6(x))
Right7(E(x)) → AE(Right7(x))
Right1(L(x)) → AL(Right1(x))
Right2(L(x)) → AL(Right2(x))
Right3(L(x)) → AL(Right3(x))
Right4(L(x)) → AL(Right4(x))
Right5(L(x)) → AL(Right5(x))
Right6(L(x)) → AL(Right6(x))
Right7(L(x)) → AL(Right7(x))
Right1(a(x)) → AAa(Right1(x))
Right2(a(x)) → AAa(Right2(x))
Right3(a(x)) → AAa(Right3(x))
Right4(a(x)) → AAa(Right4(x))
Right5(a(x)) → AAa(Right5(x))
Right6(a(x)) → AAa(Right6(x))
Right7(a(x)) → AAa(Right7(x))
Right1(Aa(x)) → AAAa(Right1(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right1(b(x)) → AAb(Right1(x))
Right2(b(x)) → AAb(Right2(x))
Right3(b(x)) → AAb(Right3(x))
Right4(b(x)) → AAb(Right4(x))
Right5(b(x)) → AAb(Right5(x))
Right6(b(x)) → AAb(Right6(x))
Right7(b(x)) → AAb(Right7(x))
Right1(Ab(x)) → AAAb(Right1(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right7(Ab(x)) → AAAb(Right7(x))
AR(Left(x)) → Left(R(x))
AE(Left(x)) → Left(E(x))
AL(Left(x)) → Left(L(x))
AAa(Left(x)) → Left(a(x))
AAAa(Left(x)) → Left(Aa(x))
AAb(Left(x)) → Left(b(x))
AAAb(Left(x)) → Left(Ab(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
a(b(L(x))) → b(a(R(x)))

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
End(a(Right6(x))) → End(R(a(b(Left(x)))))
End(b(a(Right7(x)))) → End(R(a(b(Left(x)))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
E(R(x)) → E(L(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))
L(b(a(x))) → R(a(b(x)))

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

END(R(Right1(x))) → END(E(L(Left(x))))
END(R(Right1(x))) → E¹(L(Left(x)))
END(R(Right1(x))) → L¹(Left(x))
END(R(Right1(x))) → LEFT(x)
END(a(Right2(x))) → END(Aa(L(Left(x))))
END(a(Right2(x))) → AA(L(Left(x)))
END(a(Right2(x))) → L¹(Left(x))
END(a(Right2(x))) → LEFT(x)
END(b(Right3(x))) → END(Ab(L(Left(x))))
END(b(Right3(x))) → AB(L(Left(x)))
END(b(Right3(x))) → L¹(Left(x))
END(b(Right3(x))) → LEFT(x)
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right4(x))) → R¹(a(Left(x)))
END(R(Right4(x))) → A(Left(x))
END(R(Right4(x))) → LEFT(x)
END(R(Right5(x))) → END(R(b(Left(x))))
END(R(Right5(x))) → R¹(b(Left(x)))
END(R(Right5(x))) → B(Left(x))
END(R(Right5(x))) → LEFT(x)
END(a(Right6(x))) → END(R(a(b(Left(x)))))
END(a(Right6(x))) → R¹(a(b(Left(x))))
END(a(Right6(x))) → A(b(Left(x)))
END(a(Right6(x))) → B(Left(x))
END(a(Right6(x))) → LEFT(x)
END(b(a(Right7(x)))) → END(R(a(b(Left(x)))))
END(b(a(Right7(x)))) → R¹(a(b(Left(x))))
END(b(a(Right7(x)))) → A(b(Left(x)))
END(b(a(Right7(x)))) → B(Left(x))
END(b(a(Right7(x)))) → LEFT(x)
LEFT(AR(x)) → R¹(Left(x))
LEFT(AR(x)) → LEFT(x)
LEFT(AE(x)) → E¹(Left(x))
LEFT(AE(x)) → LEFT(x)
LEFT(AL(x)) → L¹(Left(x))
LEFT(AL(x)) → LEFT(x)
LEFT(AAa(x)) → A(Left(x))
LEFT(AAa(x)) → LEFT(x)
LEFT(AAAa(x)) → AA(Left(x))
LEFT(AAAa(x)) → LEFT(x)
LEFT(AAb(x)) → B(Left(x))
LEFT(AAb(x)) → LEFT(x)
LEFT(AAAb(x)) → AB(Left(x))
LEFT(AAAb(x)) → LEFT(x)
E¹(R(x)) → E¹(L(x))
E¹(R(x)) → L¹(x)
L¹(a(x)) → AA(L(x))
L¹(a(x)) → L¹(x)
L¹(b(x)) → AB(L(x))
L¹(b(x)) → L¹(x)
AA(R(x)) → R¹(a(x))
AA(R(x)) → A(x)
AB(R(x)) → R¹(b(x))
AB(R(x)) → B(x)
L¹(b(a(x))) → R¹(a(b(x)))
L¹(b(a(x))) → A(b(x))
L¹(b(a(x))) → B(x)

The TRS R consists of the following rules:

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
End(a(Right6(x))) → End(R(a(b(Left(x)))))
End(b(a(Right7(x)))) → End(R(a(b(Left(x)))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
E(R(x)) → E(L(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))
L(b(a(x))) → R(a(b(x)))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

L¹(b(x)) → L¹(x)
L¹(a(x)) → L¹(x)

The TRS R consists of the following rules:

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
End(a(Right6(x))) → End(R(a(b(Left(x)))))
End(b(a(Right7(x)))) → End(R(a(b(Left(x)))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
E(R(x)) → E(L(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))
L(b(a(x))) → R(a(b(x)))

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

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

(9) Obligation:

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

L¹(b(x)) → L¹(x)
L¹(a(x)) → L¹(x)

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

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

L¹(b(x)) → L¹(x)
The graph contains the following edges 1 > 1
L¹(a(x)) → L¹(x)
The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

E¹(R(x)) → E¹(L(x))

The TRS R consists of the following rules:

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
End(a(Right6(x))) → End(R(a(b(Left(x)))))
End(b(a(Right7(x)))) → End(R(a(b(Left(x)))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
E(R(x)) → E(L(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))
L(b(a(x))) → R(a(b(x)))

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

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

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

E¹(R(x)) → E¹(L(x))

The TRS R consists of the following rules:

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))

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

(15) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

E¹(R(x)) → E¹(L(x))

Strictly oriented rules of the TRS R:

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right7(x)) → Right7(AL(x))
L(b(a(x))) → R(a(b(x)))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = 1 + x₁
POL(AAb(x₁)) = x₁
POL(AL(x₁)) = x₁
POL(AR(x₁)) = x₁
POL(Aa(x₁)) = 2 + 2·x₁
POL(Ab(x₁)) = 2·x₁
POL(Begin(x₁)) = 1 + x₁
POL(E¹(x₁)) = 3·x₁
POL(L(x₁)) = 2·x₁
POL(R(x₁)) = 1 + 2·x₁
POL(Right1(x₁)) = 3 + x₁
POL(Right2(x₁)) = 1 + x₁
POL(Right3(x₁)) = 1 + x₁
POL(Right4(x₁)) = 1 + x₁
POL(Right5(x₁)) = x₁
POL(Right6(x₁)) = x₁
POL(Right7(x₁)) = 2 + 2·x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = 1 + 2·x₁
POL(b(x₁)) = 2·x₁

(16) Obligation:

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

L(Begin(x)) → Right7(Wait(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))

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

(17) PisEmptyProof (EQUIVALENT transformation)

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

(18) YES

(19) Obligation:

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

LEFT(AE(x)) → LEFT(x)
LEFT(AR(x)) → LEFT(x)
LEFT(AL(x)) → LEFT(x)
LEFT(AAa(x)) → LEFT(x)
LEFT(AAAa(x)) → LEFT(x)
LEFT(AAb(x)) → LEFT(x)
LEFT(AAAb(x)) → LEFT(x)

The TRS R consists of the following rules:

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
End(a(Right6(x))) → End(R(a(b(Left(x)))))
End(b(a(Right7(x)))) → End(R(a(b(Left(x)))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
E(R(x)) → E(L(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))
L(b(a(x))) → R(a(b(x)))

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

(20) UsableRulesProof (EQUIVALENT transformation)

(21) Obligation:

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

LEFT(AE(x)) → LEFT(x)
LEFT(AR(x)) → LEFT(x)
LEFT(AL(x)) → LEFT(x)
LEFT(AAa(x)) → LEFT(x)
LEFT(AAAa(x)) → LEFT(x)
LEFT(AAb(x)) → LEFT(x)
LEFT(AAAb(x)) → LEFT(x)

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

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

LEFT(AE(x)) → LEFT(x)
The graph contains the following edges 1 > 1
LEFT(AR(x)) → LEFT(x)
The graph contains the following edges 1 > 1
LEFT(AL(x)) → LEFT(x)
The graph contains the following edges 1 > 1
LEFT(AAa(x)) → LEFT(x)
The graph contains the following edges 1 > 1
LEFT(AAAa(x)) → LEFT(x)
The graph contains the following edges 1 > 1
LEFT(AAb(x)) → LEFT(x)
The graph contains the following edges 1 > 1
LEFT(AAAb(x)) → LEFT(x)
The graph contains the following edges 1 > 1

(23) YES

(24) Obligation:

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

END(a(Right2(x))) → END(Aa(L(Left(x))))
END(R(Right1(x))) → END(E(L(Left(x))))
END(b(Right3(x))) → END(Ab(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))
END(a(Right6(x))) → END(R(a(b(Left(x)))))
END(b(a(Right7(x)))) → END(R(a(b(Left(x)))))

The TRS R consists of the following rules:

E(Begin(x)) → Right1(Wait(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
Aa(Begin(x)) → Right4(Wait(x))
Ab(Begin(x)) → Right5(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
End(R(Right1(x))) → End(E(L(Left(x))))
End(a(Right2(x))) → End(Aa(L(Left(x))))
End(b(Right3(x))) → End(Ab(L(Left(x))))
End(R(Right4(x))) → End(R(a(Left(x))))
End(R(Right5(x))) → End(R(b(Left(x))))
End(a(Right6(x))) → End(R(a(b(Left(x)))))
End(b(a(Right7(x)))) → End(R(a(b(Left(x)))))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
E(R(x)) → E(L(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
Aa(R(x)) → R(a(x))
Ab(R(x)) → R(b(x))
L(b(a(x))) → R(a(b(x)))

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

(25) UsableRulesProof (EQUIVALENT transformation)

(26) Obligation:

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

END(a(Right2(x))) → END(Aa(L(Left(x))))
END(R(Right1(x))) → END(E(L(Left(x))))
END(b(Right3(x))) → END(Ab(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))
END(a(Right6(x))) → END(R(a(b(Left(x)))))
END(b(a(Right7(x)))) → END(R(a(b(Left(x)))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))

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

(27) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

END(a(Right6(x))) → END(R(a(b(Left(x)))))
END(b(a(Right7(x)))) → END(R(a(b(Left(x)))))

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

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = x₁
POL(AL(x₁)) = x₁
POL(AR(x₁)) = x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Begin(x₁)) = x₁
POL(E(x₁)) = 1
POL(END(x₁)) = x₁
POL(L(x₁)) = 1
POL(Left(x₁)) = 0
POL(R(x₁)) = 1
POL(Right1(x₁)) = 0
POL(Right2(x₁)) = 0
POL(Right3(x₁)) = 0
POL(Right4(x₁)) = 0
POL(Right5(x₁)) = 0
POL(Right6(x₁)) = 1
POL(Right7(x₁)) = 0
POL(Wait(x₁)) = x₁
POL(a(x₁)) = 1 + x₁
POL(b(x₁)) = 1 + x₁

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

L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))

(28) Obligation:

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

END(a(Right2(x))) → END(Aa(L(Left(x))))
END(R(Right1(x))) → END(E(L(Left(x))))
END(b(Right3(x))) → END(Ab(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(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.

END(a(Right2(x))) → END(Aa(L(Left(x))))

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

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = x₁
POL(AL(x₁)) = x₁
POL(AR(x₁)) = x₁
POL(Aa(x₁)) = 0
POL(Ab(x₁)) = 0
POL(Begin(x₁)) = x₁
POL(E(x₁)) = 0
POL(END(x₁)) = x₁
POL(L(x₁)) = 0
POL(Left(x₁)) = 0
POL(R(x₁)) = 0
POL(Right1(x₁)) = 0
POL(Right2(x₁)) = 0
POL(Right3(x₁)) = 0
POL(Right4(x₁)) = 0
POL(Right5(x₁)) = 0
POL(Right6(x₁)) = 0
POL(Right7(x₁)) = 0
POL(Wait(x₁)) = x₁
POL(a(x₁)) = 1
POL(b(x₁)) = 0

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

Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))

(30) Obligation:

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

END(R(Right1(x))) → END(E(L(Left(x))))
END(b(Right3(x))) → END(Ab(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))

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

(31) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

END(b(Right3(x))) → END(Ab(L(Left(x))))

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

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = x₁
POL(AL(x₁)) = x₁
POL(AR(x₁)) = x₁
POL(Aa(x₁)) = 0
POL(Ab(x₁)) = 0
POL(Begin(x₁)) = x₁
POL(E(x₁)) = 0
POL(END(x₁)) = x₁
POL(L(x₁)) = 0
POL(Left(x₁)) = 0
POL(R(x₁)) = 0
POL(Right1(x₁)) = 0
POL(Right2(x₁)) = 0
POL(Right3(x₁)) = 0
POL(Right4(x₁)) = 0
POL(Right5(x₁)) = 0
POL(Right6(x₁)) = 0
POL(Right7(x₁)) = 0
POL(Wait(x₁)) = x₁
POL(a(x₁)) = 0
POL(b(x₁)) = 1

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

E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))

(32) Obligation:

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

END(R(Right1(x))) → END(E(L(Left(x))))
END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))

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

(33) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

END(R(Right1(x))) → END(E(L(Left(x))))

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

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = x₁
POL(AL(x₁)) = x₁
POL(AR(x₁)) = x₁
POL(Aa(x₁)) = 0
POL(Ab(x₁)) = 0
POL(Begin(x₁)) = x₁
POL(E(x₁)) = 0
POL(END(x₁)) = x₁
POL(L(x₁)) = 0
POL(Left(x₁)) = 0
POL(R(x₁)) = 1
POL(Right1(x₁)) = 0
POL(Right2(x₁)) = 0
POL(Right3(x₁)) = 0
POL(Right4(x₁)) = 0
POL(Right5(x₁)) = 0
POL(Right6(x₁)) = 0
POL(Right7(x₁)) = 0
POL(Wait(x₁)) = x₁
POL(a(x₁)) = 0
POL(b(x₁)) = 0

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

E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))

(34) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Begin(x)) → Right1(Wait(x))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))
E(R(x)) → E(L(x))

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

(35) MRRProof (EQUIVALENT transformation)

E(Begin(x)) → Right1(Wait(x))
E(Right6(x)) → Right6(AE(x))
E(Right7(x)) → Right7(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = 1 + 2·x₁
POL(AL(x₁)) = 2·x₁
POL(AR(x₁)) = 2·x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Begin(x₁)) = 2·x₁
POL(E(x₁)) = 2 + 2·x₁
POL(END(x₁)) = x₁
POL(L(x₁)) = 2·x₁
POL(Left(x₁)) = 2·x₁
POL(R(x₁)) = 2·x₁
POL(Right1(x₁)) = 2·x₁
POL(Right2(x₁)) = 2·x₁
POL(Right3(x₁)) = 2·x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = 2·x₁
POL(Right6(x₁)) = x₁
POL(Right7(x₁)) = x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(36) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right1(x)) → Right1(AR(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right1(x)) → Right1(AL(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right1(x)) → Right1(AE(x))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(R(x)) → E(L(x))

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

(37) MRRProof (EQUIVALENT transformation)

R(Right1(x)) → Right1(AR(x))
L(Right1(x)) → Right1(AL(x))
E(Right1(x)) → Right1(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = 2·x₁
POL(AL(x₁)) = 2·x₁
POL(AR(x₁)) = 2·x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Begin(x₁)) = 2·x₁
POL(E(x₁)) = 2·x₁
POL(END(x₁)) = 2·x₁
POL(L(x₁)) = 2·x₁
POL(Left(x₁)) = 2·x₁
POL(R(x₁)) = 2·x₁
POL(Right1(x₁)) = 2 + x₁
POL(Right2(x₁)) = 2·x₁
POL(Right3(x₁)) = x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = 2·x₁
POL(Right6(x₁)) = x₁
POL(Right7(x₁)) = 2·x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(38) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right3(x)) → Right3(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right2(x)) → Right2(AL(x))
L(Right3(x)) → Right3(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right2(x)) → Right2(AE(x))
E(Right3(x)) → Right3(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(R(x)) → E(L(x))

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

(39) MRRProof (EQUIVALENT transformation)

R(Right3(x)) → Right3(AR(x))
R(Right6(x)) → Right6(AR(x))
R(Right7(x)) → Right7(AR(x))
L(Begin(x)) → Right2(Wait(x))
L(Begin(x)) → Right3(Wait(x))
L(b(Begin(x))) → Right6(Wait(x))
L(Begin(x)) → Right7(Wait(x))
L(Right3(x)) → Right3(AL(x))
L(Right6(x)) → Right6(AL(x))
L(Right7(x)) → Right7(AL(x))
E(Right3(x)) → Right3(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = 2·x₁
POL(AL(x₁)) = 2·x₁
POL(AR(x₁)) = 2·x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Begin(x₁)) = 2 + 2·x₁
POL(E(x₁)) = 2·x₁
POL(END(x₁)) = x₁
POL(L(x₁)) = 2·x₁
POL(Left(x₁)) = 2·x₁
POL(R(x₁)) = 2·x₁
POL(Right1(x₁)) = 2·x₁
POL(Right2(x₁)) = 3·x₁
POL(Right3(x₁)) = 1 + 2·x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = 2·x₁
POL(Right6(x₁)) = 1 + 2·x₁
POL(Right7(x₁)) = 1 + 2·x₁
POL(Wait(x₁)) = 1 + x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(40) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right2(x)) → Right2(AE(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(R(x)) → E(L(x))

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

(41) MRRProof (EQUIVALENT transformation)

E(Right2(x)) → Right2(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AE(x₁)) = 1 + x₁
POL(AL(x₁)) = x₁
POL(AR(x₁)) = x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Begin(x₁)) = 2·x₁
POL(E(x₁)) = 2 + x₁
POL(END(x₁)) = 2·x₁
POL(L(x₁)) = x₁
POL(Left(x₁)) = 2·x₁
POL(R(x₁)) = x₁
POL(Right1(x₁)) = 2·x₁
POL(Right2(x₁)) = x₁
POL(Right3(x₁)) = 2·x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = 2·x₁
POL(Right6(x₁)) = 2·x₁
POL(Right7(x₁)) = x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁

(42) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))
END(R(Right5(x))) → END(R(b(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(R(x)) → E(L(x))

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

(43) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

END(R(Right5(x))) → END(R(b(Left(x))))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( END(x₁) ) = max{0, x₁ - 2}

POL( R(x₁) ) = 2x₁ + 2

POL( a(x₁) ) = 2x₁ + 2

POL( b(x₁) ) = 2x₁ + 1

POL( Left(x₁) ) = x₁

POL( AR(x₁) ) = 2x₁ + 2

POL( AE(x₁) ) = x₁

POL( E(x₁) ) = x₁

POL( AL(x₁) ) = 2x₁ + 1

POL( L(x₁) ) = 2x₁

POL( AAa(x₁) ) = 2x₁ + 2

POL( AAAa(x₁) ) = 2x₁ + 2

POL( Aa(x₁) ) = 2x₁ + 2

POL( AAb(x₁) ) = 2x₁ + 1

POL( AAAb(x₁) ) = 2x₁ + 2

POL( Ab(x₁) ) = 2x₁ + 2

POL( Wait(x₁) ) = 0

POL( Begin(x₁) ) = 0

POL( Right1(x₁) ) = x₁ + 1

POL( Right2(x₁) ) = max{0, -2}

POL( Right3(x₁) ) = max{0, -2}

POL( Right4(x₁) ) = 2x₁ + 2

POL( Right5(x₁) ) = 2x₁ + 2

POL( Right6(x₁) ) = 1

POL( Right7(x₁) ) = max{0, -2}

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

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(R(x)) → E(L(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))

(44) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right1(x)) → Right1(AAb(x))
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right1(x)) → Right1(AAAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(R(x)) → E(L(x))

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

(45) MRRProof (EQUIVALENT transformation)

b(Right1(x)) → Right1(AAb(x))
Ab(Right1(x)) → Right1(AAAb(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = 2·x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = 2·x₁
POL(AE(x₁)) = x₁
POL(AL(x₁)) = 2·x₁
POL(AR(x₁)) = 2·x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = 2·x₁
POL(Begin(x₁)) = 2·x₁
POL(E(x₁)) = x₁
POL(END(x₁)) = 2·x₁
POL(L(x₁)) = 2·x₁
POL(Left(x₁)) = 2·x₁
POL(R(x₁)) = 2·x₁
POL(Right1(x₁)) = 2 + 2·x₁
POL(Right2(x₁)) = x₁
POL(Right3(x₁)) = 2·x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = 2·x₁
POL(Right6(x₁)) = 2·x₁
POL(Right7(x₁)) = x₁
POL(Wait(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = 2·x₁

(46) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right2(x)) → Right2(AAb(x))
b(Right3(x)) → Right3(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right5(x)) → Right5(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(Right5(x)) → Right5(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right4(x)) → Right4(AE(x))
E(Right5(x)) → Right5(AE(x))
E(R(x)) → E(L(x))

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

(47) MRRProof (EQUIVALENT transformation)

b(Right3(x)) → Right3(AAb(x))
b(Right5(x)) → Right5(AAb(x))
R(Right5(x)) → Right5(AR(x))
Ab(Begin(x)) → Right5(Wait(x))
Ab(Right3(x)) → Right3(AAAb(x))
Ab(Right5(x)) → Right5(AAAb(x))
L(Right5(x)) → Right5(AL(x))
E(Right5(x)) → Right5(AE(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = 2·x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = 2·x₁
POL(AE(x₁)) = 1 + 2·x₁
POL(AL(x₁)) = 2·x₁
POL(AR(x₁)) = 2·x₁
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = 2·x₁
POL(Begin(x₁)) = 2 + 2·x₁
POL(E(x₁)) = 2 + 2·x₁
POL(END(x₁)) = 2·x₁
POL(L(x₁)) = 2·x₁
POL(Left(x₁)) = 2·x₁
POL(R(x₁)) = 2·x₁
POL(Right1(x₁)) = 2·x₁
POL(Right2(x₁)) = 2·x₁
POL(Right3(x₁)) = 2 + 2·x₁
POL(Right4(x₁)) = 2·x₁
POL(Right5(x₁)) = 1 + 2·x₁
POL(Right6(x₁)) = 2·x₁
POL(Right7(x₁)) = 2·x₁
POL(Wait(x₁)) = 1 + x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = 2·x₁

(48) Obligation:

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

END(R(Right4(x))) → END(R(a(Left(x))))

The TRS R consists of the following rules:

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right2(x)) → Right2(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right4(x)) → Right4(AE(x))
E(R(x)) → E(L(x))

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

(49) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

END(R(Right4(x))) → END(R(a(Left(x))))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( END(x₁) ) = max{0, x₁ - 2}

POL( R(x₁) ) = 2x₁

POL( a(x₁) ) = x₁ + 1

POL( Left(x₁) ) = x₁

POL( AR(x₁) ) = 2x₁

POL( AE(x₁) ) = x₁

POL( E(x₁) ) = x₁

POL( AL(x₁) ) = 2x₁ + 2

POL( L(x₁) ) = 2x₁

POL( AAa(x₁) ) = x₁ + 1

POL( AAAa(x₁) ) = x₁ + 2

POL( Aa(x₁) ) = x₁ + 2

POL( AAb(x₁) ) = x₁

POL( b(x₁) ) = x₁

POL( AAAb(x₁) ) = x₁

POL( Ab(x₁) ) = x₁

POL( Wait(x₁) ) = 0

POL( Begin(x₁) ) = 0

POL( Right1(x₁) ) = max{0, x₁ - 1}

POL( Right2(x₁) ) = 2

POL( Right3(x₁) ) = 1

POL( Right4(x₁) ) = x₁ + 2

POL( Right5(x₁) ) = max{0, -2}

POL( Right6(x₁) ) = max{0, -2}

POL( Right7(x₁) ) = 2

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

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
E(Right4(x)) → Right4(AE(x))
E(R(x)) → E(L(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
b(Right2(x)) → Right2(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))

(50) Obligation:

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

Left(AR(x)) → R(Left(x))
Left(AE(x)) → E(Left(x))
Left(AL(x)) → L(Left(x))
Left(AAa(x)) → a(Left(x))
Left(AAAa(x)) → Aa(Left(x))
Left(AAb(x)) → b(Left(x))
Left(AAAb(x)) → Ab(Left(x))
Left(Wait(x)) → Begin(x)
b(Right2(x)) → Right2(AAb(x))
b(Right4(x)) → Right4(AAb(x))
b(Right6(x)) → Right6(AAb(x))
b(Right7(x)) → Right7(AAb(x))
a(Right1(x)) → Right1(AAa(x))
a(Right2(x)) → Right2(AAa(x))
a(Right3(x)) → Right3(AAa(x))
a(Right4(x)) → Right4(AAa(x))
a(Right5(x)) → Right5(AAa(x))
a(Right6(x)) → Right6(AAa(x))
a(Right7(x)) → Right7(AAa(x))
R(Right2(x)) → Right2(AR(x))
R(Right4(x)) → Right4(AR(x))
Ab(Right2(x)) → Right2(AAAb(x))
Ab(Right4(x)) → Right4(AAAb(x))
Ab(Right6(x)) → Right6(AAAb(x))
Ab(Right7(x)) → Right7(AAAb(x))
Ab(R(x)) → R(b(x))
Aa(Begin(x)) → Right4(Wait(x))
Aa(Right1(x)) → Right1(AAAa(x))
Aa(Right2(x)) → Right2(AAAa(x))
Aa(Right3(x)) → Right3(AAAa(x))
Aa(Right4(x)) → Right4(AAAa(x))
Aa(Right5(x)) → Right5(AAAa(x))
Aa(Right6(x)) → Right6(AAAa(x))
Aa(Right7(x)) → Right7(AAAa(x))
Aa(R(x)) → R(a(x))
L(Right2(x)) → Right2(AL(x))
L(Right4(x)) → Right4(AL(x))
L(a(x)) → Aa(L(x))
L(b(x)) → Ab(L(x))
L(b(a(x))) → R(a(b(x)))
E(Right4(x)) → Right4(AE(x))
E(R(x)) → E(L(x))

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

(51) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) QTRS Reverse (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

(15) MRRProof (EQUIVALENT transformation)

(16) Obligation:

(17) PisEmptyProof (EQUIVALENT transformation)

(18) YES

(19) Obligation:

(20) UsableRulesProof (EQUIVALENT transformation)

(21) Obligation:

(22) QDPSizeChangeProof (EQUIVALENT transformation)

(23) YES

(24) Obligation:

(25) UsableRulesProof (EQUIVALENT transformation)

(26) Obligation:

(27) QDPOrderProof (EQUIVALENT transformation)

(28) Obligation:

(29) QDPOrderProof (EQUIVALENT transformation)

(30) Obligation:

(31) QDPOrderProof (EQUIVALENT transformation)

(32) Obligation:

(33) QDPOrderProof (EQUIVALENT transformation)

(34) Obligation:

(35) MRRProof (EQUIVALENT transformation)

(36) Obligation:

(37) MRRProof (EQUIVALENT transformation)

(38) Obligation:

(39) MRRProof (EQUIVALENT transformation)

(40) Obligation:

(41) MRRProof (EQUIVALENT transformation)

(42) Obligation:

(43) QDPOrderProof (EQUIVALENT transformation)

(44) Obligation:

(45) MRRProof (EQUIVALENT transformation)

(46) Obligation:

(47) MRRProof (EQUIVALENT transformation)

(48) Obligation:

(49) QDPOrderProof (EQUIVALENT transformation)

(50) Obligation:

(51) PisEmptyProof (EQUIVALENT transformation)

(52) YES