proposition: Lemma inc_dec_in_append : forall (s0 : Site) (q1 q2 q3 q4 : queue Message), append Message q1 q2 = append Message q3 q4 -> inc_dec_in_queue s0 (append Message q3 (input Message copy q4)) -> inc_dec_in_queue s0 (append Message q1 (input Message copy q2)).
proof: Proof. intros. apply inc_dec_in_append1. rewrite H. apply inc_dec_in_append2. auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4