Library OSMutexPendPart3

Require Import sem_common.
Require Import sempend_pure.
Require Import os_mutex.
Require Import OSEventTaskRdyPure.
Require Import OSQPendPure.
Require Import OSQPostPure.
Require Import mathlib.
Require Import OSMutex_common.
Require Import OSMutexPendPure1.
Require Import gen_lemmas.
Open Scope code_scope.

Lemma mutex_pend_ptcb_is_rdy_left_to_cur´: gen_mutex_pend_ptcb_is_rdy_left_to_cur´.
  Ltac simpl_vqm :=
    repeat
    match goal with
      | H: _ = Some _ |- _ => simpl in H;inverts H
      | _ => idtac
    end.

Close Scope code_scope.