(VAR @_@1 @b @b1 @b2 @b3 @n @r @r' @s @x @x_1 @x_2 @xs @y @y_1 @y_2 @ys @z @zs ) (STRATEGY INNERMOST) (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,*(@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)))) #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))) )