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