WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() - Weak TRS: mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0,set/1,true/0,union/2} - Obligation: innermost runtime complexity wrt. defined symbols {MEM,OR,mem,or} and constructors {=,c,c1,c2,c3,c4,c5,c6 ,false,nil,set,true,union} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() - Weak TRS: mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0,set/1,true/0,union/2} - Obligation: innermost runtime complexity wrt. defined symbols {MEM,OR,mem,or} and constructors {=,c,c1,c2,c3,c4,c5,c6 ,false,nil,set,true,union} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() - Weak TRS: mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0,set/1,true/0,union/2} - Obligation: innermost runtime complexity wrt. defined symbols {MEM,OR,mem,or} and constructors {=,c,c1,c2,c3,c4,c5,c6 ,false,nil,set,true,union} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: MEM(x,y){y -> union(y,z)} = MEM(x,union(y,z)) ->^+ c5(OR(mem(x,y),mem(x,z)),MEM(x,y)) = C[MEM(x,y) = MEM(x,y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() - Weak TRS: mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0,set/1,true/0,union/2} - Obligation: innermost runtime complexity wrt. defined symbols {MEM,OR,mem,or} and constructors {=,c,c1,c2,c3,c4,c5,c6 ,false,nil,set,true,union} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs MEM#(z0,nil()) -> c_1() MEM#(z0,set(z1)) -> c_2() MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)) OR#(z0,true()) -> c_5() OR#(false(),false()) -> c_6() OR#(true(),z0) -> c_7() Weak DPs mem#(z0,nil()) -> c_8() mem#(z0,set(z1)) -> c_9() mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)) or#(z0,true()) -> c_11() or#(false(),false()) -> c_12() or#(true(),z0) -> c_13() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MEM#(z0,nil()) -> c_1() MEM#(z0,set(z1)) -> c_2() MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)) OR#(z0,true()) -> c_5() OR#(false(),false()) -> c_6() OR#(true(),z0) -> c_7() - Weak DPs: mem#(z0,nil()) -> c_8() mem#(z0,set(z1)) -> c_9() mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)) or#(z0,true()) -> c_11() or#(false(),false()) -> c_12() or#(true(),z0) -> c_13() - Weak TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2,MEM#/2,OR#/2,mem#/2,or#/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0 ,set/1,true/0,union/2,c_1/0,c_2/0,c_3/4,c_4/4,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {MEM#,OR#,mem#,or#} and constructors {=,c,c1,c2,c3,c4,c5 ,c6,false,nil,set,true,union} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,5,6,7} by application of Pre({1,2,5,6,7}) = {3,4}. Here rules are labelled as follows: 1: MEM#(z0,nil()) -> c_1() 2: MEM#(z0,set(z1)) -> c_2() 3: MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)) 4: MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)) 5: OR#(z0,true()) -> c_5() 6: OR#(false(),false()) -> c_6() 7: OR#(true(),z0) -> c_7() 8: mem#(z0,nil()) -> c_8() 9: mem#(z0,set(z1)) -> c_9() 10: mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)) 11: or#(z0,true()) -> c_11() 12: or#(false(),false()) -> c_12() 13: or#(true(),z0) -> c_13() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)) - Weak DPs: MEM#(z0,nil()) -> c_1() MEM#(z0,set(z1)) -> c_2() OR#(z0,true()) -> c_5() OR#(false(),false()) -> c_6() OR#(true(),z0) -> c_7() mem#(z0,nil()) -> c_8() mem#(z0,set(z1)) -> c_9() mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)) or#(z0,true()) -> c_11() or#(false(),false()) -> c_12() or#(true(),z0) -> c_13() - Weak TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2,MEM#/2,OR#/2,mem#/2,or#/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0 ,set/1,true/0,union/2,c_1/0,c_2/0,c_3/4,c_4/4,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {MEM#,OR#,mem#,or#} and constructors {=,c,c1,c2,c3,c4,c5 ,c6,false,nil,set,true,union} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)) -->_3 mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)):10 -->_2 mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)):10 -->_4 MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)):2 -->_3 mem#(z0,set(z1)) -> c_9():9 -->_2 mem#(z0,set(z1)) -> c_9():9 -->_3 mem#(z0,nil()) -> c_8():8 -->_2 mem#(z0,nil()) -> c_8():8 -->_1 OR#(true(),z0) -> c_7():7 -->_1 OR#(false(),false()) -> c_6():6 -->_1 OR#(z0,true()) -> c_5():5 -->_4 MEM#(z0,set(z1)) -> c_2():4 -->_4 MEM#(z0,nil()) -> c_1():3 -->_4 MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)):1 2:S:MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)) -->_3 mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)):10 -->_2 mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)):10 -->_3 mem#(z0,set(z1)) -> c_9():9 -->_2 mem#(z0,set(z1)) -> c_9():9 -->_3 mem#(z0,nil()) -> c_8():8 -->_2 mem#(z0,nil()) -> c_8():8 -->_1 OR#(true(),z0) -> c_7():7 -->_1 OR#(false(),false()) -> c_6():6 -->_1 OR#(z0,true()) -> c_5():5 -->_4 MEM#(z0,set(z1)) -> c_2():4 -->_4 MEM#(z0,nil()) -> c_1():3 -->_4 MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)):2 -->_4 MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)):1 3:W:MEM#(z0,nil()) -> c_1() 4:W:MEM#(z0,set(z1)) -> c_2() 5:W:OR#(z0,true()) -> c_5() 6:W:OR#(false(),false()) -> c_6() 7:W:OR#(true(),z0) -> c_7() 8:W:mem#(z0,nil()) -> c_8() 9:W:mem#(z0,set(z1)) -> c_9() 10:W:mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)) -->_1 or#(true(),z0) -> c_13():13 -->_1 or#(false(),false()) -> c_12():12 -->_1 or#(z0,true()) -> c_11():11 -->_3 mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)):10 -->_2 mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)):10 -->_3 mem#(z0,set(z1)) -> c_9():9 -->_2 mem#(z0,set(z1)) -> c_9():9 -->_3 mem#(z0,nil()) -> c_8():8 -->_2 mem#(z0,nil()) -> c_8():8 11:W:or#(z0,true()) -> c_11() 12:W:or#(false(),false()) -> c_12() 13:W:or#(true(),z0) -> c_13() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: MEM#(z0,nil()) -> c_1() 4: MEM#(z0,set(z1)) -> c_2() 5: OR#(z0,true()) -> c_5() 6: OR#(false(),false()) -> c_6() 7: OR#(true(),z0) -> c_7() 10: mem#(z0,union(z1,z2)) -> c_10(or#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2)) 8: mem#(z0,nil()) -> c_8() 9: mem#(z0,set(z1)) -> c_9() 11: or#(z0,true()) -> c_11() 12: or#(false(),false()) -> c_12() 13: or#(true(),z0) -> c_13() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)) - Weak TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2,MEM#/2,OR#/2,mem#/2,or#/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0 ,set/1,true/0,union/2,c_1/0,c_2/0,c_3/4,c_4/4,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {MEM#,OR#,mem#,or#} and constructors {=,c,c1,c2,c3,c4,c5 ,c6,false,nil,set,true,union} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)) -->_4 MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)):2 -->_4 MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)):1 2:S:MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)) -->_4 MEM#(z0,union(z1,z2)) -> c_4(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z2)):2 -->_4 MEM#(z0,union(z1,z2)) -> c_3(OR#(mem(z0,z1),mem(z0,z2)),mem#(z0,z1),mem#(z0,z2),MEM#(z0,z1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: MEM#(z0,union(z1,z2)) -> c_3(MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(MEM#(z0,z2)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MEM#(z0,union(z1,z2)) -> c_3(MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(MEM#(z0,z2)) - Weak TRS: MEM(z0,nil()) -> c3() MEM(z0,set(z1)) -> c4() MEM(z0,union(z1,z2)) -> c5(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z1)) MEM(z0,union(z1,z2)) -> c6(OR(mem(z0,z1),mem(z0,z2)),MEM(z0,z2)) OR(z0,true()) -> c1() OR(false(),false()) -> c2() OR(true(),z0) -> c() mem(z0,nil()) -> false() mem(z0,set(z1)) -> =(z0,z1) mem(z0,union(z1,z2)) -> or(mem(z0,z1),mem(z0,z2)) or(z0,true()) -> true() or(false(),false()) -> false() or(true(),z0) -> true() - Signature: {MEM/2,OR/2,mem/2,or/2,MEM#/2,OR#/2,mem#/2,or#/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0 ,set/1,true/0,union/2,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {MEM#,OR#,mem#,or#} and constructors {=,c,c1,c2,c3,c4,c5 ,c6,false,nil,set,true,union} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: MEM#(z0,union(z1,z2)) -> c_3(MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(MEM#(z0,z2)) ** Step 1.b:6: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: MEM#(z0,union(z1,z2)) -> c_3(MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(MEM#(z0,z2)) - Signature: {MEM/2,OR/2,mem/2,or/2,MEM#/2,OR#/2,mem#/2,or#/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0 ,set/1,true/0,union/2,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {MEM#,OR#,mem#,or#} and constructors {=,c,c1,c2,c3,c4,c5 ,c6,false,nil,set,true,union} + 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}, uargs(c_4) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(=) = [0] p(MEM) = [0] p(OR) = [0] p(c) = [0] p(c1) = [0] p(c2) = [0] p(c3) = [0] p(c4) = [0] p(c5) = [1] x1 + [1] x2 + [0] p(c6) = [1] x2 + [0] p(false) = [0] p(mem) = [0] p(nil) = [0] p(or) = [0] p(set) = [1] x1 + [0] p(true) = [0] p(union) = [1] x1 + [1] x2 + [1] p(MEM#) = [9] x2 + [6] p(OR#) = [0] p(mem#) = [0] p(or#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [0] Following rules are strictly oriented: MEM#(z0,union(z1,z2)) = [9] z1 + [9] z2 + [15] > [9] z1 + [6] = c_3(MEM#(z0,z1)) MEM#(z0,union(z1,z2)) = [9] z1 + [9] z2 + [15] > [9] z2 + [6] = c_4(MEM#(z0,z2)) Following rules are (at-least) weakly oriented: Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 1.b:7: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: MEM#(z0,union(z1,z2)) -> c_3(MEM#(z0,z1)) MEM#(z0,union(z1,z2)) -> c_4(MEM#(z0,z2)) - Signature: {MEM/2,OR/2,mem/2,or/2,MEM#/2,OR#/2,mem#/2,or#/2} / {=/2,c/0,c1/0,c2/0,c3/0,c4/0,c5/2,c6/2,false/0,nil/0 ,set/1,true/0,union/2,c_1/0,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0,c_8/0,c_9/0,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {MEM#,OR#,mem#,or#} and constructors {=,c,c1,c2,c3,c4,c5 ,c6,false,nil,set,true,union} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))