provide a way to `or` rules together

[k4b7]

For instance, we'd like a single rule for a + 0 => a and 0 + a => a. It would be nice if there we could create a rule that would match either of these situations from simpler rules.

[tkosan]

In some CASs commutativity and associativity are built into the matcher, and in other CASs they are explicitly encoded in rewrite rules. In MathPiper they are encoded in rewrite rules.

[k4b7]

@tkosan could you post an example of how MathPip encodes commutativity and associativity in its rewrite rules?

[tkosan]

@kevinbarabash here are MathPiper's rewrite rules for addition:

MathPiper's addition rewrite rules

There are a number of examples of commutatively in these rules. Associativity would be achieved by using parentheses in the head of a rule.

[tkosan]

@kevinbarabash here is an example of associativity being used:

200 # (x_ / y_)/ z_ <-- x/(y*z);
230 # x_ / (y_ / z_) <-- (x*z)/y;