Reachability #
Any configuration is reachable from a subconfiguration by firing the events of the gap one at a time. This is because configurations are secured.
theorem
path_exists
{L : Type u_1}
(F : ConfFamily L)
{c₀ c : F.Conf}
(hsub : ↑c₀ ⊆ ↑c)
(hfin : (↑c \ ↑c₀).Finite)
:
A configuration is reachable from any subconfiguration with a finite gap.
theorem
execList_exists
{L : Type u_1}
(F : ConfFamily L)
{c₀ c : F.Conf}
(hsub : ↑c₀ ⊆ ↑c)
(hfin : (↑c \ ↑c₀).Finite)
:
Nonempty ((t : List F.Event) × Path.ExecList F c₀ t c)
The same, as an execution list.