English
If q' belongs to trStmts₁(q), then trStmts₁(q') is a subset of trStmts₁(q).
Русский
Если q' принадлежит trStmts₁( q ), тогда trStmts₁(q') ⊆ trStmts₁(q).
LaTeX
$$$\\forall q, q'.\\; q' \\in \\operatorname{trStmts}_1(q) \\rightarrow \\operatorname{trStmts}_1(q') \\subseteq \\operatorname{trStmts}_1(q)$$$
Lean4
theorem trStmts₁_trans {q q'} : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q :=
by
induction q with
| move _ _ _ q q_ih => _
| clear _ _ q q_ih => _
| copy q q_ih => _
| push _ _ q q_ih => _
| read q q_ih => _
| succ q q_ih => _
| pred q₁ q₂ q₁_ih q₂_ih => _
| ret => _ <;>
all_goals
simp +contextual only [trStmts₁, Finset.mem_insert, Finset.mem_union, or_imp, Finset.mem_singleton,
Finset.Subset.refl, imp_true_iff, true_and]
repeat exact fun h => Finset.Subset.trans (q_ih h) (Finset.subset_insert _ _)
· simp
intro s h x h'
simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, Finset.mem_insert]
exact Or.inr ⟨_, q_ih s h h'⟩
· constructor
· rintro rfl
apply Finset.subset_insert
· intro h x h'
simp only [Finset.mem_insert]
exact Or.inr (Or.inr <| q_ih h h')
· refine ⟨fun h x h' => ?_, fun _ x h' => ?_, fun h x h' => ?_⟩ <;> simp
· exact Or.inr (Or.inr <| Or.inl <| q₁_ih h h')
· rcases Finset.mem_insert.1 h' with h' | h' <;> simp [h', unrev]
· exact Or.inr (Or.inr <| Or.inr <| q₂_ih h h')
