proposition: Remark rinc_trans_sigma_dec : forall s0 : Site, sigma_ctrl_dec s0 (bm (rec_inc_trans c0 s1 s2)) = (if eq_site_dec s0 s2 then (sigma_ctrl_dec s0 (bm c0) + 1)%Z else sigma_ctrl_dec s0 (bm c0)).
proof: Proof. intros; unfold sigma_ctrl_dec in |- *. case (eq_site_dec s0 s2); intro. apply sigma__S with (eq_E_dec := eq_site_dec) (x0 := owner). exact finite_site. rewrite rinc_trans_ctrl_dec; rewrite e; rewrite case_eq; apply case_eq. intros; rewrite rinc_trans_ctrl_dec; rewrite e; rewrite case_eq; apply case_ineq; auto. apply sigma_simpl; intros; rewrite rinc_trans_ctrl_dec; apply case_ineq; auto. Qed.
imports: init table_act mess_act