pub broadcast group fn disjointness_lemmas()Expand description
Canonical automation for right-associated formats.
Every recursive rule reduces a constructor visible in the trigger. This includes the
right-oriented OptionalEnd and RepeatTillEnd rules: although they expose productivity and
safety side conditions, they still strictly peel the triggered continuation. Reverse-oriented
rules remain opt-in so that automation cannot oscillate between equivalent orientations.