Qcert.NRA.Optim.NRARewriteContext

Section ROptimContext.




  Context {fruntime:foreign_runtime}.


  Lemma lt_nat_compat (x y:nat) : ¬ x < y → ¬ y < x → x = y.

  Lemma insertion_sort_equivlist_nat l l':
    equivlist l l' → insertion_sort lt_dec l = insertion_sort lt_dec l'.



  Lemma ctxt_and_comm_ctxt :
    $2 ∧ $1 ≡ₐ $1 ∧ $2.

  Lemma ctxt_unnest_singleton_ctxt s1 s2 s3 :
    s1 ≠ s2 ∧ s2 ≠ s3 ∧ s3 ≠ s1 →
    χ⟨¬π[s1 ]( ID)
     ⟩( ⋈ᵈ⟨χ⟨‵[| (s2, ID)|] ⟩( (ID) · s1)
          ⟩( ‵{|‵[| (s3, $1)|] ⊕ ‵[| (s1, ‵{| $2|})|]|}))
     ≡ₐ ‵{|‵[| (s3, $1)|] ⊕ ‵[| (s2, $2)|]|}.

  Lemma ctxt_select_union_distr :
    σ⟨ $0 ⟩($1 ⋃ $2) ≡ₐ σ⟨ $0 ⟩($1) ⋃ σ⟨ $0 ⟩($2).

End ROptimContext.