(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* RECEIVE INC *)

(*definit la transition receive inc et ses consequences*)

Require Export init.
Require Export table_act.
Require Export mess_act.

Unset Standard Proposition Elimination Names.

Section DEF_REC_INC.

Definition rec_inc_trans (c : Config) (s1 s3 : Site) :=
  mkconfig (S (time c)) (dt c) (Inc_send_table (st c) owner) 
    (rt c) (Post_message dec (Collect_message (bm c) s1 owner) owner s3). 

End DEF_REC_INC.

Section REC_INC_EFFECT.

(* invariants *)

Variable c0 : Config.

Variable s1 s2 : Site.

Lemma rinc_trans_le_dt_time :
 forall s0 : Site,
 dt c0 s0 <= time c0 ->
 dt (rec_inc_trans c0 s1 s2) s0 <= time (rec_inc_trans c0 s1 s2).
Proof.
(* Goal: forall (s0 : Site) (_ : le (dt c0 s0) (time c0)), le (dt (rec_inc_trans c0 s1 s2) s0) (time (rec_inc_trans c0 s1 s2)) *)
 simpl in |- *; auto.
Qed.

Lemma rinc_trans_diff_site :
 forall s3 s4 : Site,
 (In_queue Message copy (bm c0 s3 s4) -> s3 <> s4) ->
 In_queue Message copy (bm (rec_inc_trans c0 s1 s2) s3 s4) -> s3 <> s4.
Proof.
(* Goal: forall (s3 s4 : Site) (_ : forall _ : parent c0 s3 s4, lt (dt c0 s3) (dt c0 s4)) (_ : parent (rec_inc_trans c0 s1 s2) s3 s4), lt (dt (rec_inc_trans c0 s1 s2) s3) (dt (rec_inc_trans c0 s1 s2) s4) *)
 simpl in |- *; intros; apply H.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s3 s4) *)
 apply in_collect with (s1 := s1) (s2 := owner).
(* Goal: In_queue Message (inc_dec s0) (Collect_message (bm c0) s1 owner s3 s4) *)
 apply in_post with (m' := dec) (s1 := owner) (s2 := s2).
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: In_queue Message (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s4) *)
 discriminate.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.
Qed.

Lemma rinc_trans_st :
 forall s0 : Site,
 st (rec_inc_trans c0 s1 s2) s0 =
 (if eq_site_dec s0 owner
  then (st c0 s0 + 1)%Z
  else st c0 s0).
Proof.
(* Goal: forall s0 : Site, @eq Z (st (rec_inc_trans c0 s1 s2) s0) (if eq_site_dec s0 owner then Z.add (st c0 s0) (Zpos xH) else st c0 s0) *)
 intro; simpl in |- *; case (eq_site_dec s0 owner); intro.
(* Goal: @eq Z (Inc_send_table (st c0) owner s0) (Z.add (st c0 s0) (Zpos xH)) *)
(* Goal: @eq Z (Inc_send_table (st c0) owner s0) (st c0 s0) *)
 rewrite e; apply S_inc_send_table.

(* Goal: @eq Z (Inc_send_table (st c0) owner s0) (st c0 s0) *)
 apply no_inc_send_table; auto.
Qed.

Lemma rinc_trans_in_queue :
 forall s0 s3 s4 : Site,
 In_queue Message (inc_dec s0) (bm (rec_inc_trans c0 s1 s2) s3 s4) ->
 In_queue Message (inc_dec s0) (bm c0 s3 s4).
Proof.
(* Goal: forall (s0 s3 s4 : Site) (_ : In_queue Message (inc_dec s0) (bm (rec_inc_trans c0 s1 s2) s3 s4)), In_queue Message (inc_dec s0) (bm c0 s3 s4) *)
 simpl in |- *; intros.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s3 s4) *)
 apply in_collect with (s1 := s1) (s2 := owner).
(* Goal: In_queue Message (inc_dec s0) (Collect_message (bm c0) s1 owner s3 s4) *)
 apply in_post with (m' := dec) (s1 := owner) (s2 := s2).
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: In_queue Message (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s4) *)
 discriminate.

