MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { start(i) ->
    busy(F(), closed(), stop(), false(), false(), false(), i)
  , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
  , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
  , busy(F(), d, stop(), b1, true(), b3, i) ->
    idle(F(), open(), stop(), b1, false(), b3, i)
  , busy(F(), closed(), stop(), false(), false(), false(), empty())
    -> correct()
  , 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(F(), closed(), stop(), false(), false(), true(), i) ->
    idle(F(), 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(), up(), b1, false(), b3, i) ->
    idle(FS(), closed(), up(), b1, false(), b3, i)
  , busy(F(), closed(), up(), b1, true(), b3, i) ->
    idle(F(), closed(), stop(), b1, true(), b3, i)
  , busy(F(), closed(), down(), b1, false(), b3, i) ->
    idle(BF(), closed(), down(), b1, false(), b3, i)
  , busy(F(), closed(), down(), b1, true(), b3, i) ->
    idle(F(), closed(), stop(), b1, true(), b3, i)
  , busy(F(), open(), stop(), b1, false(), b3, i) ->
    idle(F(), closed(), stop(), b1, false(), b3, i)
  , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
  , 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(), d, stop(), b1, b2, b3, i) -> incorrect()
  , 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(), d, stop(), true(), b2, b3, i) ->
    idle(B(), open(), stop(), false(), b2, b3, i)
  , busy(B(), 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(B(), closed(), stop(), false(), false(), true(), i) ->
    idle(B(), closed(), up(), false(), false(), true(), i)
  , busy(B(), closed(), stop(), false(), true(), b3, i) ->
    idle(B(), closed(), up(), false(), true(), b3, i)
  , busy(B(), closed(), up(), false(), b2, b3, i) ->
    idle(BF(), closed(), up(), false(), b2, b3, i)
  , busy(B(), closed(), up(), true(), b2, b3, i) ->
    idle(B(), closed(), stop(), true(), b2, b3, i)
  , busy(B(), closed(), down(), b1, b2, b3, i) ->
    idle(B(), closed(), stop(), b1, b2, b3, i)
  , busy(B(), open(), stop(), false(), b2, b3, i) ->
    idle(B(), closed(), stop(), false(), b2, b3, i)
  , busy(S(), d, stop(), b1, b2, true(), i) ->
    idle(S(), open(), stop(), b1, b2, false(), i)
  , busy(S(), closed(), stop(), b1, true(), false(), i) ->
    idle(S(), closed(), down(), b1, true(), false(), i)
  , busy(S(), closed(), stop(), false(), false(), false(), empty())
    -> correct()
  , 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(S(), closed(), stop(), true(), false(), false(), i) ->
    idle(S(), closed(), down(), true(), false(), false(), i)
  , busy(S(), closed(), up(), b1, b2, b3, i) ->
    idle(S(), closed(), stop(), b1, b2, b3, i)
  , busy(S(), closed(), down(), b1, b2, false(), i) ->
    idle(FS(), closed(), down(), b1, b2, false(), i)
  , busy(S(), closed(), down(), b1, b2, true(), i) ->
    idle(S(), closed(), stop(), b1, b2, true(), i)
  , busy(S(), open(), stop(), b1, b2, false(), i) ->
    idle(S(), closed(), stop(), b1, b2, 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(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following weak dependency pairs:

Strict DPs:
  { start^#(i) ->
    c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
  , busy^#(fl, open(), up(), b1, b2, b3, i) -> c_2()
  , busy^#(fl, open(), down(), b1, b2, b3, i) -> c_3()
  , busy^#(F(), d, stop(), b1, true(), b3, i) ->
    c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
  , busy^#(F(), closed(), stop(), false(), false(), false(), empty())
    -> c_5()
  , busy^#(F(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_6(idle^#(F(),
               closed(),
               stop(),
               false(),
               false(),
               false(),
               newbuttons(i1, i2, i3, i)))
  , busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
    c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
  , busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
    c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
  , busy^#(F(), closed(), up(), b1, false(), b3, i) ->
    c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
  , busy^#(F(), closed(), up(), b1, true(), b3, i) ->
    c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), closed(), down(), b1, false(), b3, i) ->
    c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
  , busy^#(F(), closed(), down(), b1, true(), b3, i) ->
    c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), open(), stop(), b1, false(), b3, i) ->
    c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
  , busy^#(BF(), d, stop(), b1, b2, b3, i) -> c_14()
  , busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
    c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
  , busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
    c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
  , busy^#(FS(), d, stop(), b1, b2, b3, i) -> c_17()
  , busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
    c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
  , busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
    c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
  , busy^#(B(), d, stop(), true(), b2, b3, i) ->
    c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
  , busy^#(B(), closed(), stop(), false(), false(), false(), empty())
    -> c_21()
  , busy^#(B(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_22(idle^#(B(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
    c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
  , busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
    c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
  , busy^#(B(), closed(), up(), false(), b2, b3, i) ->
    c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
  , busy^#(B(), closed(), up(), true(), b2, b3, i) ->
    c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
  , busy^#(B(), closed(), down(), b1, b2, b3, i) ->
    c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
  , busy^#(B(), open(), stop(), false(), b2, b3, i) ->
    c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
  , busy^#(S(), d, stop(), b1, b2, true(), i) ->
    c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
  , busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
    c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
  , busy^#(S(), closed(), stop(), false(), false(), false(), empty())
    -> c_31()
  , busy^#(S(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_32(idle^#(S(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
    c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
  , busy^#(S(), closed(), up(), b1, b2, b3, i) ->
    c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
  , busy^#(S(), closed(), down(), b1, b2, false(), i) ->
    c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
  , busy^#(S(), closed(), down(), b1, b2, true(), i) ->
    c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
  , busy^#(S(), open(), stop(), b1, b2, false(), i) ->
    c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
  , idle^#(fl, d, m, b1, b2, b3, empty()) ->
    c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
  , idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i))
  , or^#(false(), b) -> c_40()
  , or^#(true(), b) -> c_41() }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { start^#(i) ->
    c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
  , busy^#(fl, open(), up(), b1, b2, b3, i) -> c_2()
  , busy^#(fl, open(), down(), b1, b2, b3, i) -> c_3()
  , busy^#(F(), d, stop(), b1, true(), b3, i) ->
    c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
  , busy^#(F(), closed(), stop(), false(), false(), false(), empty())
    -> c_5()
  , busy^#(F(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_6(idle^#(F(),
               closed(),
               stop(),
               false(),
               false(),
               false(),
               newbuttons(i1, i2, i3, i)))
  , busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
    c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
  , busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
    c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
  , busy^#(F(), closed(), up(), b1, false(), b3, i) ->
    c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
  , busy^#(F(), closed(), up(), b1, true(), b3, i) ->
    c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), closed(), down(), b1, false(), b3, i) ->
    c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
  , busy^#(F(), closed(), down(), b1, true(), b3, i) ->
    c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), open(), stop(), b1, false(), b3, i) ->
    c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
  , busy^#(BF(), d, stop(), b1, b2, b3, i) -> c_14()
  , busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
    c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
  , busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
    c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
  , busy^#(FS(), d, stop(), b1, b2, b3, i) -> c_17()
  , busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
    c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
  , busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
    c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
  , busy^#(B(), d, stop(), true(), b2, b3, i) ->
    c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
  , busy^#(B(), closed(), stop(), false(), false(), false(), empty())
    -> c_21()
  , busy^#(B(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_22(idle^#(B(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
    c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
  , busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
    c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
  , busy^#(B(), closed(), up(), false(), b2, b3, i) ->
    c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
  , busy^#(B(), closed(), up(), true(), b2, b3, i) ->
    c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
  , busy^#(B(), closed(), down(), b1, b2, b3, i) ->
    c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
  , busy^#(B(), open(), stop(), false(), b2, b3, i) ->
    c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
  , busy^#(S(), d, stop(), b1, b2, true(), i) ->
    c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
  , busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
    c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
  , busy^#(S(), closed(), stop(), false(), false(), false(), empty())
    -> c_31()
  , busy^#(S(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_32(idle^#(S(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
    c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
  , busy^#(S(), closed(), up(), b1, b2, b3, i) ->
    c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
  , busy^#(S(), closed(), down(), b1, b2, false(), i) ->
    c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
  , busy^#(S(), closed(), down(), b1, b2, true(), i) ->
    c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
  , busy^#(S(), open(), stop(), b1, b2, false(), i) ->
    c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
  , idle^#(fl, d, m, b1, b2, b3, empty()) ->
    c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
  , idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i))
  , or^#(false(), b) -> c_40()
  , or^#(true(), b) -> c_41() }
