complex - ACL2 Book

other

(in-package "ACL2")

complex-openertheorem

(defthm complex-opener
  (equal (complex x y)
    (+ (realfix x) (* #C(0 1) (realfix y))))
  :hints (("Goal" :use (:instance complex-definition
       (x (realfix x))
       (y (realfix y))))))