(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 auto.
Qed.

Lemma rinc_trans_st_rt :
 forall s0 : Site,
 s0 <> owner ->
 ((st c0 s0 > 0)%Z -> rt c0 s0 = true) ->
 (st (rec_inc_trans c0 s1 s2) s0 > 0)%Z ->
 rt (rec_inc_trans c0 s1 s2) s0 = true.
Proof.
(* Goal: forall (s0 : Site) (_ : not (@eq Site s0 owner)) (_ : forall _ : Z.gt (st c0 s0) Z0, @eq bool (rt c0 s0) true) (_ : Z.gt (st (rec_inc_trans c0 s1 s2) s0) Z0), @eq bool (rt (rec_inc_trans c0 s1 s2) s0) true *)
 intros s0 H; simpl in |- *.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 rewrite no_inc_send_table; auto.
Qed.

End REC_INC_EFFECT.

Section REC_INC_CTRL.

(* decomptes de messages *)

Variable c0 : Config.

Variable s1 s2 : Site.

Hypothesis
  first_mess : first Message (bm c0 s1 owner) = value Message (inc_dec s2).

Lemma rinc_trans_ctrl_copy :
 forall s0 s3 : Site,
 ctrl_copy s0 s3 (bm (rec_inc_trans c0 s1 s2)) = ctrl_copy s0 s3 (bm c0).
Proof.
(* Goal: forall s0 s3 : Site, @eq Z (ctrl_copy s0 s3 (bm (rec_inc_trans c0 s1 s2))) (ctrl_copy s0 s3 (bm c0)) *)
 intros; unfold ctrl_copy in |- *; simpl in |- *.
(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
 rewrite diff_post_card_mess.
(* Goal: @eq Z (card_mess (inc_dec s0) (Collect_message (bm c0) s1 owner s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
(* Goal: or (not (@eq Message (inc_dec s0) dec)) (or (not (@eq Site s3 owner)) (not (@eq Site owner s2))) *)
 apply diff_collect_card_mess.
(* Goal: or (not (@eq (exc Message) (first Message (bm c0 s3 s0)) (value Message dec))) (or (not (@eq Site s3 s1)) (not (@eq Site s0 owner))) *)
(* Goal: or (not (@eq Message dec dec)) (or (not (@eq Site s3 owner)) (not (@eq Site s0 s2))) *)
 apply diff_or_elsewhere with (m := inc_dec s2); [ trivial | discriminate ].

(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: In_queue Message (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s4) *)
 left; discriminate.
Qed.

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.
(* Goal: forall s0 s3 : Site, @eq Z (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 Z.add (ctrl_dec s0 s3 (bm c0)) (Zpos xH) else ctrl_dec s0 s3 (bm c0) else ctrl_dec s0 s3 (bm c0)) *)
 intros; unfold ctrl_dec in |- *; simpl in |- *.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (if eq_site_dec s0 s2 then Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH) else sigma_ctrl_dec s0 (bm c0))) (if eq_site_dec s0 s2 then Z.sub (sigma_ctrl_inc s0 (bm c0)) (Zpos xH) else sigma_ctrl_inc s0 (bm c0))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 case (eq_site_dec s0 s2); intro.
(* Goal: @eq Z (card_mess dec (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s0)) (if eq_site_dec s3 owner then Z.add (card_mess dec (bm c0 s3 s0)) (Zpos xH) else card_mess dec (bm c0 s3 s0)) *)
(* Goal: @eq Z (card_mess dec (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s0)) (card_mess dec (bm c0 s3 s0)) *)
 case (eq_site_dec s3 owner); intro.
(* Goal: @eq Z (card_mess dec (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s0)) (Z.add (card_mess dec (bm c0 s3 s0)) (Zpos xH)) *)
(* Goal: @eq Z (card_mess dec (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s0)) (card_mess dec (bm c0 s3 s0)) *)
(* Goal: @eq Z (card_mess dec (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s0)) (card_mess dec (bm c0 s3 s0)) *)
 rewrite e; rewrite e0; rewrite post_card_mess.
(* Goal: @eq Z (Z.add (card_mess dec (Collect_message (bm c0) s1 owner owner s2)) (Zpos xH)) (Z.add (card_mess dec (bm c0 owner s2)) (Zpos xH)) *)
(* Goal: @eq Z (card_mess dec (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s0)) (card_mess dec (bm c0 s3 s0)) *)
(* Goal: @eq Z (card_mess dec (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s0)) (card_mess dec (bm c0 s3 s0)) *)
 rewrite diff_collect_card_mess.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.

(* Goal: or (not (@eq (exc Message) (first Message (bm c0 s3 s0)) (value Message dec))) (or (not (@eq Site s3 s1)) (not (@eq Site s0 owner))) *)
(* Goal: or (not (@eq Message dec dec)) (or (not (@eq Site s3 owner)) (not (@eq Site s0 s2))) *)
 apply diff_or_elsewhere with (m := inc_dec s2); [ trivial | discriminate ].

(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
 rewrite diff_post_card_mess.
(* Goal: @eq Z (card_mess (inc_dec s0) (Collect_message (bm c0) s1 owner s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
(* Goal: or (not (@eq Message (inc_dec s0) dec)) (or (not (@eq Site s3 owner)) (not (@eq Site owner s2))) *)
 apply diff_collect_card_mess.

(* Goal: or (not (@eq (exc Message) (first Message (bm c0 s3 s0)) (value Message dec))) (or (not (@eq Site s3 s1)) (not (@eq Site s0 owner))) *)
(* Goal: or (not (@eq Message dec dec)) (or (not (@eq Site s3 owner)) (not (@eq Site s0 s2))) *)
 apply diff_or_elsewhere with (m := inc_dec s2); [ trivial | discriminate ].

(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 auto.

(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
 rewrite diff_post_card_mess.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 apply diff_collect_card_mess; auto.

(* Goal: or (not (@eq (exc Message) (first Message (bm c0 s3 s0)) (value Message dec))) (or (not (@eq Site s3 s1)) (not (@eq Site s0 owner))) *)
(* Goal: or (not (@eq Message dec dec)) (or (not (@eq Site s3 owner)) (not (@eq Site s0 s2))) *)
 apply diff_or_elsewhere with (m := inc_dec s2); [ trivial | discriminate ].

(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 auto.
Qed.

Lemma rinc_trans_ctrl_inc :
 forall s0 s3 : Site,
 ctrl_inc s0 s3 (bm (rec_inc_trans c0 s1 s2)) =
 (if eq_site_dec s0 s2
  then
   if eq_site_dec s3 s1
   then (ctrl_inc s0 s3 (bm c0) - 1)%Z
   else ctrl_inc s0 s3 (bm c0)
  else ctrl_inc s0 s3 (bm c0)).
Proof.
(* Goal: forall s0 s3 : Site, @eq Z (ctrl_inc s0 s3 (bm (rec_inc_trans c0 s1 s2))) (if eq_site_dec s0 s2 then if eq_site_dec s3 s1 then Z.sub (ctrl_inc s0 s3 (bm c0)) (Zpos xH) else ctrl_inc s0 s3 (bm c0) else ctrl_inc s0 s3 (bm c0)) *)
 intros; unfold ctrl_inc in |- *; simpl in |- *.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (if eq_site_dec s0 s2 then Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH) else sigma_ctrl_dec s0 (bm c0))) (if eq_site_dec s0 s2 then Z.sub (sigma_ctrl_inc s0 (bm c0)) (Zpos xH) else sigma_ctrl_inc s0 (bm c0))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 case (eq_site_dec s0 s2); intro.
(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (if eq_site_dec s3 s1 then Z.sub (card_mess (inc_dec s0) (bm c0 s3 owner)) (Zpos xH) else card_mess (inc_dec s0) (bm c0 s3 owner)) *)
(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
 case (eq_site_dec s3 s1); intro.
(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
 rewrite e; rewrite e0; rewrite diff_post_card_mess.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 apply collect_card_mess; trivial.

(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: In_queue Message (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s4) *)
 left; discriminate.

(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
 rewrite diff_post_card_mess.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 apply diff_collect_card_mess; auto.

(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: In_queue Message (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s4) *)
 left; discriminate.

(* Goal: @eq Z (card_mess (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
 rewrite diff_post_card_mess.
(* Goal: @eq Z (card_mess (inc_dec s0) (Collect_message (bm c0) s1 owner s3 owner)) (card_mess (inc_dec s0) (bm c0 s3 owner)) *)
(* Goal: or (not (@eq Message (inc_dec s0) dec)) (or (not (@eq Site s3 owner)) (not (@eq Site owner s2))) *)
 apply diff_collect_card_mess.
 apply diff_or_elsewhere with (m := inc_dec s2);
  [ trivial | injection; auto ].

(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: In_queue Message (inc_dec s0) (Post_message dec (Collect_message (bm c0) s1 owner) owner s2 s3 s4) *)
 left; discriminate.
Qed.

Remark rinc_trans_sigma_copy :
 forall s0 : Site,
 sigma_ctrl_copy s0 (bm (rec_inc_trans c0 s1 s2)) =
 sigma_ctrl_copy s0 (bm c0).
Proof.
(* Goal: forall s0 : Site, @eq Z (sigma_ctrl_copy s0 (bm (rec_inc_trans c0 s1 s2))) (sigma_ctrl_copy s0 (bm c0)) *)
 intros; unfold sigma_ctrl_copy in |- *.
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_copy s0 si (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun si : Site => ctrl_copy s0 si (bm c0))) *)
 apply sigma_simpl; intros; apply rinc_trans_ctrl_copy.
Qed.

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.
(* Goal: forall s0 : Site, @eq Z (sigma_ctrl_dec s0 (bm (rec_inc_trans c0 s1 s2))) (if eq_site_dec s0 s2 then Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH) else sigma_ctrl_dec s0 (bm c0)) *)
 intros; unfold sigma_ctrl_dec in |- *.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (if eq_site_dec s0 s2 then Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH) else sigma_ctrl_dec s0 (bm c0))) (if eq_site_dec s0 s2 then Z.sub (sigma_ctrl_inc s0 (bm c0)) (Zpos xH) else sigma_ctrl_inc s0 (bm c0))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 case (eq_site_dec s0 s2); intro.
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_dec s0 si (bm (rec_inc_trans c0 s1 s2)))) (Z.add (sigma Site LS (fun si : Site => ctrl_dec s0 si (bm c0))) (Zpos xH)) *)
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_dec s0 si (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun si : Site => ctrl_dec s0 si (bm c0))) *)
 apply sigma__S with (eq_E_dec := eq_site_dec) (x0 := owner).
(* Goal: list_of_elements Site eq_site_dec LS *)
(* Goal: @eq Z (yi (rec_inc_trans c0 s1 s2) s1) (Z.sub (yi c0 s1) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s1)), @eq Z (yi (rec_inc_trans c0 s1 s2) x) (yi c0 x) *)
 exact finite_site.

(* Goal: @eq Z (ctrl_dec s0 owner (bm (rec_inc_trans c0 s1 s2))) (Z.add (ctrl_dec s0 owner (bm c0)) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x owner)), @eq Z (ctrl_dec s0 x (bm (rec_inc_trans c0 s1 s2))) (ctrl_dec s0 x (bm c0)) *)
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_dec s0 si (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun si : Site => ctrl_dec s0 si (bm c0))) *)
 rewrite rinc_trans_ctrl_dec; rewrite e; rewrite case_eq; apply case_eq.

 intros; rewrite rinc_trans_ctrl_dec; rewrite e; rewrite case_eq;
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
  apply case_ineq; auto.

 apply sigma_simpl; intros; rewrite rinc_trans_ctrl_dec; apply case_ineq;
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
  auto.
