Theorem: run_OpM_toTopM_denoteRegion (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
env : SSAEnv Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (OpM.toTopM rs (OpM.denoteRegion r ix args)) env = run (TopM.denoteRegionsByIx rs ix args) env
Tactic:
simp[OpM.denoteRegion]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
env : SSAEnv Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (OpM.toTopM rs (OpM.RunRegion ix args fun retvals => OpM.Ret retvals)) env =
    run (TopM.denoteRegionsByIx rs ix args) env

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
ix : ℕ
Δ : Dialect α σ ε
args : TypedArgs Δ
r : Region Δ
env : SSAEnv Δ
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ run (OpM.toTopM rs (OpM.RunRegion ix args fun retvals => OpM.Ret retvals)) env =
    run (TopM.denoteRegionsByIx rs ix args) env
Tactic:
simp[OpM.toTopM]
State after:
no goals