Termination w.r.t. Q proof of /tmp/tmpnRBy8f/t009.trs

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

0 QTRS

↳1 AAECC Innermost (⇔)

↳2 QTRS

↳3 DependencyPairsProof (⇔)

↳4 QDP

↳5 DependencyGraphProof (⇔)

↳6 QDP

↳7 QDPOrderProof (⇔)

↳8 QDP

↳9 DependencyGraphProof (⇔)

↳10 QDP

↳11 QDPOrderProof (⇔)

↳12 QDP

↳13 QDPOrderProof (⇔)

↳14 QDP

↳15 QDPOrderProof (⇔)

↳16 QDP

↳17 QDPOrderProof (⇔)

↳18 QDP

(0) Obligation:

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

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is

or(true, b) → true
or(false, b) → b

The TRS R 2 is

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)

The signature Sigma is {busy, idle, start, incorrect, correct}

(2) Obligation:

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

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

START(i) → BUSY(F, closed, stop, false, false, false, i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b1, i1)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b2, i2)
IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → OR(b3, i3)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(6) Obligation:

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

IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

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

(7) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IDLE(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → BUSY(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IDLE(x1, x2, x3, x4, x5, x6, x7) = IDLE(x7)
newbuttons(x1, x2, x3, x4) = newbuttons(x4)
BUSY(x1, x2, x3, x4, x5, x6, x7) = BUSY(x7)
or(x1, x2) = or
B = B
closed = closed
stop = stop
false = false
F = F
S = S
open = open
empty = empty
true = true
down = down
up = up
BF = BF
FS = FS

Lexicographic Path Order [LPO].
Precedence:

or > true > down > [B, open]
[stop, false] > [IDLE₁, BUSY₁, empty] > [closed, BF] > [F, S, up] > newbuttons₁ > [B, open]
[stop, false] > [IDLE₁, BUSY₁, empty] > [closed, BF] > [F, S, up] > true > down > [B, open]
FS > [IDLE₁, BUSY₁, empty] > [closed, BF] > [F, S, up] > newbuttons₁ > [B, open]
FS > [IDLE₁, BUSY₁, empty] > [closed, BF] > [F, S, up] > true > down > [B, open]

The following usable rules [FROCOS05] were oriented: none

(8) Obligation:

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

BUSY(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → IDLE(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, 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 1 SCC with 3 less nodes.

(10) Obligation:

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

IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

BUSY(F, d, stop, b1, true, b3, i) → IDLE(F, open, stop, b1, false, b3, i)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IDLE(x1, x2, x3, x4, x5, x6, x7) = IDLE(x5)
empty = empty
BUSY(x1, x2, x3, x4, x5, x6, x7) = BUSY(x5)
B = B
open = open
stop = stop
false = false
closed = closed
F = F
S = S
true = true
down = down
up = up
BF = BF
FS = FS

Lexicographic Path Order [LPO].
Precedence:

empty > [IDLE₁, BUSY₁, stop] > [open, F, BF] > [B, false]
[closed, S, true, down, up, FS] > [IDLE₁, BUSY₁, stop] > [open, F, BF] > [B, false]

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

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

IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

BUSY(B, d, stop, true, b2, b3, i) → IDLE(B, open, stop, false, b2, b3, i)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IDLE(x1, x2, x3, x4, x5, x6, x7) = IDLE(x1, x3, x4)
empty = empty
BUSY(x1, x2, x3, x4, x5, x6, x7) = BUSY(x1, x3, x4)
B = B
open = open
stop = stop
false = false
closed = closed
F = F
S = S
true = true
down = down
up = up
BF = BF
FS = FS

Lexicographic Path Order [LPO].
Precedence:

[IDLE₃, BUSY₃] > empty
[IDLE₃, BUSY₃] > [B, closed, F, S, true, BF, FS] > false > [stop, down, up] > open

The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

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

IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

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

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

BUSY(S, d, stop, b1, b2, true, i) → IDLE(S, open, stop, b1, b2, false, i)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IDLE(x1, x2, x3, x4, x5, x6, x7) = IDLE(x2, x6)
empty = empty
BUSY(x1, x2, x3, x4, x5, x6, x7) = BUSY(x2, x6)
B = B
open = open
stop = stop
false = false
closed = closed
F = F
S = S
true = true
down = down
up = up
BF = BF
FS = FS

Lexicographic Path Order [LPO].
Precedence:

BF > [IDLE₂, BUSY₂] > true > up > [stop, F] > false > down > B > [empty, open, closed]
BF > [IDLE₂, BUSY₂] > true > up > [stop, F] > false > down > S > [empty, open, closed]
FS > [IDLE₂, BUSY₂] > true > up > [stop, F] > false > down > B > [empty, open, closed]
FS > [IDLE₂, BUSY₂] > true > up > [stop, F] > false > down > S > [empty, open, closed]

The following usable rules [FROCOS05] were oriented: none

(16) Obligation:

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

IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

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

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

BUSY(B, open, stop, false, b2, b3, i) → IDLE(B, closed, stop, false, b2, b3, i)
BUSY(F, open, stop, b1, false, b3, i) → IDLE(F, closed, stop, b1, false, b3, i)
BUSY(S, open, stop, b1, b2, false, i) → IDLE(S, closed, stop, b1, b2, false, i)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
IDLE(x1, x2, x3, x4, x5, x6, x7) = x2
empty = empty
BUSY(x1, x2, x3, x4, x5, x6, x7) = x2
B = B
open = open
stop = stop
false = false
closed = closed
F = F
S = S
down = down
up = up
true = true
BF = BF
FS = FS

Lexicographic Path Order [LPO].
Precedence:

empty > stop
BF > down > [open, F, up] > [B, closed] > [false, true] > stop
FS > S > down > [open, F, up] > [B, closed] > [false, true] > stop

The following usable rules [FROCOS05] were oriented: none

(18) Obligation:

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

IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)

The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

The set Q consists of the following terms:

start(x0)
busy(BF, x0, stop, x1, x2, x3, x4)
busy(FS, x0, stop, x1, x2, x3, x4)
busy(x0, open, up, x1, x2, x3, x4)
busy(x0, open, down, x1, x2, x3, x4)
busy(B, closed, stop, false, false, false, empty)
busy(F, closed, stop, false, false, false, empty)
busy(S, closed, stop, false, false, false, empty)
busy(B, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(F, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(S, closed, stop, false, false, false, newbuttons(x0, x1, x2, x3))
busy(B, open, stop, false, x0, x1, x2)
busy(F, open, stop, x0, false, x1, x2)
busy(S, open, stop, x0, x1, false, x2)
busy(B, x0, stop, true, x1, x2, x3)
busy(F, x0, stop, x1, true, x2, x3)
busy(S, x0, stop, x1, x2, true, x3)
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
idle(x0, x1, x2, x3, x4, x5, newbuttons(x6, x7, x8, x9))
or(true, x0)
or(false, x0)

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