Qed.

Remark rinc_trans_sigma_inc :
 forall s0 : Site,
 sigma_ctrl_inc s0 (bm (rec_inc_trans c0 s1 s2)) =
 (if eq_site_dec s0 s2
  then (sigma_ctrl_inc s0 (bm c0) - 1)%Z
  else sigma_ctrl_inc s0 (bm c0)).
Proof.
(* Goal: forall s0 : Site, @eq Z (sigma_ctrl_inc s0 (bm (rec_inc_trans c0 s1 s2))) (if eq_site_dec s0 s2 then Z.sub (sigma_ctrl_inc s0 (bm c0)) (Zpos xH) else sigma_ctrl_inc s0 (bm c0)) *)
 intros; unfold sigma_ctrl_inc in |- *.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (if eq_site_dec s0 s2 then Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH) else sigma_ctrl_dec s0 (bm c0))) (if eq_site_dec s0 s2 then Z.sub (sigma_ctrl_inc s0 (bm c0)) (Zpos xH) else sigma_ctrl_inc s0 (bm c0))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 case (eq_site_dec s0 s2); intro.
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm (rec_inc_trans c0 s1 s2)))) (Z.sub (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm c0))) (Zpos xH)) *)
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm c0))) *)
 apply sigma__pred with (eq_E_dec := eq_site_dec) (x0 := s1).
