Major Section: PROGRAMMING

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)