proposition: Lemma rdec_trans_ctrl_dec : forall s3 : Site, ctrl_dec s0 s3 (bm (rec_dec_trans c0 s1 s2)) = (if eq_site_dec s0 s2 then if eq_site_dec s3 s1 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 s1); 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