* Step 1: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1} / {a/0,b/0,s/1} - Obligation: runtime complexity wrt. defined symbols {cons,f,g} and constructors {a,b,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following weak dependency pairs: Strict DPs cons#(x,y) -> c_1(x) cons#(x,y) -> c_2(y) f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z))) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: cons#(x,y) -> c_1(x) cons#(x,y) -> c_2(y) f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z))) - Strict TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1} - Obligation: runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: cons#(x,y) -> c_1(x) cons#(x,y) -> c_2(y) f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) * Step 3: WeightGap WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: cons#(x,y) -> c_1(x) cons#(x,y) -> c_2(y) f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1} - Obligation: runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: none Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [0] p(cons) = [0] p(f) = [0] p(g) = [0] p(s) = [0] p(cons#) = [0] p(f#) = [15] p(g#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] Following rules are strictly oriented: f#(s(a()),s(b()),x) = [15] > [0] = c_3(f#(x,x,x)) Following rules are (at-least) weakly oriented: cons#(x,y) = [0] >= [0] = c_1(x) cons#(x,y) = [0] >= [0] = c_2(y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: cons#(x,y) -> c_1(x) cons#(x,y) -> c_2(y) - Weak DPs: f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1} - Obligation: runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: none Following symbols are considered usable: all TcT has computed the following interpretation: p(a) = [0] p(b) = [0] p(cons) = [0] p(f) = [0] p(g) = [0] p(s) = [11] p(cons#) = [1] p(f#) = [0] p(g#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] Following rules are strictly oriented: cons#(x,y) = [1] > [0] = c_1(x) cons#(x,y) = [1] > [0] = c_2(y) Following rules are (at-least) weakly oriented: f#(s(a()),s(b()),x) = [0] >= [0] = c_3(f#(x,x,x)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: cons#(x,y) -> c_1(x) cons#(x,y) -> c_2(y) f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1} - Obligation: runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))