(* 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.machine3.machine.
Require Export DistributedReferenceCounting.machine3.cardinal.
Require Export DistributedReferenceCounting.machine3.comm.
Require Export DistributedReferenceCounting.machine3.still_to_prove.

Unset Standard Proposition Elimination Names.

Section ROOTED.

Variable s0 : Site.

Definition rooted_fun (s1 s2 : Site) (m : Message) :=
  match m with
  | copy => if eq_site_dec s1 s0 then 1%Z else 0%Z
  | dec => if eq_site_dec s2 s0 then 1%Z else 0%Z
  | inc_dec s3 =>
      if eq_site_dec s3 s0
      then
       if eq_site_dec s2 owner then 1%Z else 0%Z
      else 0%Z
  end.

Definition rooted (s1 s2 : Site) (q : queue Message) :=
  reduce Message (rooted_fun s1 s2) q.


Definition sigma_rooted (bm : Bag_of_message) :=
  sigma2_table Site LS LS (queue Message) rooted bm.

End ROOTED.



Section ROOTED1.



Lemma sigma_rooted_post_message :
 forall (m : Message) (s0 s1 s2 : Site) (b : Bag_of_message),
 s0 <> owner ->
 sigma_rooted s0 (Post_message Message m b s1 s2) =
 (sigma_rooted s0 b + rooted_fun s0 s1 s2 m)%Z.
Proof.
(* Goal: forall _ : In_queue Message (inc_dec s0) (bm c s5 owner), Z.gt (sigma_rooted s0 (bm c)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  unfold sigma_rooted in |- *.
(* Goal: forall (m : Message) (s0 s1 s2 : Site) (b : Bag_of_message) (_ : not (@eq Site s0 owner)), @eq Z (sigma2_table Site LS LS (queue Message) (rooted s0) (Post_message Message m b s1 s2)) (Z.add (sigma2_table Site LS LS (queue Message) (rooted s0) b) (rooted_fun s0 s1 s2 m)) *)
  unfold Post_message in |- *.
(* Goal: forall (m : Message) (s0 s1 s2 : Site) (b : Bag_of_message) (_ : not (@eq Site s0 owner)), @eq Z (sigma2_table Site LS LS (queue Message) (rooted s0) (change_queue (queue Message) b s1 s2 (input Message m (b s1 s2)))) (Z.add (sigma2_table Site LS LS (queue Message) (rooted s0) b) (rooted_fun s0 s1 s2 m)) *)
  unfold change_queue in |- *.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (rooted s0) (update2_table Site eq_site_dec (queue Message) b s1 s2 (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (rooted s0) b) (rooted_fun s0 s1 s2 m)) *)
  rewrite sigma_table2_change.
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
Qed.


Lemma rooted_first_out :
 forall (s0 s1 s2 : Site) (q : queue Message) (m : Message),
 first Message q = value Message m ->
 rooted s0 s1 s2 (first_out Message q) =
 (rooted s0 s1 s2 q - rooted_fun s0 s1 s2 m)%Z.
Proof.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: Z.ge (rooted s0 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted in |- *.
(* Goal: @eq Z (reduce Message (rooted_fun s0 s1 s2) (first_out Message q)) (Z.sub (reduce Message (rooted_fun s0 s1 s2) q) (rooted_fun s0 s1 s2 m)) *)
  apply reduce_first_out.
(* Goal: not (@eq Site s0 owner) *)
  auto.
Qed.

Lemma sigma_rooted_collect_message :
 forall (m : Message) (s0 s1 s2 : Site) (b : Bag_of_message),
 first Message (b s1 s2) = value Message m ->
 s0 <> owner ->
 sigma_rooted s0 (Collect_message Message b s1 s2) =
 (sigma_rooted s0 b - rooted_fun s0 s1 s2 m)%Z.
Proof.
(* Goal: forall (m : Message) (s0 s1 s2 : Site) (b : Bag_of_message) (_ : @eq (exc Message) (first Message (b s1 s2)) (value Message m)) (_ : not (@eq Site s0 owner)), @eq Z (sigma_rooted s0 (Collect_message Message b s1 s2)) (Z.sub (sigma_rooted s0 b) (rooted_fun s0 s1 s2 m)) *)
  unfold sigma_rooted, Collect_message, change_queue in |- *.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (rooted s0) (update2_table Site eq_site_dec (queue Message) b s1 s2 (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (rooted s0) b) (rooted_fun s0 s1 s2 m)) *)
  rewrite sigma_table2_change.
(* Goal: @eq Z (Z.add (Z.sub (sigma2_table Site LS LS (queue Message) (rooted s0) b) (rooted s0 s1 s2 (b s1 s2))) (rooted s0 s1 s2 (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (rooted s0) b) (rooted_fun s0 s1 s2 m)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  rewrite (rooted_first_out s0 s1 s2 (b s1 s2) m).
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
Qed.

Lemma rooted_fun_positive_or_null :
 forall (s0 x y : Site) (a : Message), (rooted_fun s0 x y a >= 0)%Z.
Proof.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: Z.ge match a with | dec => if eq_site_dec y s0 then Zpos xH else Z0 | inc_dec s3 => if eq_site_dec s3 s0 then if eq_site_dec y owner then Zpos xH else Z0 else Z0 | copy => if eq_site_dec x s0 then Zpos xH else Z0 end Z0 *)
  elim a.
(* Goal: Z.ge (if eq_site_dec y s0 then Zpos xH else Z0) Z0 *)
(* Goal: forall s : Site, Z.ge (if eq_site_dec s s0 then if eq_site_dec y owner then Zpos xH else Z0 else Z0) Z0 *)
(* Goal: Z.ge (if eq_site_dec x s0 then Zpos xH else Z0) Z0 *)
  case (eq_site_dec y s0).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec s s0).
(* Goal: forall _ : @eq Site s s0, Z.ge (if eq_site_dec y owner then Zpos xH else Z0) Z0 *)
(* Goal: forall _ : not (@eq Site s s0), Z.ge Z0 Z0 *)
(* Goal: Z.ge (if eq_site_dec x s0 then Zpos xH else Z0) Z0 *)
  case (eq_site_dec y owner).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
(* Goal: Z.ge (if eq_site_dec x s0 then Zpos xH else Z0) Z0 *)
  case (eq_site_dec x s0).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
Qed.

Lemma rooted_positive_or_null :
 forall (s0 x y : Site) (q : queue Message), (rooted s0 x y q >= 0)%Z.
Proof.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: Z.ge (rooted s0 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted in |- *.
(* Goal: Z.ge (reduce Message (rooted_fun s0 x' y') (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  apply reduce_positive_or_null.
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.ge (rooted_fun s0 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  apply rooted_fun_positive_or_null.
Qed.




Axiom
  sigma_rooted_change_queue :
    forall (s0 s1 s2 : Site) (b : Bag_of_message) (q : queue Message),
    s0 <> owner ->
    b s1 owner = input Message dec (input Message (inc_dec s2) q) ->
    sigma_rooted s0 (change_queue (queue Message) b s1 owner q) =
    (sigma_rooted s0 b - rooted_fun s0 s1 owner dec -
     rooted_fun s0 s1 owner (inc_dec s2))%Z.



End ROOTED1.

Section INVARIANT2.

Lemma invariant2_init :
 forall s0 : Site, st config_init s0 = sigma_rooted s0 (bm config_init).
Proof.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq Z (send_init s0) (sigma_rooted s0 bag_init) *)
  unfold send_init, sigma_rooted, bag_init in |- *.
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (rooted s0) (fun _ _ : Site => empty Message)) *)
  unfold sigma2_table in |- *.
(* Goal: @eq Z Z0 (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (rooted s0 s1) (fun _ : Site => empty Message))) *)
  unfold sigma_table in |- *.
(* Goal: @eq Z Z0 (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun s1 : Site => rooted s0 s s1 (empty Message))))) *)
  unfold Z_id in |- *.
(* Goal: Z.ge (rooted s0 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted in |- *.
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq Z Z0 (sigma Site LS (fun _ : Site => Z0)) *)
  rewrite sigma_null.
(* Goal: @eq Z Z0 (sigma Site LS (fun _ : Site => Z0)) *)
  rewrite sigma_null.
(* Goal: not (@eq Site s0 owner) *)
  auto.
Qed.

Lemma invariant2_ind :
 forall s0 : Site,
 s0 <> owner ->
 forall (c : Config) (t : class_trans c),
 legal c ->
 st c s0 = sigma_rooted s0 (bm c) ->
 st (transition c t) s0 = sigma_rooted s0 (bm (transition c t)).
Proof.
(* Goal: forall (s0 : Site) (_ : not (@eq Site s0 owner)) (c : Config) (t : class_trans c) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c t) s0) (sigma_rooted s0 (bm (transition c t))) *)
  simple induction t.

  (* 1 *)

