Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema

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

0 QTRS

↳1 QTRS Reverse (⇔, 0 ms)

↳2 QTRS

↳3 QTRSRRRProof (⇔, 105 ms)

↳4 QTRS

↳5 Overlay + Local Confluence (⇔, 108 ms)

↳6 QTRS

↳7 DependencyPairsProof (⇔, 64 ms)

↳8 QDP

↳9 DependencyGraphProof (⇔, 0 ms)

↳10 AND

    ↳11 QDP

        ↳12 UsableRulesProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QReductionProof (⇔, 0 ms)

        ↳15 QDP

        ↳16 MRRProof (⇔, 6 ms)

        ↳17 QDP

        ↳18 MRRProof (⇔, 0 ms)

        ↳19 QDP

        ↳20 QDPOrderProof (⇔, 2 ms)

        ↳21 QDP

        ↳22 PisEmptyProof (⇔, 0 ms)

        ↳23 YES

    ↳24 QDP

        ↳25 UsableRulesProof (⇔, 0 ms)

        ↳26 QDP

        ↳27 QReductionProof (⇔, 0 ms)

        ↳28 QDP

        ↳29 MRRProof (⇔, 37 ms)

        ↳30 QDP

        ↳31 QDPOrderProof (⇔, 9 ms)

        ↳32 QDP

        ↳33 PisEmptyProof (⇔, 0 ms)

        ↳34 YES

    ↳35 QDP

        ↳36 UsableRulesProof (⇔, 0 ms)

        ↳37 QDP

        ↳38 QReductionProof (⇔, 0 ms)

        ↳39 QDP

        ↳40 MRRProof (⇔, 6 ms)

        ↳41 QDP

        ↳42 QDPOrderProof (⇔, 0 ms)

        ↳43 QDP

        ↳44 PisEmptyProof (⇔, 0 ms)

        ↳45 YES

    ↳46 QDP

        ↳47 UsableRulesProof (⇔, 0 ms)

        ↳48 QDP

        ↳49 QReductionProof (⇔, 0 ms)

        ↳50 QDP

        ↳51 MRRProof (⇔, 6 ms)

        ↳52 QDP

        ↳53 MRRProof (⇔, 0 ms)

        ↳54 QDP

        ↳55 QDPOrderProof (⇔, 7 ms)

        ↳56 QDP

        ↳57 PisEmptyProof (⇔, 0 ms)

        ↳58 YES

    ↳59 QDP

        ↳60 UsableRulesProof (⇔, 0 ms)

        ↳61 QDP

        ↳62 QReductionProof (⇔, 0 ms)

        ↳63 QDP

        ↳64 MRRProof (⇔, 10 ms)

        ↳65 QDP

        ↳66 MRRProof (⇔, 0 ms)

        ↳67 QDP

        ↳68 QDPOrderProof (⇔, 7 ms)

        ↳69 QDP

        ↳70 PisEmptyProof (⇔, 0 ms)

        ↳71 YES

    ↳72 QDP

        ↳73 UsableRulesProof (⇔, 0 ms)

        ↳74 QDP

        ↳75 QReductionProof (⇔, 0 ms)

        ↳76 QDP

        ↳77 MRRProof (⇔, 7 ms)

        ↳78 QDP

        ↳79 MRRProof (⇔, 0 ms)

        ↳80 QDP

        ↳81 MRRProof (⇔, 4 ms)

        ↳82 QDP

        ↳83 MRRProof (⇔, 3 ms)

        ↳84 QDP

        ↳85 QDPOrderProof (⇔, 0 ms)

        ↳86 QDP

        ↳87 MRRProof (⇔, 2 ms)

        ↳88 QDP

        ↳89 PisEmptyProof (⇔, 0 ms)

        ↳90 YES

    ↳91 QDP

        ↳92 UsableRulesProof (⇔, 0 ms)

        ↳93 QDP

        ↳94 QReductionProof (⇔, 0 ms)

        ↳95 QDP

        ↳96 QDPSizeChangeProof (⇔, 1 ms)

        ↳97 YES

    ↳98 QDP

        ↳99 UsableRulesProof (⇔, 0 ms)

        ↳100 QDP

        ↳101 QReductionProof (⇔, 0 ms)

        ↳102 QDP

        ↳103 QDPSizeChangeProof (⇔, 0 ms)

        ↳104 YES

