Qcert.NNRC.Core.cNNRCNorm

Section cNNRCProp.

Named Nested Relational Calculus

  Context {fruntime:foreign_runtime}.
  Context (h:brand_relation_t).

  Lemma nnrc_core_eval_normalized env e {o} :
    nnrc_core_eval h env e = Some o →
    Forall (data_normalized h) (map snd env) →
    data_normalized h o.

End cNNRCProp.