7/9/26
You can try some of the testing
The PLI rules have been tested and should be working.
The PME rules also should be working, but they have not been fully tested yet.
Testing the PME rules.
[When there is a suitable match, a rewrite rule can rewrite an entire formula or a subformula of a formula. This opens the way to a short cut when testing manually. For example, the entire formula P∨(Q.R) ≡(P∨Q).(P∨R) cannot be rewritten by a Dist rule p∨(q.r) :: (p∨q).(p∨r) but the left subformula of it can be rewritten to (P∨Q).(P∨R) ≡(P∨Q).(P∨R), alternatively the right subformula can be rewritten to P∨(Q.R) ≡P∨(Q.R). Checking that both these rewrites goes through gives an assurance that this Dist rule is working (left-to-right and right-to-left). This technique has little or no educational value. But it does speed up manual testing.]