NO Nontermination Proof

Nontermination 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(0(x0))) → Wait(Right3(x0))
Begin(0(x0)) → Wait(Right4(x0))
Begin(s(s(x0))) → Wait(Right5(x0))
Begin(s(x0)) → Wait(Right6(x0))
Begin(half(s(s(s(s(x0)))))) → Wait(Right7(x0))
Begin(s(s(s(s(x0))))) → Wait(Right8(x0))
Begin(s(s(s(x0)))) → Wait(Right9(x0))
Begin(s(s(x0))) → Wait(Right10(x0))
Begin(s(x0)) → Wait(Right11(x0))
Begin(s(s(s(x0)))) → Wait(Right12(x0))
Begin(s(s(x0))) → Wait(Right13(x0))
Begin(s(x0)) → Wait(Right14(x0))
Begin(s(p(s(x0)))) → Wait(Right15(x0))
Begin(p(s(x0))) → Wait(Right16(x0))
Begin(s(x0)) → Wait(Right17(x0))
Right1(log(End(x0))) → Left(s(log(half(s(End(x0))))))
Right2(half(End(x0))) → Left(0(s(s(half(End(x0))))))
Right3(half(End(x0))) → Left(0(End(x0)))
Right4(half(s(End(x0)))) → Left(0(End(x0)))
Right5(half(End(x0))) → Left(s(half(p(s(s(End(x0)))))))
Right6(half(s(End(x0)))) → Left(s(half(p(s(s(End(x0)))))))
Right7(half(End(x0))) → Left(s(s(half(half(End(x0))))))
Right8(half(half(End(x0)))) → Left(s(s(half(half(End(x0))))))
Right9(half(half(s(End(x0))))) → Left(s(s(half(half(End(x0))))))
Right10(half(half(s(s(End(x0)))))) → Left(s(s(half(half(End(x0))))))
Right11(half(half(s(s(s(End(x0))))))) → Left(s(s(half(half(End(x0))))))
Right12(p(End(x0))) → Left(s(p(s(s(End(x0))))))
Right13(p(s(End(x0)))) → Left(s(p(s(s(End(x0))))))
Right14(p(s(s(End(x0))))) → Left(s(p(s(s(End(x0))))))
Right15(s(End(x0))) → Left(s(s(End(x0))))
Right16(s(s(End(x0)))) → Left(s(s(End(x0))))
Right17(s(s(p(End(x0))))) → Left(s(s(End(x0))))
Right1(log(x0)) → Alog(Right1(x0))
Right2(log(x0)) → Alog(Right2(x0))
Right3(log(x0)) → Alog(Right3(x0))
Right4(log(x0)) → Alog(Right4(x0))
Right5(log(x0)) → Alog(Right5(x0))
Right6(log(x0)) → Alog(Right6(x0))
Right7(log(x0)) → Alog(Right7(x0))
Right8(log(x0)) → Alog(Right8(x0))
Right9(log(x0)) → Alog(Right9(x0))
Right10(log(x0)) → Alog(Right10(x0))
Right11(log(x0)) → Alog(Right11(x0))
Right12(log(x0)) → Alog(Right12(x0))
Right13(log(x0)) → Alog(Right13(x0))
Right14(log(x0)) → Alog(Right14(x0))
Right15(log(x0)) → Alog(Right15(x0))
Right16(log(x0)) → Alog(Right16(x0))
Right17(log(x0)) → Alog(Right17(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))
Right8(s(x0)) → As(Right8(x0))
Right9(s(x0)) → As(Right9(x0))
Right10(s(x0)) → As(Right10(x0))
Right11(s(x0)) → As(Right11(x0))
Right12(s(x0)) → As(Right12(x0))
Right13(s(x0)) → As(Right13(x0))
Right14(s(x0)) → As(Right14(x0))
Right15(s(x0)) → As(Right15(x0))
Right16(s(x0)) → As(Right16(x0))
Right17(s(x0)) → As(Right17(x0))
Right1(half(x0)) → Ahalf(Right1(x0))
Right2(half(x0)) → Ahalf(Right2(x0))
Right3(half(x0)) → Ahalf(Right3(x0))
Right4(half(x0)) → Ahalf(Right4(x0))
Right5(half(x0)) → Ahalf(Right5(x0))
Right6(half(x0)) → Ahalf(Right6(x0))
Right7(half(x0)) → Ahalf(Right7(x0))
Right8(half(x0)) → Ahalf(Right8(x0))
Right9(half(x0)) → Ahalf(Right9(x0))
Right10(half(x0)) → Ahalf(Right10(x0))
Right11(half(x0)) → Ahalf(Right11(x0))
Right12(half(x0)) → Ahalf(Right12(x0))
Right13(half(x0)) → Ahalf(Right13(x0))
Right14(half(x0)) → Ahalf(Right14(x0))
Right15(half(x0)) → Ahalf(Right15(x0))
Right16(half(x0)) → Ahalf(Right16(x0))
Right17(half(x0)) → Ahalf(Right17(x0))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
Right5(0(x0)) → A0(Right5(x0))
Right6(0(x0)) → A0(Right6(x0))
Right7(0(x0)) → A0(Right7(x0))
Right8(0(x0)) → A0(Right8(x0))
Right9(0(x0)) → A0(Right9(x0))
Right10(0(x0)) → A0(Right10(x0))
Right11(0(x0)) → A0(Right11(x0))
Right12(0(x0)) → A0(Right12(x0))
Right13(0(x0)) → A0(Right13(x0))
Right14(0(x0)) → A0(Right14(x0))
Right15(0(x0)) → A0(Right15(x0))
Right16(0(x0)) → A0(Right16(x0))
Right17(0(x0)) → A0(Right17(x0))
Right1(p(x0)) → Ap(Right1(x0))
Right2(p(x0)) → Ap(Right2(x0))
Right3(p(x0)) → Ap(Right3(x0))
Right4(p(x0)) → Ap(Right4(x0))
Right5(p(x0)) → Ap(Right5(x0))
Right6(p(x0)) → Ap(Right6(x0))
Right7(p(x0)) → Ap(Right7(x0))
Right8(p(x0)) → Ap(Right8(x0))
Right9(p(x0)) → Ap(Right9(x0))
Right10(p(x0)) → Ap(Right10(x0))
Right11(p(x0)) → Ap(Right11(x0))
Right12(p(x0)) → Ap(Right12(x0))
Right13(p(x0)) → Ap(Right13(x0))
Right14(p(x0)) → Ap(Right14(x0))
Right15(p(x0)) → Ap(Right15(x0))
Right16(p(x0)) → Ap(Right16(x0))
Right17(p(x0)) → Ap(Right17(x0))
Alog(Left(x0)) → Left(log(x0))
As(Left(x0)) → Left(s(x0))
Ahalf(Left(x0)) → Left(half(x0))
A0(Left(x0)) → Left(0(x0))
Ap(Left(x0)) → Left(p(x0))
Wait(Left(x0)) → Begin(x0)
log(s(x0)) → s(log(half(s(x0))))
half(0(x0)) → 0(s(s(half(x0))))
half(s(0(x0))) → 0(x0)
half(s(s(x0))) → s(half(p(s(s(x0)))))
half(half(s(s(s(s(x0)))))) → s(s(half(half(x0))))
p(s(s(s(x0)))) → s(p(s(s(x0))))
s(s(p(s(x0)))) → s(s(x0))
0(x0) → x0

Proof

1 Loop

The following loop proves nontermination.

t0 = Begin(s(p(s(s(End(x85151))))))
→ε Wait(Right14(p(s(s(End(x85151))))))
→1 Wait(Left(s(p(s(s(End(x85151)))))))
→ε Begin(s(p(s(s(End(x85151))))))
= t3
where t3 = t0σ and σ = {x85151/x85151}