(* Goal: list_of_elements Site eq_site_dec LS *)
(* Goal: @eq Z (yi (rec_inc_trans c0 s1 s2) s1) (Z.sub (yi c0 s1) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s1)), @eq Z (yi (rec_inc_trans c0 s1 s2) x) (yi c0 x) *)
 exact finite_site.

(* Goal: @eq Z (ctrl_inc s0 s1 (bm (rec_inc_trans c0 s1 s2))) (Z.sub (ctrl_inc s0 s1 (bm c0)) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s1)), @eq Z (ctrl_inc s0 x (bm (rec_inc_trans c0 s1 s2))) (ctrl_inc s0 x (bm c0)) *)
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm c0))) *)
 rewrite rinc_trans_ctrl_inc; rewrite e; rewrite case_eq; apply case_eq.

 intros; rewrite rinc_trans_ctrl_inc; rewrite e; rewrite case_eq;
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
  apply case_ineq; auto.

 apply sigma_simpl; intros; rewrite rinc_trans_ctrl_inc; apply case_ineq;
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
  auto.
Qed.

Lemma rinc_trans_sigma_ctrl :
 forall s0 : Site,
 sigma_ctrl s0 (bm (rec_inc_trans c0 s1 s2)) = sigma_ctrl s0 (bm c0).
