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