Strict Trs:
  { start(i) ->
    busy(F(), closed(), stop(), false(), false(), false(), i)
  , busy(fl, open(), up(), b1, b2, b3, i) -> incorrect()
  , busy(fl, open(), down(), b1, b2, b3, i) -> incorrect()
  , busy(F(), d, stop(), b1, true(), b3, i) ->
    idle(F(), open(), stop(), b1, false(), b3, i)
  , busy(F(), closed(), stop(), false(), false(), false(), empty())
    -> correct()
  , 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(F(), closed(), stop(), false(), false(), true(), i) ->
    idle(F(), 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(), up(), b1, false(), b3, i) ->
    idle(FS(), closed(), up(), b1, false(), b3, i)
  , busy(F(), closed(), up(), b1, true(), b3, i) ->
    idle(F(), closed(), stop(), b1, true(), b3, i)
  , busy(F(), closed(), down(), b1, false(), b3, i) ->
    idle(BF(), closed(), down(), b1, false(), b3, i)
  , busy(F(), closed(), down(), b1, true(), b3, i) ->
    idle(F(), closed(), stop(), b1, true(), b3, i)
  , busy(F(), open(), stop(), b1, false(), b3, i) ->
    idle(F(), closed(), stop(), b1, false(), b3, i)
  , busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect()
  , 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(), d, stop(), b1, b2, b3, i) -> incorrect()
  , 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(), d, stop(), true(), b2, b3, i) ->
    idle(B(), open(), stop(), false(), b2, b3, i)
  , busy(B(), 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(B(), closed(), stop(), false(), false(), true(), i) ->
    idle(B(), closed(), up(), false(), false(), true(), i)
  , busy(B(), closed(), stop(), false(), true(), b3, i) ->
    idle(B(), closed(), up(), false(), true(), b3, i)
  , busy(B(), closed(), up(), false(), b2, b3, i) ->
    idle(BF(), closed(), up(), false(), b2, b3, i)
  , busy(B(), closed(), up(), true(), b2, b3, i) ->
    idle(B(), closed(), stop(), true(), b2, b3, i)
  , busy(B(), closed(), down(), b1, b2, b3, i) ->
    idle(B(), closed(), stop(), b1, b2, b3, i)
  , busy(B(), open(), stop(), false(), b2, b3, i) ->
    idle(B(), closed(), stop(), false(), b2, b3, i)
  , busy(S(), d, stop(), b1, b2, true(), i) ->
    idle(S(), open(), stop(), b1, b2, false(), i)
  , busy(S(), closed(), stop(), b1, true(), false(), i) ->
    idle(S(), closed(), down(), b1, true(), false(), i)
  , busy(S(), closed(), stop(), false(), false(), false(), empty())
    -> correct()
  , 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(S(), closed(), stop(), true(), false(), false(), i) ->
    idle(S(), closed(), down(), true(), false(), false(), i)
  , busy(S(), closed(), up(), b1, b2, b3, i) ->
    idle(S(), closed(), stop(), b1, b2, b3, i)
  , busy(S(), closed(), down(), b1, b2, false(), i) ->
    idle(FS(), closed(), down(), b1, b2, false(), i)
  , busy(S(), closed(), down(), b1, b2, true(), i) ->
    idle(S(), closed(), stop(), b1, b2, true(), i)
  , busy(S(), open(), stop(), b1, b2, false(), i) ->
    idle(S(), closed(), stop(), b1, b2, 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(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { or(false(), b) -> b
    , or(true(), b) -> true() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { start^#(i) ->
    c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
  , busy^#(fl, open(), up(), b1, b2, b3, i) -> c_2()
  , busy^#(fl, open(), down(), b1, b2, b3, i) -> c_3()
  , busy^#(F(), d, stop(), b1, true(), b3, i) ->
    c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
  , busy^#(F(), closed(), stop(), false(), false(), false(), empty())
    -> c_5()
  , busy^#(F(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_6(idle^#(F(),
               closed(),
               stop(),
               false(),
               false(),
               false(),
               newbuttons(i1, i2, i3, i)))
  , busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
    c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
  , busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
    c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
  , busy^#(F(), closed(), up(), b1, false(), b3, i) ->
    c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
  , busy^#(F(), closed(), up(), b1, true(), b3, i) ->
    c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), closed(), down(), b1, false(), b3, i) ->
    c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
  , busy^#(F(), closed(), down(), b1, true(), b3, i) ->
    c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), open(), stop(), b1, false(), b3, i) ->
    c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
  , busy^#(BF(), d, stop(), b1, b2, b3, i) -> c_14()
  , busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
    c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
  , busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
    c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
  , busy^#(FS(), d, stop(), b1, b2, b3, i) -> c_17()
  , busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
    c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
  , busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
    c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
  , busy^#(B(), d, stop(), true(), b2, b3, i) ->
    c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
  , busy^#(B(), closed(), stop(), false(), false(), false(), empty())
    -> c_21()
  , busy^#(B(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_22(idle^#(B(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
    c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
  , busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
    c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
  , busy^#(B(), closed(), up(), false(), b2, b3, i) ->
    c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
  , busy^#(B(), closed(), up(), true(), b2, b3, i) ->
    c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
  , busy^#(B(), closed(), down(), b1, b2, b3, i) ->
    c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
  , busy^#(B(), open(), stop(), false(), b2, b3, i) ->
    c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
  , busy^#(S(), d, stop(), b1, b2, true(), i) ->
    c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
  , busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
    c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
  , busy^#(S(), closed(), stop(), false(), false(), false(), empty())
    -> c_31()
  , busy^#(S(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_32(idle^#(S(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
    c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
  , busy^#(S(), closed(), up(), b1, b2, b3, i) ->
    c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
  , busy^#(S(), closed(), down(), b1, b2, false(), i) ->
    c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
  , busy^#(S(), closed(), down(), b1, b2, true(), i) ->
    c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
  , busy^#(S(), open(), stop(), b1, b2, false(), i) ->
    c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
  , idle^#(fl, d, m, b1, b2, b3, empty()) ->
    c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
  , idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i))
  , or^#(false(), b) -> c_40()
  , or^#(true(), b) -> c_41() }
