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


(* Communications *)

(* Without specifying how messages are defined, I am constructing
general Lemma in terms of reduce *)

Require Export reduce.
Require Export DistributedReferenceCounting.machine4.cardinal.
Require Export sigma2.
Require Export sum.

Unset Standard Proposition Elimination Names.

Section CARDINAL_EFFECT.

(* This section is really using the inductive type Message *)
Let Bag_of_message := Bag_of_Data Message.

Variable inc_fun : Site -> Z.

Lemma cardinal_post_message :
 forall (m : Message) (s1 s2 : Site) (b : Bag_of_message),
 cardinal (Post_message Message m b s1 s2 s1 s2) =
 (cardinal (b s1 s2) + cardinal_count m)%Z.
Proof.
(* Goal: forall (x y : Site) (_ : not (and (@eq Site x s1) (@eq Site y s2))), @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  intros.
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => cardinal) (change_queue (queue Message) b s1 s2 q)) (cardinal (change_queue (queue Message) b s1 s2 q s1 s2))) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => cardinal) b) (cardinal (b s1 s2))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  unfold cardinal in |- *.
(* Goal: @eq Z (reduce Message cardinal_count (Post_message Message m b s1 s2 s1 s2)) (Z.add (reduce Message cardinal_count (b s1 s2)) (cardinal_count m)) *)
  apply reduce_post_message.
Qed.

Lemma cardinal_collect_message :
 forall (m : Message) (s1 s2 : Site) (b : Bag_of_message),
 first Message (b s1 s2) = value Message m ->
 cardinal (Collect_message Message b s1 s2 s1 s2) =
 (cardinal (b s1 s2) - cardinal_count m)%Z.
Proof.
(* Goal: forall (x y : Site) (_ : not (and (@eq Site x s1) (@eq Site y s2))), @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  intros.
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => cardinal) (change_queue (queue Message) b s1 s2 q)) (cardinal (change_queue (queue Message) b s1 s2 q s1 s2))) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => cardinal) b) (cardinal (b s1 s2))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  unfold cardinal in |- *.
(* Goal: @eq Z (reduce Message cardinal_count (Collect_message Message b s1 s2 s1 s2)) (Z.sub (reduce Message cardinal_count (b s1 s2)) (cardinal_count m)) *)
  apply reduce_collect_message.
