proposition: Lemma rcop3_trans_ctrl_inc : forall s3 : Site, ctrl_inc s0 s3 (bm (rec_copy3_trans c0 s1 s2)) = (if eq_site_dec s0 s1 then if eq_site_dec s3 s2 then (ctrl_inc s0 s3 (bm c0) + 1)%Z else ctrl_inc s0 s3 (bm c0) else ctrl_inc s0 s3 (bm c0)).
proof: Proof. intros; unfold ctrl_inc in |- *; simpl in |- *. case (eq_site_dec s0 s1); intro. case (eq_site_dec s3 s2); intro. rewrite e; rewrite e0; rewrite post_card_mess. rewrite diff_collect_card_mess. trivial. apply diff_or_elsewhere with (m := copy); [ trivial | discriminate ]. rewrite diff_post_card_mess. apply diff_collect_card_mess. apply diff_or_elsewhere with (m := copy); [ trivial | discriminate ]. auto. rewrite diff_post_card_mess. apply diff_collect_card_mess. apply diff_or_elsewhere with (m := copy); [ trivial | discriminate ]. left; injection; auto. Qed.
imports: init table_act mess_act