English
If S is disjoint from the states reachable by reading x in the reverse automaton from S', then S' is disjoint from the states reachable by reading reverse(x) in the original automaton from S.
Русский
Если S не пересекается с множеством состояний, достигаемых чтением x в обратном автомате из S', тогда S' не пересекается с состояниями, достигаемыми чтением reverse(x) в исходном автомате из S.
LaTeX
$$Disjoint S (M.reverse.evalFrom S' x) ⇒ Disjoint S' (M.evalFrom S x.reverse)$$
Lean4
theorem disjoint_evalFrom_reverse {x : List α} {S S' : Set σ} (h : Disjoint S (M.reverse.evalFrom S' x)) :
Disjoint S' (M.evalFrom S x.reverse) :=
by
simp only [evalFrom, List.foldl_reverse] at h ⊢
induction x generalizing S S' with
| nil =>
rw [disjoint_comm]
exact h
| cons x xs ih =>
rw [List.foldl_cons] at h
rw [List.foldr_cons, ← NFA.disjoint_stepSet_reverse, disjoint_comm]
exact ih h
