(STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (VAR @_@1 @b @b1 @b2 @b3 @n @r @r' @s @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys @z @zs) (RULES #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,*(@y,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())))) #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)) ->= #positive(#natdiv(@x,@y)) #div(#neg(@x),#pos(@y)) ->= #negative(#natdiv(@x,@y)) #div(#pos(@x),#0()) ->= #divByZero() #div(#pos(@x),#neg(@y)) ->= #negative(#natdiv(@x,@y)) #div(#pos(@x),#pos(@y)) ->= #positive(#natdiv(@x,@y)) #divsub(#0(),#0()) ->= #0() #divsub(#0(),#s(@y)) ->= #underflow() #divsub(#s(@x),#0()) ->= #s(@x) #divsub(#s(@x),#s(@y)) ->= #divsub(@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)) #natadd(#0(),@y) ->= @y #natadd(#s(@x),@y) ->= #s(#natadd(@x,@y)) #natdiv(#0(),#0()) ->= #divByZero() #natdiv(#0(),#s(@y)) ->= #0() #natdiv(#s(@x),#0()) ->= #divByZero() #natdiv(#s(@x),#s(@y)) ->= #natdiv'(#divsub(@x,@y),#s(@y)) #natdiv'(#0(),@y) ->= #s(#0()) #natdiv'(#s(@x),@y) ->= #s(#natdiv(#s(@x),@y)) #natdiv'(#underflow(),@y) ->= #0() #natmult(#0(),@y) ->= #0() #natmult(#s(@x),@y) ->= #natadd(@y,#natmult(@x,@y)) #natsub(@x,#0()) ->= @x #natsub(#s(@x),#s(@y)) ->= #natsub(@x,@y) #negative(#0()) ->= #0() #negative(#neg(@x)) ->= #pos(@x) #negative(#pos(@x)) ->= #neg(@x) #negative(#s(@x)) ->= #neg(#s(@x)) #positive(#0()) ->= #0() #positive(#neg(@x)) ->= #neg(@x) #positive(#pos(@x)) ->= #pos(@x) #positive(#s(@x)) ->= #pos(#s(@x)) #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)))) (COMMENT This TRS was automatically generated from the resource aware ML program 'bitvectors.raml', c.f. http://raml.tcs.ifi.lmu.de/)