case halt
S : Finset Λ'
H : contSupp Cont'.halt ⊆ S
⊢ Supports (contSupp Cont'.halt) S

case cons₁
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.cons₁ a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ a✝¹ a✝)) S

case cons₂
S : Finset Λ'
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.cons₂ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ a✝)) S

case comp
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.comp a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.comp a✝¹ a✝)) S

case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
S : Finset Λ'
k : Cont'
H : contSupp k ⊆ S
⊢ Supports (contSupp k) S
induction k
case cons₂
S : Finset Λ'
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.cons₂ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ a✝)) S

case comp
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.comp a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.comp a✝¹ a✝)) S

case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
case cons₁
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.cons₁ a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ a✝¹ a✝)) S

case cons₂
S : Finset Λ'
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.cons₂ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ a✝)) S

case comp
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.comp a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.comp a✝¹ a✝)) S

case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
case cons₁ f k IH =>
  have H₁ := H; rw [contSupp_cons₁] at H₁; have H₂ := Finset.union_subset_right H₁
  refine' trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => _
  refine' supports_union.2 ⟨codeSupp'_supports H₂, _⟩
  simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
  exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
case comp
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.comp a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.comp a✝¹ a✝)) S

case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
case cons₂
S : Finset Λ'
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.cons₂ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ a✝)) S

case comp
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.comp a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.comp a✝¹ a✝)) S

case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
case cons₂ k IH =>
  have H' := H; rw [contSupp_cons₂] at H'
  exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
case comp
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.comp a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.comp a✝¹ a✝)) S

case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
case comp f k IH =>
  have H' := H; rw [contSupp_comp] at H'; have H₂ := Finset.union_subset_right H'
  exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩
no goals
case fix
S : Finset Λ'
a✝¹ : Code
a✝ : Cont'
a_ih✝ : contSupp a✝ ⊆ S → Supports (contSupp a✝) S
H : contSupp (Cont'.fix a✝¹ a✝) ⊆ S
⊢ Supports (contSupp (Cont'.fix a✝¹ a✝)) S
case fix f k IH =>
  rw [contSupp] at H
  exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩
no goals
case halt
S : Finset Λ'
H : contSupp Cont'.halt ⊆ S
⊢ Supports (contSupp Cont'.halt) S
simp [contSupp_halt, Supports]
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H₁ : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
have H₁ := H
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H₁ : contSupp (Cont'.cons₁ f k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
rw [contSupp_cons₁] at H₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
H₂ : codeSupp f (Cont'.cons₂ k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
have H₂ := Finset.union_subset_right H₁
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
H₂ : codeSupp f (Cont'.cons₂ k) ⊆ S
h : codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
H₂ : codeSupp f (Cont'.cons₂ k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₁ f k)) S
refine' trStmts₁_supports' (trNormal_supports H₂) H₁ fun h => _
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
H₂ : codeSupp f (Cont'.cons₂ k) ⊆ S
h : codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
H₂ : codeSupp f (Cont'.cons₂ k) ⊆ S
h : codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k)) S
refine' supports_union.2 ⟨codeSupp'_supports H₂, _⟩
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
h : codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
H₂ : codeSupp' f (Cont'.cons₂ k) ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
H₂ : codeSupp f (Cont'.cons₂ k) ⊆ S
h : codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S
simp only [codeSupp, contSupp_cons₂, Finset.union_subset_iff] at H₂
no goals
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₁ f k) ⊆ S
H₁ :
  trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal f (Cont'.cons₂ k))))) ∪
      codeSupp f (Cont'.cons₂ k) ⊆
    S
h : codeSupp' f (Cont'.cons₂ k) ∪ (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) ⊆ S
H₂ : codeSupp' f (Cont'.cons₂ k) ⊆ S ∧ trStmts₁ (head stack (Λ'.ret k)) ⊆ S ∧ contSupp k ⊆ S
⊢ Supports (trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k) S
exact trStmts₁_supports' (head_supports H₂.2.2) (Finset.union_subset_right h) IH
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.cons₂ k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ k)) S
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₂ k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ k)) S
have H' := H
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₂ k) ⊆ S
H' : trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ k)) S
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.cons₂ k) ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ k)) S
rw [contSupp_cons₂] at H'
no goals
S : Finset Λ'
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.cons₂ k) ⊆ S
H' : trStmts₁ (head stack (Λ'.ret k)) ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.cons₂ k)) S
exact trStmts₁_supports' (head_supports <| Finset.union_subset_right H') H' IH
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
have H' := H
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H H' : contSupp (Cont'.comp f k) ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
rw [contSupp_comp] at H'
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
H₂ : contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
have H₂ := Finset.union_subset_right H'
no goals
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.comp f k) ⊆ S
H' : codeSupp f k ⊆ S
H₂ : contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.comp f k)) S
exact supports_union.2 ⟨codeSupp'_supports H', IH H₂⟩
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : codeSupp' (Code.fix f) k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : contSupp (Cont'.fix f k) ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S
rw [contSupp] at H
no goals
S : Finset Λ'
f : Code
k : Cont'
IH : contSupp k ⊆ S → Supports (contSupp k) S
H : codeSupp' (Code.fix f) k ∪ contSupp k ⊆ S
⊢ Supports (contSupp (Cont'.fix f k)) S
exact supports_union.2 ⟨codeSupp'_supports H, IH (Finset.union_subset_right H)⟩