Library MboxPendPart2

Require Import include.
Require Import memory.
Require Import memdata.
Require Import NPeano.
Require Import os_code_defs.
Require Import os_code_notations.
Require Import os_ucos_h.
Require Import ucert.
Require Import OSQCreatePure.
Require Import os_code_notations.
Require Import List.
Require Import Mbox_common.
Require Import OSTimeDlyPure.
Require Import gen_lemmas.
Open Scope code_scope.
Ltac can_change_aop_solver := clear; try unfold OSInv;
  try unfold AOSEventFreeList, AOSQFreeList, AOSQFreeBlk, AECBList;
  try unfold AOSMapTbl, AOSUnMapTbl, AOSTCBPrioTbl, AOSIntNesting, AOSTCBList, AOSTCBFreeList;
  try unfold AOSRdyTblGrp, AOSRdyTbl, AOSRdyGrp, AOSTime, AGVars;
  try unfold AOSEvent, AOSEventTbl, AMsgData, AOSQCtr, AOSQBlk, node;
  unfold can_change_aop; fold can_change_aop; intuition auto 1 with can_change_aop;simpl;intros; intuition auto 1 with can_change_aop.

  Hint Resolve CltEnvMod.beq_refl: brel .

Lemma mbox_pend_part0: gen_mbox_pend_part0.