proposition: Lemma copy_trans_ctrl_copy : forall s' : Site, ctrl_copy s0 s' (bm (copy_trans c0 s1 s2)) = (if eq_site_dec s0 s1 then if eq_site_dec s' s2 then (ctrl_copy s0 s' (bm c0) + 1)%Z else ctrl_copy s0 s' (bm c0) else ctrl_copy s0 s' (bm c0)).
proof: Proof. intros; unfold ctrl_copy in |- *; simpl in |- *. case (eq_site_dec s0 s1); intro. case (eq_site_dec s' s2); intro. rewrite e; rewrite e0; apply post_card_mess. apply diff_post_card_mess; auto. apply diff_post_card_mess; auto. Qed.
imports: init table_act mess_act