/home/nowonder/forschung/aprove/TPDB05/TRS/HM/t009.trs

The program

(VAR fl d m i b b1 b2 b3 i1 i2 i3)
(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
)

(COMMENT
The rewrite system LIFT in \cite{G96}.
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend