MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Termination Assumption

We assume termination of the following TRS
Begin(E(x0)) → Wait(Right1(x0))
Begin(L(x0)) → Wait(Right2(x0))
Begin(L(x0)) → Wait(Right3(x0))
Begin(L(x0)) → Wait(Right4(x0))
Begin(Aa(x0)) → Wait(Right5(x0))
Begin(Ab(x0)) → Wait(Right6(x0))
Begin(Ac(x0)) → Wait(Right7(x0))
Begin(b(L(x0))) → Wait(Right8(x0))
Begin(L(x0)) → Wait(Right9(x0))
Begin(b(L(x0))) → Wait(Right10(x0))
Begin(L(x0)) → Wait(Right11(x0))
Right1(R(End(x0))) → Left(L(E(End(x0))))
Right2(a(End(x0))) → Left(L(Aa(End(x0))))
Right3(b(End(x0))) → Left(L(Ab(End(x0))))
Right4(c(End(x0))) → Left(L(Ac(End(x0))))
Right5(R(End(x0))) → Left(a(R(End(x0))))
Right6(R(End(x0))) → Left(b(R(End(x0))))
Right7(R(End(x0))) → Left(c(R(End(x0))))
Right8(a(End(x0))) → Left(b(c(a(R(End(x0))))))
Right9(a(b(End(x0)))) → Left(b(c(a(R(End(x0))))))
Right10(c(End(x0))) → Left(b(b(c(R(End(x0))))))
Right11(c(b(End(x0)))) → Left(b(b(c(R(End(x0))))))
Right1(R(x0)) → AR(Right1(x0))
Right2(R(x0)) → AR(Right2(x0))
Right3(R(x0)) → AR(Right3(x0))
Right4(R(x0)) → AR(Right4(x0))
Right5(R(x0)) → AR(Right5(x0))
Right6(R(x0)) → AR(Right6(x0))
Right7(R(x0)) → AR(Right7(x0))
Right8(R(x0)) → AR(Right8(x0))
Right9(R(x0)) → AR(Right9(x0))
Right10(R(x0)) → AR(Right10(x0))
Right11(R(x0)) → AR(Right11(x0))
Right1(E(x0)) → AE(Right1(x0))
Right2(E(x0)) → AE(Right2(x0))
Right3(E(x0)) → AE(Right3(x0))
Right4(E(x0)) → AE(Right4(x0))
Right5(E(x0)) → AE(Right5(x0))
Right6(E(x0)) → AE(Right6(x0))
Right7(E(x0)) → AE(Right7(x0))
Right8(E(x0)) → AE(Right8(x0))
Right9(E(x0)) → AE(Right9(x0))
Right10(E(x0)) → AE(Right10(x0))
Right11(E(x0)) → AE(Right11(x0))
Right1(L(x0)) → AL(Right1(x0))
Right2(L(x0)) → AL(Right2(x0))
Right3(L(x0)) → AL(Right3(x0))
Right4(L(x0)) → AL(Right4(x0))
Right5(L(x0)) → AL(Right5(x0))
Right6(L(x0)) → AL(Right6(x0))
Right7(L(x0)) → AL(Right7(x0))
Right8(L(x0)) → AL(Right8(x0))
Right9(L(x0)) → AL(Right9(x0))
Right10(L(x0)) → AL(Right10(x0))
Right11(L(x0)) → AL(Right11(x0))
Right1(a(x0)) → AAa(Right1(x0))
Right2(a(x0)) → AAa(Right2(x0))
Right3(a(x0)) → AAa(Right3(x0))
Right4(a(x0)) → AAa(Right4(x0))
Right5(a(x0)) → AAa(Right5(x0))
Right6(a(x0)) → AAa(Right6(x0))
Right7(a(x0)) → AAa(Right7(x0))
Right8(a(x0)) → AAa(Right8(x0))
Right9(a(x0)) → AAa(Right9(x0))
Right10(a(x0)) → AAa(Right10(x0))
Right11(a(x0)) → AAa(Right11(x0))
Right1(Aa(x0)) → AAAa(Right1(x0))
Right2(Aa(x0)) → AAAa(Right2(x0))
Right3(Aa(x0)) → AAAa(Right3(x0))
Right4(Aa(x0)) → AAAa(Right4(x0))
Right5(Aa(x0)) → AAAa(Right5(x0))
Right6(Aa(x0)) → AAAa(Right6(x0))
Right7(Aa(x0)) → AAAa(Right7(x0))
Right8(Aa(x0)) → AAAa(Right8(x0))
Right9(Aa(x0)) → AAAa(Right9(x0))
Right10(Aa(x0)) → AAAa(Right10(x0))
Right11(Aa(x0)) → AAAa(Right11(x0))
Right1(b(x0)) → AAb(Right1(x0))
Right2(b(x0)) → AAb(Right2(x0))
Right3(b(x0)) → AAb(Right3(x0))
Right4(b(x0)) → AAb(Right4(x0))
Right5(b(x0)) → AAb(Right5(x0))
Right6(b(x0)) → AAb(Right6(x0))
Right7(b(x0)) → AAb(Right7(x0))
Right8(b(x0)) → AAb(Right8(x0))
Right9(b(x0)) → AAb(Right9(x0))
Right10(b(x0)) → AAb(Right10(x0))
Right11(b(x0)) → AAb(Right11(x0))
Right1(Ab(x0)) → AAAb(Right1(x0))
Right2(Ab(x0)) → AAAb(Right2(x0))
Right3(Ab(x0)) → AAAb(Right3(x0))
Right4(Ab(x0)) → AAAb(Right4(x0))
Right5(Ab(x0)) → AAAb(Right5(x0))
Right6(Ab(x0)) → AAAb(Right6(x0))
Right7(Ab(x0)) → AAAb(Right7(x0))
Right8(Ab(x0)) → AAAb(Right8(x0))
Right9(Ab(x0)) → AAAb(Right9(x0))
Right10(Ab(x0)) → AAAb(Right10(x0))
Right11(Ab(x0)) → AAAb(Right11(x0))
Right1(c(x0)) → AAc(Right1(x0))
Right2(c(x0)) → AAc(Right2(x0))
Right3(c(x0)) → AAc(Right3(x0))
Right4(c(x0)) → AAc(Right4(x0))
Right5(c(x0)) → AAc(Right5(x0))
Right6(c(x0)) → AAc(Right6(x0))
Right7(c(x0)) → AAc(Right7(x0))
Right8(c(x0)) → AAc(Right8(x0))
Right9(c(x0)) → AAc(Right9(x0))
Right10(c(x0)) → AAc(Right10(x0))
Right11(c(x0)) → AAc(Right11(x0))
Right1(Ac(x0)) → AAAc(Right1(x0))
Right2(Ac(x0)) → AAAc(Right2(x0))
Right3(Ac(x0)) → AAAc(Right3(x0))
Right4(Ac(x0)) → AAAc(Right4(x0))
Right5(Ac(x0)) → AAAc(Right5(x0))
Right6(Ac(x0)) → AAAc(Right6(x0))
Right7(Ac(x0)) → AAAc(Right7(x0))
Right8(Ac(x0)) → AAAc(Right8(x0))
Right9(Ac(x0)) → AAAc(Right9(x0))
Right10(Ac(x0)) → AAAc(Right10(x0))
Right11(Ac(x0)) → AAAc(Right11(x0))
AR(Left(x0)) → Left(R(x0))
AE(Left(x0)) → Left(E(x0))
AL(Left(x0)) → Left(L(x0))
AAa(Left(x0)) → Left(a(x0))
AAAa(Left(x0)) → Left(Aa(x0))
AAb(Left(x0)) → Left(b(x0))
AAAb(Left(x0)) → Left(Ab(x0))
AAc(Left(x0)) → Left(c(x0))
AAAc(Left(x0)) → Left(Ac(x0))
Wait(Left(x0)) → Begin(x0)
R(E(x0)) → L(E(x0))
a(L(x0)) → L(Aa(x0))
b(L(x0)) → L(Ab(x0))
c(L(x0)) → L(Ac(x0))
R(Aa(x0)) → a(R(x0))
R(Ab(x0)) → b(R(x0))
R(Ac(x0)) → c(R(x0))
a(b(L(x0))) → b(c(a(R(x0))))
c(b(L(x0))) → b(b(c(R(x0))))