(* 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.machine2.invariant0.
Require Export DistributedReferenceCounting.machine2.invariant1.
Require Export DistributedReferenceCounting.machine2.invariant2.
Require Export DistributedReferenceCounting.machine2.invariant3.

Unset Standard Proposition Elimination Names.

(* Where send_table on the owner is defined in terms of the other components *)

(* Proofs are indentical to the ones for machine1.
   The only differnce is that aux1, add_reduce, and invariant4
   have an explicit -1 *)

Section INVARIANT4.

Definition new_inc_count (m : Message) :=
  match m with
  | inc_dec s => 1%Z
  | _ => 0%Z
  end.


(* Below five remarks aux1, aux2, aux3, aux4, aux5 ... followed by
  the real meat the invariant 4. *)

Remark aux1 :
 forall c : Config,
 legal c ->
 st c owner =
 (sigma_receive_table (rt c) + sigma_weight (bm c) -
  sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c) - 1)%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: forall _ : @eq Z (sigma_send_table (st c)) (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (Zpos xH)), @eq Z (st c owner) (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c))) (Zpos xH)) *)
  unfold sigma_send_table in |- *.
(* Goal: @eq Z (st c owner) (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c))) (Zpos xH)) *)
  generalize (invariant1 c H).
(* Goal: forall _ : @eq Z (sigma_send_table (st c)) (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (Zpos xH)), @eq Z (st c owner) (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c))) (Zpos xH)) *)
  unfold sigma_send_table in |- *.
(* Goal: forall _ : @eq Z (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (st c)) (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (Zpos xH)), @eq Z (st c owner) (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c))) (Zpos xH)) *)
  rewrite sigma_sigma_but_owner.
(* Goal: forall _ : @eq Z (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c)) (st c owner)) (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (Zpos xH)), @eq Z (st c owner) (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c))) (Zpos xH)) *)
  generalize (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c)).
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  omega.
Qed.


Remark aux2 :
 forall c : Config,
 legal c ->
 sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c) =
 sigma_but Site owner eq_site_dec LS (fun s : Site => sigma_rooted s (bm c)).
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c)) (sigma_but Site owner eq_site_dec LS (fun s : Site => sigma_rooted s (bm c))) *)
  unfold sigma_table_but_owner in |- *.
(* Goal: @eq Z (sigma_but Site owner eq_site_dec LS (fun s : Site => st c s)) (sigma_but Site owner eq_site_dec LS (fun s : Site => sigma_rooted s (bm c))) *)
  apply sigma_but_simpl.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (st c s) (sigma_rooted s (bm c)) *)
  rewrite (invariant2 c s).
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
Qed.

Remark aux3 :
 forall (s1 s2 : Site) (q : queue Message),
 (cardinal q -
  sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 q))%Z =
 reduce Message
   (fun a : Message =>
    (cardinal_count a -
     sigma_but Site owner eq_site_dec LS
       (fun s : Site => rooted_fun s s1 s2 a))%Z) q.
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.sub (cardinal q) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 q))) (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) *)
  unfold rooted in |- *.
(* Goal: @eq Z (Z.sub (cardinal q) (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message (rooted_fun s s1 s2) q))) (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) *)
  unfold cardinal in |- *.
(* Goal: @eq Z (Z.sub (reduce Message cardinal_count q) (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message (rooted_fun s s1 s2) q))) (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) *)
  rewrite permute_sigma_but_reduce.
(* Goal: @eq Z (Z.sub (reduce Message cardinal_count q) (reduce Message (fun d : Message => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d)) q)) (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) *)
  rewrite <- disjoint_reduce3.
(* Goal: @eq Z (reduce Message (fun_minus Message cardinal_count (fun d : Message => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d))) q) (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) *)
  unfold fun_minus in |- *.
(* Goal: legal c *)
  auto.
Qed.

Remark aux4 :
 forall t : Site -> Site -> queue Message,
 sigma2_table Site LS LS (queue Message)
   (fun (s1 s2 : Site) (q : queue Message) =>
    (cardinal q -
     sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 q))%Z)
   t =
 sigma2_table Site LS LS (queue Message)
   (fun (s1 s2 : Site) (q : queue Message) =>
    reduce Message
      (fun a : Message =>
       (cardinal_count a -
        sigma_but Site owner eq_site_dec LS
          (fun s : Site => rooted_fun s s1 s2 a))%Z) q) t.
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c)) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner))) *)
  unfold sigma2_table in |- *.
(* Goal: @eq Z (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b s1))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (b s1 owner))) *)
  apply sigma_table_simpl.
