You must work in pairs on this assignment. Put names on your solutions like this: Student name 1: TODO: PUT ONE NAME HERE Student name 2: TODO: PUT OTHER NAME HERE This assignment will NOT involve ACL2s, though you may use the .lisp editor in ACL2s to help with code/formula formatting. You must construct proofs by hand in the style presented in class, and turn them in in a text file (.txt or .lisp is OK. .doc or .docx or .rtf is NOT) Follow the proof format as shown in the sample proof. Open the pdf of the homework