proposition: Lemma rdec_trans_sigma_xi : sigma_xi (rec_dec_trans c0 s1 s2) = (if eq_site_dec owner s2 then (sigma_xi c0 - 1)%Z else sigma_xi c0).
proof: Proof. unfold sigma_xi in |- *; case (eq_site_dec owner s2); intro. apply sigma__pred with (eq_E_dec := eq_site_dec) (x0 := s1). exact finite_site. rewrite rdec_trans_xi. rewrite e; rewrite case_eq; apply case_eq. intros; rewrite rdec_trans_xi. rewrite e; rewrite case_eq; apply case_ineq; trivial. apply sigma_simpl. intros; rewrite rdec_trans_xi. apply case_ineq; trivial. Qed.
imports: init table_act mess_act