NUMERATOR

dividend of a ratio in lowest terms 
Major Section:  ACL2-BUILT-INS

Completion Axiom (completion-of-numerator): 

(equal (numerator x)
       (if (rationalp x)
           (numerator x)
         0))

Guard for (numerator x): 

(rationalp x)