(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(b(x)) → rotate(cut(Cb(guess(x))))
begin(c(x)) → rotate(cut(Cc(guess(x))))
begin(d(x)) → rotate(cut(Cd(guess(x))))
begin(f(x)) → rotate(cut(Cf(guess(x))))
begin(g(x)) → rotate(cut(Cg(guess(x))))
guess(a(x)) → Ca(guess(x))
guess(b(x)) → Cb(guess(x))
guess(c(x)) → Cc(guess(x))
guess(d(x)) → Cd(guess(x))
guess(f(x)) → Cf(guess(x))
guess(g(x)) → Cg(guess(x))
guess(a(x)) → moveleft(Ba(wait(x)))
guess(b(x)) → moveleft(Bb(wait(x)))
guess(c(x)) → moveleft(Bc(wait(x)))
guess(d(x)) → moveleft(Bd(wait(x)))
guess(f(x)) → moveleft(Bf(wait(x)))
guess(g(x)) → moveleft(Bg(wait(x)))
guess(end(x)) → finish(end(x))
Ca(moveleft(Ba(x))) → moveleft(Ba(Aa(x)))
Cb(moveleft(Ba(x))) → moveleft(Ba(Ab(x)))
Cc(moveleft(Ba(x))) → moveleft(Ba(Ac(x)))
Cd(moveleft(Ba(x))) → moveleft(Ba(Ad(x)))
Cf(moveleft(Ba(x))) → moveleft(Ba(Af(x)))
Cg(moveleft(Ba(x))) → moveleft(Ba(Ag(x)))
Ca(moveleft(Bb(x))) → moveleft(Bb(Aa(x)))
Cb(moveleft(Bb(x))) → moveleft(Bb(Ab(x)))
Cc(moveleft(Bb(x))) → moveleft(Bb(Ac(x)))
Cd(moveleft(Bb(x))) → moveleft(Bb(Ad(x)))
Cf(moveleft(Bb(x))) → moveleft(Bb(Af(x)))
Cg(moveleft(Bb(x))) → moveleft(Bb(Ag(x)))
Ca(moveleft(Bc(x))) → moveleft(Bc(Aa(x)))
Cb(moveleft(Bc(x))) → moveleft(Bc(Ab(x)))
Cc(moveleft(Bc(x))) → moveleft(Bc(Ac(x)))
Cd(moveleft(Bc(x))) → moveleft(Bc(Ad(x)))
Cf(moveleft(Bc(x))) → moveleft(Bc(Af(x)))
Cg(moveleft(Bc(x))) → moveleft(Bc(Ag(x)))
Ca(moveleft(Bd(x))) → moveleft(Bd(Aa(x)))
Cb(moveleft(Bd(x))) → moveleft(Bd(Ab(x)))
Cc(moveleft(Bd(x))) → moveleft(Bd(Ac(x)))
Cd(moveleft(Bd(x))) → moveleft(Bd(Ad(x)))
Cf(moveleft(Bd(x))) → moveleft(Bd(Af(x)))
Cg(moveleft(Bd(x))) → moveleft(Bd(Ag(x)))
Ca(moveleft(Bf(x))) → moveleft(Bf(Aa(x)))
Cb(moveleft(Bf(x))) → moveleft(Bf(Ab(x)))
Cc(moveleft(Bf(x))) → moveleft(Bf(Ac(x)))
Cd(moveleft(Bf(x))) → moveleft(Bf(Ad(x)))
Cf(moveleft(Bf(x))) → moveleft(Bf(Af(x)))
Cg(moveleft(Bf(x))) → moveleft(Bf(Ag(x)))
Ca(moveleft(Bg(x))) → moveleft(Bg(Aa(x)))
Cb(moveleft(Bg(x))) → moveleft(Bg(Ab(x)))
Cc(moveleft(Bg(x))) → moveleft(Bg(Ac(x)))
Cd(moveleft(Bg(x))) → moveleft(Bg(Ad(x)))
Cf(moveleft(Bg(x))) → moveleft(Bg(Af(x)))
Cg(moveleft(Bg(x))) → moveleft(Bg(Ag(x)))
cut(moveleft(Ba(x))) → Da(cut(goright(x)))
cut(moveleft(Bb(x))) → Db(cut(goright(x)))
cut(moveleft(Bc(x))) → Dc(cut(goright(x)))
cut(moveleft(Bd(x))) → Dd(cut(goright(x)))
cut(moveleft(Bf(x))) → Df(cut(goright(x)))
cut(moveleft(Bg(x))) → Dg(cut(goright(x)))
goright(Aa(x)) → Ca(goright(x))
goright(Ab(x)) → Cb(goright(x))
goright(Ac(x)) → Cc(goright(x))
goright(Ad(x)) → Cd(goright(x))
goright(Af(x)) → Cf(goright(x))
goright(Ag(x)) → Cg(goright(x))
goright(wait(a(x))) → moveleft(Ba(wait(x)))
goright(wait(b(x))) → moveleft(Bb(wait(x)))
goright(wait(c(x))) → moveleft(Bc(wait(x)))
goright(wait(d(x))) → moveleft(Bd(wait(x)))
goright(wait(f(x))) → moveleft(Bf(wait(x)))
goright(wait(g(x))) → moveleft(Bg(wait(x)))
goright(wait(end(x))) → finish(end(x))
Ca(finish(x)) → finish(a(x))
Cb(finish(x)) → finish(b(x))
Cc(finish(x)) → finish(c(x))
Cd(finish(x)) → finish(d(x))
Cf(finish(x)) → finish(f(x))
Cg(finish(x)) → finish(g(x))
cut(finish(x)) → finish2(x)
Da(finish2(x)) → finish2(a(x))
Db(finish2(x)) → finish2(b(x))
Dc(finish2(x)) → finish2(c(x))
Dd(finish2(x)) → finish2(d(x))
Df(finish2(x)) → finish2(f(x))
Dg(finish2(x)) → finish2(g(x))
rotate(finish2(x)) → rewrite(x)
rewrite(a(a(x))) → begin(b(c(x)))
rewrite(b(b(x))) → begin(c(d(x)))
rewrite(b(x)) → begin(a(x))
rewrite(c(c(x))) → begin(d(f(x)))
rewrite(d(d(x))) → begin(f(f(f(x))))
rewrite(d(x)) → begin(b(x))
rewrite(f(f(x))) → begin(g(a(x)))
rewrite(g(g(x))) → begin(a(x))

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

end(begin(x)) → end(rewrite(x))
a(begin(x)) → guess(Ca(cut(rotate(x))))
b(begin(x)) → guess(Cb(cut(rotate(x))))
c(begin(x)) → guess(Cc(cut(rotate(x))))
d(begin(x)) → guess(Cd(cut(rotate(x))))
f(begin(x)) → guess(Cf(cut(rotate(x))))
g(begin(x)) → guess(Cg(cut(rotate(x))))
a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
a(guess(x)) → wait(Ba(moveleft(x)))
b(guess(x)) → wait(Bb(moveleft(x)))
c(guess(x)) → wait(Bc(moveleft(x)))
d(guess(x)) → wait(Bd(moveleft(x)))
f(guess(x)) → wait(Bf(moveleft(x)))
g(guess(x)) → wait(Bg(moveleft(x)))
end(guess(x)) → end(finish(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
end(wait(goright(x))) → end(finish(x))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish(cut(x)) → finish2(x)
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))
finish2(rotate(x)) → rewrite(x)
a(a(rewrite(x))) → c(b(begin(x)))
b(b(rewrite(x))) → d(c(begin(x)))
b(rewrite(x)) → a(begin(x))
c(c(rewrite(x))) → f(d(begin(x)))
d(d(rewrite(x))) → f(f(f(begin(x))))
d(rewrite(x)) → b(begin(x))
f(f(rewrite(x))) → a(g(begin(x)))
g(g(rewrite(x))) → a(begin(x))

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(Aa(x₁)) = 930 + x₁
POL(Ab(x₁)) = 972 + x₁
POL(Ac(x₁)) = 882 + x₁
POL(Ad(x₁)) = 1056 + x₁
POL(Af(x₁)) = 702 + x₁
POL(Ag(x₁)) = 468 + x₁
POL(Ba(x₁)) = 930 + x₁
POL(Bb(x₁)) = 972 + x₁
POL(Bc(x₁)) = 882 + x₁
POL(Bd(x₁)) = 1056 + x₁
POL(Bf(x₁)) = 702 + x₁
POL(Bg(x₁)) = 468 + x₁
POL(Ca(x₁)) = 930 + x₁
POL(Cb(x₁)) = 972 + x₁
POL(Cc(x₁)) = 882 + x₁
POL(Cd(x₁)) = 1056 + x₁
POL(Cf(x₁)) = 702 + x₁
POL(Cg(x₁)) = 468 + x₁
POL(Da(x₁)) = 930 + x₁
POL(Db(x₁)) = 972 + x₁
POL(Dc(x₁)) = 882 + x₁
POL(Dd(x₁)) = 1056 + x₁
POL(Df(x₁)) = 702 + x₁
POL(Dg(x₁)) = 468 + x₁
POL(a(x₁)) = 930 + x₁
POL(b(x₁)) = 972 + x₁
POL(begin(x₁)) = 5 + x₁
POL(c(x₁)) = 882 + x₁
POL(cut(x₁)) = 2 + x₁
POL(d(x₁)) = 1056 + x₁
POL(end(x₁)) = x₁
POL(f(x₁)) = 702 + x₁
POL(finish(x₁)) = x₁
POL(finish2(x₁)) = 1 + x₁
POL(g(x₁)) = 468 + x₁
POL(goright(x₁)) = x₁
POL(guess(x₁)) = 2 + x₁
POL(moveleft(x₁)) = x₁
POL(rewrite(x₁)) = x₁
POL(rotate(x₁)) = x₁
POL(wait(x₁)) = 1 + x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

end(begin(x)) → end(rewrite(x))
a(begin(x)) → guess(Ca(cut(rotate(x))))
b(begin(x)) → guess(Cb(cut(rotate(x))))
c(begin(x)) → guess(Cc(cut(rotate(x))))
d(begin(x)) → guess(Cd(cut(rotate(x))))
f(begin(x)) → guess(Cf(cut(rotate(x))))
g(begin(x)) → guess(Cg(cut(rotate(x))))
a(guess(x)) → wait(Ba(moveleft(x)))
b(guess(x)) → wait(Bb(moveleft(x)))
c(guess(x)) → wait(Bc(moveleft(x)))
d(guess(x)) → wait(Bd(moveleft(x)))
f(guess(x)) → wait(Bf(moveleft(x)))
g(guess(x)) → wait(Bg(moveleft(x)))
end(guess(x)) → end(finish(x))
end(wait(goright(x))) → end(finish(x))
finish(cut(x)) → finish2(x)
finish2(rotate(x)) → rewrite(x)
a(a(rewrite(x))) → c(b(begin(x)))
b(b(rewrite(x))) → d(c(begin(x)))
b(rewrite(x)) → a(begin(x))
c(c(rewrite(x))) → f(d(begin(x)))
d(d(rewrite(x))) → f(f(f(begin(x))))
d(rewrite(x)) → b(begin(x))
f(f(rewrite(x))) → a(g(begin(x)))
g(g(rewrite(x))) → a(begin(x))

(4) Obligation:

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

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

Q is empty.

(5) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(6) Obligation:

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

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(7) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Ca(x))) → AA(Ba(moveleft(x)))
BA(moveleft(Ca(x))) → BA(moveleft(x))
BA(moveleft(Cb(x))) → AB(Ba(moveleft(x)))
BA(moveleft(Cb(x))) → BA(moveleft(x))
BA(moveleft(Cc(x))) → AC(Ba(moveleft(x)))
BA(moveleft(Cc(x))) → BA(moveleft(x))
BA(moveleft(Cd(x))) → AD(Ba(moveleft(x)))
BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → AF(Ba(moveleft(x)))
BA(moveleft(Cf(x))) → BA(moveleft(x))
BA(moveleft(Cg(x))) → AG(Ba(moveleft(x)))
BA(moveleft(Cg(x))) → BA(moveleft(x))
BB(moveleft(Ca(x))) → AA(Bb(moveleft(x)))
BB(moveleft(Ca(x))) → BB(moveleft(x))
BB(moveleft(Cb(x))) → AB(Bb(moveleft(x)))
BB(moveleft(Cb(x))) → BB(moveleft(x))
BB(moveleft(Cc(x))) → AC(Bb(moveleft(x)))
BB(moveleft(Cc(x))) → BB(moveleft(x))
BB(moveleft(Cd(x))) → AD(Bb(moveleft(x)))
BB(moveleft(Cd(x))) → BB(moveleft(x))
BB(moveleft(Cf(x))) → AF(Bb(moveleft(x)))
BB(moveleft(Cf(x))) → BB(moveleft(x))
BB(moveleft(Cg(x))) → AG(Bb(moveleft(x)))
BB(moveleft(Cg(x))) → BB(moveleft(x))
BC(moveleft(Ca(x))) → AA(Bc(moveleft(x)))
BC(moveleft(Ca(x))) → BC(moveleft(x))
BC(moveleft(Cb(x))) → AB(Bc(moveleft(x)))
BC(moveleft(Cb(x))) → BC(moveleft(x))
BC(moveleft(Cc(x))) → AC(Bc(moveleft(x)))
BC(moveleft(Cc(x))) → BC(moveleft(x))
BC(moveleft(Cd(x))) → AD(Bc(moveleft(x)))
BC(moveleft(Cd(x))) → BC(moveleft(x))
BC(moveleft(Cf(x))) → AF(Bc(moveleft(x)))
BC(moveleft(Cf(x))) → BC(moveleft(x))
BC(moveleft(Cg(x))) → AG(Bc(moveleft(x)))
BC(moveleft(Cg(x))) → BC(moveleft(x))
BD(moveleft(Ca(x))) → AA(Bd(moveleft(x)))
BD(moveleft(Ca(x))) → BD(moveleft(x))
BD(moveleft(Cb(x))) → AB(Bd(moveleft(x)))
BD(moveleft(Cb(x))) → BD(moveleft(x))
BD(moveleft(Cc(x))) → AC(Bd(moveleft(x)))
BD(moveleft(Cc(x))) → BD(moveleft(x))
BD(moveleft(Cd(x))) → AD(Bd(moveleft(x)))
BD(moveleft(Cd(x))) → BD(moveleft(x))
BD(moveleft(Cf(x))) → AF(Bd(moveleft(x)))
BD(moveleft(Cf(x))) → BD(moveleft(x))
BD(moveleft(Cg(x))) → AG(Bd(moveleft(x)))
BD(moveleft(Cg(x))) → BD(moveleft(x))
BF(moveleft(Ca(x))) → AA(Bf(moveleft(x)))
BF(moveleft(Ca(x))) → BF(moveleft(x))
BF(moveleft(Cb(x))) → AB(Bf(moveleft(x)))
BF(moveleft(Cb(x))) → BF(moveleft(x))
BF(moveleft(Cc(x))) → AC(Bf(moveleft(x)))
BF(moveleft(Cc(x))) → BF(moveleft(x))
BF(moveleft(Cd(x))) → AD(Bf(moveleft(x)))
BF(moveleft(Cd(x))) → BF(moveleft(x))
BF(moveleft(Cf(x))) → AF(Bf(moveleft(x)))
BF(moveleft(Cf(x))) → BF(moveleft(x))
BF(moveleft(Cg(x))) → AG(Bf(moveleft(x)))
BF(moveleft(Cg(x))) → BF(moveleft(x))
BG(moveleft(Ca(x))) → AA(Bg(moveleft(x)))
BG(moveleft(Ca(x))) → BG(moveleft(x))
BG(moveleft(Cb(x))) → AB(Bg(moveleft(x)))
BG(moveleft(Cb(x))) → BG(moveleft(x))
BG(moveleft(Cc(x))) → AC(Bg(moveleft(x)))
BG(moveleft(Cc(x))) → BG(moveleft(x))
BG(moveleft(Cd(x))) → AD(Bg(moveleft(x)))
BG(moveleft(Cd(x))) → BG(moveleft(x))
BG(moveleft(Cf(x))) → AF(Bg(moveleft(x)))
BG(moveleft(Cf(x))) → BG(moveleft(x))
BG(moveleft(Cg(x))) → AG(Bg(moveleft(x)))
BG(moveleft(Cg(x))) → BG(moveleft(x))
A(wait(goright(x))) → BA(moveleft(x))
B(wait(goright(x))) → BB(moveleft(x))
C(wait(goright(x))) → BC(moveleft(x))
D(wait(goright(x))) → BD(moveleft(x))
F(wait(goright(x))) → BF(moveleft(x))
G(wait(goright(x))) → BG(moveleft(x))
FINISH(Ca(x)) → A(finish(x))
FINISH(Ca(x)) → FINISH(x)
FINISH(Cb(x)) → B(finish(x))
FINISH(Cb(x)) → FINISH(x)
FINISH(Cc(x)) → C(finish(x))
FINISH(Cc(x)) → FINISH(x)
FINISH(Cd(x)) → D(finish(x))
FINISH(Cd(x)) → FINISH(x)
FINISH(Cf(x)) → F(finish(x))
FINISH(Cf(x)) → FINISH(x)
FINISH(Cg(x)) → G(finish(x))
FINISH(Cg(x)) → FINISH(x)
FINISH2(Da(x)) → A(finish2(x))
FINISH2(Da(x)) → FINISH2(x)
FINISH2(Db(x)) → B(finish2(x))
FINISH2(Db(x)) → FINISH2(x)
FINISH2(Dc(x)) → C(finish2(x))
FINISH2(Dc(x)) → FINISH2(x)
FINISH2(Dd(x)) → D(finish2(x))
FINISH2(Dd(x)) → FINISH2(x)
FINISH2(Df(x)) → F(finish2(x))
FINISH2(Df(x)) → FINISH2(x)
FINISH2(Dg(x)) → G(finish2(x))
FINISH2(Dg(x)) → FINISH2(x)

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(9) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 8 SCCs with 54 less nodes.

