| Input File | Output File | The Proof | Commentary | Date |
| PA-OrderTransitivity.in | PA-OrderTransitivity.out | PA-OrderTransitivity.prf | PA-OrderTransitivity.html | Sun, 07 Aug 2005 23:29:13 -0700 |
| PA-Trichotomy.in | PA-Trichotomy.out | PA-Trichotomy.prf | PA-Trichotomy.html | Sun, 07 Aug 2005 23:29:15 -0700 |
| PA-TwoToTheN.in | PA-TwoToTheN.out | PA-TwoToTheN.prf | PA-TwoToTheN.html | Wed, 10 Aug 2005 22:23:37 -0700 |
| PA-assocplus.in | PA-assocplus.out | PA-assocplus.prf | PA-assocplus.html | Sun, 07 Aug 2005 23:27:27 -0700 |
| PA-cancellation.in | PA-cancellation.out | PA-cancellation.prf | PA-cancellation.html | Sun, 07 Aug 2005 23:27:28 -0700 |
| PA-complus.in | PA-complus.out | PA-complus.prf | PA-complus.html | Sun, 07 Aug 2005 23:27:29 -0700 |
| PA-distributivity.in | PA-distributivity.out | PA-distributivity.prf | PA-distributivity.html | Sun, 07 Aug 2005 23:27:45 -0700 |
| PA-multcom.in | PA-multcom.out | PA-multcom.prf | PA-multcom.html | Tue, 06 Dec 2005 23:28:04 -0800 |
| le.in | le.out | le.prf | le.html | Tue, 04 Jul 2006 12:58:10 -0700 |
| le2.in | le2.out | le2.prf | le2.html | Wed, 10 Aug 2005 22:23:33 -0700 |
| le3.in | le3.out | le3.prf | le3.html | Thu, 06 Jul 2006 12:01:43 -0700 |