NO Nontermination Proof

Nontermination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(1(x0)) → Wait(Right1(x0))
Begin(9(x0)) → Wait(Right2(x0))
Begin(5(x0)) → Wait(Right3(x0))
Begin(4(x0)) → Wait(Right4(x0))
Begin(6(x0)) → Wait(Right5(x0))
Begin(8(x0)) → Wait(Right6(x0))
Begin(8(4(x0))) → Wait(Right7(x0))
Begin(4(x0)) → Wait(Right8(x0))
Begin(1(x0)) → Wait(Right9(x0))
Begin(9(x0)) → Wait(Right10(x0))
Begin(5(x0)) → Wait(Right11(x0))
Right1(3(End(x0))) → Left(4(1(End(x0))))
Right2(5(End(x0))) → Left(2(6(5(End(x0)))))
Right3(3(End(x0))) → Left(8(9(7(End(x0)))))
Right4(8(End(x0))) → Left(6(End(x0)))
Right5(2(End(x0))) → Left(4(3(End(x0))))
Right6(3(End(x0))) → Left(3(2(7(End(x0)))))
Right7(8(End(x0))) → Left(1(9(End(x0))))
Right8(8(8(End(x0)))) → Left(1(9(End(x0))))
Right9(7(End(x0))) → Left(6(9(End(x0))))
Right10(3(End(x0))) → Left(9(3(End(x0))))
Right11(7(End(x0))) → Left(1(0(End(x0))))
Right1(3(x0)) → A3(Right1(x0))
Right2(3(x0)) → A3(Right2(x0))
Right3(3(x0)) → A3(Right3(x0))
Right4(3(x0)) → A3(Right4(x0))
Right5(3(x0)) → A3(Right5(x0))
Right6(3(x0)) → A3(Right6(x0))
Right7(3(x0)) → A3(Right7(x0))
Right8(3(x0)) → A3(Right8(x0))
Right9(3(x0)) → A3(Right9(x0))
Right10(3(x0)) → A3(Right10(x0))
Right11(3(x0)) → A3(Right11(x0))
Right1(1(x0)) → A1(Right1(x0))
Right2(1(x0)) → A1(Right2(x0))
Right3(1(x0)) → A1(Right3(x0))
Right4(1(x0)) → A1(Right4(x0))
Right5(1(x0)) → A1(Right5(x0))
Right6(1(x0)) → A1(Right6(x0))
Right7(1(x0)) → A1(Right7(x0))
Right8(1(x0)) → A1(Right8(x0))
Right9(1(x0)) → A1(Right9(x0))
Right10(1(x0)) → A1(Right10(x0))
Right11(1(x0)) → A1(Right11(x0))
Right1(4(x0)) → A4(Right1(x0))
Right2(4(x0)) → A4(Right2(x0))
Right3(4(x0)) → A4(Right3(x0))
Right4(4(x0)) → A4(Right4(x0))
Right5(4(x0)) → A4(Right5(x0))
Right6(4(x0)) → A4(Right6(x0))
Right7(4(x0)) → A4(Right7(x0))
Right8(4(x0)) → A4(Right8(x0))
Right9(4(x0)) → A4(Right9(x0))
Right10(4(x0)) → A4(Right10(x0))
Right11(4(x0)) → A4(Right11(x0))
Right1(5(x0)) → A5(Right1(x0))
Right2(5(x0)) → A5(Right2(x0))
Right3(5(x0)) → A5(Right3(x0))
Right4(5(x0)) → A5(Right4(x0))
Right5(5(x0)) → A5(Right5(x0))
Right6(5(x0)) → A5(Right6(x0))
Right7(5(x0)) → A5(Right7(x0))
Right8(5(x0)) → A5(Right8(x0))
Right9(5(x0)) → A5(Right9(x0))
Right10(5(x0)) → A5(Right10(x0))
Right11(5(x0)) → A5(Right11(x0))
Right1(9(x0)) → A9(Right1(x0))
Right2(9(x0)) → A9(Right2(x0))
Right3(9(x0)) → A9(Right3(x0))
Right4(9(x0)) → A9(Right4(x0))
Right5(9(x0)) → A9(Right5(x0))
Right6(9(x0)) → A9(Right6(x0))
Right7(9(x0)) → A9(Right7(x0))
Right8(9(x0)) → A9(Right8(x0))
Right9(9(x0)) → A9(Right9(x0))
Right10(9(x0)) → A9(Right10(x0))
Right11(9(x0)) → A9(Right11(x0))
Right1(2(x0)) → A2(Right1(x0))
Right2(2(x0)) → A2(Right2(x0))
Right3(2(x0)) → A2(Right3(x0))
Right4(2(x0)) → A2(Right4(x0))
Right5(2(x0)) → A2(Right5(x0))
Right6(2(x0)) → A2(Right6(x0))
Right7(2(x0)) → A2(Right7(x0))
Right8(2(x0)) → A2(Right8(x0))
Right9(2(x0)) → A2(Right9(x0))
Right10(2(x0)) → A2(Right10(x0))
Right11(2(x0)) → A2(Right11(x0))
Right1(6(x0)) → A6(Right1(x0))
Right2(6(x0)) → A6(Right2(x0))
Right3(6(x0)) → A6(Right3(x0))
Right4(6(x0)) → A6(Right4(x0))
Right5(6(x0)) → A6(Right5(x0))
Right6(6(x0)) → A6(Right6(x0))
Right7(6(x0)) → A6(Right7(x0))
Right8(6(x0)) → A6(Right8(x0))
Right9(6(x0)) → A6(Right9(x0))
Right10(6(x0)) → A6(Right10(x0))
Right11(6(x0)) → A6(Right11(x0))
Right1(8(x0)) → A8(Right1(x0))
Right2(8(x0)) → A8(Right2(x0))
Right3(8(x0)) → A8(Right3(x0))
Right4(8(x0)) → A8(Right4(x0))
Right5(8(x0)) → A8(Right5(x0))
Right6(8(x0)) → A8(Right6(x0))
Right7(8(x0)) → A8(Right7(x0))
Right8(8(x0)) → A8(Right8(x0))
Right9(8(x0)) → A8(Right9(x0))
Right10(8(x0)) → A8(Right10(x0))
Right11(8(x0)) → A8(Right11(x0))
Right1(7(x0)) → A7(Right1(x0))
Right2(7(x0)) → A7(Right2(x0))
Right3(7(x0)) → A7(Right3(x0))
Right4(7(x0)) → A7(Right4(x0))
Right5(7(x0)) → A7(Right5(x0))
Right6(7(x0)) → A7(Right6(x0))
Right7(7(x0)) → A7(Right7(x0))
Right8(7(x0)) → A7(Right8(x0))
Right9(7(x0)) → A7(Right9(x0))
Right10(7(x0)) → A7(Right10(x0))
Right11(7(x0)) → A7(Right11(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))
A3(Left(x0)) → Left(3(x0))
A1(Left(x0)) → Left(1(x0))
A4(Left(x0)) → Left(4(x0))
A5(Left(x0)) → Left(5(x0))
A9(Left(x0)) → Left(9(x0))
A2(Left(x0)) → Left(2(x0))
A6(Left(x0)) → Left(6(x0))
A8(Left(x0)) → Left(8(x0))
A7(Left(x0)) → Left(7(x0))
A0(Left(x0)) → Left(0(x0))
Wait(Left(x0)) → Begin(x0)
3(1(x0)) → 4(1(x0))
5(9(x0)) → 2(6(5(x0)))
3(5(x0)) → 8(9(7(x0)))
9(x0) → 3(2(3(x0)))
8(4(x0)) → 6(x0)
2(6(x0)) → 4(3(x0))
3(8(x0)) → 3(2(7(x0)))
9(x0) → 5(0(2(x0)))
8(8(4(x0))) → 1(9(x0))
7(1(x0)) → 6(9(x0))
3(9(x0)) → 9(3(x0))
7(5(x0)) → 1(0(x0))

Proof

1 Loop

The following loop proves nontermination.

t0 = Begin(9(3(End(x104336))))
→ε Wait(Right10(3(End(x104336))))
→1 Wait(Left(9(3(End(x104336)))))
→ε Begin(9(3(End(x104336))))
= t3
where t3 = t0σ and σ = {x104336/x104336}