Library OSSemCreateProof

Require Import sem_common.
Require Import semacc_pure.
Require Import lab.

Open Scope code_scope.

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