A4vec-0
(a4vec-0) return an a4vec that evaluates to 0 under
every environment.
Macro: a4vec-0
(defmacro a4vec-0 nil
(list 'quote
(a4vec (aig-sterm nil)
(aig-sterm nil))))
Definitions and Theorems
Theorem: a4vec-0-correct
(defthm a4vec-0-correct
(equal (a4vec-eval (a4vec-0) env)
(4vec 0 0)))
