WORST_CASE(?,O(n^2)) * Step 1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict 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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,nil} + 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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = [0] p(#add) = [2] x2 + [4] p(#mult) = [0] p(#natadd) = [1] x2 + [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(dd) = [1] x1 + [1] x2 + [0] p(dyade) = [2] x2 + [0] p(dyade#1) = [2] x2 + [0] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] Following rules are strictly oriented: #add(#0(),y) = [2] y + [4] > [1] y + [0] = y #add(#neg(#s(#0())),y) = [2] y + [4] > [1] y + [0] = #pred(y) #add(#pos(#s(#0())),y) = [2] y + [4] > [1] y + [0] = #succ(y) Following rules are (at-least) weakly oriented: #add(#neg(#s(#s(x))),y) = [2] y + [4] >= [2] y + [4] = #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#s(x))),y) = [2] y + [4] >= [2] y + [4] = #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)) #natadd(#0(),y) = [1] y + [0] >= [1] y + [0] = y #natadd(#s(x),y) = [1] y + [0] >= [1] y + [0] = #s(#natadd(x,y)) #natmult(#0(),y) = [0] >= [0] = #0() #natmult(#s(x),y) = [0] >= [0] = #natadd(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))) dyade(l1,l2) = [2] l2 + [0] >= [2] l2 + [0] = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = [2] l2 + [0] >= [2] l2 + [0] = dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) = [2] l2 + [0] >= [0] = nil() mult(n,l) = [0] >= [0] = mult#1(l,n) mult(x,y) = [0] >= [0] = #mult(x,y) mult#1(dd(x,xs),n) = [0] >= [0] = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = [0] >= [0] = nil() * Step 2: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Weak TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#pos(#s(#0())),y) -> #succ(y) - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,nil} + 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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = [0] p(#add) = [1] x2 + [0] p(#mult) = [0] p(#natadd) = [2] x2 + [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(dd) = [1] x1 + [1] x2 + [0] p(dyade) = [4] x2 + [4] p(dyade#1) = [4] x2 + [4] p(mult) = [0] p(mult#1) = [0] p(nil) = [0] Following rules are strictly oriented: dyade#1(nil(),l2) = [4] l2 + [4] > [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)) #natadd(#0(),y) = [2] y + [0] >= [1] y + [0] = y #natadd(#s(x),y) = [2] y + [0] >= [2] y + [0] = #s(#natadd(x,y)) #natmult(#0(),y) = [0] >= [0] = #0() #natmult(#s(x),y) = [0] >= [0] = #natadd(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))) dyade(l1,l2) = [4] l2 + [4] >= [4] l2 + [4] = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = [4] l2 + [4] >= [4] l2 + [4] = dd(mult(x,l2),dyade(xs,l2)) mult(n,l) = [0] >= [0] = mult#1(l,n) mult(x,y) = [0] >= [0] = #mult(x,y) mult#1(dd(x,xs),n) = [0] >= [0] = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = [0] >= [0] = nil() * Step 3: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Weak TRS: #add(#0(),y) -> y #add(#neg(#s(#0())),y) -> #pred(y) #add(#pos(#s(#0())),y) -> #succ(y) dyade#1(nil(),l2) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "#0") :: [] -(0)-> "A"(0) F (TrsFun "#0") :: [] -(0)-> "A"(2) F (TrsFun "#add") :: ["A"(2) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#mult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#natadd") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#natmult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#neg") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "#neg") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#pos") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "#pos") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#pred") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "#s") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "#s") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#succ") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "dd") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "dyade") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "dyade#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "mult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "mult#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(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))) 2. Weak: #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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() * Step 4: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) dyade(l1,l2) -> dyade#1(l1,l2) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(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)) #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(nil(),l2) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "#0") :: [] -(0)-> "A"(0) F (TrsFun "#0") :: [] -(0)-> "A"(1) F (TrsFun "#0") :: [] -(0)-> "A"(7) F (TrsFun "#0") :: [] -(0)-> "A"(15) F (TrsFun "#add") :: ["A"(1) x "A"(8)] -(1)-> "A"(0) F (TrsFun "#mult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#natadd") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#natmult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#neg") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#neg") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "#pos") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#pos") :: ["A"(0)] -(1)-> "A"(1) F (TrsFun "#pos") :: ["A"(0)] -(2)-> "A"(2) F (TrsFun "#pred") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#s") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#s") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "#succ") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "dd") :: ["A"(0) x "A"(15)] -(15)-> "A"(15) F (TrsFun "dd") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "dd") :: ["A"(0) x "A"(3)] -(3)-> "A"(3) F (TrsFun "dyade") :: ["A"(15) x "A"(11)] -(6)-> "A"(3) F (TrsFun "dyade#1") :: ["A"(15) x "A"(11)] -(5)-> "A"(3) F (TrsFun "mult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "mult#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(15) F (TrsFun "nil") :: [] -(0)-> "A"(7) F (TrsFun "nil") :: [] -(0)-> "A"(5) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"#0\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"#neg\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"#pos\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"#s\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"dd\")_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: dyade(l1,l2) -> dyade#1(l1,l2) 2. Weak: #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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() * Step 5: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(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)) #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(nil(),l2) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "#0") :: [] -(0)-> "A"(0) F (TrsFun "#0") :: [] -(0)-> "A"(10) F (TrsFun "#0") :: [] -(0)-> "A"(14) F (TrsFun "#add") :: ["A"(10) x "A"(14)] -(2)-> "A"(0) F (TrsFun "#mult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#natadd") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#natmult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "#neg") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#neg") :: ["A"(10)] -(0)-> "A"(10) F (TrsFun "#pos") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#pos") :: ["A"(0)] -(0)-> "A"(10) F (TrsFun "#pos") :: ["A"(0)] -(0)-> "A"(14) F (TrsFun "#pos") :: ["A"(0)] -(0)-> "A"(2) F (TrsFun "#pred") :: ["A"(0)] -(4)-> "A"(0) F (TrsFun "#s") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "#s") :: ["A"(0)] -(10)-> "A"(10) F (TrsFun "#succ") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "dd") :: ["A"(0) x "A"(15)] -(15)-> "A"(15) F (TrsFun "dd") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "dyade") :: ["A"(15) x "A"(0)] -(1)-> "A"(0) F (TrsFun "dyade#1") :: ["A"(15) x "A"(0)] -(1)-> "A"(0) F (TrsFun "mult") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "mult#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(15) F (TrsFun "nil") :: [] -(0)-> "A"(14) F (TrsFun "nil") :: [] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"#0\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"#neg\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"#pos\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"#s\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"dd\")_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: dyade#1(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) 2. Weak: #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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() * Step 6: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(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)) #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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = 0 p(#add) = 2*x1 + x2 p(#mult) = 0 p(#natadd) = x2 p(#natmult) = 0 p(#neg) = x1 p(#pos) = x1 p(#pred) = x1 p(#s) = x1 p(#succ) = x1 p(dd) = 2 + x1 + x2 p(dyade) = 1 + x1 + 2*x1*x2 p(dyade#1) = 1 + x1 + 2*x1*x2 p(mult) = 2*x2 p(mult#1) = 2*x1 p(nil) = 1 Following rules are strictly oriented: mult#1(dd(x,xs),n) = 4 + 2*x + 2*xs > 2 + 2*x + 2*xs = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = 2 > 1 = nil() 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) = 2*x + y >= 2*x + y = #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) = y >= y = #succ(y) #add(#pos(#s(#s(x))),y) = 2*x + y >= 2*x + 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)) #natadd(#0(),y) = y >= y = y #natadd(#s(x),y) = y >= y = #s(#natadd(x,y)) #natmult(#0(),y) = 0 >= 0 = #0() #natmult(#s(x),y) = 0 >= 0 = #natadd(y,#natmult(x,y)) #pred(#0()) = 0 >= 0 = #neg(#s(#0())) #pred(#neg(#s(x))) = x >= x = #neg(#s(#s(x))) #pred(#pos(#s(#0()))) = 0 >= 0 = #0() #pred(#pos(#s(#s(x)))) = x >= x = #pos(#s(x)) #succ(#0()) = 0 >= 0 = #pos(#s(#0())) #succ(#neg(#s(#0()))) = 0 >= 0 = #0() #succ(#neg(#s(#s(x)))) = x >= x = #neg(#s(x)) #succ(#pos(#s(x))) = x >= x = #pos(#s(#s(x))) dyade(l1,l2) = 1 + l1 + 2*l1*l2 >= 1 + l1 + 2*l1*l2 = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = 3 + 4*l2 + 2*l2*x + 2*l2*xs + x + xs >= 3 + 2*l2 + 2*l2*xs + xs = dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) = 2 + 2*l2 >= 1 = nil() mult(n,l) = 2*l >= 2*l = mult#1(l,n) mult(x,y) = 2*y >= 0 = #mult(x,y) * Step 7: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) - 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)) #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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = 0 p(#add) = x1 + x2 p(#mult) = 2*x1*x2 p(#natadd) = 2*x1 + x2 p(#natmult) = 2*x1*x2 p(#neg) = x1 p(#pos) = x1 p(#pred) = 1 + x1 p(#s) = 1 + x1 p(#succ) = 1 + x1 p(dd) = x1 + x2 p(dyade) = 3*x1 + 2*x1*x2 p(dyade#1) = 3*x1 + 2*x1*x2 p(mult) = 2*x1*x2 p(mult#1) = 2*x1*x2 p(nil) = 0 Following rules are strictly oriented: #natadd(#s(x),y) = 2 + 2*x + y > 1 + 2*x + y = #s(#natadd(x,y)) Following rules are (at-least) weakly oriented: #add(#0(),y) = y >= y = y #add(#neg(#s(#0())),y) = 1 + y >= 1 + y = #pred(y) #add(#neg(#s(#s(x))),y) = 2 + x + y >= 2 + x + y = #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) = 1 + y >= 1 + y = #succ(y) #add(#pos(#s(#s(x))),y) = 2 + x + y >= 2 + x + 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)) = 2*x*y >= 2*x*y = #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) = 2*x*y >= 2*x*y = #neg(#natmult(x,y)) #mult(#pos(x),#0()) = 0 >= 0 = #0() #mult(#pos(x),#neg(y)) = 2*x*y >= 2*x*y = #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) = 2*x*y >= 2*x*y = #pos(#natmult(x,y)) #natadd(#0(),y) = y >= y = y #natmult(#0(),y) = 0 >= 0 = #0() #natmult(#s(x),y) = 2*x*y + 2*y >= 2*x*y + 2*y = #natadd(y,#natmult(x,y)) #pred(#0()) = 1 >= 1 = #neg(#s(#0())) #pred(#neg(#s(x))) = 2 + x >= 2 + x = #neg(#s(#s(x))) #pred(#pos(#s(#0()))) = 2 >= 0 = #0() #pred(#pos(#s(#s(x)))) = 3 + x >= 1 + x = #pos(#s(x)) #succ(#0()) = 1 >= 1 = #pos(#s(#0())) #succ(#neg(#s(#0()))) = 2 >= 0 = #0() #succ(#neg(#s(#s(x)))) = 3 + x >= 1 + x = #neg(#s(x)) #succ(#pos(#s(x))) = 2 + x >= 2 + x = #pos(#s(#s(x))) dyade(l1,l2) = 3*l1 + 2*l1*l2 >= 3*l1 + 2*l1*l2 = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = 2*l2*x + 2*l2*xs + 3*x + 3*xs >= 2*l2*x + 2*l2*xs + 3*xs = dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) = 0 >= 0 = nil() mult(n,l) = 2*l*n >= 2*l*n = mult#1(l,n) mult(x,y) = 2*x*y >= 2*x*y = #mult(x,y) mult#1(dd(x,xs),n) = 2*n*x + 2*n*xs >= 2*n*x + 2*n*xs = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = 0 >= 0 = nil() * Step 8: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #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)) #natadd(#0(),y) -> y #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) - 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)) #natadd(#s(x),y) -> #s(#natadd(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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = 0 p(#add) = 2 + x2 p(#mult) = 1 p(#natadd) = x2 p(#natmult) = 0 p(#neg) = x1 p(#pos) = x1 p(#pred) = x1 p(#s) = x1 p(#succ) = x1 p(dd) = 1 + x1 + x2 p(dyade) = 3*x1*x2 + 3*x1^2 + 2*x2 p(dyade#1) = 3*x1*x2 + 3*x1^2 + 2*x2 p(mult) = 2 + 3*x2 p(mult#1) = 2 + 3*x1 p(nil) = 0 Following rules are strictly oriented: #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 > 0 = #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) = 1 > 0 = #neg(#natmult(x,y)) #mult(#pos(x),#0()) = 1 > 0 = #0() #mult(#pos(x),#neg(y)) = 1 > 0 = #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) = 1 > 0 = #pos(#natmult(x,y)) mult(x,y) = 2 + 3*y > 1 = #mult(x,y) 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)) #natadd(#0(),y) = y >= y = y #natadd(#s(x),y) = y >= y = #s(#natadd(x,y)) #natmult(#0(),y) = 0 >= 0 = #0() #natmult(#s(x),y) = 0 >= 0 = #natadd(y,#natmult(x,y)) #pred(#0()) = 0 >= 0 = #neg(#s(#0())) #pred(#neg(#s(x))) = x >= x = #neg(#s(#s(x))) #pred(#pos(#s(#0()))) = 0 >= 0 = #0() #pred(#pos(#s(#s(x)))) = x >= x = #pos(#s(x)) #succ(#0()) = 0 >= 0 = #pos(#s(#0())) #succ(#neg(#s(#0()))) = 0 >= 0 = #0() #succ(#neg(#s(#s(x)))) = x >= x = #neg(#s(x)) #succ(#pos(#s(x))) = x >= x = #pos(#s(#s(x))) dyade(l1,l2) = 3*l1*l2 + 3*l1^2 + 2*l2 >= 3*l1*l2 + 3*l1^2 + 2*l2 = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = 3 + 5*l2 + 3*l2*x + 3*l2*xs + 6*x + 6*x*xs + 3*x^2 + 6*xs + 3*xs^2 >= 3 + 5*l2 + 3*l2*xs + 3*xs^2 = dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) = 2*l2 >= 0 = nil() mult(n,l) = 2 + 3*l >= 2 + 3*l = mult#1(l,n) mult#1(dd(x,xs),n) = 5 + 3*x + 3*xs >= 5 + 3*x + 3*xs = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = 2 >= 0 = nil() * Step 9: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #natadd(#0(),y) -> y #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) mult(n,l) -> mult#1(l,n) - 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)) #natadd(#s(x),y) -> #s(#natadd(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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = 2 p(#add) = 1 + x1 + 2*x1*x2 p(#mult) = 2*x1 + x2 p(#natadd) = x2 p(#natmult) = 2*x1 p(#neg) = x1 p(#pos) = x1 p(#pred) = x1 p(#s) = x1 p(#succ) = x1 p(dd) = 1 + x1 + x2 p(dyade) = 3 + 2*x1 + 2*x1*x2 + 2*x1^2 p(dyade#1) = 2*x1 + 2*x1*x2 + 2*x1^2 p(mult) = 2*x1 + 2*x1*x2 + x2 p(mult#1) = x1 + 2*x1*x2 + 2*x2 p(nil) = 0 Following rules are strictly oriented: #natmult(#0(),y) = 4 > 2 = #0() Following rules are (at-least) weakly oriented: #add(#0(),y) = 3 + 4*y >= y = y #add(#neg(#s(#0())),y) = 3 + 4*y >= y = #pred(y) #add(#neg(#s(#s(x))),y) = 1 + x + 2*x*y >= 1 + x + 2*x*y = #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) = 3 + 4*y >= y = #succ(y) #add(#pos(#s(#s(x))),y) = 1 + x + 2*x*y >= 1 + x + 2*x*y = #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) = 6 >= 2 = #0() #mult(#0(),#neg(y)) = 4 + y >= 2 = #0() #mult(#0(),#pos(y)) = 4 + y >= 2 = #0() #mult(#neg(x),#0()) = 2 + 2*x >= 2 = #0() #mult(#neg(x),#neg(y)) = 2*x + y >= 2*x = #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) = 2*x + y >= 2*x = #neg(#natmult(x,y)) #mult(#pos(x),#0()) = 2 + 2*x >= 2 = #0() #mult(#pos(x),#neg(y)) = 2*x + y >= 2*x = #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) = 2*x + y >= 2*x = #pos(#natmult(x,y)) #natadd(#0(),y) = y >= y = y #natadd(#s(x),y) = y >= y = #s(#natadd(x,y)) #natmult(#s(x),y) = 2*x >= 2*x = #natadd(y,#natmult(x,y)) #pred(#0()) = 2 >= 2 = #neg(#s(#0())) #pred(#neg(#s(x))) = x >= x = #neg(#s(#s(x))) #pred(#pos(#s(#0()))) = 2 >= 2 = #0() #pred(#pos(#s(#s(x)))) = x >= x = #pos(#s(x)) #succ(#0()) = 2 >= 2 = #pos(#s(#0())) #succ(#neg(#s(#0()))) = 2 >= 2 = #0() #succ(#neg(#s(#s(x)))) = x >= x = #neg(#s(x)) #succ(#pos(#s(x))) = x >= x = #pos(#s(#s(x))) dyade(l1,l2) = 3 + 2*l1 + 2*l1*l2 + 2*l1^2 >= 2*l1 + 2*l1*l2 + 2*l1^2 = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = 4 + 2*l2 + 2*l2*x + 2*l2*xs + 6*x + 4*x*xs + 2*x^2 + 6*xs + 2*xs^2 >= 4 + l2 + 2*l2*x + 2*l2*xs + 2*x + 2*xs + 2*xs^2 = dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) = 0 >= 0 = nil() mult(n,l) = l + 2*l*n + 2*n >= l + 2*l*n + 2*n = mult#1(l,n) mult(x,y) = 2*x + 2*x*y + y >= 2*x + y = #mult(x,y) mult#1(dd(x,xs),n) = 1 + 4*n + 2*n*x + 2*n*xs + x + xs >= 1 + 4*n + 2*n*x + 2*n*xs + x + xs = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = 2*n >= 0 = nil() * Step 10: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #natadd(#0(),y) -> y #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) mult(n,l) -> mult#1(l,n) - 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)) #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = 0 p(#add) = 1 + x2 p(#mult) = x1*x2 p(#natadd) = x2 p(#natmult) = x1*x2 p(#neg) = x1 p(#pos) = x1 p(#pred) = x1 p(#s) = x1 p(#succ) = x1 p(dd) = 1 + x1 + x2 p(dyade) = 3 + 3*x1 + 3*x1*x2 p(dyade#1) = 3 + 3*x1 + 3*x1*x2 p(mult) = 1 + x1*x2 + 3*x2 p(mult#1) = 3*x1 + x1*x2 p(nil) = 0 Following rules are strictly oriented: mult(n,l) = 1 + 3*l + l*n > 3*l + l*n = mult#1(l,n) Following rules are (at-least) weakly oriented: #add(#0(),y) = 1 + y >= y = y #add(#neg(#s(#0())),y) = 1 + y >= y = #pred(y) #add(#neg(#s(#s(x))),y) = 1 + y >= 1 + y = #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) = 1 + y >= y = #succ(y) #add(#pos(#s(#s(x))),y) = 1 + y >= 1 + 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)) = x*y >= x*y = #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) = x*y >= x*y = #neg(#natmult(x,y)) #mult(#pos(x),#0()) = 0 >= 0 = #0() #mult(#pos(x),#neg(y)) = x*y >= x*y = #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) = x*y >= x*y = #pos(#natmult(x,y)) #natadd(#0(),y) = y >= y = y #natadd(#s(x),y) = y >= y = #s(#natadd(x,y)) #natmult(#0(),y) = 0 >= 0 = #0() #natmult(#s(x),y) = x*y >= x*y = #natadd(y,#natmult(x,y)) #pred(#0()) = 0 >= 0 = #neg(#s(#0())) #pred(#neg(#s(x))) = x >= x = #neg(#s(#s(x))) #pred(#pos(#s(#0()))) = 0 >= 0 = #0() #pred(#pos(#s(#s(x)))) = x >= x = #pos(#s(x)) #succ(#0()) = 0 >= 0 = #pos(#s(#0())) #succ(#neg(#s(#0()))) = 0 >= 0 = #0() #succ(#neg(#s(#s(x)))) = x >= x = #neg(#s(x)) #succ(#pos(#s(x))) = x >= x = #pos(#s(#s(x))) dyade(l1,l2) = 3 + 3*l1 + 3*l1*l2 >= 3 + 3*l1 + 3*l1*l2 = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = 6 + 3*l2 + 3*l2*x + 3*l2*xs + 3*x + 3*xs >= 5 + 3*l2 + l2*x + 3*l2*xs + 3*xs = dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) = 3 >= 0 = nil() mult(x,y) = 1 + x*y + 3*y >= x*y = #mult(x,y) mult#1(dd(x,xs),n) = 3 + n + n*x + n*xs + 3*x + 3*xs >= 3 + n*x + n*xs + 3*x + 3*xs = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = 0 >= 0 = nil() * Step 11: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #natadd(#0(),y) -> y #natmult(#s(x),y) -> #natadd(y,#natmult(x,y)) - 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)) #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,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(#natadd) = {2}, uargs(#neg) = {1}, uargs(#pos) = {1}, uargs(#pred) = {1}, uargs(#s) = {1}, uargs(#succ) = {1}, uargs(dd) = {1,2} Following symbols are considered usable: {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1,mult,mult#1} TcT has computed the following interpretation: p(#0) = 1 p(#add) = x1 + x2 p(#mult) = x1 + 2*x1*x2 + x2 p(#natadd) = 2*x1 + x2 p(#natmult) = x1 + 2*x1*x2 p(#neg) = x1 p(#pos) = x1 p(#pred) = 1 + x1 p(#s) = 1 + x1 p(#succ) = 1 + x1 p(dd) = 1 + x1 + x2 p(dyade) = 2*x1 + 3*x1*x2 + 2*x1^2 + 2*x2^2 p(dyade#1) = 2*x1 + 3*x1*x2 + 2*x1^2 + 2*x2^2 p(mult) = x1 + 2*x1*x2 + 2*x2 p(mult#1) = 2*x1 + 2*x1*x2 p(nil) = 1 Following rules are strictly oriented: #natadd(#0(),y) = 2 + y > y = y #natmult(#s(x),y) = 1 + x + 2*x*y + 2*y > x + 2*x*y + 2*y = #natadd(y,#natmult(x,y)) Following rules are (at-least) weakly oriented: #add(#0(),y) = 1 + y >= y = y #add(#neg(#s(#0())),y) = 2 + y >= 1 + y = #pred(y) #add(#neg(#s(#s(x))),y) = 2 + x + y >= 2 + x + y = #pred(#add(#pos(#s(x)),y)) #add(#pos(#s(#0())),y) = 2 + y >= 1 + y = #succ(y) #add(#pos(#s(#s(x))),y) = 2 + x + y >= 2 + x + y = #succ(#add(#pos(#s(x)),y)) #mult(#0(),#0()) = 4 >= 1 = #0() #mult(#0(),#neg(y)) = 1 + 3*y >= 1 = #0() #mult(#0(),#pos(y)) = 1 + 3*y >= 1 = #0() #mult(#neg(x),#0()) = 1 + 3*x >= 1 = #0() #mult(#neg(x),#neg(y)) = x + 2*x*y + y >= x + 2*x*y = #pos(#natmult(x,y)) #mult(#neg(x),#pos(y)) = x + 2*x*y + y >= x + 2*x*y = #neg(#natmult(x,y)) #mult(#pos(x),#0()) = 1 + 3*x >= 1 = #0() #mult(#pos(x),#neg(y)) = x + 2*x*y + y >= x + 2*x*y = #neg(#natmult(x,y)) #mult(#pos(x),#pos(y)) = x + 2*x*y + y >= x + 2*x*y = #pos(#natmult(x,y)) #natadd(#s(x),y) = 2 + 2*x + y >= 1 + 2*x + y = #s(#natadd(x,y)) #natmult(#0(),y) = 1 + 2*y >= 1 = #0() #pred(#0()) = 2 >= 2 = #neg(#s(#0())) #pred(#neg(#s(x))) = 2 + x >= 2 + x = #neg(#s(#s(x))) #pred(#pos(#s(#0()))) = 3 >= 1 = #0() #pred(#pos(#s(#s(x)))) = 3 + x >= 1 + x = #pos(#s(x)) #succ(#0()) = 2 >= 2 = #pos(#s(#0())) #succ(#neg(#s(#0()))) = 3 >= 1 = #0() #succ(#neg(#s(#s(x)))) = 3 + x >= 1 + x = #neg(#s(x)) #succ(#pos(#s(x))) = 2 + x >= 2 + x = #pos(#s(#s(x))) dyade(l1,l2) = 2*l1 + 3*l1*l2 + 2*l1^2 + 2*l2^2 >= 2*l1 + 3*l1*l2 + 2*l1^2 + 2*l2^2 = dyade#1(l1,l2) dyade#1(dd(x,xs),l2) = 4 + 3*l2 + 3*l2*x + 3*l2*xs + 2*l2^2 + 6*x + 4*x*xs + 2*x^2 + 6*xs + 2*xs^2 >= 1 + 2*l2 + 2*l2*x + 3*l2*xs + 2*l2^2 + x + 2*xs + 2*xs^2 = dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) = 4 + 3*l2 + 2*l2^2 >= 1 = nil() mult(n,l) = 2*l + 2*l*n + n >= 2*l + 2*l*n = mult#1(l,n) mult(x,y) = x + 2*x*y + 2*y >= x + 2*x*y + y = #mult(x,y) mult#1(dd(x,xs),n) = 2 + 2*n + 2*n*x + 2*n*xs + 2*x + 2*xs >= 1 + 2*n + 2*n*x + 2*n*xs + 2*x + 2*xs = dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) = 2 + 2*n >= 1 = nil() * Step 12: 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)) #natadd(#0(),y) -> y #natadd(#s(x),y) -> #s(#natadd(x,y)) #natmult(#0(),y) -> #0() #natmult(#s(x),y) -> #natadd(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(dd(x,xs),l2) -> dd(mult(x,l2),dyade(xs,l2)) dyade#1(nil(),l2) -> nil() mult(n,l) -> mult#1(l,n) mult(x,y) -> #mult(x,y) mult#1(dd(x,xs),n) -> dd(mult(n,x),mult(n,xs)) mult#1(nil(),n) -> nil() - Signature: {#add/2,#mult/2,#natadd/2,#natmult/2,#pred/1,#succ/1,dyade/2,dyade#1/2,mult/2,mult#1/2} / {#0/0,#neg/1 ,#pos/1,#s/1,dd/2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {#add,#mult,#natadd,#natmult,#pred,#succ,dyade,dyade#1 ,mult,mult#1} and constructors {#0,#neg,#pos,#s,dd,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))