English
The translation preserves supports: for any S, if ss holds for M on S, then tr M has supports on trStmts M S.
Русский
Перевод сохраняет поддержку: для любого S, если ss выполняется для M на S, то tr M поддерживает trStmts M S.
LaTeX
$$tr_supports (M) (ss) : TM0.Supports (tr M) (trStmts M S)$$
Lean4
theorem tr_supports {S : Finset Λ} (ss : TM1.Supports M S) : TM0.Supports (tr M) ↑(trStmts M S) := by
classical
constructor
· apply Finset.mem_product.2
constructor
· simp only [default, TM1.stmts, Finset.mem_insertNone, Option.mem_def, Option.some_inj, forall_eq',
Finset.mem_biUnion]
exact ⟨_, ss.1, TM1.stmts₁_self⟩
· apply Finset.mem_univ
· intro q a q' s h₁ h₂
rcases q with ⟨_ | q, v⟩; · cases h₁
obtain ⟨q', v'⟩ := q'
simp only [trStmts, Finset.mem_coe] at h₂ ⊢
rw [Finset.mem_product] at h₂ ⊢
simp only [Finset.mem_univ, and_true] at h₂ ⊢
cases q'; · exact Multiset.mem_cons_self _ _
simp only [tr, Option.mem_def] at h₁
have := TM1.stmts_supportsStmt ss h₂
revert this;
induction q generalizing v with intro hs
| move d q =>
cases h₁; refine TM1.stmts_trans ?_ h₂
unfold TM1.stmts₁
exact Finset.mem_insert_of_mem TM1.stmts₁_self
| write b q =>
cases h₁; refine TM1.stmts_trans ?_ h₂
unfold TM1.stmts₁
exact Finset.mem_insert_of_mem TM1.stmts₁_self
| load b q IH =>
refine IH _ (TM1.stmts_trans ?_ h₂) h₁ hs
unfold TM1.stmts₁
exact Finset.mem_insert_of_mem TM1.stmts₁_self
| branch p q₁ q₂ IH₁ IH₂ =>
cases h : p a v <;> rw [trAux, h] at h₁
· refine IH₂ _ (TM1.stmts_trans ?_ h₂) h₁ hs.2
unfold TM1.stmts₁
exact Finset.mem_insert_of_mem (Finset.mem_union_right _ TM1.stmts₁_self)
· refine IH₁ _ (TM1.stmts_trans ?_ h₂) h₁ hs.1
unfold TM1.stmts₁
exact Finset.mem_insert_of_mem (Finset.mem_union_left _ TM1.stmts₁_self)
| goto l =>
cases h₁
exact Finset.some_mem_insertNone.2 (Finset.mem_biUnion.2 ⟨_, hs _ _, TM1.stmts₁_self⟩)
| halt => cases h₁
