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

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 DependencyGraphProof (⇔)
↳8 QDP
↳9 QDPOrderProof (⇔)
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 QDPOrderProof (⇔)
↳16 QDP
↳17 QDPOrderProof (⇔)
↳18 QDP
↳19 QDPOrderProof (⇔)
↳20 QDP
↳21 QDPOrderProof (⇔)
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 QDPOrderProof (⇔)
↳28 QDP
↳29 QDPOrderProof (⇔)
↳30 QDP
↳31 QDPOrderProof (⇔)
↳32 QDP
↳33 QDPOrderProof (⇔)
↳34 QDP
↳35 QDPOrderProof (⇔)
↳36 QDP
↳37 QDPOrderProof (⇔)
↳38 QDP
↳39 QDPOrderProof (⇔)
↳40 QDP
↳41 QDPOrderProof (⇔)
↳42 QDP
↳43 QDPOrderProof (⇔)
↳44 QDP
↳45 QDPOrderProof (⇔)
↳46 QDP
↳47 QDPOrderProof (⇔)
↳48 QDP
↳49 QDPOrderProof (⇔)
↳50 QDP
↳51 QDPOrderProof (⇔)
↳52 QDP
↳53 QDPOrderProof (⇔)
↳54 QDP
↳55 QDPOrderProof (⇔)
↳56 QDP
↳57 DependencyGraphProof (⇔)
↳58 TRUE

(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) DependencyPairsProof (EQUIVALENT transformation)

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

(2) 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

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) 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

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

(5) 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: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x7)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x7)

Tags:
IDLE has tags [11,8,14,11,12,9,2]
BUSY has tags [7,1,1,8,6,10,2]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
newbuttons(x1, x2, x3, x4)  =  newbuttons(x1, x2, x3, x4)
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 with status [LPO].
Quasi-Precedence:
or > [open, empty]
[B, closed, false, F, S, true, down, up, BF, FS] > stop > newbuttons4 > [open, empty]

Status:
newbuttons4: [4,3,2,1]
or: []
B: []
closed: []
stop: []
false: []
F: []
S: []
open: []
empty: []
true: []
down: []
up: []
BF: []
FS: []


The following usable rules [FROCOS05] were oriented: none

(6) 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

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) 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

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

(9) 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: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3, x5)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x5)

Tags:
IDLE has tags [2,2,2,11,2,15,15]
BUSY has tags [2,1,1,0,2,0,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[open, true] > [B, stop, false, S, down, up, BF, FS] > [closed, F]

Status:
empty: []
B: []
open: []
stop: []
false: []
closed: []
F: []
S: []
true: []
down: []
up: []
BF: []
FS: []


The following usable rules [FROCOS05] were oriented: none

(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(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

Q is empty.
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(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: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x4)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x2, x3, x4)

Tags:
IDLE has tags [0,0,0,1,7,15,9]
BUSY has tags [0,0,0,1,8,0,6]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[B, stop, closed, F, S, true, BF] > down > [open, false]
[B, stop, closed, F, S, true, BF] > down > FS
[B, stop, closed, F, S, true, BF] > up > [open, false]
[B, stop, closed, F, S, true, BF] > up > FS

Status:
empty: []
B: []
open: []
stop: []
false: []
closed: []
F: []
S: []
true: []
down: []
up: []
BF: []
FS: []


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(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

Q is empty.
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, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x4)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x3, x4)

Tags:
IDLE has tags [8,8,8,8,11,15,1]
BUSY has tags [7,0,8,8,4,0,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[false, up] > [stop, closed, S, true, down] > B > BF
[false, up] > [stop, closed, S, true, down] > open
[false, up] > [stop, closed, S, true, down] > F > BF
[false, up] > [stop, closed, S, true, down] > F > FS

Status:
empty: []
B: []
open: []
stop: []
false: []
closed: []
F: []
S: []
true: []
down: []
up: []
BF: []
FS: []


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(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

Q is empty.
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: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x6)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x6)

Tags:
IDLE has tags [1,1,1,15,15,1,4]
BUSY has tags [1,0,1,0,0,1,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > FS
true > [B, open, false, closed, F, down, up] > S > stop > FS
true > [B, open, false, closed, F, down, up] > BF > FS

Status:
empty: []
B: []
open: []
stop: []
false: []
closed: []
F: []
S: []
true: []
down: []
up: []
BF: []
FS: []


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(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

Q is empty.
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)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x4)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x2, x4)

Tags:
IDLE has tags [3,8,8,8,15,8,9]
BUSY has tags [0,8,0,8,0,4,6]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > [S, BF]
open > [B, stop, false, closed, F, down, up, true, FS] > [S, BF]

