proposition: Lemma del_trans_ctrl_dec : forall s2 : Site, ctrl_dec s0 s2 (bm (delete_trans c0 s1)) = (if eq_site_dec owner s0 then if eq_site_dec s2 s1 then (ctrl_dec s0 s2 (bm c0) + 1)%Z else ctrl_dec s0 s2 (bm c0) else ctrl_dec s0 s2 (bm c0)).
proof: Proof. intros; unfold ctrl_dec in |- *; simpl in |- *. case (eq_site_dec owner s0); intro. case (eq_site_dec s2 s1); 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