(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) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = 1 + x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(closed) = 0
POL(correct) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = 1 + x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(incorrect) = 0
POL(newbuttons(x1, x2, x3, x4)) = 4 + x1 + x2 + x3 + x4
POL(open) = 0
POL(or(x1, x2)) = 1 + x1 + x2
POL(start(x1)) = 2 + x1
POL(stop) = 0
POL(true) = 0
POL(up) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
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
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
(2) Obligation:
Q restricted rewrite system:
The TRS R 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)
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)
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(closed) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(newbuttons(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(open) = 1
POL(stop) = 0
POL(true) = 1
POL(up) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
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)
(4) Obligation:
Q restricted rewrite system:
The TRS R 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, 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)
Q is empty.
(5) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(closed) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = x1 + x2 + x3 + x4 + x5 + x6 + x7
POL(newbuttons(x1, x2, x3, x4)) = x1 + x2 + x3 + x4
POL(open) = 0
POL(stop) = 0
POL(true) = 1
POL(up) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
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)
(6) Obligation:
Q restricted rewrite system:
The TRS R 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, 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)
Q is empty.
(7) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x1, x2, x3, x4, x5, x6, x7)) = 2·x1 + 2·x2 + x3 + x4 + x5 + x6 + 2·x7
POL(closed) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x1, x2, x3, x4, x5, x6, x7)) = 2·x1 + 2·x2 + 2·x3 + x4 + x5 + x6 + x7
POL(newbuttons(x1, x2, x3, x4)) = 2 + 2·x1 + x2 + x3 + x4
POL(stop) = 0
POL(true) = 0
POL(up) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
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))
(8) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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)
Q is empty.
(9) AAECC Innermost (EQUIVALENT transformation)
We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is none
The TRS R 2 is
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)
The signature Sigma is {
busy,
idle}
(10) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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)
The set Q consists of the following terms:
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
(11) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
The TRS R consists of the following rules:
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)
The set Q consists of the following terms:
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
We have to consider all minimal (P,Q,R)-chains.
(13) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
R is empty.
The set Q consists of the following terms:
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
We have to consider all minimal (P,Q,R)-chains.
(15) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(17) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
B,
closed,
down,
b1,
b2,
b3,
i) →
IDLE(
B,
closed,
stop,
b1,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
S,
closed,
up,
b1,
b2,
b3,
i) →
IDLE(
S,
closed,
stop,
b1,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
B,
closed,
up,
true,
b2,
b3,
i) →
IDLE(
B,
closed,
stop,
true,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
F,
closed,
up,
b1,
true,
b3,
i) →
IDLE(
F,
closed,
stop,
b1,
true,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(25) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
F,
closed,
down,
b1,
true,
b3,
i) →
IDLE(
F,
closed,
stop,
b1,
true,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
S,
closed,
down,
b1,
b2,
true,
i) →
IDLE(
S,
closed,
stop,
b1,
b2,
true,
i) we obtained the following new rules [LPAR04]:
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(29) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
B,
closed,
up,
false,
b2,
b3,
i) →
IDLE(
BF,
closed,
up,
false,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
(30) 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)
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(31) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
F,
closed,
up,
b1,
false,
b3,
i) →
IDLE(
FS,
closed,
up,
b1,
false,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
F,
closed,
down,
b1,
false,
b3,
i) →
IDLE(
BF,
closed,
down,
b1,
false,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(35) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
S,
closed,
down,
b1,
b2,
false,
i) →
IDLE(
FS,
closed,
down,
b1,
b2,
false,
i) we obtained the following new rules [LPAR04]:
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(37) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
BF,
closed,
up,
b1,
b2,
b3,
i) →
IDLE(
F,
closed,
up,
b1,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(39) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
BF,
closed,
down,
b1,
b2,
b3,
i) →
IDLE(
B,
closed,
down,
b1,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(41) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
FS,
closed,
up,
b1,
b2,
b3,
i) →
IDLE(
S,
closed,
up,
b1,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(43) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
FS,
closed,
down,
b1,
b2,
b3,
i) →
IDLE(
F,
closed,
down,
b1,
b2,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(45) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
B,
closed,
stop,
false,
true,
b3,
i) →
IDLE(
B,
closed,
up,
false,
true,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(47) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
B,
closed,
stop,
false,
false,
true,
i) →
IDLE(
B,
closed,
up,
false,
false,
true,
i) we obtained the following new rules [LPAR04]:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(49) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
F,
closed,
stop,
true,
false,
b3,
i) →
IDLE(
F,
closed,
down,
true,
false,
b3,
i) we obtained the following new rules [LPAR04]:
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(51) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
F,
closed,
stop,
false,
false,
true,
i) →
IDLE(
F,
closed,
up,
false,
false,
true,
i) we obtained the following new rules [LPAR04]:
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(53) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
S,
closed,
stop,
b1,
true,
false,
i) →
IDLE(
S,
closed,
down,
b1,
true,
false,
i) we obtained the following new rules [LPAR04]:
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(55) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
S,
closed,
stop,
true,
false,
false,
i) →
IDLE(
S,
closed,
down,
true,
false,
false,
i) we obtained the following new rules [LPAR04]:
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
(56) 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, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(57) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IDLE(
fl,
d,
m,
b1,
b2,
b3,
empty) →
BUSY(
fl,
d,
m,
b1,
b2,
b3,
empty) we obtained the following new rules [LPAR04]:
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
IDLE(B, closed, stop, true, z0, z1, empty) → BUSY(B, closed, stop, true, z0, z1, empty)
IDLE(F, closed, stop, z0, true, z1, empty) → BUSY(F, closed, stop, z0, true, z1, empty)
IDLE(S, closed, stop, z0, z1, true, empty) → BUSY(S, closed, stop, z0, z1, true, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, stop, true, false, z5, empty) → IDLE(F, closed, down, true, false, z5, empty)
BUSY(F, closed, stop, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
IDLE(B, closed, stop, true, z0, z1, empty) → BUSY(B, closed, stop, true, z0, z1, empty)
IDLE(F, closed, stop, z0, true, z1, empty) → BUSY(F, closed, stop, z0, true, z1, empty)
IDLE(S, closed, stop, z0, z1, true, empty) → BUSY(S, closed, stop, z0, z1, true, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(59) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 9 less nodes.
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(61) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
B,
closed,
up,
false,
z4,
z5,
empty) →
IDLE(
BF,
closed,
up,
false,
z4,
z5,
empty) we obtained the following new rules [LPAR04]:
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(63) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IDLE(
BF,
closed,
up,
false,
z0,
z1,
empty) →
BUSY(
BF,
closed,
up,
false,
z0,
z1,
empty) we obtained the following new rules [LPAR04]:
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(65) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
BF,
closed,
up,
z3,
z4,
z5,
empty) →
IDLE(
F,
closed,
up,
z3,
z4,
z5,
empty) we obtained the following new rules [LPAR04]:
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(67) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IDLE(
F,
closed,
up,
z0,
z1,
z2,
empty) →
BUSY(
F,
closed,
up,
z0,
z1,
z2,
empty) we obtained the following new rules [LPAR04]:
IDLE(F, closed, up, false, true, z0, empty) → BUSY(F, closed, up, false, true, z0, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, z5, empty) → IDLE(B, closed, up, false, true, z5, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, true, z0, empty) → BUSY(F, closed, up, false, true, z0, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(69) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 6 less nodes.
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(F, closed, up, z3, false, z5, empty) → IDLE(FS, closed, up, z3, false, z5, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(71) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
F,
closed,
up,
z3,
false,
z5,
empty) →
IDLE(
FS,
closed,
up,
z3,
false,
z5,
empty) we obtained the following new rules [LPAR04]:
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(73) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IDLE(
FS,
closed,
up,
z0,
false,
z1,
empty) →
BUSY(
FS,
closed,
up,
z0,
false,
z1,
empty) we obtained the following new rules [LPAR04]:
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(75) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
FS,
closed,
up,
z3,
z4,
z5,
empty) →
IDLE(
S,
closed,
up,
z3,
z4,
z5,
empty) we obtained the following new rules [LPAR04]:
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(77) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IDLE(
S,
closed,
up,
z0,
z1,
z2,
empty) →
BUSY(
S,
closed,
up,
z0,
z1,
z2,
empty) we obtained the following new rules [LPAR04]:
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(S, closed, up, z3, z4, z5, empty) → IDLE(S, closed, stop, z3, z4, z5, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(79) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
BUSY(
S,
closed,
up,
z3,
z4,
z5,
empty) →
IDLE(
S,
closed,
stop,
z3,
z4,
z5,
empty) we obtained the following new rules [LPAR04]:
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(81) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IDLE(
S,
closed,
stop,
z0,
z1,
z2,
empty) →
BUSY(
S,
closed,
stop,
z0,
z1,
z2,
empty) we obtained the following new rules [LPAR04]:
IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, stop, false, false, true, empty)
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(F, closed, down, z3, false, z5, empty) → IDLE(BF, closed, down, z3, false, z5, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
BUSY(BF, closed, down, z3, z4, z5, empty) → IDLE(B, closed, down, z3, z4, z5, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
BUSY(B, closed, down, z3, z4, z5, empty) → IDLE(B, closed, stop, z3, z4, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(S, closed, stop, true, false, false, empty) → IDLE(S, closed, down, true, false, false, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, stop, false, false, true, empty)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(83) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 27 less nodes.
(84) TRUE