MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: #abs(#0()) -> #0() #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #equal(@x,@y) -> #eq(@x,@y) #greater(@x,@y) -> #ckgt(#compare(@x,@y)) #less(@x,@y) -> #cklt(#compare(@x,@y)) *(@x,@y) -> #mult(@x,@y) +(@x,@y) -> #add(@x,@y) -(@x,@y) -> #sub(@x,@y) add(@b1,@b2) -> add'(@b1,@b2,#abs(#0())) add'(@b1,@b2,@r) -> add'#1(@b1,@b2,@r) add'#1(::(@x,@xs),@b2,@r) -> add'#2(@b2,@r,@x,@xs) add'#1(nil(),@b2,@r) -> nil() add'#2(::(@y,@ys),@r,@x,@xs) -> add'#3(sum(@x,@y,@r),@xs,@ys) add'#2(nil(),@r,@x,@xs) -> nil() add'#3(tuple#2(@z,@r'),@xs,@ys) -> ::(@z,add'(@xs,@ys,@r')) bitToInt(@b) -> bitToInt'(@b,#abs(#pos(#s(#0())))) bitToInt'(@b,@n) -> bitToInt'#1(@b,@n) bitToInt'#1(::(@x,@xs),@n) -> +(*(@x,@n),bitToInt'(@xs,*(@n,#pos(#s(#s(#0())))))) bitToInt'#1(nil(),@n) -> #abs(#0()) compare(@b1,@b2) -> compare#1(@b1,@b2) compare#1(::(@x,@xs),@b2) -> compare#2(@b2,@x,@xs) compare#1(nil(),@b2) -> #abs(#0()) compare#2(::(@y,@ys),@x,@xs) -> compare#3(compare(@xs,@ys),@x,@y) compare#2(nil(),@x,@xs) -> #abs(#0()) compare#3(@r,@x,@y) -> compare#4(#equal(@r,#0()),@r,@x,@y) compare#4(#false(),@r,@x,@y) -> @r compare#4(#true(),@r,@x,@y) -> compare#5(#less(@x,@y),@x,@y) compare#5(#false(),@x,@y) -> compare#6(#greater(@x,@y)) compare#5(#true(),@x,@y) -> -(#0(),#pos(#s(#0()))) compare#6(#false()) -> #abs(#0()) compare#6(#true()) -> #abs(#pos(#s(#0()))) diff(@x,@y,@r) -> tuple#2(mod(+(+(@x,@y),@r),#pos(#s(#s(#0())))),diff#1(#less(-(-(@x,@y),@r),#0()))) diff#1(#false()) -> #abs(#0()) diff#1(#true()) -> #abs(#pos(#s(#0()))) div(@x,@y) -> #div(@x,@y) leq(@b1,@b2) -> #less(compare(@b1,@b2),#pos(#s(#0()))) mod(@x,@y) -> -(@x,*(@x,div(@x,@y))) mult(@b1,@b2) -> mult#1(@b1,@b2) mult#1(::(@x,@xs),@b2) -> mult#2(::(#abs(#0()),mult(@xs,@b2)),@b2,@x) mult#1(nil(),@b2) -> nil() mult#2(@zs,@b2,@x) -> mult#3(#equal(@x,#pos(#s(#0()))),@b2,@zs) mult#3(#false(),@b2,@zs) -> @zs mult#3(#true(),@b2,@zs) -> add(@b2,@zs) mult3(@b1,@b2,@b3) -> mult(mult(@b1,@b2),@b2) sub(@b1,@b2) -> sub#1(sub'(@b1,@b2,#abs(#0()))) sub#1(tuple#2(@b,@_@1)) -> @b sub'(@b1,@b2,@r) -> sub'#1(@b1,@b2,@r) sub'#1(::(@x,@xs),@b2,@r) -> sub'#2(@b2,@r,@x,@xs) sub'#1(nil(),@b2,@r) -> tuple#2(nil(),@r) sub'#2(::(@y,@ys),@r,@x,@xs) -> sub'#3(diff(@x,@y,@r),@xs,@ys) sub'#2(nil(),@r,@x,@xs) -> tuple#2(nil(),@r) sub'#3(tuple#2(@z,@r'),@xs,@ys) -> sub'#4(sub'(@xs,@ys,@r'),@z) sub'#4(tuple#2(@zs,@s),@z) -> tuple#2(sub'#5(#equal(@s,#pos(#s(#0()))),@z,@zs),@s) sub'#5(#false(),@z,@zs) -> ::(@z,@zs) sub'#5(#true(),@z,@zs) -> ::(#abs(#0()),@zs) sum(@x,@y,@r) -> sum#1(+(+(@x,@y),@r)) sum#1(@s) -> sum#2(#equal(@s,#0()),@s) sum#2(#false(),@s) -> sum#3(#equal(@s,#pos(#s(#0()))),@s) sum#2(#true(),@s) -> tuple#2(#abs(#0()),#abs(#0())) sum#3(#false(),@s) -> sum#4(#equal(@s,#pos(#s(#s(#0()))))) sum#3(#true(),@s) -> tuple#2(#abs(#pos(#s(#0()))),#abs(#0())) sum#4(#false()) -> tuple#2(#abs(#pos(#s(#0()))),#abs(#pos(#s(#0())))) sum#4(#true()) -> tuple#2(#abs(#0()),#abs(#pos(#s(#0())))) - 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)) #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #ckgt(#EQ()) -> #false() #ckgt(#GT()) -> #true() #ckgt(#LT()) -> #false() #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #div(#0(),#0()) -> #divByZero() #div(#0(),#neg(@y)) -> #0() #div(#0(),#pos(@y)) -> #0() #div(#neg(@x),#0()) -> #divByZero() #div(#neg(@x),#neg(@y)) -> #pos(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#0()) -> #divByZero() #div(#pos(@x),#neg(@y)) -> #neg(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) -> #pos(#natdiv(@x,@y)) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(::(@x_1,@x_2),tuple#2(@y_1,@y_2)) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #eq(nil(),tuple#2(@y_1,@y_2)) -> #false() #eq(tuple#2(@x_1,@x_2),::(@y_1,@y_2)) -> #false() #eq(tuple#2(@x_1,@x_2),nil()) -> #false() #eq(tuple#2(@x_1,@x_2),tuple#2(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #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)) #natdiv(#0(),#0()) -> #divByZero() #natdiv(#s(@x),#s(@y)) -> #s(#natdiv(#natsub(@x,@y),#s(@y))) #natmult(#0(),@y) -> #0() #natmult(#s(@x),@y) -> #add(#pos(@y),#natmult(@x,@y)) #natsub(@x,#0()) -> @x #natsub(#s(@x),#s(@y)) -> #natsub(@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)) #sub(@x,#0()) -> @x #sub(@x,#neg(@y)) -> #add(@x,#pos(@y)) #sub(@x,#pos(@y)) -> #add(@x,#neg(@y)) #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: {#abs/1,#add/2,#and/2,#ckgt/1,#cklt/1,#compare/2,#div/2,#eq/2,#equal/2,#greater/2,#less/2,#mult/2,#natdiv/2 ,#natmult/2,#natsub/2,#pred/1,#sub/2,#succ/1,*/2,+/2,-/2,add/2,add'/3,add'#1/3,add'#2/4,add'#3/3,bitToInt/1 ,bitToInt'/2,bitToInt'#1/2,compare/2,compare#1/2,compare#2/3,compare#3/3,compare#4/4,compare#5/3,compare#6/1 ,diff/3,diff#1/1,div/2,leq/2,mod/2,mult/2,mult#1/2,mult#2/3,mult#3/3,mult3/3,sub/2,sub#1/1,sub'/3,sub'#1/3 ,sub'#2/4,sub'#3/3,sub'#4/2,sub'#5/3,sum/3,sum#1/1,sum#2/2,sum#3/2,sum#4/1} / {#0/0,#EQ/0,#GT/0,#LT/0 ,#divByZero/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,::/2,nil/0,tuple#2/2} - Obligation: innermost runtime complexity wrt. defined symbols {#abs,#add,#and,#ckgt,#cklt,#compare,#div,#eq,#equal ,#greater,#less,#mult,#natdiv,#natmult,#natsub,#pred,#sub,#succ,*,+,-,add,add',add'#1,add'#2,add'#3,bitToInt ,bitToInt',bitToInt'#1,compare,compare#1,compare#2,compare#3,compare#4,compare#5,compare#6,diff,diff#1,div ,leq,mod,mult,mult#1,mult#2,mult#3,mult3,sub,sub#1,sub',sub'#1,sub'#2,sub'#3,sub'#4,sub'#5,sum,sum#1,sum#2 ,sum#3,sum#4} and constructors {#0,#EQ,#GT,#LT,#divByZero,#false,#neg,#pos,#s,#true,::,nil,tuple#2} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: Incompatible MAYBE