Strict Trs:
  { or(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(c_1) = {1}, Uargs(busy^#) = {4, 5, 6}, Uargs(c_4) = {1},
  Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1},
  Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1},
  Uargs(c_12) = {1}, Uargs(c_13) = {1}, Uargs(c_15) = {1},
  Uargs(c_16) = {1}, Uargs(c_18) = {1}, Uargs(c_19) = {1},
  Uargs(c_20) = {1}, Uargs(c_22) = {1}, Uargs(c_23) = {1},
  Uargs(c_24) = {1}, Uargs(c_25) = {1}, Uargs(c_26) = {1},
  Uargs(c_27) = {1}, Uargs(c_28) = {1}, Uargs(c_29) = {1},
  Uargs(c_30) = {1}, Uargs(c_32) = {1}, Uargs(c_33) = {1},
  Uargs(c_34) = {1}, Uargs(c_35) = {1}, Uargs(c_36) = {1},
  Uargs(c_37) = {1}, Uargs(c_38) = {1}, Uargs(c_39) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

                                   [F] = [0]                                    
                                                                                
                              [closed] = [0]                                    
                                                                                
                                [stop] = [0]                                    
                                                                                
                               [false] = [0]                                    
                                                                                
                                  [BF] = [0]                                    
                                                                                
                                  [FS] = [0]                                    
                                                                                
                                [open] = [0]                                    
                                                                                
                                  [up] = [0]                                    
                                                                                
                                [down] = [0]                                    
                                                                                
                                   [B] = [0]                                    
                                                                                
                               [empty] = [0]                                    
                                                                                
                                   [S] = [0]                                    
                                                                                
          [newbuttons](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0]
                                                                                
                                [true] = [0]                                    
                                                                                
                          [or](x1, x2) = [1] x2 + [1]                           
                                                                                
                         [start^#](x1) = [1] x1 + [1]                           
                                                                                
                             [c_1](x1) = [1] x1 + [2]                           
                                                                                
  [busy^#](x1, x2, x3, x4, x5, x6, x7) = [1] x4 + [1] x5 + [1] x6 + [1] x7 + [0]
                                                                                
                                 [c_2] = [1]                                    
                                                                                
                                 [c_3] = [1]                                    
                                                                                
                             [c_4](x1) = [1] x1 + [2]                           
                                                                                
  [idle^#](x1, x2, x3, x4, x5, x6, x7) = [1] x4 + [1] x5 + [1] x6 + [1] x7 + [0]
                                                                                
                                 [c_5] = [1]                                    
                                                                                
                             [c_6](x1) = [1] x1 + [2]                           
                                                                                
                             [c_7](x1) = [1] x1 + [2]                           
                                                                                
                             [c_8](x1) = [1] x1 + [2]                           
                                                                                
                             [c_9](x1) = [1] x1 + [2]                           
                                                                                
                            [c_10](x1) = [1] x1 + [2]                           
                                                                                
                            [c_11](x1) = [1] x1 + [2]                           
                                                                                
                            [c_12](x1) = [1] x1 + [2]                           
                                                                                
                            [c_13](x1) = [1] x1 + [2]                           
                                                                                
                                [c_14] = [1]                                    
                                                                                
                            [c_15](x1) = [1] x1 + [2]                           
                                                                                
                            [c_16](x1) = [1] x1 + [2]                           
                                                                                
                                [c_17] = [1]                                    
                                                                                
                            [c_18](x1) = [1] x1 + [2]                           
                                                                                
                            [c_19](x1) = [1] x1 + [2]                           
                                                                                
                            [c_20](x1) = [1] x1 + [2]                           
                                                                                
                                [c_21] = [1]                                    
                                                                                
                            [c_22](x1) = [1] x1 + [2]                           
                                                                                
                            [c_23](x1) = [1] x1 + [2]                           
                                                                                
                            [c_24](x1) = [1] x1 + [2]                           
                                                                                
                            [c_25](x1) = [1] x1 + [2]                           
                                                                                
                            [c_26](x1) = [1] x1 + [2]                           
                                                                                
                            [c_27](x1) = [1] x1 + [2]                           
                                                                                
                            [c_28](x1) = [1] x1 + [2]                           
                                                                                
                            [c_29](x1) = [1] x1 + [2]                           
                                                                                
                            [c_30](x1) = [1] x1 + [2]                           
                                                                                
                                [c_31] = [1]                                    
                                                                                
                            [c_32](x1) = [1] x1 + [2]                           
                                                                                
                            [c_33](x1) = [1] x1 + [2]                           
                                                                                
                            [c_34](x1) = [1] x1 + [2]                           
                                                                                
                            [c_35](x1) = [1] x1 + [2]                           
                                                                                
                            [c_36](x1) = [1] x1 + [2]                           
                                                                                
                            [c_37](x1) = [1] x1 + [2]                           
                                                                                
                            [c_38](x1) = [1] x1 + [2]                           
                                                                                
                            [c_39](x1) = [1] x1 + [1]                           
                                                                                
                        [or^#](x1, x2) = [2] x1 + [2]                           
                                                                                
                                [c_40] = [1]                                    
                                                                                
                                [c_41] = [1]                                    

This order satisfies following ordering constraints:

  [or(false(), b)] = [1] b + [1]
                   > [1] b + [0]
                   = [b]        
                                
   [or(true(), b)] = [1] b + [1]
                   > [0]        
                   = [true()]   
                                

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { start^#(i) ->
    c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
  , busy^#(fl, open(), up(), b1, b2, b3, i) -> c_2()
  , busy^#(fl, open(), down(), b1, b2, b3, i) -> c_3()
  , busy^#(F(), d, stop(), b1, true(), b3, i) ->
    c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
  , busy^#(F(), closed(), stop(), false(), false(), false(), empty())
    -> c_5()
  , busy^#(F(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_6(idle^#(F(),
               closed(),
               stop(),
               false(),
               false(),
               false(),
               newbuttons(i1, i2, i3, i)))
  , busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
    c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
  , busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
    c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
  , busy^#(F(), closed(), up(), b1, false(), b3, i) ->
    c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
  , busy^#(F(), closed(), up(), b1, true(), b3, i) ->
    c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), closed(), down(), b1, false(), b3, i) ->
    c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
  , busy^#(F(), closed(), down(), b1, true(), b3, i) ->
    c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), open(), stop(), b1, false(), b3, i) ->
    c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
  , busy^#(BF(), d, stop(), b1, b2, b3, i) -> c_14()
  , busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
    c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
  , busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
    c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
  , busy^#(FS(), d, stop(), b1, b2, b3, i) -> c_17()
  , busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
    c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
  , busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
    c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
  , busy^#(B(), d, stop(), true(), b2, b3, i) ->
    c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
  , busy^#(B(), closed(), stop(), false(), false(), false(), empty())
    -> c_21()
  , busy^#(B(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_22(idle^#(B(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
    c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
  , busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
    c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
  , busy^#(B(), closed(), up(), false(), b2, b3, i) ->
    c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
  , busy^#(B(), closed(), up(), true(), b2, b3, i) ->
    c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
  , busy^#(B(), closed(), down(), b1, b2, b3, i) ->
    c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
  , busy^#(B(), open(), stop(), false(), b2, b3, i) ->
    c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
  , busy^#(S(), d, stop(), b1, b2, true(), i) ->
    c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
  , busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
    c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
  , busy^#(S(), closed(), stop(), false(), false(), false(), empty())
    -> c_31()
  , busy^#(S(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_32(idle^#(S(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
    c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
  , busy^#(S(), closed(), up(), b1, b2, b3, i) ->
    c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
  , busy^#(S(), closed(), down(), b1, b2, false(), i) ->
    c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
  , busy^#(S(), closed(), down(), b1, b2, true(), i) ->
    c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
  , busy^#(S(), open(), stop(), b1, b2, false(), i) ->
    c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
  , idle^#(fl, d, m, b1, b2, b3, empty()) ->
    c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
  , idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) }