(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (st c s0) (sigma_rooted s0 (Post_message Message dec (change_queue (queue Message) (bm c) s1 owner q) s1 s2)) *)
  rewrite sigma_rooted_post_message.
(* Goal: @eq Z (Inc_send_table (st c) s1 s0) (Z.add (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 s2 copy)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_dec c s1 s2 e)) s0) (sigma_rooted s0 (bm (transition c (receive_dec c s1 s2 e)))) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  unfold Inc_send_table in |- *.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) (if eq_site_dec s1 s0 then Zpos xH else Z0)) (if eq_site_dec s1 s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  case (eq_site_dec s1 s0).
(* Goal: forall _ : @eq Site s1 s0, @eq Z (update_table Site eq_site_dec Z (st c) s1 (Z.add (st c s1) (Zpos xH)) s0) (Z.add (sigma_rooted s0 (bm c)) (Zpos xH)) *)
(* Goal: forall _ : not (@eq Site s1 s0), @eq Z (update_table Site eq_site_dec Z (st c) s1 (Z.add (st c s1) (Zpos xH)) s0) (Z.add (sigma_rooted s0 (bm c)) Z0) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_dec c s1 s2 e)) s0) (sigma_rooted s0 (bm (transition c (receive_dec c s1 s2 e)))) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  intro; rewrite e.
(* Goal: @eq Z (update_table Site eq_site_dec Z (st c) s0 (Z.sub (st c s0) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) (Zpos xH)) *)
(* Goal: forall _ : not (@eq Site s2 s0), @eq Z (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) Z0) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  unfold update_table in |- *; rewrite here.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: forall _ : not (@eq Site s1 s0), @eq Z (update_table Site eq_site_dec Z (st c) s1 (Z.add (st c s1) (Zpos xH)) s0) (Z.add (sigma_rooted s0 (bm c)) Z0) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_dec c s1 s2 e)) s0) (sigma_rooted s0 (bm (transition c (receive_dec c s1 s2 e)))) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  intro; unfold update_table in |- *; rewrite elsewhere.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.

  (* 2 *)
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (Dec_send_table (st c) s2 s0) (sigma_rooted s0 (Collect_message Message (bm c) s1 s2)) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite sigma_rooted_collect_message with (m := dec).
(* Goal: @eq Z (Dec_send_table (st c) s2 s0) (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  unfold Dec_send_table in |- *.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: @eq Z (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) (if eq_site_dec s2 s0 then Zpos xH else Z0)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  case (eq_site_dec s2 s0).
(* Goal: forall _ : @eq Site s2 s0, @eq Z (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) (Zpos xH)) *)
(* Goal: forall _ : not (@eq Site s2 s0), @eq Z (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) Z0) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  intro; rewrite e0.
(* Goal: @eq Z (update_table Site eq_site_dec Z (st c) s0 (Z.sub (st c s0) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) (Zpos xH)) *)
(* Goal: forall _ : not (@eq Site s2 s0), @eq Z (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) Z0) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  unfold update_table in |- *; rewrite here.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: forall _ : not (@eq Site s2 s0), @eq Z (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) (Z.sub (sigma_rooted s0 (bm c)) Z0) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_inc c s1 s3 e)) s0) (sigma_rooted s0 (bm (transition c (receive_inc c s1 s3 e)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  intros; unfold update_table in |- *; rewrite elsewhere.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.

  (* 3 *)
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (st c s0) (sigma_rooted s0 (Post_message Message dec (change_queue (queue Message) (bm c) s1 owner q) s1 s2)) *)
  rewrite sigma_rooted_post_message.
(* Goal: @eq Z (Inc_send_table (st c) owner s0) (Z.add (sigma_rooted s0 (Collect_message Message (bm c) s1 owner)) (rooted_fun s0 owner s3 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite sigma_rooted_collect_message with (m := inc_dec s3).
(* Goal: @eq Z (Inc_send_table (st c) owner s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner (inc_dec s3))) (rooted_fun s0 owner s3 dec)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  unfold Inc_send_table, rooted_fun in |- *.
(* Goal: @eq Z (update_table Site eq_site_dec Z (st c) owner (Z.add (st c owner) (Zpos xH)) s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) (if eq_site_dec s3 s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) (if eq_site_dec s3 s0 then Zpos xH else Z0)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  unfold update_table in |- *; rewrite elsewhere.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) (if eq_site_dec s3 s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) (if eq_site_dec s3 s0 then Zpos xH else Z0)) *)
(* Goal: not (@eq Site owner s0) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy1 c s1 s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy1 c s1 s2 e e0)))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy2 c s2 e e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy2 c s2 e e0)))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (n0 : not (@eq Site s2 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (receive_copy3 c s1 s2 e n n0 e0)) s0) (sigma_rooted s0 (bm (transition c (receive_copy3 c s1 s2 e n n0 e0)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  case (eq_site_dec s3 s0).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec owner owner then Zpos xH else Z0)) Z0 *)
(* Goal: forall _ : not (@eq Site s s0), Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec owner owner).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
(* Goal: forall _ : @eq Message (inc_dec s0) (inc_dec s), Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) q, Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; elim n.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.

  (* 4 *)
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (st c s0) (sigma_rooted s0 (Post_message Message dec (change_queue (queue Message) (bm c) s1 owner q) s1 s2)) *)
  rewrite sigma_rooted_post_message.