(* Goal: @eq (forall _ : Site, Z) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b s1)) (fun s1 : Site => reduce Message new_inc_count (b s1 owner)) *)
  apply funct_eq.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma_table Site LS (queue Message) (fun (s2 : Site) (q : queue Message) => Z.sub (cardinal q) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s e s2 q))) (t e)) (sigma_table Site LS (queue Message) (fun (s2 : Site) (q : queue Message) => reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s e s2 a))) q) (t e)) *)
  apply sigma_table_simpl2.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.sub (cardinal d) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted s0 e s d))) (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 e s a))) d) *)
  apply aux3.
Qed.




Remark aux5 :
 forall c : Config,
 legal c ->
 sigma2_table Site LS LS (queue Message)
   (fun (s1 s2 : Site) (q : queue Message) =>
    reduce Message
      (fun a : Message =>
       (cardinal_count a -
        sigma_but Site owner eq_site_dec LS
          (fun s : Site => rooted_fun s s1 s2 a))%Z) q) 
   (bm c) =
 (sigma2_table Site LS LS (queue Message)
    (fun (s1 s2 : Site) (q : queue Message) =>
     if eq_site_dec s2 owner
     then reduce Message dec_count q
     else 0) (bm c) +
  sigma2_table Site LS LS (queue Message)
    (fun (s1 s2 : Site) (q : queue Message) =>
     if eq_site_dec s1 owner
     then reduce Message copy_count q
     else 0) (bm c) -
  sigma2_table Site LS LS (queue Message)
    (fun (s1 s2 : Site) (q : queue Message) => reduce Message new_inc_count q)
    (bm c))%Z.


Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) (bm c)) (Z.sub (Z.add (sigma2_table Site LS LS (queue Message) (fun (_ s2 : Site) (q : queue Message) => if eq_site_dec s2 owner then reduce Message dec_count q else Z0) (bm c)) (sigma2_table Site LS LS (queue Message) (fun (s1 _ : Site) (q : queue Message) => if eq_site_dec s1 owner then reduce Message copy_count q else Z0) (bm c))) (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c))) *)
  rewrite <- sigma2_disjoint.
(* Goal: @eq Z (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (bm c)) (sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (d : queue Message) => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 d)) (bm c))) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  rewrite <- sigma2_disjoint2.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) (bm c)) (sigma2_table Site LS LS (queue Message) (fun_minus_site2 Site (queue Message) (fun_sum_site2 Site (queue Message) (fun (_ s2 : Site) (q : queue Message) => if eq_site_dec s2 owner then reduce Message dec_count q else Z0) (fun (s1 _ : Site) (q : queue Message) => if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q)) (bm c)) *)
  apply sigma2_table_simpl_partial.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun_minus_site2 Site (queue Message) (fun _ _ : Site => cardinal) (fun (s1 s2 : Site) (d : queue Message) => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 d))) (bm c)) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  unfold fun_minus_site2 in |- *.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun s1 : Site => fun_minus_site Site (queue Message) (fun (_ : Site) (a : queue Message) => cardinal a) (fun (s2 : Site) (a : queue Message) => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 a))) (bm c)) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  unfold fun_minus_site in |- *.
(* Goal: forall (s1 s2 : Site) (d : queue Message) (_ : @eq (queue Message) (bm c s1 s2) d), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) d) (Z.sub (fun_sum_site2 Site (queue Message) (fun (_ s4 : Site) (q : queue Message) => if eq_site_dec s4 owner then reduce Message dec_count q else Z0) (fun (s3 _ : Site) (q : queue Message) => if eq_site_dec s3 owner then reduce Message copy_count q else Z0) s1 s2 d) (reduce Message new_inc_count d)) *)
  unfold fun_sum_site2 in |- *.
(* Goal: forall (s1 s2 : Site) (d : queue Message) (_ : @eq (queue Message) (bm c s1 s2) d), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) d) (Z.sub (fun_sum_site Site (queue Message) (fun (s3 : Site) (a : queue Message) => if eq_site_dec s3 owner then reduce Message dec_count a else Z0) (fun (_ : Site) (a : queue Message) => if eq_site_dec s1 owner then reduce Message copy_count a else Z0) s2 d) (reduce Message new_inc_count d)) *)
  unfold fun_sum_site in |- *.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) d) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count d else Z0) (if eq_site_dec s1 owner then reduce Message copy_count d else Z0)) (reduce Message new_inc_count d)) *)
  generalize (not_owner_inc4 c s1 s2 H).
(* Goal: forall _ : forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m (bm c s1 s2)), not (@eq Site s0 owner), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) d) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count d else Z0) (if eq_site_dec s1 owner then reduce Message copy_count d else Z0)) (reduce Message new_inc_count d)) *)
  generalize (inc_dec_owner4 c s1 s2 H).
