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

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

0 QTRS

↳1 DependencyPairsProof (⇔, 46 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 1 ms)

↳4 AND

    ↳5 QDP

        ↳6 UsableRulesProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 QDPOrderProof (⇔, 4 ms)

        ↳9 QDP

        ↳10 QDPOrderProof (⇔, 92 ms)

        ↳11 QDP

        ↳12 PisEmptyProof (⇔, 0 ms)

        ↳13 YES

    ↳14 QDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 QDPSizeChangeProof (⇔, 0 ms)

        ↳18 YES

    ↳19 QDP

        ↳20 UsableRulesProof (⇔, 0 ms)

        ↳21 QDP

        ↳22 QDPSizeChangeProof (⇔, 0 ms)

        ↳23 YES

    ↳24 QDP

        ↳25 UsableRulesProof (⇔, 0 ms)

        ↳26 QDP

        ↳27 QDPSizeChangeProof (⇔, 0 ms)

        ↳28 YES

    ↳29 QDP

        ↳30 UsableRulesProof (⇔, 0 ms)

        ↳31 QDP

        ↳32 QDPSizeChangeProof (⇔, 0 ms)

        ↳33 YES

    ↳34 QDP

        ↳35 UsableRulesProof (⇔, 0 ms)

        ↳36 QDP

        ↳37 QDPSizeChangeProof (⇔, 0 ms)

        ↳38 YES

    ↳39 QDP

        ↳40 UsableRulesProof (⇔, 0 ms)

        ↳41 QDP

        ↳42 QDPSizeChangeProof (⇔, 0 ms)

        ↳43 YES

    ↳44 QDP

        ↳45 UsableRulesProof (⇔, 0 ms)

        ↳46 QDP

        ↳47 QDPSizeChangeProof (⇔, 0 ms)

        ↳48 YES

    ↳49 QDP

        ↳50 UsableRulesProof (⇔, 0 ms)

        ↳51 QDP

        ↳52 QDPSizeChangeProof (⇔, 0 ms)

        ↳53 YES

    ↳54 QDP

        ↳55 UsableRulesProof (⇔, 0 ms)

        ↳56 QDP

        ↳57 QDPSizeChangeProof (⇔, 0 ms)

        ↳58 YES

    ↳59 QDP

        ↳60 UsableRulesProof (⇔, 0 ms)

        ↳61 QDP

        ↳62 QDPSizeChangeProof (⇔, 0 ms)

        ↳63 YES

    ↳64 QDP

        ↳65 UsableRulesProof (⇔, 0 ms)

        ↳66 QDP

        ↳67 QDPSizeChangeProof (⇔, 0 ms)

        ↳68 YES

    ↳69 QDP

        ↳70 UsableRulesProof (⇔, 0 ms)

        ↳71 QDP

        ↳72 QDPOrderProof (⇔, 3489 ms)

        ↳73 QDP

        ↳74 UsableRulesProof (⇔, 0 ms)

        ↳75 QDP

        ↳76 QDPOrderProof (⇔, 64 ms)

        ↳77 QDP

        ↳78 UsableRulesProof (⇔, 0 ms)

        ↳79 QDP

        ↳80 MRRProof (⇔, 54 ms)

        ↳81 QDP

        ↳82 MRRProof (⇔, 61 ms)

        ↳83 QDP

        ↳84 QDPOrderProof (⇔, 3126 ms)

        ↳85 QDP

        ↳86 UsableRulesProof (⇔, 0 ms)

        ↳87 QDP

        ↳88 QDPOrderProof (⇔, 266 ms)

        ↳89 QDP

        ↳90 UsableRulesProof (⇔, 0 ms)

        ↳91 QDP

        ↳92 QDPOrderProof (⇔, 825 ms)

        ↳93 QDP

        ↳94 UsableRulesProof (⇔, 0 ms)

        ↳95 QDP

        ↳96 QDPOrderProof (⇔, 14 ms)

        ↳97 QDP

        ↳98 DependencyGraphProof (⇔, 0 ms)

        ↳99 TRUE

