(GOAL COMPLEXITY) (STARTTERM CONSTRUCTOR-BASED) (STRATEGY INNERMOST) (STRATEGY INNERMOST) (VAR @l @l1 @l2 @n @x @xs @y) (DATATYPES A = µX.< ::(X, X), nil, #0, #neg(X), #s(X), #pos(X) >) (SIGNATURES * :: [A x A] -> A dyade :: [A x A] -> A dyade#1 :: [A x A] -> A mult :: [A x A] -> A mult#1 :: [A x A] -> A #add :: [A x A] -> A #mult :: [A x A] -> A #natmult :: [A x A] -> A #pred :: [A] -> A #succ :: [A] -> A) (RULES *(@x,@y) -> #mult(@x,@y) dyade(@l1,@l2) -> dyade#1(@l1 ,@l2) dyade#1(::(@x,@xs),@l2) -> ::(mult(@x,@l2),dyade(@xs,@l2)) dyade#1(nil(),@l2) -> nil() mult(@n,@l) -> mult#1(@l,@n) mult#1(::(@x,@xs),@n) -> ::(*(@n ,@x) ,mult(@n,@xs)) mult#1(nil(),@n) -> nil() #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))))