MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(o(x0)) → Wait(Right1(x0))
Begin(e(x0)) → Wait(Right2(x0))
Begin(l(x0)) → Wait(Right3(x0))
Begin(m(a(x0))) → Wait(Right4(x0))
Begin(a(x0)) → Wait(Right5(x0))
Begin(a(x0)) → Wait(Right6(x0))
Begin(s(x0)) → Wait(Right7(x0))
Right1(t(End(x0))) → Left(m(a(End(x0))))
Right2(t(End(x0))) → Left(n(s(End(x0))))
Right3(a(End(x0))) → Left(a(t(End(x0))))
Right4(o(End(x0))) → Left(t(e(n(End(x0)))))
Right5(o(m(End(x0)))) → Left(t(e(n(End(x0)))))
Right6(s(End(x0))) → Left(l(a(t(o(m(a(t(e(End(x0))))))))))
Right7(n(End(x0))) → Left(a(l(a(t(End(x0))))))
Right1(t(x0)) → At(Right1(x0))
Right2(t(x0)) → At(Right2(x0))
Right3(t(x0)) → At(Right3(x0))
Right4(t(x0)) → At(Right4(x0))
Right5(t(x0)) → At(Right5(x0))
Right6(t(x0)) → At(Right6(x0))
Right7(t(x0)) → At(Right7(x0))
Right1(o(x0)) → Ao(Right1(x0))
Right2(o(x0)) → Ao(Right2(x0))
Right3(o(x0)) → Ao(Right3(x0))
Right4(o(x0)) → Ao(Right4(x0))
Right5(o(x0)) → Ao(Right5(x0))
Right6(o(x0)) → Ao(Right6(x0))
Right7(o(x0)) → Ao(Right7(x0))
Right1(m(x0)) → Am(Right1(x0))
Right2(m(x0)) → Am(Right2(x0))
Right3(m(x0)) → Am(Right3(x0))
Right4(m(x0)) → Am(Right4(x0))
Right5(m(x0)) → Am(Right5(x0))
Right6(m(x0)) → Am(Right6(x0))
Right7(m(x0)) → Am(Right7(x0))
Right1(a(x0)) → Aa(Right1(x0))
Right2(a(x0)) → Aa(Right2(x0))
Right3(a(x0)) → Aa(Right3(x0))
Right4(a(x0)) → Aa(Right4(x0))
Right5(a(x0)) → Aa(Right5(x0))
Right6(a(x0)) → Aa(Right6(x0))
Right7(a(x0)) → Aa(Right7(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))
Right1(n(x0)) → An(Right1(x0))
Right2(n(x0)) → An(Right2(x0))
Right3(n(x0)) → An(Right3(x0))
Right4(n(x0)) → An(Right4(x0))
Right5(n(x0)) → An(Right5(x0))
Right6(n(x0)) → An(Right6(x0))
Right7(n(x0)) → An(Right7(x0))
Right1(s(x0)) → As(Right1(x0))
Right2(s(x0)) → As(Right2(x0))
Right3(s(x0)) → As(Right3(x0))
Right4(s(x0)) → As(Right4(x0))
Right5(s(x0)) → As(Right5(x0))
Right6(s(x0)) → As(Right6(x0))
Right7(s(x0)) → As(Right7(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))
At(Left(x0)) → Left(t(x0))
Ao(Left(x0)) → Left(o(x0))
Am(Left(x0)) → Left(m(x0))
Aa(Left(x0)) → Left(a(x0))
Ae(Left(x0)) → Left(e(x0))
An(Left(x0)) → Left(n(x0))
As(Left(x0)) → Left(s(x0))
Al(Left(x0)) → Left(l(x0))
Wait(Left(x0)) → Begin(x0)
t(o(x0)) → m(a(x0))
t(e(x0)) → n(s(x0))
a(l(x0)) → a(t(x0))
o(m(a(x0))) → t(e(n(x0)))
s(a(x0)) → l(a(t(o(m(a(t(e(x0))))))))
n(s(x0)) → a(l(a(t(x0))))

Proof

1 Termination Assumption

