@misc(Equal-by-nths,
 title        = {Equal-by-nths},
 howpublished = {\url{https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____EQUAL-BY-NTHS}},
 note         = {Accessed: 2022-02-26},
)
@inbook(Bertoli2000,
 author       = {Piergiorgio Bertoli and Paolo Traverso},
 year         = {2000},
 title        = {Design Verification of a Safety-Critical Embedded Verifier},
 pages        = {233--245},
 publisher    = {Springer US},
 address      = {Boston, MA},
 doi          = {10.1007/978-1-4757-3188-0_14},
)
@inproceedings(gamboa2003using,
 author       = {Ruben Gamboa and John Cowles and JV Baalen},
 year         = {2003},
 title        = {Using {ACL}2 {A}rrays to {F}ormalize {M}atrix {A}lgebra},
 booktitle    = {Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2\IeC{\textquoteright}03)},
 volume       = {1},
)
@book(jech2008axiom,
 author       = {Thomas J Jech},
 year         = {2008},
 title        = {The {A}xiom of {C}hoice},
 publisher    = {Courier Corporation},
)
@misc(Equal-by-nths1,
 author       = {Rotation matrix},
 year         = {2021},
 title        = {Rotation matrix --- {W}ikipedia{,} The Free Encyclopedia},
 howpublished = {\url{https://en.wikipedia.org/wiki/Rotation_matrix}},
 note         = {Online; Accessed: 2022-02-04},
)
@unpublished(banachmadeline,
 author       = {Madeline Tremblay},
 year         = {2017},
 title        = {The {B}anach-{T}arski {P}aradox},
 note         = {Unpublished},
)
@article(weston2016banach,
 author       = {Tom Weston},
 year         = {2016},
 title        = {The {B}anach-{T}arski {P}aradox},
 journal      = {Citado},
 volume       = {2},
 pages        = {15},
)