(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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

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

(2) Obligation:

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

BEGIN(E(x)) → WAIT(Right1(x))
BEGIN(E(x)) → RIGHT1(x)
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → RIGHT2(x)
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → RIGHT3(x)
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(L(x)) → RIGHT4(x)
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Aa(x)) → RIGHT5(x)
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ab(x)) → RIGHT6(x)
BEGIN(Ac(x)) → WAIT(Right7(x))
BEGIN(Ac(x)) → RIGHT7(x)
BEGIN(b(L(x))) → WAIT(Right8(x))
BEGIN(b(L(x))) → RIGHT8(x)
BEGIN(L(x)) → WAIT(Right9(x))
BEGIN(L(x)) → RIGHT9(x)
BEGIN(b(L(x))) → WAIT(Right10(x))
BEGIN(b(L(x))) → RIGHT10(x)
BEGIN(L(x)) → WAIT(Right11(x))
BEGIN(L(x)) → RIGHT11(x)
RIGHT5(R(End(x))) → A(R(End(x)))
RIGHT6(R(End(x))) → B(R(End(x)))
RIGHT7(R(End(x))) → C(R(End(x)))
RIGHT8(a(End(x))) → B(c(a(R(End(x)))))
RIGHT8(a(End(x))) → C(a(R(End(x))))
RIGHT8(a(End(x))) → A(R(End(x)))
RIGHT8(a(End(x))) → R¹(End(x))
RIGHT9(a(b(End(x)))) → B(c(a(R(End(x)))))
RIGHT9(a(b(End(x)))) → C(a(R(End(x))))
RIGHT9(a(b(End(x)))) → A(R(End(x)))
RIGHT9(a(b(End(x)))) → R¹(End(x))
RIGHT10(c(End(x))) → B(b(c(R(End(x)))))
RIGHT10(c(End(x))) → B(c(R(End(x))))
RIGHT10(c(End(x))) → C(R(End(x)))
RIGHT10(c(End(x))) → R¹(End(x))
RIGHT11(c(b(End(x)))) → B(b(c(R(End(x)))))
RIGHT11(c(b(End(x)))) → B(c(R(End(x))))
RIGHT11(c(b(End(x)))) → C(R(End(x)))
RIGHT11(c(b(End(x)))) → R¹(End(x))
RIGHT1(R(x)) → AR¹(Right1(x))
RIGHT1(R(x)) → RIGHT1(x)
RIGHT2(R(x)) → AR¹(Right2(x))
RIGHT2(R(x)) → RIGHT2(x)
RIGHT3(R(x)) → AR¹(Right3(x))
RIGHT3(R(x)) → RIGHT3(x)
RIGHT4(R(x)) → AR¹(Right4(x))
RIGHT4(R(x)) → RIGHT4(x)
RIGHT5(R(x)) → AR¹(Right5(x))
RIGHT5(R(x)) → RIGHT5(x)
RIGHT6(R(x)) → AR¹(Right6(x))
RIGHT6(R(x)) → RIGHT6(x)
RIGHT7(R(x)) → AR¹(Right7(x))
RIGHT7(R(x)) → RIGHT7(x)
RIGHT8(R(x)) → AR¹(Right8(x))
RIGHT8(R(x)) → RIGHT8(x)
RIGHT9(R(x)) → AR¹(Right9(x))
RIGHT9(R(x)) → RIGHT9(x)
RIGHT10(R(x)) → AR¹(Right10(x))
RIGHT10(R(x)) → RIGHT10(x)
RIGHT11(R(x)) → AR¹(Right11(x))
RIGHT11(R(x)) → RIGHT11(x)
RIGHT1(E(x)) → AE¹(Right1(x))
RIGHT1(E(x)) → RIGHT1(x)
RIGHT2(E(x)) → AE¹(Right2(x))
RIGHT2(E(x)) → RIGHT2(x)
RIGHT3(E(x)) → AE¹(Right3(x))
RIGHT3(E(x)) → RIGHT3(x)
RIGHT4(E(x)) → AE¹(Right4(x))
RIGHT4(E(x)) → RIGHT4(x)
RIGHT5(E(x)) → AE¹(Right5(x))
RIGHT5(E(x)) → RIGHT5(x)
RIGHT6(E(x)) → AE¹(Right6(x))
RIGHT6(E(x)) → RIGHT6(x)
RIGHT7(E(x)) → AE¹(Right7(x))
RIGHT7(E(x)) → RIGHT7(x)
RIGHT8(E(x)) → AE¹(Right8(x))
RIGHT8(E(x)) → RIGHT8(x)
RIGHT9(E(x)) → AE¹(Right9(x))
RIGHT9(E(x)) → RIGHT9(x)
RIGHT10(E(x)) → AE¹(Right10(x))
RIGHT10(E(x)) → RIGHT10(x)
RIGHT11(E(x)) → AE¹(Right11(x))
RIGHT11(E(x)) → RIGHT11(x)
RIGHT1(L(x)) → AL¹(Right1(x))
RIGHT1(L(x)) → RIGHT1(x)
RIGHT2(L(x)) → AL¹(Right2(x))
RIGHT2(L(x)) → RIGHT2(x)
RIGHT3(L(x)) → AL¹(Right3(x))
RIGHT3(L(x)) → RIGHT3(x)
RIGHT4(L(x)) → AL¹(Right4(x))
RIGHT4(L(x)) → RIGHT4(x)
RIGHT5(L(x)) → AL¹(Right5(x))
RIGHT5(L(x)) → RIGHT5(x)
RIGHT6(L(x)) → AL¹(Right6(x))
RIGHT6(L(x)) → RIGHT6(x)
RIGHT7(L(x)) → AL¹(Right7(x))
RIGHT7(L(x)) → RIGHT7(x)
RIGHT8(L(x)) → AL¹(Right8(x))
RIGHT8(L(x)) → RIGHT8(x)
RIGHT9(L(x)) → AL¹(Right9(x))
RIGHT9(L(x)) → RIGHT9(x)
RIGHT10(L(x)) → AL¹(Right10(x))
RIGHT10(L(x)) → RIGHT10(x)
RIGHT11(L(x)) → AL¹(Right11(x))
RIGHT11(L(x)) → RIGHT11(x)
RIGHT1(a(x)) → AAA(Right1(x))
RIGHT1(a(x)) → RIGHT1(x)
RIGHT2(a(x)) → AAA(Right2(x))
RIGHT2(a(x)) → RIGHT2(x)
RIGHT3(a(x)) → AAA(Right3(x))
RIGHT3(a(x)) → RIGHT3(x)
RIGHT4(a(x)) → AAA(Right4(x))
RIGHT4(a(x)) → RIGHT4(x)
RIGHT5(a(x)) → AAA(Right5(x))
RIGHT5(a(x)) → RIGHT5(x)
RIGHT6(a(x)) → AAA(Right6(x))
RIGHT6(a(x)) → RIGHT6(x)
RIGHT7(a(x)) → AAA(Right7(x))
RIGHT7(a(x)) → RIGHT7(x)
RIGHT8(a(x)) → AAA(Right8(x))
RIGHT8(a(x)) → RIGHT8(x)
RIGHT9(a(x)) → AAA(Right9(x))
RIGHT9(a(x)) → RIGHT9(x)
RIGHT10(a(x)) → AAA(Right10(x))
RIGHT10(a(x)) → RIGHT10(x)
RIGHT11(a(x)) → AAA(Right11(x))
RIGHT11(a(x)) → RIGHT11(x)
RIGHT1(Aa(x)) → AAAA(Right1(x))
RIGHT1(Aa(x)) → RIGHT1(x)
RIGHT2(Aa(x)) → AAAA(Right2(x))
RIGHT2(Aa(x)) → RIGHT2(x)
RIGHT3(Aa(x)) → AAAA(Right3(x))
RIGHT3(Aa(x)) → RIGHT3(x)
RIGHT4(Aa(x)) → AAAA(Right4(x))
RIGHT4(Aa(x)) → RIGHT4(x)
RIGHT5(Aa(x)) → AAAA(Right5(x))
RIGHT5(Aa(x)) → RIGHT5(x)
RIGHT6(Aa(x)) → AAAA(Right6(x))
RIGHT6(Aa(x)) → RIGHT6(x)
RIGHT7(Aa(x)) → AAAA(Right7(x))
RIGHT7(Aa(x)) → RIGHT7(x)
RIGHT8(Aa(x)) → AAAA(Right8(x))
RIGHT8(Aa(x)) → RIGHT8(x)
RIGHT9(Aa(x)) → AAAA(Right9(x))
RIGHT9(Aa(x)) → RIGHT9(x)
RIGHT10(Aa(x)) → AAAA(Right10(x))
RIGHT10(Aa(x)) → RIGHT10(x)
RIGHT11(Aa(x)) → AAAA(Right11(x))
RIGHT11(Aa(x)) → RIGHT11(x)
RIGHT1(b(x)) → AAB(Right1(x))
RIGHT1(b(x)) → RIGHT1(x)
RIGHT2(b(x)) → AAB(Right2(x))
RIGHT2(b(x)) → RIGHT2(x)
RIGHT3(b(x)) → AAB(Right3(x))
RIGHT3(b(x)) → RIGHT3(x)
RIGHT4(b(x)) → AAB(Right4(x))
RIGHT4(b(x)) → RIGHT4(x)
RIGHT5(b(x)) → AAB(Right5(x))
RIGHT5(b(x)) → RIGHT5(x)
RIGHT6(b(x)) → AAB(Right6(x))
RIGHT6(b(x)) → RIGHT6(x)
RIGHT7(b(x)) → AAB(Right7(x))
RIGHT7(b(x)) → RIGHT7(x)
RIGHT8(b(x)) → AAB(Right8(x))
RIGHT8(b(x)) → RIGHT8(x)
RIGHT9(b(x)) → AAB(Right9(x))
RIGHT9(b(x)) → RIGHT9(x)
RIGHT10(b(x)) → AAB(Right10(x))
RIGHT10(b(x)) → RIGHT10(x)
RIGHT11(b(x)) → AAB(Right11(x))
RIGHT11(b(x)) → RIGHT11(x)
RIGHT1(Ab(x)) → AAAB(Right1(x))
RIGHT1(Ab(x)) → RIGHT1(x)
RIGHT2(Ab(x)) → AAAB(Right2(x))
RIGHT2(Ab(x)) → RIGHT2(x)
RIGHT3(Ab(x)) → AAAB(Right3(x))
RIGHT3(Ab(x)) → RIGHT3(x)
RIGHT4(Ab(x)) → AAAB(Right4(x))
RIGHT4(Ab(x)) → RIGHT4(x)
RIGHT5(Ab(x)) → AAAB(Right5(x))
RIGHT5(Ab(x)) → RIGHT5(x)
RIGHT6(Ab(x)) → AAAB(Right6(x))
RIGHT6(Ab(x)) → RIGHT6(x)
RIGHT7(Ab(x)) → AAAB(Right7(x))
RIGHT7(Ab(x)) → RIGHT7(x)
RIGHT8(Ab(x)) → AAAB(Right8(x))
RIGHT8(Ab(x)) → RIGHT8(x)
RIGHT9(Ab(x)) → AAAB(Right9(x))
RIGHT9(Ab(x)) → RIGHT9(x)
RIGHT10(Ab(x)) → AAAB(Right10(x))
RIGHT10(Ab(x)) → RIGHT10(x)
RIGHT11(Ab(x)) → AAAB(Right11(x))
RIGHT11(Ab(x)) → RIGHT11(x)
RIGHT1(c(x)) → AAC(Right1(x))
RIGHT1(c(x)) → RIGHT1(x)
RIGHT2(c(x)) → AAC(Right2(x))
RIGHT2(c(x)) → RIGHT2(x)
RIGHT3(c(x)) → AAC(Right3(x))
RIGHT3(c(x)) → RIGHT3(x)
RIGHT4(c(x)) → AAC(Right4(x))
RIGHT4(c(x)) → RIGHT4(x)
RIGHT5(c(x)) → AAC(Right5(x))
RIGHT5(c(x)) → RIGHT5(x)
RIGHT6(c(x)) → AAC(Right6(x))
RIGHT6(c(x)) → RIGHT6(x)
RIGHT7(c(x)) → AAC(Right7(x))
RIGHT7(c(x)) → RIGHT7(x)
RIGHT8(c(x)) → AAC(Right8(x))
RIGHT8(c(x)) → RIGHT8(x)
RIGHT9(c(x)) → AAC(Right9(x))
RIGHT9(c(x)) → RIGHT9(x)
RIGHT10(c(x)) → AAC(Right10(x))
RIGHT10(c(x)) → RIGHT10(x)
RIGHT11(c(x)) → AAC(Right11(x))
RIGHT11(c(x)) → RIGHT11(x)
RIGHT1(Ac(x)) → AAAC(Right1(x))
RIGHT1(Ac(x)) → RIGHT1(x)
RIGHT2(Ac(x)) → AAAC(Right2(x))
RIGHT2(Ac(x)) → RIGHT2(x)
RIGHT3(Ac(x)) → AAAC(Right3(x))
RIGHT3(Ac(x)) → RIGHT3(x)
RIGHT4(Ac(x)) → AAAC(Right4(x))
RIGHT4(Ac(x)) → RIGHT4(x)
RIGHT5(Ac(x)) → AAAC(Right5(x))
RIGHT5(Ac(x)) → RIGHT5(x)
RIGHT6(Ac(x)) → AAAC(Right6(x))
RIGHT6(Ac(x)) → RIGHT6(x)
RIGHT7(Ac(x)) → AAAC(Right7(x))
RIGHT7(Ac(x)) → RIGHT7(x)
RIGHT8(Ac(x)) → AAAC(Right8(x))
RIGHT8(Ac(x)) → RIGHT8(x)
RIGHT9(Ac(x)) → AAAC(Right9(x))
RIGHT9(Ac(x)) → RIGHT9(x)
RIGHT10(Ac(x)) → AAAC(Right10(x))
RIGHT10(Ac(x)) → RIGHT10(x)
RIGHT11(Ac(x)) → AAAC(Right11(x))
RIGHT11(Ac(x)) → RIGHT11(x)
AR¹(Left(x)) → R¹(x)
AAA(Left(x)) → A(x)
AAB(Left(x)) → B(x)
AAC(Left(x)) → C(x)
WAIT(Left(x)) → BEGIN(x)
R¹(Aa(x)) → A(R(x))
R¹(Aa(x)) → R¹(x)
R¹(Ab(x)) → B(R(x))
R¹(Ab(x)) → R¹(x)
R¹(Ac(x)) → C(R(x))
R¹(Ac(x)) → R¹(x)
A(b(L(x))) → B(c(a(R(x))))
A(b(L(x))) → C(a(R(x)))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R¹(x)
C(b(L(x))) → B(b(c(R(x))))
C(b(L(x))) → B(c(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

A(b(L(x))) → C(a(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)
R¹(Aa(x)) → A(R(x))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R¹(x)
R¹(Aa(x)) → R¹(x)
R¹(Ab(x)) → R¹(x)
R¹(Ac(x)) → C(R(x))
R¹(Ac(x)) → R¹(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

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

(7) Obligation:

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

A(b(L(x))) → C(a(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)
R¹(Aa(x)) → A(R(x))
A(b(L(x))) → A(R(x))
A(b(L(x))) → R¹(x)
R¹(Aa(x)) → R¹(x)
R¹(Ab(x)) → R¹(x)
R¹(Ac(x)) → C(R(x))
R¹(Ac(x)) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))

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

(8) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

A(b(L(x))) → R¹(x)
R¹(Aa(x)) → R¹(x)

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

POL(A(x₁)) = 1 + x₁
POL(Aa(x₁)) = 1 + x₁
POL(Ab(x₁)) = x₁
POL(Ac(x₁)) = x₁
POL(C(x₁)) = x₁
POL(E(x₁)) = 1 + x₁
POL(L(x₁)) = x₁
POL(R(x₁)) = x₁
POL(R¹(x₁)) = x₁
POL(a(x₁)) = 1 + x₁
POL(b(x₁)) = x₁
POL(c(x₁)) = x₁

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

R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))

(9) Obligation:

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

A(b(L(x))) → C(a(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)
R¹(Aa(x)) → A(R(x))
A(b(L(x))) → A(R(x))
R¹(Ab(x)) → R¹(x)
R¹(Ac(x)) → C(R(x))
R¹(Ac(x)) → R¹(x)

The TRS R consists of the following rules:

R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))

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

