English
For any code c and continuation k, if codeSupp c k ⊆ S, then the trace tr of code c with k is TM2-supported by S.
Русский
Для любого кода c и продолжения k, если codeSupp c k ⊆ S, то трейс tr кода c с k поддерживается S TM2.
LaTeX
$$$\\forall c,k,\\; (\\mathrm{codeSupp}(c,k) \\subseteq S) \\Rightarrow \\mathrm{TM2.Supports}(S, \\mathrm{tr}(c,k)).$$$
Lean4
theorem codeSupp'_supports {S c k} (H : codeSupp c k ⊆ S) : Supports (codeSupp' c k) S := by
induction c generalizing k with
| cons f fs IHf IHfs =>
have H' := H; simp only [codeSupp_cons, Finset.union_subset_iff] at H'
refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
refine supports_union.2 ⟨IHf H'.2, ?_⟩
refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun h => ?_
· simp only [codeSupp, Finset.union_subset_iff, contSupp] at h H ⊢
exact ⟨h.2.2.1, h.2.2.2, H.2⟩
refine supports_union.2 ⟨IHfs ?_, ?_⟩
· rw [codeSupp, contSupp_cons₁] at H'
exact Finset.union_subset_right (Finset.union_subset_right H'.2)
exact trStmts₁_supports (head_supports <| Finset.union_subset_right H) (Finset.union_subset_right h)
| comp f g IHf IHg =>
have H' := H; rw [codeSupp_comp] at H'; have H' := Finset.union_subset_right H'
refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
refine supports_union.2 ⟨IHg H', ?_⟩
refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
· simp only [codeSupp', codeSupp, Finset.union_subset_iff] at h H ⊢
exact ⟨h.2.2, H.2⟩
exact IHf (Finset.union_subset_right H')
| case f g IHf IHg =>
have H' := H; simp only [codeSupp_case, Finset.union_subset_iff] at H'
refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_
exact supports_union.2 ⟨IHf H'.2.1, IHg H'.2.2⟩
| fix f IHf =>
have H' := H; simp only [codeSupp_fix, Finset.union_subset_iff] at H'
refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun h => ?_
refine supports_union.2 ⟨IHf H'.2, ?_⟩
refine trStmts₁_supports' (trNormal_supports ?_) (Finset.union_subset_right h) fun _ => ?_
· simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp, trStmts₁, Finset.insert_subset_iff] at h H ⊢
exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩
exact supports_singleton.2 (ret_supports <| Finset.union_subset_right H)
| _ => exact trStmts₁_supports (trNormal_supports H) (Finset.Subset.trans (codeSupp_self _ _) H)
