| Input File | Output File | The Proof | Commentary | Date |
| PA-distributivity.in | PA-distributivity.out | PA-distributivity.prf | PA-distributivity.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| PA-assocplus.in | PA-assocplus.out | PA-assocplus.prf | PA-assocplus.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| PA-Trichotomy.in | PA-Trichotomy.out | PA-Trichotomy.prf | PA-Trichotomy.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| le.in | le.out | le.prf | le.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| PA-complus.in | PA-complus.out | PA-complus.prf | PA-complus.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| PA-OrderTransitivity.in | PA-OrderTransitivity.out | PA-OrderTransitivity.prf | PA-OrderTransitivity.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| PA-multcom.in | PA-multcom.out | PA-multcom.prf | PA-multcom.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| le2.in | le2.out | le2.prf | le2.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| le3.in | le3.out | le3.prf | le3.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| PA-TwoToTheN.in | PA-TwoToTheN.out | PA-TwoToTheN.prf | PA-TwoToTheN.html | Tue, 25 Nov 2025 11:47:43 +0000 |
| PA-cancellation.in | PA-cancellation.out | PA-cancellation.prf | PA-cancellation.html | Tue, 25 Nov 2025 11:47:43 +0000 |