We assume termination of the following TRS
Begin(o(x0)) → Wait(Right1(x0))
Begin(e(x0)) → Wait(Right2(x0))
Begin(l(x0)) → Wait(Right3(x0))
Begin(m(a(x0))) → Wait(Right4(x0))
Begin(a(x0)) → Wait(Right5(x0))
Begin(a(x0)) → Wait(Right6(x0))
Begin(s(x0)) → Wait(Right7(x0))
Right1(t(End(x0))) → Left(m(a(End(x0))))
Right2(t(End(x0))) → Left(n(s(End(x0))))
Right3(a(End(x0))) → Left(a(t(End(x0))))
Right4(o(End(x0))) → Left(t(e(n(End(x0)))))
Right5(o(m(End(x0)))) → Left(t(e(n(End(x0)))))
Right6(s(End(x0))) → Left(l(a(t(o(m(a(t(e(End(x0))))))))))
Right7(n(End(x0))) → Left(a(l(a(t(End(x0))))))
Right1(t(x0)) → At(Right1(x0))
Right2(t(x0)) → At(Right2(x0))
Right3(t(x0)) → At(Right3(x0))
Right4(t(x0)) → At(Right4(x0))
Right5(t(x0)) → At(Right5(x0))
Right6(t(x0)) → At(Right6(x0))
Right7(t(x0)) → At(Right7(x0))
Right1(o(x0)) → Ao(Right1(x0))
Right2(o(x0)) → Ao(Right2(x0))
Right3(o(x0)) → Ao(Right3(x0))
Right4(o(x0)) → Ao(Right4(x0))
Right5(o(x0)) → Ao(Right5(x0))
Right6(o(x0)) → Ao(Right6(x0))
Right7(o(x0)) → Ao(Right7(x0))
Right1(m(x0)) → Am(Right1(x0))
Right2(m(x0)) → Am(Right2(x0))
Right3(m(x0)) → Am(Right3(x0))
Right4(m(x0)) → Am(Right4(x0))
Right5(m(x0)) → Am(Right5(x0))
Right6(m(x0)) → Am(Right6(x0))
Right7(m(x0)) → Am(Right7(x0))
Right1(a(x0)) → Aa(Right1(x0))
Right2(a(x0)) → Aa(Right2(x0))
Right3(a(x0)) → Aa(Right3(x0))
Right4(a(x0)) → Aa(Right4(x0))
Right5(a(x0)) → Aa(Right5(x0))
Right6(a(x0)) → Aa(Right6(x0))
Right7(a(x0)) → Aa(Right7(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))
Right1(n(x0)) → An(Right1(x0))
Right2(n(x0)) → An(Right2(x0))
Right3(n(x0)) → An(Right3(x0))
Right4(n(x0)) → An(Right4(x0))
Right5(n(x0)) → An(Right5(x0))
Right6(n(x0)) → An(Right6(x0))
Right7(n(x0)) → An(Right7(x0))
Right1(s(x0)) → As(Right1(x0))
Right2(s(x0)) → As(Right2(x0))
Right3(s(x0)) → As(Right3(x0))
Right4(s(x0)) → As(Right4(x0))
Right5(s(x0)) → As(Right5(x0))
Right6(s(x0)) → As(Right6(x0))
Right7(s(x0)) → As(Right7(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))
At(Left(x0)) → Left(t(x0))
Ao(Left(x0)) → Left(o(x0))
Am(Left(x0)) → Left(m(x0))
Aa(Left(x0)) → Left(a(x0))
Ae(Left(x0)) → Left(e(x0))
An(Left(x0)) → Left(n(x0))
As(Left(x0)) → Left(s(x0))
Al(Left(x0)) → Left(l(x0))
Wait(Left(x0)) → Begin(x0)
t(o(x0)) → m(a(x0))
t(e(x0)) → n(s(x0))
a(l(x0)) → a(t(x0))
o(m(a(x0))) → t(e(n(x0)))
s(a(x0)) → l(a(t(o(m(a(t(e(x0))))))))
n(s(x0)) → a(l(a(t(x0))))