Library OSMutexPendPart2

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 OSMutexPendPure1.
Require Import OSMutex_common.
Require Import OSMutexPendPart4.
Require Import gen_lemmas.
Open Scope code_scope.

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

Lemma mutex_pend_can_not_lift_right_to_cur:gen_mutex_pend_can_not_lift_right_to_cur.