(* Goal: forall (_ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (bm c s1 s2))) (_ : forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m (bm c s1 s2)), not (@eq Site s0 owner)), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) d) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count d else Z0) (if eq_site_dec s1 owner then reduce Message copy_count d else Z0)) (reduce Message new_inc_count d)) *)
  generalize (inc_dec_owner2 c s1 s2 H).
(* Goal: forall (_ : forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) (bm c s1 s2))) (_ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (bm c s1 s2))) (_ : forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m (bm c s1 s2)), not (@eq Site s0 owner)), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) d) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count d else Z0) (if eq_site_dec s1 owner then reduce Message copy_count d else Z0)) (reduce Message new_inc_count d)) *)
  generalize (empty_queue2 c H s1 s2 owner).
(* Goal: @eq Z (Z.add (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (if eq_site_dec s2 owner then Z.add (reduce Message dec_count q) (dec_count d0) else Z0) (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
  rewrite H0.
(* Goal: forall (_ : forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) d (empty Message)) (_ : forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) d)) (_ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) d)) (_ : forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m d), not (@eq Site s0 owner)), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) d) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count d else Z0) (if eq_site_dec s1 owner then reduce Message copy_count d else Z0)) (reduce Message new_inc_count d)) *)
  clear H0.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) d) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count d)) Z0 *)
  elim d.
(* Goal: forall (_ : forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) (empty Message) (empty Message)) (_ : forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) (empty Message))) (_ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (empty Message))) (_ : forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m (empty Message)), not (@eq Site s0 owner)), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) (empty Message)) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count (empty Message) else Z0) (if eq_site_dec s1 owner then reduce Message copy_count (empty Message) else Z0)) (reduce Message new_inc_count (empty Message))) *)
(* Goal: forall (d : Message) (q : queue Message) (_ : forall (_ : forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message)) (_ : forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q)) (_ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q)) (_ : forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner)), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count q else Z0) (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q))) (_ : forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) (input Message d q) (empty Message)) (_ : forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) (input Message d q))) (_ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (input Message d q))) (_ : forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m (input Message d q)), not (@eq Site s0 owner)), @eq Z (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) (input Message d q)) (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count (input Message d q) else Z0) (if eq_site_dec s1 owner then reduce Message copy_count (input Message d q) else Z0)) (reduce Message new_inc_count (input Message d q))) *)
  intros; simpl in |- *.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count q else Z0) (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (if eq_site_dec s2 owner then Z.add (reduce Message dec_count q) (dec_count d0) else Z0) (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  case (eq_site_dec s2 owner).
(* Goal: @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  case (eq_site_dec s1 owner).
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  intros; omega.
  
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  intros; omega.
  
(* Goal: @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  case (eq_site_dec s1 owner).
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  intros; omega.
  
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  intros; omega.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (if eq_site_dec s2 owner then Z.add (reduce Message dec_count q) (dec_count d0) else Z0) (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
  rewrite H0.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (if eq_site_dec s2 owner then reduce Message dec_count q else Z0) (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (if eq_site_dec s2 owner then Z.add (reduce Message dec_count q) (dec_count d0) else Z0) (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  case (eq_site_dec s2 owner).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  case (eq_site_dec s1 owner).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) (reduce Message copy_count q)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count d0)) (Z.add (reduce Message copy_count q) (copy_count d0))) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count d0)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H1 e0 e).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) (reduce Message copy_count q)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count d0)) (Z.add (reduce Message copy_count q) (copy_count d0))) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count d0)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (Z.sub (Z.add Z0 (reduce Message copy_count q)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (Z.add (reduce Message copy_count q) (copy_count d0))) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite e.
(* Goal: @eq Z (Z.sub (copy_count d0) (new_inc_count d0)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  unfold cardinal_count in |- *.
(* Goal: @eq Z (Z.sub (copy_count d0) (new_inc_count d0)) (Z.sub (fun_sum Message dec_count (fun_sum Message inc_count copy_count) d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  unfold fun_sum in |- *.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count d0) (Z.add (inc_count d0) (copy_count d0))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 owner d0)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count d0)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H4 d0).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message d0 q)), @eq Z (Z.opp (new_inc_count d0)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  elim d0.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count dec) (Z.add (inc_count dec) (copy_count dec))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 owner dec)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count dec)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count dec))) *)
(* Goal: forall (s : Site) (_ : forall (s0 : Site) (_ : @eq Message (inc_dec s) (inc_dec s0)) (_ : In_queue Message (inc_dec s) (input Message (inc_dec s) q)), not (@eq Site s0 owner)), @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count (inc_dec s)) (Z.add (inc_count (inc_dec s)) (copy_count (inc_dec s)))) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 s1 owner (inc_dec s))))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count (inc_dec s))) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count (inc_dec s)))) *)
(* Goal: forall _ : forall (s0 : Site) (_ : @eq Message copy (inc_dec s0)) (_ : In_queue Message copy (input Message copy q)), not (@eq Site s0 owner), @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count copy) (Z.add (inc_count copy) (copy_count copy))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 owner copy)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count copy)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count copy))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite sigma_rooted_fun3.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  omega.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count (inc_dec s)) (Z.add (inc_count (inc_dec s)) (copy_count (inc_dec s)))) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 s1 owner (inc_dec s))))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count (inc_dec s))) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count (inc_dec s)))) *)
(* Goal: forall _ : forall (s0 : Site) (_ : @eq Message copy (inc_dec s0)) (_ : In_queue Message copy (input Message copy q)), not (@eq Site s0 owner), @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count copy) (Z.add (inc_count copy) (copy_count copy))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 owner copy)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count copy)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count copy))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite sigma_rooted_fun5.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  omega.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
  
