Verification Update #9
Description
Currently verification for rules with multiple parents is done in a hacky way where for each node we do a search over all parent's formula to determine if it is the correct form. For an example see the following code where we need to compute the left and right parents individually.
https://github.com/James-Oswald/lazyslate/blob/master/src/core/Proof/verify.ts#L242C15-L261
This type code is the source of many bugs (including #8). A better way to write this would be to generalize by writing a verification method for each rule that assumes the Premise proof nodes are passed in in a given order, just like how the real inference rules work. With this we can then try to verify all permutations of the premises, if just one of these verifies than the node verifies, otherwise if none of the permutations verify the node does not verify.
Additionally, this method probably does not sacrifice efficiency over the current version. Or Elim, the largest rule, only has 6 permutations of parents, and the code already basically checks these inside of the current verification function.