*** 1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
*(@x,@y) -> #mult(@x,@y)
dyade(@l1,@l2) -> dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) -> nil()
mult(@n,@l) -> mult#1(@l,@n)
mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) -> nil()
Weak DP Rules:
Weak TRS Rules:
#add(#0(),@y) -> @y
#add(#neg(#s(#0())),@y) -> #pred(@y)
#add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) -> #succ(@y)
#add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) -> #0()
#mult(#0(),#neg(@y)) -> #0()
#mult(#0(),#pos(@y)) -> #0()
#mult(#neg(@x),#0()) -> #0()
#mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) -> #0()
#mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y))
#natmult(#0(),@y) -> #0()
#natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) -> #neg(#s(#0()))
#pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) -> #0()
#pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
#succ(#0()) -> #pos(#s(#0()))
#succ(#neg(#s(#0()))) -> #0()
#succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
#succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0}
Obligation:
Innermost
basic terms: {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}/{#0,#neg,#pos,#s,::,nil}
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(#add) = {2},
uargs(#neg) = {1},
uargs(#pos) = {1},
uargs(#pred) = {1},
uargs(#succ) = {1},
uargs(::) = {1,2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(#0) = [0]
p(#add) = [1] x2 + [0]
p(#mult) = [4]
p(#natmult) = [4]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#pred) = [1] x1 + [0]
p(#s) = [0]
p(#succ) = [1] x1 + [0]
p(*) = [3]
p(::) = [1] x1 + [1] x2 + [2]
p(dyade) = [4] x1 + [4] x2 + [0]
p(dyade#1) = [4] x1 + [4] x2 + [0]
p(mult) = [0]
p(mult#1) = [0]
p(nil) = [0]
Following rules are strictly oriented:
dyade#1(::(@x,@xs),@l2) = [4] @l2 + [4] @x + [4] @xs + [8]
> [4] @l2 + [4] @xs + [2]
= ::(mult(@x,@l2),dyade(@xs,@l2))
Following rules are (at-least) weakly oriented:
#add(#0(),@y) = [1] @y + [0]
>= [1] @y + [0]
= @y
#add(#neg(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(@y)
#add(#neg(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(@y)
#add(#pos(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) = [4]
>= [0]
= #0()
#mult(#0(),#neg(@y)) = [4]
>= [0]
= #0()
#mult(#0(),#pos(@y)) = [4]
>= [0]
= #0()
#mult(#neg(@x),#0()) = [4]
>= [0]
= #0()
#mult(#neg(@x),#neg(@y)) = [4]
>= [4]
= #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) = [4]
>= [4]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) = [4]
>= [0]
= #0()
#mult(#pos(@x),#neg(@y)) = [4]
>= [4]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) = [4]
>= [4]
= #pos(#natmult(@x,@y))
#natmult(#0(),@y) = [4]
>= [0]
= #0()
#natmult(#s(@x),@y) = [4]
>= [4]
= #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) = [0]
>= [0]
= #neg(#s(#0()))
#pred(#neg(#s(@x))) = [0]
>= [0]
= #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) = [0]
>= [0]
= #0()
#pred(#pos(#s(#s(@x)))) = [0]
>= [0]
= #pos(#s(@x))
#succ(#0()) = [0]
>= [0]
= #pos(#s(#0()))
#succ(#neg(#s(#0()))) = [0]
>= [0]
= #0()
#succ(#neg(#s(#s(@x)))) = [0]
>= [0]
= #neg(#s(@x))
#succ(#pos(#s(@x))) = [0]
>= [0]
= #pos(#s(#s(@x)))
*(@x,@y) = [3]
>= [4]
= #mult(@x,@y)
dyade(@l1,@l2) = [4] @l1 + [4] @l2 + [0]
>= [4] @l1 + [4] @l2 + [0]
= dyade#1(@l1,@l2)
dyade#1(nil(),@l2) = [4] @l2 + [0]
>= [0]
= nil()
mult(@n,@l) = [0]
>= [0]
= mult#1(@l,@n)
mult#1(::(@x,@xs),@n) = [0]
>= [5]
= ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) = [0]
>= [0]
= nil()
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:
*(@x,@y) -> #mult(@x,@y)
dyade(@l1,@l2) -> dyade#1(@l1,@l2)
dyade#1(nil(),@l2) -> nil()
mult(@n,@l) -> mult#1(@l,@n)
mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) -> nil()
Weak DP Rules:
Weak TRS Rules:
#add(#0(),@y) -> @y
#add(#neg(#s(#0())),@y) -> #pred(@y)
#add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) -> #succ(@y)
#add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) -> #0()
#mult(#0(),#neg(@y)) -> #0()
#mult(#0(),#pos(@y)) -> #0()
#mult(#neg(@x),#0()) -> #0()
#mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) -> #0()
#mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y))
#natmult(#0(),@y) -> #0()
#natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) -> #neg(#s(#0()))
#pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) -> #0()
#pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
#succ(#0()) -> #pos(#s(#0()))
#succ(#neg(#s(#0()))) -> #0()
#succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
#succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2))
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0}
Obligation:
Innermost
basic terms: {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}/{#0,#neg,#pos,#s,::,nil}
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(#add) = {2},
uargs(#neg) = {1},
uargs(#pos) = {1},
uargs(#pred) = {1},
uargs(#succ) = {1},
uargs(::) = {1,2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(#0) = [0]
p(#add) = [1] x2 + [0]
p(#mult) = [5]
p(#natmult) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#pred) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#succ) = [1] x1 + [0]
p(*) = [0]
p(::) = [1] x1 + [1] x2 + [3]
p(dyade) = [2] x1 + [5]
p(dyade#1) = [2] x1 + [7]
p(mult) = [4]
p(mult#1) = [2]
p(nil) = [2]
Following rules are strictly oriented:
dyade#1(nil(),@l2) = [11]
> [2]
= nil()
mult(@n,@l) = [4]
> [2]
= mult#1(@l,@n)
Following rules are (at-least) weakly oriented:
#add(#0(),@y) = [1] @y + [0]
>= [1] @y + [0]
= @y
#add(#neg(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(@y)
#add(#neg(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(@y)
#add(#pos(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) = [5]
>= [0]
= #0()
#mult(#0(),#neg(@y)) = [5]
>= [0]
= #0()
#mult(#0(),#pos(@y)) = [5]
>= [0]
= #0()
#mult(#neg(@x),#0()) = [5]
>= [0]
= #0()
#mult(#neg(@x),#neg(@y)) = [5]
>= [0]
= #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) = [5]
>= [0]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) = [5]
>= [0]
= #0()
#mult(#pos(@x),#neg(@y)) = [5]
>= [0]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) = [5]
>= [0]
= #pos(#natmult(@x,@y))
#natmult(#0(),@y) = [0]
>= [0]
= #0()
#natmult(#s(@x),@y) = [0]
>= [0]
= #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) = [0]
>= [0]
= #neg(#s(#0()))
#pred(#neg(#s(@x))) = [1] @x + [0]
>= [1] @x + [0]
= #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) = [0]
>= [0]
= #0()
#pred(#pos(#s(#s(@x)))) = [1] @x + [0]
>= [1] @x + [0]
= #pos(#s(@x))
#succ(#0()) = [0]
>= [0]
= #pos(#s(#0()))
#succ(#neg(#s(#0()))) = [0]
>= [0]
= #0()
#succ(#neg(#s(#s(@x)))) = [1] @x + [0]
>= [1] @x + [0]
= #neg(#s(@x))
#succ(#pos(#s(@x))) = [1] @x + [0]
>= [1] @x + [0]
= #pos(#s(#s(@x)))
*(@x,@y) = [0]
>= [5]
= #mult(@x,@y)
dyade(@l1,@l2) = [2] @l1 + [5]
>= [2] @l1 + [7]
= dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) = [2] @x + [2] @xs + [13]
>= [2] @xs + [12]
= ::(mult(@x,@l2),dyade(@xs,@l2))
mult#1(::(@x,@xs),@n) = [2]
>= [7]
= ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) = [2]
>= [2]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
*(@x,@y) -> #mult(@x,@y)
dyade(@l1,@l2) -> dyade#1(@l1,@l2)
mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) -> nil()
Weak DP Rules:
Weak TRS Rules:
#add(#0(),@y) -> @y
#add(#neg(#s(#0())),@y) -> #pred(@y)
#add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) -> #succ(@y)
#add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) -> #0()
#mult(#0(),#neg(@y)) -> #0()
#mult(#0(),#pos(@y)) -> #0()
#mult(#neg(@x),#0()) -> #0()
#mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) -> #0()
#mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y))
#natmult(#0(),@y) -> #0()
#natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) -> #neg(#s(#0()))
#pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) -> #0()
#pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
#succ(#0()) -> #pos(#s(#0()))
#succ(#neg(#s(#0()))) -> #0()
#succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
#succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) -> nil()
mult(@n,@l) -> mult#1(@l,@n)
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0}
Obligation:
Innermost
basic terms: {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}/{#0,#neg,#pos,#s,::,nil}
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(#add) = {2},
uargs(#neg) = {1},
uargs(#pos) = {1},
uargs(#pred) = {1},
uargs(#succ) = {1},
uargs(::) = {1,2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(#0) = [0]
p(#add) = [1] x2 + [0]
p(#mult) = [4]
p(#natmult) = [4]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#pred) = [1] x1 + [0]
p(#s) = [0]
p(#succ) = [1] x1 + [0]
p(*) = [3]
p(::) = [1] x1 + [1] x2 + [5]
p(dyade) = [2] x1 + [2]
p(dyade#1) = [2] x1 + [1]
p(mult) = [1]
p(mult#1) = [0]
p(nil) = [2]
Following rules are strictly oriented:
dyade(@l1,@l2) = [2] @l1 + [2]
> [2] @l1 + [1]
= dyade#1(@l1,@l2)
Following rules are (at-least) weakly oriented:
#add(#0(),@y) = [1] @y + [0]
>= [1] @y + [0]
= @y
#add(#neg(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(@y)
#add(#neg(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(@y)
#add(#pos(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) = [4]
>= [0]
= #0()
#mult(#0(),#neg(@y)) = [4]
>= [0]
= #0()
#mult(#0(),#pos(@y)) = [4]
>= [0]
= #0()
#mult(#neg(@x),#0()) = [4]
>= [0]
= #0()
#mult(#neg(@x),#neg(@y)) = [4]
>= [4]
= #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) = [4]
>= [4]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) = [4]
>= [0]
= #0()
#mult(#pos(@x),#neg(@y)) = [4]
>= [4]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) = [4]
>= [4]
= #pos(#natmult(@x,@y))
#natmult(#0(),@y) = [4]
>= [0]
= #0()
#natmult(#s(@x),@y) = [4]
>= [4]
= #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) = [0]
>= [0]
= #neg(#s(#0()))
#pred(#neg(#s(@x))) = [0]
>= [0]
= #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) = [0]
>= [0]
= #0()
#pred(#pos(#s(#s(@x)))) = [0]
>= [0]
= #pos(#s(@x))
#succ(#0()) = [0]
>= [0]
= #pos(#s(#0()))
#succ(#neg(#s(#0()))) = [0]
>= [0]
= #0()
#succ(#neg(#s(#s(@x)))) = [0]
>= [0]
= #neg(#s(@x))
#succ(#pos(#s(@x))) = [0]
>= [0]
= #pos(#s(#s(@x)))
*(@x,@y) = [3]
>= [4]
= #mult(@x,@y)
dyade#1(::(@x,@xs),@l2) = [2] @x + [2] @xs + [11]
>= [2] @xs + [8]
= ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) = [5]
>= [2]
= nil()
mult(@n,@l) = [1]
>= [0]
= mult#1(@l,@n)
mult#1(::(@x,@xs),@n) = [0]
>= [9]
= ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) = [0]
>= [2]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
*(@x,@y) -> #mult(@x,@y)
mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) -> nil()
Weak DP Rules:
Weak TRS Rules:
#add(#0(),@y) -> @y
#add(#neg(#s(#0())),@y) -> #pred(@y)
#add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) -> #succ(@y)
#add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) -> #0()
#mult(#0(),#neg(@y)) -> #0()
#mult(#0(),#pos(@y)) -> #0()
#mult(#neg(@x),#0()) -> #0()
#mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) -> #0()
#mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y))
#natmult(#0(),@y) -> #0()
#natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) -> #neg(#s(#0()))
#pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) -> #0()
#pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
#succ(#0()) -> #pos(#s(#0()))
#succ(#neg(#s(#0()))) -> #0()
#succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
#succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
dyade(@l1,@l2) -> dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) -> nil()
mult(@n,@l) -> mult#1(@l,@n)
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0}
Obligation:
Innermost
basic terms: {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}/{#0,#neg,#pos,#s,::,nil}
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(#add) = {2},
uargs(#neg) = {1},
uargs(#pos) = {1},
uargs(#pred) = {1},
uargs(#succ) = {1},
uargs(::) = {1,2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(#0) = [2]
p(#add) = [1] x2 + [0]
p(#mult) = [4]
p(#natmult) = [2]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#pred) = [1] x1 + [0]
p(#s) = [2]
p(#succ) = [1] x1 + [0]
p(*) = [6]
p(::) = [1] x1 + [1] x2 + [0]
p(dyade) = [1] x1 + [4]
p(dyade#1) = [1] x1 + [4]
p(mult) = [0]
p(mult#1) = [0]
p(nil) = [0]
Following rules are strictly oriented:
*(@x,@y) = [6]
> [4]
= #mult(@x,@y)
Following rules are (at-least) weakly oriented:
#add(#0(),@y) = [1] @y + [0]
>= [1] @y + [0]
= @y
#add(#neg(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(@y)
#add(#neg(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(@y)
#add(#pos(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) = [4]
>= [2]
= #0()
#mult(#0(),#neg(@y)) = [4]
>= [2]
= #0()
#mult(#0(),#pos(@y)) = [4]
>= [2]
= #0()
#mult(#neg(@x),#0()) = [4]
>= [2]
= #0()
#mult(#neg(@x),#neg(@y)) = [4]
>= [2]
= #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) = [4]
>= [2]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) = [4]
>= [2]
= #0()
#mult(#pos(@x),#neg(@y)) = [4]
>= [2]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) = [4]
>= [2]
= #pos(#natmult(@x,@y))
#natmult(#0(),@y) = [2]
>= [2]
= #0()
#natmult(#s(@x),@y) = [2]
>= [2]
= #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) = [2]
>= [2]
= #neg(#s(#0()))
#pred(#neg(#s(@x))) = [2]
>= [2]
= #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) = [2]
>= [2]
= #0()
#pred(#pos(#s(#s(@x)))) = [2]
>= [2]
= #pos(#s(@x))
#succ(#0()) = [2]
>= [2]
= #pos(#s(#0()))
#succ(#neg(#s(#0()))) = [2]
>= [2]
= #0()
#succ(#neg(#s(#s(@x)))) = [2]
>= [2]
= #neg(#s(@x))
#succ(#pos(#s(@x))) = [2]
>= [2]
= #pos(#s(#s(@x)))
dyade(@l1,@l2) = [1] @l1 + [4]
>= [1] @l1 + [4]
= dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) = [1] @x + [1] @xs + [4]
>= [1] @xs + [4]
= ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) = [4]
>= [0]
= nil()
mult(@n,@l) = [0]
>= [0]
= mult#1(@l,@n)
mult#1(::(@x,@xs),@n) = [0]
>= [6]
= ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) = [0]
>= [0]
= nil()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) -> nil()
Weak DP Rules:
Weak TRS Rules:
#add(#0(),@y) -> @y
#add(#neg(#s(#0())),@y) -> #pred(@y)
#add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) -> #succ(@y)
#add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) -> #0()
#mult(#0(),#neg(@y)) -> #0()
#mult(#0(),#pos(@y)) -> #0()
#mult(#neg(@x),#0()) -> #0()
#mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) -> #0()
#mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y))
#natmult(#0(),@y) -> #0()
#natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) -> #neg(#s(#0()))
#pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) -> #0()
#pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
#succ(#0()) -> #pos(#s(#0()))
#succ(#neg(#s(#0()))) -> #0()
#succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
#succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
*(@x,@y) -> #mult(@x,@y)
dyade(@l1,@l2) -> dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) -> nil()
mult(@n,@l) -> mult#1(@l,@n)
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0}
Obligation:
Innermost
basic terms: {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}/{#0,#neg,#pos,#s,::,nil}
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(#add) = {2},
uargs(#neg) = {1},
uargs(#pos) = {1},
uargs(#pred) = {1},
uargs(#succ) = {1},
uargs(::) = {1,2}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(#0) = [0]
p(#add) = [1] x2 + [0]
p(#mult) = [0]
p(#natmult) = [0]
p(#neg) = [1] x1 + [0]
p(#pos) = [1] x1 + [0]
p(#pred) = [1] x1 + [0]
p(#s) = [0]
p(#succ) = [1] x1 + [0]
p(*) = [0]
p(::) = [1] x1 + [1] x2 + [5]
p(dyade) = [2] x1 + [3] x2 + [0]
p(dyade#1) = [2] x1 + [3] x2 + [0]
p(mult) = [2] x1 + [5]
p(mult#1) = [2] x2 + [5]
p(nil) = [0]
Following rules are strictly oriented:
mult#1(nil(),@n) = [2] @n + [5]
> [0]
= nil()
Following rules are (at-least) weakly oriented:
#add(#0(),@y) = [1] @y + [0]
>= [1] @y + [0]
= @y
#add(#neg(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(@y)
#add(#neg(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(@y)
#add(#pos(#s(#s(@x))),@y) = [1] @y + [0]
>= [1] @y + [0]
= #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) = [0]
>= [0]
= #0()
#mult(#0(),#neg(@y)) = [0]
>= [0]
= #0()
#mult(#0(),#pos(@y)) = [0]
>= [0]
= #0()
#mult(#neg(@x),#0()) = [0]
>= [0]
= #0()
#mult(#neg(@x),#neg(@y)) = [0]
>= [0]
= #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) = [0]
>= [0]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) = [0]
>= [0]
= #0()
#mult(#pos(@x),#neg(@y)) = [0]
>= [0]
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) = [0]
>= [0]
= #pos(#natmult(@x,@y))
#natmult(#0(),@y) = [0]
>= [0]
= #0()
#natmult(#s(@x),@y) = [0]
>= [0]
= #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) = [0]
>= [0]
= #neg(#s(#0()))
#pred(#neg(#s(@x))) = [0]
>= [0]
= #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) = [0]
>= [0]
= #0()
#pred(#pos(#s(#s(@x)))) = [0]
>= [0]
= #pos(#s(@x))
#succ(#0()) = [0]
>= [0]
= #pos(#s(#0()))
#succ(#neg(#s(#0()))) = [0]
>= [0]
= #0()
#succ(#neg(#s(#s(@x)))) = [0]
>= [0]
= #neg(#s(@x))
#succ(#pos(#s(@x))) = [0]
>= [0]
= #pos(#s(#s(@x)))
*(@x,@y) = [0]
>= [0]
= #mult(@x,@y)
dyade(@l1,@l2) = [2] @l1 + [3] @l2 + [0]
>= [2] @l1 + [3] @l2 + [0]
= dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) = [3] @l2 + [2] @x + [2] @xs + [10]
>= [3] @l2 + [2] @x + [2] @xs + [10]
= ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) = [3] @l2 + [0]
>= [0]
= nil()
mult(@n,@l) = [2] @n + [5]
>= [2] @n + [5]
= mult#1(@l,@n)
mult#1(::(@x,@xs),@n) = [2] @n + [5]
>= [2] @n + [10]
= ::(*(@n,@x),mult(@n,@xs))
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs))
Weak DP Rules:
Weak TRS Rules:
#add(#0(),@y) -> @y
#add(#neg(#s(#0())),@y) -> #pred(@y)
#add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) -> #succ(@y)
#add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) -> #0()
#mult(#0(),#neg(@y)) -> #0()
#mult(#0(),#pos(@y)) -> #0()
#mult(#neg(@x),#0()) -> #0()
#mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) -> #0()
#mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y))
#natmult(#0(),@y) -> #0()
#natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) -> #neg(#s(#0()))
#pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) -> #0()
#pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
#succ(#0()) -> #pos(#s(#0()))
#succ(#neg(#s(#0()))) -> #0()
#succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
#succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
*(@x,@y) -> #mult(@x,@y)
dyade(@l1,@l2) -> dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) -> nil()
mult(@n,@l) -> mult#1(@l,@n)
mult#1(nil(),@n) -> nil()
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0}
Obligation:
Innermost
basic terms: {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}/{#0,#neg,#pos,#s,::,nil}
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(#add) = {2},
uargs(#neg) = {1},
uargs(#pos) = {1},
uargs(#pred) = {1},
uargs(#succ) = {1},
uargs(::) = {1,2}
Following symbols are considered usable:
{#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}
TcT has computed the following interpretation:
p(#0) = 0
p(#add) = 2*x2
p(#mult) = 0
p(#natmult) = 0
p(#neg) = x1
p(#pos) = x1
p(#pred) = x1
p(#s) = 0
p(#succ) = x1
p(*) = 2*x2
p(::) = 1 + x1 + x2
p(dyade) = 2 + 2*x1 + 3*x1*x2 + 2*x1^2 + x2^2
p(dyade#1) = 2*x1 + 3*x1*x2 + 2*x1^2 + x2^2
p(mult) = 1 + 3*x2
p(mult#1) = 1 + 3*x1
p(nil) = 0
Following rules are strictly oriented:
mult#1(::(@x,@xs),@n) = 4 + 3*@x + 3*@xs
> 2 + 2*@x + 3*@xs
= ::(*(@n,@x),mult(@n,@xs))
Following rules are (at-least) weakly oriented:
#add(#0(),@y) = 2*@y
>= @y
= @y
#add(#neg(#s(#0())),@y) = 2*@y
>= @y
= #pred(@y)
#add(#neg(#s(#s(@x))),@y) = 2*@y
>= 2*@y
= #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) = 2*@y
>= @y
= #succ(@y)
#add(#pos(#s(#s(@x))),@y) = 2*@y
>= 2*@y
= #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) = 0
>= 0
= #0()
#mult(#0(),#neg(@y)) = 0
>= 0
= #0()
#mult(#0(),#pos(@y)) = 0
>= 0
= #0()
#mult(#neg(@x),#0()) = 0
>= 0
= #0()
#mult(#neg(@x),#neg(@y)) = 0
>= 0
= #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) = 0
>= 0
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) = 0
>= 0
= #0()
#mult(#pos(@x),#neg(@y)) = 0
>= 0
= #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) = 0
>= 0
= #pos(#natmult(@x,@y))
#natmult(#0(),@y) = 0
>= 0
= #0()
#natmult(#s(@x),@y) = 0
>= 0
= #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) = 0
>= 0
= #neg(#s(#0()))
#pred(#neg(#s(@x))) = 0
>= 0
= #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) = 0
>= 0
= #0()
#pred(#pos(#s(#s(@x)))) = 0
>= 0
= #pos(#s(@x))
#succ(#0()) = 0
>= 0
= #pos(#s(#0()))
#succ(#neg(#s(#0()))) = 0
>= 0
= #0()
#succ(#neg(#s(#s(@x)))) = 0
>= 0
= #neg(#s(@x))
#succ(#pos(#s(@x))) = 0
>= 0
= #pos(#s(#s(@x)))
*(@x,@y) = 2*@y
>= 0
= #mult(@x,@y)
dyade(@l1,@l2) = 2 + 2*@l1 + 3*@l1*@l2 + 2*@l1^2 + @l2^2
>= 2*@l1 + 3*@l1*@l2 + 2*@l1^2 + @l2^2
= dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) = 4 + 3*@l2 + 3*@l2*@x + 3*@l2*@xs + @l2^2 + 6*@x + 4*@x*@xs + 2*@x^2 + 6*@xs + 2*@xs^2
>= 4 + 3*@l2 + 3*@l2*@xs + @l2^2 + 2*@xs + 2*@xs^2
= ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) = @l2^2
>= 0
= nil()
mult(@n,@l) = 1 + 3*@l
>= 1 + 3*@l
= mult#1(@l,@n)
mult#1(nil(),@n) = 1
>= 0
= nil()
*** 1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
#add(#0(),@y) -> @y
#add(#neg(#s(#0())),@y) -> #pred(@y)
#add(#neg(#s(#s(@x))),@y) -> #pred(#add(#pos(#s(@x)),@y))
#add(#pos(#s(#0())),@y) -> #succ(@y)
#add(#pos(#s(#s(@x))),@y) -> #succ(#add(#pos(#s(@x)),@y))
#mult(#0(),#0()) -> #0()
#mult(#0(),#neg(@y)) -> #0()
#mult(#0(),#pos(@y)) -> #0()
#mult(#neg(@x),#0()) -> #0()
#mult(#neg(@x),#neg(@y)) -> #pos(#natmult(@x,@y))
#mult(#neg(@x),#pos(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#0()) -> #0()
#mult(#pos(@x),#neg(@y)) -> #neg(#natmult(@x,@y))
#mult(#pos(@x),#pos(@y)) -> #pos(#natmult(@x,@y))
#natmult(#0(),@y) -> #0()
#natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y))
#pred(#0()) -> #neg(#s(#0()))
#pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
#pred(#pos(#s(#0()))) -> #0()
#pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
#succ(#0()) -> #pos(#s(#0()))
#succ(#neg(#s(#0()))) -> #0()
#succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
#succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
*(@x,@y) -> #mult(@x,@y)
dyade(@l1,@l2) -> dyade#1(@l1,@l2)
dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2))
dyade#1(nil(),@l2) -> nil()
mult(@n,@l) -> mult#1(@l,@n)
mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs))
mult#1(nil(),@n) -> nil()
Signature:
{#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1,#pos/1,#s/1,::/2,nil/0}
Obligation:
Innermost
basic terms: {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult,mult#1}/{#0,#neg,#pos,#s,::,nil}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).