WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 6557 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 15.2 s] (6) BEST (7) proven lower bound (8) LowerBoundPropagationProof [FINISHED, 0 ms] (9) BOUNDS(n^1, INF) (10) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: START(z0) -> c(BUSY(F, closed, stop, false, false, false, z0)) BUSY(BF, z0, stop, z1, z2, z3, z4) -> c1 BUSY(FS, z0, stop, z1, z2, z3, z4) -> c2 BUSY(z0, open, up, z1, z2, z3, z4) -> c3 BUSY(z0, open, down, z1, z2, z3, z4) -> c4 BUSY(B, closed, stop, false, false, false, empty) -> c5 BUSY(F, closed, stop, false, false, false, empty) -> c6 BUSY(S, closed, stop, false, false, false, empty) -> c7 BUSY(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c8(IDLE(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c9(IDLE(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c10(IDLE(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(B, open, stop, false, z0, z1, z2) -> c11(IDLE(B, closed, stop, false, z0, z1, z2)) BUSY(F, open, stop, z0, false, z1, z2) -> c12(IDLE(F, closed, stop, z0, false, z1, z2)) BUSY(S, open, stop, z0, z1, false, z2) -> c13(IDLE(S, closed, stop, z0, z1, false, z2)) BUSY(B, z0, stop, true, z1, z2, z3) -> c14(IDLE(B, open, stop, false, z1, z2, z3)) BUSY(F, z0, stop, z1, true, z2, z3) -> c15(IDLE(F, open, stop, z1, false, z2, z3)) BUSY(S, z0, stop, z1, z2, true, z3) -> c16(IDLE(S, open, stop, z1, z2, false, z3)) BUSY(B, closed, down, z0, z1, z2, z3) -> c17(IDLE(B, closed, stop, z0, z1, z2, z3)) BUSY(S, closed, up, z0, z1, z2, z3) -> c18(IDLE(S, closed, stop, z0, z1, z2, z3)) BUSY(B, closed, up, true, z0, z1, z2) -> c19(IDLE(B, closed, stop, true, z0, z1, z2)) BUSY(F, closed, up, z0, true, z1, z2) -> c20(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(F, closed, down, z0, true, z1, z2) -> c21(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(S, closed, down, z0, z1, true, z2) -> c22(IDLE(S, closed, stop, z0, z1, true, z2)) BUSY(B, closed, up, false, z0, z1, z2) -> c23(IDLE(BF, closed, up, false, z0, z1, z2)) BUSY(F, closed, up, z0, false, z1, z2) -> c24(IDLE(FS, closed, up, z0, false, z1, z2)) BUSY(F, closed, down, z0, false, z1, z2) -> c25(IDLE(BF, closed, down, z0, false, z1, z2)) BUSY(S, closed, down, z0, z1, false, z2) -> c26(IDLE(FS, closed, down, z0, z1, false, z2)) BUSY(BF, closed, up, z0, z1, z2, z3) -> c27(IDLE(F, closed, up, z0, z1, z2, z3)) BUSY(BF, closed, down, z0, z1, z2, z3) -> c28(IDLE(B, closed, down, z0, z1, z2, z3)) BUSY(FS, closed, up, z0, z1, z2, z3) -> c29(IDLE(S, closed, up, z0, z1, z2, z3)) BUSY(FS, closed, down, z0, z1, z2, z3) -> c30(IDLE(F, closed, down, z0, z1, z2, z3)) BUSY(B, closed, stop, false, true, z0, z1) -> c31(IDLE(B, closed, up, false, true, z0, z1)) BUSY(B, closed, stop, false, false, true, z0) -> c32(IDLE(B, closed, up, false, false, true, z0)) BUSY(F, closed, stop, true, false, z0, z1) -> c33(IDLE(F, closed, down, true, false, z0, z1)) BUSY(F, closed, stop, false, false, true, z0) -> c34(IDLE(F, closed, up, false, false, true, z0)) BUSY(S, closed, stop, z0, true, false, z1) -> c35(IDLE(S, closed, down, z0, true, false, z1)) BUSY(S, closed, stop, true, false, false, z0) -> c36(IDLE(S, closed, down, true, false, false, z0)) IDLE(z0, z1, z2, z3, z4, z5, empty) -> c37(BUSY(z0, z1, z2, z3, z4, z5, empty)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c38(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z3, z6)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c39(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z4, z7)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c40(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z5, z8)) OR(true, z0) -> c41 OR(false, z0) -> c42 The (relative) TRS S consists of the following rules: start(z0) -> busy(F, closed, stop, false, false, false, z0) busy(BF, z0, stop, z1, z2, z3, z4) -> incorrect busy(FS, z0, stop, z1, z2, z3, z4) -> incorrect busy(z0, open, up, z1, z2, z3, z4) -> incorrect busy(z0, open, down, z1, z2, z3, z4) -> incorrect busy(B, closed, stop, false, false, false, empty) -> correct busy(F, closed, stop, false, false, false, empty) -> correct busy(S, closed, stop, false, false, false, empty) -> correct busy(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(B, open, stop, false, z0, z1, z2) -> idle(B, closed, stop, false, z0, z1, z2) busy(F, open, stop, z0, false, z1, z2) -> idle(F, closed, stop, z0, false, z1, z2) busy(S, open, stop, z0, z1, false, z2) -> idle(S, closed, stop, z0, z1, false, z2) busy(B, z0, stop, true, z1, z2, z3) -> idle(B, open, stop, false, z1, z2, z3) busy(F, z0, stop, z1, true, z2, z3) -> idle(F, open, stop, z1, false, z2, z3) busy(S, z0, stop, z1, z2, true, z3) -> idle(S, open, stop, z1, z2, false, z3) busy(B, closed, down, z0, z1, z2, z3) -> idle(B, closed, stop, z0, z1, z2, z3) busy(S, closed, up, z0, z1, z2, z3) -> idle(S, closed, stop, z0, z1, z2, z3) busy(B, closed, up, true, z0, z1, z2) -> idle(B, closed, stop, true, z0, z1, z2) busy(F, closed, up, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(F, closed, down, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(S, closed, down, z0, z1, true, z2) -> idle(S, closed, stop, z0, z1, true, z2) busy(B, closed, up, false, z0, z1, z2) -> idle(BF, closed, up, false, z0, z1, z2) busy(F, closed, up, z0, false, z1, z2) -> idle(FS, closed, up, z0, false, z1, z2) busy(F, closed, down, z0, false, z1, z2) -> idle(BF, closed, down, z0, false, z1, z2) busy(S, closed, down, z0, z1, false, z2) -> idle(FS, closed, down, z0, z1, false, z2) busy(BF, closed, up, z0, z1, z2, z3) -> idle(F, closed, up, z0, z1, z2, z3) busy(BF, closed, down, z0, z1, z2, z3) -> idle(B, closed, down, z0, z1, z2, z3) busy(FS, closed, up, z0, z1, z2, z3) -> idle(S, closed, up, z0, z1, z2, z3) busy(FS, closed, down, z0, z1, z2, z3) -> idle(F, closed, down, z0, z1, z2, z3) busy(B, closed, stop, false, true, z0, z1) -> idle(B, closed, up, false, true, z0, z1) busy(B, closed, stop, false, false, true, z0) -> idle(B, closed, up, false, false, true, z0) busy(F, closed, stop, true, false, z0, z1) -> idle(F, closed, down, true, false, z0, z1) busy(F, closed, stop, false, false, true, z0) -> idle(F, closed, up, false, false, true, z0) busy(S, closed, stop, z0, true, false, z1) -> idle(S, closed, down, z0, true, false, z1) busy(S, closed, stop, true, false, false, z0) -> idle(S, closed, down, true, false, false, z0) idle(z0, z1, z2, z3, z4, z5, empty) -> busy(z0, z1, z2, z3, z4, z5, empty) idle(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> busy(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9) or(true, z0) -> true or(false, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: START(z0) -> c(BUSY(F, closed, stop, false, false, false, z0)) BUSY(BF, z0, stop, z1, z2, z3, z4) -> c1 BUSY(FS, z0, stop, z1, z2, z3, z4) -> c2 BUSY(z0, open, up, z1, z2, z3, z4) -> c3 BUSY(z0, open, down, z1, z2, z3, z4) -> c4 BUSY(B, closed, stop, false, false, false, empty) -> c5 BUSY(F, closed, stop, false, false, false, empty) -> c6 BUSY(S, closed, stop, false, false, false, empty) -> c7 BUSY(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c8(IDLE(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c9(IDLE(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c10(IDLE(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(B, open, stop, false, z0, z1, z2) -> c11(IDLE(B, closed, stop, false, z0, z1, z2)) BUSY(F, open, stop, z0, false, z1, z2) -> c12(IDLE(F, closed, stop, z0, false, z1, z2)) BUSY(S, open, stop, z0, z1, false, z2) -> c13(IDLE(S, closed, stop, z0, z1, false, z2)) BUSY(B, z0, stop, true, z1, z2, z3) -> c14(IDLE(B, open, stop, false, z1, z2, z3)) BUSY(F, z0, stop, z1, true, z2, z3) -> c15(IDLE(F, open, stop, z1, false, z2, z3)) BUSY(S, z0, stop, z1, z2, true, z3) -> c16(IDLE(S, open, stop, z1, z2, false, z3)) BUSY(B, closed, down, z0, z1, z2, z3) -> c17(IDLE(B, closed, stop, z0, z1, z2, z3)) BUSY(S, closed, up, z0, z1, z2, z3) -> c18(IDLE(S, closed, stop, z0, z1, z2, z3)) BUSY(B, closed, up, true, z0, z1, z2) -> c19(IDLE(B, closed, stop, true, z0, z1, z2)) BUSY(F, closed, up, z0, true, z1, z2) -> c20(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(F, closed, down, z0, true, z1, z2) -> c21(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(S, closed, down, z0, z1, true, z2) -> c22(IDLE(S, closed, stop, z0, z1, true, z2)) BUSY(B, closed, up, false, z0, z1, z2) -> c23(IDLE(BF, closed, up, false, z0, z1, z2)) BUSY(F, closed, up, z0, false, z1, z2) -> c24(IDLE(FS, closed, up, z0, false, z1, z2)) BUSY(F, closed, down, z0, false, z1, z2) -> c25(IDLE(BF, closed, down, z0, false, z1, z2)) BUSY(S, closed, down, z0, z1, false, z2) -> c26(IDLE(FS, closed, down, z0, z1, false, z2)) BUSY(BF, closed, up, z0, z1, z2, z3) -> c27(IDLE(F, closed, up, z0, z1, z2, z3)) BUSY(BF, closed, down, z0, z1, z2, z3) -> c28(IDLE(B, closed, down, z0, z1, z2, z3)) BUSY(FS, closed, up, z0, z1, z2, z3) -> c29(IDLE(S, closed, up, z0, z1, z2, z3)) BUSY(FS, closed, down, z0, z1, z2, z3) -> c30(IDLE(F, closed, down, z0, z1, z2, z3)) BUSY(B, closed, stop, false, true, z0, z1) -> c31(IDLE(B, closed, up, false, true, z0, z1)) BUSY(B, closed, stop, false, false, true, z0) -> c32(IDLE(B, closed, up, false, false, true, z0)) BUSY(F, closed, stop, true, false, z0, z1) -> c33(IDLE(F, closed, down, true, false, z0, z1)) BUSY(F, closed, stop, false, false, true, z0) -> c34(IDLE(F, closed, up, false, false, true, z0)) BUSY(S, closed, stop, z0, true, false, z1) -> c35(IDLE(S, closed, down, z0, true, false, z1)) BUSY(S, closed, stop, true, false, false, z0) -> c36(IDLE(S, closed, down, true, false, false, z0)) IDLE(z0, z1, z2, z3, z4, z5, empty) -> c37(BUSY(z0, z1, z2, z3, z4, z5, empty)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c38(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z3, z6)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c39(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z4, z7)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c40(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z5, z8)) OR(true, z0) -> c41 OR(false, z0) -> c42 The (relative) TRS S consists of the following rules: start(z0) -> busy(F, closed, stop, false, false, false, z0) busy(BF, z0, stop, z1, z2, z3, z4) -> incorrect busy(FS, z0, stop, z1, z2, z3, z4) -> incorrect busy(z0, open, up, z1, z2, z3, z4) -> incorrect busy(z0, open, down, z1, z2, z3, z4) -> incorrect busy(B, closed, stop, false, false, false, empty) -> correct busy(F, closed, stop, false, false, false, empty) -> correct busy(S, closed, stop, false, false, false, empty) -> correct busy(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(B, open, stop, false, z0, z1, z2) -> idle(B, closed, stop, false, z0, z1, z2) busy(F, open, stop, z0, false, z1, z2) -> idle(F, closed, stop, z0, false, z1, z2) busy(S, open, stop, z0, z1, false, z2) -> idle(S, closed, stop, z0, z1, false, z2) busy(B, z0, stop, true, z1, z2, z3) -> idle(B, open, stop, false, z1, z2, z3) busy(F, z0, stop, z1, true, z2, z3) -> idle(F, open, stop, z1, false, z2, z3) busy(S, z0, stop, z1, z2, true, z3) -> idle(S, open, stop, z1, z2, false, z3) busy(B, closed, down, z0, z1, z2, z3) -> idle(B, closed, stop, z0, z1, z2, z3) busy(S, closed, up, z0, z1, z2, z3) -> idle(S, closed, stop, z0, z1, z2, z3) busy(B, closed, up, true, z0, z1, z2) -> idle(B, closed, stop, true, z0, z1, z2) busy(F, closed, up, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(F, closed, down, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(S, closed, down, z0, z1, true, z2) -> idle(S, closed, stop, z0, z1, true, z2) busy(B, closed, up, false, z0, z1, z2) -> idle(BF, closed, up, false, z0, z1, z2) busy(F, closed, up, z0, false, z1, z2) -> idle(FS, closed, up, z0, false, z1, z2) busy(F, closed, down, z0, false, z1, z2) -> idle(BF, closed, down, z0, false, z1, z2) busy(S, closed, down, z0, z1, false, z2) -> idle(FS, closed, down, z0, z1, false, z2) busy(BF, closed, up, z0, z1, z2, z3) -> idle(F, closed, up, z0, z1, z2, z3) busy(BF, closed, down, z0, z1, z2, z3) -> idle(B, closed, down, z0, z1, z2, z3) busy(FS, closed, up, z0, z1, z2, z3) -> idle(S, closed, up, z0, z1, z2, z3) busy(FS, closed, down, z0, z1, z2, z3) -> idle(F, closed, down, z0, z1, z2, z3) busy(B, closed, stop, false, true, z0, z1) -> idle(B, closed, up, false, true, z0, z1) busy(B, closed, stop, false, false, true, z0) -> idle(B, closed, up, false, false, true, z0) busy(F, closed, stop, true, false, z0, z1) -> idle(F, closed, down, true, false, z0, z1) busy(F, closed, stop, false, false, true, z0) -> idle(F, closed, up, false, false, true, z0) busy(S, closed, stop, z0, true, false, z1) -> idle(S, closed, down, z0, true, false, z1) busy(S, closed, stop, true, false, false, z0) -> idle(S, closed, down, true, false, false, z0) idle(z0, z1, z2, z3, z4, z5, empty) -> busy(z0, z1, z2, z3, z4, z5, empty) idle(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> busy(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9) or(true, z0) -> true or(false, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (4) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: START(z0) -> c(BUSY(F, closed, stop, false, false, false, z0)) BUSY(BF, z0, stop, z1, z2, z3, z4) -> c1 BUSY(FS, z0, stop, z1, z2, z3, z4) -> c2 BUSY(z0, open, up, z1, z2, z3, z4) -> c3 BUSY(z0, open, down, z1, z2, z3, z4) -> c4 BUSY(B, closed, stop, false, false, false, empty) -> c5 BUSY(F, closed, stop, false, false, false, empty) -> c6 BUSY(S, closed, stop, false, false, false, empty) -> c7 BUSY(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c8(IDLE(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c9(IDLE(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c10(IDLE(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(B, open, stop, false, z0, z1, z2) -> c11(IDLE(B, closed, stop, false, z0, z1, z2)) BUSY(F, open, stop, z0, false, z1, z2) -> c12(IDLE(F, closed, stop, z0, false, z1, z2)) BUSY(S, open, stop, z0, z1, false, z2) -> c13(IDLE(S, closed, stop, z0, z1, false, z2)) BUSY(B, z0, stop, true, z1, z2, z3) -> c14(IDLE(B, open, stop, false, z1, z2, z3)) BUSY(F, z0, stop, z1, true, z2, z3) -> c15(IDLE(F, open, stop, z1, false, z2, z3)) BUSY(S, z0, stop, z1, z2, true, z3) -> c16(IDLE(S, open, stop, z1, z2, false, z3)) BUSY(B, closed, down, z0, z1, z2, z3) -> c17(IDLE(B, closed, stop, z0, z1, z2, z3)) BUSY(S, closed, up, z0, z1, z2, z3) -> c18(IDLE(S, closed, stop, z0, z1, z2, z3)) BUSY(B, closed, up, true, z0, z1, z2) -> c19(IDLE(B, closed, stop, true, z0, z1, z2)) BUSY(F, closed, up, z0, true, z1, z2) -> c20(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(F, closed, down, z0, true, z1, z2) -> c21(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(S, closed, down, z0, z1, true, z2) -> c22(IDLE(S, closed, stop, z0, z1, true, z2)) BUSY(B, closed, up, false, z0, z1, z2) -> c23(IDLE(BF, closed, up, false, z0, z1, z2)) BUSY(F, closed, up, z0, false, z1, z2) -> c24(IDLE(FS, closed, up, z0, false, z1, z2)) BUSY(F, closed, down, z0, false, z1, z2) -> c25(IDLE(BF, closed, down, z0, false, z1, z2)) BUSY(S, closed, down, z0, z1, false, z2) -> c26(IDLE(FS, closed, down, z0, z1, false, z2)) BUSY(BF, closed, up, z0, z1, z2, z3) -> c27(IDLE(F, closed, up, z0, z1, z2, z3)) BUSY(BF, closed, down, z0, z1, z2, z3) -> c28(IDLE(B, closed, down, z0, z1, z2, z3)) BUSY(FS, closed, up, z0, z1, z2, z3) -> c29(IDLE(S, closed, up, z0, z1, z2, z3)) BUSY(FS, closed, down, z0, z1, z2, z3) -> c30(IDLE(F, closed, down, z0, z1, z2, z3)) BUSY(B, closed, stop, false, true, z0, z1) -> c31(IDLE(B, closed, up, false, true, z0, z1)) BUSY(B, closed, stop, false, false, true, z0) -> c32(IDLE(B, closed, up, false, false, true, z0)) BUSY(F, closed, stop, true, false, z0, z1) -> c33(IDLE(F, closed, down, true, false, z0, z1)) BUSY(F, closed, stop, false, false, true, z0) -> c34(IDLE(F, closed, up, false, false, true, z0)) BUSY(S, closed, stop, z0, true, false, z1) -> c35(IDLE(S, closed, down, z0, true, false, z1)) BUSY(S, closed, stop, true, false, false, z0) -> c36(IDLE(S, closed, down, true, false, false, z0)) IDLE(z0, z1, z2, z3, z4, z5, empty) -> c37(BUSY(z0, z1, z2, z3, z4, z5, empty)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c38(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z3, z6)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c39(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z4, z7)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c40(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z5, z8)) OR(true, z0) -> c41 OR(false, z0) -> c42 The (relative) TRS S consists of the following rules: start(z0) -> busy(F, closed, stop, false, false, false, z0) busy(BF, z0, stop, z1, z2, z3, z4) -> incorrect busy(FS, z0, stop, z1, z2, z3, z4) -> incorrect busy(z0, open, up, z1, z2, z3, z4) -> incorrect busy(z0, open, down, z1, z2, z3, z4) -> incorrect busy(B, closed, stop, false, false, false, empty) -> correct busy(F, closed, stop, false, false, false, empty) -> correct busy(S, closed, stop, false, false, false, empty) -> correct busy(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(B, open, stop, false, z0, z1, z2) -> idle(B, closed, stop, false, z0, z1, z2) busy(F, open, stop, z0, false, z1, z2) -> idle(F, closed, stop, z0, false, z1, z2) busy(S, open, stop, z0, z1, false, z2) -> idle(S, closed, stop, z0, z1, false, z2) busy(B, z0, stop, true, z1, z2, z3) -> idle(B, open, stop, false, z1, z2, z3) busy(F, z0, stop, z1, true, z2, z3) -> idle(F, open, stop, z1, false, z2, z3) busy(S, z0, stop, z1, z2, true, z3) -> idle(S, open, stop, z1, z2, false, z3) busy(B, closed, down, z0, z1, z2, z3) -> idle(B, closed, stop, z0, z1, z2, z3) busy(S, closed, up, z0, z1, z2, z3) -> idle(S, closed, stop, z0, z1, z2, z3) busy(B, closed, up, true, z0, z1, z2) -> idle(B, closed, stop, true, z0, z1, z2) busy(F, closed, up, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(F, closed, down, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(S, closed, down, z0, z1, true, z2) -> idle(S, closed, stop, z0, z1, true, z2) busy(B, closed, up, false, z0, z1, z2) -> idle(BF, closed, up, false, z0, z1, z2) busy(F, closed, up, z0, false, z1, z2) -> idle(FS, closed, up, z0, false, z1, z2) busy(F, closed, down, z0, false, z1, z2) -> idle(BF, closed, down, z0, false, z1, z2) busy(S, closed, down, z0, z1, false, z2) -> idle(FS, closed, down, z0, z1, false, z2) busy(BF, closed, up, z0, z1, z2, z3) -> idle(F, closed, up, z0, z1, z2, z3) busy(BF, closed, down, z0, z1, z2, z3) -> idle(B, closed, down, z0, z1, z2, z3) busy(FS, closed, up, z0, z1, z2, z3) -> idle(S, closed, up, z0, z1, z2, z3) busy(FS, closed, down, z0, z1, z2, z3) -> idle(F, closed, down, z0, z1, z2, z3) busy(B, closed, stop, false, true, z0, z1) -> idle(B, closed, up, false, true, z0, z1) busy(B, closed, stop, false, false, true, z0) -> idle(B, closed, up, false, false, true, z0) busy(F, closed, stop, true, false, z0, z1) -> idle(F, closed, down, true, false, z0, z1) busy(F, closed, stop, false, false, true, z0) -> idle(F, closed, up, false, false, true, z0) busy(S, closed, stop, z0, true, false, z1) -> idle(S, closed, down, z0, true, false, z1) busy(S, closed, stop, true, false, false, z0) -> idle(S, closed, down, true, false, false, z0) idle(z0, z1, z2, z3, z4, z5, empty) -> busy(z0, z1, z2, z3, z4, z5, empty) idle(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> busy(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9) or(true, z0) -> true or(false, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (5) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence IDLE(B, z1, stop, false, true, true, newbuttons(true, z7, z8, z9)) ->^+ c40(c14(IDLE(B, open, stop, false, true, true, z9)), OR(true, z8)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0]. The pumping substitution is [z9 / newbuttons(true, z7, z8, z9)]. The result substitution is [z1 / open]. ---------------------------------------- (6) Complex Obligation (BEST) ---------------------------------------- (7) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: START(z0) -> c(BUSY(F, closed, stop, false, false, false, z0)) BUSY(BF, z0, stop, z1, z2, z3, z4) -> c1 BUSY(FS, z0, stop, z1, z2, z3, z4) -> c2 BUSY(z0, open, up, z1, z2, z3, z4) -> c3 BUSY(z0, open, down, z1, z2, z3, z4) -> c4 BUSY(B, closed, stop, false, false, false, empty) -> c5 BUSY(F, closed, stop, false, false, false, empty) -> c6 BUSY(S, closed, stop, false, false, false, empty) -> c7 BUSY(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c8(IDLE(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c9(IDLE(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c10(IDLE(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(B, open, stop, false, z0, z1, z2) -> c11(IDLE(B, closed, stop, false, z0, z1, z2)) BUSY(F, open, stop, z0, false, z1, z2) -> c12(IDLE(F, closed, stop, z0, false, z1, z2)) BUSY(S, open, stop, z0, z1, false, z2) -> c13(IDLE(S, closed, stop, z0, z1, false, z2)) BUSY(B, z0, stop, true, z1, z2, z3) -> c14(IDLE(B, open, stop, false, z1, z2, z3)) BUSY(F, z0, stop, z1, true, z2, z3) -> c15(IDLE(F, open, stop, z1, false, z2, z3)) BUSY(S, z0, stop, z1, z2, true, z3) -> c16(IDLE(S, open, stop, z1, z2, false, z3)) BUSY(B, closed, down, z0, z1, z2, z3) -> c17(IDLE(B, closed, stop, z0, z1, z2, z3)) BUSY(S, closed, up, z0, z1, z2, z3) -> c18(IDLE(S, closed, stop, z0, z1, z2, z3)) BUSY(B, closed, up, true, z0, z1, z2) -> c19(IDLE(B, closed, stop, true, z0, z1, z2)) BUSY(F, closed, up, z0, true, z1, z2) -> c20(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(F, closed, down, z0, true, z1, z2) -> c21(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(S, closed, down, z0, z1, true, z2) -> c22(IDLE(S, closed, stop, z0, z1, true, z2)) BUSY(B, closed, up, false, z0, z1, z2) -> c23(IDLE(BF, closed, up, false, z0, z1, z2)) BUSY(F, closed, up, z0, false, z1, z2) -> c24(IDLE(FS, closed, up, z0, false, z1, z2)) BUSY(F, closed, down, z0, false, z1, z2) -> c25(IDLE(BF, closed, down, z0, false, z1, z2)) BUSY(S, closed, down, z0, z1, false, z2) -> c26(IDLE(FS, closed, down, z0, z1, false, z2)) BUSY(BF, closed, up, z0, z1, z2, z3) -> c27(IDLE(F, closed, up, z0, z1, z2, z3)) BUSY(BF, closed, down, z0, z1, z2, z3) -> c28(IDLE(B, closed, down, z0, z1, z2, z3)) BUSY(FS, closed, up, z0, z1, z2, z3) -> c29(IDLE(S, closed, up, z0, z1, z2, z3)) BUSY(FS, closed, down, z0, z1, z2, z3) -> c30(IDLE(F, closed, down, z0, z1, z2, z3)) BUSY(B, closed, stop, false, true, z0, z1) -> c31(IDLE(B, closed, up, false, true, z0, z1)) BUSY(B, closed, stop, false, false, true, z0) -> c32(IDLE(B, closed, up, false, false, true, z0)) BUSY(F, closed, stop, true, false, z0, z1) -> c33(IDLE(F, closed, down, true, false, z0, z1)) BUSY(F, closed, stop, false, false, true, z0) -> c34(IDLE(F, closed, up, false, false, true, z0)) BUSY(S, closed, stop, z0, true, false, z1) -> c35(IDLE(S, closed, down, z0, true, false, z1)) BUSY(S, closed, stop, true, false, false, z0) -> c36(IDLE(S, closed, down, true, false, false, z0)) IDLE(z0, z1, z2, z3, z4, z5, empty) -> c37(BUSY(z0, z1, z2, z3, z4, z5, empty)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c38(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z3, z6)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c39(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z4, z7)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c40(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z5, z8)) OR(true, z0) -> c41 OR(false, z0) -> c42 The (relative) TRS S consists of the following rules: start(z0) -> busy(F, closed, stop, false, false, false, z0) busy(BF, z0, stop, z1, z2, z3, z4) -> incorrect busy(FS, z0, stop, z1, z2, z3, z4) -> incorrect busy(z0, open, up, z1, z2, z3, z4) -> incorrect busy(z0, open, down, z1, z2, z3, z4) -> incorrect busy(B, closed, stop, false, false, false, empty) -> correct busy(F, closed, stop, false, false, false, empty) -> correct busy(S, closed, stop, false, false, false, empty) -> correct busy(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(B, open, stop, false, z0, z1, z2) -> idle(B, closed, stop, false, z0, z1, z2) busy(F, open, stop, z0, false, z1, z2) -> idle(F, closed, stop, z0, false, z1, z2) busy(S, open, stop, z0, z1, false, z2) -> idle(S, closed, stop, z0, z1, false, z2) busy(B, z0, stop, true, z1, z2, z3) -> idle(B, open, stop, false, z1, z2, z3) busy(F, z0, stop, z1, true, z2, z3) -> idle(F, open, stop, z1, false, z2, z3) busy(S, z0, stop, z1, z2, true, z3) -> idle(S, open, stop, z1, z2, false, z3) busy(B, closed, down, z0, z1, z2, z3) -> idle(B, closed, stop, z0, z1, z2, z3) busy(S, closed, up, z0, z1, z2, z3) -> idle(S, closed, stop, z0, z1, z2, z3) busy(B, closed, up, true, z0, z1, z2) -> idle(B, closed, stop, true, z0, z1, z2) busy(F, closed, up, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(F, closed, down, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(S, closed, down, z0, z1, true, z2) -> idle(S, closed, stop, z0, z1, true, z2) busy(B, closed, up, false, z0, z1, z2) -> idle(BF, closed, up, false, z0, z1, z2) busy(F, closed, up, z0, false, z1, z2) -> idle(FS, closed, up, z0, false, z1, z2) busy(F, closed, down, z0, false, z1, z2) -> idle(BF, closed, down, z0, false, z1, z2) busy(S, closed, down, z0, z1, false, z2) -> idle(FS, closed, down, z0, z1, false, z2) busy(BF, closed, up, z0, z1, z2, z3) -> idle(F, closed, up, z0, z1, z2, z3) busy(BF, closed, down, z0, z1, z2, z3) -> idle(B, closed, down, z0, z1, z2, z3) busy(FS, closed, up, z0, z1, z2, z3) -> idle(S, closed, up, z0, z1, z2, z3) busy(FS, closed, down, z0, z1, z2, z3) -> idle(F, closed, down, z0, z1, z2, z3) busy(B, closed, stop, false, true, z0, z1) -> idle(B, closed, up, false, true, z0, z1) busy(B, closed, stop, false, false, true, z0) -> idle(B, closed, up, false, false, true, z0) busy(F, closed, stop, true, false, z0, z1) -> idle(F, closed, down, true, false, z0, z1) busy(F, closed, stop, false, false, true, z0) -> idle(F, closed, up, false, false, true, z0) busy(S, closed, stop, z0, true, false, z1) -> idle(S, closed, down, z0, true, false, z1) busy(S, closed, stop, true, false, false, z0) -> idle(S, closed, down, true, false, false, z0) idle(z0, z1, z2, z3, z4, z5, empty) -> busy(z0, z1, z2, z3, z4, z5, empty) idle(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> busy(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9) or(true, z0) -> true or(false, z0) -> z0 Rewrite Strategy: INNERMOST ---------------------------------------- (8) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (9) BOUNDS(n^1, INF) ---------------------------------------- (10) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: START(z0) -> c(BUSY(F, closed, stop, false, false, false, z0)) BUSY(BF, z0, stop, z1, z2, z3, z4) -> c1 BUSY(FS, z0, stop, z1, z2, z3, z4) -> c2 BUSY(z0, open, up, z1, z2, z3, z4) -> c3 BUSY(z0, open, down, z1, z2, z3, z4) -> c4 BUSY(B, closed, stop, false, false, false, empty) -> c5 BUSY(F, closed, stop, false, false, false, empty) -> c6 BUSY(S, closed, stop, false, false, false, empty) -> c7 BUSY(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c8(IDLE(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c9(IDLE(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> c10(IDLE(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3))) BUSY(B, open, stop, false, z0, z1, z2) -> c11(IDLE(B, closed, stop, false, z0, z1, z2)) BUSY(F, open, stop, z0, false, z1, z2) -> c12(IDLE(F, closed, stop, z0, false, z1, z2)) BUSY(S, open, stop, z0, z1, false, z2) -> c13(IDLE(S, closed, stop, z0, z1, false, z2)) BUSY(B, z0, stop, true, z1, z2, z3) -> c14(IDLE(B, open, stop, false, z1, z2, z3)) BUSY(F, z0, stop, z1, true, z2, z3) -> c15(IDLE(F, open, stop, z1, false, z2, z3)) BUSY(S, z0, stop, z1, z2, true, z3) -> c16(IDLE(S, open, stop, z1, z2, false, z3)) BUSY(B, closed, down, z0, z1, z2, z3) -> c17(IDLE(B, closed, stop, z0, z1, z2, z3)) BUSY(S, closed, up, z0, z1, z2, z3) -> c18(IDLE(S, closed, stop, z0, z1, z2, z3)) BUSY(B, closed, up, true, z0, z1, z2) -> c19(IDLE(B, closed, stop, true, z0, z1, z2)) BUSY(F, closed, up, z0, true, z1, z2) -> c20(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(F, closed, down, z0, true, z1, z2) -> c21(IDLE(F, closed, stop, z0, true, z1, z2)) BUSY(S, closed, down, z0, z1, true, z2) -> c22(IDLE(S, closed, stop, z0, z1, true, z2)) BUSY(B, closed, up, false, z0, z1, z2) -> c23(IDLE(BF, closed, up, false, z0, z1, z2)) BUSY(F, closed, up, z0, false, z1, z2) -> c24(IDLE(FS, closed, up, z0, false, z1, z2)) BUSY(F, closed, down, z0, false, z1, z2) -> c25(IDLE(BF, closed, down, z0, false, z1, z2)) BUSY(S, closed, down, z0, z1, false, z2) -> c26(IDLE(FS, closed, down, z0, z1, false, z2)) BUSY(BF, closed, up, z0, z1, z2, z3) -> c27(IDLE(F, closed, up, z0, z1, z2, z3)) BUSY(BF, closed, down, z0, z1, z2, z3) -> c28(IDLE(B, closed, down, z0, z1, z2, z3)) BUSY(FS, closed, up, z0, z1, z2, z3) -> c29(IDLE(S, closed, up, z0, z1, z2, z3)) BUSY(FS, closed, down, z0, z1, z2, z3) -> c30(IDLE(F, closed, down, z0, z1, z2, z3)) BUSY(B, closed, stop, false, true, z0, z1) -> c31(IDLE(B, closed, up, false, true, z0, z1)) BUSY(B, closed, stop, false, false, true, z0) -> c32(IDLE(B, closed, up, false, false, true, z0)) BUSY(F, closed, stop, true, false, z0, z1) -> c33(IDLE(F, closed, down, true, false, z0, z1)) BUSY(F, closed, stop, false, false, true, z0) -> c34(IDLE(F, closed, up, false, false, true, z0)) BUSY(S, closed, stop, z0, true, false, z1) -> c35(IDLE(S, closed, down, z0, true, false, z1)) BUSY(S, closed, stop, true, false, false, z0) -> c36(IDLE(S, closed, down, true, false, false, z0)) IDLE(z0, z1, z2, z3, z4, z5, empty) -> c37(BUSY(z0, z1, z2, z3, z4, z5, empty)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c38(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z3, z6)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c39(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z4, z7)) IDLE(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> c40(BUSY(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9), OR(z5, z8)) OR(true, z0) -> c41 OR(false, z0) -> c42 The (relative) TRS S consists of the following rules: start(z0) -> busy(F, closed, stop, false, false, false, z0) busy(BF, z0, stop, z1, z2, z3, z4) -> incorrect busy(FS, z0, stop, z1, z2, z3, z4) -> incorrect busy(z0, open, up, z1, z2, z3, z4) -> incorrect busy(z0, open, down, z1, z2, z3, z4) -> incorrect busy(B, closed, stop, false, false, false, empty) -> correct busy(F, closed, stop, false, false, false, empty) -> correct busy(S, closed, stop, false, false, false, empty) -> correct busy(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(B, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(F, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) -> idle(S, closed, stop, false, false, false, newbuttons(z0, z1, z2, z3)) busy(B, open, stop, false, z0, z1, z2) -> idle(B, closed, stop, false, z0, z1, z2) busy(F, open, stop, z0, false, z1, z2) -> idle(F, closed, stop, z0, false, z1, z2) busy(S, open, stop, z0, z1, false, z2) -> idle(S, closed, stop, z0, z1, false, z2) busy(B, z0, stop, true, z1, z2, z3) -> idle(B, open, stop, false, z1, z2, z3) busy(F, z0, stop, z1, true, z2, z3) -> idle(F, open, stop, z1, false, z2, z3) busy(S, z0, stop, z1, z2, true, z3) -> idle(S, open, stop, z1, z2, false, z3) busy(B, closed, down, z0, z1, z2, z3) -> idle(B, closed, stop, z0, z1, z2, z3) busy(S, closed, up, z0, z1, z2, z3) -> idle(S, closed, stop, z0, z1, z2, z3) busy(B, closed, up, true, z0, z1, z2) -> idle(B, closed, stop, true, z0, z1, z2) busy(F, closed, up, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(F, closed, down, z0, true, z1, z2) -> idle(F, closed, stop, z0, true, z1, z2) busy(S, closed, down, z0, z1, true, z2) -> idle(S, closed, stop, z0, z1, true, z2) busy(B, closed, up, false, z0, z1, z2) -> idle(BF, closed, up, false, z0, z1, z2) busy(F, closed, up, z0, false, z1, z2) -> idle(FS, closed, up, z0, false, z1, z2) busy(F, closed, down, z0, false, z1, z2) -> idle(BF, closed, down, z0, false, z1, z2) busy(S, closed, down, z0, z1, false, z2) -> idle(FS, closed, down, z0, z1, false, z2) busy(BF, closed, up, z0, z1, z2, z3) -> idle(F, closed, up, z0, z1, z2, z3) busy(BF, closed, down, z0, z1, z2, z3) -> idle(B, closed, down, z0, z1, z2, z3) busy(FS, closed, up, z0, z1, z2, z3) -> idle(S, closed, up, z0, z1, z2, z3) busy(FS, closed, down, z0, z1, z2, z3) -> idle(F, closed, down, z0, z1, z2, z3) busy(B, closed, stop, false, true, z0, z1) -> idle(B, closed, up, false, true, z0, z1) busy(B, closed, stop, false, false, true, z0) -> idle(B, closed, up, false, false, true, z0) busy(F, closed, stop, true, false, z0, z1) -> idle(F, closed, down, true, false, z0, z1) busy(F, closed, stop, false, false, true, z0) -> idle(F, closed, up, false, false, true, z0) busy(S, closed, stop, z0, true, false, z1) -> idle(S, closed, down, z0, true, false, z1) busy(S, closed, stop, true, false, false, z0) -> idle(S, closed, down, true, false, false, z0) idle(z0, z1, z2, z3, z4, z5, empty) -> busy(z0, z1, z2, z3, z4, z5, empty) idle(z0, z1, z2, z3, z4, z5, newbuttons(z6, z7, z8, z9)) -> busy(z0, z1, z2, or(z3, z6), or(z4, z7), or(z5, z8), z9) or(true, z0) -> true or(false, z0) -> z0 Rewrite Strategy: INNERMOST