Qcert.NRAEnv.Optim.NRAEnvRewriteContext

Section ROptimEnvContext.




  Context {fruntime:foreign_runtime}.




  Lemma envctxt_and_comm_ctxt :
    $2 ∧ $1 ≡ₑ $1 ∧ $2.

  Lemma ctxt_envunion_assoc :
    ($1 ⋃ $2) ⋃ $3 ≡ₑ $1 ⋃ ($2 ⋃ $3).

  Lemma ctxt_app_over_merge :
    (ENV ⊗ $1) ◯ $2 ≡ₑ ENV ⊗ ($1 ◯ $2).

  Lemma envctxt_select_union_distr :
    σ⟨ $0 ⟩($1 ⋃ $2) ≡ₑ σ⟨ $0 ⟩($1) ⋃ σ⟨ $0 ⟩($2).

End ROptimEnvContext.