(* Goal: @eq Z (reduce Message cardinal_count (b x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: or (not (@eq Site x s1)) (not (@eq Site y s2)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  auto.
Qed.

End CARDINAL_EFFECT.


Section WEIGHT_EFFECT2.

Lemma sigma_weight_post_message :
 forall (m : Message) (s1 s2 : Site) (b : Bag_of_message),
 sigma_weight (Post_message Message m b s1 s2) =
 (sigma_weight b + cardinal_count m)%Z.
Proof.
(* Goal: @eq Z (sigma_weight (change_queue (queue Message) b s1 s2 q)) (Z.sub (Z.sub (sigma_weight b) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
  unfold sigma_weight in |- *.
(* Goal: forall (m : Message) (s1 s2 : Site) (b : Bag_of_message), @eq Z (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (Post_message Message m b s1 s2)) (Z.add (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
  unfold Post_message in |- *.
(* Goal: forall (m : Message) (s1 s2 : Site) (b : Bag_of_message) (_ : @eq (exc Message) (first Message (b s1 s2)) (value Message m)), @eq Z (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (change_queue (queue Message) b s1 s2 (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
  unfold change_queue in |- *.
(* Goal: forall (x y : Site) (_ : not (and (@eq Site x s1) (@eq Site y s2))), @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (update2_table Site eq_site_dec (queue Message) b s1 s2 (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
  rewrite sigma_table2_change.
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) (change_queue (queue Message) b s1 s2 q)) (reduce Message cardinal_count q)) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) b) (reduce Message cardinal_count (input Message dec (input Message (inc_dec s3) q)))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal (b s1 s2))) (Z.sub (cardinal (b s1 s2)) (cardinal_count m))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
(* Goal: @eq (exc Message) (first Message (b s1 s2)) (value Message m) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  omega.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
Qed.

Lemma sigma_weight_collect_message :
 forall (m : Message) (s1 s2 : Site) (b : Bag_of_message),
 first Message (b s1 s2) = value Message m ->
 sigma_weight (Collect_message Message b s1 s2) =
 (sigma_weight b - cardinal_count m)%Z.
Proof.
(* Goal: @eq Z (sigma_weight (change_queue (queue Message) b s1 s2 q)) (Z.sub (Z.sub (sigma_weight b) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
  unfold sigma_weight in |- *.
(* Goal: forall (m : Message) (s1 s2 : Site) (b : Bag_of_message) (_ : @eq (exc Message) (first Message (b s1 s2)) (value Message m)), @eq Z (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (Collect_message Message b s1 s2)) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
  unfold Collect_message in |- *.
(* Goal: forall (m : Message) (s1 s2 : Site) (b : Bag_of_message) (_ : @eq (exc Message) (first Message (b s1 s2)) (value Message m)), @eq Z (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (change_queue (queue Message) b s1 s2 (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
  unfold change_queue in |- *.
(* Goal: forall (x y : Site) (_ : not (and (@eq Site x s1) (@eq Site y s2))), @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  intros.
(* Goal: @eq Z (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (update2_table Site eq_site_dec (queue Message) b s1 s2 (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
  rewrite sigma_table2_change.
(* Goal: @eq Z (Z.add (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal (b s1 s2))) (cardinal (first_out Message (b s1 s2)))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  rewrite cardinal_first_out with (m := m).
(* Goal: @eq Z (Z.add (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal (b s1 s2))) (Z.sub (cardinal (b s1 s2)) (cardinal_count m))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
(* Goal: @eq (exc Message) (first Message (b s1 s2)) (value Message m) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  omega.
(* Goal: @eq Z (reduce Message cardinal_count (b x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: or (not (@eq Site x s1)) (not (@eq Site y s2)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  auto.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
Qed.

Remark add_reduce :
 forall x y z w a : Z, x = a -> (x + y)%Z = (a + (y + z + w) - w - z)%Z.
Proof.
(* Goal: @eq Z (Z.add (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal (b s1 s2))) (Z.sub (cardinal (b s1 s2)) (cardinal_count m))) (Z.sub (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) b) (cardinal_count m)) *)
(* Goal: @eq (exc Message) (first Message (b s1 s2)) (value Message m) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
intros; omega.
Qed.


Lemma sigma_weight_change_queue :
 forall (s1 s2 s3 : Site) (b : Bag_of_message) (q : queue Message),
 b s1 s2 = input Message dec (input Message (inc_dec s3) q) ->
 sigma_weight (change_queue (queue Message) b s1 s2 q) =
 (sigma_weight b - cardinal_count dec - cardinal_count (inc_dec s3))%Z.
Proof.
(* Goal: forall (x y : Site) (_ : not (and (@eq Site x s1) (@eq Site y s2))), @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  intros.
(* Goal: @eq Z (sigma_weight (change_queue (queue Message) b s1 s2 q)) (Z.sub (Z.sub (sigma_weight b) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
  unfold sigma_weight in |- *.
  rewrite
   sigma2_sigma2_but_x_y
                         with
                         (s0 := s1)
                        (s1 := s2)
                        (eq_site_dec := eq_site_dec).
  rewrite
   sigma2_sigma2_but_x_y
                         with
                         (s0 := s1)
                        (s1 := s2)
                        (eq_site_dec := eq_site_dec).
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => cardinal) (change_queue (queue Message) b s1 s2 q)) (cardinal (change_queue (queue Message) b s1 s2 q s1 s2))) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => cardinal) b) (cardinal (b s1 s2))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  unfold cardinal in |- *.
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) (change_queue (queue Message) b s1 s2 q)) (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q s1 s2))) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) b) (reduce Message cardinal_count (b s1 s2))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  rewrite that_queue.
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) (change_queue (queue Message) b s1 s2 q)) (reduce Message cardinal_count q)) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) b) (reduce Message cardinal_count (b s1 s2))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  rewrite H.
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) (change_queue (queue Message) b s1 s2 q)) (reduce Message cardinal_count q)) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) b) (reduce Message cardinal_count (input Message dec (input Message (inc_dec s3) q)))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) (change_queue (queue Message) b s1 s2 q)) (reduce Message cardinal_count q)) (Z.sub (Z.sub (Z.add (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) b) (Z.add (Z.add (reduce Message cardinal_count q) (cardinal_count (inc_dec s3))) (cardinal_count dec))) (cardinal_count dec)) (cardinal_count (inc_dec s3))) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply add_reduce.
(* Goal: @eq Z (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) (change_queue (queue Message) b s1 s2 q)) (sigma2_but_table Site eq_site_dec LS LS (queue Message) s1 s2 (fun _ _ : Site => reduce Message cardinal_count) b) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply sigma2_but_simpl2.
(* Goal: forall (x y : Site) (_ : not (and (@eq Site x s1) (@eq Site y s2))), @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  intros.
(* Goal: @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  case (eq_queue_dec s1 x s2 y); intro.
(* Goal: @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  elim H0.
(* Goal: @eq Z (reduce Message cardinal_count (b x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: or (not (@eq Site x s1)) (not (@eq Site y s2)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  split; decompose [and] a; auto.
  
(* Goal: @eq Z (reduce Message cardinal_count (change_queue (queue Message) b s1 s2 q x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  rewrite other_queue.
(* Goal: @eq Z (reduce Message cardinal_count (b x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: or (not (@eq Site x s1)) (not (@eq Site y s2)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  auto.
  
(* Goal: @eq Z (reduce Message cardinal_count (b x y)) (reduce Message cardinal_count (b x y)) *)
(* Goal: or (not (@eq Site x s1)) (not (@eq Site y s2)) *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
(* Goal: only_once Site eq_site_dec s1 LS *)
(* Goal: only_once Site eq_site_dec s2 LS *)
  elim o; auto.
  
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
  
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
  
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
  
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
  
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
  
(* Goal: only_once Site eq_site_dec s2 LS *)
  apply finite_site.
Qed.

End WEIGHT_EFFECT2.
