Library MboxDelProof

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.
Open Scope code_scope.
Require Import os_code_notations.
Require Import List.
Require Import OSQCreatePure.
Require Import Mbox_common.

Lemma MboxDelProof:
    forall vl p r,
      Some p =
      BuildPreA´ os_api OSMboxDel
                 mbox_delapi vl ->
      Some r =
      BuildRetA´ os_api OSMboxDel
                 mbox_delapi vl ->
      exists t d1 d2 s,
        os_api OSMboxDel = Some (t, d1, d2, s) /\
        {|OSQ_spec , GetHPrio , I, r, Afalse|}|- {{p}}s {{Afalse}}.
  Require Import mathlib.