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