MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__p(X) -> p(X) , a__p(0()) -> 0() , a__p(s(X)) -> mark(X) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(diff(X1, X2)) -> a__diff(mark(X1), mark(X2)) , mark(p(X)) -> a__p(mark(X)) , mark(leq(X1, X2)) -> a__leq(mark(X1), mark(X2)) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__leq(X1, X2) -> leq(X1, X2) , a__leq(0(), Y) -> true() , a__leq(s(X), 0()) -> false() , a__leq(s(X), s(Y)) -> a__leq(mark(X), mark(Y)) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__diff(X, Y) -> a__if(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))) , a__diff(X1, X2) -> diff(X1, X2) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { a__p^#(X) -> c_1() , a__p^#(0()) -> c_2() , a__p^#(s(X)) -> c_3(mark^#(X)) , mark^#(0()) -> c_4() , mark^#(s(X)) -> c_5(mark^#(X)) , mark^#(true()) -> c_6() , mark^#(false()) -> c_7() , mark^#(diff(X1, X2)) -> c_8(a__diff^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(p(X)) -> c_9(a__p^#(mark(X)), mark^#(X)) , mark^#(leq(X1, X2)) -> c_10(a__leq^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(if(X1, X2, X3)) -> c_11(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__diff^#(X, Y) -> c_19(a__if^#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))), a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__diff^#(X1, X2) -> c_20() , a__leq^#(X1, X2) -> c_12() , a__leq^#(0(), Y) -> c_13() , a__leq^#(s(X), 0()) -> c_14() , a__leq^#(s(X), s(Y)) -> c_15(a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__if^#(X1, X2, X3) -> c_16() , a__if^#(true(), X, Y) -> c_17(mark^#(X)) , a__if^#(false(), X, Y) -> c_18(mark^#(Y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__p^#(X) -> c_1() , a__p^#(0()) -> c_2() , a__p^#(s(X)) -> c_3(mark^#(X)) , mark^#(0()) -> c_4() , mark^#(s(X)) -> c_5(mark^#(X)) , mark^#(true()) -> c_6() , mark^#(false()) -> c_7() , mark^#(diff(X1, X2)) -> c_8(a__diff^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(p(X)) -> c_9(a__p^#(mark(X)), mark^#(X)) , mark^#(leq(X1, X2)) -> c_10(a__leq^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(if(X1, X2, X3)) -> c_11(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__diff^#(X, Y) -> c_19(a__if^#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))), a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__diff^#(X1, X2) -> c_20() , a__leq^#(X1, X2) -> c_12() , a__leq^#(0(), Y) -> c_13() , a__leq^#(s(X), 0()) -> c_14() , a__leq^#(s(X), s(Y)) -> c_15(a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__if^#(X1, X2, X3) -> c_16() , a__if^#(true(), X, Y) -> c_17(mark^#(X)) , a__if^#(false(), X, Y) -> c_18(mark^#(Y)) } Weak Trs: { a__p(X) -> p(X) , a__p(0()) -> 0() , a__p(s(X)) -> mark(X) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(diff(X1, X2)) -> a__diff(mark(X1), mark(X2)) , mark(p(X)) -> a__p(mark(X)) , mark(leq(X1, X2)) -> a__leq(mark(X1), mark(X2)) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__leq(X1, X2) -> leq(X1, X2) , a__leq(0(), Y) -> true() , a__leq(s(X), 0()) -> false() , a__leq(s(X), s(Y)) -> a__leq(mark(X), mark(Y)) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__diff(X, Y) -> a__if(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))) , a__diff(X1, X2) -> diff(X1, X2) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,6,7,13,14,15,16,18} by applications of Pre({1,2,4,6,7,13,14,15,16,18}) = {3,5,8,9,10,11,12,17,19,20}. Here rules are labeled as follows: DPs: { 1: a__p^#(X) -> c_1() , 2: a__p^#(0()) -> c_2() , 3: a__p^#(s(X)) -> c_3(mark^#(X)) , 4: mark^#(0()) -> c_4() , 5: mark^#(s(X)) -> c_5(mark^#(X)) , 6: mark^#(true()) -> c_6() , 7: mark^#(false()) -> c_7() , 8: mark^#(diff(X1, X2)) -> c_8(a__diff^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , 9: mark^#(p(X)) -> c_9(a__p^#(mark(X)), mark^#(X)) , 10: mark^#(leq(X1, X2)) -> c_10(a__leq^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , 11: mark^#(if(X1, X2, X3)) -> c_11(a__if^#(mark(X1), X2, X3), mark^#(X1)) , 12: a__diff^#(X, Y) -> c_19(a__if^#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))), a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , 13: a__diff^#(X1, X2) -> c_20() , 14: a__leq^#(X1, X2) -> c_12() , 15: a__leq^#(0(), Y) -> c_13() , 16: a__leq^#(s(X), 0()) -> c_14() , 17: a__leq^#(s(X), s(Y)) -> c_15(a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , 18: a__if^#(X1, X2, X3) -> c_16() , 19: a__if^#(true(), X, Y) -> c_17(mark^#(X)) , 20: a__if^#(false(), X, Y) -> c_18(mark^#(Y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__p^#(s(X)) -> c_3(mark^#(X)) , mark^#(s(X)) -> c_5(mark^#(X)) , mark^#(diff(X1, X2)) -> c_8(a__diff^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(p(X)) -> c_9(a__p^#(mark(X)), mark^#(X)) , mark^#(leq(X1, X2)) -> c_10(a__leq^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(if(X1, X2, X3)) -> c_11(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__diff^#(X, Y) -> c_19(a__if^#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))), a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__leq^#(s(X), s(Y)) -> c_15(a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__if^#(true(), X, Y) -> c_17(mark^#(X)) , a__if^#(false(), X, Y) -> c_18(mark^#(Y)) } Weak DPs: { a__p^#(X) -> c_1() , a__p^#(0()) -> c_2() , mark^#(0()) -> c_4() , mark^#(true()) -> c_6() , mark^#(false()) -> c_7() , a__diff^#(X1, X2) -> c_20() , a__leq^#(X1, X2) -> c_12() , a__leq^#(0(), Y) -> c_13() , a__leq^#(s(X), 0()) -> c_14() , a__if^#(X1, X2, X3) -> c_16() } Weak Trs: { a__p(X) -> p(X) , a__p(0()) -> 0() , a__p(s(X)) -> mark(X) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(diff(X1, X2)) -> a__diff(mark(X1), mark(X2)) , mark(p(X)) -> a__p(mark(X)) , mark(leq(X1, X2)) -> a__leq(mark(X1), mark(X2)) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__leq(X1, X2) -> leq(X1, X2) , a__leq(0(), Y) -> true() , a__leq(s(X), 0()) -> false() , a__leq(s(X), s(Y)) -> a__leq(mark(X), mark(Y)) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__diff(X, Y) -> a__if(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))) , a__diff(X1, X2) -> diff(X1, X2) } 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. { a__p^#(X) -> c_1() , a__p^#(0()) -> c_2() , mark^#(0()) -> c_4() , mark^#(true()) -> c_6() , mark^#(false()) -> c_7() , a__diff^#(X1, X2) -> c_20() , a__leq^#(X1, X2) -> c_12() , a__leq^#(0(), Y) -> c_13() , a__leq^#(s(X), 0()) -> c_14() , a__if^#(X1, X2, X3) -> c_16() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__p^#(s(X)) -> c_3(mark^#(X)) , mark^#(s(X)) -> c_5(mark^#(X)) , mark^#(diff(X1, X2)) -> c_8(a__diff^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(p(X)) -> c_9(a__p^#(mark(X)), mark^#(X)) , mark^#(leq(X1, X2)) -> c_10(a__leq^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(if(X1, X2, X3)) -> c_11(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__diff^#(X, Y) -> c_19(a__if^#(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))), a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__leq^#(s(X), s(Y)) -> c_15(a__leq^#(mark(X), mark(Y)), mark^#(X), mark^#(Y)) , a__if^#(true(), X, Y) -> c_17(mark^#(X)) , a__if^#(false(), X, Y) -> c_18(mark^#(Y)) } Weak Trs: { a__p(X) -> p(X) , a__p(0()) -> 0() , a__p(s(X)) -> mark(X) , mark(0()) -> 0() , mark(s(X)) -> s(mark(X)) , mark(true()) -> true() , mark(false()) -> false() , mark(diff(X1, X2)) -> a__diff(mark(X1), mark(X2)) , mark(p(X)) -> a__p(mark(X)) , mark(leq(X1, X2)) -> a__leq(mark(X1), mark(X2)) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__leq(X1, X2) -> leq(X1, X2) , a__leq(0(), Y) -> true() , a__leq(s(X), 0()) -> false() , a__leq(s(X), s(Y)) -> a__leq(mark(X), mark(Y)) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__diff(X, Y) -> a__if(a__leq(mark(X), mark(Y)), 0(), s(diff(p(X), Y))) , a__diff(X1, X2) -> diff(X1, X2) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: Following exception was raised: stack overflow 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..