MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(c(x0)) → Wait(Right1(x0))
Begin(f(c(x0))) → Wait(Right2(x0))
Begin(c(x0)) → Wait(Right3(x0))
Begin(g(x0)) → Wait(Right4(x0))
Begin(f(g(x0))) → Wait(Right5(x0))
Begin(g(x0)) → Wait(Right6(x0))
Right1(g(End(x0))) → Left(g(f(c(End(x0)))))
Right2(g(End(x0))) → Left(g(f(f(c(End(x0))))))
Right3(g(f(End(x0)))) → Left(g(f(f(c(End(x0))))))
Right4(g(End(x0))) → Left(g(f(g(End(x0)))))
Right5(f(End(x0))) → Left(g(f(End(x0))))
Right6(f(f(End(x0)))) → Left(g(f(End(x0))))
Right1(g(x0)) → Ag(Right1(x0))
Right2(g(x0)) → Ag(Right2(x0))
Right3(g(x0)) → Ag(Right3(x0))
Right4(g(x0)) → Ag(Right4(x0))
Right5(g(x0)) → Ag(Right5(x0))
Right6(g(x0)) → Ag(Right6(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
Right5(c(x0)) → Ac(Right5(x0))
Right6(c(x0)) → Ac(Right6(x0))
Right1(f(x0)) → Af(Right1(x0))
Right2(f(x0)) → Af(Right2(x0))
Right3(f(x0)) → Af(Right3(x0))
Right4(f(x0)) → Af(Right4(x0))
Right5(f(x0)) → Af(Right5(x0))
Right6(f(x0)) → Af(Right6(x0))
Ag(Left(x0)) → Left(g(x0))
Ac(Left(x0)) → Left(c(x0))
Af(Left(x0)) → Left(f(x0))
Wait(Left(x0)) → Begin(x0)
g(c(x0)) → g(f(c(x0)))
g(f(c(x0))) → g(f(f(c(x0))))
g(g(x0)) → g(f(g(x0)))
f(f(g(x0))) → g(f(x0))

Proof

1 Termination Assumption

We assume termination of the following TRS
Begin(c(x0)) → Wait(Right1(x0))
Begin(f(c(x0))) → Wait(Right2(x0))
Begin(c(x0)) → Wait(Right3(x0))
Begin(g(x0)) → Wait(Right4(x0))
Begin(f(g(x0))) → Wait(Right5(x0))
Begin(g(x0)) → Wait(Right6(x0))
Right1(g(End(x0))) → Left(g(f(c(End(x0)))))
Right2(g(End(x0))) → Left(g(f(f(c(End(x0))))))
Right3(g(f(End(x0)))) → Left(g(f(f(c(End(x0))))))
Right4(g(End(x0))) → Left(g(f(g(End(x0)))))
Right5(f(End(x0))) → Left(g(f(End(x0))))
Right6(f(f(End(x0)))) → Left(g(f(End(x0))))
Right1(g(x0)) → Ag(Right1(x0))
Right2(g(x0)) → Ag(Right2(x0))
Right3(g(x0)) → Ag(Right3(x0))
Right4(g(x0)) → Ag(Right4(x0))
Right5(g(x0)) → Ag(Right5(x0))
Right6(g(x0)) → Ag(Right6(x0))
Right1(c(x0)) → Ac(Right1(x0))
Right2(c(x0)) → Ac(Right2(x0))
Right3(c(x0)) → Ac(Right3(x0))
Right4(c(x0)) → Ac(Right4(x0))
Right5(c(x0)) → Ac(Right5(x0))
Right6(c(x0)) → Ac(Right6(x0))
Right1(f(x0)) → Af(Right1(x0))
Right2(f(x0)) → Af(Right2(x0))
Right3(f(x0)) → Af(Right3(x0))
Right4(f(x0)) → Af(Right4(x0))
Right5(f(x0)) → Af(Right5(x0))
Right6(f(x0)) → Af(Right6(x0))
Ag(Left(x0)) → Left(g(x0))
Ac(Left(x0)) → Left(c(x0))
Af(Left(x0)) → Left(f(x0))
Wait(Left(x0)) → Begin(x0)
g(c(x0)) → g(f(c(x0)))
g(f(c(x0))) → g(f(f(c(x0))))
g(g(x0)) → g(f(g(x0)))
f(f(g(x0))) → g(f(x0))