WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(z0,Cons(z1,z2)) -> c11(F(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) ,F[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) F(z0,Cons(z1,z2)) -> c12(F(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) ,F[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) F(z0,Nil()) -> c10() G(z0,Cons(z1,z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) G(z0,Nil()) -> c8() GOAL(z0,z1) -> c14(F(z0,z1)) GOAL(z0,z1) -> c15(G(z0,z1)) LT0(z0,Nil()) -> c7() LT0(Cons(z0,z1),Cons(z2,z3)) -> c6(LT0(z1,z3)) NUMBER42() -> c13() - Weak TRS: F[ITE][FALSE][ITE](False(),z0,z1) -> c4() F[ITE][FALSE][ITE](False(),Cons(z0,z1),z2) -> c2() F[ITE][FALSE][ITE](True(),z0,z1) -> c5() F[ITE][FALSE][ITE](True(),z0,Cons(z1,z2)) -> c3() G[ITE][FALSE][ITE](False(),Cons(z0,z1),z2) -> c(G(z1,Cons(Cons(Nil(),Nil()),z2))) G[ITE][FALSE][ITE](True(),z0,Cons(z1,z2)) -> c1(G(z0,z2)) f(z0,Cons(z1,z2)) -> f(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) f(z0,Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) f[Ite][False][Ite](False(),z0,z1) -> Cons(Cons(Nil(),Nil()),z1) f[Ite][False][Ite](False(),Cons(z0,z1),z2) -> z1 f[Ite][False][Ite](True(),z0,z1) -> z0 f[Ite][False][Ite](True(),z0,Cons(z1,z2)) -> z2 g(z0,Cons(z1,z2)) -> g[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) g(z0,Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) g[Ite][False][Ite](False(),Cons(z0,z1),z2) -> g(z1,Cons(Cons(Nil(),Nil()),z2)) g[Ite][False][Ite](True(),z0,Cons(z1,z2)) -> g(z0,z2) goal(z0,z1) -> Cons(f(z0,z1),Cons(g(z0,z1),Nil())) lt0(z0,Nil()) -> False() lt0(Cons(z0,z1),Cons(z2,z3)) -> lt0(z1,z3) number42() -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {F/2,F[ITE][FALSE][ITE]/3,G/2,GOAL/2,G[ITE][FALSE][ITE]/3,LT0/2,NUMBER42/0,f/2,f[Ite][False][Ite]/3,g/2 ,g[Ite][False][Ite]/3,goal/2,lt0/2,number42/0} / {Cons/2,False/0,Nil/0,True/0,c/1,c1/1,c10/0,c11/3,c12/3 ,c13/0,c14/1,c15/1,c2/0,c3/0,c4/0,c5/0,c6/1,c7/0,c8/0,c9/2} - Obligation: innermost runtime complexity wrt. defined symbols {F,F[ITE][FALSE][ITE],G,GOAL,G[ITE][FALSE][ITE],LT0 ,NUMBER42,f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,number42} and constructors {Cons,False,Nil,True ,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(z0,Cons(z1,z2)) -> c11(F(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) ,F[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) F(z0,Cons(z1,z2)) -> c12(F(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) ,F[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) F(z0,Nil()) -> c10() G(z0,Cons(z1,z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) G(z0,Nil()) -> c8() GOAL(z0,z1) -> c14(F(z0,z1)) GOAL(z0,z1) -> c15(G(z0,z1)) LT0(z0,Nil()) -> c7() LT0(Cons(z0,z1),Cons(z2,z3)) -> c6(LT0(z1,z3)) NUMBER42() -> c13() - Weak TRS: F[ITE][FALSE][ITE](False(),z0,z1) -> c4() F[ITE][FALSE][ITE](False(),Cons(z0,z1),z2) -> c2() F[ITE][FALSE][ITE](True(),z0,z1) -> c5() F[ITE][FALSE][ITE](True(),z0,Cons(z1,z2)) -> c3() G[ITE][FALSE][ITE](False(),Cons(z0,z1),z2) -> c(G(z1,Cons(Cons(Nil(),Nil()),z2))) G[ITE][FALSE][ITE](True(),z0,Cons(z1,z2)) -> c1(G(z0,z2)) f(z0,Cons(z1,z2)) -> f(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) f(z0,Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) f[Ite][False][Ite](False(),z0,z1) -> Cons(Cons(Nil(),Nil()),z1) f[Ite][False][Ite](False(),Cons(z0,z1),z2) -> z1 f[Ite][False][Ite](True(),z0,z1) -> z0 f[Ite][False][Ite](True(),z0,Cons(z1,z2)) -> z2 g(z0,Cons(z1,z2)) -> g[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) g(z0,Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) g[Ite][False][Ite](False(),Cons(z0,z1),z2) -> g(z1,Cons(Cons(Nil(),Nil()),z2)) g[Ite][False][Ite](True(),z0,Cons(z1,z2)) -> g(z0,z2) goal(z0,z1) -> Cons(f(z0,z1),Cons(g(z0,z1),Nil())) lt0(z0,Nil()) -> False() lt0(Cons(z0,z1),Cons(z2,z3)) -> lt0(z1,z3) number42() -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {F/2,F[ITE][FALSE][ITE]/3,G/2,GOAL/2,G[ITE][FALSE][ITE]/3,LT0/2,NUMBER42/0,f/2,f[Ite][False][Ite]/3,g/2 ,g[Ite][False][Ite]/3,goal/2,lt0/2,number42/0} / {Cons/2,False/0,Nil/0,True/0,c/1,c1/1,c10/0,c11/3,c12/3 ,c13/0,c14/1,c15/1,c2/0,c3/0,c4/0,c5/0,c6/1,c7/0,c8/0,c9/2} - Obligation: innermost runtime complexity wrt. defined symbols {F,F[ITE][FALSE][ITE],G,GOAL,G[ITE][FALSE][ITE],LT0 ,NUMBER42,f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,number42} and constructors {Cons,False,Nil,True ,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: F(z0,Cons(z1,z2)) -> c11(F(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) ,F[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) F(z0,Cons(z1,z2)) -> c12(F(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) ,F[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) F(z0,Nil()) -> c10() G(z0,Cons(z1,z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,LT0(z0,Cons(Nil(),Nil()))) G(z0,Nil()) -> c8() GOAL(z0,z1) -> c14(F(z0,z1)) GOAL(z0,z1) -> c15(G(z0,z1)) LT0(z0,Nil()) -> c7() LT0(Cons(z0,z1),Cons(z2,z3)) -> c6(LT0(z1,z3)) NUMBER42() -> c13() - Weak TRS: F[ITE][FALSE][ITE](False(),z0,z1) -> c4() F[ITE][FALSE][ITE](False(),Cons(z0,z1),z2) -> c2() F[ITE][FALSE][ITE](True(),z0,z1) -> c5() F[ITE][FALSE][ITE](True(),z0,Cons(z1,z2)) -> c3() G[ITE][FALSE][ITE](False(),Cons(z0,z1),z2) -> c(G(z1,Cons(Cons(Nil(),Nil()),z2))) G[ITE][FALSE][ITE](True(),z0,Cons(z1,z2)) -> c1(G(z0,z2)) f(z0,Cons(z1,z2)) -> f(f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) ,f[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2))) f(z0,Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) f[Ite][False][Ite](False(),z0,z1) -> Cons(Cons(Nil(),Nil()),z1) f[Ite][False][Ite](False(),Cons(z0,z1),z2) -> z1 f[Ite][False][Ite](True(),z0,z1) -> z0 f[Ite][False][Ite](True(),z0,Cons(z1,z2)) -> z2 g(z0,Cons(z1,z2)) -> g[Ite][False][Ite](lt0(z0,Cons(Nil(),Nil())),z0,Cons(z1,z2)) g(z0,Nil()) -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) g[Ite][False][Ite](False(),Cons(z0,z1),z2) -> g(z1,Cons(Cons(Nil(),Nil()),z2)) g[Ite][False][Ite](True(),z0,Cons(z1,z2)) -> g(z0,z2) goal(z0,z1) -> Cons(f(z0,z1),Cons(g(z0,z1),Nil())) lt0(z0,Nil()) -> False() lt0(Cons(z0,z1),Cons(z2,z3)) -> lt0(z1,z3) number42() -> Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Cons(Nil() ,Nil())))))))))))))))))))))))))))))))))))))))))) - Signature: {F/2,F[ITE][FALSE][ITE]/3,G/2,GOAL/2,G[ITE][FALSE][ITE]/3,LT0/2,NUMBER42/0,f/2,f[Ite][False][Ite]/3,g/2 ,g[Ite][False][Ite]/3,goal/2,lt0/2,number42/0} / {Cons/2,False/0,Nil/0,True/0,c/1,c1/1,c10/0,c11/3,c12/3 ,c13/0,c14/1,c15/1,c2/0,c3/0,c4/0,c5/0,c6/1,c7/0,c8/0,c9/2} - Obligation: innermost runtime complexity wrt. defined symbols {F,F[ITE][FALSE][ITE],G,GOAL,G[ITE][FALSE][ITE],LT0 ,NUMBER42,f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,number42} and constructors {Cons,False,Nil,True ,c,c1,c10,c11,c12,c13,c14,c15,c2,c3,c4,c5,c6,c7,c8,c9} + 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)) ->^+ c6(LT0(y,u)) = C[LT0(y,u) = LT0(y,u){}] WORST_CASE(Omega(n^1),?)