Library OSSemDeleteProof

Require Import sem_common.
Require Import semdel_pure.

Open Scope code_scope.

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