Proof.
(* Goal: forall s0 : Site, @eq Z (sigma_ctrl s0 (bm (rec_inc_trans c0 s1 s2))) (sigma_ctrl s0 (bm c0)) *)
 intros; unfold sigma_ctrl in |- *.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm (rec_inc_trans c0 s1 s2))) (sigma_ctrl_dec s0 (bm (rec_inc_trans c0 s1 s2)))) (sigma_ctrl_inc s0 (bm (rec_inc_trans c0 s1 s2)))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 rewrite rinc_trans_sigma_copy.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm (rec_inc_trans c0 s1 s2)))) (sigma_ctrl_inc s0 (bm (rec_inc_trans c0 s1 s2)))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 rewrite rinc_trans_sigma_dec.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (if eq_site_dec s0 s2 then Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH) else sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm (rec_inc_trans c0 s1 s2)))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 rewrite rinc_trans_sigma_inc.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (if eq_site_dec s0 s2 then Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH) else sigma_ctrl_dec s0 (bm c0))) (if eq_site_dec s0 s2 then Z.sub (sigma_ctrl_inc s0 (bm c0)) (Zpos xH) else sigma_ctrl_inc s0 (bm c0))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 case (eq_site_dec s0 s2); intro.
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (Z.add (sigma_ctrl_dec s0 (bm c0)) (Zpos xH))) (Z.sub (sigma_ctrl_inc s0 (bm c0)) (Zpos xH))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
(* Goal: @eq Z (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) (Z.add (Z.add (sigma_ctrl_copy s0 (bm c0)) (sigma_ctrl_dec s0 (bm c0))) (sigma_ctrl_inc s0 (bm c0))) *)
 omega.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.
Qed.

End REC_INC_CTRL.

Section REC_INC_XY.

Variable c0 : Config.

Variable s1 s2 : Site.

Hypothesis
  first_mess : first Message (bm c0 s1 owner) = value Message (inc_dec s2).

Hypothesis not_owner : s2 <> owner.

Remark rinc_trans_xi :
 forall s0 : Site, xi (rec_inc_trans c0 s1 s2) s0 = xi c0 s0.
Proof.
(* Goal: forall s0 : Site, @eq Z (xi (rec_inc_trans c0 s1 s2) s0) (xi c0 s0) *)
 intro; unfold xi in |- *.
(* Goal: @eq Z (Z.add (Z.add (Int (rt (rec_inc_trans c0 s1 s2) s0)) (ctrl_copy owner s0 (bm (rec_inc_trans c0 s1 s2)))) (ctrl_dec owner s0 (bm (rec_inc_trans c0 s1 s2)))) (Z.add (Z.add (Int (rt c0 s0)) (ctrl_copy owner s0 (bm c0))) (ctrl_dec owner s0 (bm c0))) *)
 rewrite rinc_trans_ctrl_copy.
