* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) -> plus_x#1(x3,comp_f_g#1(x1,x2,0()))
comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0())
foldr#3(Cons(x32,x6)) -> comp_f_g(x32,foldr#3(x6))
foldr#3(Nil()) -> id()
foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24)
foldr_f#3(Nil(),0()) -> 0()
main(x3) -> foldr_f#3(map#2(x3),0())
map#2(Cons(x16,x6)) -> Cons(plus_x(x16),map#2(x6))
map#2(Nil()) -> Nil()
plus_x#1(0(),x6) -> x6
plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10))
- Signature:
{comp_f_g#1/3,foldr#3/1,foldr_f#3/2,main/1,map#2/1,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,id/0
,plus_x/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {comp_f_g#1,foldr#3,foldr_f#3,main,map#2
,plus_x#1} and constructors {0,Cons,Nil,S,comp_f_g,id,plus_x}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) -> plus_x#1(x3,comp_f_g#1(x1,x2,0()))
comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0())
foldr#3(Cons(x32,x6)) -> comp_f_g(x32,foldr#3(x6))
foldr#3(Nil()) -> id()
foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24)
foldr_f#3(Nil(),0()) -> 0()
main(x3) -> foldr_f#3(map#2(x3),0())
map#2(Cons(x16,x6)) -> Cons(plus_x(x16),map#2(x6))
map#2(Nil()) -> Nil()
plus_x#1(0(),x6) -> x6
plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10))
- Signature:
{comp_f_g#1/3,foldr#3/1,foldr_f#3/2,main/1,map#2/1,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,id/0
,plus_x/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {comp_f_g#1,foldr#3,foldr_f#3,main,map#2
,plus_x#1} and constructors {0,Cons,Nil,S,comp_f_g,id,plus_x}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
foldr#3(y){y -> Cons(x,y)} =
foldr#3(Cons(x,y)) ->^+ comp_f_g(x,foldr#3(y))
= C[foldr#3(y) = foldr#3(y){}]
** Step 1.b:1: Bounds WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) -> plus_x#1(x3,comp_f_g#1(x1,x2,0()))
comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0())
foldr#3(Cons(x32,x6)) -> comp_f_g(x32,foldr#3(x6))
foldr#3(Nil()) -> id()
foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24)
foldr_f#3(Nil(),0()) -> 0()
main(x3) -> foldr_f#3(map#2(x3),0())
map#2(Cons(x16,x6)) -> Cons(plus_x(x16),map#2(x6))
map#2(Nil()) -> Nil()
plus_x#1(0(),x6) -> x6
plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10))
- Signature:
{comp_f_g#1/3,foldr#3/1,foldr_f#3/2,main/1,map#2/1,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,id/0
,plus_x/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {comp_f_g#1,foldr#3,foldr_f#3,main,map#2
,plus_x#1} and constructors {0,Cons,Nil,S,comp_f_g,id,plus_x}
+ Applied Processor:
Bounds {initialAutomaton = minimal, enrichment = match}
+ Details:
The problem is match-bounded by 2.
The enriched problem is compatible with follwoing automaton.
0_0() -> 1
0_0() -> 2
0_0() -> 8
0_0() -> 10
0_1() -> 1
0_1() -> 3
0_1() -> 4
0_1() -> 10
0_2() -> 1
0_2() -> 10
Cons_0(2,2) -> 1
Cons_0(2,2) -> 2
Cons_0(2,2) -> 8
Cons_0(2,2) -> 10
Cons_1(7,6) -> 1
Cons_1(7,6) -> 6
Cons_1(7,6) -> 10
Nil_0() -> 1
Nil_0() -> 2
Nil_0() -> 8
Nil_0() -> 10
Nil_1() -> 1
Nil_1() -> 6
Nil_1() -> 10
S_0(2) -> 1
S_0(2) -> 2
S_0(2) -> 8
S_0(2) -> 10
S_1(1) -> 1
S_1(1) -> 10
S_1(3) -> 1
S_1(3) -> 3
S_1(3) -> 10
S_1(8) -> 1
S_1(8) -> 8
S_1(8) -> 10
comp_f_g_0(2,2) -> 1
comp_f_g_0(2,2) -> 2
comp_f_g_0(2,2) -> 8
comp_f_g_0(2,2) -> 10
comp_f_g_1(2,5) -> 1
comp_f_g_1(2,5) -> 5
comp_f_g_1(2,5) -> 10
comp_f_g_2(7,9) -> 9
comp_f_g#1_0(2,2,2) -> 1
comp_f_g#1_0(2,2,2) -> 10
comp_f_g#1_1(2,2,4) -> 1
comp_f_g#1_1(2,2,4) -> 3
comp_f_g#1_1(2,2,4) -> 10
comp_f_g#1_1(2,5,2) -> 1
comp_f_g#1_1(2,5,2) -> 10
comp_f_g#1_1(2,5,4) -> 1
comp_f_g#1_1(2,5,4) -> 3
comp_f_g#1_1(2,5,4) -> 10
comp_f_g#1_1(7,9,10) -> 1
comp_f_g#1_1(7,9,10) -> 10
comp_f_g#1_2(7,9,1) -> 1
comp_f_g#1_2(7,9,1) -> 10
comp_f_g#1_2(7,9,4) -> 1
comp_f_g#1_2(7,9,4) -> 10
foldr#3_0(2) -> 1
foldr#3_0(2) -> 10
foldr#3_1(2) -> 5
foldr#3_2(6) -> 9
foldr_f#3_0(2,2) -> 1
foldr_f#3_0(2,2) -> 10
foldr_f#3_1(6,4) -> 1
foldr_f#3_1(6,4) -> 10
id_0() -> 1
id_0() -> 2
id_0() -> 8
id_0() -> 10
id_1() -> 1
id_1() -> 5
id_1() -> 10
id_2() -> 9
main_0(2) -> 1
main_0(2) -> 10
map#2_0(2) -> 1
map#2_0(2) -> 10
map#2_1(2) -> 6
plus_x_0(2) -> 1
plus_x_0(2) -> 2
plus_x_0(2) -> 8
plus_x_0(2) -> 10
plus_x_1(2) -> 7
plus_x#1_0(2,2) -> 1
plus_x#1_0(2,2) -> 10
plus_x#1_1(2,1) -> 1
plus_x#1_1(2,1) -> 10
plus_x#1_1(2,2) -> 8
plus_x#1_1(2,3) -> 1
plus_x#1_1(2,3) -> 3
plus_x#1_1(2,3) -> 10
plus_x#1_1(2,4) -> 1
plus_x#1_1(2,4) -> 3
plus_x#1_1(2,4) -> 10
plus_x#1_1(2,10) -> 1
plus_x#1_1(2,10) -> 10
plus_x#1_2(2,1) -> 1
plus_x#1_2(2,1) -> 10
plus_x#1_2(2,10) -> 1
plus_x#1_2(2,10) -> 10
1 -> 10
2 -> 1
2 -> 8
2 -> 10
3 -> 1
3 -> 10
4 -> 1
4 -> 3
4 -> 10
10 -> 1
** Step 1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
comp_f_g#1(plus_x(x3),comp_f_g(x1,x2),0()) -> plus_x#1(x3,comp_f_g#1(x1,x2,0()))
comp_f_g#1(plus_x(x3),id(),0()) -> plus_x#1(x3,0())
foldr#3(Cons(x32,x6)) -> comp_f_g(x32,foldr#3(x6))
foldr#3(Nil()) -> id()
foldr_f#3(Cons(x16,x5),x24) -> comp_f_g#1(x16,foldr#3(x5),x24)
foldr_f#3(Nil(),0()) -> 0()
main(x3) -> foldr_f#3(map#2(x3),0())
map#2(Cons(x16,x6)) -> Cons(plus_x(x16),map#2(x6))
map#2(Nil()) -> Nil()
plus_x#1(0(),x6) -> x6
plus_x#1(S(x8),x10) -> S(plus_x#1(x8,x10))
- Signature:
{comp_f_g#1/3,foldr#3/1,foldr_f#3/2,main/1,map#2/1,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,comp_f_g/2,id/0
,plus_x/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {comp_f_g#1,foldr#3,foldr_f#3,main,map#2
,plus_x#1} and constructors {0,Cons,Nil,S,comp_f_g,id,plus_x}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))