proposition: Lemma rcop1_trans_ctrl_copy : forall s3 : Site, ctrl_copy s0 s3 (bm (rec_copy1_trans c0 s1 s2)) = (if eq_site_dec s0 s1 then if eq_site_dec s3 s2 then (ctrl_copy s0 s3 (bm c0) - 1)%Z else ctrl_copy s0 s3 (bm c0) else ctrl_copy s0 s3 (bm c0)).
proof: Proof. intros; unfold ctrl_copy in |- *; simpl in |- *. rewrite diff_post_card_mess. case (eq_site_dec s0 s1); intro. case (eq_site_dec s3 s2); intro. rewrite e; rewrite e0; apply collect_card_mess; trivial. apply diff_collect_card_mess; auto. apply diff_collect_card_mess; auto. left; discriminate. Qed.
imports: init table_act mess_act