YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { a__and(X1, X2) -> and(X1, X2) , a__and(true(), X) -> mark(X) , a__and(false(), Y) -> false() , mark(true()) -> true() , mark(false()) -> false() , mark(0()) -> 0() , mark(s(X)) -> s(X) , mark(add(X1, X2)) -> a__add(mark(X1), X2) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) , mark(from(X)) -> a__from(X) , mark(and(X1, X2)) -> a__and(mark(X1), X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__add(X1, X2) -> add(X1, X2) , a__add(0(), X) -> mark(X) , a__add(s(X), Y) -> s(add(X, Y)) , a__first(X1, X2) -> first(X1, X2) , a__first(0(), X) -> nil() , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , a__from(X) -> cons(X, from(s(X))) , a__from(X) -> from(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We add following dependency tuples: Strict DPs: { a__and^#(X1, X2) -> c_1() , a__and^#(true(), X) -> c_2(mark^#(X)) , a__and^#(false(), Y) -> c_3() , mark^#(true()) -> c_4() , mark^#(false()) -> c_5() , mark^#(0()) -> c_6() , mark^#(s(X)) -> c_7() , mark^#(add(X1, X2)) -> c_8(a__add^#(mark(X1), X2), mark^#(X1)) , mark^#(nil()) -> c_9() , mark^#(cons(X1, X2)) -> c_10() , mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_12(a__from^#(X)) , mark^#(and(X1, X2)) -> c_13(a__and^#(mark(X1), X2), mark^#(X1)) , mark^#(if(X1, X2, X3)) -> c_14(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__add^#(X1, X2) -> c_18() , a__add^#(0(), X) -> c_19(mark^#(X)) , a__add^#(s(X), Y) -> c_20() , a__first^#(X1, X2) -> c_21() , a__first^#(0(), X) -> c_22() , a__first^#(s(X), cons(Y, Z)) -> c_23() , a__from^#(X) -> c_24() , a__from^#(X) -> c_25() , a__if^#(X1, X2, X3) -> c_15() , a__if^#(true(), X, Y) -> c_16(mark^#(X)) , a__if^#(false(), X, Y) -> c_17(mark^#(Y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { a__and^#(X1, X2) -> c_1() , a__and^#(true(), X) -> c_2(mark^#(X)) , a__and^#(false(), Y) -> c_3() , mark^#(true()) -> c_4() , mark^#(false()) -> c_5() , mark^#(0()) -> c_6() , mark^#(s(X)) -> c_7() , mark^#(add(X1, X2)) -> c_8(a__add^#(mark(X1), X2), mark^#(X1)) , mark^#(nil()) -> c_9() , mark^#(cons(X1, X2)) -> c_10() , mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_12(a__from^#(X)) , mark^#(and(X1, X2)) -> c_13(a__and^#(mark(X1), X2), mark^#(X1)) , mark^#(if(X1, X2, X3)) -> c_14(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__add^#(X1, X2) -> c_18() , a__add^#(0(), X) -> c_19(mark^#(X)) , a__add^#(s(X), Y) -> c_20() , a__first^#(X1, X2) -> c_21() , a__first^#(0(), X) -> c_22() , a__first^#(s(X), cons(Y, Z)) -> c_23() , a__from^#(X) -> c_24() , a__from^#(X) -> c_25() , a__if^#(X1, X2, X3) -> c_15() , a__if^#(true(), X, Y) -> c_16(mark^#(X)) , a__if^#(false(), X, Y) -> c_17(mark^#(Y)) } Weak Trs: { a__and(X1, X2) -> and(X1, X2) , a__and(true(), X) -> mark(X) , a__and(false(), Y) -> false() , mark(true()) -> true() , mark(false()) -> false() , mark(0()) -> 0() , mark(s(X)) -> s(X) , mark(add(X1, X2)) -> a__add(mark(X1), X2) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) , mark(from(X)) -> a__from(X) , mark(and(X1, X2)) -> a__and(mark(X1), X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__add(X1, X2) -> add(X1, X2) , a__add(0(), X) -> mark(X) , a__add(s(X), Y) -> s(add(X, Y)) , a__first(X1, X2) -> first(X1, X2) , a__first(0(), X) -> nil() , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , a__from(X) -> cons(X, from(s(X))) , a__from(X) -> from(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We estimate the number of application of {1,3,4,5,6,7,9,10,15,17,18,19,20,21,22,23} by applications of Pre({1,3,4,5,6,7,9,10,15,17,18,19,20,21,22,23}) = {2,8,11,12,13,14,16,24,25}. Here rules are labeled as follows: DPs: { 1: a__and^#(X1, X2) -> c_1() , 2: a__and^#(true(), X) -> c_2(mark^#(X)) , 3: a__and^#(false(), Y) -> c_3() , 4: mark^#(true()) -> c_4() , 5: mark^#(false()) -> c_5() , 6: mark^#(0()) -> c_6() , 7: mark^#(s(X)) -> c_7() , 8: mark^#(add(X1, X2)) -> c_8(a__add^#(mark(X1), X2), mark^#(X1)) , 9: mark^#(nil()) -> c_9() , 10: mark^#(cons(X1, X2)) -> c_10() , 11: mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , 12: mark^#(from(X)) -> c_12(a__from^#(X)) , 13: mark^#(and(X1, X2)) -> c_13(a__and^#(mark(X1), X2), mark^#(X1)) , 14: mark^#(if(X1, X2, X3)) -> c_14(a__if^#(mark(X1), X2, X3), mark^#(X1)) , 15: a__add^#(X1, X2) -> c_18() , 16: a__add^#(0(), X) -> c_19(mark^#(X)) , 17: a__add^#(s(X), Y) -> c_20() , 18: a__first^#(X1, X2) -> c_21() , 19: a__first^#(0(), X) -> c_22() , 20: a__first^#(s(X), cons(Y, Z)) -> c_23() , 21: a__from^#(X) -> c_24() , 22: a__from^#(X) -> c_25() , 23: a__if^#(X1, X2, X3) -> c_15() , 24: a__if^#(true(), X, Y) -> c_16(mark^#(X)) , 25: a__if^#(false(), X, Y) -> c_17(mark^#(Y)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { a__and^#(true(), X) -> c_2(mark^#(X)) , mark^#(add(X1, X2)) -> c_8(a__add^#(mark(X1), X2), mark^#(X1)) , mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(from(X)) -> c_12(a__from^#(X)) , mark^#(and(X1, X2)) -> c_13(a__and^#(mark(X1), X2), mark^#(X1)) , mark^#(if(X1, X2, X3)) -> c_14(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__add^#(0(), X) -> c_19(mark^#(X)) , a__if^#(true(), X, Y) -> c_16(mark^#(X)) , a__if^#(false(), X, Y) -> c_17(mark^#(Y)) } Weak DPs: { a__and^#(X1, X2) -> c_1() , a__and^#(false(), Y) -> c_3() , mark^#(true()) -> c_4() , mark^#(false()) -> c_5() , mark^#(0()) -> c_6() , mark^#(s(X)) -> c_7() , mark^#(nil()) -> c_9() , mark^#(cons(X1, X2)) -> c_10() , a__add^#(X1, X2) -> c_18() , a__add^#(s(X), Y) -> c_20() , a__first^#(X1, X2) -> c_21() , a__first^#(0(), X) -> c_22() , a__first^#(s(X), cons(Y, Z)) -> c_23() , a__from^#(X) -> c_24() , a__from^#(X) -> c_25() , a__if^#(X1, X2, X3) -> c_15() } Weak Trs: { a__and(X1, X2) -> and(X1, X2) , a__and(true(), X) -> mark(X) , a__and(false(), Y) -> false() , mark(true()) -> true() , mark(false()) -> false() , mark(0()) -> 0() , mark(s(X)) -> s(X) , mark(add(X1, X2)) -> a__add(mark(X1), X2) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) , mark(from(X)) -> a__from(X) , mark(and(X1, X2)) -> a__and(mark(X1), X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__add(X1, X2) -> add(X1, X2) , a__add(0(), X) -> mark(X) , a__add(s(X), Y) -> s(add(X, Y)) , a__first(X1, X2) -> first(X1, X2) , a__first(0(), X) -> nil() , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , a__from(X) -> cons(X, from(s(X))) , a__from(X) -> from(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) We estimate the number of application of {4} by applications of Pre({4}) = {1,2,3,5,6,7,8,9}. Here rules are labeled as follows: DPs: { 1: a__and^#(true(), X) -> c_2(mark^#(X)) , 2: mark^#(add(X1, X2)) -> c_8(a__add^#(mark(X1), X2), mark^#(X1)) , 3: mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , 4: mark^#(from(X)) -> c_12(a__from^#(X)) , 5: mark^#(and(X1, X2)) -> c_13(a__and^#(mark(X1), X2), mark^#(X1)) , 6: mark^#(if(X1, X2, X3)) -> c_14(a__if^#(mark(X1), X2, X3), mark^#(X1)) , 7: a__add^#(0(), X) -> c_19(mark^#(X)) , 8: a__if^#(true(), X, Y) -> c_16(mark^#(X)) , 9: a__if^#(false(), X, Y) -> c_17(mark^#(Y)) , 10: a__and^#(X1, X2) -> c_1() , 11: a__and^#(false(), Y) -> c_3() , 12: mark^#(true()) -> c_4() , 13: mark^#(false()) -> c_5() , 14: mark^#(0()) -> c_6() , 15: mark^#(s(X)) -> c_7() , 16: mark^#(nil()) -> c_9() , 17: mark^#(cons(X1, X2)) -> c_10() , 18: a__add^#(X1, X2) -> c_18() , 19: a__add^#(s(X), Y) -> c_20() , 20: a__first^#(X1, X2) -> c_21() , 21: a__first^#(0(), X) -> c_22() , 22: a__first^#(s(X), cons(Y, Z)) -> c_23() , 23: a__from^#(X) -> c_24() , 24: a__from^#(X) -> c_25() , 25: a__if^#(X1, X2, X3) -> c_15() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { a__and^#(true(), X) -> c_2(mark^#(X)) , mark^#(add(X1, X2)) -> c_8(a__add^#(mark(X1), X2), mark^#(X1)) , mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(and(X1, X2)) -> c_13(a__and^#(mark(X1), X2), mark^#(X1)) , mark^#(if(X1, X2, X3)) -> c_14(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__add^#(0(), X) -> c_19(mark^#(X)) , a__if^#(true(), X, Y) -> c_16(mark^#(X)) , a__if^#(false(), X, Y) -> c_17(mark^#(Y)) } Weak DPs: { a__and^#(X1, X2) -> c_1() , a__and^#(false(), Y) -> c_3() , mark^#(true()) -> c_4() , mark^#(false()) -> c_5() , mark^#(0()) -> c_6() , mark^#(s(X)) -> c_7() , mark^#(nil()) -> c_9() , mark^#(cons(X1, X2)) -> c_10() , mark^#(from(X)) -> c_12(a__from^#(X)) , a__add^#(X1, X2) -> c_18() , a__add^#(s(X), Y) -> c_20() , a__first^#(X1, X2) -> c_21() , a__first^#(0(), X) -> c_22() , a__first^#(s(X), cons(Y, Z)) -> c_23() , a__from^#(X) -> c_24() , a__from^#(X) -> c_25() , a__if^#(X1, X2, X3) -> c_15() } Weak Trs: { a__and(X1, X2) -> and(X1, X2) , a__and(true(), X) -> mark(X) , a__and(false(), Y) -> false() , mark(true()) -> true() , mark(false()) -> false() , mark(0()) -> 0() , mark(s(X)) -> s(X) , mark(add(X1, X2)) -> a__add(mark(X1), X2) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) , mark(from(X)) -> a__from(X) , mark(and(X1, X2)) -> a__and(mark(X1), X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__add(X1, X2) -> add(X1, X2) , a__add(0(), X) -> mark(X) , a__add(s(X), Y) -> s(add(X, Y)) , a__first(X1, X2) -> first(X1, X2) , a__first(0(), X) -> nil() , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , a__from(X) -> cons(X, from(s(X))) , a__from(X) -> from(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { a__and^#(X1, X2) -> c_1() , a__and^#(false(), Y) -> c_3() , mark^#(true()) -> c_4() , mark^#(false()) -> c_5() , mark^#(0()) -> c_6() , mark^#(s(X)) -> c_7() , mark^#(nil()) -> c_9() , mark^#(cons(X1, X2)) -> c_10() , mark^#(from(X)) -> c_12(a__from^#(X)) , a__add^#(X1, X2) -> c_18() , a__add^#(s(X), Y) -> c_20() , a__first^#(X1, X2) -> c_21() , a__first^#(0(), X) -> c_22() , a__first^#(s(X), cons(Y, Z)) -> c_23() , a__from^#(X) -> c_24() , a__from^#(X) -> c_25() , a__if^#(X1, X2, X3) -> c_15() } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { a__and^#(true(), X) -> c_2(mark^#(X)) , mark^#(add(X1, X2)) -> c_8(a__add^#(mark(X1), X2), mark^#(X1)) , mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) , mark^#(and(X1, X2)) -> c_13(a__and^#(mark(X1), X2), mark^#(X1)) , mark^#(if(X1, X2, X3)) -> c_14(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__add^#(0(), X) -> c_19(mark^#(X)) , a__if^#(true(), X, Y) -> c_16(mark^#(X)) , a__if^#(false(), X, Y) -> c_17(mark^#(Y)) } Weak Trs: { a__and(X1, X2) -> and(X1, X2) , a__and(true(), X) -> mark(X) , a__and(false(), Y) -> false() , mark(true()) -> true() , mark(false()) -> false() , mark(0()) -> 0() , mark(s(X)) -> s(X) , mark(add(X1, X2)) -> a__add(mark(X1), X2) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) , mark(from(X)) -> a__from(X) , mark(and(X1, X2)) -> a__and(mark(X1), X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__add(X1, X2) -> add(X1, X2) , a__add(0(), X) -> mark(X) , a__add(s(X), Y) -> s(add(X, Y)) , a__first(X1, X2) -> first(X1, X2) , a__first(0(), X) -> nil() , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , a__from(X) -> cons(X, from(s(X))) , a__from(X) -> from(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { mark^#(first(X1, X2)) -> c_11(a__first^#(mark(X1), mark(X2)), mark^#(X1), mark^#(X2)) } We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict DPs: { a__and^#(true(), X) -> c_1(mark^#(X)) , mark^#(add(X1, X2)) -> c_2(a__add^#(mark(X1), X2), mark^#(X1)) , mark^#(first(X1, X2)) -> c_3(mark^#(X1), mark^#(X2)) , mark^#(and(X1, X2)) -> c_4(a__and^#(mark(X1), X2), mark^#(X1)) , mark^#(if(X1, X2, X3)) -> c_5(a__if^#(mark(X1), X2, X3), mark^#(X1)) , a__add^#(0(), X) -> c_6(mark^#(X)) , a__if^#(true(), X, Y) -> c_7(mark^#(X)) , a__if^#(false(), X, Y) -> c_8(mark^#(Y)) } Weak Trs: { a__and(X1, X2) -> and(X1, X2) , a__and(true(), X) -> mark(X) , a__and(false(), Y) -> false() , mark(true()) -> true() , mark(false()) -> false() , mark(0()) -> 0() , mark(s(X)) -> s(X) , mark(add(X1, X2)) -> a__add(mark(X1), X2) , mark(nil()) -> nil() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) , mark(from(X)) -> a__from(X) , mark(and(X1, X2)) -> a__and(mark(X1), X2) , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) , a__if(X1, X2, X3) -> if(X1, X2, X3) , a__if(true(), X, Y) -> mark(X) , a__if(false(), X, Y) -> mark(Y) , a__add(X1, X2) -> add(X1, X2) , a__add(0(), X) -> mark(X) , a__add(s(X), Y) -> s(add(X, Y)) , a__first(X1, X2) -> first(X1, X2) , a__first(0(), X) -> nil() , a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) , a__from(X) -> cons(X, from(s(X))) , a__from(X) -> from(X) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [a__and](x1, x2) = [3] x2 + [0] [true] = [0] [mark](x1) = [0] [false] = [0] [a__if](x1, x2, x3) = [3] x2 + [3] x3 + [0] [a__add](x1, x2) = [3] x2 + [0] [0] = [0] [s](x1) = [0] [add](x1, x2) = [1] x1 + [1] x2 + [3] [a__first](x1, x2) = [0] [nil] = [0] [cons](x1, x2) = [1] x1 + [0] [first](x1, x2) = [1] x1 + [1] x2 + [1] [a__from](x1) = [3] x1 + [0] [from](x1) = [1] x1 + [0] [and](x1, x2) = [1] x1 + [1] x2 + [2] [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [3] [a__and^#](x1, x2) = [1] x2 + [1] [mark^#](x1) = [1] x1 + [0] [a__add^#](x1, x2) = [1] x2 + [2] [a__if^#](x1, x2, x3) = [1] x2 + [1] x3 + [2] [c_1](x1) = [1] x1 + [0] [c_2](x1, x2) = [1] x1 + [1] x2 + [0] [c_3](x1, x2) = [1] x1 + [1] x2 + [0] [c_4](x1, x2) = [1] x1 + [1] x2 + [0] [c_5](x1, x2) = [1] x1 + [1] x2 + [0] [c_6](x1) = [1] x1 + [1] [c_7](x1) = [1] x1 + [1] [c_8](x1) = [1] x1 + [1] This order satisfies following ordering constraints: [a__and^#(true(), X)] = [1] X + [1] > [1] X + [0] = [c_1(mark^#(X))] [mark^#(add(X1, X2))] = [1] X1 + [1] X2 + [3] > [1] X1 + [1] X2 + [2] = [c_2(a__add^#(mark(X1), X2), mark^#(X1))] [mark^#(first(X1, X2))] = [1] X1 + [1] X2 + [1] > [1] X1 + [1] X2 + [0] = [c_3(mark^#(X1), mark^#(X2))] [mark^#(and(X1, X2))] = [1] X1 + [1] X2 + [2] > [1] X1 + [1] X2 + [1] = [c_4(a__and^#(mark(X1), X2), mark^#(X1))] [mark^#(if(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [3] > [1] X1 + [1] X2 + [1] X3 + [2] = [c_5(a__if^#(mark(X1), X2, X3), mark^#(X1))] [a__add^#(0(), X)] = [1] X + [2] > [1] X + [1] = [c_6(mark^#(X))] [a__if^#(true(), X, Y)] = [1] X + [1] Y + [2] > [1] X + [1] = [c_7(mark^#(X))] [a__if^#(false(), X, Y)] = [1] X + [1] Y + [2] > [1] Y + [1] = [c_8(mark^#(Y))] Hurray, we answered YES(?,O(n^1))