(* Goal: @eq Z (st c s0) (Z.add (sigma_rooted s0 (Collect_message Message (bm c) s1 s2)) (rooted_fun s0 s2 owner (inc_dec s1))) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite sigma_rooted_collect_message with (m := copy).
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) (if eq_site_dec s1 s0 then Zpos xH else Z0)) (if eq_site_dec s1 s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  case (eq_site_dec s1 s0).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.


  (* 5 *)
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (st c s0) (Z.add (sigma_rooted s0 (Collect_message Message (bm c) s1 s2)) (rooted_fun s0 s2 owner (inc_dec s1))) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite sigma_rooted_collect_message with (m := copy).
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: @eq Z (st c s0) (Z.add (sigma_rooted s0 (bm c)) (if eq_site_dec owner s0 then Zpos xH else Z0)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite case_ineq.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.

  (* 6 *)
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (st c s0) (sigma_rooted s0 (Post_message Message dec (change_queue (queue Message) (bm c) s1 owner q) s1 s2)) *)
  rewrite sigma_rooted_post_message.
(* Goal: @eq Z (st c s0) (Z.add (sigma_rooted s0 (Collect_message Message (bm c) s1 s2)) (rooted_fun s0 s2 owner (inc_dec s1))) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite sigma_rooted_collect_message with (m := copy).
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) (if eq_site_dec s1 s0 then Zpos xH else Z0)) (if eq_site_dec s1 s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  case (eq_site_dec s1 s0).
(* Goal: forall _ : @eq Site s1 s0, @eq Z (st c s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) (Zpos xH)) (if eq_site_dec owner owner then Zpos xH else Z0)) *)
(* Goal: forall _ : not (@eq Site s1 s0), @eq Z (st c s0) (Z.add (Z.sub (sigma_rooted s0 (bm c)) Z0) Z0) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (delete_entry c s e e0 n)) s0) (sigma_rooted s0 (bm (transition c (delete_entry c s e e0 n)))) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite case_eq.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.

  (* 7 *)
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (st c s0) (sigma_rooted s0 (Post_message Message dec (change_queue (queue Message) (bm c) s1 owner q) s1 s2)) *)
  rewrite sigma_rooted_post_message.
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: @eq Z (st c s0) (Z.add (sigma_rooted s0 (bm c)) (if eq_site_dec owner s0 then Zpos xH else Z0)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall (s1 s2 : Site) (q : queue Message) (n : not (@eq Site s1 s2)) (e : @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q))) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c (redirect_inc c s1 s2 q n e)) s0) (sigma_rooted s0 (bm (transition c (redirect_inc c s1 s2 q n e)))) *)
  rewrite case_ineq.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.  
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.

  (* optim 1 *)