(10) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

A(b(L(x))) → C(a(R(x)))
C(b(L(x))) → C(R(x))
C(b(L(x))) → R¹(x)
R¹(Aa(x)) → A(R(x))
A(b(L(x))) → A(R(x))
R¹(Ab(x)) → R¹(x)
R¹(Ac(x)) → C(R(x))
R¹(Ac(x)) → R¹(x)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
A(x1) = A(x1)
b(x1) = b(x1)
L(x1) = x1
C(x1) = C(x1)
a(x1) = a(x1)
R(x1) = x1
R¹(x1) = R¹(x1)
Aa(x1) = Aa(x1)
Ab(x1) = Ab(x1)
Ac(x1) = Ac(x1)
E(x1) = E(x1)
c(x1) = c(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:

[A₁, a₁, Aa₁] > [C₁, R^1₁, Ac₁, c₁] > [b₁, Ab₁]

Status:

A₁: [1]
b₁: [1]
C₁: [1]
a₁: [1]
R^1₁: [1]
Aa₁: [1]
Ab₁: [1]
Ac₁: [1]
E₁: [1]
c₁: [1]

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

R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))

(11) Obligation:

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

R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))

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

(12) PisEmptyProof (EQUIVALENT transformation)

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

(13) YES

(14) Obligation:

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

