WORST_CASE(?,O(n^2)) * Step 1: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: *(@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 TRS: #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 runtime complexity wrt. defined symbols {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult ,mult#1} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: 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: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [1] x2 + [0] p(#mult) = [1] p(#natmult) = [1] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#pred) = [1] x1 + [0] p(#s) = [0] p(#succ) = [1] x1 + [0] p(*) = [5] p(::) = [1] x1 + [1] x2 + [4] p(dyade) = [2] x2 + [0] p(dyade#1) = [2] x2 + [3] p(mult) = [0] p(mult#1) = [2] p(nil) = [0] Following rules are strictly oriented: *(@x,@y) = [5] > [1] = #mult(@x,@y) dyade#1(nil(),@l2) = [2] @l2 + [3] > [0] = nil() mult#1(nil(),@n) = [2] > [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()) = [1] >= [0] = #0() #mult(#0(),#neg(@y)) = [1] >= [0] = #0() #mult(#0(),#pos(@y)) = [1] >= [0] = #0() #mult(#neg(@x),#0()) = [1] >= [0] = #0() #mult(#neg(@x),#neg(@y)) = [1] >= [1] = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = [1] >= [1] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = [1] >= [0] = #0() #mult(#pos(@x),#neg(@y)) = [1] >= [1] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = [1] >= [1] = #pos(#natmult(@x,@y)) #natmult(#0(),@y) = [1] >= [0] = #0() #natmult(#s(@x),@y) = [1] >= [1] = #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))) dyade(@l1,@l2) = [2] @l2 + [0] >= [2] @l2 + [3] = dyade#1(@l1,@l2) dyade#1(::(@x,@xs),@l2) = [2] @l2 + [3] >= [2] @l2 + [4] = ::(mult(@x,@l2),dyade(@xs,@l2)) mult(@n,@l) = [0] >= [2] = mult#1(@l,@n) mult#1(::(@x,@xs),@n) = [2] >= [9] = ::(*(@n,@x),mult(@n,@xs)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: dyade(@l1,@l2) -> dyade#1(@l1,@l2) dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2)) mult(@n,@l) -> mult#1(@l,@n) mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs)) - Weak TRS: #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#1(nil(),@l2) -> nil() 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 runtime complexity wrt. defined symbols {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult ,mult#1} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: 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: all 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) = [1] x1 + [0] p(#succ) = [1] x1 + [0] p(*) = [0] p(::) = [1] x1 + [1] x2 + [1] p(dyade) = [4] x1 + [2] x2 + [0] p(dyade#1) = [4] x1 + [2] x2 + [0] p(mult) = [4] x1 + [7] p(mult#1) = [4] x2 + [6] p(nil) = [0] Following rules are strictly oriented: mult(@n,@l) = [4] @n + [7] > [4] @n + [6] = 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()) = [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))) = [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] >= [0] = #mult(@x,@y) dyade(@l1,@l2) = [4] @l1 + [2] @l2 + [0] >= [4] @l1 + [2] @l2 + [0] = dyade#1(@l1,@l2) dyade#1(::(@x,@xs),@l2) = [2] @l2 + [4] @x + [4] @xs + [4] >= [2] @l2 + [4] @x + [4] @xs + [8] = ::(mult(@x,@l2),dyade(@xs,@l2)) dyade#1(nil(),@l2) = [2] @l2 + [0] >= [0] = nil() mult#1(::(@x,@xs),@n) = [4] @n + [6] >= [4] @n + [8] = ::(*(@n,@x),mult(@n,@xs)) mult#1(nil(),@n) = [4] @n + [6] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: dyade(@l1,@l2) -> dyade#1(@l1,@l2) dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2)) mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs)) - Weak TRS: #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#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 runtime complexity wrt. defined symbols {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult ,mult#1} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: 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: all TcT has computed the following interpretation: p(#0) = [2] p(#add) = [1] x2 + [0] p(#mult) = [6] p(#natmult) = [2] p(#neg) = [1] x1 + [2] p(#pos) = [1] x1 + [2] p(#pred) = [1] x1 + [0] p(#s) = [0] p(#succ) = [1] x1 + [0] p(*) = [6] p(::) = [1] x1 + [1] x2 + [0] p(dyade) = [2] x1 + [4] x2 + [4] p(dyade#1) = [2] x1 + [4] x2 + [0] p(mult) = [1] x1 + [0] p(mult#1) = [1] x2 + [0] p(nil) = [0] Following rules are strictly oriented: dyade(@l1,@l2) = [2] @l1 + [4] @l2 + [4] > [2] @l1 + [4] @l2 + [0] = 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()) = [6] >= [2] = #0() #mult(#0(),#neg(@y)) = [6] >= [2] = #0() #mult(#0(),#pos(@y)) = [6] >= [2] = #0() #mult(#neg(@x),#0()) = [6] >= [2] = #0() #mult(#neg(@x),#neg(@y)) = [6] >= [4] = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = [6] >= [4] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = [6] >= [2] = #0() #mult(#pos(@x),#neg(@y)) = [6] >= [4] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = [6] >= [4] = #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))) *(@x,@y) = [6] >= [6] = #mult(@x,@y) dyade#1(::(@x,@xs),@l2) = [4] @l2 + [2] @x + [2] @xs + [0] >= [4] @l2 + [1] @x + [2] @xs + [4] = ::(mult(@x,@l2),dyade(@xs,@l2)) dyade#1(nil(),@l2) = [4] @l2 + [0] >= [0] = nil() mult(@n,@l) = [1] @n + [0] >= [1] @n + [0] = mult#1(@l,@n) mult#1(::(@x,@xs),@n) = [1] @n + [0] >= [1] @n + [6] = ::(*(@n,@x),mult(@n,@xs)) mult#1(nil(),@n) = [1] @n + [0] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2)) mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs)) - Weak TRS: #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(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 runtime complexity wrt. defined symbols {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult ,mult#1} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: 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: all TcT has computed the following interpretation: p(#0) = [0] p(#add) = [1] x2 + [0] p(#mult) = [2] 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(*) = [4] p(::) = [1] x1 + [1] x2 + [5] p(dyade) = [2] x1 + [0] p(dyade#1) = [2] x1 + [0] p(mult) = [4] p(mult#1) = [2] p(nil) = [0] Following rules are strictly oriented: dyade#1(::(@x,@xs),@l2) = [2] @x + [2] @xs + [10] > [2] @xs + [9] = ::(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()) = [2] >= [0] = #0() #mult(#0(),#neg(@y)) = [2] >= [0] = #0() #mult(#0(),#pos(@y)) = [2] >= [0] = #0() #mult(#neg(@x),#0()) = [2] >= [0] = #0() #mult(#neg(@x),#neg(@y)) = [2] >= [0] = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = [2] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = [2] >= [0] = #0() #mult(#pos(@x),#neg(@y)) = [2] >= [0] = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = [2] >= [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) = [4] >= [2] = #mult(@x,@y) dyade(@l1,@l2) = [2] @l1 + [0] >= [2] @l1 + [0] = dyade#1(@l1,@l2) dyade#1(nil(),@l2) = [0] >= [0] = nil() mult(@n,@l) = [4] >= [2] = mult#1(@l,@n) mult#1(::(@x,@xs),@n) = [2] >= [13] = ::(*(@n,@x),mult(@n,@xs)) mult#1(nil(),@n) = [2] >= [0] = nil() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: mult#1(::(@x,@xs),@n) -> ::(*(@n,@x),mult(@n,@xs)) - Weak TRS: #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 runtime complexity wrt. defined symbols {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult ,mult#1} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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) = x2 p(#mult) = 1 + x2 p(#natmult) = 0 p(#neg) = x1 p(#pos) = x1 p(#pred) = x1 p(#s) = 0 p(#succ) = x1 p(*) = 1 + x1 + 2*x2 p(::) = 2 + x1 + x2 p(dyade) = 2 + 2*x1 + 2*x1*x2 + 3*x2 p(dyade#1) = 2 + 2*x1 + 2*x1*x2 + x2 p(mult) = 2 + 2*x1*x2 + 2*x2 p(mult#1) = 2 + 2*x1 + 2*x1*x2 p(nil) = 0 Following rules are strictly oriented: mult#1(::(@x,@xs),@n) = 6 + 4*@n + 2*@n*@x + 2*@n*@xs + 2*@x + 2*@xs > 5 + @n + 2*@n*@xs + 2*@x + 2*@xs = ::(*(@n,@x),mult(@n,@xs)) Following rules are (at-least) weakly oriented: #add(#0(),@y) = @y >= @y = @y #add(#neg(#s(#0())),@y) = @y >= @y = #pred(@y) #add(#neg(#s(#s(@x))),@y) = @y >= @y = #pred(#add(#pos(#s(@x)),@y)) #add(#pos(#s(#0())),@y) = @y >= @y = #succ(@y) #add(#pos(#s(#s(@x))),@y) = @y >= @y = #succ(#add(#pos(#s(@x)),@y)) #mult(#0(),#0()) = 1 >= 0 = #0() #mult(#0(),#neg(@y)) = 1 + @y >= 0 = #0() #mult(#0(),#pos(@y)) = 1 + @y >= 0 = #0() #mult(#neg(@x),#0()) = 1 >= 0 = #0() #mult(#neg(@x),#neg(@y)) = 1 + @y >= 0 = #pos(#natmult(@x,@y)) #mult(#neg(@x),#pos(@y)) = 1 + @y >= 0 = #neg(#natmult(@x,@y)) #mult(#pos(@x),#0()) = 1 >= 0 = #0() #mult(#pos(@x),#neg(@y)) = 1 + @y >= 0 = #neg(#natmult(@x,@y)) #mult(#pos(@x),#pos(@y)) = 1 + @y >= 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) = 1 + @x + 2*@y >= 1 + @y = #mult(@x,@y) dyade(@l1,@l2) = 2 + 2*@l1 + 2*@l1*@l2 + 3*@l2 >= 2 + 2*@l1 + 2*@l1*@l2 + @l2 = dyade#1(@l1,@l2) dyade#1(::(@x,@xs),@l2) = 6 + 5*@l2 + 2*@l2*@x + 2*@l2*@xs + 2*@x + 2*@xs >= 6 + 5*@l2 + 2*@l2*@x + 2*@l2*@xs + 2*@xs = ::(mult(@x,@l2),dyade(@xs,@l2)) dyade#1(nil(),@l2) = 2 + @l2 >= 0 = nil() mult(@n,@l) = 2 + 2*@l + 2*@l*@n >= 2 + 2*@l + 2*@l*@n = mult#1(@l,@n) mult#1(nil(),@n) = 2 >= 0 = nil() * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: #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 runtime complexity wrt. defined symbols {#add,#mult,#natmult,#pred,#succ,*,dyade,dyade#1,mult ,mult#1} and constructors {#0,#neg,#pos,#s,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))