Weak DPs:
  { or^#(false(), b) -> c_40()
  , or^#(true(), b) -> c_41() }
Weak Trs:
  { or(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {2,3,5,14,17,21,31} by
applications of Pre({2,3,5,14,17,21,31}) = {1,38,39}. Here rules
are labeled as follows:

  DPs:
    { 1: start^#(i) ->
         c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
    , 2: busy^#(fl, open(), up(), b1, b2, b3, i) -> c_2()
    , 3: busy^#(fl, open(), down(), b1, b2, b3, i) -> c_3()
    , 4: busy^#(F(), d, stop(), b1, true(), b3, i) ->
         c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
    , 5: busy^#(F(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                empty())
         -> c_5()
    , 6: busy^#(F(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i))
         ->
         c_6(idle^#(F(),
                    closed(),
                    stop(),
                    false(),
                    false(),
                    false(),
                    newbuttons(i1, i2, i3, i)))
    , 7: busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
         c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
    , 8: busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
         c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
    , 9: busy^#(F(), closed(), up(), b1, false(), b3, i) ->
         c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
    , 10: busy^#(F(), closed(), up(), b1, true(), b3, i) ->
          c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
    , 11: busy^#(F(), closed(), down(), b1, false(), b3, i) ->
          c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
    , 12: busy^#(F(), closed(), down(), b1, true(), b3, i) ->
          c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
    , 13: busy^#(F(), open(), stop(), b1, false(), b3, i) ->
          c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
    , 14: busy^#(BF(), d, stop(), b1, b2, b3, i) -> c_14()
    , 15: busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
          c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
    , 16: busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
          c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
    , 17: busy^#(FS(), d, stop(), b1, b2, b3, i) -> c_17()
    , 18: busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
          c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
    , 19: busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
          c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
    , 20: busy^#(B(), d, stop(), true(), b2, b3, i) ->
          c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
    , 21: busy^#(B(),
                 closed(),
                 stop(),
                 false(),
                 false(),
                 false(),
                 empty())
          -> c_21()
    , 22: busy^#(B(),
                 closed(),
                 stop(),
                 false(),
                 false(),
                 false(),
                 newbuttons(i1, i2, i3, i))
          ->
          c_22(idle^#(B(),
                      closed(),
                      stop(),
                      false(),
                      false(),
                      false(),
                      newbuttons(i1, i2, i3, i)))
    , 23: busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
          c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
    , 24: busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
          c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
    , 25: busy^#(B(), closed(), up(), false(), b2, b3, i) ->
          c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
    , 26: busy^#(B(), closed(), up(), true(), b2, b3, i) ->
          c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
    , 27: busy^#(B(), closed(), down(), b1, b2, b3, i) ->
          c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
    , 28: busy^#(B(), open(), stop(), false(), b2, b3, i) ->
          c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
    , 29: busy^#(S(), d, stop(), b1, b2, true(), i) ->
          c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
    , 30: busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
          c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
    , 31: busy^#(S(),
                 closed(),
                 stop(),
                 false(),
                 false(),
                 false(),
                 empty())
          -> c_31()
    , 32: busy^#(S(),
                 closed(),
                 stop(),
                 false(),
                 false(),
                 false(),
                 newbuttons(i1, i2, i3, i))
          ->
          c_32(idle^#(S(),
                      closed(),
                      stop(),
                      false(),
                      false(),
                      false(),
                      newbuttons(i1, i2, i3, i)))
    , 33: busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
          c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
    , 34: busy^#(S(), closed(), up(), b1, b2, b3, i) ->
          c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
    , 35: busy^#(S(), closed(), down(), b1, b2, false(), i) ->
          c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
    , 36: busy^#(S(), closed(), down(), b1, b2, true(), i) ->
          c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
    , 37: busy^#(S(), open(), stop(), b1, b2, false(), i) ->
          c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
    , 38: idle^#(fl, d, m, b1, b2, b3, empty()) ->
          c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
    , 39: idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
          c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i))
    , 40: or^#(false(), b) -> c_40()
    , 41: or^#(true(), b) -> c_41() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { start^#(i) ->
    c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
  , busy^#(F(), d, stop(), b1, true(), b3, i) ->
    c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
  , busy^#(F(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_6(idle^#(F(),
               closed(),
               stop(),
               false(),
               false(),
               false(),
               newbuttons(i1, i2, i3, i)))
  , busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
    c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
  , busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
    c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
  , busy^#(F(), closed(), up(), b1, false(), b3, i) ->
    c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
  , busy^#(F(), closed(), up(), b1, true(), b3, i) ->
    c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), closed(), down(), b1, false(), b3, i) ->
    c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
  , busy^#(F(), closed(), down(), b1, true(), b3, i) ->
    c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), open(), stop(), b1, false(), b3, i) ->
    c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
  , busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
    c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
  , busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
    c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
  , busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
    c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
  , busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
    c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
  , busy^#(B(), d, stop(), true(), b2, b3, i) ->
    c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
  , busy^#(B(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_22(idle^#(B(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
    c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
  , busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
    c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
  , busy^#(B(), closed(), up(), false(), b2, b3, i) ->
    c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
  , busy^#(B(), closed(), up(), true(), b2, b3, i) ->
    c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
  , busy^#(B(), closed(), down(), b1, b2, b3, i) ->
    c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
  , busy^#(B(), open(), stop(), false(), b2, b3, i) ->
    c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
  , busy^#(S(), d, stop(), b1, b2, true(), i) ->
    c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
  , busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
    c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
  , busy^#(S(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_32(idle^#(S(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
    c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
  , busy^#(S(), closed(), up(), b1, b2, b3, i) ->
    c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
  , busy^#(S(), closed(), down(), b1, b2, false(), i) ->
    c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
  , busy^#(S(), closed(), down(), b1, b2, true(), i) ->
    c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
  , busy^#(S(), open(), stop(), b1, b2, false(), i) ->
    c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
  , idle^#(fl, d, m, b1, b2, b3, empty()) ->
    c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
  , idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) }