(* Goal: not (@eq Site s owner) *)
(* Goal: forall _ : forall (s0 : Site) (_ : @eq Message copy (inc_dec s0)) (_ : In_queue Message copy (input Message copy q)), not (@eq Site s0 owner), @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count copy) (Z.add (inc_count copy) (copy_count copy))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 owner copy)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count copy)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count copy))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  apply H5.
(* Goal: legal c *)
  auto.
  
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: legal c *)
  left; auto.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (Z.add (dec_count copy) (Z.add (inc_count copy) (copy_count copy))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 owner copy)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count copy)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count copy))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite sigma_rooted_fun7.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  omega.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
  
(* Goal: legal c *)
  auto.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  case (eq_site_dec s1 owner).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (Z.sub (Z.add Z0 (reduce Message copy_count q)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (Z.add (reduce Message copy_count q) (copy_count d0))) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite e.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
  replace
   (cardinal_count d0 -
    sigma_but Site owner eq_site_dec LS
      (fun s : Site => rooted_fun s owner s2 d0))%Z with
   (copy_count d0 - new_inc_count d0)%Z.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  omega.
  
(* Goal: @eq Z (Z.sub (copy_count d0) (new_inc_count d0)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  unfold cardinal_count in |- *.
(* Goal: @eq Z (Z.sub (copy_count d0) (new_inc_count d0)) (Z.sub (fun_sum Message dec_count (fun_sum Message inc_count copy_count) d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  unfold fun_sum in |- *.
(* Goal: @eq Z (Z.sub (copy_count d0) (new_inc_count d0)) (Z.sub (Z.add (dec_count d0) (Z.add (inc_count d0) (copy_count d0))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize H3.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message d0 q)), @eq Z (Z.opp (new_inc_count d0)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  elim d0.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.sub (copy_count dec) (new_inc_count dec)) (Z.sub (Z.add (dec_count dec) (Z.add (inc_count dec) (copy_count dec))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 dec))) *)
(* Goal: forall (s : Site) (_ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (input Message (inc_dec s) q))), @eq Z (Z.sub (copy_count (inc_dec s)) (new_inc_count (inc_dec s))) (Z.sub (Z.add (dec_count (inc_dec s)) (Z.add (inc_count (inc_dec s)) (copy_count (inc_dec s)))) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 owner s2 (inc_dec s)))) *)
(* Goal: forall _ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (input Message copy q)), @eq Z (Z.sub (copy_count copy) (new_inc_count copy)) (Z.sub (Z.add (dec_count copy) (Z.add (inc_count copy) (copy_count copy))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 copy))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite sigma_rooted_fun9.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: legal c *)
  auto.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
  
(* Goal: legal c *)
  auto.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.sub (copy_count (inc_dec s)) (new_inc_count (inc_dec s))) (Z.sub (Z.add (dec_count (inc_dec s)) (Z.add (inc_count (inc_dec s)) (copy_count (inc_dec s)))) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 owner s2 (inc_dec s)))) *)
(* Goal: forall _ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (input Message copy q)), @eq Z (Z.sub (copy_count copy) (new_inc_count copy)) (Z.sub (Z.add (dec_count copy) (Z.add (inc_count copy) (copy_count copy))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 copy))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H5 e s).
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Zneg xH) (Z.opp (sigma_but Site owner eq_site_dec LS (fun s0 : Site => if eq_site_dec s s0 then if eq_site_dec s2 owner then Zpos xH else Z0 else Z0))) *)
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message copy q)), @eq Z (Z.opp (new_inc_count copy)) (Z.sub (cardinal_count copy) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 copy))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  elim H6.
(* Goal: legal c *)
  left; auto.
  
