This is our 2800 final project . We worked on proving (thm (implies (and (lorp ls) (descendingp ls)) (descending-powersetp (powerset ls)))) in ACL2s.
When passing this in ACL2s, make sure to copy over all of our functions from the functions file and the proof from the proof file. Included in this project, we also have our old versions of the functions (powerset in particular) and lemmas that we thought we needed, but didn't end up using. Those are in the old lemma file.
To access the structure of this repository, reference the file called Program Structure