(10) Complex Obligation (AND)

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BG(moveleft(Cb(x))) → BG(moveleft(x))
BG(moveleft(Ca(x))) → BG(moveleft(x))
BG(moveleft(Cc(x))) → BG(moveleft(x))
BG(moveleft(Cd(x))) → BG(moveleft(x))
BG(moveleft(Cf(x))) → BG(moveleft(x))
BG(moveleft(Cg(x))) → BG(moveleft(x))

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(12) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BG(moveleft(Cb(x))) → BG(moveleft(x))
BG(moveleft(Ca(x))) → BG(moveleft(x))
BG(moveleft(Cc(x))) → BG(moveleft(x))
BG(moveleft(Cd(x))) → BG(moveleft(x))
BG(moveleft(Cf(x))) → BG(moveleft(x))
BG(moveleft(Cg(x))) → BG(moveleft(x))

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(14) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BG(moveleft(Cb(x))) → BG(moveleft(x))
BG(moveleft(Ca(x))) → BG(moveleft(x))
BG(moveleft(Cc(x))) → BG(moveleft(x))
BG(moveleft(Cd(x))) → BG(moveleft(x))
BG(moveleft(Cf(x))) → BG(moveleft(x))
BG(moveleft(Cg(x))) → BG(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

BG(moveleft(Cb(x))) → BG(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BG(x₁)) = 2·x₁
POL(Ca(x₁)) = 2·x₁
POL(Cb(x₁)) = 1 + x₁
POL(Cc(x₁)) = x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = x₁
POL(moveleft(x₁)) = x₁

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BG(moveleft(Ca(x))) → BG(moveleft(x))
BG(moveleft(Cc(x))) → BG(moveleft(x))
BG(moveleft(Cd(x))) → BG(moveleft(x))
BG(moveleft(Cf(x))) → BG(moveleft(x))
BG(moveleft(Cg(x))) → BG(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) MRRProof (EQUIVALENT transformation)

BG(moveleft(Cg(x))) → BG(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BG(x₁)) = 2·x₁
POL(Ca(x₁)) = x₁
POL(Cc(x₁)) = 2·x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = 1 + 2·x₁
POL(moveleft(x₁)) = x₁

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BG(moveleft(Ca(x))) → BG(moveleft(x))
BG(moveleft(Cc(x))) → BG(moveleft(x))
BG(moveleft(Cd(x))) → BG(moveleft(x))
BG(moveleft(Cf(x))) → BG(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

BG(moveleft(Ca(x))) → BG(moveleft(x))
BG(moveleft(Cc(x))) → BG(moveleft(x))
BG(moveleft(Cd(x))) → BG(moveleft(x))
BG(moveleft(Cf(x))) → BG(moveleft(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(BG(x₁)) = x₁
POL(Ca(x₁)) = 1 + x₁
POL(Cc(x₁)) = 1 + x₁
POL(Cd(x₁)) = 1 + x₁
POL(Cf(x₁)) = 1 + x₁
POL(moveleft(x₁)) = x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(21) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(22) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(23) YES

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BF(moveleft(Cb(x))) → BF(moveleft(x))
BF(moveleft(Ca(x))) → BF(moveleft(x))
BF(moveleft(Cc(x))) → BF(moveleft(x))
BF(moveleft(Cd(x))) → BF(moveleft(x))
BF(moveleft(Cf(x))) → BF(moveleft(x))
BF(moveleft(Cg(x))) → BF(moveleft(x))

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(25) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BF(moveleft(Cb(x))) → BF(moveleft(x))
BF(moveleft(Ca(x))) → BF(moveleft(x))
BF(moveleft(Cc(x))) → BF(moveleft(x))
BF(moveleft(Cd(x))) → BF(moveleft(x))
BF(moveleft(Cf(x))) → BF(moveleft(x))
BF(moveleft(Cg(x))) → BF(moveleft(x))

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(27) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BF(moveleft(Cb(x))) → BF(moveleft(x))
BF(moveleft(Ca(x))) → BF(moveleft(x))
BF(moveleft(Cc(x))) → BF(moveleft(x))
BF(moveleft(Cd(x))) → BF(moveleft(x))
BF(moveleft(Cf(x))) → BF(moveleft(x))
BF(moveleft(Cg(x))) → BF(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) MRRProof (EQUIVALENT transformation)

BF(moveleft(Cb(x))) → BF(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BF(x₁)) = 2·x₁
POL(Ca(x₁)) = 2·x₁
POL(Cb(x₁)) = 1 + x₁
POL(Cc(x₁)) = x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = x₁
POL(moveleft(x₁)) = x₁

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BF(moveleft(Ca(x))) → BF(moveleft(x))
BF(moveleft(Cc(x))) → BF(moveleft(x))
BF(moveleft(Cd(x))) → BF(moveleft(x))
BF(moveleft(Cf(x))) → BF(moveleft(x))
BF(moveleft(Cg(x))) → BF(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(31) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

BF(moveleft(Ca(x))) → BF(moveleft(x))
BF(moveleft(Cc(x))) → BF(moveleft(x))
BF(moveleft(Cd(x))) → BF(moveleft(x))
BF(moveleft(Cf(x))) → BF(moveleft(x))
BF(moveleft(Cg(x))) → BF(moveleft(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( BF(x₁) ) = max{0, 2x₁ - 1}

POL( moveleft(x₁) ) = 2x₁

POL( Ca(x₁) ) = 2x₁ + 2

POL( Cc(x₁) ) = x₁ + 1

POL( Cd(x₁) ) = 2x₁ + 2

POL( Cf(x₁) ) = 2x₁ + 2

POL( Cg(x₁) ) = 2x₁ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(32) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(33) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(34) YES

(35) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BD(moveleft(Cb(x))) → BD(moveleft(x))
BD(moveleft(Ca(x))) → BD(moveleft(x))
BD(moveleft(Cc(x))) → BD(moveleft(x))
BD(moveleft(Cd(x))) → BD(moveleft(x))
BD(moveleft(Cf(x))) → BD(moveleft(x))
BD(moveleft(Cg(x))) → BD(moveleft(x))

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(36) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(37) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BD(moveleft(Cb(x))) → BD(moveleft(x))
BD(moveleft(Ca(x))) → BD(moveleft(x))
BD(moveleft(Cc(x))) → BD(moveleft(x))
BD(moveleft(Cd(x))) → BD(moveleft(x))
BD(moveleft(Cf(x))) → BD(moveleft(x))
BD(moveleft(Cg(x))) → BD(moveleft(x))

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(38) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BD(moveleft(Cb(x))) → BD(moveleft(x))
BD(moveleft(Ca(x))) → BD(moveleft(x))
BD(moveleft(Cc(x))) → BD(moveleft(x))
BD(moveleft(Cd(x))) → BD(moveleft(x))
BD(moveleft(Cf(x))) → BD(moveleft(x))
BD(moveleft(Cg(x))) → BD(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(40) MRRProof (EQUIVALENT transformation)

BD(moveleft(Cb(x))) → BD(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BD(x₁)) = 2·x₁
POL(Ca(x₁)) = 2·x₁
POL(Cb(x₁)) = 1 + x₁
POL(Cc(x₁)) = x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = x₁
POL(moveleft(x₁)) = x₁

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BD(moveleft(Ca(x))) → BD(moveleft(x))
BD(moveleft(Cc(x))) → BD(moveleft(x))
BD(moveleft(Cd(x))) → BD(moveleft(x))
BD(moveleft(Cf(x))) → BD(moveleft(x))
BD(moveleft(Cg(x))) → BD(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

BD(moveleft(Ca(x))) → BD(moveleft(x))
BD(moveleft(Cc(x))) → BD(moveleft(x))
BD(moveleft(Cd(x))) → BD(moveleft(x))
BD(moveleft(Cf(x))) → BD(moveleft(x))
BD(moveleft(Cg(x))) → BD(moveleft(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( BD(x₁) ) = max{0, 2x₁ - 1}

POL( moveleft(x₁) ) = 2x₁

POL( Ca(x₁) ) = 2x₁ + 2

POL( Cc(x₁) ) = x₁ + 1

POL( Cd(x₁) ) = 2x₁ + 2

POL( Cf(x₁) ) = 2x₁ + 2

POL( Cg(x₁) ) = 2x₁ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(43) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(44) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(45) YES

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BC(moveleft(Cb(x))) → BC(moveleft(x))
BC(moveleft(Ca(x))) → BC(moveleft(x))
BC(moveleft(Cc(x))) → BC(moveleft(x))
BC(moveleft(Cd(x))) → BC(moveleft(x))
BC(moveleft(Cf(x))) → BC(moveleft(x))
BC(moveleft(Cg(x))) → BC(moveleft(x))

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(47) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BC(moveleft(Cb(x))) → BC(moveleft(x))
BC(moveleft(Ca(x))) → BC(moveleft(x))
BC(moveleft(Cc(x))) → BC(moveleft(x))
BC(moveleft(Cd(x))) → BC(moveleft(x))
BC(moveleft(Cf(x))) → BC(moveleft(x))
BC(moveleft(Cg(x))) → BC(moveleft(x))

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(49) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BC(moveleft(Cb(x))) → BC(moveleft(x))
BC(moveleft(Ca(x))) → BC(moveleft(x))
BC(moveleft(Cc(x))) → BC(moveleft(x))
BC(moveleft(Cd(x))) → BC(moveleft(x))
BC(moveleft(Cf(x))) → BC(moveleft(x))
BC(moveleft(Cg(x))) → BC(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(51) MRRProof (EQUIVALENT transformation)

BC(moveleft(Cb(x))) → BC(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BC(x₁)) = 2·x₁
POL(Ca(x₁)) = 2·x₁
POL(Cb(x₁)) = 1 + x₁
POL(Cc(x₁)) = x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = x₁
POL(moveleft(x₁)) = x₁

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BC(moveleft(Ca(x))) → BC(moveleft(x))
BC(moveleft(Cc(x))) → BC(moveleft(x))
BC(moveleft(Cd(x))) → BC(moveleft(x))
BC(moveleft(Cf(x))) → BC(moveleft(x))
BC(moveleft(Cg(x))) → BC(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(53) MRRProof (EQUIVALENT transformation)

BC(moveleft(Cg(x))) → BC(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BC(x₁)) = 2·x₁
POL(Ca(x₁)) = x₁
POL(Cc(x₁)) = 2·x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = 1 + 2·x₁
POL(moveleft(x₁)) = x₁

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BC(moveleft(Ca(x))) → BC(moveleft(x))
BC(moveleft(Cc(x))) → BC(moveleft(x))
BC(moveleft(Cd(x))) → BC(moveleft(x))
BC(moveleft(Cf(x))) → BC(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(55) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

BC(moveleft(Ca(x))) → BC(moveleft(x))
BC(moveleft(Cc(x))) → BC(moveleft(x))
BC(moveleft(Cd(x))) → BC(moveleft(x))
BC(moveleft(Cf(x))) → BC(moveleft(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( BC(x₁) ) = max{0, 2x₁ - 1}

POL( moveleft(x₁) ) = 2x₁

POL( Ca(x₁) ) = 2x₁ + 2

POL( Cc(x₁) ) = 2x₁ + 1

POL( Cd(x₁) ) = 2x₁ + 2

POL( Cf(x₁) ) = 2x₁ + 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(56) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(57) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(58) YES

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BB(moveleft(Cb(x))) → BB(moveleft(x))
BB(moveleft(Ca(x))) → BB(moveleft(x))
BB(moveleft(Cc(x))) → BB(moveleft(x))
BB(moveleft(Cd(x))) → BB(moveleft(x))
BB(moveleft(Cf(x))) → BB(moveleft(x))
BB(moveleft(Cg(x))) → BB(moveleft(x))

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(60) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(61) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BB(moveleft(Cb(x))) → BB(moveleft(x))
BB(moveleft(Ca(x))) → BB(moveleft(x))
BB(moveleft(Cc(x))) → BB(moveleft(x))
BB(moveleft(Cd(x))) → BB(moveleft(x))
BB(moveleft(Cf(x))) → BB(moveleft(x))
BB(moveleft(Cg(x))) → BB(moveleft(x))

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(62) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(63) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BB(moveleft(Cb(x))) → BB(moveleft(x))
BB(moveleft(Ca(x))) → BB(moveleft(x))
BB(moveleft(Cc(x))) → BB(moveleft(x))
BB(moveleft(Cd(x))) → BB(moveleft(x))
BB(moveleft(Cf(x))) → BB(moveleft(x))
BB(moveleft(Cg(x))) → BB(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(64) MRRProof (EQUIVALENT transformation)

BB(moveleft(Cb(x))) → BB(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BB(x₁)) = 2·x₁
POL(Ca(x₁)) = 2·x₁
POL(Cb(x₁)) = 1 + x₁
POL(Cc(x₁)) = x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = x₁
POL(moveleft(x₁)) = x₁

(65) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BB(moveleft(Ca(x))) → BB(moveleft(x))
BB(moveleft(Cc(x))) → BB(moveleft(x))
BB(moveleft(Cd(x))) → BB(moveleft(x))
BB(moveleft(Cf(x))) → BB(moveleft(x))
BB(moveleft(Cg(x))) → BB(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(66) MRRProof (EQUIVALENT transformation)

BB(moveleft(Cg(x))) → BB(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BB(x₁)) = 2·x₁
POL(Ca(x₁)) = x₁
POL(Cc(x₁)) = 2·x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = 1 + 2·x₁
POL(moveleft(x₁)) = x₁

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BB(moveleft(Ca(x))) → BB(moveleft(x))
BB(moveleft(Cc(x))) → BB(moveleft(x))
BB(moveleft(Cd(x))) → BB(moveleft(x))
BB(moveleft(Cf(x))) → BB(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(68) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

BB(moveleft(Ca(x))) → BB(moveleft(x))
BB(moveleft(Cc(x))) → BB(moveleft(x))
BB(moveleft(Cd(x))) → BB(moveleft(x))
BB(moveleft(Cf(x))) → BB(moveleft(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( BB(x₁) ) = max{0, 2x₁ - 1}

POL( moveleft(x₁) ) = 2x₁

POL( Ca(x₁) ) = 2x₁ + 2

POL( Cc(x₁) ) = 2x₁ + 1

POL( Cd(x₁) ) = 2x₁ + 2

POL( Cf(x₁) ) = 2x₁ + 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(69) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(70) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(71) YES

(72) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Cb(x))) → BA(moveleft(x))
BA(moveleft(Ca(x))) → BA(moveleft(x))
BA(moveleft(Cc(x))) → BA(moveleft(x))
BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → BA(moveleft(x))
BA(moveleft(Cg(x))) → BA(moveleft(x))

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(73) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(74) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Cb(x))) → BA(moveleft(x))
BA(moveleft(Ca(x))) → BA(moveleft(x))
BA(moveleft(Cc(x))) → BA(moveleft(x))
BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → BA(moveleft(x))
BA(moveleft(Cg(x))) → BA(moveleft(x))

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(75) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(76) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Cb(x))) → BA(moveleft(x))
BA(moveleft(Ca(x))) → BA(moveleft(x))
BA(moveleft(Cc(x))) → BA(moveleft(x))
BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → BA(moveleft(x))
BA(moveleft(Cg(x))) → BA(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(77) MRRProof (EQUIVALENT transformation)

BA(moveleft(Cb(x))) → BA(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BA(x₁)) = 2·x₁
POL(Ca(x₁)) = 2·x₁
POL(Cb(x₁)) = 1 + x₁
POL(Cc(x₁)) = x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = x₁
POL(moveleft(x₁)) = x₁

(78) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Ca(x))) → BA(moveleft(x))
BA(moveleft(Cc(x))) → BA(moveleft(x))
BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → BA(moveleft(x))
BA(moveleft(Cg(x))) → BA(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(79) MRRProof (EQUIVALENT transformation)

BA(moveleft(Cg(x))) → BA(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BA(x₁)) = 2·x₁
POL(Ca(x₁)) = x₁
POL(Cc(x₁)) = 2·x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = x₁
POL(Cg(x₁)) = 1 + 2·x₁
POL(moveleft(x₁)) = x₁

(80) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Ca(x))) → BA(moveleft(x))
BA(moveleft(Cc(x))) → BA(moveleft(x))
BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → BA(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(81) MRRProof (EQUIVALENT transformation)

BA(moveleft(Ca(x))) → BA(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BA(x₁)) = 2·x₁
POL(Ca(x₁)) = 1 + x₁
POL(Cc(x₁)) = 2·x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = 2·x₁
POL(moveleft(x₁)) = 2·x₁

(82) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Cc(x))) → BA(moveleft(x))
BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → BA(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(83) MRRProof (EQUIVALENT transformation)

BA(moveleft(Cc(x))) → BA(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BA(x₁)) = 2·x₁
POL(Cc(x₁)) = 1 + x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = 2·x₁
POL(moveleft(x₁)) = x₁

(84) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Cd(x))) → BA(moveleft(x))
BA(moveleft(Cf(x))) → BA(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(85) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

BA(moveleft(Cf(x))) → BA(moveleft(x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(BA(x₁)) = 4·x₁
POL(Cd(x₁)) = 2·x₁
POL(Cf(x₁)) = 5 + 2·x₁
POL(moveleft(x₁)) = 5·x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(86) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BA(moveleft(Cd(x))) → BA(moveleft(x))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(87) MRRProof (EQUIVALENT transformation)

BA(moveleft(Cd(x))) → BA(moveleft(x))

Used ordering: Polynomial interpretation [POLO]:

POL(BA(x₁)) = x₁
POL(Cd(x₁)) = 1 + x₁
POL(moveleft(x₁)) = x₁

(88) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(89) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(90) YES

(91) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FINISH2(Db(x)) → FINISH2(x)
FINISH2(Da(x)) → FINISH2(x)
FINISH2(Dc(x)) → FINISH2(x)
FINISH2(Dd(x)) → FINISH2(x)
FINISH2(Df(x)) → FINISH2(x)
FINISH2(Dg(x)) → FINISH2(x)

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(92) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(93) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FINISH2(Db(x)) → FINISH2(x)
FINISH2(Da(x)) → FINISH2(x)
FINISH2(Dc(x)) → FINISH2(x)
FINISH2(Dd(x)) → FINISH2(x)
FINISH2(Df(x)) → FINISH2(x)
FINISH2(Dg(x)) → FINISH2(x)

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(94) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(95) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FINISH2(Db(x)) → FINISH2(x)
FINISH2(Da(x)) → FINISH2(x)
FINISH2(Dc(x)) → FINISH2(x)
FINISH2(Dd(x)) → FINISH2(x)
FINISH2(Df(x)) → FINISH2(x)
FINISH2(Dg(x)) → FINISH2(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(96) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

FINISH2(Db(x)) → FINISH2(x)
The graph contains the following edges 1 > 1
FINISH2(Da(x)) → FINISH2(x)
The graph contains the following edges 1 > 1
FINISH2(Dc(x)) → FINISH2(x)
The graph contains the following edges 1 > 1
FINISH2(Dd(x)) → FINISH2(x)
The graph contains the following edges 1 > 1
FINISH2(Df(x)) → FINISH2(x)
The graph contains the following edges 1 > 1
FINISH2(Dg(x)) → FINISH2(x)
The graph contains the following edges 1 > 1

(97) YES

(98) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FINISH(Cb(x)) → FINISH(x)
FINISH(Ca(x)) → FINISH(x)
FINISH(Cc(x)) → FINISH(x)
FINISH(Cd(x)) → FINISH(x)
FINISH(Cf(x)) → FINISH(x)
FINISH(Cg(x)) → FINISH(x)

The TRS R consists of the following rules:

a(guess(x)) → guess(Ca(x))
b(guess(x)) → guess(Cb(x))
c(guess(x)) → guess(Cc(x))
d(guess(x)) → guess(Cd(x))
f(guess(x)) → guess(Cf(x))
g(guess(x)) → guess(Cg(x))
Ba(moveleft(Ca(x))) → Aa(Ba(moveleft(x)))
Ba(moveleft(Cb(x))) → Ab(Ba(moveleft(x)))
Ba(moveleft(Cc(x))) → Ac(Ba(moveleft(x)))
Ba(moveleft(Cd(x))) → Ad(Ba(moveleft(x)))
Ba(moveleft(Cf(x))) → Af(Ba(moveleft(x)))
Ba(moveleft(Cg(x))) → Ag(Ba(moveleft(x)))
Bb(moveleft(Ca(x))) → Aa(Bb(moveleft(x)))
Bb(moveleft(Cb(x))) → Ab(Bb(moveleft(x)))
Bb(moveleft(Cc(x))) → Ac(Bb(moveleft(x)))
Bb(moveleft(Cd(x))) → Ad(Bb(moveleft(x)))
Bb(moveleft(Cf(x))) → Af(Bb(moveleft(x)))
Bb(moveleft(Cg(x))) → Ag(Bb(moveleft(x)))
Bc(moveleft(Ca(x))) → Aa(Bc(moveleft(x)))
Bc(moveleft(Cb(x))) → Ab(Bc(moveleft(x)))
Bc(moveleft(Cc(x))) → Ac(Bc(moveleft(x)))
Bc(moveleft(Cd(x))) → Ad(Bc(moveleft(x)))
Bc(moveleft(Cf(x))) → Af(Bc(moveleft(x)))
Bc(moveleft(Cg(x))) → Ag(Bc(moveleft(x)))
Bd(moveleft(Ca(x))) → Aa(Bd(moveleft(x)))
Bd(moveleft(Cb(x))) → Ab(Bd(moveleft(x)))
Bd(moveleft(Cc(x))) → Ac(Bd(moveleft(x)))
Bd(moveleft(Cd(x))) → Ad(Bd(moveleft(x)))
Bd(moveleft(Cf(x))) → Af(Bd(moveleft(x)))
Bd(moveleft(Cg(x))) → Ag(Bd(moveleft(x)))
Bf(moveleft(Ca(x))) → Aa(Bf(moveleft(x)))
Bf(moveleft(Cb(x))) → Ab(Bf(moveleft(x)))
Bf(moveleft(Cc(x))) → Ac(Bf(moveleft(x)))
Bf(moveleft(Cd(x))) → Ad(Bf(moveleft(x)))
Bf(moveleft(Cf(x))) → Af(Bf(moveleft(x)))
Bf(moveleft(Cg(x))) → Ag(Bf(moveleft(x)))
Bg(moveleft(Ca(x))) → Aa(Bg(moveleft(x)))
Bg(moveleft(Cb(x))) → Ab(Bg(moveleft(x)))
Bg(moveleft(Cc(x))) → Ac(Bg(moveleft(x)))
Bg(moveleft(Cd(x))) → Ad(Bg(moveleft(x)))
Bg(moveleft(Cf(x))) → Af(Bg(moveleft(x)))
Bg(moveleft(Cg(x))) → Ag(Bg(moveleft(x)))
Ba(moveleft(cut(x))) → goright(cut(Da(x)))
Bb(moveleft(cut(x))) → goright(cut(Db(x)))
Bc(moveleft(cut(x))) → goright(cut(Dc(x)))
Bd(moveleft(cut(x))) → goright(cut(Dd(x)))
Bf(moveleft(cut(x))) → goright(cut(Df(x)))
Bg(moveleft(cut(x))) → goright(cut(Dg(x)))
Aa(goright(x)) → goright(Ca(x))
Ab(goright(x)) → goright(Cb(x))
Ac(goright(x)) → goright(Cc(x))
Ad(goright(x)) → goright(Cd(x))
Af(goright(x)) → goright(Cf(x))
Ag(goright(x)) → goright(Cg(x))
a(wait(goright(x))) → wait(Ba(moveleft(x)))
b(wait(goright(x))) → wait(Bb(moveleft(x)))
c(wait(goright(x))) → wait(Bc(moveleft(x)))
d(wait(goright(x))) → wait(Bd(moveleft(x)))
f(wait(goright(x))) → wait(Bf(moveleft(x)))
g(wait(goright(x))) → wait(Bg(moveleft(x)))
finish(Ca(x)) → a(finish(x))
finish(Cb(x)) → b(finish(x))
finish(Cc(x)) → c(finish(x))
finish(Cd(x)) → d(finish(x))
finish(Cf(x)) → f(finish(x))
finish(Cg(x)) → g(finish(x))
finish2(Da(x)) → a(finish2(x))
finish2(Db(x)) → b(finish2(x))
finish2(Dc(x)) → c(finish2(x))
finish2(Dd(x)) → d(finish2(x))
finish2(Df(x)) → f(finish2(x))
finish2(Dg(x)) → g(finish2(x))

The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(99) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(100) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FINISH(Cb(x)) → FINISH(x)
FINISH(Ca(x)) → FINISH(x)
FINISH(Cc(x)) → FINISH(x)
FINISH(Cd(x)) → FINISH(x)
FINISH(Cf(x)) → FINISH(x)
FINISH(Cg(x)) → FINISH(x)

R is empty.
The set Q consists of the following terms:

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

We have to consider all minimal (P,Q,R)-chains.

(101) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

a(guess(x0))
b(guess(x0))
c(guess(x0))
d(guess(x0))
f(guess(x0))
g(guess(x0))
Ba(moveleft(Ca(x0)))
Ba(moveleft(Cb(x0)))
Ba(moveleft(Cc(x0)))
Ba(moveleft(Cd(x0)))
Ba(moveleft(Cf(x0)))
Ba(moveleft(Cg(x0)))
Bb(moveleft(Ca(x0)))
Bb(moveleft(Cb(x0)))
Bb(moveleft(Cc(x0)))
Bb(moveleft(Cd(x0)))
Bb(moveleft(Cf(x0)))
Bb(moveleft(Cg(x0)))
Bc(moveleft(Ca(x0)))
Bc(moveleft(Cb(x0)))
Bc(moveleft(Cc(x0)))
Bc(moveleft(Cd(x0)))
Bc(moveleft(Cf(x0)))
Bc(moveleft(Cg(x0)))
Bd(moveleft(Ca(x0)))
Bd(moveleft(Cb(x0)))
Bd(moveleft(Cc(x0)))
Bd(moveleft(Cd(x0)))
Bd(moveleft(Cf(x0)))
Bd(moveleft(Cg(x0)))
Bf(moveleft(Ca(x0)))
Bf(moveleft(Cb(x0)))
Bf(moveleft(Cc(x0)))
Bf(moveleft(Cd(x0)))
Bf(moveleft(Cf(x0)))
Bf(moveleft(Cg(x0)))
Bg(moveleft(Ca(x0)))
Bg(moveleft(Cb(x0)))
Bg(moveleft(Cc(x0)))
Bg(moveleft(Cd(x0)))
Bg(moveleft(Cf(x0)))
Bg(moveleft(Cg(x0)))
Ba(moveleft(cut(x0)))
Bb(moveleft(cut(x0)))
Bc(moveleft(cut(x0)))
Bd(moveleft(cut(x0)))
Bf(moveleft(cut(x0)))
Bg(moveleft(cut(x0)))
Aa(goright(x0))
Ab(goright(x0))
Ac(goright(x0))
Ad(goright(x0))
Af(goright(x0))
Ag(goright(x0))
a(wait(goright(x0)))
b(wait(goright(x0)))
c(wait(goright(x0)))
d(wait(goright(x0)))
f(wait(goright(x0)))
g(wait(goright(x0)))
finish(Ca(x0))
finish(Cb(x0))
finish(Cc(x0))
finish(Cd(x0))
finish(Cf(x0))
finish(Cg(x0))
finish2(Da(x0))
finish2(Db(x0))
finish2(Dc(x0))
finish2(Dd(x0))
finish2(Df(x0))
finish2(Dg(x0))

(102) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FINISH(Cb(x)) → FINISH(x)
FINISH(Ca(x)) → FINISH(x)
FINISH(Cc(x)) → FINISH(x)
FINISH(Cd(x)) → FINISH(x)
FINISH(Cf(x)) → FINISH(x)
FINISH(Cg(x)) → FINISH(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(103) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

FINISH(Cb(x)) → FINISH(x)
The graph contains the following edges 1 > 1
FINISH(Ca(x)) → FINISH(x)
The graph contains the following edges 1 > 1
FINISH(Cc(x)) → FINISH(x)
The graph contains the following edges 1 > 1
FINISH(Cd(x)) → FINISH(x)
The graph contains the following edges 1 > 1
FINISH(Cf(x)) → FINISH(x)
The graph contains the following edges 1 > 1
FINISH(Cg(x)) → FINISH(x)
The graph contains the following edges 1 > 1