LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ 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}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
Strict Trs:
{ 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}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ 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}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
MAYBE
We consider the following Problem:
Strict Trs:
{ 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}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ 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}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
MAYBE
We consider the following Problem:
Strict Trs:
{ 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}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..