NO Nontermination Proof

Nontermination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Loop

The following loop proves nontermination.

t0 = Begin(0(1(1(1(End(x18658))))))
→ε Wait(Right5(1(1(End(x18658)))))
→1 Wait(Left(0(0(0(0(End(x18658)))))))
→ε Begin(0(0(0(0(End(x18658))))))
→1 Begin(0(1(1(1(End(x18658))))))
= t4
where t4 = t0σ and σ = {x18658/x18658}