Weak DPs:
  { busy^#(fl, open(), up(), b1, b2, b3, i) -> c_2()
  , busy^#(fl, open(), down(), b1, b2, b3, i) -> c_3()
  , busy^#(F(), closed(), stop(), false(), false(), false(), empty())
    -> c_5()
  , busy^#(BF(), d, stop(), b1, b2, b3, i) -> c_14()
  , busy^#(FS(), d, stop(), b1, b2, b3, i) -> c_17()
  , busy^#(B(), closed(), stop(), false(), false(), false(), empty())
    -> c_21()
  , busy^#(S(), closed(), stop(), false(), false(), false(), empty())
    -> c_31()
  , or^#(false(), b) -> c_40()
  , or^#(true(), b) -> c_41() }
Weak Trs:
  { or(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ busy^#(fl, open(), up(), b1, b2, b3, i) -> c_2()
, busy^#(fl, open(), down(), b1, b2, b3, i) -> c_3()
, busy^#(F(), closed(), stop(), false(), false(), false(), empty())
  -> c_5()
, busy^#(BF(), d, stop(), b1, b2, b3, i) -> c_14()
, busy^#(FS(), d, stop(), b1, b2, b3, i) -> c_17()
, busy^#(B(), closed(), stop(), false(), false(), false(), empty())
  -> c_21()
, busy^#(S(), closed(), stop(), false(), false(), false(), empty())
  -> c_31()
, or^#(false(), b) -> c_40()
, or^#(true(), b) -> c_41() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { start^#(i) ->
    c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
  , busy^#(F(), d, stop(), b1, true(), b3, i) ->
    c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
  , busy^#(F(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_6(idle^#(F(),
               closed(),
               stop(),
               false(),
               false(),
               false(),
               newbuttons(i1, i2, i3, i)))
  , busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
    c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
  , busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
    c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
  , busy^#(F(), closed(), up(), b1, false(), b3, i) ->
    c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
  , busy^#(F(), closed(), up(), b1, true(), b3, i) ->
    c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), closed(), down(), b1, false(), b3, i) ->
    c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
  , busy^#(F(), closed(), down(), b1, true(), b3, i) ->
    c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), open(), stop(), b1, false(), b3, i) ->
    c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
  , busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
    c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
  , busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
    c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
  , busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
    c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
  , busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
    c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
  , busy^#(B(), d, stop(), true(), b2, b3, i) ->
    c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
  , busy^#(B(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_22(idle^#(B(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
    c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
  , busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
    c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
  , busy^#(B(), closed(), up(), false(), b2, b3, i) ->
    c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
  , busy^#(B(), closed(), up(), true(), b2, b3, i) ->
    c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
  , busy^#(B(), closed(), down(), b1, b2, b3, i) ->
    c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
  , busy^#(B(), open(), stop(), false(), b2, b3, i) ->
    c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
  , busy^#(S(), d, stop(), b1, b2, true(), i) ->
    c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
  , busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
    c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
  , busy^#(S(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_32(idle^#(S(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
    c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
  , busy^#(S(), closed(), up(), b1, b2, b3, i) ->
    c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
  , busy^#(S(), closed(), down(), b1, b2, false(), i) ->
    c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
  , busy^#(S(), closed(), down(), b1, b2, true(), i) ->
    c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
  , busy^#(S(), open(), stop(), b1, b2, false(), i) ->
    c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
  , idle^#(fl, d, m, b1, b2, b3, empty()) ->
    c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
  , idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) }
