  Axiomatization and expressibility problems for Milner's process semantics
(1984) of regular expressions modulo bisimilarity have turned out to be
difficult for the full class of expressions with deadlock 0 and empty step~1.
We report on a phenomenon that arises from the added presence of 1 when 0 is
available, and that brings a crucial reason for this difficulty into focus. To
wit, while interpretations of 1-free regular expressions are closed under
bisimulation collapse, this is not the case for the interpretations of
arbitrary regular expressions.
  Process graph interpretations of 1-free regular expressions satisfy the loop
existence and elimination property LEE, which is preserved under bisimulation
collapse. These features of LEE were applied for showing that an equational
proof system for 1-free regular expressions modulo bisimilarity is complete,
and that it is decidable in polynomial time whether a process graph is
bisimilar to the interpretation of a 1-free regular expression.
  While interpretations of regular expressions do not satisfy the property LEE
in general, we show that LEE can be recovered by refined interpretations as
graphs with 1-transitions refined interpretations with 1-transitions (which are
similar to silent steps for automata). This suggests that LEE can be expedient
also for the general axiomatization and expressibility problems. But a new
phenomenon emerges that needs to be addressed: the property of a process graph
`to can be refined into a process graph with 1-transitions and with LEE' is not
preserved under bisimulation collapse. We provide a 10-vertex graph with two
1-transitions that satisfies LEE, and in which a pair of bisimilar vertices
cannot be collapsed on to each other while preserving the refinement property.
This implies that the image of the process interpretation of regular
expressions is not closed under bisimulation collapse.
