YES(?,O(n^2)) Problem: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) Proof: Complexity Transformation Processor: strict: app(nil(),xs) -> nil() app(cons(x,xs),ys) -> cons(x,app(xs,ys)) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [cons](x0, x1) = x0 + x1, [app](x0, x1) = x0 + x1 + 1, [nil] = 1 orientation: app(nil(),xs) = xs + 2 >= 1 = nil() app(cons(x,xs),ys) = x + xs + ys + 1 >= x + xs + ys + 1 = cons(x,app(xs,ys)) problem: strict: app(cons(x,xs),ys) -> cons(x,app(xs,ys)) weak: app(nil(),xs) -> nil() Matrix Interpretation Processor: dimension: 2 max_matrix: [1 1] [0 1] interpretation: [1 1] [0] [cons](x0, x1) = [0 1]x0 + x1 + [1], [1 1] [1 0] [0] [app](x0, x1) = [0 1]x0 + [0 0]x1 + [1], [0] [nil] = [1] orientation: [1 2] [1 1] [1 0] [1] [1 1] [1 1] [1 0] [0] app(cons(x,xs),ys) = [0 1]x + [0 1]xs + [0 0]ys + [2] >= [0 1]x + [0 1]xs + [0 0]ys + [2] = cons(x,app(xs,ys)) [1 0] [1] [0] app(nil(),xs) = [0 0]xs + [2] >= [1] = nil() problem: strict: weak: app(cons(x,xs),ys) -> cons(x,app(xs,ys)) app(nil(),xs) -> nil() Qed