Weak Trs:
  { or(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: start^#(i) ->
     c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i))
     -->_1 busy^#(F(),
                  closed(),
                  stop(),
                  false(),
                  false(),
                  false(),
                  newbuttons(i1, i2, i3, i))
           ->
           c_6(idle^#(F(),
                      closed(),
                      stop(),
                      false(),
                      false(),
                      false(),
                      newbuttons(i1, i2, i3, i))) :3
  
  2: busy^#(F(), d, stop(), b1, true(), b3, i) ->
     c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  3: busy^#(F(),
            closed(),
            stop(),
            false(),
            false(),
            false(),
            newbuttons(i1, i2, i3, i))
     ->
     c_6(idle^#(F(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
  
  4: busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
     c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  5: busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
     c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  6: busy^#(F(), closed(), up(), b1, false(), b3, i) ->
     c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  7: busy^#(F(), closed(), up(), b1, true(), b3, i) ->
     c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  8: busy^#(F(), closed(), down(), b1, false(), b3, i) ->
     c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  9: busy^#(F(), closed(), down(), b1, true(), b3, i) ->
     c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  10: busy^#(F(), open(), stop(), b1, false(), b3, i) ->
      c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  11: busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
      c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  12: busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
      c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  13: busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
      c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  14: busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
      c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  15: busy^#(B(), d, stop(), true(), b2, b3, i) ->
      c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  16: busy^#(B(),
             closed(),
             stop(),
             false(),
             false(),
             false(),
             newbuttons(i1, i2, i3, i))
      ->
      c_22(idle^#(B(),
                  closed(),
                  stop(),
                  false(),
                  false(),
                  false(),
                  newbuttons(i1, i2, i3, i)))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
  
  17: busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
      c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  18: busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
      c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  19: busy^#(B(), closed(), up(), false(), b2, b3, i) ->
      c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  20: busy^#(B(), closed(), up(), true(), b2, b3, i) ->
      c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  21: busy^#(B(), closed(), down(), b1, b2, b3, i) ->
      c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  22: busy^#(B(), open(), stop(), false(), b2, b3, i) ->
      c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  23: busy^#(S(), d, stop(), b1, b2, true(), i) ->
      c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  24: busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
      c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  25: busy^#(S(),
             closed(),
             stop(),
             false(),
             false(),
             false(),
             newbuttons(i1, i2, i3, i))
      ->
      c_32(idle^#(S(),
                  closed(),
                  stop(),
                  false(),
                  false(),
                  false(),
                  newbuttons(i1, i2, i3, i)))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
  
  26: busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
      c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  27: busy^#(S(), closed(), up(), b1, b2, b3, i) ->
      c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  28: busy^#(S(), closed(), down(), b1, b2, false(), i) ->
      c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  29: busy^#(S(), closed(), down(), b1, b2, true(), i) ->
      c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  30: busy^#(S(), open(), stop(), b1, b2, false(), i) ->
      c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
     -->_1 idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
           c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) :32
     -->_1 idle^#(fl, d, m, b1, b2, b3, empty()) ->
           c_38(busy^#(fl, d, m, b1, b2, b3, empty())) :31
  
  31: idle^#(fl, d, m, b1, b2, b3, empty()) ->
      c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
     -->_1 busy^#(S(), open(), stop(), b1, b2, false(), i) ->
           c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i)) :30
     -->_1 busy^#(S(), closed(), down(), b1, b2, true(), i) ->
           c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i)) :29
     -->_1 busy^#(S(), closed(), down(), b1, b2, false(), i) ->
           c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i)) :28
     -->_1 busy^#(S(), closed(), up(), b1, b2, b3, i) ->
           c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i)) :27
     -->_1 busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
           c_33(idle^#(S(),
                       closed(),
                       down(),
                       true(),
                       false(),
                       false(),
                       i)) :26
     -->_1 busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
           c_30(idle^#(S(), closed(), down(), b1, true(), false(), i)) :24
     -->_1 busy^#(S(), d, stop(), b1, b2, true(), i) ->
           c_29(idle^#(S(), open(), stop(), b1, b2, false(), i)) :23
     -->_1 busy^#(B(), open(), stop(), false(), b2, b3, i) ->
           c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i)) :22
     -->_1 busy^#(B(), closed(), down(), b1, b2, b3, i) ->
           c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i)) :21
     -->_1 busy^#(B(), closed(), up(), true(), b2, b3, i) ->
           c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i)) :20
     -->_1 busy^#(B(), closed(), up(), false(), b2, b3, i) ->
           c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i)) :19
     -->_1 busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
           c_24(idle^#(B(), closed(), up(), false(), true(), b3, i)) :18
     -->_1 busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
           c_23(idle^#(B(), closed(), up(), false(), false(), true(), i)) :17
     -->_1 busy^#(B(), d, stop(), true(), b2, b3, i) ->
           c_20(idle^#(B(), open(), stop(), false(), b2, b3, i)) :15
     -->_1 busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
           c_19(idle^#(F(), closed(), down(), b1, b2, b3, i)) :14
     -->_1 busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
           c_18(idle^#(S(), closed(), up(), b1, b2, b3, i)) :13
     -->_1 busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
           c_16(idle^#(B(), closed(), down(), b1, b2, b3, i)) :12
     -->_1 busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
           c_15(idle^#(F(), closed(), up(), b1, b2, b3, i)) :11
     -->_1 busy^#(F(), open(), stop(), b1, false(), b3, i) ->
           c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i)) :10
     -->_1 busy^#(F(), closed(), down(), b1, true(), b3, i) ->
           c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i)) :9
     -->_1 busy^#(F(), closed(), down(), b1, false(), b3, i) ->
           c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i)) :8
     -->_1 busy^#(F(), closed(), up(), b1, true(), b3, i) ->
           c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i)) :7
     -->_1 busy^#(F(), closed(), up(), b1, false(), b3, i) ->
           c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i)) :6
     -->_1 busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
           c_8(idle^#(F(), closed(), down(), true(), false(), b3, i)) :5
     -->_1 busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
           c_7(idle^#(F(), closed(), up(), false(), false(), true(), i)) :4
     -->_1 busy^#(F(), d, stop(), b1, true(), b3, i) ->
           c_4(idle^#(F(), open(), stop(), b1, false(), b3, i)) :2
  
  32: idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
      c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i))
     -->_1 busy^#(S(), open(), stop(), b1, b2, false(), i) ->
           c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i)) :30
     -->_1 busy^#(S(), closed(), down(), b1, b2, true(), i) ->
           c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i)) :29
     -->_1 busy^#(S(), closed(), down(), b1, b2, false(), i) ->
           c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i)) :28
     -->_1 busy^#(S(), closed(), up(), b1, b2, b3, i) ->
           c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i)) :27
     -->_1 busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
           c_33(idle^#(S(),
                       closed(),
                       down(),
                       true(),
                       false(),
                       false(),
                       i)) :26
     -->_1 busy^#(S(),
                  closed(),
                  stop(),
                  false(),
                  false(),
                  false(),
                  newbuttons(i1, i2, i3, i))
           ->
           c_32(idle^#(S(),
                       closed(),
                       stop(),
                       false(),
                       false(),
                       false(),
                       newbuttons(i1, i2, i3, i))) :25
     -->_1 busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
           c_30(idle^#(S(), closed(), down(), b1, true(), false(), i)) :24
     -->_1 busy^#(S(), d, stop(), b1, b2, true(), i) ->
           c_29(idle^#(S(), open(), stop(), b1, b2, false(), i)) :23
     -->_1 busy^#(B(), open(), stop(), false(), b2, b3, i) ->
           c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i)) :22
     -->_1 busy^#(B(), closed(), down(), b1, b2, b3, i) ->
           c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i)) :21
     -->_1 busy^#(B(), closed(), up(), true(), b2, b3, i) ->
           c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i)) :20
     -->_1 busy^#(B(), closed(), up(), false(), b2, b3, i) ->
           c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i)) :19
     -->_1 busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
           c_24(idle^#(B(), closed(), up(), false(), true(), b3, i)) :18
     -->_1 busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
           c_23(idle^#(B(), closed(), up(), false(), false(), true(), i)) :17
     -->_1 busy^#(B(),
                  closed(),
                  stop(),
                  false(),
                  false(),
                  false(),
                  newbuttons(i1, i2, i3, i))
           ->
           c_22(idle^#(B(),
                       closed(),
                       stop(),
                       false(),
                       false(),
                       false(),
                       newbuttons(i1, i2, i3, i))) :16
     -->_1 busy^#(B(), d, stop(), true(), b2, b3, i) ->
           c_20(idle^#(B(), open(), stop(), false(), b2, b3, i)) :15
     -->_1 busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
           c_19(idle^#(F(), closed(), down(), b1, b2, b3, i)) :14
     -->_1 busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
           c_18(idle^#(S(), closed(), up(), b1, b2, b3, i)) :13
     -->_1 busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
           c_16(idle^#(B(), closed(), down(), b1, b2, b3, i)) :12
     -->_1 busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
           c_15(idle^#(F(), closed(), up(), b1, b2, b3, i)) :11
     -->_1 busy^#(F(), open(), stop(), b1, false(), b3, i) ->
           c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i)) :10
     -->_1 busy^#(F(), closed(), down(), b1, true(), b3, i) ->
           c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i)) :9
     -->_1 busy^#(F(), closed(), down(), b1, false(), b3, i) ->
           c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i)) :8
     -->_1 busy^#(F(), closed(), up(), b1, true(), b3, i) ->
           c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i)) :7
     -->_1 busy^#(F(), closed(), up(), b1, false(), b3, i) ->
           c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i)) :6
     -->_1 busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
           c_8(idle^#(F(), closed(), down(), true(), false(), b3, i)) :5
     -->_1 busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
           c_7(idle^#(F(), closed(), up(), false(), false(), true(), i)) :4
     -->_1 busy^#(F(),
                  closed(),
                  stop(),
                  false(),
                  false(),
                  false(),
                  newbuttons(i1, i2, i3, i))
           ->
           c_6(idle^#(F(),
                      closed(),
                      stop(),
                      false(),
                      false(),
                      false(),
                      newbuttons(i1, i2, i3, i))) :3
     -->_1 busy^#(F(), d, stop(), b1, true(), b3, i) ->
           c_4(idle^#(F(), open(), stop(), b1, false(), b3, i)) :2
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { start^#(i) ->
    c_1(busy^#(F(), closed(), stop(), false(), false(), false(), i)) }


We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { busy^#(F(), d, stop(), b1, true(), b3, i) ->
    c_4(idle^#(F(), open(), stop(), b1, false(), b3, i))
  , busy^#(F(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_6(idle^#(F(),
               closed(),
               stop(),
               false(),
               false(),
               false(),
               newbuttons(i1, i2, i3, i)))
  , busy^#(F(), closed(), stop(), false(), false(), true(), i) ->
    c_7(idle^#(F(), closed(), up(), false(), false(), true(), i))
  , busy^#(F(), closed(), stop(), true(), false(), b3, i) ->
    c_8(idle^#(F(), closed(), down(), true(), false(), b3, i))
  , busy^#(F(), closed(), up(), b1, false(), b3, i) ->
    c_9(idle^#(FS(), closed(), up(), b1, false(), b3, i))
  , busy^#(F(), closed(), up(), b1, true(), b3, i) ->
    c_10(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), closed(), down(), b1, false(), b3, i) ->
    c_11(idle^#(BF(), closed(), down(), b1, false(), b3, i))
  , busy^#(F(), closed(), down(), b1, true(), b3, i) ->
    c_12(idle^#(F(), closed(), stop(), b1, true(), b3, i))
  , busy^#(F(), open(), stop(), b1, false(), b3, i) ->
    c_13(idle^#(F(), closed(), stop(), b1, false(), b3, i))
  , busy^#(BF(), closed(), up(), b1, b2, b3, i) ->
    c_15(idle^#(F(), closed(), up(), b1, b2, b3, i))
  , busy^#(BF(), closed(), down(), b1, b2, b3, i) ->
    c_16(idle^#(B(), closed(), down(), b1, b2, b3, i))
  , busy^#(FS(), closed(), up(), b1, b2, b3, i) ->
    c_18(idle^#(S(), closed(), up(), b1, b2, b3, i))
  , busy^#(FS(), closed(), down(), b1, b2, b3, i) ->
    c_19(idle^#(F(), closed(), down(), b1, b2, b3, i))
  , busy^#(B(), d, stop(), true(), b2, b3, i) ->
    c_20(idle^#(B(), open(), stop(), false(), b2, b3, i))
  , busy^#(B(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_22(idle^#(B(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(B(), closed(), stop(), false(), false(), true(), i) ->
    c_23(idle^#(B(), closed(), up(), false(), false(), true(), i))
  , busy^#(B(), closed(), stop(), false(), true(), b3, i) ->
    c_24(idle^#(B(), closed(), up(), false(), true(), b3, i))
  , busy^#(B(), closed(), up(), false(), b2, b3, i) ->
    c_25(idle^#(BF(), closed(), up(), false(), b2, b3, i))
  , busy^#(B(), closed(), up(), true(), b2, b3, i) ->
    c_26(idle^#(B(), closed(), stop(), true(), b2, b3, i))
  , busy^#(B(), closed(), down(), b1, b2, b3, i) ->
    c_27(idle^#(B(), closed(), stop(), b1, b2, b3, i))
  , busy^#(B(), open(), stop(), false(), b2, b3, i) ->
    c_28(idle^#(B(), closed(), stop(), false(), b2, b3, i))
  , busy^#(S(), d, stop(), b1, b2, true(), i) ->
    c_29(idle^#(S(), open(), stop(), b1, b2, false(), i))
  , busy^#(S(), closed(), stop(), b1, true(), false(), i) ->
    c_30(idle^#(S(), closed(), down(), b1, true(), false(), i))
  , busy^#(S(),
           closed(),
           stop(),
           false(),
           false(),
           false(),
           newbuttons(i1, i2, i3, i))
    ->
    c_32(idle^#(S(),
                closed(),
                stop(),
                false(),
                false(),
                false(),
                newbuttons(i1, i2, i3, i)))
  , busy^#(S(), closed(), stop(), true(), false(), false(), i) ->
    c_33(idle^#(S(), closed(), down(), true(), false(), false(), i))
  , busy^#(S(), closed(), up(), b1, b2, b3, i) ->
    c_34(idle^#(S(), closed(), stop(), b1, b2, b3, i))
  , busy^#(S(), closed(), down(), b1, b2, false(), i) ->
    c_35(idle^#(FS(), closed(), down(), b1, b2, false(), i))
  , busy^#(S(), closed(), down(), b1, b2, true(), i) ->
    c_36(idle^#(S(), closed(), stop(), b1, b2, true(), i))
  , busy^#(S(), open(), stop(), b1, b2, false(), i) ->
    c_37(idle^#(S(), closed(), stop(), b1, b2, false(), i))
  , idle^#(fl, d, m, b1, b2, b3, empty()) ->
    c_38(busy^#(fl, d, m, b1, b2, b3, empty()))
  , idle^#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) ->
    c_39(busy^#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) }
Weak Trs:
  { or(false(), b) -> b
  , or(true(), b) -> true() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..