WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil())) lt0(x,Nil()) -> False() lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs) lt0(Nil(),Cons(x',xs)) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) - Weak TRS: f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y)) f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs) g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y)) g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs) - Signature: {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0 ,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0 ,notEmpty,number4} and constructors {Cons,False,Nil,True} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil())) lt0(x,Nil()) -> False() lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs) lt0(Nil(),Cons(x',xs)) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) - Weak TRS: f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y)) f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs) g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y)) g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs) - Signature: {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0 ,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0 ,notEmpty,number4} and constructors {Cons,False,Nil,True} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: lt0(y,u){y -> Cons(x,y),u -> Cons(z,u)} = lt0(Cons(x,y),Cons(z,u)) ->^+ lt0(y,u) = C[lt0(y,u) = lt0(y,u){}] ** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil())) lt0(x,Nil()) -> False() lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs) lt0(Nil(),Cons(x',xs)) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) - Weak TRS: f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y)) f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs) g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y)) g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs) - Signature: {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0 ,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0 ,notEmpty,number4} and constructors {Cons,False,Nil,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(Cons) = {1,2}, uargs(f[Ite][False][Ite]) = {1}, uargs(g[Ite][False][Ite]) = {1} Following symbols are considered usable: {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4} TcT has computed the following interpretation: p(Cons) = x1 + x2 p(False) = 0 p(Nil) = 0 p(True) = 0 p(f) = 6 p(f[Ite][False][Ite]) = 6 + x1 p(g) = 0 p(g[Ite][False][Ite]) = x1 p(goal) = 6 + x2 p(lt0) = 0 p(notEmpty) = 3 p(number4) = 0 Following rules are strictly oriented: f(x,Nil()) = 6 > 0 = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) notEmpty(Cons(x,xs)) = 3 > 0 = True() notEmpty(Nil()) = 3 > 0 = False() Following rules are (at-least) weakly oriented: f(x,Cons(x',xs)) = 6 >= 6 = f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) f[Ite][False][Ite](False(),Cons(x,xs),y) = 6 >= 6 = f(xs,Cons(Cons(Nil(),Nil()),y)) f[Ite][False][Ite](True(),x',Cons(x,xs)) = 6 >= 6 = f(x',xs) g(x,Cons(x',xs)) = 0 >= 0 = g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g(x,Nil()) = 0 >= 0 = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) g[Ite][False][Ite](False(),Cons(x,xs),y) = 0 >= 0 = g(xs,Cons(Cons(Nil(),Nil()),y)) g[Ite][False][Ite](True(),x',Cons(x,xs)) = 0 >= 0 = g(x',xs) goal(x,y) = 6 + y >= 6 = Cons(f(x,y),Cons(g(x,y),Nil())) lt0(x,Nil()) = 0 >= 0 = False() lt0(Cons(x',xs'),Cons(x,xs)) = 0 >= 0 = lt0(xs',xs) lt0(Nil(),Cons(x',xs)) = 0 >= 0 = True() number4(n) = 0 >= 0 = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil())) lt0(x,Nil()) -> False() lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs) lt0(Nil(),Cons(x',xs)) -> True() number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) - Weak TRS: f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y)) f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs) g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y)) g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0 ,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0 ,notEmpty,number4} and constructors {Cons,False,Nil,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(Cons) = {1,2}, uargs(f[Ite][False][Ite]) = {1}, uargs(g[Ite][False][Ite]) = {1} Following symbols are considered usable: {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4} TcT has computed the following interpretation: p(Cons) = x1 + x2 p(False) = 0 p(Nil) = 0 p(True) = 0 p(f) = 0 p(f[Ite][False][Ite]) = 2*x1 p(g) = 2 + 6*x2 p(g[Ite][False][Ite]) = 2 + x1 + 6*x3 p(goal) = 6 + 6*x2 p(lt0) = 0 p(notEmpty) = 7 + x1 p(number4) = 4 Following rules are strictly oriented: g(x,Nil()) = 2 > 0 = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) goal(x,y) = 6 + 6*y > 2 + 6*y = Cons(f(x,y),Cons(g(x,y),Nil())) number4(n) = 4 > 0 = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) Following rules are (at-least) weakly oriented: f(x,Cons(x',xs)) = 0 >= 0 = f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) f(x,Nil()) = 0 >= 0 = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) f[Ite][False][Ite](False(),Cons(x,xs),y) = 0 >= 0 = f(xs,Cons(Cons(Nil(),Nil()),y)) f[Ite][False][Ite](True(),x',Cons(x,xs)) = 0 >= 0 = f(x',xs) g(x,Cons(x',xs)) = 2 + 6*x' + 6*xs >= 2 + 6*x' + 6*xs = g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g[Ite][False][Ite](False(),Cons(x,xs),y) = 2 + 6*y >= 2 + 6*y = g(xs,Cons(Cons(Nil(),Nil()),y)) g[Ite][False][Ite](True(),x',Cons(x,xs)) = 2 + 6*x + 6*xs >= 2 + 6*xs = g(x',xs) lt0(x,Nil()) = 0 >= 0 = False() lt0(Cons(x',xs'),Cons(x,xs)) = 0 >= 0 = lt0(xs',xs) lt0(Nil(),Cons(x',xs)) = 0 >= 0 = True() notEmpty(Cons(x,xs)) = 7 + x + xs >= 0 = True() notEmpty(Nil()) = 7 >= 0 = False() ** Step 1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs)) lt0(x,Nil()) -> False() lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs) lt0(Nil(),Cons(x',xs)) -> True() - Weak TRS: f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y)) f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs) g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y)) g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs) goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil())) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil())))) - Signature: {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0 ,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0 ,notEmpty,number4} and constructors {Cons,False,Nil,True} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 5, araRuleShifting = Nothing} + Details: Signatures used: ---------------- Cons :: ["A"(0) x "A"(3)] -(3)-> "A"(3) Cons :: ["A"(0) x "A"(4)] -(4)-> "A"(4) Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Cons :: ["A"(0) x "A"(1)] -(1)-> "A"(1) Cons :: ["A"(0) x "A"(6)] -(6)-> "A"(6) Cons :: ["A"(0) x "A"(9)] -(9)-> "A"(9) False :: [] -(0)-> "A"(0) False :: [] -(0)-> "A"(1) False :: [] -(0)-> "A"(10) Nil :: [] -(0)-> "A"(1) Nil :: [] -(0)-> "A"(0) Nil :: [] -(0)-> "A"(3) Nil :: [] -(0)-> "A"(4) Nil :: [] -(0)-> "A"(12) Nil :: [] -(0)-> "A"(8) Nil :: [] -(0)-> "A"(14) True :: [] -(0)-> "A"(0) True :: [] -(0)-> "A"(14) True :: [] -(0)-> "A"(12) f :: ["A"(6) x "A"(3)] -(4)-> "A"(0) f[Ite][False][Ite] :: ["A"(0) x "A"(6) x "A"(3)] -(1)-> "A"(0) g :: ["A"(9) x "A"(4)] -(8)-> "A"(0) g[Ite][False][Ite] :: ["A"(0) x "A"(9) x "A"(4)] -(4)-> "A"(0) goal :: ["A"(15) x "A"(15)] -(15)-> "A"(0) lt0 :: ["A"(0) x "A"(1)] -(1)-> "A"(1) notEmpty :: ["A"(4)] -(0)-> "A"(6) number4 :: ["A"(0)] -(15)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "Cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "False_A" :: [] -(0)-> "A"(1) "Nil_A" :: [] -(0)-> "A"(1) "True_A" :: [] -(0)-> "A"(1) WORST_CASE(Omega(n^1),O(n^1))