WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1} - Obligation: innermost runtime complexity wrt. defined symbols {goal,list,notEmpty} and constructors {Cons,False,Nil,True ,isEmpty[Match]} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1} - Obligation: innermost runtime complexity wrt. defined symbols {goal,list,notEmpty} and constructors {Cons,False,Nil,True ,isEmpty[Match]} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1} - Obligation: innermost runtime complexity wrt. defined symbols {goal,list,notEmpty} and constructors {Cons,False,Nil,True ,isEmpty[Match]} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: list(y){y -> Cons(x,y)} = list(Cons(x,y)) ->^+ list(y) = C[list(y) = list(y){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1} - Obligation: innermost runtime complexity wrt. defined symbols {goal,list,notEmpty} and constructors {Cons,False,Nil,True ,isEmpty[Match]} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs goal#(x) -> c_1(list#(x)) list#(Cons(x,xs)) -> c_2(list#(xs)) list#(Nil()) -> c_3() list#(Nil()) -> c_4() notEmpty#(Cons(x,xs)) -> c_5() notEmpty#(Nil()) -> c_6() Weak DPs and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: goal#(x) -> c_1(list#(x)) list#(Cons(x,xs)) -> c_2(list#(xs)) list#(Nil()) -> c_3() list#(Nil()) -> c_4() notEmpty#(Cons(x,xs)) -> c_5() notEmpty#(Nil()) -> c_6() - Weak TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1,goal#/1,list#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1,c_1/1 ,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {goal#,list#,notEmpty#} and constructors {Cons,False,Nil ,True,isEmpty[Match]} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,4,5,6} by application of Pre({3,4,5,6}) = {1,2}. Here rules are labelled as follows: 1: goal#(x) -> c_1(list#(x)) 2: list#(Cons(x,xs)) -> c_2(list#(xs)) 3: list#(Nil()) -> c_3() 4: list#(Nil()) -> c_4() 5: notEmpty#(Cons(x,xs)) -> c_5() 6: notEmpty#(Nil()) -> c_6() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: goal#(x) -> c_1(list#(x)) list#(Cons(x,xs)) -> c_2(list#(xs)) - Weak DPs: list#(Nil()) -> c_3() list#(Nil()) -> c_4() notEmpty#(Cons(x,xs)) -> c_5() notEmpty#(Nil()) -> c_6() - Weak TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1,goal#/1,list#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1,c_1/1 ,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {goal#,list#,notEmpty#} and constructors {Cons,False,Nil ,True,isEmpty[Match]} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:goal#(x) -> c_1(list#(x)) -->_1 list#(Cons(x,xs)) -> c_2(list#(xs)):2 -->_1 list#(Nil()) -> c_4():4 -->_1 list#(Nil()) -> c_3():3 2:S:list#(Cons(x,xs)) -> c_2(list#(xs)) -->_1 list#(Nil()) -> c_4():4 -->_1 list#(Nil()) -> c_3():3 -->_1 list#(Cons(x,xs)) -> c_2(list#(xs)):2 3:W:list#(Nil()) -> c_3() 4:W:list#(Nil()) -> c_4() 5:W:notEmpty#(Cons(x,xs)) -> c_5() 6:W:notEmpty#(Nil()) -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: notEmpty#(Nil()) -> c_6() 5: notEmpty#(Cons(x,xs)) -> c_5() 3: list#(Nil()) -> c_3() 4: list#(Nil()) -> c_4() ** Step 1.b:4: RemoveHeads. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: goal#(x) -> c_1(list#(x)) list#(Cons(x,xs)) -> c_2(list#(xs)) - Weak TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1,goal#/1,list#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1,c_1/1 ,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {goal#,list#,notEmpty#} and constructors {Cons,False,Nil ,True,isEmpty[Match]} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:goal#(x) -> c_1(list#(x)) -->_1 list#(Cons(x,xs)) -> c_2(list#(xs)):2 2:S:list#(Cons(x,xs)) -> c_2(list#(xs)) -->_1 list#(Cons(x,xs)) -> c_2(list#(xs)):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#(x) -> c_1(list#(x)))] ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: list#(Cons(x,xs)) -> c_2(list#(xs)) - Weak TRS: goal(x) -> list(x) list(Cons(x,xs)) -> list(xs) list(Nil()) -> True() list(Nil()) -> isEmpty[Match](Nil()) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {goal/1,list/1,notEmpty/1,goal#/1,list#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1,c_1/1 ,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {goal#,list#,notEmpty#} and constructors {Cons,False,Nil ,True,isEmpty[Match]} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: list#(Cons(x,xs)) -> c_2(list#(xs)) ** Step 1.b:6: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: list#(Cons(x,xs)) -> c_2(list#(xs)) - Signature: {goal/1,list/1,notEmpty/1,goal#/1,list#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1,c_1/1 ,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {goal#,list#,notEmpty#} and constructors {Cons,False,Nil ,True,isEmpty[Match]} + 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: {goal#,list#,notEmpty#} TcT has computed the following interpretation: p(Cons) = [1] x2 + [1] p(False) = [1] p(Nil) = [1] p(True) = [0] p(goal) = [2] p(isEmpty[Match]) = [0] p(list) = [1] x1 + [4] p(notEmpty) = [1] p(goal#) = [8] x1 + [0] p(list#) = [2] x1 + [1] p(notEmpty#) = [4] x1 + [1] p(c_1) = [2] x1 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [8] p(c_4) = [0] p(c_5) = [2] p(c_6) = [0] Following rules are strictly oriented: list#(Cons(x,xs)) = [2] xs + [3] > [2] xs + [1] = c_2(list#(xs)) Following rules are (at-least) weakly oriented: ** Step 1.b:7: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: list#(Cons(x,xs)) -> c_2(list#(xs)) - Signature: {goal/1,list/1,notEmpty/1,goal#/1,list#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0,isEmpty[Match]/1,c_1/1 ,c_2/1,c_3/0,c_4/0,c_5/0,c_6/0} - Obligation: innermost runtime complexity wrt. defined symbols {goal#,list#,notEmpty#} and constructors {Cons,False,Nil ,True,isEmpty[Match]} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))