Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
⊢ q₀ ∈ stmts₁ q₂
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
⊢ q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂
intro h₁₂ q₀ h₀₁
case move
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Dir
q : Stmt₁
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = move a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (move a✝ q) (stmts₁ q)

case write
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Γ
q : Stmt₁
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = write a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (write a✝ q) (stmts₁ q)

case load
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt₁
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = load a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

case branch
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝² : Γ → σ → Bool
a✝¹ a✝ : Stmt₁
a_ih✝¹ : q₁ ∈ stmts₁ a✝¹ → q₀ ∈ stmts₁ a✝¹
a_ih✝ : q₁ ∈ stmts₁ a✝ → q₀ ∈ stmts₁ a✝
h₁₂ : q₁ = branch a✝² a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝¹ ∨ q₁ ∈ stmts₁ a✝
⊢ q₀ ∈ insert (branch a✝² a✝¹ a✝) (stmts₁ a✝¹ ∪ stmts₁ a✝)

case goto
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Λ
h₁₂ : q₁ = goto a✝
⊢ q₀ ∈ {goto a✝}

case halt
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
⊢ q₀ ∈ stmts₁ q₂
induction' q₂ with _ q IH _ q IH _ q IH <;> simp only [stmts₁] at h₁₂⊢ <;>
  simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂
case halt
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
case goto
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Λ
h₁₂ : q₁ = goto a✝
⊢ q₀ ∈ {goto a✝}

case halt
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
case goto l => subst h₁₂; exact h₀₁
no goals
case halt
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
case halt => subst h₁₂; exact h₀₁
case load.inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
a✝ : Γ → σ → σ
q : Stmt₁
h₁₂ : load a✝ q ∈ stmts₁ q₂
h₀₁ : q₀ ∈ stmts₁ (load a✝ q)
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

case load.inr
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt₁
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

case branch
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝² : Γ → σ → Bool
a✝¹ a✝ : Stmt₁
a_ih✝¹ : q₁ ∈ stmts₁ a✝¹ → q₀ ∈ stmts₁ a✝¹
a_ih✝ : q₁ ∈ stmts₁ a✝ → q₀ ∈ stmts₁ a✝
h₁₂ : q₁ = branch a✝² a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝¹ ∨ q₁ ∈ stmts₁ a✝
⊢ q₀ ∈ insert (branch a✝² a✝¹ a✝) (stmts₁ a✝¹ ∪ stmts₁ a✝)

case goto
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Λ
h₁₂ : q₁ = goto a✝
⊢ q₀ ∈ {goto a✝}

case halt
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
case load
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt₁
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = load a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)

case branch
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝² : Γ → σ → Bool
a✝¹ a✝ : Stmt₁
a_ih✝¹ : q₁ ∈ stmts₁ a✝¹ → q₀ ∈ stmts₁ a✝¹
a_ih✝ : q₁ ∈ stmts₁ a✝ → q₀ ∈ stmts₁ a✝
h₁₂ : q₁ = branch a✝² a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝¹ ∨ q₁ ∈ stmts₁ a✝
⊢ q₀ ∈ insert (branch a✝² a✝¹ a✝) (stmts₁ a✝¹ ∪ stmts₁ a✝)

case goto
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → Λ
h₁₂ : q₁ = goto a✝
⊢ q₀ ∈ {goto a✝}

case halt
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
rcases h₁₂ with (rfl | h₁₂)
case load.inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
a✝ : Γ → σ → σ
q : Stmt₁
h₁₂ : load a✝ q ∈ stmts₁ q₂
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₀₁ : q₀ ∈ insert (load a✝ q) (stmts₁ q)
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
case load.inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
a✝ : Γ → σ → σ
q : Stmt₁
h₁₂ : load a✝ q ∈ stmts₁ q₂
h₀₁ : q₀ ∈ stmts₁ (load a✝ q)
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
unfold stmts₁ at h₀₁
no goals
case load.inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
a✝ : Γ → σ → σ
q : Stmt₁
h₁₂ : load a✝ q ∈ stmts₁ q₂
IH : load a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₀₁ : q₀ ∈ insert (load a✝ q) (stmts₁ q)
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
exact h₀₁
no goals
case load.inr
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
a✝ : Γ → σ → σ
q : Stmt₁
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (load a✝ q) (stmts₁ q)
exact Finset.mem_insert_of_mem (IH h₁₂)
case inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂✝ q₀ : Stmt₁
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂✝
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case inr.inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁✝ q₂✝ : Stmt₁
h₁₂✝ : q₁✝ ∈ stmts₁ q₂✝
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case inr.inr
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁✝ q₂✝ : Stmt₁
h₁₂✝ : q₁✝ ∈ stmts₁ q₂✝
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁✝ q₂✝ : Stmt₁
h₁₂✝ : q₁✝ ∈ stmts₁ q₂✝
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ = branch p q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
rcases h₁₂ with (rfl | h₁₂ | h₁₂)
case inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂✝ q₀ : Stmt₁
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂✝
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₀₁ : q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
case inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂✝ q₀ : Stmt₁
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂✝
h₀₁ : q₀ ∈ stmts₁ (branch p q₁ q₂)
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
unfold stmts₁ at h₀₁
no goals
case inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂✝ q₀ : Stmt₁
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
h₁₂ : branch p q₁ q₂ ∈ stmts₁ q₂✝
IH₁ : branch p q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch p q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₀₁ : q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
exact h₀₁
no goals
case inr.inl
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁✝ q₂✝ : Stmt₁
h₁₂✝ : q₁✝ ∈ stmts₁ q₂✝
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
exact Finset.mem_insert_of_mem (Finset.mem_union_left _ <| IH₁ h₁₂)
no goals
case inr.inr
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁✝ q₂✝ : Stmt₁
h₁₂✝ : q₁✝ ∈ stmts₁ q₂✝
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁✝
p : Γ → σ → Bool
q₁ q₂ : Stmt₁
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch p q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
exact Finset.mem_insert_of_mem (Finset.mem_union_right _ <| IH₂ h₁₂)
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
l : Γ → σ → Λ
h₁₂ : goto l ∈ stmts₁ q₂
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
l : Γ → σ → Λ
h₁₂ : q₁ = goto l
⊢ q₀ ∈ {goto l}
subst h₁₂
no goals
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
l : Γ → σ → Λ
h₁₂ : goto l ∈ stmts₁ q₂
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}
exact h₀₁
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
h₁₂ : halt ∈ stmts₁ q₂
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₁ q₂ : Stmt₁
h₁₂✝ : q₁ ∈ stmts₁ q₂
q₀ : Stmt₁
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}
subst h₁₂
no goals
Γ : Type u_1
inst✝ : Inhabited Γ
Λ : Type u_2
σ : Type u_3
q₂ q₀ : Stmt₁
h₁₂ : halt ∈ stmts₁ q₂
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}
exact h₀₁