(* Goal: forall _ : forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) (input Message copy q)), @eq Z (Z.sub (copy_count copy) (new_inc_count copy)) (Z.sub (Z.add (dec_count copy) (Z.add (inc_count copy) (copy_count copy))) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 copy))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add Z0 Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite sigma_rooted_fun10.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: legal c *)
  auto.
  
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
  replace
   (cardinal_count d0 -
    sigma_but Site owner eq_site_dec LS
      (fun s : Site => rooted_fun s s1 s2 d0))%Z with 
   (- new_inc_count d0)%Z.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  omega.
  
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (Z.opp (new_inc_count d0)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H2 n0 n).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message d0 q)), @eq Z (Z.opp (new_inc_count d0)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  elim d0.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.opp (new_inc_count dec)) (Z.sub (cardinal_count dec) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 dec))) *)
(* Goal: forall (s : Site) (_ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message (inc_dec s) q))), @eq Z (Z.opp (new_inc_count (inc_dec s))) (Z.sub (cardinal_count (inc_dec s)) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 s1 s2 (inc_dec s)))) *)
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message copy q)), @eq Z (Z.opp (new_inc_count copy)) (Z.sub (cardinal_count copy) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 copy))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite sigma_rooted_fun12.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.opp (new_inc_count (inc_dec s))) (Z.sub (cardinal_count (inc_dec s)) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted_fun s0 s1 s2 (inc_dec s)))) *)
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message copy q)), @eq Z (Z.opp (new_inc_count copy)) (Z.sub (cardinal_count copy) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 copy))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H5 s).
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Zneg xH) (Z.opp (sigma_but Site owner eq_site_dec LS (fun s0 : Site => if eq_site_dec s s0 then if eq_site_dec s2 owner then Zpos xH else Z0 else Z0))) *)
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (input Message copy q)), @eq Z (Z.opp (new_inc_count copy)) (Z.sub (cardinal_count copy) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 copy))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  elim H6.
(* Goal: legal c *)
  left; auto.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z.opp (new_inc_count copy)) (Z.sub (cardinal_count copy) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 copy))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  rewrite sigma_rooted_fun14.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H1 H5 H6).
(* Goal: @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) (reduce Message copy_count q)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count d0)) (Z.add (reduce Message copy_count q) (copy_count d0))) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq Z (Z.add (Z.sub (Z.add (reduce Message dec_count q) Z0) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add (Z.add (reduce Message dec_count q) (dec_count d0)) Z0) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall _ : not (@eq Site s2 owner), @eq Z (Z.add (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then reduce Message copy_count q else Z0)) (reduce Message new_inc_count q)) (Z.sub (cardinal_count d0) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 d0)))) (Z.sub (Z.add Z0 (if eq_site_dec s1 owner then Z.add (reduce Message copy_count q) (copy_count d0) else Z0)) (Z.add (reduce Message new_inc_count q) (new_inc_count d0))) *)
(* Goal: forall (_ : @eq Site s1 owner) (_ : @eq Site s2 owner), @eq (queue Message) q (empty Message) *)
(* Goal: forall (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  intro; discriminate.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (_ : @eq Site s1 owner) (s0 : Site), not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H2 H5 H6 s0).
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), not (In_queue Message (inc_dec s0) q0) *)
  intuition.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: not (In_queue Message (inc_dec s0) q) *)
(* Goal: forall (m : Message) (s0 : Site) (_ : @eq Message m (inc_dec s0)) (_ : In_queue Message m q), not (@eq Site s0 owner) *)
  generalize (H3 H5 s0).
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), not (In_queue Message (inc_dec s0) q0) *)
  intuition.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: not (@eq Site s0 owner) *)
  generalize (H4 m s0 H5).
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: not (@eq Site s0 owner) *)
  apply H7.
(* Goal: legal c *)
  right; auto.
Qed.

Lemma simpl_dec_sum :
 forall c : Config,
 legal c ->
 sigma2_table Site LS LS (queue Message)
   (fun (s1 s2 : Site) (q : queue Message) =>
    if eq_site_dec s2 owner
    then reduce Message dec_count q
    else 0%Z) (bm c) =
 sigma_table Site LS Z (Z_id Site)
   (fun s1 : Site => reduce Message dec_count (bm c s1 owner)).

Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c)) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner))) *)
  unfold sigma2_table in |- *.
(* Goal: @eq Z (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b s1))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (b s1 owner))) *)
  apply sigma_table_simpl.
