Qcert.Translation.TCAMPtocNRAEnv

Section TCAMPtocNRAEnv.

  Context {m:basic_model}.

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

Some corollaries of the main Lemma

  Lemma cnraenv_of_pat_cnraenv_of_pat_top p τc τin τout :
    cnraenv_of_pat p ▷ τin >=> Coll τ out ⊣ τ c ;(Rec Closed nil eq_refl ) →
    cnraenv_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 →
    cnraenv_of_pat_top p ▷ τin >=> Coll τ out ⊣ τ c ;(Rec Closed nil eq_refl ).

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

End TCAMPtocNRAEnv.