Library OSTimeDlyProof

Require Import ucert.
Require Import OSTimeDlyPure.

Open Scope code_scope.

Lemma OSTimeDlyProof :
  forall vl p r,
    Some p = BuildPreA´ os_api OSTimeDly dlyapi vl ->
    Some r = BuildRetA´ os_api OSTimeDly dlyapi vl ->
    exists t d1 d2 s,
      os_api OSTimeDly = Some (t, d1, d2, s) /\
      {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{ p }} s {{ Afalse }}.