Library MboxPendProof

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 OSTimeDlyPure.
Require Import Mbox_common.

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.

Lemma MboxPendProof:
    forall vl p r,
      Some p =
      BuildPreA´ os_api OSMboxPend
                 mbox_pendapi vl ->
      Some r =
      BuildRetA´ os_api OSMboxPend
                 mbox_pendapi vl ->
      exists t d1 d2 s,
        os_api OSMboxPend = Some (t, d1, d2, s) /\
        {|OSQ_spec , GetHPrio , I, r, Afalse|}|- {{p}}s {{Afalse}}.
  Hint Resolve CltEnvMod.beq_refl.
  Require Import MboxPendPart2.