Library OSQDelProof

Require Import ucert.
Require Import OSQDelPure.

Open Scope code_scope.

Lemma OSQDelProof:
  forall vl p r,
    Some p =
    BuildPreA´ os_api OSQDel
               (qdel, (Tint8, Tptr os_ucos_h.OS_EVENT :: nil)) vl ->
    Some r =
    BuildRetA´ os_api OSQDel
               (qdel, (Tint8, Tptr os_ucos_h.OS_EVENT :: nil)) vl ->
    exists t d1 d2 s,
      os_api OSQDel = Some (t, d1, d2, s) /\
      {|OSQ_spec , GetHPrio, I, r, Afalse|}|- {{p}}s {{Afalse}}.

Close Scope code_scope.