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


Require Export DistributedReferenceCounting.machine4.invariant5.
Require Export DistributedReferenceCounting.machine4.invariant7.

Unset Standard Proposition Elimination Names.

(* changes:
   In safety1 and safety2, I had to use 
   sigma_but_strictly_positive, instead of sigma_strictly_positive.

   In safety2, the case ~s2=owner should not be isolated
*)


Lemma direct_son_is_positive :
 forall c : Config,
 legal c ->
 forall s : Site,
 direct_son c s ->
 (Int (rt c s) + reduce Message dec_count (bm c s owner) +
  reduce Message copy_count (bm c owner s) -
  reduce Message new_inc_count (bm c s owner) > 0)%Z.


Proof.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Int (rt c s)) (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  elim H0.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Int (rt c s0)) (reduce Message dec_count (bm c s0 owner))) (reduce Message copy_count (bm c owner s0))) (reduce Message new_inc_count (bm c s0 owner))) Z0 *)
  rewrite H2; unfold Int in |- *.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Zpos xH) (reduce Message dec_count (bm c s0 owner))) (reduce Message copy_count (bm c owner s0))) (reduce Message new_inc_count (bm c s0 owner))) Z0 *)
  generalize (not_inc_dec_in (bm c s0 owner) H3); intro.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Zpos xH) (reduce Message dec_count (bm c s0 owner))) (reduce Message copy_count (bm c owner s0))) (reduce Message new_inc_count (bm c s0 owner))) Z0 *)
  generalize (copy_count_is_positive (bm c owner s0)).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (dec_count_is_positive (bm c s0 owner)); intro.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Zpos xH) (reduce Message dec_count (bm c s0 owner))) (reduce Message copy_count (bm c owner s0))) (reduce Message new_inc_count (bm c s0 owner))) Z0 *)
  cut (reduce Message new_inc_count (bm c s0 owner) = 0%Z).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: @eq Z (reduce Message new_inc_count (bm c s0 owner)) Z0 *)
  generalize H4.
(* Goal: forall _ : forall s : Site, not (In_queue Message (inc_dec s) (bm c s0 owner)), @eq Z (reduce Message new_inc_count (bm c s0 owner)) Z0 *)
  elim (bm c s0 owner).
(* Goal: forall _ : forall s : Site, not (In_queue Message (inc_dec s) (empty Message)), @eq Z (reduce Message new_inc_count (empty Message)) Z0 *)
(* Goal: forall (d : Message) (q : queue Message) (_ : forall _ : forall s : Site, not (In_queue Message (inc_dec s) q), @eq Z (reduce Message new_inc_count q) Z0) (_ : forall s : Site, not (In_queue Message (inc_dec s) (input Message d q))), @eq Z (reduce Message new_inc_count (input Message d q)) Z0 *)
  simpl in |- *; auto.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : forall s : Site, not (In_queue Message (inc_dec s) q), @eq Z (reduce Message new_inc_count q) Z0) (_ : forall s : Site, not (In_queue Message (inc_dec s) (input Message d q))), @eq Z (reduce Message new_inc_count (input Message d q)) Z0 *)
  case d.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (empty Message))) (reduce Message copy_count (empty Message))) (reduce Message new_inc_count (empty Message)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  simpl in |- *.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: @eq Z (Z.add (reduce Message new_inc_count q) Z0) Z0 *)
  rewrite H7.
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: not (In_queue Message (inc_dec s1) q) *)
  generalize (H8 s1).
(* Goal: forall _ : not (or (@eq Message (inc_dec s1) copy) (In_queue Message (inc_dec s1) q)), not (In_queue Message (inc_dec s1) q) *)
  intuition.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (empty Message))) (reduce Message copy_count (empty Message))) (reduce Message new_inc_count (empty Message)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  elim (H8 s1); simpl in |- *.
(* Goal: not (@eq Site s1 owner) *)
  left; auto.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  simpl in |- *; intros.
(* Goal: @eq Z (Z.add (reduce Message new_inc_count q) Z0) Z0 *)
  rewrite H7.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: not (In_queue Message (inc_dec s1) q) *)
  generalize (H8 s1).
(* Goal: forall _ : not (or (@eq Message (inc_dec s1) copy) (In_queue Message (inc_dec s1) q)), not (In_queue Message (inc_dec s1) q) *)
  intuition.
