(* 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                                                     *)


(* EVOLUTION *)

(* definit l'evolution de la machine au cours du temps et ses invariants *)

Require Export copy.
Require Export del.
Require Export rece_copy1.
Require Export rece_copy2.
Require Export rece_copy3.
Require Export rece_dec.
Require Export rece_inc.

Unset Standard Proposition Elimination Names.

Section EVOLUTION.
	
(* ou l'on trouvera successivement la definition des transitions avec
les preconditions, puis l'action elle_meme, pour finir avec la
definition d'un etat legal comme etant celui obtenu a partir de l'etat
initial et d'un nombre quelconque de transitions *)

Inductive class_trans (c : Config) : Set :=
  | make_copy :
      forall s1 s2 : Site,
      s1 <> s2 -> s2 <> owner -> access s1 (rt c) -> class_trans c
  | receive_dec :
      forall s1 s2 : Site,
      first Message (bm c s1 s2) = value Message dec -> class_trans c
  | receive_inc :
      forall s1 s3 : Site,
      first Message (bm c s1 owner) = value Message (inc_dec s3) ->
      class_trans c
  | receive_copy1 :
      forall s1 s2 : Site,
      rt c s2 = true ->
      first Message (bm c s1 s2) = value Message copy -> class_trans c
  | receive_copy2 :
      forall s2 : Site,
      rt c s2 = false ->
      first Message (bm c owner s2) = value Message copy -> class_trans c
  | receive_copy3 :
      forall s1 s2 : Site,
      rt c s2 = false ->
      s1 <> owner ->
      first Message (bm c s1 s2) = value Message copy -> class_trans c
  | delete_entry :
      forall s : Site,
      st c s = 0%Z -> rt c s = true -> s <> owner -> class_trans c.

Definition transition (c : Config) (t : class_trans c) :=
  match t with
  | make_copy s1 s2 h1 h2 h3 => copy_trans c s1 s2
  | receive_dec s1 s2 h1 => rec_dec_trans c s1 s2
  | receive_inc s1 s3 h1 => rec_inc_trans c s1 s3
  | receive_copy1 s1 s2 h1 h2 => rec_copy1_trans c s1 s2
  | receive_copy2 s2 h1 h2 => rec_copy2_trans c s2
  | receive_copy3 s1 s2 h1 h2 h3 => rec_copy3_trans c s1 s2
  | delete_entry s h1 h2 h3 => delete_trans c s
  end.

Inductive legal : Config -> Prop :=
  | begin : legal config_init
  | after :
      forall (c : Config) (t : class_trans c),
      legal c -> legal (transition c t).
	
End EVOLUTION.

Section M_INVARIANTS.

(* il s'agit d'invariants d'etat de la machine, leurs preuves suivant
le meme schema, verification sur la situation initiale puis induction
et etude par cas *)

(* l'estampille est inferieure au temps *)

Lemma le_dt_time :
 forall (c0 : Config) (s0 : Site), legal c0 -> dt c0 s0 <= time c0.
Proof.
(* Goal: forall (s1 s2 : Site) (_ : ancestor c0 s2 s1), @eq bool (rt c0 s2) true *)
 intros; elim H.
(* Goal: le (dt config_init s0) (time config_init) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : le (dt c s0) (time c)), le (dt (transition c t) s0) (time (transition c t)) *)
 apply init_le_dt_time.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: le (dt (copy_trans c s1 s2) s0) (time (copy_trans c s1 s2)) *)
(* Goal: le (dt (rec_dec_trans c s1 s2) s0) (time (rec_dec_trans c s1 s2)) *)
(* Goal: le (dt (rec_inc_trans c s1 s3) s0) (time (rec_inc_trans c s1 s3)) *)
(* Goal: le (dt (rec_copy1_trans c s1 s2) s0) (time (rec_copy1_trans c s1 s2)) *)
(* Goal: le (dt (rec_copy2_trans c s2) s0) (time (rec_copy2_trans c s2)) *)
(* Goal: le (dt (rec_copy3_trans c s1 s2) s0) (time (rec_copy3_trans c s1 s2)) *)
(* Goal: le (dt (delete_trans c s) s0) (time (delete_trans c s)) *)
 apply copy_trans_le_dt_time; trivial.

(* Goal: le (dt (rec_dec_trans c s1 s2) s0) (time (rec_dec_trans c s1 s2)) *)
(* Goal: le (dt (rec_inc_trans c s1 s3) s0) (time (rec_inc_trans c s1 s3)) *)
(* Goal: le (dt (rec_copy1_trans c s1 s2) s0) (time (rec_copy1_trans c s1 s2)) *)
(* Goal: le (dt (rec_copy2_trans c s2) s0) (time (rec_copy2_trans c s2)) *)
(* Goal: le (dt (rec_copy3_trans c s1 s2) s0) (time (rec_copy3_trans c s1 s2)) *)
(* Goal: le (dt (delete_trans c s) s0) (time (delete_trans c s)) *)
 apply rdec_trans_le_dt_time; trivial.

(* Goal: le (dt (rec_inc_trans c s1 s3) s0) (time (rec_inc_trans c s1 s3)) *)
(* Goal: le (dt (rec_copy1_trans c s1 s2) s0) (time (rec_copy1_trans c s1 s2)) *)
(* Goal: le (dt (rec_copy2_trans c s2) s0) (time (rec_copy2_trans c s2)) *)
(* Goal: le (dt (rec_copy3_trans c s1 s2) s0) (time (rec_copy3_trans c s1 s2)) *)
(* Goal: le (dt (delete_trans c s) s0) (time (delete_trans c s)) *)
 apply rinc_trans_le_dt_time; trivial.

(* Goal: le (dt (rec_copy1_trans c s1 s2) s0) (time (rec_copy1_trans c s1 s2)) *)
(* Goal: le (dt (rec_copy2_trans c s2) s0) (time (rec_copy2_trans c s2)) *)
(* Goal: le (dt (rec_copy3_trans c s1 s2) s0) (time (rec_copy3_trans c s1 s2)) *)
(* Goal: le (dt (delete_trans c s) s0) (time (delete_trans c s)) *)
 apply rcop1_trans_le_dt_time; trivial.

(* Goal: le (dt (rec_copy2_trans c s2) s0) (time (rec_copy2_trans c s2)) *)
(* Goal: le (dt (rec_copy3_trans c s1 s2) s0) (time (rec_copy3_trans c s1 s2)) *)
(* Goal: le (dt (delete_trans c s) s0) (time (delete_trans c s)) *)
 apply rcop2_trans_le_dt_time; trivial.

(* Goal: le (dt (rec_copy3_trans c s1 s2) s0) (time (rec_copy3_trans c s1 s2)) *)
(* Goal: le (dt (delete_trans c s) s0) (time (delete_trans c s)) *)
 apply rcop3_trans_le_dt_time; trivial.

(* Goal: le (dt (delete_trans c s) s0) (time (delete_trans c s)) *)
 apply del_trans_le_dt_time; trivial.
Qed.

(* le site destination d'un message inc_dec n'est jamais le
proprietaire *)

Lemma not_owner_inc :
 forall (c : Config) (s0 s1 s2 : Site),
 legal c -> In_queue Message (inc_dec s0) (bm c s1 s2) -> s0 <> owner.
Proof.
(* Goal: forall (c : Config) (s0 s1 s2 : Site) (_ : legal c) (_ : In_queue Message (inc_dec s0) (bm c s1 s2)), not (@eq Site s0 owner) *)
 intros c s0 s1 s2 H; elim H; simpl in |- *.
(* Goal: forall _ : False, not (@eq Site s0 owner) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : In_queue Message (inc_dec s0) (bm c s1 s2), not (@eq Site s0 owner)) (_ : In_queue Message (inc_dec s0) (bm (transition c t) s1 s2)), not (@eq Site s0 owner) *)
 contradiction.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 apply H1; apply copy_trans_in_queue with (s1 := s3) (s2 := s4); trivial.

