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

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

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

(0) Obligation:

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

begin(end(x)) → rewrite(end(x))
begin(f(x)) → rotate(cut(Cf(guess(x))))
begin(n(x)) → rotate(cut(Cn(guess(x))))
begin(c(x)) → rotate(cut(Cc(guess(x))))
begin(a(x)) → rotate(cut(Ca(guess(x))))
begin(s(x)) → rotate(cut(Cs(guess(x))))
guess(f(x)) → Cf(guess(x))
guess(n(x)) → Cn(guess(x))
guess(c(x)) → Cc(guess(x))
guess(a(x)) → Ca(guess(x))
guess(s(x)) → Cs(guess(x))
guess(f(x)) → moveleft(Bf(wait(x)))
guess(n(x)) → moveleft(Bn(wait(x)))
guess(c(x)) → moveleft(Bc(wait(x)))
guess(a(x)) → moveleft(Ba(wait(x)))
guess(s(x)) → moveleft(Bs(wait(x)))
guess(end(x)) → finish(end(x))
Cf(moveleft(Bf(x))) → moveleft(Bf(Af(x)))
Cn(moveleft(Bf(x))) → moveleft(Bf(An(x)))
Cc(moveleft(Bf(x))) → moveleft(Bf(Ac(x)))
Ca(moveleft(Bf(x))) → moveleft(Bf(Aa(x)))
Cs(moveleft(Bf(x))) → moveleft(Bf(As(x)))
Cf(moveleft(Bn(x))) → moveleft(Bn(Af(x)))
Cn(moveleft(Bn(x))) → moveleft(Bn(An(x)))
Cc(moveleft(Bn(x))) → moveleft(Bn(Ac(x)))
Ca(moveleft(Bn(x))) → moveleft(Bn(Aa(x)))
Cs(moveleft(Bn(x))) → moveleft(Bn(As(x)))
Cf(moveleft(Bc(x))) → moveleft(Bc(Af(x)))
Cn(moveleft(Bc(x))) → moveleft(Bc(An(x)))
Cc(moveleft(Bc(x))) → moveleft(Bc(Ac(x)))
Ca(moveleft(Bc(x))) → moveleft(Bc(Aa(x)))
Cs(moveleft(Bc(x))) → moveleft(Bc(As(x)))
Cf(moveleft(Ba(x))) → moveleft(Ba(Af(x)))
Cn(moveleft(Ba(x))) → moveleft(Ba(An(x)))
Cc(moveleft(Ba(x))) → moveleft(Ba(Ac(x)))
Ca(moveleft(Ba(x))) → moveleft(Ba(Aa(x)))
Cs(moveleft(Ba(x))) → moveleft(Ba(As(x)))
Cf(moveleft(Bs(x))) → moveleft(Bs(Af(x)))
Cn(moveleft(Bs(x))) → moveleft(Bs(An(x)))
Cc(moveleft(Bs(x))) → moveleft(Bs(Ac(x)))
Ca(moveleft(Bs(x))) → moveleft(Bs(Aa(x)))
Cs(moveleft(Bs(x))) → moveleft(Bs(As(x)))
cut(moveleft(Bf(x))) → Df(cut(goright(x)))
cut(moveleft(Bn(x))) → Dn(cut(goright(x)))
cut(moveleft(Bc(x))) → Dc(cut(goright(x)))
cut(moveleft(Ba(x))) → Da(cut(goright(x)))
cut(moveleft(Bs(x))) → Ds(cut(goright(x)))
goright(Af(x)) → Cf(goright(x))
goright(An(x)) → Cn(goright(x))
goright(Ac(x)) → Cc(goright(x))
goright(Aa(x)) → Ca(goright(x))
goright(As(x)) → Cs(goright(x))
goright(wait(f(x))) → moveleft(Bf(wait(x)))
goright(wait(n(x))) → moveleft(Bn(wait(x)))
goright(wait(c(x))) → moveleft(Bc(wait(x)))
goright(wait(a(x))) → moveleft(Ba(wait(x)))
goright(wait(s(x))) → moveleft(Bs(wait(x)))
goright(wait(end(x))) → finish(end(x))
Cf(finish(x)) → finish(f(x))
Cn(finish(x)) → finish(n(x))
Cc(finish(x)) → finish(c(x))
Ca(finish(x)) → finish(a(x))
Cs(finish(x)) → finish(s(x))
cut(finish(x)) → finish2(x)
Df(finish2(x)) → finish2(f(x))
Dn(finish2(x)) → finish2(n(x))
Dc(finish2(x)) → finish2(c(x))
Da(finish2(x)) → finish2(a(x))
Ds(finish2(x)) → finish2(s(x))
rotate(finish2(x)) → rewrite(x)
rewrite(f(x)) → begin(n(c(n(a(x)))))
rewrite(c(f(x))) → begin(f(n(a(c(x)))))
rewrite(n(a(x))) → begin(c(x))
rewrite(c(c(x))) → begin(c(x))
rewrite(n(s(x))) → begin(f(s(s(x))))
rewrite(n(f(x))) → begin(f(n(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:
rewrite n f end → rewrite n f end

rewrite n f end → rewrite n f end
by OverlapClosure OC 3
rewrite n f end → rotate finish2 n f end
by OverlapClosure OC 3
rewrite n f end → rotate Dn finish2 f end
by OverlapClosure OC 3
rewrite n f end → rotate Dn cut finish f end
by OverlapClosure OC 3
rewrite n f end → rotate Dn cut Cf finish end
by OverlapClosure OC 2
rewrite n f → rotate Dn cut Cf goright wait
by OverlapClosure OC 3
rewrite n f → rotate Dn cut goright Af wait
by OverlapClosure OC 3
rewrite n f → rotate cut moveleft Bn Af wait
by OverlapClosure OC 3
rewrite n f → rotate cut Cf moveleft Bn wait
by OverlapClosure OC 2
rewrite n f → rotate cut Cf guess n
by OverlapClosure OC 3
rewrite n f → begin f n
by original rule (OC 1)
begin f → rotate cut Cf guess
by original rule (OC 1)
guess n → moveleft Bn wait
by original rule (OC 1)
Cf moveleft Bn → moveleft Bn Af
by original rule (OC 1)
cut moveleft Bn → Dn cut goright
by original rule (OC 1)
goright Af → Cf goright
by original rule (OC 1)
goright wait end → finish end
by original rule (OC 1)
Cf finish → finish f
by original rule (OC 1)
cut finish → finish2
by original rule (OC 1)
Dn finish2 → finish2 n
by original rule (OC 1)
rotate finish2 → rewrite
by original rule (OC 1)

(2) NO