WORST_CASE(?,O(n^2)) * Step 1: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(cons(x,xs),ys) -> cons(x,append(xs,ys)) append(nil(),ys) -> ys attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys)) attach(x,nil()) -> nil() pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs)) pairs(nil()) -> nil() - Signature: {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(append) = {1,2}, uargs(cons) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(append) = [1] x1 + [1] x2 + [0] p(attach) = [0] p(cons) = [1] x2 + [0] p(nil) = [0] p(pair) = [1] x1 + [1] x2 + [0] p(pairs) = [15] Following rules are strictly oriented: pairs(nil()) = [15] > [0] = nil() Following rules are (at-least) weakly oriented: append(cons(x,xs),ys) = [1] xs + [1] ys + [0] >= [1] xs + [1] ys + [0] = cons(x,append(xs,ys)) append(nil(),ys) = [1] ys + [0] >= [1] ys + [0] = ys attach(x,cons(y,ys)) = [0] >= [0] = cons(pair(x,y),attach(x,ys)) attach(x,nil()) = [0] >= [0] = nil() pairs(cons(x,xs)) = [15] >= [15] = append(attach(x,xs),pairs(xs)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(cons(x,xs),ys) -> cons(x,append(xs,ys)) append(nil(),ys) -> ys attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys)) attach(x,nil()) -> nil() pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs)) - Weak TRS: pairs(nil()) -> nil() - Signature: {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(append) = {1,2}, uargs(cons) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(append) = [1] x1 + [1] x2 + [10] p(attach) = [8] p(cons) = [1] x2 + [0] p(nil) = [0] p(pair) = [1] x1 + [1] p(pairs) = [1] Following rules are strictly oriented: append(nil(),ys) = [1] ys + [10] > [1] ys + [0] = ys attach(x,nil()) = [8] > [0] = nil() Following rules are (at-least) weakly oriented: append(cons(x,xs),ys) = [1] xs + [1] ys + [10] >= [1] xs + [1] ys + [10] = cons(x,append(xs,ys)) attach(x,cons(y,ys)) = [8] >= [8] = cons(pair(x,y),attach(x,ys)) pairs(cons(x,xs)) = [1] >= [19] = append(attach(x,xs),pairs(xs)) pairs(nil()) = [1] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(cons(x,xs),ys) -> cons(x,append(xs,ys)) attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys)) pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs)) - Weak TRS: append(nil(),ys) -> ys attach(x,nil()) -> nil() pairs(nil()) -> nil() - Signature: {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(append) = {1,2}, uargs(cons) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(append) = [1] x1 + [1] x2 + [0] p(attach) = [0] p(cons) = [1] x2 + [9] p(nil) = [0] p(pair) = [1] x2 + [1] p(pairs) = [1] x1 + [4] Following rules are strictly oriented: pairs(cons(x,xs)) = [1] xs + [13] > [1] xs + [4] = append(attach(x,xs),pairs(xs)) Following rules are (at-least) weakly oriented: append(cons(x,xs),ys) = [1] xs + [1] ys + [9] >= [1] xs + [1] ys + [9] = cons(x,append(xs,ys)) append(nil(),ys) = [1] ys + [0] >= [1] ys + [0] = ys attach(x,cons(y,ys)) = [0] >= [9] = cons(pair(x,y),attach(x,ys)) attach(x,nil()) = [0] >= [0] = nil() pairs(nil()) = [4] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(cons(x,xs),ys) -> cons(x,append(xs,ys)) attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys)) - Weak TRS: append(nil(),ys) -> ys attach(x,nil()) -> nil() pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs)) pairs(nil()) -> nil() - Signature: {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(append) = {1,2}, uargs(cons) = {2} Following symbols are considered usable: {append,attach,pairs} TcT has computed the following interpretation: p(append) = x1 + x2 p(attach) = 3*x2 p(cons) = 1 + x2 p(nil) = 2 p(pair) = 1 p(pairs) = 2*x1 + 2*x1^2 Following rules are strictly oriented: attach(x,cons(y,ys)) = 3 + 3*ys > 1 + 3*ys = cons(pair(x,y),attach(x,ys)) Following rules are (at-least) weakly oriented: append(cons(x,xs),ys) = 1 + xs + ys >= 1 + xs + ys = cons(x,append(xs,ys)) append(nil(),ys) = 2 + ys >= ys = ys attach(x,nil()) = 6 >= 2 = nil() pairs(cons(x,xs)) = 4 + 6*xs + 2*xs^2 >= 5*xs + 2*xs^2 = append(attach(x,xs),pairs(xs)) pairs(nil()) = 12 >= 2 = nil() * Step 5: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append(cons(x,xs),ys) -> cons(x,append(xs,ys)) - Weak TRS: append(nil(),ys) -> ys attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys)) attach(x,nil()) -> nil() pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs)) pairs(nil()) -> nil() - Signature: {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(append) = {1,2}, uargs(cons) = {2} Following symbols are considered usable: {append,attach,pairs} TcT has computed the following interpretation: p(append) = 1 + 4*x1 + x2 p(attach) = x2 p(cons) = 2 + x2 p(nil) = 0 p(pair) = x1 p(pairs) = 2*x1 + 2*x1^2 Following rules are strictly oriented: append(cons(x,xs),ys) = 9 + 4*xs + ys > 3 + 4*xs + ys = cons(x,append(xs,ys)) Following rules are (at-least) weakly oriented: append(nil(),ys) = 1 + ys >= ys = ys attach(x,cons(y,ys)) = 2 + ys >= 2 + ys = cons(pair(x,y),attach(x,ys)) attach(x,nil()) = 0 >= 0 = nil() pairs(cons(x,xs)) = 12 + 10*xs + 2*xs^2 >= 1 + 6*xs + 2*xs^2 = append(attach(x,xs),pairs(xs)) pairs(nil()) = 0 >= 0 = nil() * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: append(cons(x,xs),ys) -> cons(x,append(xs,ys)) append(nil(),ys) -> ys attach(x,cons(y,ys)) -> cons(pair(x,y),attach(x,ys)) attach(x,nil()) -> nil() pairs(cons(x,xs)) -> append(attach(x,xs),pairs(xs)) pairs(nil()) -> nil() - Signature: {append/2,attach/2,pairs/1} / {cons/2,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {append,attach,pairs} and constructors {cons,nil,pair} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))