Library MboxCreateProof

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 MboxCreatePure.

Open Scope code_scope.

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