(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; simpl in |- *.
(* Goal: @eq Z (st c s0) (sigma_rooted s0 (Post_message Message dec (change_queue (queue Message) (bm c) s1 owner q) s1 s2)) *)
  rewrite sigma_rooted_post_message.
(* Goal: @eq Z (st c s0) (Z.add (sigma_rooted s0 (change_queue (queue Message) (bm c) s1 owner q)) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
  rewrite sigma_rooted_change_queue with (s2 := s2).
(* Goal: @eq Z (st c s0) (Z.add (Z.sub (Z.sub (sigma_rooted s0 (bm c)) (rooted_fun s0 s1 owner dec)) (rooted_fun s0 s1 owner (inc_dec s2))) (rooted_fun s0 s1 s2 dec)) *)
(* Goal: not (@eq Site s0 owner) *)
(* Goal: @eq (queue Message) (bm c s1 owner) (input Message dec (input Message (inc_dec s2) q)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted_fun in |- *.
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec owner s0); intro.
(* Goal: not (@eq Site s0 owner) *)
  elim H; auto.
  
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec s2 s0); intro.
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec owner owner); intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
  
(* Goal: not (@eq Site s0 owner) *)
  elim n1; auto.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
Qed.


Lemma invariant2 :
 forall (c0 : Config) (s0 : Site),
 legal c0 -> s0 <> owner -> st c0 s0 = sigma_rooted s0 (bm c0).

Proof.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: @eq Z (st c0 s0) (sigma_rooted s0 (bm c0)) *)
  elim H.
(* Goal: @eq Z (st config_init s0) (sigma_rooted s0 (bm config_init)) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : @eq Z (st c s0) (sigma_rooted s0 (bm c))), @eq Z (st (transition c t) s0) (sigma_rooted s0 (bm (transition c t))) *)
  apply invariant2_init.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: @eq Z (st (transition c t) s0) (sigma_rooted s0 (bm (transition c t))) *)
  apply invariant2_ind.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: not (@eq Site s0 owner) *)
  auto.