Qed.

Remark add_reduce : forall x : Z, (x > 0)%Z -> (x + 1 - 1 > 0)%Z.
Proof.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro; omega.
Qed.

Lemma safety1 :
 forall c : Config,
 legal c ->
 forall s : Site, s <> owner -> rt c s = true -> (st c owner > 0)%Z.

Proof.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: Z.gt (st c owner) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite (invariant4 c H).
(* Goal: Z.gt (Z.sub (Z.sub (Z.add (Z.add (sigma_receive_table (rt c)) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite other_definition_for_sigma_receive_table.
(* Goal: Z.gt (Z.sub (Z.sub (Z.add (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite <- sigma_same_table.
(* Goal: Z.gt (Z.sub (Z.sub (Z.add (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite <- sigma_same_table.
(* Goal: Z.gt (Z.sub (Z.sub (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite <- sigma_same_table2.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (Z_id Site) (fun_minus Site (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold Z_id in |- *.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun_minus Site (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold fun_minus in |- *.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2)) a) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold fun_sum in |- *.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite sigma_sigma_but_owner.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int (rt c owner)) (reduce Message dec_count (bm c owner owner))) (reduce Message copy_count (bm c owner owner))) (reduce Message new_inc_count (bm c owner owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite owner_rt_true.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (bm c owner owner))) (reduce Message copy_count (bm c owner owner))) (reduce Message new_inc_count (bm c owner owner)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite empty_q_to_me.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (empty Message))) (reduce Message copy_count (empty Message))) (reduce Message new_inc_count (empty Message)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  simpl in |- *.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (empty Message))) (reduce Message copy_count (empty Message))) (reduce Message new_inc_count (empty Message)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  simpl in |- *.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  elim (direct_or_indirect_son1 c s H0 H1); intro.
(* Goal: Z.gt (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold sigma_table_but_owner in |- *.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  apply add_reduce.
(* Goal: Z.gt (sigma_but Site owner eq_site_dec LS (fun s : Site => Z.sub (Z.add (Z.add (Int (rt c s)) (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner)))) Z0 *)
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  apply sigma_but_strictly_positive with (x := s).
(* Goal: @List.In Site s2 LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s1 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply in_s_LS.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  intro; apply invariant5; auto.
  
(* Goal: not (@eq Site s1 owner) *)
  apply direct_son_is_positive; auto.
  
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  apply add_reduce.
(* Goal: Z.gt (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  elim (parent_invariant c H s b).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: Z.gt (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  decompose [and] H2.
(* Goal: Z.gt (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold sigma_table_but_owner in |- *.
(* Goal: Z.gt (sigma_but Site owner eq_site_dec LS (fun s : Site => Z.sub (Z.add (Z.add (Int (rt c s)) (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  apply sigma_but_strictly_positive with (x := x).
(* Goal: @List.In Site s2 LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s1 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply in_s_LS.
  
(* Goal: not (@eq Site x owner) *)
(* Goal: forall y : Site, Z.ge (Z.sub (Z.add (Z.add (Int (rt c y)) (reduce Message dec_count (bm c y owner))) (reduce Message copy_count (bm c owner y))) (reduce Message new_inc_count (bm c y owner))) Z0 *)
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Int (rt c x)) (reduce Message dec_count (bm c x owner))) (reduce Message copy_count (bm c owner x))) (reduce Message new_inc_count (bm c x owner))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  elim H3.
(* Goal: not (@eq Site s1 owner) *)
  intros; auto.
  
(* Goal: not (@eq Site s1 owner) *)
  intro; apply invariant5; auto.
  
(* Goal: not (@eq Site s1 owner) *)
  apply direct_son_is_positive; auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
Qed.


Lemma safety2 :
 forall c : Config,
 legal c ->
 forall s1 s2 : Site,
 In_queue Message copy (bm c s1 s2) -> (st c owner > 0)%Z.
Proof.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  elim (decide_inc_dec_in_queue c s2); intro.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  elim a; intros.
(* Goal: Z.gt (st c owner) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  apply safety1 with (s := x).
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site x owner) *)
(* Goal: @eq bool (rt c x) true *)
(* Goal: Z.gt (st c owner) Z0 *)
  apply (not_owner_inc3 c s2 owner H x).
(* Goal: not (@eq Site s1 owner) *)
  apply inc_dec_in; auto.
  
(* Goal: @eq bool (rt c x) true *)
(* Goal: Z.gt (st c owner) Z0 *)
  generalize (inc_dec_in x (bm c s2 owner) p).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: @eq bool (rt c x) true *)
(* Goal: Z.gt (st c owner) Z0 *)
  generalize (not_owner_inc3 c s2 owner H x H1).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: @eq bool (rt c x) true *)
(* Goal: Z.gt (st c owner) Z0 *)
  generalize (positive_st c x s2 H2 H H1).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: @eq bool (rt c x) true *)
(* Goal: Z.gt (st c owner) Z0 *)
  generalize (st_rt c x H H2 H3).
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  case (eq_site_dec s1 owner); intro.
(* Goal: Z.gt (st c owner) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite (invariant4 c H).
(* Goal: Z.gt (Z.sub (Z.sub (Z.add (Z.add (sigma_receive_table (rt c)) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite other_definition_for_sigma_receive_table.
(* Goal: Z.gt (Z.sub (Z.sub (Z.add (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite <- sigma_same_table.
(* Goal: Z.gt (Z.sub (Z.sub (Z.add (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite <- sigma_same_table.
(* Goal: Z.gt (Z.sub (Z.sub (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite <- sigma_same_table2.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (Z_id Site) (fun_minus Site (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold Z_id in |- *.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun_minus Site (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold fun_minus in |- *.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2)) a) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold fun_sum in |- *.
(* Goal: Z.gt (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite sigma_sigma_but_owner.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int (rt c owner)) (reduce Message dec_count (bm c owner owner))) (reduce Message copy_count (bm c owner owner))) (reduce Message new_inc_count (bm c owner owner)))) (Zpos xH)) Z0 *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite owner_rt_true.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (bm c owner owner))) (reduce Message copy_count (bm c owner owner))) (reduce Message new_inc_count (bm c owner owner)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite empty_q_to_me.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (empty Message))) (reduce Message copy_count (empty Message))) (reduce Message new_inc_count (empty Message)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  simpl in |- *.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  apply add_reduce.
(* Goal: Z.gt (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold sigma_table_but_owner in |- *.
(* Goal: Z.gt (sigma_but Site owner eq_site_dec LS (fun s : Site => Z.sub (Z.add (Z.add (Int (rt c s)) (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  apply sigma_but_strictly_positive with (x := s2).
(* Goal: @List.In Site s2 LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s1 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply in_s_LS.
  
(* Goal: not (@eq Site s2 owner) *)
(* Goal: forall y : Site, Z.ge (Z.sub (Z.add (Z.add (Int (rt c y)) (reduce Message dec_count (bm c y owner))) (reduce Message copy_count (bm c owner y))) (reduce Message new_inc_count (bm c y owner))) Z0 *)
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Int (rt c s2)) (reduce Message dec_count (bm c s2 owner))) (reduce Message copy_count (bm c owner s2))) (reduce Message new_inc_count (bm c s2 owner))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold not in |- *; intro; generalize H0.
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (empty Message))) (reduce Message copy_count (empty Message))) (reduce Message new_inc_count (empty Message)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  rewrite e; rewrite H1; rewrite empty_q_to_me; simpl in |- *.
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  intro; apply invariant5; auto.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (dec_count_is_positive (bm c s2 owner)); intro.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Int (rt c s2)) (reduce Message dec_count (bm c s2 owner))) (reduce Message copy_count (bm c owner s2))) (reduce Message new_inc_count (bm c s2 owner))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  cut (Int (rt c s2) >= 0)%Z.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Int (rt c s2)) (reduce Message dec_count (bm c s2 owner))) (reduce Message copy_count (bm c owner s2))) (reduce Message new_inc_count (bm c s2 owner))) Z0 *)
(* Goal: Z.ge (Int (rt c s2)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  cut (reduce Message new_inc_count (bm c s2 owner) = 0%Z).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: Z.gt (Z.sub (Z.add (Z.add (Int (rt c s2)) (reduce Message dec_count (bm c s2 owner))) (reduce Message copy_count (bm c owner s2))) (reduce Message new_inc_count (bm c s2 owner))) Z0 *)
(* Goal: @eq Z (reduce Message new_inc_count (bm c s2 owner)) Z0 *)
(* Goal: Z.ge (Int (rt c s2)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  cut (reduce Message copy_count (bm c owner s2) > 0)%Z.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: Z.gt (reduce Message (rooted_fun s1 s1 s2) (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply reduce_in_queue_strictly_positive with (x := copy).
(* Goal: forall a : Message, Z.ge (copy_count a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (copy_count copy) Z0 *)
(* Goal: In_queue Message copy (bm c owner s2) *)
(* Goal: @eq Z (reduce Message new_inc_count (bm c s2 owner)) Z0 *)
(* Goal: Z.ge (Int (rt c s2)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  intro; unfold copy_count in |- *.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  case a; intros.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  exact eq_message_dec.
  
(* Goal: Z.gt (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (empty Message))) (reduce Message copy_count (empty Message))) (reduce Message new_inc_count (empty Message)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold copy_count in |- *; simpl in |- *.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: not (@eq Site s1 owner) *)
  rewrite <- e; auto.
  
(* Goal: @eq Z (reduce Message new_inc_count (bm c s2 owner)) Z0 *)
(* Goal: Z.ge (Int (rt c s2)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  generalize (not_inc_dec_in (bm c s2 owner) b).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: @eq Z (reduce Message new_inc_count (bm c s2 owner)) Z0 *)
(* Goal: Z.ge (Int (rt c s2)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  apply reduce_in_queue_null.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  case x; simpl in |- *; intros.
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  elim (H3 s); auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: Z.ge (Int (rt c s2)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  unfold Int in |- *.
(* Goal: Z.ge (if rt c s2 then Zpos xH else Z0) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: Z.gt (st c owner) Z0 *)
  case (eq_bool_dec (rt c s2)).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  rewrite e0; simpl in |- *; omega.
  
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro; rewrite e0; simpl in |- *; omega.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: Z.gt (st c owner) Z0 *)
  apply safety1 with (s := s1).
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: @eq bool (rt c s1) true *)
  apply st_rt.
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: Z.gt (st c s1) Z0 *)
  rewrite invariant2.
(* Goal: Z.gt (sigma_rooted s1 (bm c)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  unfold sigma_rooted in |- *.
(* Goal: Z.gt (sigma2_table Site LS LS (queue Message) (rooted s1) (bm c)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply sigma2_strictly_positive with (x := s1) (y := s2).
(* Goal: eq_dec Site *)
(* Goal: @List.In Site s1 LS *)
(* Goal: @List.In Site s2 LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s1 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  exact eq_site_dec.
  
(* Goal: @List.In Site s2 LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s1 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply in_s_LS.
  
(* Goal: @List.In Site s2 LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s1 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply in_s_LS.
  
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  unfold rooted in |- *; intros.
(* Goal: Z.ge (reduce Message (rooted_fun s1 x' y') (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply reduce_positive_or_null.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intros.
(* Goal: Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply rooted_fun_positive_or_null.
  
(* Goal: Z.gt (rooted s1 s1 s2 (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  unfold rooted in |- *.
(* Goal: Z.gt (reduce Message (rooted_fun s1 s1 s2) (bm c s1 s2)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply reduce_in_queue_strictly_positive with (x := copy).
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  intro.
(* Goal: Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  apply rooted_fun_positive_or_null.
  
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  exact eq_message_dec.
  
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  unfold rooted_fun in |- *.
(* Goal: forall a : Message, Z.ge (rooted_fun s1 s1 s2 a) Z0 *)
(* Goal: eq_dec Message *)
(* Goal: Z.gt (rooted_fun s1 s1 s2 copy) Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  case (eq_site_dec s1 s1); intro.
(* Goal: Z.gt (Zpos xH) Z0 *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  omega.
  
(* Goal: Z.gt Z0 Z0 *)
(* Goal: In_queue Message copy (bm c s1 s2) *)
(* Goal: legal c *)
(* Goal: not (@eq Site s1 owner) *)
  elim n0.
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
  
(* Goal: not (@eq Site s1 owner) *)
  auto.
Qed.
