MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) computeLine(@line,@m,@acc) -> computeLine#1(@line,@acc,@m) computeLine#1(::(@x,@xs),@acc,@m) -> computeLine#2(@m,@acc,@x,@xs) computeLine#1(nil(),@acc,@m) -> @acc computeLine#2(::(@l,@ls),@acc,@x,@xs) -> computeLine(@xs,@ls,lineMult(@x,@l,@acc)) computeLine#2(nil(),@acc,@x,@xs) -> nil() lineMult(@n,@l1,@l2) -> lineMult#1(@l1,@l2,@n) lineMult#1(::(@x,@xs),@l2,@n) -> lineMult#2(@l2,@n,@x,@xs) lineMult#1(nil(),@l2,@n) -> nil() lineMult#2(::(@y,@ys),@n,@x,@xs) -> ::(+(*(@x,@n),@y),lineMult(@n,@xs,@ys)) lineMult#2(nil(),@n,@x,@xs) -> ::(*(@x,@n),lineMult(@n,@xs,nil())) matrixMult(@m1,@m2) -> matrixMult#1(@m1,@m2) matrixMult#1(::(@l,@ls),@m2) -> ::(computeLine(@l,@m2,nil()),matrixMult(@ls,@m2)) matrixMult#1(nil(),@m2) -> 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,+/2,computeLine/3,computeLine#1/3,computeLine#2/4,lineMult/3 ,lineMult#1/3,lineMult#2/4,matrixMult/2,matrixMult#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,*,+,computeLine ,computeLine#1,computeLine#2,lineMult,lineMult#1,lineMult#2,matrixMult,matrixMult#1} and constructors {#0 ,#neg,#pos,#s,::,nil} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: Incompatible MAYBE