* Step 1: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: and(not(not(x)),y,not(z)) -> and(y,band(x,z),x) - Signature: {and/3} / {band/2,not/1} - Obligation: runtime complexity wrt. defined symbols {and} and constructors {band,not} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following weak dependency pairs: Strict DPs and#(not(not(x)),y,not(z)) -> c_1(and#(y,band(x,z),x)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: and#(not(not(x)),y,not(z)) -> c_1(and#(y,band(x,z),x)) - Strict TRS: and(not(not(x)),y,not(z)) -> and(y,band(x,z),x) - Signature: {and/3,and#/3} / {band/2,not/1,c_1/1} - Obligation: runtime complexity wrt. defined symbols {and#} and constructors {band,not} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: and#(not(not(x)),y,not(z)) -> c_1(and#(y,band(x,z),x)) * Step 3: WeightGap WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: and#(not(not(x)),y,not(z)) -> c_1(and#(y,band(x,z),x)) - Signature: {and/3,and#/3} / {band/2,not/1,c_1/1} - Obligation: runtime complexity wrt. defined symbols {and#} and constructors {band,not} + 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: uargs(c_1) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(and) = [4] x1 + [2] x2 + [1] x3 + [4] p(band) = [0] p(not) = [1] p(and#) = [1] x1 + [2] x2 + [0] p(c_1) = [1] x1 + [0] Following rules are strictly oriented: and#(not(not(x)),y,not(z)) = [2] y + [1] > [1] y + [0] = c_1(and#(y,band(x,z),x)) Following rules are (at-least) weakly oriented: Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: and#(not(not(x)),y,not(z)) -> c_1(and#(y,band(x,z),x)) - Signature: {and/3,and#/3} / {band/2,not/1,c_1/1} - Obligation: runtime complexity wrt. defined symbols {and#} and constructors {band,not} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))