Status:
empty: []
B: []
open: []
stop: []
false: []
closed: []
F: []
S: []
down: []
up: []
true: []
BF: []
FS: []


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(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(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

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x2)

Tags:
IDLE has tags [8,4,12,11,12,15,15]
BUSY has tags [8,1,1,3,3,4,3]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
open > [F, false, closed, S, B, down, true, BF, FS] > stop
up > [F, false, closed, S, B, down, true, BF, FS] > stop

Status:
empty: []
F: []
open: []
stop: []
false: []
closed: []
S: []
B: []
down: []
up: []
true: []
BF: []
FS: []


The following usable rules [FROCOS05] were oriented: none

(20) 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(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

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3, x6)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x6)

Tags:
IDLE has tags [7,7,7,15,7,7,12]
BUSY has tags [7,0,0,0,0,7,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[B, closed, down, F, false, BF, FS] > [stop, S, true] > up

Status:
empty: []
B: []
closed: []
down: []
stop: []
S: []
up: []
F: []
true: []
false: []
BF: []
FS: []


The following usable rules [FROCOS05] were oriented: none

(22) 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(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(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

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

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x5)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x5)

Tags:
IDLE has tags [1,1,1,15,1,11,2]
BUSY has tags [1,0,1,0,1,4,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > [B, closed, stop, up, F, true, BF]
[down, S, false, FS] > [B, closed, stop, up, F, true, BF]

Status:
empty: []
B: []
closed: []
down: []
stop: []
S: []
up: []
F: []
true: []
false: []
BF: []
FS: []


The following usable rules [FROCOS05] were oriented: none

(24) 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(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, 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

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

(25) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x5)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x5)

Tags:
IDLE has tags [3,15,3,15,3,15,10]
BUSY has tags [3,0,3,0,3,0,2]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > [closed, stop, S, FS]
[B, up, false, BF] > [down, F, true] > [closed, stop, S, FS]

Status:
empty: []
B: []
closed: []
down: []
stop: []
S: []
up: []
F: []
true: []
false: []
BF: []
FS: []


The following usable rules [FROCOS05] were oriented: none

(26) 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, 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

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

(27) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3, x5)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x5)

Tags:
IDLE has tags [0,8,0,15,0,7,5]
BUSY has tags [0,15,0,0,0,8,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[closed, down, stop, S, false, FS] > [up, true] > [BF, F] > B

Status:
empty: []
B: []
closed: []
down: []
stop: []
S: []
up: []
false: []
BF: []
F: []
FS: []
true: []


The following usable rules [FROCOS05] were oriented: none

(28) 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, 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, 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

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

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x6)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x6)

