If an umambiguous concatenation is disjoint from an unambiguous alternation, then adding the concatenation maintains the alternation unambiguous.
This theorem can be used to show that an alternation is unambiguous,
one constituting concatenation at a time,
starting with
Theorem:
(defthm alternation-unambiguousp-of-cons-when-disjointp (implies (and (concatenation-unambiguousp concatenation rules) (alternation-unambiguousp alternation rules) (concatenation-alternation-disjointp concatenation alternation rules)) (alternation-unambiguousp (cons concatenation alternation) rules)))