Library OSMutexPostPart3_3_5a

Require Import ucert.

Require Import os_code_defs.

Require Import mathlib.

Require Import OSMutex_common.
Require Import lab.

Require Import OSMutexPostPure.
Require Import OSQPostPure.
Require Import OSQPendPure.
Require Import OSMutexPostPart3_3_0.
Require Import gen_lemmas.
Open Scope code_scope.

Lemma OSMutexPost3_3_event_rdy_post5´ :gen_OSMutexPost3_3_event_rdy_post5´.