Multiplication function
Completion Axiom (completion-of-*):
(equal (binary-* x y) (if (acl2-numberp x) (if (acl2-numberp y) (binary-* x y) 0) 0))
Guard for (binary-* x y):
(and (acl2-numberp x) (acl2-numberp y))
Notice that like all arithmetic functions, binary-* treats non-numeric inputs as 0.
Calls of the macro * expand to calls of binary-*; see *.
