WORST_CASE(?,O(n^2)) * Step 1: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(lam1_n(x24),x14,Cons(x32,x6)) -> Cons(Pair(x24,x32),foldr#3(lam1_n(x24),x14,x6)) foldr#3(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) main(x2,x1) -> foldr#3(lam2_ms(x2),Nil(),x1) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3,main} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + 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(Cons) = {2}, uargs(foldr#3) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [0] p(Nil) = [0] p(Pair) = [12] p(foldr#3) = [4] x1 + [1] x2 + [6] p(lam1_n) = [0] p(lam2_ms) = [2] p(main) = [15] Following rules are strictly oriented: foldr#3(x8,x12,Nil()) = [1] x12 + [4] x8 + [6] > [1] x12 + [0] = x12 main(x2,x1) = [15] > [14] = foldr#3(lam2_ms(x2),Nil(),x1) Following rules are (at-least) weakly oriented: foldr#3(lam1_n(x24),x14,Cons(x32,x6)) = [1] x14 + [6] >= [1] x14 + [18] = Cons(Pair(x24,x32),foldr#3(lam1_n(x24),x14,x6)) foldr#3(lam2_ms(x3),Nil(),Cons(x2,x1)) = [14] >= [20] = foldr#3(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(lam1_n(x24),x14,Cons(x32,x6)) -> Cons(Pair(x24,x32),foldr#3(lam1_n(x24),x14,x6)) foldr#3(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 main(x2,x1) -> foldr#3(lam2_ms(x2),Nil(),x1) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3,main} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + 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(Cons) = {2}, uargs(foldr#3) = {2} Following symbols are considered usable: {foldr#3,main} TcT has computed the following interpretation: p(Cons) = 2 + x2 p(Nil) = 2 p(Pair) = 0 p(foldr#3) = x1*x3 + x2 p(lam1_n) = 1 p(lam2_ms) = 2 + x1 p(main) = 4 + 4*x1*x2 + x1^2 + 3*x2 Following rules are strictly oriented: foldr#3(lam2_ms(x3),Nil(),Cons(x2,x1)) = 6 + 2*x1 + x1*x3 + 2*x3 > 2 + 2*x1 + x1*x3 + x3 = foldr#3(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) Following rules are (at-least) weakly oriented: foldr#3(x8,x12,Nil()) = x12 + 2*x8 >= x12 = x12 foldr#3(lam1_n(x24),x14,Cons(x32,x6)) = 2 + x14 + x6 >= 2 + x14 + x6 = Cons(Pair(x24,x32),foldr#3(lam1_n(x24),x14,x6)) main(x2,x1) = 4 + 3*x1 + 4*x1*x2 + x2^2 >= 2 + 2*x1 + x1*x2 = foldr#3(lam2_ms(x2),Nil(),x1) * Step 3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(lam1_n(x24),x14,Cons(x32,x6)) -> Cons(Pair(x24,x32),foldr#3(lam1_n(x24),x14,x6)) - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) main(x2,x1) -> foldr#3(lam2_ms(x2),Nil(),x1) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3,main} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + 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(Cons) = {2}, uargs(foldr#3) = {2} Following symbols are considered usable: {foldr#3,main} TcT has computed the following interpretation: p(Cons) = 2 + x1 + x2 p(Nil) = 0 p(Pair) = 4 p(foldr#3) = 2*x1*x3 + x1^2 + x2 p(lam1_n) = 2 p(lam2_ms) = 1 + x1 p(main) = 1 + 5*x1 + 4*x1*x2 + 2*x1^2 + 2*x2 + x2^2 Following rules are strictly oriented: foldr#3(lam1_n(x24),x14,Cons(x32,x6)) = 12 + x14 + 4*x32 + 4*x6 > 10 + x14 + 4*x6 = Cons(Pair(x24,x32),foldr#3(lam1_n(x24),x14,x6)) Following rules are (at-least) weakly oriented: foldr#3(x8,x12,Nil()) = x12 + x8^2 >= x12 = x12 foldr#3(lam2_ms(x3),Nil(),Cons(x2,x1)) = 5 + 2*x1 + 2*x1*x3 + 2*x2 + 2*x2*x3 + 6*x3 + x3^2 >= 5 + 2*x1 + 2*x1*x3 + 6*x3 + x3^2 = foldr#3(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) main(x2,x1) = 1 + 2*x1 + 4*x1*x2 + x1^2 + 5*x2 + 2*x2^2 >= 1 + 2*x1 + 2*x1*x2 + 2*x2 + x2^2 = foldr#3(lam2_ms(x2),Nil(),x1) * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(lam1_n(x24),x14,Cons(x32,x6)) -> Cons(Pair(x24,x32),foldr#3(lam1_n(x24),x14,x6)) foldr#3(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) main(x2,x1) -> foldr#3(lam2_ms(x2),Nil(),x1) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3,main} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))