Require Import sem_common.
Require Import sempend_pure.
Require Import os_mutex.
Require Import OSMutex_common.
Require Import OSQPostPure.
Require Import gen_lemmas.
Open Scope code_scope.

Lemma mutex_pend_ptcb_is_cur_err: gen_mutex_pend_ptcb_is_cur_err.

Lemma mutex_pend_ptcb_is_idle_err_left_to_cur: gen_mutex_pend_ptcb_is_idle_err_left_to_cur.

Lemma mutex_pend_ptcb_is_not_rdy_left_to_cur: gen_mutex_pend_ptcb_is_not_rdy_left_to_cur.

Lemma mutex_pend_cur_prio_eql_mprio_left_to_cur:gen_mutex_pend_cur_prio_eql_mprio_left_to_cur.

Lemma mutex_pend_pip_is_not_hold_left_to_cur:gen_mutex_pend_pip_is_not_hold_left_to_cur.

Lemma mutex_pend_ptcb_is_idle_err_right_to_cur: gen_mutex_pend_ptcb_is_idle_err_right_to_cur.

Lemma mutex_pend_ptcb_is_not_rdy_right_to_cur: gen_mutex_pend_ptcb_is_not_rdy_right_to_cur.

Lemma mutex_pend_cur_prio_eql_mprio_right_to_cur:gen_mutex_pend_cur_prio_eql_mprio_right_to_cur.

Lemma mutex_pend_pip_is_not_hold_right_to_cur:gen_mutex_pend_pip_is_not_hold_right_to_cur.