Qcert.Translation.TCAMPtoNRAEnv

Section TCAMPtoNRAEnv.

  Context {m:basic_model}.

  Lemma nraenv_of_pat_type_preserve τc Γ pf p τin τout :
    [τ c &Γ ] |= p ; τin ~> τ out →
    nraenv_of_pat p ▷ₓ τin >=> Coll τ out ⊣ τ c ;(Rec Closed Γ pf ).

Some corollaries of the main Lemma

  Lemma nraenv_of_pat_nraenv_of_pat_top p τc τin τout :
    nraenv_of_pat p ▷ₓ τin >=> Coll τ out ⊣ τ c ;(Rec Closed nil eq_refl ) →
    nraenv_of_pat_top p ▷ₓ τin >=> Coll τ out ⊣ τ c ;(Rec Closed nil eq_refl ).

  Theorem alg_of_pat_top_type_preserve p τc τin τout :
    [τ c &nil ] |= p ; τin ~> τ out →
    nraenv_of_pat_top p ▷ₓ τin >=> Coll τ out ⊣ τ c ;(Rec Closed nil eq_refl ).

  Theorem nraenv_of_rule_type_preserve τworld τout r :
    @rule_type m τ world τ out r →
    nraenv_of_rule r ▷ₓ Unit >=> Coll τ out ⊣ (mkTWorld τ world );(Rec Closed nil eq_refl ).

End TCAMPtoNRAEnv.