*** 1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
main(x5,x12) -> map#2(plus_x(x12),x5)
map#2(plus_x(x2),Nil()) -> Nil()
map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2))
plus_x#1(0(),x8) -> x8
plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14))
Weak DP Rules:
Weak TRS Rules:
Signature:
{main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1}
Obligation:
Innermost
basic terms: {main,map#2,plus_x#1}/{0,Cons,Nil,S,plus_x}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(Cons) = {1,2},
uargs(S) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [1]
p(Cons) = [1] x1 + [1] x2 + [6]
p(Nil) = [10]
p(S) = [1] x1 + [1]
p(main) = [2] x1 + [13]
p(map#2) = [1] x1 + [2] x2 + [5]
p(plus_x) = [4]
p(plus_x#1) = [2] x2 + [4]
Following rules are strictly oriented:
main(x5,x12) = [2] x5 + [13]
> [2] x5 + [9]
= map#2(plus_x(x12),x5)
map#2(plus_x(x2),Nil()) = [29]
> [10]
= Nil()
map#2(plus_x(x6),Cons(x4,x2)) = [2] x2 + [2] x4 + [21]
> [2] x2 + [2] x4 + [19]
= Cons(plus_x#1(x6,x4)
,map#2(plus_x(x6),x2))
plus_x#1(0(),x8) = [2] x8 + [4]
> [1] x8 + [0]
= x8
Following rules are (at-least) weakly oriented:
plus_x#1(S(x12),x14) = [2] x14 + [4]
>= [2] x14 + [5]
= S(plus_x#1(x12,x14))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14))
Weak DP Rules:
Weak TRS Rules:
main(x5,x12) -> map#2(plus_x(x12),x5)
map#2(plus_x(x2),Nil()) -> Nil()
map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2))
plus_x#1(0(),x8) -> x8
Signature:
{main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1}
Obligation:
Innermost
basic terms: {main,map#2,plus_x#1}/{0,Cons,Nil,S,plus_x}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
Proof:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(Cons) = {1,2},
uargs(S) = {1}
Following symbols are considered usable:
{main,map#2,plus_x#1}
TcT has computed the following interpretation:
p(0) = 1
p(Cons) = 1 + x1 + x2
p(Nil) = 1
p(S) = 1 + x1
p(main) = 5*x1 + 4*x1*x2 + 4*x1^2 + 4*x2 + 6*x2^2
p(map#2) = x1 + 2*x1*x2 + 4*x1^2 + 3*x2 + 2*x2^2
p(plus_x) = x1
p(plus_x#1) = 2*x1 + x2
Following rules are strictly oriented:
plus_x#1(S(x12),x14) = 2 + 2*x12 + x14
> 1 + 2*x12 + x14
= S(plus_x#1(x12,x14))
Following rules are (at-least) weakly oriented:
main(x5,x12) = 4*x12 + 4*x12*x5 + 6*x12^2 + 5*x5 + 4*x5^2
>= x12 + 2*x12*x5 + 4*x12^2 + 3*x5 + 2*x5^2
= map#2(plus_x(x12),x5)
map#2(plus_x(x2),Nil()) = 5 + 3*x2 + 4*x2^2
>= 1
= Nil()
map#2(plus_x(x6),Cons(x4,x2)) = 5 + 7*x2 + 4*x2*x4 + 2*x2*x6 + 2*x2^2 + 7*x4 + 2*x4*x6 + 2*x4^2 + 3*x6 + 4*x6^2
>= 1 + 3*x2 + 2*x2*x6 + 2*x2^2 + x4 + 3*x6 + 4*x6^2
= Cons(plus_x#1(x6,x4)
,map#2(plus_x(x6),x2))
plus_x#1(0(),x8) = 2 + x8
>= x8
= x8
*** 1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
main(x5,x12) -> map#2(plus_x(x12),x5)
map#2(plus_x(x2),Nil()) -> Nil()
map#2(plus_x(x6),Cons(x4,x2)) -> Cons(plus_x#1(x6,x4),map#2(plus_x(x6),x2))
plus_x#1(0(),x8) -> x8
plus_x#1(S(x12),x14) -> S(plus_x#1(x12,x14))
Signature:
{main/2,map#2/2,plus_x#1/2} / {0/0,Cons/2,Nil/0,S/1,plus_x/1}
Obligation:
Innermost
basic terms: {main,map#2,plus_x#1}/{0,Cons,Nil,S,plus_x}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).