MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: BUSY(z0,open(),down(),z1,z2,z3,z4) -> c4() BUSY(z0,open(),up(),z1,z2,z3,z4) -> c3() BUSY(B(),z0,stop(),true(),z1,z2,z3) -> c14(IDLE(B(),open(),stop(),false(),z1,z2,z3)) BUSY(B(),closed(),down(),z0,z1,z2,z3) -> c17(IDLE(B(),closed(),stop(),z0,z1,z2,z3)) BUSY(B(),closed(),stop(),false(),false(),false(),empty()) -> c5() 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(B(),closed(),stop(),false(),false(),true(),z0) -> c32(IDLE(B() ,closed() ,up() ,false() ,false() ,true() ,z0)) BUSY(B(),closed(),stop(),false(),true(),z0,z1) -> c31(IDLE(B(),closed(),up(),false(),true(),z0,z1)) BUSY(B(),closed(),up(),false(),z0,z1,z2) -> c23(IDLE(BF(),closed(),up(),false(),z0,z1,z2)) BUSY(B(),closed(),up(),true(),z0,z1,z2) -> c19(IDLE(B(),closed(),stop(),true(),z0,z1,z2)) BUSY(B(),open(),stop(),false(),z0,z1,z2) -> c11(IDLE(B(),closed(),stop(),false(),z0,z1,z2)) BUSY(BF(),z0,stop(),z1,z2,z3,z4) -> c1() BUSY(BF(),closed(),down(),z0,z1,z2,z3) -> c28(IDLE(B(),closed(),down(),z0,z1,z2,z3)) BUSY(BF(),closed(),up(),z0,z1,z2,z3) -> c27(IDLE(F(),closed(),up(),z0,z1,z2,z3)) BUSY(F(),z0,stop(),z1,true(),z2,z3) -> c15(IDLE(F(),open(),stop(),z1,false(),z2,z3)) BUSY(F(),closed(),down(),z0,false(),z1,z2) -> c25(IDLE(BF(),closed(),down(),z0,false(),z1,z2)) BUSY(F(),closed(),down(),z0,true(),z1,z2) -> c21(IDLE(F(),closed(),stop(),z0,true(),z1,z2)) BUSY(F(),closed(),stop(),false(),false(),false(),empty()) -> c6() 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(F(),closed(),stop(),false(),false(),true(),z0) -> c34(IDLE(F() ,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(),up(),z0,false(),z1,z2) -> c24(IDLE(FS(),closed(),up(),z0,false(),z1,z2)) BUSY(F(),closed(),up(),z0,true(),z1,z2) -> c20(IDLE(F(),closed(),stop(),z0,true(),z1,z2)) BUSY(F(),open(),stop(),z0,false(),z1,z2) -> c12(IDLE(F(),closed(),stop(),z0,false(),z1,z2)) BUSY(FS(),z0,stop(),z1,z2,z3,z4) -> c2() BUSY(FS(),closed(),down(),z0,z1,z2,z3) -> c30(IDLE(F(),closed(),down(),z0,z1,z2,z3)) BUSY(FS(),closed(),up(),z0,z1,z2,z3) -> c29(IDLE(S(),closed(),up(),z0,z1,z2,z3)) BUSY(S(),z0,stop(),z1,z2,true(),z3) -> c16(IDLE(S(),open(),stop(),z1,z2,false(),z3)) BUSY(S(),closed(),down(),z0,z1,false(),z2) -> c26(IDLE(FS(),closed(),down(),z0,z1,false(),z2)) BUSY(S(),closed(),down(),z0,z1,true(),z2) -> c22(IDLE(S(),closed(),stop(),z0,z1,true(),z2)) BUSY(S(),closed(),stop(),z0,true(),false(),z1) -> c35(IDLE(S(),closed(),down(),z0,true(),false(),z1)) BUSY(S(),closed(),stop(),false(),false(),false(),empty()) -> c7() 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(S(),closed(),stop(),true(),false(),false(),z0) -> c36(IDLE(S() ,closed() ,down() ,true() ,false() ,false() ,z0)) BUSY(S(),closed(),up(),z0,z1,z2,z3) -> c18(IDLE(S(),closed(),stop(),z0,z1,z2,z3)) BUSY(S(),open(),stop(),z0,z1,false(),z2) -> c13(IDLE(S(),closed(),stop(),z0,z1,false(),z2)) 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(false(),z0) -> c42() OR(true(),z0) -> c41() START(z0) -> c(BUSY(F(),closed(),stop(),false(),false(),false(),z0)) - Weak TRS: busy(z0,open(),down(),z1,z2,z3,z4) -> incorrect() busy(z0,open(),up(),z1,z2,z3,z4) -> incorrect() busy(B(),z0,stop(),true(),z1,z2,z3) -> idle(B(),open(),stop(),false(),z1,z2,z3) busy(B(),closed(),down(),z0,z1,z2,z3) -> idle(B(),closed(),stop(),z0,z1,z2,z3) busy(B(),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(B(),closed(),stop(),false(),false(),true(),z0) -> idle(B(),closed(),up(),false(),false(),true(),z0) busy(B(),closed(),stop(),false(),true(),z0,z1) -> idle(B(),closed(),up(),false(),true(),z0,z1) busy(B(),closed(),up(),false(),z0,z1,z2) -> idle(BF(),closed(),up(),false(),z0,z1,z2) busy(B(),closed(),up(),true(),z0,z1,z2) -> idle(B(),closed(),stop(),true(),z0,z1,z2) busy(B(),open(),stop(),false(),z0,z1,z2) -> idle(B(),closed(),stop(),false(),z0,z1,z2) busy(BF(),z0,stop(),z1,z2,z3,z4) -> incorrect() busy(BF(),closed(),down(),z0,z1,z2,z3) -> idle(B(),closed(),down(),z0,z1,z2,z3) busy(BF(),closed(),up(),z0,z1,z2,z3) -> idle(F(),closed(),up(),z0,z1,z2,z3) busy(F(),z0,stop(),z1,true(),z2,z3) -> idle(F(),open(),stop(),z1,false(),z2,z3) busy(F(),closed(),down(),z0,false(),z1,z2) -> idle(BF(),closed(),down(),z0,false(),z1,z2) busy(F(),closed(),down(),z0,true(),z1,z2) -> idle(F(),closed(),stop(),z0,true(),z1,z2) busy(F(),closed(),stop(),false(),false(),false(),empty()) -> correct() 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(F(),closed(),stop(),false(),false(),true(),z0) -> idle(F(),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(),up(),z0,false(),z1,z2) -> idle(FS(),closed(),up(),z0,false(),z1,z2) busy(F(),closed(),up(),z0,true(),z1,z2) -> idle(F(),closed(),stop(),z0,true(),z1,z2) busy(F(),open(),stop(),z0,false(),z1,z2) -> idle(F(),closed(),stop(),z0,false(),z1,z2) busy(FS(),z0,stop(),z1,z2,z3,z4) -> incorrect() busy(FS(),closed(),down(),z0,z1,z2,z3) -> idle(F(),closed(),down(),z0,z1,z2,z3) busy(FS(),closed(),up(),z0,z1,z2,z3) -> idle(S(),closed(),up(),z0,z1,z2,z3) busy(S(),z0,stop(),z1,z2,true(),z3) -> idle(S(),open(),stop(),z1,z2,false(),z3) busy(S(),closed(),down(),z0,z1,false(),z2) -> idle(FS(),closed(),down(),z0,z1,false(),z2) busy(S(),closed(),down(),z0,z1,true(),z2) -> idle(S(),closed(),stop(),z0,z1,true(),z2) busy(S(),closed(),stop(),z0,true(),false(),z1) -> idle(S(),closed(),down(),z0,true(),false(),z1) busy(S(),closed(),stop(),false(),false(),false(),empty()) -> correct() 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(S(),closed(),stop(),true(),false(),false(),z0) -> idle(S(),closed(),down(),true(),false(),false(),z0) busy(S(),closed(),up(),z0,z1,z2,z3) -> idle(S(),closed(),stop(),z0,z1,z2,z3) busy(S(),open(),stop(),z0,z1,false(),z2) -> idle(S(),closed(),stop(),z0,z1,false(),z2) 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(false(),z0) -> z0 or(true(),z0) -> true() start(z0) -> busy(F(),closed(),stop(),false(),false(),false(),z0) - Signature: {BUSY/7,IDLE/7,OR/2,START/1,busy/7,idle/7,or/2,start/1} / {B/0,BF/0,F/0,FS/0,S/0,c/1,c1/0,c10/1,c11/1,c12/1 ,c13/1,c14/1,c15/1,c16/1,c17/1,c18/1,c19/1,c2/0,c20/1,c21/1,c22/1,c23/1,c24/1,c25/1,c26/1,c27/1,c28/1,c29/1 ,c3/0,c30/1,c31/1,c32/1,c33/1,c34/1,c35/1,c36/1,c37/1,c38/2,c39/2,c4/0,c40/2,c41/0,c42/0,c5/0,c6/0,c7/0,c8/1 ,c9/1,closed/0,correct/0,down/0,empty/0,false/0,incorrect/0,newbuttons/4,open/0,stop/0,true/0,up/0} - Obligation: innermost runtime complexity wrt. defined symbols {BUSY,IDLE,OR,START,busy,idle,or ,start} and constructors {B,BF,F,FS,S,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24 ,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c5,c6,c7,c8,c9,closed,correct ,down,empty,false,incorrect,newbuttons,open,stop,true,up} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: None MAYBE