(* Goal: @eq (forall _ : Site, Z) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b s1)) (fun s1 : Site => reduce Message new_inc_count (b s1 owner)) *)
  apply funct_eq.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b e)) (reduce Message new_inc_count (b e owner)) *)
  unfold sigma_table in |- *.
  rewrite
   (sigma_sigma_but Site owner eq_site_dec
      (fun s : Site =>
       match eq_site_dec s owner with
       | left _ => reduce Message dec_count (bm c e s)
       | right _ => 0%Z
       end)).
  replace
   (sigma_but Site owner eq_site_dec LS
      (fun s : Site =>
       match eq_site_dec s owner with
       | left _ => reduce Message dec_count (bm c e s)
       | right _ => 0%Z
       end)) with 0%Z.
(* Goal: @eq Z (Z.add Z0 (if eq_site_dec owner owner then reduce Message dec_count (bm c e owner) else Z0)) (reduce Message dec_count (bm c e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => if eq_site_dec s owner then reduce Message dec_count (bm c e s) else Z0)) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  case (eq_site_dec owner owner).
(* Goal: legal c *)
  intro; auto.
(* Goal: forall _ : not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), not (In_queue Message (inc_dec s0) q0) *)
  intuition.
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite sigma_but_null.
(* Goal: legal c *)
  auto.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (if eq_site_dec s owner then reduce Message dec_count (bm c e s) else Z0) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite case_ineq.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.    

Lemma simpl_copy_sum :
 forall c : Config,
 legal c ->
 sigma2_table Site LS LS (queue Message)
   (fun (s1 _ : Site) (q : queue Message) =>
    match eq_site_dec s1 owner with
    | left _ => reduce Message copy_count q
    | right _ => 0%Z
    end) (bm c) =
 sigma_table Site LS Z (Z_id Site)
   (fun s2 : Site => reduce Message copy_count (bm c owner s2)).
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c)) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner))) *)
  unfold sigma2_table in |- *.
(* Goal: @eq Z (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => if eq_site_dec s1 owner then reduce Message copy_count q else Z0) (bm c s1))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) *)
  unfold sigma in |- *.
(* Goal: @eq Z (sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b e)) (reduce Message new_inc_count (b e owner)) *)
  unfold sigma_table in |- *.
  rewrite
   (sigma_sigma_but Site owner eq_site_dec
      (fun s : Site =>
       Z_id Site s
         (sigma Site LS
            (fun s0 : Site =>
             match eq_site_dec s owner with
             | left _ => reduce Message copy_count (bm c s s0)
             | right _ => 0%Z
             end)))).
(* Goal: @eq Z (Z_id Site s (sigma Site LS (fun s0 : Site => if eq_site_dec s owner then reduce Message copy_count (bm c s s0) else Z0))) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite Z_id_reduce.
  replace
   (sigma_but Site owner eq_site_dec LS
      (fun s : Site =>
       Z_id Site s
         (sigma Site LS
            (fun s0 : Site =>
             match eq_site_dec s owner with
             | left _ => reduce Message copy_count (bm c s s0)
             | right _ => 0%Z
             end)))) with 0%Z.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (sigma Site LS (fun s0 : Site => if eq_site_dec owner owner then reduce Message copy_count (bm c owner s0) else Z0)) (sigma Site LS (fun s : Site => Z_id Site s (reduce Message copy_count (bm c owner s)))) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => Z_id Site s (sigma Site LS (fun s0 : Site => if eq_site_dec s owner then reduce Message copy_count (bm c s s0) else Z0)))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  apply sigma_simpl.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (if eq_site_dec owner owner then reduce Message copy_count (bm c owner x) else Z0) (Z_id Site x (reduce Message copy_count (bm c owner x))) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => Z_id Site s (sigma Site LS (fun s0 : Site => if eq_site_dec s owner then reduce Message copy_count (bm c s s0) else Z0)))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite case_eq.
(* Goal: @eq Z (Z_id Site s (sigma Site LS (fun s0 : Site => if eq_site_dec s owner then reduce Message copy_count (bm c s s0) else Z0))) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite Z_id_reduce.
(* Goal: legal c *)
  auto.
  
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite sigma_but_null.
(* Goal: legal c *)
  auto.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (Z_id Site s (sigma Site LS (fun s0 : Site => if eq_site_dec s owner then reduce Message copy_count (bm c s s0) else Z0))) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite Z_id_reduce.
(* Goal: @eq Z (sigma Site LS (fun s0 : Site => if eq_site_dec s owner then reduce Message copy_count (bm c s s0) else Z0)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  case (eq_site_dec s owner).
(* Goal: legal c *)
  intro; elim H0; auto.
  
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (sigma Site LS (fun _ : Site => Z0)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  apply sigma_null.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.


Lemma no_inc_dec :
 forall q : queue Message,
 (forall s0 : Site, ~ In_queue Message (inc_dec s0) q) ->
 reduce Message new_inc_count q = 0%Z.
Proof.
(* Goal: forall (q : queue Message) (_ : forall s0 : Site, not (In_queue Message (inc_dec s0) q)), @eq Z (reduce Message new_inc_count q) Z0 *)
  simple induction q.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: legal c *)
  auto.
  
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall (d : Message) (q : queue Message) (_ : forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) q), @eq Z (reduce Message new_inc_count q) Z0) (_ : forall s0 : Site, not (or (@eq Message (inc_dec s0) d) (In_queue Message (inc_dec s0) q))), @eq Z (Z.add (reduce Message new_inc_count q) (new_inc_count d)) Z0 *)
  intros d q0 H.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) d) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count d)) Z0 *)
  elim d.
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (reduce Message new_inc_count q0) Z0) Z0 *)
  rewrite H.
