NO Nontermination Proof

Nontermination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(a(x0)) → Wait(Right1(x0))
Begin(a(x0)) → Wait(Right2(x0))
Begin(l1(x0)) → Wait(Right3(x0))
Begin(a(l2(x0))) → Wait(Right4(x0))
Begin(l2(x0)) → Wait(Right5(x0))
Begin(b(x0)) → Wait(Right6(x0))
Begin(b(x0)) → Wait(Right7(x0))
Begin(l1(x0)) → Wait(Right8(x0))
Begin(l2(x0)) → Wait(Right9(x0))
Begin(a(x0)) → Wait(Right10(x0))
Right1(r1(End(x0))) → Left(a(a(a(r1(End(x0))))))
Right2(r2(End(x0))) → Left(a(a(a(r2(End(x0))))))
Right3(a(End(x0))) → Left(l1(a(a(a(End(x0))))))
Right4(a(End(x0))) → Left(l2(a(a(End(x0)))))
Right5(a(a(End(x0)))) → Left(l2(a(a(End(x0)))))
Right6(r1(End(x0))) → Left(l1(b(End(x0))))
Right7(r2(End(x0))) → Left(l2(a(b(End(x0)))))
Right8(b(End(x0))) → Left(b(r2(End(x0))))
Right9(b(End(x0))) → Left(b(r1(End(x0))))
Right10(a(End(x0))) → Left(End(x0))
Right1(r1(x0)) → Ar1(Right1(x0))
Right2(r1(x0)) → Ar1(Right2(x0))
Right3(r1(x0)) → Ar1(Right3(x0))
Right4(r1(x0)) → Ar1(Right4(x0))
Right5(r1(x0)) → Ar1(Right5(x0))
Right6(r1(x0)) → Ar1(Right6(x0))
Right7(r1(x0)) → Ar1(Right7(x0))
Right8(r1(x0)) → Ar1(Right8(x0))
Right9(r1(x0)) → Ar1(Right9(x0))
Right10(r1(x0)) → Ar1(Right10(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))
Right8(a(x0)) → Aa(Right8(x0))
Right9(a(x0)) → Aa(Right9(x0))
Right10(a(x0)) → Aa(Right10(x0))
Right1(r2(x0)) → Ar2(Right1(x0))
Right2(r2(x0)) → Ar2(Right2(x0))
Right3(r2(x0)) → Ar2(Right3(x0))
Right4(r2(x0)) → Ar2(Right4(x0))
Right5(r2(x0)) → Ar2(Right5(x0))
Right6(r2(x0)) → Ar2(Right6(x0))
Right7(r2(x0)) → Ar2(Right7(x0))
Right8(r2(x0)) → Ar2(Right8(x0))
Right9(r2(x0)) → Ar2(Right9(x0))
Right10(r2(x0)) → Ar2(Right10(x0))
Right1(l1(x0)) → Al1(Right1(x0))
Right2(l1(x0)) → Al1(Right2(x0))
Right3(l1(x0)) → Al1(Right3(x0))
Right4(l1(x0)) → Al1(Right4(x0))
Right5(l1(x0)) → Al1(Right5(x0))
Right6(l1(x0)) → Al1(Right6(x0))
Right7(l1(x0)) → Al1(Right7(x0))
Right8(l1(x0)) → Al1(Right8(x0))
Right9(l1(x0)) → Al1(Right9(x0))
Right10(l1(x0)) → Al1(Right10(x0))
Right1(l2(x0)) → Al2(Right1(x0))
Right2(l2(x0)) → Al2(Right2(x0))
Right3(l2(x0)) → Al2(Right3(x0))
Right4(l2(x0)) → Al2(Right4(x0))
Right5(l2(x0)) → Al2(Right5(x0))
Right6(l2(x0)) → Al2(Right6(x0))
Right7(l2(x0)) → Al2(Right7(x0))
Right8(l2(x0)) → Al2(Right8(x0))
Right9(l2(x0)) → Al2(Right9(x0))
Right10(l2(x0)) → Al2(Right10(x0))
Right1(b(x0)) → Ab(Right1(x0))
Right2(b(x0)) → Ab(Right2(x0))
Right3(b(x0)) → Ab(Right3(x0))
Right4(b(x0)) → Ab(Right4(x0))
Right5(b(x0)) → Ab(Right5(x0))
Right6(b(x0)) → Ab(Right6(x0))
Right7(b(x0)) → Ab(Right7(x0))
Right8(b(x0)) → Ab(Right8(x0))
Right9(b(x0)) → Ab(Right9(x0))
Right10(b(x0)) → Ab(Right10(x0))
Ar1(Left(x0)) → Left(r1(x0))
Aa(Left(x0)) → Left(a(x0))
Ar2(Left(x0)) → Left(r2(x0))
Al1(Left(x0)) → Left(l1(x0))
Al2(Left(x0)) → Left(l2(x0))
Ab(Left(x0)) → Left(b(x0))
Wait(Left(x0)) → Begin(x0)
r1(a(x0)) → a(a(a(r1(x0))))
r2(a(x0)) → a(a(a(r2(x0))))
a(l1(x0)) → l1(a(a(a(x0))))
a(a(l2(x0))) → l2(a(a(x0)))
r1(b(x0)) → l1(b(x0))
r2(b(x0)) → l2(a(b(x0)))
b(l1(x0)) → b(r2(x0))
b(l2(x0)) → b(r1(x0))
a(a(x0)) → x0

Proof

1 Loop

The following loop proves nontermination.

t0 = Begin(l2(a(a(End(x31887)))))
→ε Wait(Right5(a(a(End(x31887)))))
→1 Wait(Left(l2(a(a(End(x31887))))))
→ε Begin(l2(a(a(End(x31887)))))
= t3
where t3 = t0σ and σ = {x31887/x31887}