NO Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Secret_05_SRS/aprove4.srs-torpacyc2out-split.srs

Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 NonTerminationProof (⇒, 234 ms)
↳2 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Begin(s(x)) → Wait(Right1(x))
Begin(s(0(x))) → Wait(Right2(x))
Begin(0(x)) → Wait(Right3(x))
Begin(s(s(x))) → Wait(Right4(x))
Begin(s(x)) → Wait(Right5(x))
Begin(half(s(s(s(s(x)))))) → Wait(Right6(x))
Begin(s(s(s(s(x))))) → Wait(Right7(x))
Begin(s(s(s(x)))) → Wait(Right8(x))
Begin(s(s(x))) → Wait(Right9(x))
Begin(s(x)) → Wait(Right10(x))
Begin(s(s(s(x)))) → Wait(Right11(x))
Begin(s(s(x))) → Wait(Right12(x))
Begin(s(x)) → Wait(Right13(x))
Begin(s(p(s(x)))) → Wait(Right14(x))
Begin(p(s(x))) → Wait(Right15(x))
Begin(s(x)) → Wait(Right16(x))
Right1(log(End(x))) → Left(s(log(half(s(End(x))))))
Right2(half(End(x))) → Left(0(End(x)))
Right3(half(s(End(x)))) → Left(0(End(x)))
Right4(half(End(x))) → Left(s(half(p(s(s(End(x)))))))
Right5(half(s(End(x)))) → Left(s(half(p(s(s(End(x)))))))
Right6(half(End(x))) → Left(s(s(half(half(End(x))))))
Right7(half(half(End(x)))) → Left(s(s(half(half(End(x))))))
Right8(half(half(s(End(x))))) → Left(s(s(half(half(End(x))))))
Right9(half(half(s(s(End(x)))))) → Left(s(s(half(half(End(x))))))
Right10(half(half(s(s(s(End(x))))))) → Left(s(s(half(half(End(x))))))
Right11(p(End(x))) → Left(s(p(s(s(End(x))))))
Right12(p(s(End(x)))) → Left(s(p(s(s(End(x))))))
Right13(p(s(s(End(x))))) → Left(s(p(s(s(End(x))))))
Right14(s(End(x))) → Left(s(s(End(x))))
Right15(s(s(End(x)))) → Left(s(s(End(x))))
Right16(s(s(p(End(x))))) → Left(s(s(End(x))))
Right1(log(x)) → Alog(Right1(x))
Right2(log(x)) → Alog(Right2(x))
Right3(log(x)) → Alog(Right3(x))
Right4(log(x)) → Alog(Right4(x))
Right5(log(x)) → Alog(Right5(x))
Right6(log(x)) → Alog(Right6(x))
Right7(log(x)) → Alog(Right7(x))
Right8(log(x)) → Alog(Right8(x))
Right9(log(x)) → Alog(Right9(x))
Right10(log(x)) → Alog(Right10(x))
Right11(log(x)) → Alog(Right11(x))
Right12(log(x)) → Alog(Right12(x))
Right13(log(x)) → Alog(Right13(x))
Right14(log(x)) → Alog(Right14(x))
Right15(log(x)) → Alog(Right15(x))
Right16(log(x)) → Alog(Right16(x))
Right1(s(x)) → As(Right1(x))
Right2(s(x)) → As(Right2(x))
Right3(s(x)) → As(Right3(x))
Right4(s(x)) → As(Right4(x))
Right5(s(x)) → As(Right5(x))
Right6(s(x)) → As(Right6(x))
Right7(s(x)) → As(Right7(x))
Right8(s(x)) → As(Right8(x))
Right9(s(x)) → As(Right9(x))
Right10(s(x)) → As(Right10(x))
Right11(s(x)) → As(Right11(x))
Right12(s(x)) → As(Right12(x))
Right13(s(x)) → As(Right13(x))
Right14(s(x)) → As(Right14(x))
Right15(s(x)) → As(Right15(x))
Right16(s(x)) → As(Right16(x))
Right1(half(x)) → Ahalf(Right1(x))
Right2(half(x)) → Ahalf(Right2(x))
Right3(half(x)) → Ahalf(Right3(x))
Right4(half(x)) → Ahalf(Right4(x))
Right5(half(x)) → Ahalf(Right5(x))
Right6(half(x)) → Ahalf(Right6(x))
Right7(half(x)) → Ahalf(Right7(x))
Right8(half(x)) → Ahalf(Right8(x))
Right9(half(x)) → Ahalf(Right9(x))
Right10(half(x)) → Ahalf(Right10(x))
Right11(half(x)) → Ahalf(Right11(x))
Right12(half(x)) → Ahalf(Right12(x))
Right13(half(x)) → Ahalf(Right13(x))
Right14(half(x)) → Ahalf(Right14(x))
Right15(half(x)) → Ahalf(Right15(x))
Right16(half(x)) → Ahalf(Right16(x))
Right1(0(x)) → A0(Right1(x))
Right2(0(x)) → A0(Right2(x))
Right3(0(x)) → A0(Right3(x))
Right4(0(x)) → A0(Right4(x))
Right5(0(x)) → A0(Right5(x))
Right6(0(x)) → A0(Right6(x))
Right7(0(x)) → A0(Right7(x))
Right8(0(x)) → A0(Right8(x))
Right9(0(x)) → A0(Right9(x))
Right10(0(x)) → A0(Right10(x))
Right11(0(x)) → A0(Right11(x))
Right12(0(x)) → A0(Right12(x))
Right13(0(x)) → A0(Right13(x))
Right14(0(x)) → A0(Right14(x))
Right15(0(x)) → A0(Right15(x))
Right16(0(x)) → A0(Right16(x))
Right1(p(x)) → Ap(Right1(x))
Right2(p(x)) → Ap(Right2(x))
Right3(p(x)) → Ap(Right3(x))
Right4(p(x)) → Ap(Right4(x))
Right5(p(x)) → Ap(Right5(x))
Right6(p(x)) → Ap(Right6(x))
Right7(p(x)) → Ap(Right7(x))
Right8(p(x)) → Ap(Right8(x))
Right9(p(x)) → Ap(Right9(x))
Right10(p(x)) → Ap(Right10(x))
Right11(p(x)) → Ap(Right11(x))
Right12(p(x)) → Ap(Right12(x))
Right13(p(x)) → Ap(Right13(x))
Right14(p(x)) → Ap(Right14(x))
Right15(p(x)) → Ap(Right15(x))
Right16(p(x)) → Ap(Right16(x))
Alog(Left(x)) → Left(log(x))
As(Left(x)) → Left(s(x))
Ahalf(Left(x)) → Left(half(x))
A0(Left(x)) → Left(0(x))
Ap(Left(x)) → Left(p(x))
Wait(Left(x)) → Begin(x)
log(s(x)) → s(log(half(s(x))))
half(s(0(x))) → 0(x)
half(s(s(x))) → s(half(p(s(s(x)))))
half(half(s(s(s(s(x)))))) → s(s(half(half(x))))
p(s(s(s(x)))) → s(p(s(s(x))))
s(s(p(s(x)))) → s(s(x))

Q is empty.

(1) NonTerminationProof (COMPLETE transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:
Wait Left s p s s End → Wait Left s p s s End

Wait Left s p s s End → Wait Left s p s s End
by OverlapClosure OC 2
Wait Left s → Wait Right13
by OverlapClosure OC 2
Wait Left → Begin
by original rule (OC 1)
Begin s → Wait Right13
by original rule (OC 1)
Right13 p s s End → Left s p s s End
by original rule (OC 1)

(2) NO