WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
foldr#3(Cons(x16,x6)) -> step_x_f(rev_l(),x16,foldr#3(x6))
foldr#3(Nil()) -> fleft_op_e_xs_1()
main(Cons(x8,x9)) -> step_x_f#1(rev_l(),x8,foldr#3(x9),Nil())
main(Nil()) -> Nil()
rev_l#2(x8,x10) -> Cons(x10,x8)
step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) -> rev_l#2(x3,x5)
step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) -> step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))
- Signature:
{foldr#3/1,main/1,rev_l#2/2,step_x_f#1/4} / {Cons/2,Nil/0,fleft_op_e_xs_1/0,rev_l/0,step_x_f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {foldr#3,main,rev_l#2,step_x_f#1} and constructors {Cons
,Nil,fleft_op_e_xs_1,rev_l,step_x_f}
+ 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(step_x_f) = {3},
uargs(step_x_f#1) = {3,4}
Following symbols are considered usable:
{foldr#3,main,rev_l#2,step_x_f#1}
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [2]
p(Nil) = [5]
p(fleft_op_e_xs_1) = [6]
p(foldr#3) = [2] x1 + [0]
p(main) = [3] x1 + [0]
p(rev_l) = [2]
p(rev_l#2) = [1] x1 + [2]
p(step_x_f) = [1] x3 + [4]
p(step_x_f#1) = [1] x3 + [1] x4 + [0]
Following rules are strictly oriented:
foldr#3(Nil()) = [10]
> [6]
= fleft_op_e_xs_1()
main(Cons(x8,x9)) = [3] x9 + [6]
> [2] x9 + [5]
= step_x_f#1(rev_l(),x8,foldr#3(x9),Nil())
main(Nil()) = [15]
> [5]
= Nil()
step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) = [1] x3 + [6]
> [1] x3 + [2]
= rev_l#2(x3,x5)
step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) = [1] x1 + [1] x4 + [4]
> [1] x1 + [1] x4 + [2]
= step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))
Following rules are (at-least) weakly oriented:
foldr#3(Cons(x16,x6)) = [2] x6 + [4]
>= [2] x6 + [4]
= step_x_f(rev_l(),x16,foldr#3(x6))
rev_l#2(x8,x10) = [1] x8 + [2]
>= [1] x8 + [2]
= Cons(x10,x8)
* Step 2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
foldr#3(Cons(x16,x6)) -> step_x_f(rev_l(),x16,foldr#3(x6))
rev_l#2(x8,x10) -> Cons(x10,x8)
- Weak TRS:
foldr#3(Nil()) -> fleft_op_e_xs_1()
main(Cons(x8,x9)) -> step_x_f#1(rev_l(),x8,foldr#3(x9),Nil())
main(Nil()) -> Nil()
step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) -> rev_l#2(x3,x5)
step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) -> step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))
- Signature:
{foldr#3/1,main/1,rev_l#2/2,step_x_f#1/4} / {Cons/2,Nil/0,fleft_op_e_xs_1/0,rev_l/0,step_x_f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {foldr#3,main,rev_l#2,step_x_f#1} and constructors {Cons
,Nil,fleft_op_e_xs_1,rev_l,step_x_f}
+ 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(step_x_f) = {3},
uargs(step_x_f#1) = {3,4}
Following symbols are considered usable:
{foldr#3,main,rev_l#2,step_x_f#1}
TcT has computed the following interpretation:
p(Cons) = 6 + x2
p(Nil) = 0
p(fleft_op_e_xs_1) = 0
p(foldr#3) = x1
p(main) = 6 + 4*x1
p(rev_l) = 6
p(rev_l#2) = 8 + x1
p(step_x_f) = x1 + x3
p(step_x_f#1) = 1 + 3*x1 + 4*x3 + x4
Following rules are strictly oriented:
rev_l#2(x8,x10) = 8 + x8
> 6 + x8
= Cons(x10,x8)
Following rules are (at-least) weakly oriented:
foldr#3(Cons(x16,x6)) = 6 + x6
>= 6 + x6
= step_x_f(rev_l(),x16,foldr#3(x6))
foldr#3(Nil()) = 0
>= 0
= fleft_op_e_xs_1()
main(Cons(x8,x9)) = 30 + 4*x9
>= 19 + 4*x9
= step_x_f#1(rev_l(),x8,foldr#3(x9),Nil())
main(Nil()) = 6
>= 0
= Nil()
step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) = 19 + x3
>= 8 + x3
= rev_l#2(x3,x5)
step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) = 19 + x1 + 4*x2 + 4*x4
>= 9 + x1 + 3*x2 + 4*x4
= step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))
* Step 3: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
foldr#3(Cons(x16,x6)) -> step_x_f(rev_l(),x16,foldr#3(x6))
- Weak TRS:
foldr#3(Nil()) -> fleft_op_e_xs_1()
main(Cons(x8,x9)) -> step_x_f#1(rev_l(),x8,foldr#3(x9),Nil())
main(Nil()) -> Nil()
rev_l#2(x8,x10) -> Cons(x10,x8)
step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) -> rev_l#2(x3,x5)
step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) -> step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))
- Signature:
{foldr#3/1,main/1,rev_l#2/2,step_x_f#1/4} / {Cons/2,Nil/0,fleft_op_e_xs_1/0,rev_l/0,step_x_f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {foldr#3,main,rev_l#2,step_x_f#1} and constructors {Cons
,Nil,fleft_op_e_xs_1,rev_l,step_x_f}
+ 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(step_x_f) = {3},
uargs(step_x_f#1) = {3,4}
Following symbols are considered usable:
{foldr#3,main,rev_l#2,step_x_f#1}
TcT has computed the following interpretation:
p(Cons) = [1] x2 + [4]
p(Nil) = [2]
p(fleft_op_e_xs_1) = [4]
p(foldr#3) = [1] x1 + [4]
p(main) = [4] x1 + [6]
p(rev_l) = [2]
p(rev_l#2) = [1] x1 + [4]
p(step_x_f) = [1] x1 + [1] x3 + [0]
p(step_x_f#1) = [2] x1 + [4] x3 + [1] x4 + [0]
Following rules are strictly oriented:
foldr#3(Cons(x16,x6)) = [1] x6 + [8]
> [1] x6 + [6]
= step_x_f(rev_l(),x16,foldr#3(x6))
Following rules are (at-least) weakly oriented:
foldr#3(Nil()) = [6]
>= [4]
= fleft_op_e_xs_1()
main(Cons(x8,x9)) = [4] x9 + [22]
>= [4] x9 + [22]
= step_x_f#1(rev_l(),x8,foldr#3(x9),Nil())
main(Nil()) = [14]
>= [2]
= Nil()
rev_l#2(x8,x10) = [1] x8 + [4]
>= [1] x8 + [4]
= Cons(x10,x8)
step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) = [1] x3 + [20]
>= [1] x3 + [4]
= rev_l#2(x3,x5)
step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) = [1] x1 + [4] x2 + [4] x4 + [4]
>= [1] x1 + [2] x2 + [4] x4 + [4]
= step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
foldr#3(Cons(x16,x6)) -> step_x_f(rev_l(),x16,foldr#3(x6))
foldr#3(Nil()) -> fleft_op_e_xs_1()
main(Cons(x8,x9)) -> step_x_f#1(rev_l(),x8,foldr#3(x9),Nil())
main(Nil()) -> Nil()
rev_l#2(x8,x10) -> Cons(x10,x8)
step_x_f#1(rev_l(),x5,fleft_op_e_xs_1(),x3) -> rev_l#2(x3,x5)
step_x_f#1(rev_l(),x5,step_x_f(x2,x3,x4),x1) -> step_x_f#1(x2,x3,x4,rev_l#2(x1,x5))
- Signature:
{foldr#3/1,main/1,rev_l#2/2,step_x_f#1/4} / {Cons/2,Nil/0,fleft_op_e_xs_1/0,rev_l/0,step_x_f/3}
- Obligation:
innermost runtime complexity wrt. defined symbols {foldr#3,main,rev_l#2,step_x_f#1} and constructors {Cons
,Nil,fleft_op_e_xs_1,rev_l,step_x_f}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))