proposition: Lemma inc_dec_in_first_out : forall (q : queue Message) (m : Message) (s3 : Site), first Message q = value Message m -> m <> inc_dec s3 -> inc_dec_in_queue s3 q -> inc_dec_in_queue s3 (first_out Message q).
proof: Proof. simple induction q. simpl in |- *. auto. intros d q0. case q0. intro. intros m s3. simpl in |- *. case d. auto. intro. case (eq_site_dec s s3). intros. elim H1. generalize H0. auto. rewrite e. auto. generalize (inc_dec s3). intro. auto. intro. symmetry in |- *. injection H3. auto. auto. intros. contradiction. intros m q1 H m0 s3 H0 H1. case d. generalize (H m0 s3). simpl in |- *. auto. intro. case (eq_site_dec s3 s). intro. rewrite e. simpl in |- *. case (eq_site_dec s s). auto. intro. elim n; auto. intro. simpl in |- *. case (eq_site_dec s s3). auto. intro. generalize (H m0 s3). simpl in |- *. auto. generalize (H m0 s3). simpl in |- *. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4