Library OSEventTaskWait

Require Import ucert.
Require Import OSETWaitPure.
Open Scope code_scope.

Lemma OSEventTaskWait_proof:
    forall vl p r ll,
      Some p =
      BuildPreI os_internal OS_EventTaskWait
                  vl ll OS_EventTaskWaitPre ->
      Some r =
      BuildRetI os_internal OS_EventTaskWait vl ll OS_EventTaskWaitPost ->
      exists t d1 d2 s,
        os_internal OS_EventTaskWait = Some (t, d1, d2, s) /\
        {|OSQ_spec , GetHPrio, I, r, Afalse|}|- {{p}} s {{Afalse}}.