Major Section: ACL2-BUILT-INS

Completion Axiom (completion-of-denominator):

completion-of-denominator

(equal (denominator x) (if (rationalp x) (denominator x) 1))

Guard for (denominator x):

(denominator x)

(rationalp x)