Library MboxPostProof

Require Import include.
Require Import memory.
Require Import memdata.
Require Import NPeano.
Require Import os_code_defs.
Require Import os_code_notations.
Require Import os_ucos_h.
Require Import ucert.
Require Import OSQCreatePure.
Require Import os_code_notations.
Require Import List.
Require Import Mbox_common.
Require Import OSQPostPure.
Require Import gen_lemmas.
Open Scope code_scope.

Lemma mbox_post_part1: gen_mbox_post_part1.

Lemma mbox_post_part2: gen_mbox_post_part2.
  Require Import OSQPostPure.

Lemma mbox_post_part3: gen_mbox_post_part3.

Lemma mbox_post_part4 :gen_mbox_post_part4.

Lemma mbox_post_part5: gen_mbox_post_part5.

Lemma mbox_post_part6: gen_mbox_post_part6.

Lemma mbox_post_part0 : gen_mbox_post_part0.
Lemma MboxPostProof:
    forall vl p r,
      Some p =
      BuildPreA´ os_api OSMboxPost
                 mbox_postapi vl ->
      Some r =
      BuildRetA´ os_api OSMboxPost
                 mbox_postapi vl ->
      exists t d1 d2 s,
        os_api OSMboxPost = Some (t, d1, d2, s) /\
        {|OSQ_spec , GetHPrio , I, r, Afalse|}|- {{p}}s {{Afalse}}.