NO Nontermination Proof

Nontermination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

Begin(0(x0)) → Wait(Right1(x0))
Begin(1(x0)) → Wait(Right2(x0))
Begin(1(x0)) → Wait(Right3(x0))
Begin(0(x0)) → Wait(Right4(x0))
Right1(1(End(x0))) → Left(0(0(0(1(End(x0))))))
Right2(0(End(x0))) → Left(1(End(x0)))
Right3(1(End(x0))) → Left(0(0(0(0(End(x0))))))
Right4(0(End(x0))) → Left(0(End(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))
Right1(0(x0)) → A0(Right1(x0))
Right2(0(x0)) → A0(Right2(x0))
Right3(0(x0)) → A0(Right3(x0))
Right4(0(x0)) → A0(Right4(x0))
A1(Left(x0)) → Left(1(x0))
A0(Left(x0)) → Left(0(x0))
Wait(Left(x0)) → Begin(x0)
1(0(x0)) → 0(0(0(1(x0))))
0(1(x0)) → 1(x0)
1(1(x0)) → 0(0(0(0(x0))))
0(0(x0)) → 0(x0)

Proof

1 Loop

The following loop proves nontermination.

t0 = Begin(0(1(End(x28801))))
→ε Wait(Right1(1(End(x28801))))
→1 Wait(Left(0(0(0(1(End(x28801)))))))
→ε Begin(0(0(0(1(End(x28801))))))
→1.1.1 Begin(0(0(1(End(x28801)))))
→1.1 Begin(0(1(End(x28801))))
= t5
where t5 = t0σ and σ = {x28801/x28801}