(* Goal: @eq Z (Z.add (Z.add (Int (rt (rec_inc_trans c0 s1 s2) s0)) (ctrl_copy owner s0 (bm c0))) (ctrl_dec owner s0 (bm (rec_inc_trans c0 s1 s2)))) (Z.add (Z.add (Int (rt c0 s0)) (ctrl_copy owner s0 (bm c0))) (ctrl_dec owner s0 (bm c0))) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 rewrite rinc_trans_ctrl_dec.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 simpl in |- *; rewrite case_ineq; auto.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.
Qed.

Remark rinc_trans_yi :
 forall s0 : Site,
 yi (rec_inc_trans c0 s1 s2) s0 =
 (if eq_site_dec s0 s1 then (yi c0 s0 - 1)%Z else yi c0 s0).
Proof.
(* Goal: forall s0 : Site, @eq Z (yi (rec_inc_trans c0 s1 s2) s0) (if eq_site_dec s0 s1 then Z.sub (yi c0 s0) (Zpos xH) else yi c0 s0) *)
 intro; unfold yi in |- *.
(* Goal: @eq Z (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm (rec_inc_trans c0 s1 s2)))) (if eq_site_dec s0 s1 then Z.sub (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) (Zpos xH) else sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) *)
 case (eq_site_dec s0 s1); intro.
(* Goal: @eq Z (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm (rec_inc_trans c0 s1 s2)))) (Z.sub (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) (Zpos xH)) *)
(* Goal: @eq Z (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) *)
 apply sigma__pred with (eq_E_dec := eq_site_dec) (x0 := s2).
(* Goal: list_of_elements Site eq_site_dec LS *)
(* Goal: @eq Z (yi (rec_inc_trans c0 s1 s2) s1) (Z.sub (yi c0 s1) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s1)), @eq Z (yi (rec_inc_trans c0 s1 s2) x) (yi c0 x) *)
 exact finite_site.

(* Goal: @eq Z (ctrl_inc s2 s0 (bm (rec_inc_trans c0 s1 s2))) (Z.sub (ctrl_inc s2 s0 (bm c0)) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s2)), @eq Z (ctrl_inc x s0 (bm (rec_inc_trans c0 s1 s2))) (ctrl_inc x s0 (bm c0)) *)
(* Goal: @eq Z (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) *)
 rewrite rinc_trans_ctrl_inc.
(* Goal: @eq Z (if eq_site_dec s2 s2 then if eq_site_dec s0 s1 then Z.sub (ctrl_inc s2 s0 (bm c0)) (Zpos xH) else ctrl_inc s2 s0 (bm c0) else ctrl_inc s2 s0 (bm c0)) (Z.sub (ctrl_inc s2 s0 (bm c0)) (Zpos xH)) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s2)), @eq Z (ctrl_inc x s0 (bm (rec_inc_trans c0 s1 s2))) (ctrl_inc x s0 (bm c0)) *)
(* Goal: @eq Z (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) *)
 rewrite e; rewrite case_eq; apply case_eq.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.

(* Goal: @eq Z (ctrl_inc s2 s0 (bm (rec_inc_trans c0 s1 s2))) (Z.sub (ctrl_inc s2 s0 (bm c0)) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s2)), @eq Z (ctrl_inc x s0 (bm (rec_inc_trans c0 s1 s2))) (ctrl_inc x s0 (bm c0)) *)
(* Goal: @eq Z (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) *)
 intros; rewrite rinc_trans_ctrl_inc.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 apply case_ineq; trivial.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.

(* Goal: @eq Z (ctrl_inc s2 s0 (bm (rec_inc_trans c0 s1 s2))) (Z.sub (ctrl_inc s2 s0 (bm c0)) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s2)), @eq Z (ctrl_inc x s0 (bm (rec_inc_trans c0 s1 s2))) (ctrl_inc x s0 (bm c0)) *)
(* Goal: @eq Z (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun s' : Site => ctrl_inc s' s0 (bm c0))) *)
 apply sigma_simpl; intros; rewrite rinc_trans_ctrl_inc.
(* Goal: @eq Z (if eq_site_dec x s2 then if eq_site_dec s0 s1 then Z.sub (ctrl_inc x s0 (bm c0)) (Zpos xH) else ctrl_inc x s0 (bm c0) else ctrl_inc x s0 (bm c0)) (ctrl_inc x s0 (bm c0)) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 case (eq_site_dec x s2); intro.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 apply case_ineq; auto.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 trivial.
Qed.

Lemma rinc_trans_sigma_xi : sigma_xi (rec_inc_trans c0 s1 s2) = sigma_xi c0.
Proof.
(* Goal: @eq Z (sigma_xi (rec_inc_trans c0 s1 s2)) (sigma_xi c0) *)
 unfold sigma_xi in |- *; apply sigma_simpl; intros; apply rinc_trans_xi.
Qed.

Lemma rinc_trans_sigma_yi :
 sigma_yi (rec_inc_trans c0 s1 s2) = (sigma_yi c0 - 1)%Z.
Proof.
 unfold sigma_yi in |- *;
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm (rec_inc_trans c0 s1 s2)))) (Z.sub (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm c0))) (Zpos xH)) *)
(* Goal: @eq Z (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm (rec_inc_trans c0 s1 s2)))) (sigma Site LS (fun si : Site => ctrl_inc s0 si (bm c0))) *)
  apply sigma__pred with (eq_E_dec := eq_site_dec) (x0 := s1).
