NO Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_06/02-rotate.srs

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

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

(0) Obligation:

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

begin(end(x)) → rewrite(end(x))
begin(a(x)) → rotate(cut(Ca(guess(x))))
begin(p(x)) → rotate(cut(Cp(guess(x))))
begin(A(x)) → rotate(cut(CA(guess(x))))
guess(a(x)) → Ca(guess(x))
guess(p(x)) → Cp(guess(x))
guess(A(x)) → CA(guess(x))
guess(a(x)) → moveleft(Ba(wait(x)))
guess(p(x)) → moveleft(Bp(wait(x)))
guess(A(x)) → moveleft(BA(wait(x)))
guess(end(x)) → finish(end(x))
Ca(moveleft(Ba(x))) → moveleft(Ba(Aa(x)))
Cp(moveleft(Ba(x))) → moveleft(Ba(Ap(x)))
CA(moveleft(Ba(x))) → moveleft(Ba(AA(x)))
Ca(moveleft(Bp(x))) → moveleft(Bp(Aa(x)))
Cp(moveleft(Bp(x))) → moveleft(Bp(Ap(x)))
CA(moveleft(Bp(x))) → moveleft(Bp(AA(x)))
Ca(moveleft(BA(x))) → moveleft(BA(Aa(x)))
Cp(moveleft(BA(x))) → moveleft(BA(Ap(x)))
CA(moveleft(BA(x))) → moveleft(BA(AA(x)))
cut(moveleft(Ba(x))) → Da(cut(goright(x)))
cut(moveleft(Bp(x))) → Dp(cut(goright(x)))
cut(moveleft(BA(x))) → DA(cut(goright(x)))
goright(Aa(x)) → Ca(goright(x))
goright(Ap(x)) → Cp(goright(x))
goright(AA(x)) → CA(goright(x))
goright(wait(a(x))) → moveleft(Ba(wait(x)))
goright(wait(p(x))) → moveleft(Bp(wait(x)))
goright(wait(A(x))) → moveleft(BA(wait(x)))
goright(wait(end(x))) → finish(end(x))
Ca(finish(x)) → finish(a(x))
Cp(finish(x)) → finish(p(x))
CA(finish(x)) → finish(A(x))
cut(finish(x)) → finish2(x)
Da(finish2(x)) → finish2(a(x))
Dp(finish2(x)) → finish2(p(x))
DA(finish2(x)) → finish2(A(x))
rotate(finish2(x)) → rewrite(x)
rewrite(a(p(x))) → begin(p(a(A(x))))
rewrite(a(A(x))) → begin(A(a(x)))
rewrite(p(A(A(x)))) → begin(a(p(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:
rotate finish2 a A end → rotate finish2 a A end

rotate finish2 a A end → rotate finish2 a A end
by OverlapClosure OC 3
rotate finish2 a A end → rotate Da finish2 A end
by OverlapClosure OC 3
rotate finish2 a A end → rotate Da cut finish A end
by OverlapClosure OC 3
rotate finish2 a A end → rotate Da cut CA finish end
by OverlapClosure OC 2
rotate finish2 a A → rotate Da cut CA goright wait
by OverlapClosure OC 2
rotate finish2 a A → begin A a
by OverlapClosure OC 2
rotate finish2 → rewrite
by original rule (OC 1)
rewrite a A → begin A a
by original rule (OC 1)
begin A a → rotate Da cut CA goright wait
by OverlapClosure OC 3
begin A a → rotate cut moveleft Ba AA wait
by OverlapClosure OC 3
begin A a → rotate cut CA moveleft Ba wait
by OverlapClosure OC 2
begin A → rotate cut CA guess
by original rule (OC 1)
guess a → moveleft Ba wait
by original rule (OC 1)
CA moveleft Ba → moveleft Ba AA
by original rule (OC 1)
cut moveleft Ba AA → Da cut CA goright
by OverlapClosure OC 2
cut moveleft Ba → Da cut goright
by original rule (OC 1)
goright AA → CA goright
by original rule (OC 1)
goright wait end → finish end
by original rule (OC 1)
CA finish → finish A
by original rule (OC 1)
cut finish → finish2
by original rule (OC 1)
Da finish2 → finish2 a
by original rule (OC 1)

(2) NO