(* Goal: legal c *)
  auto.
  
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: not (In_queue Message (inc_dec s0) q0) *)
  generalize (H0 s0).
(* Goal: forall _ : not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), not (In_queue Message (inc_dec s0) q0) *)
  intuition.
  
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (reduce Message new_inc_count q0) (Zpos xH)) Z0 *)
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  generalize (H0 s).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: legal c *)
  elim H1; left; auto.
  
(* Goal: forall _ : forall s0 : Site, not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), @eq Z (Z.add (reduce Message new_inc_count q0) (new_inc_count copy)) Z0 *)
  simpl in |- *.
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (Z.add (reduce Message new_inc_count q0) Z0) Z0 *)
  rewrite H.
(* Goal: legal c *)
  auto.
  
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: not (In_queue Message (inc_dec s0) q0) *)
  generalize (H0 s0).
(* Goal: forall _ : not (or (@eq Message (inc_dec s0) copy) (In_queue Message (inc_dec s0) q0)), not (In_queue Message (inc_dec s0) q0) *)
  intuition.
Qed.



Lemma simpl_inc_sum :
 forall c : Config,
 legal c ->
 sigma2_table Site LS LS (queue Message)
   (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q)
   (bm c) =
 sigma_table Site LS Z (Z_id Site)
   (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)).

Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c)) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner))) *)
  unfold sigma2_table in |- *.
(* Goal: @eq Z (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c s1))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner))) *)
  generalize (inc_dec_owner2 c).
(* Goal: forall _ : forall (s1 s2 : Site) (_ : legal c) (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) (bm c s1 s2)), @eq Z (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c s1))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner))) *)
  generalize (inc_dec_owner3 c).
(* Goal: forall (_ : forall (s1 s2 : Site) (_ : legal c) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) (bm c s1 s2))) (_ : forall (s1 s2 : Site) (_ : legal c) (_ : not (@eq Site s1 owner)) (_ : not (@eq Site s2 owner)) (s0 : Site), not (In_queue Message (inc_dec s0) (bm c s1 s2))), @eq Z (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c s1))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner))) *)
  generalize (bm c).
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b s1))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (b s1 owner))) *)
  apply sigma_table_simpl.
(* Goal: @eq (forall _ : Site, Z) (fun s1 : Site => sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b s1)) (fun s1 : Site => reduce Message new_inc_count (b s1 owner)) *)
  apply funct_eq.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (sigma_table Site LS (queue Message) (fun (_ : Site) (q : queue Message) => reduce Message new_inc_count q) (b e)) (reduce Message new_inc_count (b e owner)) *)
  unfold sigma_table in |- *.
(* Goal: @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  case (eq_site_dec e owner).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
  rewrite
   (sigma_sigma_but Site owner eq_site_dec
      (fun s : Site => reduce Message new_inc_count (b e s)))
   .
  replace
   (sigma_but Site owner eq_site_dec LS
      (fun s : Site => reduce Message new_inc_count (b e s))) with 0%Z.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  omega.
  
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite sigma_but_null.
(* Goal: legal c *)
  auto.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
  generalize (H0 e s H H2).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  apply no_inc_dec.
(* Goal: legal c *)
  auto.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
  
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
  rewrite
   (sigma_sigma_but Site owner eq_site_dec
      (fun s : Site => reduce Message new_inc_count (b e s)))
   .
  replace
   (sigma_but Site owner eq_site_dec LS
      (fun s : Site => reduce Message new_inc_count (b e s))) with 0%Z.
(* Goal: legal c *)
  auto.
  
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite sigma_but_null.
(* Goal: legal c *)
  auto.
  
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  generalize (H1 e s H n H2).
(* Goal: forall _ : forall s0 : Site, not (In_queue Message (inc_dec s0) (b e s)), @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  intro.
(* Goal: @eq Z (reduce Message new_inc_count (b e s)) Z0 *)
(* Goal: only_once Site eq_site_dec owner LS *)
  apply no_inc_dec.
(* Goal: legal c *)
  auto.
  
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.


Remark add_reduce :
 forall x y a u w z : Z,
 (y - a)%Z = (z + w - u)%Z -> (x + y - a - 1)%Z = (x + z + w - u - 1)%Z.
Proof.
(* Goal: @eq Z (Z.add Z0 (reduce Message new_inc_count (b e owner))) (reduce Message new_inc_count (b e owner)) *)
(* Goal: @eq Z Z0 (sigma_but Site owner eq_site_dec LS (fun s : Site => reduce Message new_inc_count (b e s))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
(* Goal: forall _ : not (@eq Site e owner), @eq Z (sigma Site LS (fun s : Site => reduce Message new_inc_count (b e s))) (reduce Message new_inc_count (b e owner)) *)
intros; omega.
Qed.


Lemma invariant4 :
 forall c : Config,
 legal c ->
 st c owner =
 (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)) - 1)%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (st c owner) (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)) *)
  intros.
