include ../Makefile-generic

#Put dependencies (from `make -s dependencies, or other sources) below

basic-definitions-thms.cert: basic-definitions-thms.lisp
basic-definitions-thms.cert: ordinal-total-order.cert

ordinal-isomorphism.cert: ordinal-isomorphism.lisp
ordinal-isomorphism.cert: basic-definitions-thms.cert
ordinal-isomorphism.cert: top-with-meta.cert
ordinal-isomorphism.cert: ordinal-addition.cert

limits.cert: limits.lisp
limits.cert: ordinal-exponentiation.cert

ordinal-addition.cert: ordinal-addition.lisp
ordinal-addition.cert: basic-definitions-thms.cert
ordinal-addition.cert: top-with-meta.cert

ordinal-counter-examples.cert: ordinal-counter-examples.lisp
ordinal-counter-examples.cert: ordinal-definitions.cert

ordinal-definitions.cert: ordinal-definitions.lisp

ordinal-exponentiation.cert: ordinal-exponentiation.lisp
ordinal-exponentiation.cert: ordinal-multiplication.cert

ordinal-multiplication.cert: ordinal-multiplication.lisp
ordinal-multiplication.cert: ordinal-addition.cert

ordinal-total-order.cert: ordinal-total-order.lisp
ordinal-total-order.cert: ordinal-definitions.cert

top-with-meta.cert: top-with-meta.lisp
top-with-meta.cert: ../arithmetic/top-with-meta.cert
