include ../../../Makefile-generic

ACL2 = ../../../../saved_acl2

# Dependencies:

aof.cert: aof.lisp
aof.cert: ../../../arithmetic/inequalities.cert

exercise1.cert: exercise1.lisp

exercise2.cert: exercise2.lisp

exercise3.cert: exercise3.lisp
exercise3.cert: ../../../ordinals/e0-ordinal.cert

exercise4a.cert: exercise4a.lisp

exercise4b.cert: exercise4b.lisp

exercise5.cert: exercise5.lisp

exercise6a.cert: exercise6a.lisp

exercise6b.cert: exercise6b.lisp

exercise7a.cert: exercise7a.lisp

exercise7b.cert: exercise7b.lisp

knuth-arch.cert: knuth-arch.lisp
knuth-arch.cert: ../../../arithmetic/top-with-meta.cert
knuth-arch.cert: ../../../ordinals/e0-ordinal.cert
knuth-arch.cert: aof.cert