(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 apply H1; apply rdec_trans_in_queue with (s1 := s3) (s2 := s4); trivial.

(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 apply H1; apply rinc_trans_in_queue with (s1 := s3) (s2 := s4); trivial.

(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 apply H1; apply rcop1_trans_in_queue with (s1 := s3) (s2 := s4); trivial.

(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 apply H1; apply rcop2_trans_in_queue with (s2 := s3); trivial.

(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 case (eq_site_dec s0 s3); intro.
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 rewrite e1; trivial.

(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
 apply H1; apply rcop3_trans_in_queue with (s1 := s3) (s2 := s4); trivial.

(* Goal: not (@eq Site s0 owner) *)
 apply H1; apply del_trans_in_queue with (s1 := s); trivial.
Qed.

Lemma not_owner_first_inc :
 forall (c : Config) (s0 s1 s2 : Site),
 legal c ->
 first Message (bm c s1 s2) = value Message (inc_dec s0) -> s0 <> owner.
Proof.
(* Goal: forall (c : Config) (s0 s1 s2 : Site) (_ : legal c) (_ : @eq (exc Message) (first Message (bm c s1 s2)) (value Message (inc_dec s0))), not (@eq Site s0 owner) *)
 intros; apply (not_owner_inc c s0 s1 s2).
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply first_in; trivial.
Qed.

(* l'origine et la destination d'un message copy sont distincts *)

Lemma copy_diff_site :
 forall (c0 : Config) (s1 s2 : Site),
 legal c0 -> In_queue Message copy (bm c0 s1 s2) -> s1 <> s2.
Proof.
(* Goal: forall (c0 : Config) (s1 s2 : Site) (_ : legal c0) (_ : In_queue Message copy (bm c0 s1 s2)), not (@eq Site s1 s2) *)
 intros c0 s1 s2 Hlegal; elim Hlegal.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply init_copy_diff_site; trivial.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply copy_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rdec_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rinc_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rcop1_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rcop2_trans_diff_site with (c0 := c) (s2 := s0); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rcop3_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply del_trans_diff_site with (c0 := c) (s0 := s); trivial.
Qed.

Lemma first_copy_diff_site :
 forall (c0 : Config) (s1 s2 : Site),
 legal c0 -> first Message (bm c0 s1 s2) = value Message copy -> s1 <> s2.
Proof.
(* Goal: forall (c0 : Config) (s1 s2 : Site) (_ : legal c0) (_ : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)), not (@eq Site s1 s2) *)
 intros; apply (copy_diff_site c0 s1 s2).
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply first_in; trivial.
Qed.

End M_INVARIANTS.

Section X_INVARIANTS.

(* preuves de deux lemmes sur la valeur du compteur st dans un site
autre que le proprietaire et chez le proprietaire *)

Lemma two :
 forall (c0 : Config) (s0 : Site),
 legal c0 -> s0 <> owner -> st c0 s0 = sigma_ctrl s0 (bm c0).
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (Z.add (st c owner) (sigma_yi c)) (sigma_xi c) *)
 intros; elim H; simpl in |- *.
(* Goal: @eq Z (send_init s0) (sigma_ctrl s0 bag_init) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : @eq Z (st c s0) (sigma_ctrl s0 (bm c))), @eq Z (st (transition c t) s0) (sigma_ctrl s0 (bm (transition c t))) *)
 rewrite sigma_ctrl_init; auto.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: @eq Z (st (copy_trans c s1 s2) s0) (sigma_ctrl s0 (bm (copy_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_dec_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_dec_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_inc_trans c s1 s3) s0) (sigma_ctrl s0 (bm (rec_inc_trans c s1 s3))) *)
(* Goal: @eq Z (st (rec_copy1_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy1_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite copy_trans_sigma_ctrl. 
(* Goal: @eq Z (Z.add (st (copy_trans c0 s1 s2) owner) (sigma_yi (copy_trans c0 s1 s2))) (sigma_xi (copy_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_dec_trans c0 s1 s2) owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite copy_trans_st.
(* Goal: @eq Z (if eq_site_dec s0 s1 then Z.add (st c s0) (Zpos xH) else st c s0) (if eq_site_dec s0 s1 then Z.add (sigma_ctrl s0 (bm c)) (Zpos xH) else sigma_ctrl s0 (bm c)) *)
(* Goal: @eq Z (st (rec_dec_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_dec_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_inc_trans c s1 s3) s0) (sigma_ctrl s0 (bm (rec_inc_trans c s1 s3))) *)
(* Goal: @eq Z (st (rec_copy1_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy1_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 case (eq_site_dec s0 s1); intro; omega.

(* Goal: @eq Z (st (rec_dec_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_dec_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_inc_trans c s1 s3) s0) (sigma_ctrl s0 (bm (rec_inc_trans c s1 s3))) *)
(* Goal: @eq Z (st (rec_copy1_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy1_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite rdec_trans_sigma_ctrl. 
(* Goal: @eq Z (Z.add (st (rec_dec_trans c0 s1 s2) owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rdec_trans_st.
(* Goal: @eq Z (if eq_site_dec s0 s2 then Z.sub (st c s0) (Zpos xH) else st c s0) (if eq_site_dec s0 s2 then Z.sub (sigma_ctrl s0 (bm c)) (Zpos xH) else sigma_ctrl s0 (bm c)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: @eq Z (st (rec_inc_trans c s1 s3) s0) (sigma_ctrl s0 (bm (rec_inc_trans c s1 s3))) *)
(* Goal: @eq Z (st (rec_copy1_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy1_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 case (eq_site_dec s0 s2); intro; omega.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq Z (st (rec_inc_trans c s1 s3) s0) (sigma_ctrl s0 (bm (rec_inc_trans c s1 s3))) *)
(* Goal: @eq Z (st (rec_copy1_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy1_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite rinc_trans_sigma_ctrl. 
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rinc_trans_st.
(* Goal: @eq Z (if eq_site_dec s0 owner then Z.add (st c s0) (Zpos xH) else st c s0) (sigma_ctrl s0 (bm c)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3)) *)
(* Goal: @eq Z (st (rec_copy1_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy1_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite case_ineq; auto.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq Z (st (rec_copy1_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy1_trans c s1 s2))) *)
(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite rcop1_trans_sigma_ctrl; auto. 

(* Goal: @eq Z (st (rec_copy2_trans c s2) s0) (sigma_ctrl s0 (bm (rec_copy2_trans c s2))) *)
(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite rcop2_trans_sigma_ctrl; auto. 

(* Goal: @eq Z (st (rec_copy3_trans c s1 s2) s0) (sigma_ctrl s0 (bm (rec_copy3_trans c s1 s2))) *)
(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite rcop3_trans_sigma_ctrl; auto. 

(* Goal: @eq Z (st (delete_trans c s) s0) (sigma_ctrl s0 (bm (delete_trans c s))) *)
 rewrite del_trans_sigma_ctrl; auto. 
Qed.

Lemma four :
 forall c : Config, legal c -> (st c owner + sigma_yi c)%Z = sigma_xi c.
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (Z.add (st c owner) (sigma_yi c)) (sigma_xi c) *)
 intros; elim H; simpl in |- *.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 rewrite sigma_xi_init; rewrite sigma_yi_init; trivial.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: @eq Z (Z.add (st (copy_trans c0 s1 s2) owner) (sigma_yi (copy_trans c0 s1 s2))) (sigma_xi (copy_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_dec_trans c0 s1 s2) owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite copy_trans_st.
(* Goal: @eq Z (Z.add (if eq_site_dec owner s1 then Z.add (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi (copy_trans c0 s1 s2))) (sigma_xi (copy_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_dec_trans c0 s1 s2) owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite copy_trans_sigma_xi.
(* Goal: @eq Z (Z.add (if eq_site_dec owner s1 then Z.add (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi (copy_trans c0 s1 s2))) (if eq_site_dec owner s1 then Z.add (sigma_xi c0) (Zpos xH) else sigma_xi c0) *)
(* Goal: @eq Z (Z.add (st (rec_dec_trans c0 s1 s2) owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite copy_trans_sigma_yi.
(* Goal: @eq Z (Z.add (if eq_site_dec owner s1 then Z.add (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi c0)) (if eq_site_dec owner s1 then Z.add (sigma_xi c0) (Zpos xH) else sigma_xi c0) *)
(* Goal: @eq Z (Z.add (st (rec_dec_trans c0 s1 s2) owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 case (eq_site_dec owner s1); intro; omega.

(* Goal: @eq Z (Z.add (st (rec_dec_trans c0 s1 s2) owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rdec_trans_st.
(* Goal: @eq Z (Z.add (if eq_site_dec owner s2 then Z.sub (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (sigma_xi (rec_dec_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rdec_trans_sigma_xi.
(* Goal: @eq Z (Z.add (if eq_site_dec owner s2 then Z.sub (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi (rec_dec_trans c0 s1 s2))) (if eq_site_dec owner s2 then Z.sub (sigma_xi c0) (Zpos xH) else sigma_xi c0) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message dec) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rdec_trans_sigma_yi.
(* Goal: @eq Z (Z.add (if eq_site_dec owner s2 then Z.sub (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi c0)) (if eq_site_dec owner s2 then Z.sub (sigma_xi c0) (Zpos xH) else sigma_xi c0) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message dec) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message dec) *)
(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 case (eq_site_dec owner s2); intro; omega.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq Z (Z.add (st (rec_inc_trans c0 s1 s3) owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rinc_trans_st.
(* Goal: @eq Z (Z.add (if eq_site_dec owner owner then Z.add (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi (rec_inc_trans c0 s1 s3)) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rinc_trans_sigma_xi.
(* Goal: @eq Z (Z.add (if eq_site_dec owner owner then Z.add (st c0 owner) (Zpos xH) else st c0 owner) (sigma_yi (rec_inc_trans c0 s1 s3))) (sigma_xi c0) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3)) *)
(* Goal: not (@eq Site s3 owner) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rinc_trans_sigma_yi.
(* Goal: @eq Z (Z.add (if eq_site_dec owner owner then Z.add (st c0 owner) (Zpos xH) else st c0 owner) (Z.sub (sigma_yi c0) (Zpos xH))) (sigma_xi c0) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3)) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3)) *)
(* Goal: not (@eq Site s3 owner) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite case_eq; omega.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: not (@eq Site s3 owner) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 apply (not_owner_inc c0 s3 s1 owner).
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: In_queue Message (inc_dec s3) (bm c0 s1 owner) *)
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 apply first_in; auto.

(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi (rec_copy1_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rcop1_trans_sigma_xi.
(* Goal: @eq Z (Z.add (st (rec_copy1_trans c0 s1 s2) owner) (sigma_yi (rec_copy1_trans c0 s1 s2))) (sigma_xi c0) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rcop1_trans_sigma_yi.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 auto.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi (rec_copy2_trans c0 s2)) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rcop2_trans_sigma_xi.
(* Goal: @eq Z (Z.add (st (rec_copy2_trans c0 s2) owner) (sigma_yi (rec_copy2_trans c0 s2))) (sigma_xi c0) *)
(* Goal: @eq bool (rt c0 s2) false *)
(* Goal: @eq (exc Message) (first Message (bm c0 owner s2)) (value Message copy) *)
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rcop2_trans_sigma_yi.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 auto.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (sigma_xi (rec_copy3_trans c0 s1 s2)) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rcop3_trans_sigma_xi.
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (sigma_yi (rec_copy3_trans c0 s1 s2))) (Z.add (sigma_xi c0) (Zpos xH)) *)
(* Goal: @eq bool (rt c0 s2) false *)
(* Goal: not (@eq Site s1 owner) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite rcop3_trans_sigma_yi.
(* Goal: @eq Z (Z.add (st (rec_copy3_trans c0 s1 s2) owner) (Z.add (sigma_yi c0) (Zpos xH))) (Z.add (sigma_xi c0) (Zpos xH)) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: @eq bool (rt c0 s2) false *)
(* Goal: not (@eq Site s1 owner) *)
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 simpl in |- *; omega.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi (delete_trans c0 s)) *)
 rewrite del_trans_sigma_xi.
(* Goal: @eq Z (Z.add (st (delete_trans c0 s) owner) (sigma_yi (delete_trans c0 s))) (sigma_xi c0) *)
(* Goal: @eq bool (rt c0 s) true *)
 rewrite del_trans_sigma_yi.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 auto.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.
Qed.

End X_INVARIANTS.

Section ALT_PROP.

(* preuves que la file d'attente entre un site et le proprietaire
contient des alternances de messages dec et inc_dec dans lesquelles
les messages inc_dec sont toujours isoles. Cela permettra de montrer
que les yi sont toujours superieurs ou egaux a -1 *)

Lemma legal_false_D :
 forall (c0 : Config) (s0 : Site),
 legal c0 -> rt c0 s0 = false -> D_queue (bm c0 s0 owner).
Proof.
(* Goal: forall (c0 : Config) (s0 : Site) (_ : legal c0) (_ : @eq bool (rt c0 s0) false), D_queue (bm c0 s0 owner) *)
 intros c0 s0 H; elim H.
(* Goal: forall _ : @eq bool (rt config_init s0) false, D_queue (bm config_init s0 owner) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : @eq bool (rt c s0) false, D_queue (bm c s0 owner)) (_ : @eq bool (rt (transition c t) s0) false), D_queue (bm (transition c t) s0 owner) *)
 intro; apply D_init.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply copy_trans_D; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rdec_trans_D; auto.

(* Goal: D_queue (bm (rec_inc_trans c s1 s3) s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rinc_trans_D.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply (not_owner_first_inc c s3 s1 owner); auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rcop1_trans_D; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rcop2_trans_D; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rcop3_trans_D; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply del_trans_D; auto.
Qed.

Lemma legal_alternate :
 forall (s0 : Site) (c0 : Config), legal c0 -> alternate (bm c0 s0 owner).
Proof.
(* Goal: forall (s1 s2 : Site) (_ : ancestor c0 s2 s1), @eq bool (rt c0 s2) true *)
 intros; elim H.
(* Goal: alternate (bm config_init s0 owner) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : alternate (bm c s0 owner)), alternate (bm (transition c t) s0 owner) *)
 apply alt_init.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply copy_trans_alt; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rdec_trans_alt; trivial.

(* Goal: alternate (bm (rec_inc_trans c s1 s3) s0 owner) *)
(* Goal: alternate (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: alternate (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: alternate (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: alternate (bm (delete_trans c s) s0 owner) *)
 apply rinc_trans_alt.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply (not_owner_first_inc c s3 s1 owner); auto.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rcop1_trans_alt; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rcop2_trans_alt; trivial.

(* Goal: alternate (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: alternate (bm (delete_trans c s) s0 owner) *)
 apply rcop3_trans_alt.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply legal_false_D; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply del_trans_alt; trivial.
Qed.

End ALT_PROP.

Section POS_PROP.

(* ou l'on montre que pour tout site autre que le proprietaire la
valeur de xi est toujours superieure ou egale a celle de yi, et en
sommant sur tous les sites et en utilisant le lemme four on en deduit
que le compteur du proprietaire est positif ou nul *)

Variable c0 : Config.

Hypothesis Hlegal : legal c0.

(* deux cas selon que le drapeau est actif ou non sur le site *)

Lemma le_xi_yi : forall s0 : Site, (xi c0 s0 >= yi c0 s0)%Z.
Proof.
(* Goal: forall s0 : Site, Z.ge (xi c0 s0) (yi c0 s0) *)
 intros; unfold xi, yi, ctrl_copy, ctrl_dec, ctrl_inc in |- *.
(* Goal: Z.ge (Z.add (Z.add (Int (rt c0 s0)) (card_mess copy (bm c0 owner s0))) (card_mess dec (bm c0 s0 owner))) (sigma Site LS (fun s' : Site => card_mess (inc_dec s') (bm c0 s0 owner))) *)
 generalize (pos_card_mess copy (bm c0 owner s0)); intros.
(* Goal: Z.ge (Z.add (Z.add (Int (rt c0 s0)) (card_mess copy (bm c0 owner s0))) (card_mess dec (bm c0 s0 owner))) (sigma Site LS (fun s' : Site => card_mess (inc_dec s') (bm c0 s0 owner))) *)
 generalize (legal_alternate s0 c0 Hlegal); intros.
(* Goal: Z.ge (Z.add (Z.add (Int (rt c0 s0)) (card_mess copy (bm c0 owner s0))) (card_mess dec (bm c0 s0 owner))) (sigma Site LS (fun s' : Site => card_mess (inc_dec s') (bm c0 s0 owner))) *)
 case (eq_bool_dec (rt c0 s0)); intro; rewrite e; unfold Int in |- *.
(* Goal: Z.ge (Z.add (Z.add (Zpos xH) (card_mess copy (bm c0 owner s0))) (card_mess dec (bm c0 s0 owner))) (sigma Site LS (fun s' : Site => card_mess (inc_dec s') (bm c0 s0 owner))) *)
(* Goal: Z.ge (Z.add (Z.add Z0 (card_mess copy (bm c0 owner s0))) (card_mess dec (bm c0 s0 owner))) (sigma Site LS (fun s' : Site => card_mess (inc_dec s') (bm c0 s0 owner))) *)
 generalize (alt_dec_inc (bm c0 s0 owner) H0); omega.

(* Goal: Z.ge (Z.add (Z.add Z0 (card_mess copy (bm c0 owner s0))) (card_mess dec (bm c0 s0 owner))) (sigma Site LS (fun s' : Site => card_mess (inc_dec s') (bm c0 s0 owner))) *)
 generalize (legal_false_D c0 s0 Hlegal e); intro.
(* Goal: Z.ge (Z.add (Z.add Z0 (card_mess copy (bm c0 owner s0))) (card_mess dec (bm c0 s0 owner))) (sigma Site LS (fun s' : Site => card_mess (inc_dec s') (bm c0 s0 owner))) *)
 generalize (D_dec_inc (bm c0 s0 owner) H0 H1); omega.
Qed.

Lemma le_sigma_xi_yi : (sigma_xi c0 >= sigma_yi c0)%Z.
Proof.
(* Goal: Z.ge (sigma_xi c0) (sigma_yi c0) *)
 unfold sigma_xi, sigma_yi in |- *; apply ge_sigma_sigma.
(* Goal: forall x : Site, Z.ge (xi c0 x) (yi c0 x) *)
 intros; apply le_xi_yi.
Qed.

Lemma st_owner_pos : (st c0 owner >= 0)%Z.
Proof.
(* Goal: Z.ge (st c0 owner) Z0 *)
 generalize (four c0 Hlegal); generalize le_sigma_xi_yi; omega.
Qed.

End POS_PROP.

Section ANC_RT.

(* ou l'on prouve que tout antecedent de la relation parent possede un
drapeau rt actif. pour cela on montre l'implication compteur positif
-> drapeau actif, puis on utilise le lemme two *)

Variable c0 : Config.

Hypothesis Hlegal : legal c0.

Lemma st_rt :
 forall s0 : Site, s0 <> owner -> (st c0 s0 > 0)%Z -> rt c0 s0 = true.
Proof.
(* Goal: forall (s0 : Site) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
 elim Hlegal.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply st_rt_init; trivial.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply copy_trans_st_rt; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rdec_trans_st_rt; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rinc_trans_st_rt; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rcop1_trans_st_rt; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rcop2_trans_st_rt; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply rcop3_trans_st_rt; auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply del_trans_st_rt; auto.
Qed.

Lemma parent_rt : forall s0 s1 : Site, parent c0 s1 s0 -> rt c0 s1 = true.
Proof.
(* Goal: forall (s0 s1 : Site) (_ : parent c0 s1 s0), @eq bool (rt c0 s1) true *)
 intros; elim H; intros; apply st_rt.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply (not_owner_inc c0 s2 s3 owner); trivial.

(* Goal: Z.gt (st c0 s2) Z0 *)
 rewrite two.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply sigma_ctrl_strct_pos with (s1 := s3); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 apply (not_owner_inc c0 s2 s3 owner); auto.
Qed.

Lemma ancestor_rt : forall s1 s2 : Site, ancestor c0 s2 s1 -> rt c0 s2 = true.
Proof.
(* Goal: forall (s1 s2 : Site) (_ : ancestor c0 s2 s1), @eq bool (rt c0 s2) true *)
 intros; elim H.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply parent_rt with (s0 := s3); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply parent_rt with (s0 := s3); trivial.
Qed.

End ANC_RT.

Section PARENT_CRESH.

(* ou l'on verifie que la relation parent est decidable, puis qu'elle
est croissante avec l'estampille et de ce fait bien fondee *)

Lemma in_queue_parent_dec :
 forall (c1 : Config) (s1 : Site),
 {s2 : Site | In_queue Message (inc_dec s2) (bm c1 s1 owner)} +
 {(forall s2 : Site, ~ In_queue Message (inc_dec s2) (bm c1 s1 owner))}.
Proof.
(* Goal: forall (c1 : Config) (s1 : Site), sumor (@sig Site (fun s2 : Site => In_queue Message (inc_dec s2) (bm c1 s1 owner))) (forall s2 : Site, not (In_queue Message (inc_dec s2) (bm c1 s1 owner))) *)
 intros; elim (bm c1 s1 owner).
(* Goal: sumor (@sig Site (fun s2 : Site => In_queue Message (inc_dec s2) (empty Message))) (forall s2 : Site, not (In_queue Message (inc_dec s2) (empty Message))) *)
(* Goal: forall (d : Message) (q : queue Message) (_ : sumor (@sig Site (fun s2 : Site => In_queue Message (inc_dec s2) q)) (forall s2 : Site, not (In_queue Message (inc_dec s2) q))), sumor (@sig Site (fun s2 : Site => In_queue Message (inc_dec s2) (input Message d q))) (forall s2 : Site, not (In_queue Message (inc_dec s2) (input Message d q))) *)
 right; intro; apply not_in_empty.

(* Goal: forall (d : Message) (q : queue Message) (_ : sumor (@sig Site (fun s2 : Site => In_queue Message (inc_dec s2) q)) (forall s2 : Site, not (In_queue Message (inc_dec s2) q))), sumor (@sig Site (fun s2 : Site => In_queue Message (inc_dec s2) (input Message d q))) (forall s2 : Site, not (In_queue Message (inc_dec s2) (input Message d q))) *)
 intros; case d; simpl in |- *.
(* Goal: sumor (@sig Site (fun s2 : Site => or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) (forall s2 : Site, not (or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) *)
 elim H; intro y.
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
 elim y; intros.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 left; exists x; auto.

(* Goal: sumor (@sig Site (fun s2 : Site => or (@eq Message (inc_dec s2) dec) (In_queue Message (inc_dec s2) q))) (forall s2 : Site, not (or (@eq Message (inc_dec s2) dec) (In_queue Message (inc_dec s2) q))) *)
(* Goal: forall s : Site, sumor (@sig Site (fun s2 : Site => or (@eq Message (inc_dec s2) (inc_dec s)) (In_queue Message (inc_dec s2) q))) (forall s2 : Site, not (or (@eq Message (inc_dec s2) (inc_dec s)) (In_queue Message (inc_dec s2) q))) *)
(* Goal: sumor (@sig Site (fun s2 : Site => or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) (forall s2 : Site, not (or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) *)
 right; intro; red in |- *; intros; elim H0; intro.
(* Goal: False *)
(* Goal: False *)
 discriminate H1.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 absurd (In_queue Message (inc_dec s2) q); auto.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 intros; left; split with s; auto.

(* Goal: sumor (@sig Site (fun s2 : Site => or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) (forall s2 : Site, not (or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) *)
 elim H; intro y.
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
 elim y; intros.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 left; split with x; auto.

(* Goal: sumor (@sig Site (fun s2 : Site => or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) (forall s2 : Site, not (or (@eq Message (inc_dec s2) copy) (In_queue Message (inc_dec s2) q))) *)
 right; intros; red in |- *; intros; elim H0; intro.
(* Goal: False *)
(* Goal: False *)
 discriminate H1.

(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 absurd (In_queue Message (inc_dec s2) q); auto.
Qed.

Lemma parent_dec :
 forall (c1 : Config) (s1 : Site),
 {s2 : Site | parent c1 s2 s1} + {(forall s2 : Site, ~ parent c1 s2 s1)}.
Proof.
(* Goal: forall (c1 : Config) (s1 : Site), sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
 intros; generalize (in_queue_parent_dec c1 s1); intro.
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
 elim H; intros y.
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
 elim y; intros.
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
 left; split with x.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply parent_intro; trivial.

(* Goal: sumor (@sig Site (fun s2 : Site => parent c1 s2 s1)) (forall s2 : Site, not (parent c1 s2 s1)) *)
 right; intro.
(* Goal: not (parent c1 s2 s1) *)
 red in |- *; intro.
(* Goal: False *)
 inversion H0.
(* Goal: D_queue (bm c s0 owner) *)
(* Goal: D_queue (bm (rec_copy1_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy2_trans c s2) s0 owner) *)
(* Goal: D_queue (bm (rec_copy3_trans c s1 s2) s0 owner) *)
(* Goal: D_queue (bm (delete_trans c s) s0 owner) *)
 absurd (In_queue Message (inc_dec s2) (bm c1 s1 owner)); auto.
Qed.

Lemma parent_cr :
 forall (c0 : Config) (s1 s2 : Site),
 legal c0 -> parent c0 s1 s2 -> dt c0 s1 < dt c0 s2.
Proof.
(* Goal: forall (c0 : Config) (s1 s2 : Site) (_ : legal c0) (_ : parent c0 s1 s2), lt (dt c0 s1) (dt c0 s2) *)
 intros c0 s1 s2 H; elim H.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply init_parent_cr; trivial.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall _ : parent c s1 s2, lt (dt c s1) (dt c s2)) (_ : parent (transition c t) s1 s2), lt (dt (transition c t) s1) (dt (transition c t) s2) *)
 simple induction t; unfold transition in |- *; intros.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply copy_trans_parent_cr; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rdec_trans_parent_cr; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rinc_trans_parent_cr; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rcop1_trans_parent_cr; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply rcop2_trans_parent_cr; trivial.

(* Goal: lt (dt (rec_copy3_trans c s0 s3) s1) (dt (rec_copy3_trans c s0 s3) s2) *)
(* Goal: lt (dt (delete_trans c s) s1) (dt (delete_trans c s) s2) *)
 apply rcop3_trans_parent_cr.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply (first_copy_diff_site c); trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: forall (s1 s2 : Site) (_ : ancestor c s2 s1), @eq bool (rt c s2) true *)
(* Goal: forall s0 : Site, le (dt c s0) (time c) *)
(* Goal: forall _ : parent c s1 s2, lt (dt c s1) (dt c s2) *)
(* Goal: parent (rec_copy3_trans c s0 s3) s1 s2 *)
(* Goal: lt (dt (delete_trans c s) s1) (dt (delete_trans c s) s2) *)
 exact (ancestor_rt c H0).

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply le_dt_time; trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 apply del_trans_parent_cr; trivial.
Qed.

Lemma wf_parent : forall c0 : Config, legal c0 -> well_founded (parent c0).
Proof.
(* Goal: forall (c0 : Config) (_ : legal c0), @well_founded Site (parent c0) *)
 intros; apply wf_R with (f := dt c0).
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply parent_cr; trivial.
Qed.

End PARENT_CRESH.

Section SAFETY.

(* ou l'on verifie que si un site different du proprietaire est actif
(drapeau rt) alors le compteur du proprietaire est strictement
positif. On utilise pour cela la relation parent, en remontant a la
racine depuis le site actif. Cette racine se caracterise par un yi nul
(il n'y a pas de message inc_dec dans sa file avec le proprietaire) et
un xi strictement positif car son drapeau est actif. En sommant tous
les xi-yi on obtient donc une valeur strictement positive pour le
compteur du proprietaire *)

Variable c0 : Config.

Hypothesis Hlegal : legal c0.

Variable s0 : Site.

Hypothesis s0_not_owner : s0 <> owner.

Hypothesis access_so : rt c0 s0 = true.

Definition root_parent :=
  root Site (dt c0) (parent c0) (parent_dec c0)
    (fun s1 s2 : Site => parent_cr c0 s1 s2 Hlegal).

Lemma root_no_parent : forall y : Site, ~ parent c0 y (root_parent s0).
Proof.
(* Goal: forall y : Site, not (parent c0 y (root_parent s0)) *)
 intro; unfold root_parent in |- *; apply root_no_R.
Qed.

Lemma rt_root : rt c0 (root_parent s0) = true.
Proof.
(* Goal: @eq bool (rt c0 (root_parent s0)) true *)
 unfold root_parent in |- *; apply prop_root.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 trivial.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intros; apply parent_rt with (s0 := y); trivial.
Qed.

Lemma pos_root_xi : (xi c0 (root_parent s0) > 0)%Z.
Proof.
(* Goal: Z.gt (xi c0 (root_parent s0)) Z0 *)
 unfold xi in |- *; rewrite rt_root; unfold Int in |- *.
(* Goal: Z.gt (Z.add (Z.add (Zpos xH) (ctrl_copy owner (root_parent s0) (bm c0))) (ctrl_dec owner (root_parent s0) (bm c0))) Z0 *)
 generalize (ctrl_copy_pos (bm c0) owner (root_parent s0)).
(* Goal: forall _ : Z.ge (ctrl_copy owner (root_parent s0) (bm c0)) Z0, Z.gt (Z.add (Z.add (Zpos xH) (ctrl_copy owner (root_parent s0) (bm c0))) (ctrl_dec owner (root_parent s0) (bm c0))) Z0 *)
 generalize (ctrl_dec_pos (bm c0) owner (root_parent s0)).
(* Goal: forall (_ : Z.ge (ctrl_dec owner (root_parent s0) (bm c0)) Z0) (_ : Z.ge (ctrl_copy owner (root_parent s0) (bm c0)) Z0), Z.gt (Z.add (Z.add (Zpos xH) (ctrl_copy owner (root_parent s0) (bm c0))) (ctrl_dec owner (root_parent s0) (bm c0))) Z0 *)
 omega.
Qed.

Lemma root_no_in_queue_inc :
 forall y : Site,
 ~ In_queue Message (inc_dec y) (bm c0 (root_parent s0) owner).
Proof.
(* Goal: not (parent c1 s2 s1) *)
 intro; red in |- *; intro.
(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 elim (root_no_parent y); apply parent_intro; trivial.
Qed.

Lemma null_root_ctrl_inc :
 (fun s : Site => ctrl_inc s (root_parent s0) (bm c0)) =
 (fun s : Site => 0%Z).
Proof.
(* Goal: @eq (forall _ : Site, Z) (fun s : Site => ctrl_inc s (root_parent s0) (bm c0)) (fun _ : Site => Z0) *)
 apply funct_eq; intro.
(* Goal: @eq Z (ctrl_inc e (root_parent s0) (bm c0)) Z0 *)
 unfold ctrl_inc, card_mess in |- *; apply card_null.
(* Goal: not (In_queue Message (inc_dec e) (bm c0 (root_parent s0) owner)) *)
 apply root_no_in_queue_inc.
Qed.

Lemma null_root_yi : yi c0 (root_parent s0) = 0%Z.
Proof.
(* Goal: @eq Z (yi c0 (root_parent s0)) Z0 *)
 unfold yi in |- *; rewrite null_root_ctrl_inc; apply sigma_null.
Qed.

Lemma lt_root_xi_yi : (xi c0 (root_parent s0) > yi c0 (root_parent s0))%Z.
Proof.
(* Goal: Z.gt (xi c0 (root_parent s0)) (yi c0 (root_parent s0)) *)
 rewrite null_root_yi; exact pos_root_xi.
Qed.

Lemma lt_sigma_xi_yi : (sigma_xi c0 > sigma_yi c0)%Z.
Proof.
(* Goal: Z.gt (sigma_xi c0) (sigma_yi c0) *)
 apply Zlt_gt; unfold sigma_xi, sigma_yi in |- *; apply lt_sigma_sigma.

(* Goal: @eq bool (rt c0 s0) true *)
(* Goal: forall (y z : Site) (_ : @eq bool (rt c0 y) true) (_ : parent c0 z y), @eq bool (rt c0 z) true *)
 intro; apply Zge_le; apply le_xi_yi; trivial.

(* Goal: @ex Site (fun y : Site => and (Z.lt (yi c0 y) (xi c0 y)) (@List.In Site y LS)) *)
 exists (root_parent s0); split.
(* Goal: Z.lt (yi c0 (root_parent s0)) (xi c0 (root_parent s0)) *)
(* Goal: @List.In Site (root_parent s0) LS *)
 apply Zgt_lt; apply lt_root_xi_yi.

(* Goal: @List.In Site (root_parent s0) LS *)
 apply in_s_LS.
Qed.

Lemma pos_st_owner : (st c0 owner > 0)%Z.
Proof.
(* Goal: forall (_ : Z.ge (ctrl_dec owner (root_parent s0) (bm c0)) Z0) (_ : Z.ge (ctrl_copy owner (root_parent s0) (bm c0)) Z0), Z.gt (Z.add (Z.add (Zpos xH) (ctrl_copy owner (root_parent s0) (bm c0))) (ctrl_dec owner (root_parent s0) (bm c0))) Z0 *)
 generalize (four c0 Hlegal); generalize lt_sigma_xi_yi; omega.
Qed.

End SAFETY.
