Figure 10 includes a simplification rule for associating to the right:
(p;q);r --> p;(q;r).
However, in order to justifiy the simplification algorithm that the
implementation uses we need to know that it is possible to reassociate
proofs both ways, so the figure should read:
(p;q);r --> p;(q;r)
p;(q;r) --> (p;q);r.
Aaron Stump points out that one alternative is to include three
different simplification rules which combine transitivity and
cancelation of inverses:
(p;q);r --> p;(q;r)
p;(p^-1;r) --> r
p^-1;(p;r) --> r
This way, the rules form a convergent rewrite system, so they can be applied in any order. For details of this suggestion, see
Aaron Stump and Li-Yang Tan, "The Algebra of Equality Proofs", in
Proceedings of the 16th International Conference on Term Rewriting
and Applications (RTA 2005), LNCS volume 3467, 2005.