WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs 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: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs foldr#3#(x8,x12,Nil()) -> c_1() foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(x8,x12,Nil()) -> c_1() foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)) - 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,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {2,3,4}. Here rules are labelled as follows: 1: foldr#3#(x8,x12,Nil()) -> c_1() 2: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) 3: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) 4: main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)) - Weak DPs: foldr#3#(x8,x12,Nil()) -> c_1() - 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,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) -->_1 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_1 foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)):1 2:S:foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) -->_2 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_1 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_2 foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)):2 -->_1 foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)):1 3:S:main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)) -->_1 foldr#3#(x8,x12,Nil()) -> c_1():4 -->_1 foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)):2 4:W:foldr#3#(x8,x12,Nil()) -> c_1() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: foldr#3#(x8,x12,Nil()) -> c_1() * Step 4: RemoveHeads WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)) - 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,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) -->_1 foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)):1 2:S:foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) -->_2 foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2) ,foldr#3(lam2_ms(x3),Nil(),x1) ,x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)):2 -->_1 foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)):1 3:S:main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)) -->_1 foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2) ,foldr#3(lam2_ms(x3),Nil(),x1) ,x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)):2 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(3,main#(x2,x1) -> c_4(foldr#3#(lam2_ms(x2),Nil(),x1)))] * Step 5: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) - 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,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 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) foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) * Step 6: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) - 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) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) and a lower component foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) Further, following extension rules are added to the lower component. foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3#(lam2_ms(x3),Nil(),x1) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) - 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) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)) -->_2 foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam1_n(x2) ,foldr#3(lam2_ms(x3),Nil(),x1) ,x3) ,foldr#3#(lam2_ms(x3),Nil(),x1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam2_ms(x3),Nil(),x1)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam2_ms(x3),Nil(),x1)) - 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) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam2_ms(x3),Nil(),x1)) ** Step 6.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam2_ms(x3),Nil(),x1)) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/1,c_4/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 constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_3) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(Cons) = [1] x1 + [1] x2 + [3] p(Nil) = [0] p(Pair) = [1] x1 + [1] x2 + [0] p(foldr#3) = [0] p(lam1_n) = [1] x1 + [0] p(lam2_ms) = [1] x1 + [0] p(main) = [0] p(foldr#3#) = [6] x3 + [0] p(main#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] Following rules are strictly oriented: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) = [6] x1 + [6] x2 + [18] > [6] x1 + [0] = c_3(foldr#3#(lam2_ms(x3),Nil(),x1)) Following rules are (at-least) weakly oriented: Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> c_3(foldr#3#(lam2_ms(x3),Nil(),x1)) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/1,c_4/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). ** Step 6.b:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(foldr#3#(lam1_n(x24),x14,x6)) - Weak DPs: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3#(lam2_ms(x3),Nil(),x1) - 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) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {foldr#3#,main#} and constructors {Cons,Nil,Pair,lam1_n ,lam2_ms} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1} Following symbols are considered usable: {foldr#3#,main#} TcT has computed the following interpretation: p(Cons) = [1] x2 + [1] p(Nil) = [0] p(Pair) = [4] p(foldr#3) = [1] x1 + [1] x2 + [8] x3 + [7] p(lam1_n) = [0] p(lam2_ms) = [1] x1 + [2] p(main) = [1] x1 + [1] x2 + [0] p(foldr#3#) = [8] x1 + [2] x3 + [0] p(main#) = [1] p(c_1) = [2] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [4] Following rules are strictly oriented: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) = [2] x6 + [2] > [2] x6 + [0] = c_2(foldr#3#(lam1_n(x24),x14,x6)) Following rules are (at-least) weakly oriented: foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) = [2] x1 + [8] x3 + [18] >= [2] x3 + [0] = foldr#3#(lam1_n(x2),foldr#3(lam2_ms(x3),Nil(),x1),x3) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) = [2] x1 + [8] x3 + [18] >= [2] x1 + [8] x3 + [16] = foldr#3#(lam2_ms(x3),Nil(),x1) ** Step 6.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: foldr#3#(lam1_n(x24),x14,Cons(x32,x6)) -> c_2(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) foldr#3#(lam2_ms(x3),Nil(),Cons(x2,x1)) -> foldr#3#(lam2_ms(x3),Nil(),x1) - 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) - Signature: {foldr#3/3,main/2,foldr#3#/3,main#/2} / {Cons/2,Nil/0,Pair/2,lam1_n/1,lam2_ms/1,c_1/0,c_2/1,c_3/2,c_4/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))