(in-package "ACL2")

(ubt! 1)

(certify-book "term-defuns")

:u

(certify-book "term-lemmas" 0 nil)

:u

(certify-book "meta-plus-equal")

:u

(certify-book "meta-plus-lessp")

:u

(certify-book "meta-times-equal")

:u

(certify-book "meta" 0 nil)

:u

(certify-book "../arithmetic/top-with-meta" 0)

:u