Library OSESearchPure

Require Export mathlib.
Lemma evsllseg_append : forall v´19 v´16 v0 v´21 v1 v´2 v´26 x3 i0 i i1 x2 H5 d,
  H5 |= evsllseg v´16 (Vptr (v´26, Int.zero)) v´19 v´21 **
        Astruct (v´26, Int.zero) OS_EVENT (Vint32 i0 :: Vint32 i :: Vint32 i1 :: v1 :: x3 :: x2 :: nil) ** AOSEventTbl v´2 v0 ** AEventData (Vint32 i0 :: Vint32 i :: Vint32 i1 :: v1 :: x3 :: x2 :: nil) d ->
  RL_Tbl_Grp_P v0 (Vint32 i) ->
  id_addrval´ (Vptr (v´26, Int.zero)) OSEventTbl OS_EVENT = Some v´2 ->
  Int.unsigned i <= 255 -> Int.unsigned i1 <= 65535 ->
  isptr v1 ->
  isptr x2 ->
  struct_type_vallist_match OS_EVENT (Vint32 i0 :: Vint32 i :: Vint32 i1 :: v1 :: x3 :: x2 :: nil) ->
  H5 |= evsllseg v´16 x2 (v´19 ++
           (Vint32 i0 :: Vint32 i :: Vint32 i1 :: v1 :: x3 :: x2 :: nil,
            v0) :: nil) (v´21 ++ d :: nil).


Lemma ECBList_P_nil : forall l1 l2 m1 m2,
  ECBList_P Vnull Vnull l1 l2 m1 m2 -> l1 = nil /\ l2 = nil /\ m1 = EcbMod.emp.

Lemma ECBList_P_append : forall v´13 v´16 v´19 v0 v´21 v1 v´23 v´24 v´26 x3 i i1 x0 x1 x2 s H5 i0 d,
  ECBList_P v´16 (Vptr (v´26, Int.zero)) v´19 v´21 v´23 v´13 ->
  RLH_ECBData_P d x0 ->
  s |= Astruct (v´26, Int.zero) OS_EVENT
        (Vint32 i0 :: Vint32 i :: Vint32 i1 :: v1 :: x3 :: x2 :: nil) **
        evsllseg v´16 (Vptr (v´26, Int.zero)) v´19 v´21 ** H5 ->
  EcbMod.join (EcbMod.sig (v´26, Int.zero) x0) x1 v´24 ->
  R_ECB_ETbl_P (v´26, Int.zero)
               (Vint32 i0 :: Vint32 i :: Vint32 i1 :: v1 :: x3 :: x2 :: nil, v0) v´13 ->
  ECBList_P v´16 x2
     (v´19 ++ (Vint32 i0 :: Vint32 i :: Vint32 i1 :: v1 :: x3 :: x2 :: nil, v0) :: nil) (v´21 ++ d :: nil)
     (EcbMod.merge v´23 (EcbMod.sig (v´26, Int.zero) x0)) v´13.