proposition: Lemma inc_dec_in_append2 : forall (s0 : Site) (q1 q2 : queue Message), inc_dec_in_queue s0 (append Message q1 (input Message copy q2)) -> inc_dec_in_queue s0 (append Message q1 q2).
proof: Proof. intros s0 q1 q2. elim q1. simpl in |- *. auto. intro. case d; simpl in |- *; intros. apply H; auto. auto. apply H; auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4