Qed.


Lemma positive_st :
 forall (c : Config) (s0 s5 : Site),
 s0 <> owner ->
 legal c -> In_queue Message (inc_dec s0) (bm c s5 owner) -> (st c s0 > 0)%Z.
Proof.
(* Goal: forall (c : Config) (s0 s5 : Site) (_ : not (@eq Site s0 owner)) (_ : legal c) (_ : In_queue Message (inc_dec s0) (bm c s5 owner)), Z.gt (st c s0) Z0 *)
  intros c s0 s5 H HA.
(* Goal: forall _ : In_queue Message (inc_dec s0) (bm c s5 owner), Z.gt (st c s0) Z0 *)
  rewrite invariant2.
(* Goal: forall _ : In_queue Message (inc_dec s0) (bm c s5 owner), Z.gt (sigma_rooted s0 (bm c)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  unfold sigma_rooted in |- *.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: Z.gt (sigma2_table Site LS LS (queue Message) (rooted s0) (bm c)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  apply sigma2_strictly_positive with (x := s5) (y := owner).
(* Goal: not (@eq Site s0 owner) *)
  auto.
(* Goal: eq_dec Site *)
(* Goal: @List.In Site s5 LS *)
(* Goal: @List.In Site owner LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s0 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  exact eq_site_dec.
  
(* Goal: @List.In Site owner LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s0 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  apply in_s_LS.
(* Goal: @List.In Site owner LS *)
(* Goal: forall x' y' : Site, Z.ge (rooted s0 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  apply in_s_LS.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: Z.ge (rooted s0 x' y' (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  unfold rooted in |- *.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: Z.ge (reduce Message (rooted_fun s0 x' y') (bm c x' y')) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  apply reduce_positive_or_null.
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.ge (rooted_fun s0 x' y' a) Z0 *)
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  apply rooted_fun_positive_or_null.
  
(* Goal: Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H0.
(* Goal: forall _ : In_queue Message (inc_dec s0) (bm c s5 owner), Z.gt (rooted s0 s5 owner (bm c s5 owner)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  elim (bm c s5 owner).
(* Goal: forall _ : In_queue Message (inc_dec s0) (empty Message), Z.gt (rooted s0 s5 owner (empty Message)) Z0 *)
(* Goal: forall (d : Message) (q : queue Message) (_ : forall _ : In_queue Message (inc_dec s0) q, Z.gt (rooted s0 s5 owner q) Z0) (_ : In_queue Message (inc_dec s0) (input Message d q)), Z.gt (rooted s0 s5 owner (input Message d q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *; intuition.
  
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: Z.gt (rooted s0 s5 owner (input Message d q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H2.
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message d q), Z.gt (rooted s0 s5 owner (input Message d q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case d.
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  elim H3.
(* Goal: forall _ : @eq Message (inc_dec s0) copy, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) q, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; discriminate.
  
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (H1 H4).
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec owner s0 then Zpos xH else Z0)) Z0 *)
(* Goal: forall (s : Site) (_ : In_queue Message (inc_dec s0) (input Message (inc_dec s) q)), Z.gt (rooted s0 s5 owner (input Message (inc_dec s) q)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec owner s0).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
  
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros; omega.
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : or (@eq Message (inc_dec s0) (inc_dec s)) (In_queue Message (inc_dec s0) q)), Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intros.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s s0 then if eq_site_dec owner owner then Zpos xH else Z0 else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec s s0).
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec owner owner then Zpos xH else Z0)) Z0 *)
(* Goal: forall _ : not (@eq Site s s0), Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec owner owner).
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (Zpos xH)) Z0 *)
(* Goal: forall _ : not (@eq Site owner owner), Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : not (@eq Site s s0), Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (rooted_positive_or_null s0 s5 owner q).
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
  
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 owner) *)
  elim n; auto.
  
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  elim H3.
(* Goal: forall _ : @eq Message (inc_dec s0) (inc_dec s), Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) q, Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; elim n.
(* Goal: @eq Site s s0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) q, Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  inversion H4.
(* Goal: not (@eq Site s0 owner) *)
  auto.
  
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (H1 H4).
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  omega.
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  elim H3.
(* Goal: forall _ : @eq Message (inc_dec s0) copy, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) q, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; discriminate.
  
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (H1 H4).
(* Goal: forall _ : Z.gt (rooted s0 s5 owner q) Z0, Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) (if eq_site_dec s5 s0 then Zpos xH else Z0)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec s5 s0).
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
  
(* Goal: Z.gt (Z.add (rooted s0 s5 owner q) Z0) Z0 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (input Message copy q), Z.gt (rooted s0 s5 owner (input Message copy q)) Z0 *)
(* Goal: legal c *)
(* Goal: not (@eq Site s0 owner) *)
  intro; omega.
  
(* Goal: not (@eq Site s0 owner) *)
  auto.
  
(* Goal: not (@eq Site s0 owner) *)
  auto.
Qed.






End INVARIANT2.
