Library OSEventSearchProof

Require Import ucert.
Require Import common.
Require Import mathlib.
Require Import OSESearchPure.

Open Scope code_scope.

Lemma OSEventSearch_proof:
  forall vl p r logicl,
    Some p =
    BuildPreI os_internal OS_EventSearch
              vl logicl OS_EventSearchPre ->
    Some r =
    BuildRetI os_internal OS_EventSearch vl logicl OS_EventSearchPost ->
    exists t d1 d2 s,
      os_internal OS_EventSearch = Some (t, d1, d2, s) /\
      {| OSQ_spec, GetHPrio, I, r, Afalse |} |- {{p}} s {{Afalse}}.
  Ltac solve_Afalse_in_pre :=
    eapply backward_rule1 with (p:=Afalse);
    [intros s_1 H_1; destruct_s s_1; simpl in H_1; mytac; tryfalse |
     apply pfalse_rule].