WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: +FULL(0(),z0) -> c10() +FULL(S(z0),z1) -> c9(+FULL(z0,S(z1))) F(z0) -> c8(*'(z0,z0)) GOAL(z0) -> c7(MAP(z0)) MAP(Cons(z0,z1)) -> c4(F(z0)) MAP(Cons(z0,z1)) -> c5(MAP(z1)) MAP(Nil()) -> c6() - Weak TRS: *(z0,0()) -> 0() *(z0,S(0())) -> z0 *(z0,S(S(z1))) -> +(z0,*(z0,S(z1))) *(0(),z0) -> 0() *'(z0,0()) -> c2() *'(z0,S(0())) -> c1() *'(z0,S(S(z1))) -> c(*'(z0,S(z1))) *'(0(),z0) -> c3() +Full(0(),z0) -> z0 +Full(S(z0),z1) -> +Full(z0,S(z1)) f(z0) -> *(z0,z0) goal(z0) -> map(z0) map(Cons(z0,z1)) -> Cons(f(z0),map(z1)) map(Nil()) -> Nil() - Signature: {*/2,*'/2,+FULL/2,+Full/2,F/1,GOAL/1,MAP/1,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c/1,c1/0,c10/0,c2/0 ,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+FULL,+Full,F,GOAL,MAP,f,goal ,map} and constructors {+,0,Cons,Nil,S,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: +FULL(0(),z0) -> c10() +FULL(S(z0),z1) -> c9(+FULL(z0,S(z1))) F(z0) -> c8(*'(z0,z0)) GOAL(z0) -> c7(MAP(z0)) MAP(Cons(z0,z1)) -> c4(F(z0)) MAP(Cons(z0,z1)) -> c5(MAP(z1)) MAP(Nil()) -> c6() - Weak TRS: *(z0,0()) -> 0() *(z0,S(0())) -> z0 *(z0,S(S(z1))) -> +(z0,*(z0,S(z1))) *(0(),z0) -> 0() *'(z0,0()) -> c2() *'(z0,S(0())) -> c1() *'(z0,S(S(z1))) -> c(*'(z0,S(z1))) *'(0(),z0) -> c3() +Full(0(),z0) -> z0 +Full(S(z0),z1) -> +Full(z0,S(z1)) f(z0) -> *(z0,z0) goal(z0) -> map(z0) map(Cons(z0,z1)) -> Cons(f(z0),map(z1)) map(Nil()) -> Nil() - Signature: {*/2,*'/2,+FULL/2,+Full/2,F/1,GOAL/1,MAP/1,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c/1,c1/0,c10/0,c2/0 ,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+FULL,+Full,F,GOAL,MAP,f,goal ,map} and constructors {+,0,Cons,Nil,S,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: +FULL(0(),z0) -> c10() +FULL(S(z0),z1) -> c9(+FULL(z0,S(z1))) F(z0) -> c8(*'(z0,z0)) GOAL(z0) -> c7(MAP(z0)) MAP(Cons(z0,z1)) -> c4(F(z0)) MAP(Cons(z0,z1)) -> c5(MAP(z1)) MAP(Nil()) -> c6() - Weak TRS: *(z0,0()) -> 0() *(z0,S(0())) -> z0 *(z0,S(S(z1))) -> +(z0,*(z0,S(z1))) *(0(),z0) -> 0() *'(z0,0()) -> c2() *'(z0,S(0())) -> c1() *'(z0,S(S(z1))) -> c(*'(z0,S(z1))) *'(0(),z0) -> c3() +Full(0(),z0) -> z0 +Full(S(z0),z1) -> +Full(z0,S(z1)) f(z0) -> *(z0,z0) goal(z0) -> map(z0) map(Cons(z0,z1)) -> Cons(f(z0),map(z1)) map(Nil()) -> Nil() - Signature: {*/2,*'/2,+FULL/2,+Full/2,F/1,GOAL/1,MAP/1,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c/1,c1/0,c10/0,c2/0 ,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+FULL,+Full,F,GOAL,MAP,f,goal ,map} and constructors {+,0,Cons,Nil,S,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: +FULL(x,y){x -> S(x)} = +FULL(S(x),y) ->^+ c9(+FULL(x,S(y))) = C[+FULL(x,S(y)) = +FULL(x,y){y -> S(y)}] ** Step 1.b:1: NaturalPI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: +FULL(0(),z0) -> c10() +FULL(S(z0),z1) -> c9(+FULL(z0,S(z1))) F(z0) -> c8(*'(z0,z0)) GOAL(z0) -> c7(MAP(z0)) MAP(Cons(z0,z1)) -> c4(F(z0)) MAP(Cons(z0,z1)) -> c5(MAP(z1)) MAP(Nil()) -> c6() - Weak TRS: *(z0,0()) -> 0() *(z0,S(0())) -> z0 *(z0,S(S(z1))) -> +(z0,*(z0,S(z1))) *(0(),z0) -> 0() *'(z0,0()) -> c2() *'(z0,S(0())) -> c1() *'(z0,S(S(z1))) -> c(*'(z0,S(z1))) *'(0(),z0) -> c3() +Full(0(),z0) -> z0 +Full(S(z0),z1) -> +Full(z0,S(z1)) f(z0) -> *(z0,z0) goal(z0) -> map(z0) map(Cons(z0,z1)) -> Cons(f(z0),map(z1)) map(Nil()) -> Nil() - Signature: {*/2,*'/2,+FULL/2,+Full/2,F/1,GOAL/1,MAP/1,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c/1,c1/0,c10/0,c2/0 ,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+FULL,+Full,F,GOAL,MAP,f,goal ,map} and constructors {+,0,Cons,Nil,S,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + 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(+) = {2}, uargs(Cons) = {1,2}, uargs(c) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1} Following symbols are considered usable: {*,*',+FULL,+Full,F,GOAL,MAP,f,goal,map} TcT has computed the following interpretation: p(*) = 1 + 4*x1 p(*') = 1 p(+) = x2 p(+FULL) = 2*x1 + x2 p(+Full) = 1 + x1 + x2 p(0) = 1 p(Cons) = 2 + x1 + x2 p(F) = 4 + x1 p(GOAL) = 6 + 4*x1 p(MAP) = 3 + 4*x1 p(Nil) = 0 p(S) = 4 + x1 p(c) = x1 p(c1) = 1 p(c10) = 0 p(c2) = 0 p(c3) = 0 p(c4) = 7 + x1 p(c5) = 4 + x1 p(c6) = 0 p(c7) = x1 p(c8) = x1 p(c9) = 3 + x1 p(f) = 2 + 4*x1 p(goal) = 5 + 5*x1 p(map) = 2 + 5*x1 Following rules are strictly oriented: +FULL(0(),z0) = 2 + z0 > 0 = c10() +FULL(S(z0),z1) = 8 + 2*z0 + z1 > 7 + 2*z0 + z1 = c9(+FULL(z0,S(z1))) F(z0) = 4 + z0 > 1 = c8(*'(z0,z0)) GOAL(z0) = 6 + 4*z0 > 3 + 4*z0 = c7(MAP(z0)) MAP(Cons(z0,z1)) = 11 + 4*z0 + 4*z1 > 7 + 4*z1 = c5(MAP(z1)) MAP(Nil()) = 3 > 0 = c6() Following rules are (at-least) weakly oriented: *(z0,0()) = 1 + 4*z0 >= 1 = 0() *(z0,S(0())) = 1 + 4*z0 >= z0 = z0 *(z0,S(S(z1))) = 1 + 4*z0 >= 1 + 4*z0 = +(z0,*(z0,S(z1))) *(0(),z0) = 5 >= 1 = 0() *'(z0,0()) = 1 >= 0 = c2() *'(z0,S(0())) = 1 >= 1 = c1() *'(z0,S(S(z1))) = 1 >= 1 = c(*'(z0,S(z1))) *'(0(),z0) = 1 >= 0 = c3() +Full(0(),z0) = 2 + z0 >= z0 = z0 +Full(S(z0),z1) = 5 + z0 + z1 >= 5 + z0 + z1 = +Full(z0,S(z1)) MAP(Cons(z0,z1)) = 11 + 4*z0 + 4*z1 >= 11 + z0 = c4(F(z0)) f(z0) = 2 + 4*z0 >= 1 + 4*z0 = *(z0,z0) goal(z0) = 5 + 5*z0 >= 2 + 5*z0 = map(z0) map(Cons(z0,z1)) = 12 + 5*z0 + 5*z1 >= 6 + 4*z0 + 5*z1 = Cons(f(z0),map(z1)) map(Nil()) = 2 >= 0 = Nil() ** Step 1.b:2: NaturalPI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: MAP(Cons(z0,z1)) -> c4(F(z0)) - Weak TRS: *(z0,0()) -> 0() *(z0,S(0())) -> z0 *(z0,S(S(z1))) -> +(z0,*(z0,S(z1))) *(0(),z0) -> 0() *'(z0,0()) -> c2() *'(z0,S(0())) -> c1() *'(z0,S(S(z1))) -> c(*'(z0,S(z1))) *'(0(),z0) -> c3() +FULL(0(),z0) -> c10() +FULL(S(z0),z1) -> c9(+FULL(z0,S(z1))) +Full(0(),z0) -> z0 +Full(S(z0),z1) -> +Full(z0,S(z1)) F(z0) -> c8(*'(z0,z0)) GOAL(z0) -> c7(MAP(z0)) MAP(Cons(z0,z1)) -> c5(MAP(z1)) MAP(Nil()) -> c6() f(z0) -> *(z0,z0) goal(z0) -> map(z0) map(Cons(z0,z1)) -> Cons(f(z0),map(z1)) map(Nil()) -> Nil() - Signature: {*/2,*'/2,+FULL/2,+Full/2,F/1,GOAL/1,MAP/1,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c/1,c1/0,c10/0,c2/0 ,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+FULL,+Full,F,GOAL,MAP,f,goal ,map} and constructors {+,0,Cons,Nil,S,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + 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(+) = {2}, uargs(Cons) = {1,2}, uargs(c) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1} Following symbols are considered usable: {*,*',+FULL,+Full,F,GOAL,MAP,f,goal,map} TcT has computed the following interpretation: p(*) = x1 p(*') = 2 + x1 + x2 p(+) = x2 p(+FULL) = 2 + 3*x1 + 2*x2 p(+Full) = 4*x1 + 4*x2 p(0) = 0 p(Cons) = 1 + x1 + x2 p(F) = 2 + 4*x1 p(GOAL) = 4 + 5*x1 p(MAP) = 4*x1 p(Nil) = 1 p(S) = 2 + x1 p(c) = 2 + x1 p(c1) = 1 p(c10) = 0 p(c2) = 1 p(c3) = 2 p(c4) = x1 p(c5) = x1 p(c6) = 0 p(c7) = 3 + x1 p(c8) = x1 p(c9) = x1 p(f) = x1 p(goal) = 2*x1 p(map) = x1 Following rules are strictly oriented: MAP(Cons(z0,z1)) = 4 + 4*z0 + 4*z1 > 2 + 4*z0 = c4(F(z0)) Following rules are (at-least) weakly oriented: *(z0,0()) = z0 >= 0 = 0() *(z0,S(0())) = z0 >= z0 = z0 *(z0,S(S(z1))) = z0 >= z0 = +(z0,*(z0,S(z1))) *(0(),z0) = 0 >= 0 = 0() *'(z0,0()) = 2 + z0 >= 1 = c2() *'(z0,S(0())) = 4 + z0 >= 1 = c1() *'(z0,S(S(z1))) = 6 + z0 + z1 >= 6 + z0 + z1 = c(*'(z0,S(z1))) *'(0(),z0) = 2 + z0 >= 2 = c3() +FULL(0(),z0) = 2 + 2*z0 >= 0 = c10() +FULL(S(z0),z1) = 8 + 3*z0 + 2*z1 >= 6 + 3*z0 + 2*z1 = c9(+FULL(z0,S(z1))) +Full(0(),z0) = 4*z0 >= z0 = z0 +Full(S(z0),z1) = 8 + 4*z0 + 4*z1 >= 8 + 4*z0 + 4*z1 = +Full(z0,S(z1)) F(z0) = 2 + 4*z0 >= 2 + 2*z0 = c8(*'(z0,z0)) GOAL(z0) = 4 + 5*z0 >= 3 + 4*z0 = c7(MAP(z0)) MAP(Cons(z0,z1)) = 4 + 4*z0 + 4*z1 >= 4*z1 = c5(MAP(z1)) MAP(Nil()) = 4 >= 0 = c6() f(z0) = z0 >= z0 = *(z0,z0) goal(z0) = 2*z0 >= z0 = map(z0) map(Cons(z0,z1)) = 1 + z0 + z1 >= 1 + z0 + z1 = Cons(f(z0),map(z1)) map(Nil()) = 1 >= 1 = Nil() ** Step 1.b:3: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: *(z0,0()) -> 0() *(z0,S(0())) -> z0 *(z0,S(S(z1))) -> +(z0,*(z0,S(z1))) *(0(),z0) -> 0() *'(z0,0()) -> c2() *'(z0,S(0())) -> c1() *'(z0,S(S(z1))) -> c(*'(z0,S(z1))) *'(0(),z0) -> c3() +FULL(0(),z0) -> c10() +FULL(S(z0),z1) -> c9(+FULL(z0,S(z1))) +Full(0(),z0) -> z0 +Full(S(z0),z1) -> +Full(z0,S(z1)) F(z0) -> c8(*'(z0,z0)) GOAL(z0) -> c7(MAP(z0)) MAP(Cons(z0,z1)) -> c4(F(z0)) MAP(Cons(z0,z1)) -> c5(MAP(z1)) MAP(Nil()) -> c6() f(z0) -> *(z0,z0) goal(z0) -> map(z0) map(Cons(z0,z1)) -> Cons(f(z0),map(z1)) map(Nil()) -> Nil() - Signature: {*/2,*'/2,+FULL/2,+Full/2,F/1,GOAL/1,MAP/1,f/1,goal/1,map/1} / {+/2,0/0,Cons/2,Nil/0,S/1,c/1,c1/0,c10/0,c2/0 ,c3/0,c4/1,c5/1,c6/0,c7/1,c8/1,c9/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,*',+FULL,+Full,F,GOAL,MAP,f,goal ,map} and constructors {+,0,Cons,Nil,S,c,c1,c10,c2,c3,c4,c5,c6,c7,c8,c9} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))