(* Goal: @eq Z (st c owner) (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)) *)
  rewrite (aux1 c H).
(* Goal: @eq Z (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (st c))) (Zpos xH)) (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)) *)
  rewrite aux2.
(* Goal: @eq Z (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) (sigma_but Site owner eq_site_dec LS (fun s : Site => sigma_rooted s (bm c)))) (Zpos xH)) (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)) *)
(* Goal: legal c *)
  unfold sigma_weight in |- *.
(* Goal: @eq Z (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (bm c))) (sigma_but Site owner eq_site_dec LS (fun s : Site => sigma_rooted s (bm c)))) (Zpos xH)) (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)) *)
(* Goal: legal c *)
  unfold sigma_rooted in |- *.
(* Goal: @eq Z (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (bm c))) (sigma_but Site owner eq_site_dec LS (fun s : Site => sigma2_table Site LS LS (queue Message) (rooted s) (bm c)))) (Zpos xH)) (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)) *)
(* Goal: legal c *)
  rewrite sigma2_sigma_but.
(* Goal: @eq Z (Z.sub (Z.sub (Z.add (sigma_receive_table (rt c)) (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (bm c))) (sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (d : queue Message) => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 d)) (bm c))) (Zpos xH)) (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)) *)
(* Goal: legal c *)
  apply add_reduce.
(* Goal: @eq Z (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (bm c)) (sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (d : queue Message) => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 d)) (bm c))) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  rewrite <- sigma2_disjoint2.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun_minus_site2 Site (queue Message) (fun _ _ : Site => cardinal) (fun (s1 s2 : Site) (d : queue Message) => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 d))) (bm c)) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  unfold fun_minus_site2 in |- *.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun s1 : Site => fun_minus_site Site (queue Message) (fun (_ : Site) (a : queue Message) => cardinal a) (fun (s2 : Site) (a : queue Message) => sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 a))) (bm c)) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  unfold fun_minus_site in |- *.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (s1 s : Site) (a : queue Message) => Z.sub (cardinal a) (sigma_but Site owner eq_site_dec LS (fun s0 : Site => rooted s0 s1 s a))) (bm c)) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  rewrite aux4.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun (s1 s2 : Site) (q : queue Message) => reduce Message (fun a : Message => Z.sub (cardinal_count a) (sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))) q) (bm c)) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
  rewrite aux5.
(* Goal: @eq Z (Z.sub (Z.add (sigma2_table Site LS LS (queue Message) (fun (_ s2 : Site) (q : queue Message) => if eq_site_dec s2 owner then reduce Message dec_count q else Z0) (bm c)) (sigma2_table Site LS LS (queue Message) (fun (s1 _ : Site) (q : queue Message) => if eq_site_dec s1 owner then reduce Message copy_count q else Z0) (bm c))) (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c))) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
(* Goal: legal c *)
  rewrite simpl_dec_sum.
(* Goal: @eq Z (Z.sub (Z.add (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (sigma2_table Site LS LS (queue Message) (fun (s1 _ : Site) (q : queue Message) => if eq_site_dec s1 owner then reduce Message copy_count q else Z0) (bm c))) (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c))) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: legal c *)
  rewrite simpl_copy_sum.
(* Goal: @eq Z (Z.sub (Z.add (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)))) (sigma2_table Site LS LS (queue Message) (fun (_ _ : Site) (q : queue Message) => reduce Message new_inc_count q) (bm c))) (Z.sub (Z.add (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)))) *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: legal c *)
(* Goal: legal c *)
  rewrite simpl_inc_sum.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
Qed.






End INVARIANT4.




