English
If q is S-supported and trStmts₁ q ⊆ S, then trStmts₁ q is S-supported.
Русский
Если q поддерживается S и весь набор trStmts₁ q ⊆ S, то trStmts₁ q поддерживается S.
LaTeX
$$$\\text{If } q : \\Lambda' \\text{ is S-supported and } trStmts₁ q \\subseteq S, \\text{ then } \\mathrm{Supports}(trStmts₁ q, S).$$$
Lean4
theorem trStmts₁_supports {S q} (H₁ : (q : Λ').Supports S) (HS₁ : trStmts₁ q ⊆ S) : Supports (trStmts₁ q) S :=
by
have W := fun {q} => trStmts₁_self q
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 => _ <;>
simp [trStmts₁, -Finset.singleton_subset_iff] at HS₁ ⊢
any_goals
obtain ⟨h₁, h₂⟩ := Finset.insert_subset_iff.1 HS₁
first
| have h₃ := h₂ W
| try simp [Finset.subset_iff] at h₂
·
exact
supports_insert.2
⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩ -- move
·
exact
supports_insert.2
⟨⟨fun _ => h₃, fun _ => h₁⟩, q_ih H₁ h₂⟩ -- clear
·
exact
supports_insert.2
⟨⟨fun _ => h₁, fun _ => h₃⟩, q_ih H₁ h₂⟩ -- copy
·
exact
supports_insert.2
⟨⟨fun _ => h₃, fun _ => h₃⟩, q_ih H₁ h₂⟩ -- push
· refine
supports_insert.2
⟨fun _ => h₂ _ W, ?_⟩ -- read
exact supports_biUnion.2 fun _ => q_ih _ (H₁ _) fun _ h => h₂ _ h
· refine
supports_insert.2
⟨⟨fun _ => h₁, fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩ -- succ
exact supports_insert.2 ⟨⟨fun _ => h₂.2 _ W, fun _ => h₂.1⟩, q_ih H₁ h₂.2⟩
· refine -- pred
supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.2 _ (Or.inl W), fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩
refine supports_insert.2 ⟨⟨fun _ => h₂.2 _ (Or.inr W), fun _ => h₂.1⟩, ?_⟩
refine supports_union.2 ⟨?_, ?_⟩
· exact q₁_ih H₁.1 fun _ h => h₂.2 _ (Or.inl h)
· exact q₂_ih H₁.2 fun _ h => h₂.2 _ (Or.inr h)
·
exact
supports_singleton.2
(ret_supports H₁) -- ret