(* Goal: list_of_elements Site eq_site_dec LS *)
(* Goal: @eq Z (yi (rec_inc_trans c0 s1 s2) s1) (Z.sub (yi c0 s1) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s1)), @eq Z (yi (rec_inc_trans c0 s1 s2) x) (yi c0 x) *)
 exact finite_site.

(* Goal: @eq Z (yi (rec_inc_trans c0 s1 s2) s1) (Z.sub (yi c0 s1) (Zpos xH)) *)
(* Goal: forall (x : Site) (_ : not (@eq Site x s1)), @eq Z (yi (rec_inc_trans c0 s1 s2) x) (yi c0 x) *)
 rewrite rinc_trans_yi; apply case_eq.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 intros; rewrite rinc_trans_yi; apply case_ineq; trivial.
Qed.

End REC_INC_XY.

Section REC_INC_ALT.

(* structure de file d'attente *)

Variable c0 : Config.

Variable s0 s1 s2 : Site.

Hypothesis s2_not_owner : s2 <> owner.

Lemma rinc_trans_D :
 D_queue (bm c0 s0 owner) -> D_queue (bm (rec_inc_trans c0 s1 s2) s0 owner).
Proof.
(* Goal: forall _ : D_queue (bm c0 s0 owner), D_queue (bm (rec_inc_trans c0 s1 s2) s0 owner) *)
 intros; simpl in |- *; apply D_post_elsewhere.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 auto.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 apply D_collect; trivial.
Qed.

Lemma rinc_trans_alt :
 alternate (bm c0 s0 owner) ->
 alternate (bm (rec_inc_trans c0 s1 s2) s0 owner).
Proof.
(* Goal: forall _ : alternate (bm c0 s0 owner), alternate (bm (rec_inc_trans c0 s1 s2) s0 owner) *)
 intros; simpl in |- *; apply alt_post_elsewhere.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s2 owner)) *)
(* Goal: alternate (Collect_message (bm c0) s1 owner s0 owner) *)
 auto.

(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 apply alt_collect; trivial.
Qed.

End REC_INC_ALT.

Section REC_INC_RELAT.

(* sur la relation parent *)

Variable c0 : Config.

Variable s1 s2 : Site.

Remark rinc_trans_parent :
 forall s3 s4 : Site,
 parent (rec_inc_trans c0 s1 s2) s4 s3 -> parent c0 s4 s3.
Proof.
(* Goal: forall (s3 s4 : Site) (_ : parent (rec_inc_trans c0 s1 s2) s4 s3), parent c0 s4 s3 *)
 intros; elim H.
(* Goal: forall (s3 s0 : Site) (_ : In_queue Message (inc_dec s3) (bm (rec_inc_trans c0 s1 s2) s0 owner)), parent c0 s3 s0 *)
 intros; apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 apply rinc_trans_in_queue with (s1 := s1) (s2 := s2); trivial.
Qed.

Lemma rinc_trans_parent_cr :
 forall s3 s4 : Site,
 (parent c0 s3 s4 -> dt c0 s3 < dt c0 s4) ->
 parent (rec_inc_trans c0 s1 s2) s3 s4 ->
 dt (rec_inc_trans c0 s1 s2) s3 < dt (rec_inc_trans c0 s1 s2) s4.
Proof.
(* Goal: forall (s3 s4 : Site) (_ : forall _ : parent c0 s3 s4, lt (dt c0 s3) (dt c0 s4)) (_ : parent (rec_inc_trans c0 s1 s2) s3 s4), lt (dt (rec_inc_trans c0 s1 s2) s3) (dt (rec_inc_trans c0 s1 s2) s4) *)
 simpl in |- *; intros; apply H.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s2)) *)
 apply rinc_trans_parent; trivial.
Qed.

End REC_INC_RELAT.
