Theorem:
mult_commute
  ?a * ?b = ?b * ?a


applied to: r  +  (s^2 + 3) * 4 + t
at: r + ?a * ?b + t
under order: total_degree_order
?a * ?b
..matches.. (s^2 + 3) * 4
?b * ?a
..instantiates to.. 4 * (s^2 + 3)
results in: r + 4 * (s^2 + 3) + t


Proof of the theorem

Explanations:

An intutive example for this theorem is 21 elements arranged like this:

x
x
x
x
x
x
x
x
x
x
x
x
x
x
x
x
x
x
x
x
x

You can see either 3 rows of 7 giving 21 (3 * 7 = 21) or 7 colums of 3 giving 21 (7 * 3 = 21) as well.

Remark on rewrite orders:

The  theorem applied once always gives a result which allows to apply the theorem another time:

 r  +  (s^2 + 3) * 4 + t
 r  +  4 * (s^2 + 3) + t
 r  +  (s^2 + 3) * 4 + t
 r  +  4 * (s^2 + 3) + t
:
:

Usually such a theorem (called a 'rewrite rule') is put into a rule set, and then the rules are applied to a formula until none of the rules in the set can be applied any more (this is called 'simplification'). Obviously, the rule 'mult_commute' would make a ruleset 'non terminating'.
In order to make such a rule set terminating, 'mult_commute' is only applied if the resulting formula is 'smaller' in terms of a 'rewrite order'. To make such an order reliably work on terms (which are recursive datastructures) is not a trivial task.

(c) Richard Lang 2003 (math-author)
(c) isac-team 2006 (course-designer)