(VAR x y z xs)
(RULES
 times(x,y) -> sum(generate(x,y))
 generate(x,y) -> gen(x,y,0)
 gen(x,y,z) -> if(ge(z,x),x,y,z)
 if(true,x,y,z) -> nil
 if(false,x,y,z) -> cons(y,gen(x,y,s(z)))
 sum(nil) -> 0
 sum(cons(0,xs)) -> sum(xs)
 sum(cons(s(x),xs)) -> s(sum(cons(x,xs)))
 ge(x,0) -> true
 ge(0,s(y)) -> false
 ge(s(x),s(y)) -> ge(x,y)
)