MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(s(x0)) → Wait(Right1(x0))
Begin(0(x0)) → Wait(Right2(x0))
Begin(s(x0)) → Wait(Right3(x0))
Right1(f(End(x0))) → Left(s(s(f(p(s(End(x0)))))))
Right2(f(End(x0))) → Left(0(End(x0)))
Right3(p(End(x0))) → Left(End(x0))
Right1(f(x0)) → Af(Right1(x0))
Right2(f(x0)) → Af(Right2(x0))
Right3(f(x0)) → Af(Right3(x0))
Right1(s(x0)) → As(Right1(x0))
Right2(s(x0)) → As(Right2(x0))
Right3(s(x0)) → As(Right3(x0))
Right1(p(x0)) → Ap(Right1(x0))
Right2(p(x0)) → Ap(Right2(x0))
Right3(p(x0)) → Ap(Right3(x0))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Af(Left(x0)) → Left(f(x0))
As(Left(x0)) → Left(s(x0))
Ap(Left(x0)) → Left(p(x0))
A0(Left(x0)) → Left(0(x0))
Wait(Left(x0)) → Begin(x0)
f(s(x0)) → s(s(f(p(s(x0)))))
f(0(x0)) → 0(x0)
p(s(x0)) → x0

Proof

1 Termination Assumption

We assume termination of the following TRS
Begin(s(x0)) → Wait(Right1(x0))
Begin(0(x0)) → Wait(Right2(x0))
Begin(s(x0)) → Wait(Right3(x0))
Right1(f(End(x0))) → Left(s(s(f(p(s(End(x0)))))))
Right2(f(End(x0))) → Left(0(End(x0)))
Right3(p(End(x0))) → Left(End(x0))
Right1(f(x0)) → Af(Right1(x0))
Right2(f(x0)) → Af(Right2(x0))
Right3(f(x0)) → Af(Right3(x0))
Right1(s(x0)) → As(Right1(x0))
Right2(s(x0)) → As(Right2(x0))
Right3(s(x0)) → As(Right3(x0))
Right1(p(x0)) → Ap(Right1(x0))
Right2(p(x0)) → Ap(Right2(x0))
Right3(p(x0)) → Ap(Right3(x0))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Af(Left(x0)) → Left(f(x0))
As(Left(x0)) → Left(s(x0))
Ap(Left(x0)) → Left(p(x0))
A0(Left(x0)) → Left(0(x0))
Wait(Left(x0)) → Begin(x0)
f(s(x0)) → s(s(f(p(s(x0)))))
f(0(x0)) → 0(x0)
p(s(x0)) → x0