English
If contSupp(k) ⊆ S, then the trace of Λ'.ret k is TM2-supported with respect to S.
Русский
Если contSupp(k) ⊆ S, то трейс вычисления ret k поддерживается TM2 относительно S.
LaTeX
$$$\\text{If } \\operatorname{contSupp}(k) \\subseteq S, \\ \\mathrm{TM2.SupportsStmt}(S, \\mathrm{tr}(\\Lambda'.\\mathrm{ret}(k))).$$$
Lean4
theorem ret_supports {S k} (H₁ : contSupp k ⊆ S) : TM2.SupportsStmt S (tr (Λ'.ret k)) :=
by
have W := fun {q} => trStmts₁_self q
cases k with
| halt => trivial
| cons₁ => rw [contSupp_cons₁, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
| cons₂ => rw [contSupp_cons₂, Finset.union_subset_iff] at H₁; exact fun _ => H₁.1 W
| comp => rw [contSupp_comp] at H₁; exact fun _ => H₁ (codeSupp_self _ _ W)
| fix =>
rw [contSupp_fix] at H₁
have L := @Finset.mem_union_left; have R := @Finset.mem_union_right
intro s; dsimp only; cases natEnd s.iget
· refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)
· exact H₁ (R _ <| L _ <| R _ <| R _ <| R _ <| Finset.mem_singleton_self _)