RIGHT4(E(x)) → RIGHT4(x)
RIGHT4(R(x)) → RIGHT4(x)
RIGHT4(L(x)) → RIGHT4(x)
RIGHT4(a(x)) → RIGHT4(x)
RIGHT4(Aa(x)) → RIGHT4(x)
RIGHT4(b(x)) → RIGHT4(x)
RIGHT4(Ab(x)) → RIGHT4(x)
RIGHT4(c(x)) → RIGHT4(x)
RIGHT4(Ac(x)) → RIGHT4(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

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

RIGHT4(E(x)) → RIGHT4(x)
RIGHT4(R(x)) → RIGHT4(x)
RIGHT4(L(x)) → RIGHT4(x)
RIGHT4(a(x)) → RIGHT4(x)
RIGHT4(Aa(x)) → RIGHT4(x)
RIGHT4(b(x)) → RIGHT4(x)
RIGHT4(Ab(x)) → RIGHT4(x)
RIGHT4(c(x)) → RIGHT4(x)
RIGHT4(Ac(x)) → RIGHT4(x)

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

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

RIGHT4(E(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(R(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(L(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(a(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(Aa(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(b(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(Ab(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(c(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1
RIGHT4(Ac(x)) → RIGHT4(x)
The graph contains the following edges 1 > 1

(18) YES

(19) Obligation:

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

RIGHT3(E(x)) → RIGHT3(x)
RIGHT3(R(x)) → RIGHT3(x)
RIGHT3(L(x)) → RIGHT3(x)
RIGHT3(a(x)) → RIGHT3(x)
RIGHT3(Aa(x)) → RIGHT3(x)
RIGHT3(b(x)) → RIGHT3(x)
RIGHT3(Ab(x)) → RIGHT3(x)
RIGHT3(c(x)) → RIGHT3(x)
RIGHT3(Ac(x)) → RIGHT3(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(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:

RIGHT3(E(x)) → RIGHT3(x)
RIGHT3(R(x)) → RIGHT3(x)
RIGHT3(L(x)) → RIGHT3(x)
RIGHT3(a(x)) → RIGHT3(x)
RIGHT3(Aa(x)) → RIGHT3(x)
RIGHT3(b(x)) → RIGHT3(x)
RIGHT3(Ab(x)) → RIGHT3(x)
RIGHT3(c(x)) → RIGHT3(x)
RIGHT3(Ac(x)) → RIGHT3(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:

RIGHT3(E(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(R(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(L(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(a(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(Aa(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(b(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(Ab(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(c(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1
RIGHT3(Ac(x)) → RIGHT3(x)
The graph contains the following edges 1 > 1

(23) YES

(24) Obligation:

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

RIGHT2(E(x)) → RIGHT2(x)
RIGHT2(R(x)) → RIGHT2(x)
RIGHT2(L(x)) → RIGHT2(x)
RIGHT2(a(x)) → RIGHT2(x)
RIGHT2(Aa(x)) → RIGHT2(x)
RIGHT2(b(x)) → RIGHT2(x)
RIGHT2(Ab(x)) → RIGHT2(x)
RIGHT2(c(x)) → RIGHT2(x)
RIGHT2(Ac(x)) → RIGHT2(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(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:

RIGHT2(E(x)) → RIGHT2(x)
RIGHT2(R(x)) → RIGHT2(x)
RIGHT2(L(x)) → RIGHT2(x)
RIGHT2(a(x)) → RIGHT2(x)
RIGHT2(Aa(x)) → RIGHT2(x)
RIGHT2(b(x)) → RIGHT2(x)
RIGHT2(Ab(x)) → RIGHT2(x)
RIGHT2(c(x)) → RIGHT2(x)
RIGHT2(Ac(x)) → RIGHT2(x)

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

(27) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

RIGHT2(E(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(R(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(L(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(a(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(Aa(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(b(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(Ab(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(c(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1
RIGHT2(Ac(x)) → RIGHT2(x)
The graph contains the following edges 1 > 1

(28) YES

(29) Obligation:

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

RIGHT1(E(x)) → RIGHT1(x)
RIGHT1(R(x)) → RIGHT1(x)
RIGHT1(L(x)) → RIGHT1(x)
RIGHT1(a(x)) → RIGHT1(x)
RIGHT1(Aa(x)) → RIGHT1(x)
RIGHT1(b(x)) → RIGHT1(x)
RIGHT1(Ab(x)) → RIGHT1(x)
RIGHT1(c(x)) → RIGHT1(x)
RIGHT1(Ac(x)) → RIGHT1(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(30) UsableRulesProof (EQUIVALENT transformation)

(31) Obligation:

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

RIGHT1(E(x)) → RIGHT1(x)
RIGHT1(R(x)) → RIGHT1(x)
RIGHT1(L(x)) → RIGHT1(x)
RIGHT1(a(x)) → RIGHT1(x)
RIGHT1(Aa(x)) → RIGHT1(x)
RIGHT1(b(x)) → RIGHT1(x)
RIGHT1(Ab(x)) → RIGHT1(x)
RIGHT1(c(x)) → RIGHT1(x)
RIGHT1(Ac(x)) → RIGHT1(x)

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

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

RIGHT1(E(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(R(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(L(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(a(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(Aa(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(b(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(Ab(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(c(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1
RIGHT1(Ac(x)) → RIGHT1(x)
The graph contains the following edges 1 > 1

(33) YES

(34) Obligation:

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

RIGHT11(E(x)) → RIGHT11(x)
RIGHT11(R(x)) → RIGHT11(x)
RIGHT11(L(x)) → RIGHT11(x)
RIGHT11(a(x)) → RIGHT11(x)
RIGHT11(Aa(x)) → RIGHT11(x)
RIGHT11(b(x)) → RIGHT11(x)
RIGHT11(Ab(x)) → RIGHT11(x)
RIGHT11(c(x)) → RIGHT11(x)
RIGHT11(Ac(x)) → RIGHT11(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(35) UsableRulesProof (EQUIVALENT transformation)

(36) Obligation:

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

RIGHT11(E(x)) → RIGHT11(x)
RIGHT11(R(x)) → RIGHT11(x)
RIGHT11(L(x)) → RIGHT11(x)
RIGHT11(a(x)) → RIGHT11(x)
RIGHT11(Aa(x)) → RIGHT11(x)
RIGHT11(b(x)) → RIGHT11(x)
RIGHT11(Ab(x)) → RIGHT11(x)
RIGHT11(c(x)) → RIGHT11(x)
RIGHT11(Ac(x)) → RIGHT11(x)

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

(37) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

RIGHT11(E(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(R(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(L(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(a(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(Aa(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(b(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(Ab(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(c(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1
RIGHT11(Ac(x)) → RIGHT11(x)
The graph contains the following edges 1 > 1

(38) YES

(39) Obligation:

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

RIGHT10(E(x)) → RIGHT10(x)
RIGHT10(R(x)) → RIGHT10(x)
RIGHT10(L(x)) → RIGHT10(x)
RIGHT10(a(x)) → RIGHT10(x)
RIGHT10(Aa(x)) → RIGHT10(x)
RIGHT10(b(x)) → RIGHT10(x)
RIGHT10(Ab(x)) → RIGHT10(x)
RIGHT10(c(x)) → RIGHT10(x)
RIGHT10(Ac(x)) → RIGHT10(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(40) UsableRulesProof (EQUIVALENT transformation)

(41) Obligation:

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

RIGHT10(E(x)) → RIGHT10(x)
RIGHT10(R(x)) → RIGHT10(x)
RIGHT10(L(x)) → RIGHT10(x)
RIGHT10(a(x)) → RIGHT10(x)
RIGHT10(Aa(x)) → RIGHT10(x)
RIGHT10(b(x)) → RIGHT10(x)
RIGHT10(Ab(x)) → RIGHT10(x)
RIGHT10(c(x)) → RIGHT10(x)
RIGHT10(Ac(x)) → RIGHT10(x)

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

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

RIGHT10(E(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(R(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(L(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(a(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(Aa(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(b(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(Ab(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(c(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1
RIGHT10(Ac(x)) → RIGHT10(x)
The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

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

RIGHT9(E(x)) → RIGHT9(x)
RIGHT9(R(x)) → RIGHT9(x)
RIGHT9(L(x)) → RIGHT9(x)
RIGHT9(a(x)) → RIGHT9(x)
RIGHT9(Aa(x)) → RIGHT9(x)
RIGHT9(b(x)) → RIGHT9(x)
RIGHT9(Ab(x)) → RIGHT9(x)
RIGHT9(c(x)) → RIGHT9(x)
RIGHT9(Ac(x)) → RIGHT9(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(45) UsableRulesProof (EQUIVALENT transformation)

(46) Obligation:

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

RIGHT9(E(x)) → RIGHT9(x)
RIGHT9(R(x)) → RIGHT9(x)
RIGHT9(L(x)) → RIGHT9(x)
RIGHT9(a(x)) → RIGHT9(x)
RIGHT9(Aa(x)) → RIGHT9(x)
RIGHT9(b(x)) → RIGHT9(x)
RIGHT9(Ab(x)) → RIGHT9(x)
RIGHT9(c(x)) → RIGHT9(x)
RIGHT9(Ac(x)) → RIGHT9(x)

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

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

RIGHT9(E(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(R(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(L(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(a(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(Aa(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(b(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(Ab(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(c(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1
RIGHT9(Ac(x)) → RIGHT9(x)
The graph contains the following edges 1 > 1

(48) YES

(49) Obligation:

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

RIGHT8(E(x)) → RIGHT8(x)
RIGHT8(R(x)) → RIGHT8(x)
RIGHT8(L(x)) → RIGHT8(x)
RIGHT8(a(x)) → RIGHT8(x)
RIGHT8(Aa(x)) → RIGHT8(x)
RIGHT8(b(x)) → RIGHT8(x)
RIGHT8(Ab(x)) → RIGHT8(x)
RIGHT8(c(x)) → RIGHT8(x)
RIGHT8(Ac(x)) → RIGHT8(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(50) UsableRulesProof (EQUIVALENT transformation)

(51) Obligation:

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

RIGHT8(E(x)) → RIGHT8(x)
RIGHT8(R(x)) → RIGHT8(x)
RIGHT8(L(x)) → RIGHT8(x)
RIGHT8(a(x)) → RIGHT8(x)
RIGHT8(Aa(x)) → RIGHT8(x)
RIGHT8(b(x)) → RIGHT8(x)
RIGHT8(Ab(x)) → RIGHT8(x)
RIGHT8(c(x)) → RIGHT8(x)
RIGHT8(Ac(x)) → RIGHT8(x)

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

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

RIGHT8(E(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(R(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(L(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(a(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(Aa(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(b(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(Ab(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(c(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1
RIGHT8(Ac(x)) → RIGHT8(x)
The graph contains the following edges 1 > 1

(53) YES

(54) Obligation:

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

RIGHT7(E(x)) → RIGHT7(x)
RIGHT7(R(x)) → RIGHT7(x)
RIGHT7(L(x)) → RIGHT7(x)
RIGHT7(a(x)) → RIGHT7(x)
RIGHT7(Aa(x)) → RIGHT7(x)
RIGHT7(b(x)) → RIGHT7(x)
RIGHT7(Ab(x)) → RIGHT7(x)
RIGHT7(c(x)) → RIGHT7(x)
RIGHT7(Ac(x)) → RIGHT7(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(55) UsableRulesProof (EQUIVALENT transformation)

(56) Obligation:

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

RIGHT7(E(x)) → RIGHT7(x)
RIGHT7(R(x)) → RIGHT7(x)
RIGHT7(L(x)) → RIGHT7(x)
RIGHT7(a(x)) → RIGHT7(x)
RIGHT7(Aa(x)) → RIGHT7(x)
RIGHT7(b(x)) → RIGHT7(x)
RIGHT7(Ab(x)) → RIGHT7(x)
RIGHT7(c(x)) → RIGHT7(x)
RIGHT7(Ac(x)) → RIGHT7(x)

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

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

RIGHT7(E(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(R(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(L(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(a(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(Aa(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(b(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(Ab(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(c(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1
RIGHT7(Ac(x)) → RIGHT7(x)
The graph contains the following edges 1 > 1

(58) YES

(59) Obligation:

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

RIGHT6(E(x)) → RIGHT6(x)
RIGHT6(R(x)) → RIGHT6(x)
RIGHT6(L(x)) → RIGHT6(x)
RIGHT6(a(x)) → RIGHT6(x)
RIGHT6(Aa(x)) → RIGHT6(x)
RIGHT6(b(x)) → RIGHT6(x)
RIGHT6(Ab(x)) → RIGHT6(x)
RIGHT6(c(x)) → RIGHT6(x)
RIGHT6(Ac(x)) → RIGHT6(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(60) UsableRulesProof (EQUIVALENT transformation)

(61) Obligation:

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

RIGHT6(E(x)) → RIGHT6(x)
RIGHT6(R(x)) → RIGHT6(x)
RIGHT6(L(x)) → RIGHT6(x)
RIGHT6(a(x)) → RIGHT6(x)
RIGHT6(Aa(x)) → RIGHT6(x)
RIGHT6(b(x)) → RIGHT6(x)
RIGHT6(Ab(x)) → RIGHT6(x)
RIGHT6(c(x)) → RIGHT6(x)
RIGHT6(Ac(x)) → RIGHT6(x)

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

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

RIGHT6(E(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(R(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(L(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(a(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(Aa(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(b(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(Ab(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(c(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1
RIGHT6(Ac(x)) → RIGHT6(x)
The graph contains the following edges 1 > 1

(63) YES

(64) Obligation:

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

RIGHT5(E(x)) → RIGHT5(x)
RIGHT5(R(x)) → RIGHT5(x)
RIGHT5(L(x)) → RIGHT5(x)
RIGHT5(a(x)) → RIGHT5(x)
RIGHT5(Aa(x)) → RIGHT5(x)
RIGHT5(b(x)) → RIGHT5(x)
RIGHT5(Ab(x)) → RIGHT5(x)
RIGHT5(c(x)) → RIGHT5(x)
RIGHT5(Ac(x)) → RIGHT5(x)

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(65) UsableRulesProof (EQUIVALENT transformation)

(66) Obligation:

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

RIGHT5(E(x)) → RIGHT5(x)
RIGHT5(R(x)) → RIGHT5(x)
RIGHT5(L(x)) → RIGHT5(x)
RIGHT5(a(x)) → RIGHT5(x)
RIGHT5(Aa(x)) → RIGHT5(x)
RIGHT5(b(x)) → RIGHT5(x)
RIGHT5(Ab(x)) → RIGHT5(x)
RIGHT5(c(x)) → RIGHT5(x)
RIGHT5(Ac(x)) → RIGHT5(x)

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

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

RIGHT5(E(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(R(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(L(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(a(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(Aa(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(b(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(Ab(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(c(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1
RIGHT5(Ac(x)) → RIGHT5(x)
The graph contains the following edges 1 > 1

(68) YES

(69) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(E(x)) → WAIT(Right1(x))
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))
BEGIN(b(L(x))) → WAIT(Right8(x))
BEGIN(L(x)) → WAIT(Right9(x))
BEGIN(b(L(x))) → WAIT(Right10(x))
BEGIN(L(x)) → WAIT(Right11(x))

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(L(x)) → Wait(Right4(x))
Begin(Aa(x)) → Wait(Right5(x))
Begin(Ab(x)) → Wait(Right6(x))
Begin(Ac(x)) → Wait(Right7(x))
Begin(b(L(x))) → Wait(Right8(x))
Begin(L(x)) → Wait(Right9(x))
Begin(b(L(x))) → Wait(Right10(x))
Begin(L(x)) → Wait(Right11(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(c(End(x))) → Left(L(Ac(End(x))))
Right5(R(End(x))) → Left(a(R(End(x))))
Right6(R(End(x))) → Left(b(R(End(x))))
Right7(R(End(x))) → Left(c(R(End(x))))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right11(c(b(End(x)))) → Left(b(b(c(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))
Right8(R(x)) → AR(Right8(x))
Right9(R(x)) → AR(Right9(x))
Right10(R(x)) → AR(Right10(x))
Right11(R(x)) → AR(Right11(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))
Right8(E(x)) → AE(Right8(x))
Right9(E(x)) → AE(Right9(x))
Right10(E(x)) → AE(Right10(x))
Right11(E(x)) → AE(Right11(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))
Right8(L(x)) → AL(Right8(x))
Right9(L(x)) → AL(Right9(x))
Right10(L(x)) → AL(Right10(x))
Right11(L(x)) → AL(Right11(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))
Right8(a(x)) → AAa(Right8(x))
Right9(a(x)) → AAa(Right9(x))
Right10(a(x)) → AAa(Right10(x))
Right11(a(x)) → AAa(Right11(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))
Right8(Aa(x)) → AAAa(Right8(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right11(Aa(x)) → AAAa(Right11(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))
Right8(b(x)) → AAb(Right8(x))
Right9(b(x)) → AAb(Right9(x))
Right10(b(x)) → AAb(Right10(x))
Right11(b(x)) → AAb(Right11(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))
Right8(Ab(x)) → AAAb(Right8(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right1(c(x)) → AAc(Right1(x))
Right2(c(x)) → AAc(Right2(x))
Right3(c(x)) → AAc(Right3(x))
Right4(c(x)) → AAc(Right4(x))
Right5(c(x)) → AAc(Right5(x))
Right6(c(x)) → AAc(Right6(x))
Right7(c(x)) → AAc(Right7(x))
Right8(c(x)) → AAc(Right8(x))
Right9(c(x)) → AAc(Right9(x))
Right10(c(x)) → AAc(Right10(x))
Right11(c(x)) → AAc(Right11(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(Ac(x)) → AAAc(Right11(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
Wait(Left(x)) → Begin(x)
R(E(x)) → L(E(x))
a(L(x)) → L(Aa(x))
b(L(x)) → L(Ab(x))
c(L(x)) → L(Ac(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
a(b(L(x))) → b(c(a(R(x))))
c(b(L(x))) → b(b(c(R(x))))

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

(70) UsableRulesProof (EQUIVALENT transformation)

(71) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(E(x)) → WAIT(Right1(x))
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))
BEGIN(b(L(x))) → WAIT(Right8(x))
BEGIN(L(x)) → WAIT(Right9(x))
BEGIN(b(L(x))) → WAIT(Right10(x))
BEGIN(L(x)) → WAIT(Right11(x))

The TRS R consists of the following rules:

Right11(c(b(End(x)))) → Left(b(b(c(R(End(x))))))
Right11(R(x)) → AR(Right11(x))
Right11(E(x)) → AE(Right11(x))
Right11(L(x)) → AL(Right11(x))
Right11(a(x)) → AAa(Right11(x))
Right11(Aa(x)) → AAAa(Right11(x))
Right11(b(x)) → AAb(Right11(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right11(c(x)) → AAc(Right11(x))
Right11(Ac(x)) → AAAc(Right11(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right10(R(x)) → AR(Right10(x))
Right10(E(x)) → AE(Right10(x))
Right10(L(x)) → AL(Right10(x))
Right10(a(x)) → AAa(Right10(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right10(b(x)) → AAb(Right10(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right10(c(x)) → AAc(Right10(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right9(R(x)) → AR(Right9(x))
Right9(E(x)) → AE(Right9(x))
Right9(L(x)) → AL(Right9(x))
Right9(a(x)) → AAa(Right9(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right9(b(x)) → AAb(Right9(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right9(c(x)) → AAc(Right9(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right8(R(x)) → AR(Right8(x))
Right8(E(x)) → AE(Right8(x))
Right8(L(x)) → AL(Right8(x))
Right8(a(x)) → AAa(Right8(x))
Right8(Aa(x)) → AAAa(Right8(x))
Right8(b(x)) → AAb(Right8(x))
Right8(Ab(x)) → AAAb(Right8(x))
Right8(c(x)) → AAc(Right8(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(E(x)) → AE(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right1(R(End(x))) → Left(L(E(End(x))))
Right1(R(x)) → AR(Right1(x))
Right1(E(x)) → AE(Right1(x))
Right1(L(x)) → AL(Right1(x))
Right1(a(x)) → AAa(Right1(x))
Right1(Aa(x)) → AAAa(Right1(x))
Right1(b(x)) → AAb(Right1(x))
Right1(Ab(x)) → AAAb(Right1(x))
Right1(c(x)) → AAc(Right1(x))
Right1(Ac(x)) → AAAc(Right1(x))

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

(72) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

BEGIN(E(x)) → WAIT(Right1(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(WAIT(x₁)) = 0A +
[ -I, 0A, 0A ]

· x₁

POL(Left(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(BEGIN(x₁)) = 0A +
[ -I, 0A, 0A ]

· x₁

POL(E(x₁)) =
/ 1A \

| 0A |

\ 1A /

+
/ 0A 1A 1A \

| 0A 1A 0A |

\ 0A 0A 1A /

· x₁

POL(Right1(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(L(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right2(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right3(x₁)) =
/ -I \

| -I |

\ 0A /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right4(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ -I 0A 0A /

· x₁

POL(Aa(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right5(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Ab(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A 0A \

| -I -I -I |

\ 0A 0A 0A /

· x₁

POL(Right6(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Ac(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right7(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(b(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right8(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right9(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right10(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(Right11(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

POL(R(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| 0A -I -I |

\ -I 0A 0A /

· x₁

POL(End(x₁)) =
/ 1A \

| -I |

\ -I /

+
/ 1A 1A 1A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AR(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AE(x₁)) =
/ 1A \

| 1A |

\ 1A /

+
/ 0A 1A -I \

| 0A 1A 0A |

\ 0A 1A 0A /

· x₁

POL(AL(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(a(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I -I 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(AAa(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AAAa(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A -I /

· x₁

POL(AAb(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AAAb(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(c(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AAc(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AAAc(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

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

Right1(R(End(x))) → Left(L(E(End(x))))
Right1(R(x)) → AR(Right1(x))
Right1(E(x)) → AE(Right1(x))
Right1(L(x)) → AL(Right1(x))
Right1(a(x)) → AAa(Right1(x))
Right1(Aa(x)) → AAAa(Right1(x))
Right1(b(x)) → AAb(Right1(x))
Right1(Ab(x)) → AAAb(Right1(x))
Right1(c(x)) → AAc(Right1(x))
Right1(Ac(x)) → AAAc(Right1(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(E(x)) → AE(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right8(R(x)) → AR(Right8(x))
Right8(E(x)) → AE(Right8(x))
Right8(L(x)) → AL(Right8(x))
Right8(a(x)) → AAa(Right8(x))
Right8(Aa(x)) → AAAa(Right8(x))
Right8(b(x)) → AAb(Right8(x))
Right8(Ab(x)) → AAAb(Right8(x))
Right8(c(x)) → AAc(Right8(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right9(R(x)) → AR(Right9(x))
Right9(E(x)) → AE(Right9(x))
Right9(L(x)) → AL(Right9(x))
Right9(a(x)) → AAa(Right9(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right9(b(x)) → AAb(Right9(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right9(c(x)) → AAc(Right9(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right10(R(x)) → AR(Right10(x))
Right10(E(x)) → AE(Right10(x))
Right10(L(x)) → AL(Right10(x))
Right10(a(x)) → AAa(Right10(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right10(b(x)) → AAb(Right10(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right10(c(x)) → AAc(Right10(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(c(b(End(x)))) → Left(b(b(c(R(End(x))))))
Right11(R(x)) → AR(Right11(x))
Right11(E(x)) → AE(Right11(x))
Right11(L(x)) → AL(Right11(x))
Right11(a(x)) → AAa(Right11(x))
Right11(Aa(x)) → AAAa(Right11(x))
Right11(b(x)) → AAb(Right11(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right11(c(x)) → AAc(Right11(x))
Right11(Ac(x)) → AAAc(Right11(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))

(73) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))
BEGIN(b(L(x))) → WAIT(Right8(x))
BEGIN(L(x)) → WAIT(Right9(x))
BEGIN(b(L(x))) → WAIT(Right10(x))
BEGIN(L(x)) → WAIT(Right11(x))

The TRS R consists of the following rules:

Right11(c(b(End(x)))) → Left(b(b(c(R(End(x))))))
Right11(R(x)) → AR(Right11(x))
Right11(E(x)) → AE(Right11(x))
Right11(L(x)) → AL(Right11(x))
Right11(a(x)) → AAa(Right11(x))
Right11(Aa(x)) → AAAa(Right11(x))
Right11(b(x)) → AAb(Right11(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right11(c(x)) → AAc(Right11(x))
Right11(Ac(x)) → AAAc(Right11(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right10(R(x)) → AR(Right10(x))
Right10(E(x)) → AE(Right10(x))
Right10(L(x)) → AL(Right10(x))
Right10(a(x)) → AAa(Right10(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right10(b(x)) → AAb(Right10(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right10(c(x)) → AAc(Right10(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right9(R(x)) → AR(Right9(x))
Right9(E(x)) → AE(Right9(x))
Right9(L(x)) → AL(Right9(x))
Right9(a(x)) → AAa(Right9(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right9(b(x)) → AAb(Right9(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right9(c(x)) → AAc(Right9(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right8(R(x)) → AR(Right8(x))
Right8(E(x)) → AE(Right8(x))
Right8(L(x)) → AL(Right8(x))
Right8(a(x)) → AAa(Right8(x))
Right8(Aa(x)) → AAAa(Right8(x))
Right8(b(x)) → AAb(Right8(x))
Right8(Ab(x)) → AAAb(Right8(x))
Right8(c(x)) → AAc(Right8(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(E(x)) → AE(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right1(R(End(x))) → Left(L(E(End(x))))
Right1(R(x)) → AR(Right1(x))
Right1(E(x)) → AE(Right1(x))
Right1(L(x)) → AL(Right1(x))
Right1(a(x)) → AAa(Right1(x))
Right1(Aa(x)) → AAAa(Right1(x))
Right1(b(x)) → AAb(Right1(x))
Right1(Ab(x)) → AAAb(Right1(x))
Right1(c(x)) → AAc(Right1(x))
Right1(Ac(x)) → AAAc(Right1(x))

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

(74) UsableRulesProof (EQUIVALENT transformation)

(75) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))
BEGIN(b(L(x))) → WAIT(Right8(x))
BEGIN(L(x)) → WAIT(Right9(x))
BEGIN(b(L(x))) → WAIT(Right10(x))
BEGIN(L(x)) → WAIT(Right11(x))

The TRS R consists of the following rules:

Right11(c(b(End(x)))) → Left(b(b(c(R(End(x))))))
Right11(R(x)) → AR(Right11(x))
Right11(E(x)) → AE(Right11(x))
Right11(L(x)) → AL(Right11(x))
Right11(a(x)) → AAa(Right11(x))
Right11(Aa(x)) → AAAa(Right11(x))
Right11(b(x)) → AAb(Right11(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right11(c(x)) → AAc(Right11(x))
Right11(Ac(x)) → AAAc(Right11(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right10(R(x)) → AR(Right10(x))
Right10(E(x)) → AE(Right10(x))
Right10(L(x)) → AL(Right10(x))
Right10(a(x)) → AAa(Right10(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right10(b(x)) → AAb(Right10(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right10(c(x)) → AAc(Right10(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right9(R(x)) → AR(Right9(x))
Right9(E(x)) → AE(Right9(x))
Right9(L(x)) → AL(Right9(x))
Right9(a(x)) → AAa(Right9(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right9(b(x)) → AAb(Right9(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right9(c(x)) → AAc(Right9(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right8(R(x)) → AR(Right8(x))
Right8(E(x)) → AE(Right8(x))
Right8(L(x)) → AL(Right8(x))
Right8(a(x)) → AAa(Right8(x))
Right8(Aa(x)) → AAAa(Right8(x))
Right8(b(x)) → AAb(Right8(x))
Right8(Ab(x)) → AAAb(Right8(x))
Right8(c(x)) → AAc(Right8(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(E(x)) → AE(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))

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

(76) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

BEGIN(b(L(x))) → WAIT(Right8(x))
BEGIN(L(x)) → WAIT(Right9(x))
BEGIN(b(L(x))) → WAIT(Right10(x))
BEGIN(L(x)) → WAIT(Right11(x))

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

POL(AAAa(x₁)) = x₁
POL(AAAb(x₁)) = x₁
POL(AAAc(x₁)) = x₁
POL(AAa(x₁)) = x₁
POL(AAb(x₁)) = x₁
POL(AAc(x₁)) = x₁
POL(AE(x₁)) = 0
POL(AL(x₁)) = 1 + x₁
POL(AR(x₁)) = 1
POL(Aa(x₁)) = x₁
POL(Ab(x₁)) = x₁
POL(Ac(x₁)) = x₁
POL(BEGIN(x₁)) = x₁
POL(E(x₁)) = 0
POL(End(x₁)) = 1 + x₁
POL(L(x₁)) = 1 + x₁
POL(Left(x₁)) = x₁
POL(R(x₁)) = 1
POL(Right10(x₁)) = x₁
POL(Right11(x₁)) = 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₁)) = x₁
POL(Right8(x₁)) = x₁
POL(Right9(x₁)) = x₁
POL(WAIT(x₁)) = x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(c(x₁)) = x₁

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

Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(E(x)) → AE(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right8(R(x)) → AR(Right8(x))
Right8(E(x)) → AE(Right8(x))
Right8(L(x)) → AL(Right8(x))
Right8(a(x)) → AAa(Right8(x))
Right8(Aa(x)) → AAAa(Right8(x))
Right8(b(x)) → AAb(Right8(x))
Right8(Ab(x)) → AAAb(Right8(x))
Right8(c(x)) → AAc(Right8(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right9(R(x)) → AR(Right9(x))
Right9(E(x)) → AE(Right9(x))
Right9(L(x)) → AL(Right9(x))
Right9(a(x)) → AAa(Right9(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right9(b(x)) → AAb(Right9(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right9(c(x)) → AAc(Right9(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right10(R(x)) → AR(Right10(x))
Right10(E(x)) → AE(Right10(x))
Right10(L(x)) → AL(Right10(x))
Right10(a(x)) → AAa(Right10(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right10(b(x)) → AAb(Right10(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right10(c(x)) → AAc(Right10(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right11(c(b(End(x)))) → Left(b(b(c(R(End(x))))))
Right11(R(x)) → AR(Right11(x))
Right11(E(x)) → AE(Right11(x))
Right11(L(x)) → AL(Right11(x))
Right11(a(x)) → AAa(Right11(x))
Right11(Aa(x)) → AAAa(Right11(x))
Right11(b(x)) → AAb(Right11(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right11(c(x)) → AAc(Right11(x))
Right11(Ac(x)) → AAAc(Right11(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))

(77) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right11(c(b(End(x)))) → Left(b(b(c(R(End(x))))))
Right11(R(x)) → AR(Right11(x))
Right11(E(x)) → AE(Right11(x))
Right11(L(x)) → AL(Right11(x))
Right11(a(x)) → AAa(Right11(x))
Right11(Aa(x)) → AAAa(Right11(x))
Right11(b(x)) → AAb(Right11(x))
Right11(Ab(x)) → AAAb(Right11(x))
Right11(c(x)) → AAc(Right11(x))
Right11(Ac(x)) → AAAc(Right11(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right10(c(End(x))) → Left(b(b(c(R(End(x))))))
Right10(R(x)) → AR(Right10(x))
Right10(E(x)) → AE(Right10(x))
Right10(L(x)) → AL(Right10(x))
Right10(a(x)) → AAa(Right10(x))
Right10(Aa(x)) → AAAa(Right10(x))
Right10(b(x)) → AAb(Right10(x))
Right10(Ab(x)) → AAAb(Right10(x))
Right10(c(x)) → AAc(Right10(x))
Right10(Ac(x)) → AAAc(Right10(x))
Right9(a(b(End(x)))) → Left(b(c(a(R(End(x))))))
Right9(R(x)) → AR(Right9(x))
Right9(E(x)) → AE(Right9(x))
Right9(L(x)) → AL(Right9(x))
Right9(a(x)) → AAa(Right9(x))
Right9(Aa(x)) → AAAa(Right9(x))
Right9(b(x)) → AAb(Right9(x))
Right9(Ab(x)) → AAAb(Right9(x))
Right9(c(x)) → AAc(Right9(x))
Right9(Ac(x)) → AAAc(Right9(x))
Right8(a(End(x))) → Left(b(c(a(R(End(x))))))
Right8(R(x)) → AR(Right8(x))
Right8(E(x)) → AE(Right8(x))
Right8(L(x)) → AL(Right8(x))
Right8(a(x)) → AAa(Right8(x))
Right8(Aa(x)) → AAAa(Right8(x))
Right8(b(x)) → AAb(Right8(x))
Right8(Ab(x)) → AAAb(Right8(x))
Right8(c(x)) → AAc(Right8(x))
Right8(Ac(x)) → AAAc(Right8(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(E(x)) → AE(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))

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

(78) UsableRulesProof (EQUIVALENT transformation)

(79) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(E(x)) → AE(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))

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

(80) 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 rules of the TRS R:

Right5(E(x)) → AE(Right5(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = 2·x₁
POL(AAAb(x₁)) = x₁
POL(AAAc(x₁)) = x₁
POL(AAa(x₁)) = 2·x₁
POL(AAb(x₁)) = x₁
POL(AAc(x₁)) = x₁
POL(AE(x₁)) = 1 + x₁
POL(AL(x₁)) = x₁
POL(AR(x₁)) = x₁
POL(Aa(x₁)) = 2·x₁
POL(Ab(x₁)) = x₁
POL(Ac(x₁)) = x₁
POL(BEGIN(x₁)) = 2·x₁
POL(E(x₁)) = 1 + x₁
POL(End(x₁)) = 2·x₁
POL(L(x₁)) = x₁
POL(Left(x₁)) = x₁
POL(R(x₁)) = x₁
POL(Right2(x₁)) = x₁
POL(Right3(x₁)) = x₁
POL(Right4(x₁)) = x₁
POL(Right5(x₁)) = 2·x₁
POL(Right6(x₁)) = x₁
POL(Right7(x₁)) = x₁
POL(WAIT(x₁)) = 2·x₁
POL(a(x₁)) = 2·x₁
POL(b(x₁)) = x₁
POL(c(x₁)) = x₁

(81) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(E(x)) → AE(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(E(x)) → AE(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(E(x)) → AE(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))

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

(82) MRRProof (EQUIVALENT transformation)

Right4(E(x)) → AE(Right4(x))
Right3(E(x)) → AE(Right3(x))
Right2(E(x)) → AE(Right2(x))

Used ordering: Polynomial interpretation [POLO]:

POL(AAAa(x₁)) = 2·x₁
POL(AAAb(x₁)) = x₁
POL(AAAc(x₁)) = x₁
POL(AAa(x₁)) = 2·x₁
POL(AAb(x₁)) = x₁
POL(AAc(x₁)) = x₁
POL(AE(x₁)) = 1 + 2·x₁
POL(AL(x₁)) = 2·x₁
POL(AR(x₁)) = 2·x₁
POL(Aa(x₁)) = 2·x₁
POL(Ab(x₁)) = x₁
POL(Ac(x₁)) = x₁
POL(BEGIN(x₁)) = x₁
POL(E(x₁)) = 1 + 2·x₁
POL(End(x₁)) = 2·x₁
POL(L(x₁)) = 2·x₁
POL(Left(x₁)) = x₁
POL(R(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₁)) = 2·x₁
POL(b(x₁)) = x₁
POL(c(x₁)) = x₁

(83) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right2(x))
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))

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

(84) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

BEGIN(L(x)) → WAIT(Right2(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(WAIT(x₁)) = -I +
[ 0A, 0A, 0A ]

· x₁

POL(Left(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ -I 0A 0A \

| 0A 0A -I |

\ -I 0A 0A /

· x₁

POL(BEGIN(x₁)) = 0A +
[ 0A, 0A, 0A ]

· x₁

POL(L(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 1A 1A 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(Right2(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A 0A -I /

· x₁

POL(Right3(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 1A 0A 0A \

| 1A -I 0A |

\ 1A -I 0A /

· x₁

POL(Right4(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Aa(x₁)) =
/ -I \

| -I |

\ 0A /

+
/ 0A -I -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Right5(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Ab(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Right6(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ -I 0A 0A \

| 0A 0A -I |

\ -I 0A 0A /

· x₁

POL(Ac(x₁)) =
/ -I \

| -I |

\ 0A /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Right7(x₁)) =
/ -I \

| -I |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(a(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A -I -I \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(End(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 1A 1A -I /

· x₁

POL(R(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 1A 0A 0A \

| -I 1A 0A |

\ 1A 1A 0A /

· x₁

POL(AR(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 1A 0A \

| 0A 1A 0A |

\ -I 1A 0A /

· x₁

POL(AL(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A 0A \

| 0A 1A 0A |

\ 0A 0A 0A /

· x₁

POL(AAa(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(AAAa(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A -I |

\ 0A 0A 0A /

· x₁

POL(b(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A -I -I \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(AAb(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AAAb(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A -I \

| -I 0A -I |

\ -I 0A 0A /

· x₁

POL(c(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I 0A -I |

\ 0A 0A 0A /

· x₁

POL(AAc(x₁)) =
/ -I \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AAAc(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A -I |

\ 0A 0A 0A /

· x₁

POL(E(x₁)) =
/ -I \

| -I |

\ 0A /

+
/ 0A 0A -I \

| 0A -I -I |

\ 0A 0A 0A /

· x₁

POL(AE(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A -I \

| -I 0A -I |

\ 0A 0A -I /

· x₁

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

Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))

(85) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right2(a(End(x))) → Left(L(Aa(End(x))))
Right2(R(x)) → AR(Right2(x))
Right2(L(x)) → AL(Right2(x))
Right2(a(x)) → AAa(Right2(x))
Right2(Aa(x)) → AAAa(Right2(x))
Right2(b(x)) → AAb(Right2(x))
Right2(Ab(x)) → AAAb(Right2(x))
Right2(c(x)) → AAc(Right2(x))
Right2(Ac(x)) → AAAc(Right2(x))

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

(86) UsableRulesProof (EQUIVALENT transformation)

(87) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right3(x))
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))

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

(88) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

BEGIN(L(x)) → WAIT(Right3(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(WAIT(x₁)) = -I +
[ 0A, 0A, -I ]

· x₁

POL(Left(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ -I -I 0A \

| 0A 0A 0A |

\ -I -I -I /

· x₁

POL(BEGIN(x₁)) = 0A +
[ 0A, 0A, -I ]

· x₁

POL(L(x₁)) =
/ 0A \

| 0A |

\ 1A /

+
/ 1A -I 0A \

| 0A 1A 0A |

\ 0A 0A 0A /

· x₁

POL(Right3(x₁)) =
/ -I \

| -I |

\ 0A /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A -I 0A /

· x₁

POL(Right4(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 1A -I \

| 0A 1A -I |

\ 1A 0A 0A /

· x₁

POL(Aa(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Right5(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Ab(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ -I -I -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Right6(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(Ac(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| -I 0A -I |

\ 0A -I -I /

· x₁

POL(Right7(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 0A 0A 0A /

· x₁

POL(b(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ -I -I 0A \

| 0A 0A -I |

\ -I -I 0A /

· x₁

POL(End(x₁)) =
/ -I \

| -I |

\ 1A /

+
/ 0A 0A -I \

| 0A 0A -I |

\ 1A 1A 0A /

· x₁

POL(R(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 1A 0A -I \

| 0A 1A -I |

\ 0A 0A -I /

· x₁

POL(AR(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A -I \

| -I 1A -I |

\ 0A 0A -I /

· x₁

POL(AL(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 1A 0A \

| -I 1A 0A |

\ 0A 0A 0A /

· x₁

POL(a(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ -I -I 0A /

· x₁

POL(AAa(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AAAa(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| -I 0A -I |

\ 0A -I 0A /

· x₁

POL(AAb(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ -I -I -I /

· x₁

POL(AAAb(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A -I \

| 0A 0A -I |

\ -I -I -I /

· x₁

POL(c(x₁)) =
/ 0A \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(AAc(x₁)) =
/ 0A \

| -I |

\ 0A /

+
/ 0A 0A -I \

| -I 0A -I |

\ 0A 0A -I /

· x₁

POL(AAAc(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A 0A -I \

| 0A 0A -I |

\ -I -I -I /

· x₁

POL(E(x₁)) =
/ 1A \

| -I |

\ 0A /

+
/ 0A 0A -I \

| -I 0A 0A |

\ -I -I -I /

· x₁

POL(AE(x₁)) =
/ 0A \

| 1A |

\ 1A /

+
/ 0A -I 0A \

| -I 0A 0A |

\ 0A 0A 0A /

· x₁

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

Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))

(89) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right3(b(End(x))) → Left(L(Ab(End(x))))
Right3(R(x)) → AR(Right3(x))
Right3(L(x)) → AL(Right3(x))
Right3(a(x)) → AAa(Right3(x))
Right3(Aa(x)) → AAAa(Right3(x))
Right3(b(x)) → AAb(Right3(x))
Right3(Ab(x)) → AAAb(Right3(x))
Right3(c(x)) → AAc(Right3(x))
Right3(Ac(x)) → AAAc(Right3(x))

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

(90) UsableRulesProof (EQUIVALENT transformation)

(91) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(L(x)) → WAIT(Right4(x))
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))

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

(92) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

BEGIN(L(x)) → WAIT(Right4(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(WAIT(x₁)) = -I +
[ 0A, 0A, 0A ]

· x₁

POL(Left(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(BEGIN(x₁)) = 0A +
[ 0A, 0A, 0A ]

· x₁

POL(L(x₁)) =
/ -I \

| 0A |

\ -I /

+
/ 1A 0A 0A \

| -I -I 0A |

\ 0A 0A 0A /

· x₁

POL(Right4(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I -I \

| 0A -I -I |

\ 0A -I -I /

· x₁

POL(Aa(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I -I \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(Right5(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A 0A |

\ 0A -I -I /

· x₁

POL(Ab(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I -I \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(Right6(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A 0A |

\ 0A -I -I /

· x₁

POL(Ac(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A -I -I \

| -I 0A 0A |

\ -I -I -I /

· x₁

POL(Right7(x₁)) =
/ 0A \

| -I |

\ -I /

+
/ 0A 0A -I \

| 0A 0A 0A |

\ 0A -I -I /

· x₁

POL(c(x₁)) =
/ -I \

| 0A |

\ -I /

+
/ 0A 0A 0A \

| -I -I -I |

\ -I 0A 0A /

· x₁

POL(End(x₁)) =
/ -I \

| 0A |

\ 0A /

+
/ 0A -I -I \

| 1A -I 0A |

\ 0A -I -I /

· x₁

POL(R(x₁)) =
/ -I \

| -I |

\ 0A /

+
/ 1A 0A 0A \

| 0A 0A 0A |

\ 1A 0A 0A /

· x₁

POL(AR(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 1A \

| 0A 0A 1A |

\ -I 0A 1A /

· x₁

POL(AL(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 1A \

| 0A 0A 1A |

\ -I 0A 1A /

· x₁

POL(a(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I -I \

| -I 0A -I |

\ 0A -I -I /

· x₁

POL(AAa(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I 0A \

| -I -I 0A |

\ -I -I 0A /

· x₁

POL(AAAa(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I -I \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(b(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I -I \

| -I 0A -I |

\ 0A -I 0A /

· x₁

POL(AAb(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A -I 0A \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(AAAb(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| -I 0A 0A |

\ -I -I 0A /

· x₁

POL(AAc(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ -I 0A 0A /

· x₁

POL(AAAc(x₁)) =
/ -I \

| -I |

\ -I /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ -I -I 0A /

· x₁

POL(E(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

POL(AE(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I 0A -I \

| 0A 0A 0A |

\ 0A 0A 0A /

· x₁

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

Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))

(93) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right4(c(End(x))) → Left(L(Ac(End(x))))
Right4(R(x)) → AR(Right4(x))
Right4(L(x)) → AL(Right4(x))
Right4(a(x)) → AAa(Right4(x))
Right4(Aa(x)) → AAAa(Right4(x))
Right4(b(x)) → AAb(Right4(x))
Right4(Ab(x)) → AAAb(Right4(x))
Right4(c(x)) → AAc(Right4(x))
Right4(Ac(x)) → AAAc(Right4(x))

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

(94) UsableRulesProof (EQUIVALENT transformation)

(95) Obligation:

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

WAIT(Left(x)) → BEGIN(x)
BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))

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

(96) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

BEGIN(Aa(x)) → WAIT(Right5(x))
BEGIN(Ab(x)) → WAIT(Right6(x))
BEGIN(Ac(x)) → WAIT(Right7(x))

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

POL(AAAa(x₁)) = 1 + x₁
POL(AAAb(x₁)) = 1 + x₁
POL(AAAc(x₁)) = 1 + x₁
POL(AAa(x₁)) = 0
POL(AAb(x₁)) = 0
POL(AAc(x₁)) = 0
POL(AE(x₁)) = 0
POL(AL(x₁)) = 0
POL(AR(x₁)) = 0
POL(Aa(x₁)) = 1 + x₁
POL(Ab(x₁)) = 1 + x₁
POL(Ac(x₁)) = 1 + x₁
POL(BEGIN(x₁)) = x₁
POL(E(x₁)) = 0
POL(End(x₁)) = x₁
POL(L(x₁)) = 0
POL(Left(x₁)) = x₁
POL(R(x₁)) = 0
POL(Right5(x₁)) = x₁
POL(Right6(x₁)) = x₁
POL(Right7(x₁)) = x₁
POL(WAIT(x₁)) = x₁
POL(a(x₁)) = 0
POL(b(x₁)) = 0
POL(c(x₁)) = 0

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

Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(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))
AAc(Left(x)) → Left(c(x))
AAAc(Left(x)) → Left(Ac(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))

(97) Obligation:

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

WAIT(Left(x)) → BEGIN(x)

The TRS R consists of the following rules:

Right7(R(End(x))) → Left(c(R(End(x))))
Right7(R(x)) → AR(Right7(x))
Right7(E(x)) → AE(Right7(x))
Right7(L(x)) → AL(Right7(x))
Right7(a(x)) → AAa(Right7(x))
Right7(Aa(x)) → AAAa(Right7(x))
Right7(b(x)) → AAb(Right7(x))
Right7(Ab(x)) → AAAb(Right7(x))
Right7(c(x)) → AAc(Right7(x))
Right7(Ac(x)) → AAAc(Right7(x))
AAAc(Left(x)) → Left(Ac(x))
AAc(Left(x)) → Left(c(x))
c(L(x)) → L(Ac(x))
c(b(L(x))) → b(b(c(R(x))))
R(E(x)) → L(E(x))
R(Aa(x)) → a(R(x))
R(Ab(x)) → b(R(x))
R(Ac(x)) → c(R(x))
b(L(x)) → L(Ab(x))
a(L(x)) → L(Aa(x))
a(b(L(x))) → b(c(a(R(x))))
AAAb(Left(x)) → Left(Ab(x))
AAb(Left(x)) → Left(b(x))
AAAa(Left(x)) → Left(Aa(x))
AAa(Left(x)) → Left(a(x))
AL(Left(x)) → Left(L(x))
AE(Left(x)) → Left(E(x))
AR(Left(x)) → Left(R(x))
Right6(R(End(x))) → Left(b(R(End(x))))
Right6(R(x)) → AR(Right6(x))
Right6(E(x)) → AE(Right6(x))
Right6(L(x)) → AL(Right6(x))
Right6(a(x)) → AAa(Right6(x))
Right6(Aa(x)) → AAAa(Right6(x))
Right6(b(x)) → AAb(Right6(x))
Right6(Ab(x)) → AAAb(Right6(x))
Right6(c(x)) → AAc(Right6(x))
Right6(Ac(x)) → AAAc(Right6(x))
Right5(R(End(x))) → Left(a(R(End(x))))
Right5(R(x)) → AR(Right5(x))
Right5(L(x)) → AL(Right5(x))
Right5(a(x)) → AAa(Right5(x))
Right5(Aa(x)) → AAAa(Right5(x))
Right5(b(x)) → AAb(Right5(x))
Right5(Ab(x)) → AAAb(Right5(x))
Right5(c(x)) → AAc(Right5(x))
Right5(Ac(x)) → AAAc(Right5(x))

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

(98) DependencyGraphProof (EQUIVALENT transformation)

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