proposition: Lemma not_in_queue_input : forall (q : queue Message) (m1 m : Message), ~ In_queue Message m1 (input Message m q) -> ~ In_queue Message m1 q.
proof: Proof. simple induction q. simpl in |- *. intros. unfold not in |- *; contradiction. simpl in |- *. intros. unfold not in |- *; intro; elim H0. elim H1; auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4