Library OSMutexPostPart3_3

Require Import ucert.

Require Import os_code_defs.

Require Import mathlib.

Require Import OSMutex_common.
Require Import lab.

Require Import OSMutexPostPart3_3_1.
Require Import OSMutexPostPart3_3_1a.
Require Import OSMutexPostPart3_3_3.
Require Import OSMutexPostPart3_3_3a.
Require Import OSMutexPostPart3_3_5.
Require Import OSMutexPostPart3_3_5a.
Require Import OSMutexPostPure.
Require Import gen_lemmas.
Open Scope code_scope.



Theorem MutexPostNoUnliftSuccReturn : gen_MutexPostNoUnliftSuccReturn.
  Ltac unfold_event := unfold AEventNode; unfold AOSEvent; unfold AEventData; unfold AOSEventTbl.
  Ltac unfold_tcb := unfold AOSTCBList; unfold tcbdllseg; unfold V_OSTCBPrev; unfold V_OSTCBNext; unfold dllseg; fold dllseg.