WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) purge(add(N,X)) -> add(N,purge(rm(N,X))) purge(nil()) -> nil() rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s ,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) purge(add(N,X)) -> add(N,purge(rm(N,X))) purge(nil()) -> nil() rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s ,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: eq(x,y){x -> s(x),y -> s(y)} = eq(s(x),s(y)) ->^+ eq(x,y) = C[eq(x,y) = eq(x,y){}] ** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) purge(add(N,X)) -> add(N,purge(rm(N,X))) purge(nil()) -> nil() rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s ,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs eq#(0(),0()) -> c_1() eq#(0(),s(X)) -> c_2() eq#(s(X),0()) -> c_3() eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) purge#(nil()) -> c_8() rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) rm#(N,nil()) -> c_10() Weak DPs and mark the set of starting terms. ** Step 1.b:2: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(0(),0()) -> c_1() eq#(0(),s(X)) -> c_2() eq#(s(X),0()) -> c_3() eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) purge#(nil()) -> c_8() rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) rm#(N,nil()) -> c_10() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) purge(add(N,X)) -> add(N,purge(rm(N,X))) purge(nil()) -> nil() rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() eq#(0(),0()) -> c_1() eq#(0(),s(X)) -> c_2() eq#(s(X),0()) -> c_3() eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) purge#(nil()) -> c_8() rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) rm#(N,nil()) -> c_10() ** Step 1.b:3: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(0(),0()) -> c_1() eq#(0(),s(X)) -> c_2() eq#(s(X),0()) -> c_3() eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) purge#(nil()) -> c_8() rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) rm#(N,nil()) -> c_10() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,8,10} by application of Pre({1,2,3,8,10}) = {4,5,6,7,9}. Here rules are labelled as follows: 1: eq#(0(),0()) -> c_1() 2: eq#(0(),s(X)) -> c_2() 3: eq#(s(X),0()) -> c_3() 4: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) 5: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) 6: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) 7: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) 8: purge#(nil()) -> c_8() 9: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) 10: rm#(N,nil()) -> c_10() ** Step 1.b:4: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak DPs: eq#(0(),0()) -> c_1() eq#(0(),s(X)) -> c_2() eq#(s(X),0()) -> c_3() purge#(nil()) -> c_8() rm#(N,nil()) -> c_10() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) -->_1 eq#(s(X),0()) -> c_3():8 -->_1 eq#(0(),s(X)) -> c_2():7 -->_1 eq#(0(),0()) -> c_1():6 -->_1 eq#(s(X),s(Y)) -> c_4(eq#(X,Y)):1 2:S:ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):5 -->_1 rm#(N,nil()) -> c_10():10 3:S:ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):5 -->_1 rm#(N,nil()) -> c_10():10 4:S:purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) -->_2 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):5 -->_2 rm#(N,nil()) -> c_10():10 -->_1 purge#(nil()) -> c_8():9 -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)):4 5:S:rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) -->_2 eq#(s(X),0()) -> c_3():8 -->_2 eq#(0(),s(X)) -> c_2():7 -->_2 eq#(0(),0()) -> c_1():6 -->_1 ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)):3 -->_1 ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)):2 -->_2 eq#(s(X),s(Y)) -> c_4(eq#(X,Y)):1 6:W:eq#(0(),0()) -> c_1() 7:W:eq#(0(),s(X)) -> c_2() 8:W:eq#(s(X),0()) -> c_3() 9:W:purge#(nil()) -> c_8() 10:W:rm#(N,nil()) -> c_10() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: purge#(nil()) -> c_8() 10: rm#(N,nil()) -> c_10() 6: eq#(0(),0()) -> c_1() 7: eq#(0(),s(X)) -> c_2() 8: eq#(s(X),0()) -> c_3() ** Step 1.b:5: Decompose WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil ,s,true} Problem (S) - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil ,s,true} *** Step 1.b:5.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) The strictly oriented rules are moved into the weak component. **** Step 1.b:5.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1,2} Following symbols are considered usable: {ifrm,rm,eq#,ifrm#,purge#,rm#} TcT has computed the following interpretation: p(0) = 0 p(add) = 1 + x1 + x2 p(eq) = 0 p(false) = 1 p(ifrm) = x3 p(nil) = 0 p(purge) = 2*x1^2 p(rm) = x2 p(s) = 2 + x1 p(true) = 0 p(eq#) = 2*x1 p(ifrm#) = x2 + 2*x2*x3 p(purge#) = 1 + 2*x1^2 p(rm#) = 3*x1 + 2*x1*x2 p(c_1) = 2 p(c_2) = 0 p(c_3) = 0 p(c_4) = x1 p(c_5) = x1 p(c_6) = x1 p(c_7) = 1 + x1 + x2 p(c_8) = 0 p(c_9) = x1 + x2 p(c_10) = 0 Following rules are strictly oriented: eq#(s(X),s(Y)) = 4 + 2*X > 2*X = c_4(eq#(X,Y)) Following rules are (at-least) weakly oriented: ifrm#(false(),N,add(M,X)) = 2*M*N + 3*N + 2*N*X >= 3*N + 2*N*X = c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) = 2*M*N + 3*N + 2*N*X >= 3*N + 2*N*X = c_6(rm#(N,X)) purge#(add(N,X)) = 3 + 4*N + 4*N*X + 2*N^2 + 4*X + 2*X^2 >= 2 + 3*N + 2*N*X + 2*X^2 = c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) = 2*M*N + 5*N + 2*N*X >= 2*M*N + 5*N + 2*N*X = c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) ifrm(false(),N,add(M,X)) = 1 + M + X >= 1 + M + X = add(M,rm(N,X)) ifrm(true(),N,add(M,X)) = 1 + M + X >= X = rm(N,X) rm(N,add(M,X)) = 1 + M + X >= 1 + M + X = ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) = 0 >= 0 = nil() **** Step 1.b:5.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 1.b:5.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) -->_1 eq#(s(X),s(Y)) -> c_4(eq#(X,Y)):1 2:W:ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):5 3:W:ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):5 4:W:purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) -->_2 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):5 -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)):4 5:W:rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) -->_1 ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)):3 -->_1 ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)):2 -->_2 eq#(s(X),s(Y)) -> c_4(eq#(X,Y)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) 2: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) 5: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) 3: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) 1: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) **** Step 1.b:5.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak DPs: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):4 2:S:ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):4 3:S:purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) -->_2 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):4 -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)):3 4:S:rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) -->_2 eq#(s(X),s(Y)) -> c_4(eq#(X,Y)):5 -->_1 ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)):2 -->_1 ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)):1 5:W:eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) -->_1 eq#(s(X),s(Y)) -> c_4(eq#(X,Y)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: eq#(s(X),s(Y)) -> c_4(eq#(X,Y)) *** Step 1.b:5.b:2: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/2,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):4 2:S:ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):4 3:S:purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) -->_2 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)):4 -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)):3 4:S:rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X)),eq#(N,M)) -->_1 ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)):2 -->_1 ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) *** Step 1.b:5.b:3: Decompose WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil ,s,true} Problem (S) - Strict DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil ,s,true} **** Step 1.b:5.b:3.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) The strictly oriented rules are moved into the weak component. ***** Step 1.b:5.b:3.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1} Following symbols are considered usable: {eq,ifrm,rm,eq#,ifrm#,purge#,rm#} TcT has computed the following interpretation: p(0) = 2 p(add) = 2 + x1 + x2 p(eq) = x1 p(false) = 0 p(ifrm) = 2 + x3 p(nil) = 1 p(purge) = 2 + 2*x1^2 p(rm) = 2 + x2 p(s) = x1 p(true) = 2 p(eq#) = 2*x1 + x1*x2 + 2*x1^2 + x2^2 p(ifrm#) = x1 + 2*x2 + 2*x2*x3 p(purge#) = 3 + x1^2 p(rm#) = 3*x1 + 2*x1*x2 p(c_1) = 0 p(c_2) = 0 p(c_3) = 0 p(c_4) = 2 p(c_5) = x1 p(c_6) = x1 p(c_7) = x1 + x2 p(c_8) = 0 p(c_9) = x1 p(c_10) = 0 Following rules are strictly oriented: ifrm#(true(),N,add(M,X)) = 2 + 2*M*N + 6*N + 2*N*X > 3*N + 2*N*X = c_6(rm#(N,X)) Following rules are (at-least) weakly oriented: ifrm#(false(),N,add(M,X)) = 2*M*N + 6*N + 2*N*X >= 3*N + 2*N*X = c_5(rm#(N,X)) purge#(add(N,X)) = 7 + 4*N + 2*N*X + N^2 + 4*X + X^2 >= 7 + 3*N + 2*N*X + 4*X + X^2 = c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) = 2*M*N + 7*N + 2*N*X >= 2*M*N + 7*N + 2*N*X = c_9(ifrm#(eq(N,M),N,add(M,X))) eq(0(),0()) = 2 >= 2 = true() eq(0(),s(X)) = 2 >= 0 = false() eq(s(X),0()) = X >= 0 = false() eq(s(X),s(Y)) = X >= X = eq(X,Y) ifrm(false(),N,add(M,X)) = 4 + M + X >= 4 + M + X = add(M,rm(N,X)) ifrm(true(),N,add(M,X)) = 4 + M + X >= 2 + X = rm(N,X) rm(N,add(M,X)) = 4 + M + X >= 4 + M + X = ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) = 3 >= 1 = nil() ***** Step 1.b:5.b:3.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 1.b:5.b:3.a:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) The strictly oriented rules are moved into the weak component. ****** Step 1.b:5.b:3.a:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1} Following symbols are considered usable: {eq,ifrm,rm,eq#,ifrm#,purge#,rm#} TcT has computed the following interpretation: p(0) = [0] [1] [1] p(add) = [0 0 0] [0 0 1] [0] [0 0 0] x1 + [0 1 1] x2 + [0] [0 0 1] [0 0 1] [0] p(eq) = [0 0 0] [0 0 0] [0] [0 1 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 1] [0] p(false) = [0] [0] [1] p(ifrm) = [0 1 0] [0 0 1] [0] [0 0 0] x2 + [0 1 0] x3 + [0] [0 0 0] [0 0 1] [0] p(nil) = [0] [0] [0] p(purge) = [0] [0] [0] p(rm) = [0 1 0] [0 0 1] [0] [0 0 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 1] [0] p(s) = [0 0 0] [0] [0 1 1] x1 + [1] [0 0 1] [1] p(true) = [0] [1] [0] p(eq#) = [0] [0] [0] p(ifrm#) = [0 0 1] [0 0 0] [1 0 0] [0] [0 1 1] x1 + [0 0 1] x2 + [0 0 0] x3 + [1] [0 1 0] [1 0 0] [1 0 0] [0] p(purge#) = [0 1 0] [1] [0 0 0] x1 + [1] [1 0 0] [0] p(rm#) = [0 0 0] [0 0 1] [0] [1 0 0] x1 + [0 0 1] x2 + [0] [0 1 1] [0 0 0] [1] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [0] [0] [0] p(c_4) = [0] [0] [0] p(c_5) = [1 0 0] [0] [0 0 0] x1 + [1] [0 0 0] [0] p(c_6) = [1 0 0] [0] [0 0 0] x1 + [0] [0 1 0] [0] p(c_7) = [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] p(c_8) = [0] [0] [0] p(c_9) = [1 0 0] [0] [1 0 0] x1 + [0] [0 0 0] [0] p(c_10) = [0] [0] [0] Following rules are strictly oriented: ifrm#(false(),N,add(M,X)) = [0 0 0] [0 0 1] [1] [0 0 1] N + [0 0 0] X + [2] [1 0 0] [0 0 1] [0] > [0 0 1] [0] [0 0 0] X + [1] [0 0 0] [0] = c_5(rm#(N,X)) Following rules are (at-least) weakly oriented: ifrm#(true(),N,add(M,X)) = [0 0 0] [0 0 1] [0] [0 0 1] N + [0 0 0] X + [2] [1 0 0] [0 0 1] [1] >= [0 0 0] [0 0 1] [0] [0 0 0] N + [0 0 0] X + [0] [1 0 0] [0 0 1] [0] = c_6(rm#(N,X)) purge#(add(N,X)) = [0 1 1] [1] [0 0 0] X + [1] [0 0 1] [0] >= [0 1 1] [1] [0 0 0] X + [0] [0 0 0] [0] = c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) = [0 0 1] [0 0 0] [0 0 1] [0] [0 0 1] M + [1 0 0] N + [0 0 1] X + [0] [0 0 0] [0 1 1] [0 0 0] [1] >= [0 0 1] [0 0 1] [0] [0 0 1] M + [0 0 1] X + [0] [0 0 0] [0 0 0] [0] = c_9(ifrm#(eq(N,M),N,add(M,X))) eq(0(),0()) = [0] [1] [1] >= [0] [1] [0] = true() eq(0(),s(X)) = [0 0 0] [0] [0 0 0] X + [1] [0 0 1] [1] >= [0] [0] [1] = false() eq(s(X),0()) = [0 0 0] [0] [0 1 1] X + [1] [0 0 0] [1] >= [0] [0] [1] = false() eq(s(X),s(Y)) = [0 0 0] [0 0 0] [0] [0 1 1] X + [0 0 0] Y + [1] [0 0 0] [0 0 1] [1] >= [0 0 0] [0 0 0] [0] [0 1 0] X + [0 0 0] Y + [0] [0 0 0] [0 0 1] [0] = eq(X,Y) ifrm(false(),N,add(M,X)) = [0 0 1] [0 1 0] [0 0 1] [0] [0 0 0] M + [0 0 0] N + [0 1 1] X + [0] [0 0 1] [0 0 0] [0 0 1] [0] >= [0 0 0] [0 0 1] [0] [0 0 0] M + [0 1 1] X + [0] [0 0 1] [0 0 1] [0] = add(M,rm(N,X)) ifrm(true(),N,add(M,X)) = [0 0 1] [0 1 0] [0 0 1] [0] [0 0 0] M + [0 0 0] N + [0 1 1] X + [0] [0 0 1] [0 0 0] [0 0 1] [0] >= [0 1 0] [0 0 1] [0] [0 0 0] N + [0 1 0] X + [0] [0 0 0] [0 0 1] [0] = rm(N,X) rm(N,add(M,X)) = [0 0 1] [0 1 0] [0 0 1] [0] [0 0 0] M + [0 0 0] N + [0 1 1] X + [0] [0 0 1] [0 0 0] [0 0 1] [0] >= [0 0 1] [0 1 0] [0 0 1] [0] [0 0 0] M + [0 0 0] N + [0 1 1] X + [0] [0 0 1] [0 0 0] [0 0 1] [0] = ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) = [0 1 0] [0] [0 0 0] N + [0] [0 0 0] [0] >= [0] [0] [0] = nil() ****** Step 1.b:5.b:3.a:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ****** Step 1.b:5.b:3.a:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) Consider the set of all dependency pairs 1: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) 2: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) 3: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) 4: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) Processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,2,3} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ******* Step 1.b:5.b:3.a:1.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1,2}, uargs(c_9) = {1} Following symbols are considered usable: {eq,ifrm,rm,eq#,ifrm#,purge#,rm#} TcT has computed the following interpretation: p(0) = [0] [0] [1] p(add) = [0 0 0] [0 0 1] [0] [0 0 0] x1 + [0 1 1] x2 + [1] [0 0 1] [0 0 1] [0] p(eq) = [0 0 1] [0] [0 0 0] x2 + [0] [0 0 0] [0] p(false) = [1] [0] [0] p(ifrm) = [0 0 1] [1] [0 1 0] x3 + [0] [0 0 1] [0] p(nil) = [0] [1] [0] p(purge) = [0] [0] [0] p(rm) = [0 0 1] [1] [0 1 0] x2 + [0] [0 0 1] [0] p(s) = [0 0 0] [0] [0 0 0] x1 + [0] [0 0 1] [1] p(true) = [1] [0] [0] p(eq#) = [0] [0] [0] p(ifrm#) = [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 1 1] x3 + [0] [0 0 0] [0 0 0] [0] p(purge#) = [0 1 0] [0] [0 0 1] x1 + [1] [1 0 0] [1] p(rm#) = [0 0 0] [0 0 1] [1] [0 0 1] x1 + [0 0 0] x2 + [1] [0 0 0] [0 0 0] [1] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [0] [0] [0] p(c_4) = [0] [0] [0] p(c_5) = [1 0 0] [0] [0 0 0] x1 + [1] [0 0 0] [0] p(c_6) = [1 0 0] [0] [1 0 0] x1 + [0] [0 0 0] [0] p(c_7) = [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 1] [0] p(c_8) = [0] [0] [0] p(c_9) = [1 0 0] [0] [0 0 0] x1 + [1] [0 0 0] [0] p(c_10) = [0] [0] [0] Following rules are strictly oriented: rm#(N,add(M,X)) = [0 0 1] [0 0 0] [0 0 1] [1] [0 0 0] M + [0 0 1] N + [0 0 0] X + [1] [0 0 0] [0 0 0] [0 0 0] [1] > [0 0 1] [0 0 1] [0] [0 0 0] M + [0 0 0] X + [1] [0 0 0] [0 0 0] [0] = c_9(ifrm#(eq(N,M),N,add(M,X))) Following rules are (at-least) weakly oriented: ifrm#(false(),N,add(M,X)) = [0 0 0] [0 0 1] [1] [0 0 1] M + [0 1 2] X + [1] [0 0 0] [0 0 0] [0] >= [0 0 1] [1] [0 0 0] X + [1] [0 0 0] [0] = c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) = [0 0 0] [0 0 1] [1] [0 0 1] M + [0 1 2] X + [1] [0 0 0] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] = c_6(rm#(N,X)) purge#(add(N,X)) = [0 0 0] [0 1 1] [1] [0 0 1] N + [0 0 1] X + [1] [0 0 0] [0 0 1] [1] >= [0 0 0] [0 1 1] [1] [0 0 1] N + [0 0 0] X + [1] [0 0 0] [0 0 0] [1] = c_7(purge#(rm(N,X)),rm#(N,X)) eq(0(),0()) = [1] [0] [0] >= [1] [0] [0] = true() eq(0(),s(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [0] >= [1] [0] [0] = false() eq(s(X),0()) = [1] [0] [0] >= [1] [0] [0] = false() eq(s(X),s(Y)) = [0 0 1] [1] [0 0 0] Y + [0] [0 0 0] [0] >= [0 0 1] [0] [0 0 0] Y + [0] [0 0 0] [0] = eq(X,Y) ifrm(false(),N,add(M,X)) = [0 0 1] [0 0 1] [1] [0 0 0] M + [0 1 1] X + [1] [0 0 1] [0 0 1] [0] >= [0 0 0] [0 0 1] [0] [0 0 0] M + [0 1 1] X + [1] [0 0 1] [0 0 1] [0] = add(M,rm(N,X)) ifrm(true(),N,add(M,X)) = [0 0 1] [0 0 1] [1] [0 0 0] M + [0 1 1] X + [1] [0 0 1] [0 0 1] [0] >= [0 0 1] [1] [0 1 0] X + [0] [0 0 1] [0] = rm(N,X) rm(N,add(M,X)) = [0 0 1] [0 0 1] [1] [0 0 0] M + [0 1 1] X + [1] [0 0 1] [0 0 1] [0] >= [0 0 1] [0 0 1] [1] [0 0 0] M + [0 1 1] X + [1] [0 0 1] [0 0 1] [0] = ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) = [1] [1] [0] >= [0] [1] [0] = nil() ******* Step 1.b:5.b:3.a:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ******* Step 1.b:5.b:3.a:1.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))):4 2:W:ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))):4 3:W:purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) -->_2 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))):4 -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)):3 4:W:rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) -->_1 ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)):2 -->_1 ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) 1: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) 4: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) 2: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) ******* Step 1.b:5.b:3.a:1.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 1.b:5.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak DPs: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) -->_2 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))):4 -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)):1 2:W:ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))):4 3:W:ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) -->_1 rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))):4 4:W:rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) -->_1 ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)):3 -->_1 ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: rm#(N,add(M,X)) -> c_9(ifrm#(eq(N,M),N,add(M,X))) 3: ifrm#(true(),N,add(M,X)) -> c_6(rm#(N,X)) 2: ifrm#(false(),N,add(M,X)) -> c_5(rm#(N,X)) **** Step 1.b:5.b:3.b:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)) -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X)),rm#(N,X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: purge#(add(N,X)) -> c_7(purge#(rm(N,X))) **** Step 1.b:5.b:3.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: purge#(add(N,X)) -> c_7(purge#(rm(N,X))) The strictly oriented rules are moved into the weak component. ***** Step 1.b:5.b:3.b:3.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: {ifrm,rm,eq#,ifrm#,purge#,rm#} TcT has computed the following interpretation: p(0) = [0] p(add) = [1] x2 + [2] p(eq) = [0] p(false) = [0] p(ifrm) = [1] x3 + [0] p(nil) = [4] p(purge) = [1] x1 + [2] p(rm) = [1] x2 + [0] p(s) = [1] p(true) = [0] p(eq#) = [1] p(ifrm#) = [1] x1 + [2] x2 + [1] x3 + [0] p(purge#) = [4] x1 + [0] p(rm#) = [2] x1 + [2] p(c_1) = [2] p(c_2) = [2] p(c_3) = [2] p(c_4) = [1] x1 + [1] p(c_5) = [1] p(c_6) = [1] x1 + [2] p(c_7) = [1] x1 + [4] p(c_8) = [1] p(c_9) = [8] x1 + [2] p(c_10) = [8] Following rules are strictly oriented: purge#(add(N,X)) = [4] X + [8] > [4] X + [4] = c_7(purge#(rm(N,X))) Following rules are (at-least) weakly oriented: ifrm(false(),N,add(M,X)) = [1] X + [2] >= [1] X + [2] = add(M,rm(N,X)) ifrm(true(),N,add(M,X)) = [1] X + [2] >= [1] X + [0] = rm(N,X) rm(N,add(M,X)) = [1] X + [2] >= [1] X + [2] = ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) = [4] >= [4] = nil() ***** Step 1.b:5.b:3.b:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 1.b:5.b:3.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: purge#(add(N,X)) -> c_7(purge#(rm(N,X))) - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:purge#(add(N,X)) -> c_7(purge#(rm(N,X))) -->_1 purge#(add(N,X)) -> c_7(purge#(rm(N,X))):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: purge#(add(N,X)) -> c_7(purge#(rm(N,X))) ***** Step 1.b:5.b:3.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: eq(0(),0()) -> true() eq(0(),s(X)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) ifrm(false(),N,add(M,X)) -> add(M,rm(N,X)) ifrm(true(),N,add(M,X)) -> rm(N,X) rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X)) rm(N,nil()) -> nil() - Signature: {eq/2,ifrm/3,purge/1,rm/2,eq#/2,ifrm#/3,purge#/1,rm#/2} / {0/0,add/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0 ,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/1,c_10/0} - Obligation: innermost runtime complexity wrt. defined symbols {eq#,ifrm#,purge#,rm#} and constructors {0,add,false,nil,s ,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))