WORST_CASE(?,O(n^1)) * Step 1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: goal(xs,ys) -> merge(xs,ys) merge(Cons(x,xs),Nil()) -> Cons(x,xs) merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs)) merge(Nil(),ys) -> ys - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs)) merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys)) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False ,Nil,S,True} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs goal#(xs,ys) -> c_1(merge#(xs,ys)) merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)) merge#(Nil(),ys) -> c_4() Weak DPs <=#(0(),y) -> c_5() <=#(S(x),0()) -> c_6() <=#(S(x),S(y)) -> c_7(<=#(x,y)) merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) and mark the set of starting terms. * Step 2: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(merge#(xs,ys)) merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)) merge#(Nil(),ys) -> c_4() - Weak DPs: <=#(0(),y) -> c_5() <=#(S(x),0()) -> c_6() <=#(S(x),S(y)) -> c_7(<=#(x,y)) merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) goal(xs,ys) -> merge(xs,ys) merge(Cons(x,xs),Nil()) -> Cons(x,xs) merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs)) merge(Nil(),ys) -> ys merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs)) merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys)) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3,<=#/2,goal#/2,merge#/2,merge[Ite]#/3} / {0/0,Cons/2,False/0,Nil/0,S/1 ,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#} and constructors {0,Cons ,False,Nil,S,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:goal#(xs,ys) -> c_1(merge#(xs,ys)) -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3 -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 2:S:merge#(Cons(x,xs),Nil()) -> c_2() 3:S:merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)) -->_1 merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)):9 -->_1 merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)):8 -->_2 <=#(S(x),S(y)) -> c_7(<=#(x,y)):7 -->_2 <=#(S(x),0()) -> c_6():6 -->_2 <=#(0(),y) -> c_5():5 4:S:merge#(Nil(),ys) -> c_4() 5:W:<=#(0(),y) -> c_5() 6:W:<=#(S(x),0()) -> c_6() 7:W:<=#(S(x),S(y)) -> c_7(<=#(x,y)) -->_1 <=#(S(x),S(y)) -> c_7(<=#(x,y)):7 -->_1 <=#(S(x),0()) -> c_6():6 -->_1 <=#(0(),y) -> c_5():5 8:W:merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 9:W:merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: <=#(S(x),S(y)) -> c_7(<=#(x,y)) 5: <=#(0(),y) -> c_5() 6: <=#(S(x),0()) -> c_6() * Step 3: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(merge#(xs,ys)) merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)) merge#(Nil(),ys) -> c_4() - Weak DPs: merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) goal(xs,ys) -> merge(xs,ys) merge(Cons(x,xs),Nil()) -> Cons(x,xs) merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs)) merge(Nil(),ys) -> ys merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs)) merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys)) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3,<=#/2,goal#/2,merge#/2,merge[Ite]#/3} / {0/0,Cons/2,False/0,Nil/0,S/1 ,True/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#} and constructors {0,Cons ,False,Nil,S,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:goal#(xs,ys) -> c_1(merge#(xs,ys)) -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3 -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 2:S:merge#(Cons(x,xs),Nil()) -> c_2() 3:S:merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)) -->_1 merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)):9 -->_1 merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)):8 4:S:merge#(Nil(),ys) -> c_4() 8:W:merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 9:W:merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs)),<=#(x',x)):3 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) * Step 4: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(merge#(xs,ys)) merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) merge#(Nil(),ys) -> c_4() - Weak DPs: merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) goal(xs,ys) -> merge(xs,ys) merge(Cons(x,xs),Nil()) -> Cons(x,xs) merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs)) merge(Nil(),ys) -> ys merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs)) merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys)) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3,<=#/2,goal#/2,merge#/2,merge[Ite]#/3} / {0/0,Cons/2,False/0,Nil/0,S/1 ,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#} and constructors {0,Cons ,False,Nil,S,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) goal#(xs,ys) -> c_1(merge#(xs,ys)) merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) merge#(Nil(),ys) -> c_4() merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) * Step 5: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: goal#(xs,ys) -> c_1(merge#(xs,ys)) merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) merge#(Nil(),ys) -> c_4() - Weak DPs: merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3,<=#/2,goal#/2,merge#/2,merge[Ite]#/3} / {0/0,Cons/2,False/0,Nil/0,S/1 ,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#} and constructors {0,Cons ,False,Nil,S,True} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:goal#(xs,ys) -> c_1(merge#(xs,ys)) -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))):3 -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 2:S:merge#(Cons(x,xs),Nil()) -> c_2() 3:S:merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) -->_1 merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)):6 -->_1 merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)):5 4:S:merge#(Nil(),ys) -> c_4() 5:W:merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))):3 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():2 6:W:merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) -->_1 merge#(Nil(),ys) -> c_4():4 -->_1 merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))):3 -->_1 merge#(Cons(x,xs),Nil()) -> c_2():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). [(1,goal#(xs,ys) -> c_1(merge#(xs,ys)))] * Step 6: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) merge#(Nil(),ys) -> c_4() - Weak DPs: merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3,<=#/2,goal#/2,merge#/2,merge[Ite]#/3} / {0/0,Cons/2,False/0,Nil/0,S/1 ,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#} and constructors {0,Cons ,False,Nil,S,True} + 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(merge[Ite]#) = {1}, uargs(c_3) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(<=) = [0] p(Cons) = [1] x1 + [1] x2 + [0] p(False) = [0] p(Nil) = [3] p(S) = [1] x1 + [0] p(True) = [0] p(goal) = [0] p(merge) = [0] p(merge[Ite]) = [0] p(<=#) = [0] p(goal#) = [0] p(merge#) = [6] x1 + [5] p(merge[Ite]#) = [1] x1 + [6] x2 + [7] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [1] p(c_6) = [2] p(c_7) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] x1 + [2] Following rules are strictly oriented: merge#(Cons(x,xs),Nil()) = [6] x + [6] xs + [5] > [0] = c_2() merge#(Nil(),ys) = [23] > [0] = c_4() Following rules are (at-least) weakly oriented: merge#(Cons(x',xs'),Cons(x,xs)) = [6] x' + [6] xs' + [5] >= [6] x' + [6] xs' + [7] = c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) merge[Ite]#(False(),xs',Cons(x,xs)) = [6] xs' + [7] >= [6] xs' + [5] = c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) = [6] x + [6] xs + [7] >= [6] xs + [7] = c_9(merge#(xs,ys)) <=(0(),y) = [0] >= [0] = True() <=(S(x),0()) = [0] >= [0] = False() <=(S(x),S(y)) = [0] >= [0] = <=(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) - Weak DPs: merge#(Cons(x,xs),Nil()) -> c_2() merge#(Nil(),ys) -> c_4() merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3,<=#/2,goal#/2,merge#/2,merge[Ite]#/3} / {0/0,Cons/2,False/0,Nil/0,S/1 ,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#} and constructors {0,Cons ,False,Nil,S,True} + 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(merge[Ite]#) = {1}, uargs(c_3) = {1}, uargs(c_8) = {1}, uargs(c_9) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [2] p(<=) = [3] p(Cons) = [1] x2 + [8] p(False) = [0] p(Nil) = [9] p(S) = [1] p(True) = [2] p(goal) = [1] x1 + [1] p(merge) = [2] x2 + [1] p(merge[Ite]) = [1] x1 + [2] x2 + [1] p(<=#) = [2] x1 + [0] p(goal#) = [1] x2 + [1] p(merge#) = [1] x1 + [2] x2 + [5] p(merge[Ite]#) = [1] x1 + [1] x2 + [2] x3 + [1] p(c_1) = [8] x1 + [1] p(c_2) = [1] p(c_3) = [1] x1 + [0] p(c_4) = [2] p(c_5) = [1] p(c_6) = [4] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [12] p(c_9) = [1] x1 + [3] Following rules are strictly oriented: merge#(Cons(x',xs'),Cons(x,xs)) = [2] xs + [1] xs' + [29] > [2] xs + [1] xs' + [28] = c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) Following rules are (at-least) weakly oriented: merge#(Cons(x,xs),Nil()) = [1] xs + [31] >= [1] = c_2() merge#(Nil(),ys) = [2] ys + [14] >= [2] = c_4() merge[Ite]#(False(),xs',Cons(x,xs)) = [2] xs + [1] xs' + [17] >= [2] xs + [1] xs' + [17] = c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) = [1] xs + [2] ys + [11] >= [1] xs + [2] ys + [8] = c_9(merge#(xs,ys)) <=(0(),y) = [3] >= [2] = True() <=(S(x),0()) = [3] >= [0] = False() <=(S(x),S(y)) = [3] >= [3] = <=(x,y) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: merge#(Cons(x,xs),Nil()) -> c_2() merge#(Cons(x',xs'),Cons(x,xs)) -> c_3(merge[Ite]#(<=(x',x),Cons(x',xs'),Cons(x,xs))) merge#(Nil(),ys) -> c_4() merge[Ite]#(False(),xs',Cons(x,xs)) -> c_8(merge#(xs',xs)) merge[Ite]#(True(),Cons(x,xs),ys) -> c_9(merge#(xs,ys)) - Weak TRS: <=(0(),y) -> True() <=(S(x),0()) -> False() <=(S(x),S(y)) -> <=(x,y) - Signature: {<=/2,goal/2,merge/2,merge[Ite]/3,<=#/2,goal#/2,merge#/2,merge[Ite]#/3} / {0/0,Cons/2,False/0,Nil/0,S/1 ,True/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {<=#,goal#,merge#,merge[Ite]#} and constructors {0,Cons ,False,Nil,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))