Tags:
IDLE has tags [1,3,1,15,15,1,0]
BUSY has tags [1,0,1,0,0,1,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > stop
[S, up, true] > [down, F] > [B, closed, false, BF, FS] > stop

Status:
empty: []
B: []
closed: []
down: []
stop: []
S: []
up: []
false: []
BF: []
F: []
FS: []
true: []


The following usable rules [FROCOS05] were oriented: none

(30) 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, 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(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, 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

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

(31) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3)

Tags:
IDLE has tags [7,7,7,15,15,12,5]
BUSY has tags [7,0,0,0,0,3,8]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[B, up, BF, F, FS] > [closed, down, S, true] > stop > false

Status:
empty: []
B: []
closed: []
down: []
stop: []
S: []
up: []
false: []
BF: []
F: []
FS: []
true: []


The following usable rules [FROCOS05] were oriented: none

(32) 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(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(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, 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

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

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3, x5)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x5)

Tags:
IDLE has tags [1,3,5,15,1,3,8]
BUSY has tags [1,0,2,0,1,12,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[B, BF, F, FS, true] > [closed, stop, false, S] > down
[B, BF, F, FS, true] > [closed, stop, false, S] > up

Status:
empty: []
B: []
closed: []
down: []
stop: []
up: []
false: []
BF: []
F: []
FS: []
S: []
true: []


The following usable rules [FROCOS05] were oriented: none

(34) 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(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(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, 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)

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.
We have to consider all minimal (P,Q,R)-chains.

(35) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3, x5)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x5, x7)

Tags:
IDLE has tags [8,13,8,8,8,15,4]
BUSY has tags [8,3,3,4,8,0,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
closed > [B, up, false, BF, F, FS] > stop > down > [empty, true]
closed > [B, up, false, BF, F, FS] > stop > S > [empty, true]

Status:
empty: []
B: []
closed: []
down: []
stop: []
up: []
false: []
BF: []
F: []
FS: []
S: []
true: []


The following usable rules [FROCOS05] were oriented: none

(36) 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(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(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, 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)

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.
We have to consider all minimal (P,Q,R)-chains.

(37) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x3)

Tags:
IDLE has tags [1,1,1,15,15,15,8]
BUSY has tags [0,0,1,0,0,0,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > [B, up, BF, F, FS, S]
[closed, true] > false > [down, stop] > [B, up, BF, F, FS, S]

Status:
empty: []
B: []
closed: []
down: []
stop: []
up: []
false: []
BF: []
F: []
FS: []
S: []
true: []


The following usable rules [FROCOS05] were oriented: none

(38) 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(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(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(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, 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

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

(39) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3, x5)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x5, x7)

Tags:
IDLE has tags [8,14,1,3,1,2,12]
BUSY has tags [8,0,1,12,1,13,2]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
up > [closed, false, F, FS, S, true] > [down, stop] > B > [empty, BF]

Status:
empty: []
B: []
closed: []
down: []
stop: []
up: []
false: []
BF: []
F: []
FS: []
S: []
true: []


The following usable rules [FROCOS05] were oriented: none

(40) 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(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(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(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, 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

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

(41) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1)

Tags:
IDLE has tags [0,1,1,15,15,2,1]
BUSY has tags [0,2,0,0,0,12,1]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > [down, stop]
[B, BF] > [F, FS, S] > [closed, up, false] > true > [down, stop]

Status:
empty: []
B: []
closed: []
down: []
stop: []
up: []
false: []
BF: []
F: []
FS: []
S: []
true: []


The following usable rules [FROCOS05] were oriented: none

(42) 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(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(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(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, 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

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

(43) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1)

Tags:
IDLE has tags [8,0,1,15,15,12,6]
BUSY has tags [8,0,6,0,0,8,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > [down, false, S]
[B, BF] > [closed, stop, up, F, FS, true] > [down, false, S]

Status:
empty: []
B: []
closed: []
down: []
stop: []
up: []
false: []
BF: []
F: []
FS: []
S: []
true: []


The following usable rules [FROCOS05] were oriented: none

(44) 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(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(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, 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

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

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3, x4)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x4)

Tags:
IDLE has tags [8,1,1,1,7,0,1]
BUSY has tags [8,0,1,1,0,0,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > stop
true > down > [B, closed, up, false] > BF > stop
true > down > [B, closed, up, false] > F > FS > stop

Status:
empty: []
B: []
closed: []
down: []
stop: []
up: []
false: []
BF: []
F: []
FS: []
true: []


The following usable rules [FROCOS05] were oriented: none

(46) 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(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, 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

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

(47) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1)

Tags:
IDLE has tags [12,12,12,15,15,15,15]
BUSY has tags [12,2,0,1,3,0,15]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
BF > [B, closed, stop, F, FS] > down > [empty, up]
BF > [B, closed, stop, F, FS] > false > [empty, up]
true > [B, closed, stop, F, FS] > down > [empty, up]
true > [B, closed, stop, F, FS] > false > [empty, up]

Status:
empty: []
B: []
closed: []
down: []
stop: []
F: []
up: []
false: []
FS: []
BF: []
true: []


The following usable rules [FROCOS05] were oriented: none

(48) 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(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, 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

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

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3, x7)

Tags:
IDLE has tags [8,15,8,15,3,12,7]
BUSY has tags [8,0,0,0,12,0,4]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
[closed, true] > [down, F, up, FS] > B > [empty, stop]
[closed, true] > [down, F, up, FS] > false > [empty, stop]

Status:
empty: []
B: []
closed: []
down: []
stop: []
F: []
up: []
false: []
FS: []
true: []


The following usable rules [FROCOS05] were oriented: none

(50) 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(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, 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

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

(51) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x3, x4)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x3, x4)

Tags:
IDLE has tags [1,4,1,0,15,4,11]
BUSY has tags [0,8,1,0,0,1,7]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
up > closed > [false, FS] > [stop, true] > [empty, F, down]

Status:
empty: []
F: []
closed: []
up: []
false: []
FS: []
down: []
stop: []
true: []


The following usable rules [FROCOS05] were oriented: none

(52) 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(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, 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

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

(53) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2, x3)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1, x3)

Tags:
IDLE has tags [5,2,1,8,13,12,12]
BUSY has tags [3,0,1,0,2,2,0]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > [F, down]
up > false > [closed, FS] > [F, down]

Status:
empty: []
F: []
closed: []
up: []
false: []
FS: []
down: []


The following usable rules [FROCOS05] were oriented: none

(54) 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(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, 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

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

(55) 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, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
IDLE(x1, x2, x3, x4, x5, x6, x7)  =  IDLE(x1, x2)
BUSY(x1, x2, x3, x4, x5, x6, x7)  =  BUSY(x1)

Tags:
IDLE has tags [14,0,11,8,7,8,15]
BUSY has tags [0,4,0,6,0,4,4]

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Lexicographic path order with status [LPO].
Quasi-Precedence:
empty > FS
[F, closed, up, false] > FS

Status:
empty: []
F: []
closed: []
up: []
false: []
FS: []


The following usable rules [FROCOS05] were oriented: none

(56) Obligation:

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

BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, 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

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

(57) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(58) TRUE