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

Unset Standard Proposition Elimination Names.

Section MESSAGE.

Lemma not_s1_s2 : forall s s1 s2 : Site, s1 <> s2 -> s1 <> s \/ s2 <> s.
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 s)) *)
  case (eq_site_dec s1 s).
(* Goal: forall _ : @eq Site s1 s, or (not (@eq Site s1 s)) (not (@eq Site s2 s)) *)
(* Goal: forall _ : not (@eq Site s1 s), or (not (@eq Site s1 s)) (not (@eq Site s2 s)) *)
  intro; rewrite e.
(* Goal: or (not (@eq Site s s)) (not (@eq Site s2 s)) *)
(* Goal: forall _ : not (@eq Site s1 s), or (not (@eq Site s1 s)) (not (@eq Site s2 s)) *)
  rewrite e in H.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  right; auto.
  
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  left; auto.
Qed.


Lemma not_owner_inc :
 forall (c : Config) (s1 s2 : Site),
 legal c -> ~ In_queue Message (inc_dec owner) (bm c s1 s2).
Proof.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro; intro; intro.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
  elim H.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simple induction t; intros; simpl in |- *.
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec owner) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
  
(* Goal: not (In_queue Message (inc_dec owner) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
  
(* Goal: not (In_queue Message (inc_dec owner) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec owner) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_post.
(* Goal: not (@eq Message (inc_dec owner) (inc_dec s0)) *)
(* Goal: not (In_queue Message (inc_dec owner) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  injection.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
  
(* Goal: not (In_queue Message (inc_dec owner) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec owner) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.

(* as formulated by Jean *)

Lemma not_owner_inc2 :
 forall (c : Config) (s0 s1 s2 : Site),
 legal c -> In_queue Message (inc_dec s0) (bm c s1 s2) -> s0 <> owner.
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s0 owner) *)
  generalize (not_owner_inc c s1 s2 H).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
  generalize
   (equality_from_queue_membership Message eq_message_dec 
      (inc_dec owner) (inc_dec s0) (bm c s1 s2)).
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s0 owner) *)
  generalize (H2 H0 H1).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (In_queue Message copy (input Message dec (Collect_message Message (bm c) owner s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_site_dec s0 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  rewrite e in H3.
(* Goal: not (@eq Site s0 owner) *)
(* Goal: forall _ : not (@eq Site s0 owner), not (@eq Site s0 owner) *)
  generalize H3.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.

(* As I need it in my proof *)

Lemma not_owner_inc3 :
 forall (c : Config) (s1 s2 : Site),
 legal c ->
 forall s0 : Site, In_queue Message (inc_dec s0) (bm c s1 s2) -> s0 <> owner.
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s0 owner) *)
  apply (not_owner_inc2 c s0 s1 s2).
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.

Lemma not_owner_inc4 :
 forall (c : Config) (s1 s2 : Site),
 legal c ->
 forall (m : Message) (s0 : Site),
 m = inc_dec s0 -> In_queue Message m (bm c s1 s2) -> s0 <> owner.
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s0 owner) *)
  apply (not_owner_inc2 c s0 s1 s2).
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: In_queue Message (inc_dec s0) (bm c s1 s2) *)
  rewrite H0 in H1.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.


(* The proof is long and very boring, but it is a simple case
   analysis.  Could it be possible to simplify it? *)

Lemma no_copy_to_owner :
 forall c0 : Config,
 legal c0 -> forall s1 : Site, ~ In_queue Message copy (bm c0 s1 owner).
Proof.
(* Goal: forall (c0 : Config) (_ : legal c0) (s1 : Site), not (In_queue Message copy (bm c0 s1 owner)) *)
  intros c0 H.
(* Goal: forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
  elim H.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simple induction t; intros; simpl in |- *.

  (* 1 *)

(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  right; auto.

  (* 2 *)

(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_queue_dec s1 s0 s2 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H2; rewrite H3.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite collect_here.
(* Goal: not (In_queue Message m1 (first_out Message (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
  apply not_in_q_output.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 owner) owner s3 s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  intro; rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 3 *)
  
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 owner) owner s3 s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_queue_dec owner s3 s0 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 owner) owner s3 s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site owner s3)) (not (@eq Site s0 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 owner) owner s3 s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H3; rewrite <- H2.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s5) s5 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_here.
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: or (not (@eq Site owner s)) (not (@eq Site s3 s)) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  case (eq_site_dec s1 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3)), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: or (not (@eq Site owner s)) (not (@eq Site s3 s)) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  rewrite e0.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite collect_here.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message copy dec) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : not (@eq Site s0 owner), not (In_queue Message copy (input Message dec (Collect_message Message (bm c) owner s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H1 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (or (@eq Message copy dec) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : not (@eq Site s0 owner), not (In_queue Message copy (input Message dec (Collect_message Message (bm c) owner s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (not_in_q_output Message copy (bm c owner owner)).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (or (@eq Message copy dec) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : not (@eq Site s1 owner), not (In_queue Message copy (input Message dec (Collect_message Message (bm c) s1 owner owner owner))) *)
(* Goal: forall _ : or (not (@eq Site owner s3)) (not (@eq Site s0 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 owner) owner s3 s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H5 H4).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: forall (_ : not (@eq Site s0 s1)) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  unfold not in |- *.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message copy dec) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : not (@eq Site s0 owner), not (In_queue Message copy (input Message dec (Collect_message Message (bm c) owner s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H1 owner).
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  left; auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s1 owner s0 owner)) *)
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s3 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_site_dec s1 s0).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3)), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: or (not (@eq Site owner s)) (not (@eq Site s3 s)) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  rewrite e0.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite collect_here.
(* Goal: not (In_queue Message m1 (first_out Message (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
  apply not_in_q_output.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s3 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  decompose [or] o.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  right; auto.
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  left; auto.

  (* 4 *)
  
(* Goal: not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_queue_dec s2 s0 s1 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H2; rewrite H3.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s5) s5 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_here.
(* Goal: not (In_queue Message copy (input Message dec (Collect_message Message (bm c) owner s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_site_dec s0 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite e1; rewrite collect_here.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message copy dec) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : not (@eq Site s0 owner), not (In_queue Message copy (input Message dec (Collect_message Message (bm c) owner s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (not_in_q_output Message copy (bm c owner owner)).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (or (@eq Message copy dec) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : not (@eq Site s0 owner), not (In_queue Message copy (input Message dec (Collect_message Message (bm c) owner s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H1 owner).
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message copy (inc_dec s1)) (In_queue Message copy (bm c s0 owner))) *)
(* Goal: or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H1 s0).
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: or (not (@eq Site owner s0)) (not (@eq Site s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s1 owner)), not (In_queue Message copy (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1 s0 owner)) *)
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  right; auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_queue_dec s1 s0 s2 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H2; rewrite H3; rewrite collect_here.
(* Goal: not (In_queue Message m1 (first_out Message (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
  apply not_in_q_output.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 5 *)
  
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_queue_dec owner s1 s2 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: forall _ : or (not (@eq Site owner s1)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) owner s2 s1 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite <- H2; rewrite H3.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite collect_here.
(* Goal: not (In_queue Message m1 (first_out Message (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
  apply not_in_q_output.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 6 *)
  
(* Goal: @eq bool (Set_rec_table (rt c) s2 s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  case (eq_site_dec s2 s0).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy), @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 s2), @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  rewrite e1.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s5) s5 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_here.
(* Goal: not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_queue_dec s1 s0 s0 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)), not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H2; rewrite <- H3.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite collect_here.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message copy (inc_dec s0)) (In_queue Message copy (first_out Message (bm c s0 s0)))) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)), not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (not_in_q_output Message copy (bm c s0 s0)).
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (or (@eq Message copy (inc_dec s1)) (In_queue Message copy (bm c s0 owner))) *)
(* Goal: or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H1 s0).
(* Goal: forall _ : not (In_queue Message copy (bm c s0 owner)), not (or (@eq Message copy (inc_dec s0)) (In_queue Message copy (first_out Message (bm c s0 s0)))) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)), not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H3.
(* Goal: forall _ : not (In_queue Message copy (bm c owner owner)), not (or (@eq Message copy (inc_dec owner)) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)), not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H3 in H4.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (or (@eq Message copy (inc_dec owner)) (In_queue Message copy (first_out Message (bm c owner owner)))) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)), not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H4 H5).
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message copy (inc_dec s1)) (In_queue Message copy (bm c s0 owner))) *)
(* Goal: or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H1 s0).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_queue_dec s1 s0 s2 owner).
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H2; rewrite H3.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite collect_here.
(* Goal: not (In_queue Message m1 (first_out Message (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
  apply not_in_q_output.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  left; auto.

  (* 7 *)
  
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  case (eq_site_dec s s1).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy), @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 s2), @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  rewrite e1.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s5) s5 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_here.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message copy dec) (In_queue Message copy (bm c s1 owner))) *)
(* Goal: forall _ : not (@eq Site s s1), not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  generalize (H1 s1).
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.

Qed.


Lemma empty_q_to_me :
 forall c : Config, legal c -> forall s : Site, bm c s s = empty Message.
Proof.
(* Goal: forall (c : Config) (_ : legal c) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c s5 owner)), not (@eq Site s1 s5) *)
  intros c H.
(* Goal: forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
  elim H.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: @eq (queue Message) (bag_init s s) (empty Message) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall s : Site, @eq (queue Message) (bm c s s) (empty Message)) (s : Site), @eq (queue Message) (bm (transition c t) s s) (empty Message) *)
  unfold bag_init in |- *.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simple induction t; intros; simpl in |- *.

  (* 1 *)

(* Goal: not (@eq Site s s0) *)
  rewrite post_elsewhere; auto.
(* Goal: not (@eq Site s s0) *)
  apply not_s1_s2; auto.

  (* 2 *)
  
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  case (eq_site_dec s1 s2).
(* Goal: forall _ : @eq Site s1 s2, @eq (queue Message) (Collect_message Message (bm c0) s1 s2 s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 s2), @eq (queue Message) (Collect_message Message (bm c0) s1 s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  intro; generalize e.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3)), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: or (not (@eq Site owner s)) (not (@eq Site s3 s)) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  rewrite e0.
(* Goal: forall _ : forall _ : @eq Site s s2, @eq (queue Message) (bm c s s2) (empty Message), @eq (queue Message) (bm c s s2) (empty Message) *)
  rewrite H1.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  simpl in |- *; intro; discriminate.
  
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s s0) *)
  rewrite collect_elsewhere; auto.
(* Goal: not (@eq Site s s0) *)
  apply not_s1_s2; auto.
 
  (* 3 *)
 
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  generalize (not_owner_inc2 c0 s3 s1 owner H0).
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: or (not (@eq Site owner s)) (not (@eq Site s3 s)) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  case (eq_site_dec s1 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: or (not (@eq Site owner s)) (not (@eq Site s3 s)) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  generalize e.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3)), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 owner), @eq (queue Message) (Collect_message Message (bm c0) s1 owner s s) (empty Message) *)
(* Goal: or (not (@eq Site owner s)) (not (@eq Site s3 s)) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  rewrite e0.
(* Goal: forall _ : forall _ : @eq Site s s2, @eq (queue Message) (bm c s s2) (empty Message), @eq (queue Message) (bm c s s2) (empty Message) *)
  rewrite H1.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  simpl in |- *; intro; discriminate.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s s0) *)
  rewrite collect_elsewhere; auto.
(* Goal: not (@eq Site s s0) *)
  apply not_s1_s2; auto.
  
(* Goal: not (@eq Site s s0) *)
  apply not_s1_s2; auto.
(* Goal: not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : not (@eq Site s2 owner), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  cut (s3 <> owner).
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (@eq Site s3 owner) *)
(* Goal: @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  apply H2.
(* Goal: In_queue Message copy (bm c0 s0 s3) *)
(* Goal: forall _ : not (@eq Site s2 owner), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply first_in.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 4 *)
  
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  case (eq_site_dec s1 s2).
(* Goal: forall _ : @eq Site s1 s2, @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 s2), @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  intro; generalize e0.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy), @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 s2), @eq (queue Message) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  rewrite e1.
(* Goal: forall _ : forall _ : @eq Site s s2, @eq (queue Message) (bm c s s2) (empty Message), @eq (queue Message) (bm c s s2) (empty Message) *)
  rewrite H1.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  intro; discriminate.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site s s0)) (not (@eq Site owner s0)) *)
  apply not_s1_s2.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site s s0)) (not (@eq Site owner s0)) *)
  apply not_s1_s2.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 5 *)
  
(* Goal: @eq (queue Message) (Collect_message Message (bm c0) owner s2 s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  case (eq_site_dec owner s2).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  generalize e0; rewrite e1; simpl in |- *.
(* Goal: forall _ : forall _ : @eq Site s s2, @eq (queue Message) (bm c s s2) (empty Message), @eq (queue Message) (bm c s s2) (empty Message) *)
  rewrite H1.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  intro; discriminate.
  
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: or (not (@eq Site s s0)) (not (@eq Site owner s0)) *)
  apply not_s1_s2.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 6 *)
  
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  case (eq_site_dec s1 s2).
(* Goal: forall _ : @eq Site s1 s2, @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: forall _ : not (@eq Site s1 s2), @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  intro; generalize e0.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  rewrite e1; simpl in |- *.
(* Goal: forall _ : forall _ : @eq Site s s2, @eq (queue Message) (bm c s s2) (empty Message), @eq (queue Message) (bm c s s2) (empty Message) *)
  rewrite H1.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  simpl in |- *; intro; discriminate.
  
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  generalize (no_copy_to_owner c0 H0 s1).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: @eq (queue Message) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s s) (empty Message) *)
(* Goal: @eq (queue Message) (Post_message Message dec (bm c0) s owner s0 s0) (empty Message) *)
  case (eq_site_dec s2 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  elim H2.
(* Goal: In_queue Message copy (bm c0 s0 s3) *)
(* Goal: forall _ : not (@eq Site s2 owner), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply first_in.
(* Goal: not (@eq Site s s0) *)
  rewrite <- e1; auto.
  
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site s s0)) (not (@eq Site owner s0)) *)
  apply not_s1_s2.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site s s0)) (not (@eq Site owner s0)) *)
  apply not_s1_s2.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 7 *)
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site s s0)) (not (@eq Site owner s0)) *)
  apply not_s1_s2.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.

Lemma not_reflexive :
 forall c : Config,
 legal c ->
 forall s1 s5 : Site,
 In_queue Message (inc_dec s1) (bm c s5 owner) -> s1 <> s5.
Proof.
(* Goal: forall (c : Config) (_ : legal c) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c s5 owner)), not (@eq Site s1 s5) *)
  intros c H.
(* Goal: forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
  elim H.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c t) s5 owner)), not (@eq Site s1 s5) *)
  intros c0 t.
(* Goal: forall (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c t) s0) Z0), @eq bool (rt (transition c t) s0) true *)
  elim t.

  (* 1 *)

(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message dec)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_dec c0 s1 s2 e)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c0 s1 owner)) (value Message (inc_dec s3))) (_ : legal c0) (_ : forall (s2 s5 : Site) (_ : In_queue Message (inc_dec s2) (bm c0 s5 owner)), not (@eq Site s2 s5)) (s2 s5 : Site) (_ : In_queue Message (inc_dec s2) (bm (transition c0 (receive_inc c0 s1 s3 e)) s5 owner)), not (@eq Site s2 s5) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) true) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy1 c0 s1 s2 e e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c0 s2) false) (e0 : @eq (exc Message) (first Message (bm c0 owner s2)) (value Message copy)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (receive_copy2 c0 s2 e e0)) s5 owner)), not (@eq Site s1 s5) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy3 c0 s1 s2 e n e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  apply (in_post Message (inc_dec s0) copy (bm c0) s1 s2).
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 2 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  apply (in_collect Message (inc_dec s0) (bm c0) s1 s2).
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 3 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) true) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy1 c0 s1 s2 e e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c0 s2) false) (e0 : @eq (exc Message) (first Message (bm c0 owner s2)) (value Message copy)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (receive_copy2 c0 s2 e e0)) s5 owner)), not (@eq Site s1 s5) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy3 c0 s1 s2 e n e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  apply (in_collect Message (inc_dec s0) (bm c0) s1 owner).
(* Goal: not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  generalize H2.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s5 owner), In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 owner s5 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) true) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy1 c0 s1 s2 e e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c0 s2) false) (e0 : @eq (exc Message) (first Message (bm c0 owner s2)) (value Message copy)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (receive_copy2 c0 s2 e e0)) s5 owner)), not (@eq Site s1 s5) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy3 c0 s1 s2 e n e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  case (eq_queue_dec owner s5 s3 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: forall _ : not (In_queue Message copy (bm c s0 owner)), not (or (@eq Message copy (inc_dec s0)) (In_queue Message copy (first_out Message (bm c s0 s0)))) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s0 owner)), not (In_queue Message copy (input Message (inc_dec s1) (Collect_message Message (bm c) s1 s0 s0 owner))) *)
(* Goal: forall _ : not (@eq Site s2 s0), not (In_queue Message copy (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2) s2 owner s0 owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
  rewrite H4; rewrite H3.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s5) s5 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_here.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 4 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  apply (in_collect Message (inc_dec s0) (bm c0) s1 s2).
(* Goal: not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  generalize H2.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s5 owner), In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s2 s5 owner) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c0 s2) false) (e0 : @eq (exc Message) (first Message (bm c0 owner s2)) (value Message copy)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (receive_copy2 c0 s2 e e0)) s5 owner)), not (@eq Site s1 s5) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy3 c0 s1 s2 e n e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  case (eq_queue_dec s2 s5 s1 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s5 owner), In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s2 s5 owner) *)
(* Goal: forall (_ : or (not (@eq Site s2 s5)) (not (@eq Site s1 owner))) (_ : In_queue Message (inc_dec s0) (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s5 owner)), In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s2 s5 owner) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c0 s2) false) (e0 : @eq (exc Message) (first Message (bm c0 owner s2)) (value Message copy)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (receive_copy2 c0 s2 e e0)) s5 owner)), not (@eq Site s1 s5) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy3 c0 s1 s2 e n e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite H3; rewrite H4.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s5) s5 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_here.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
  intuition.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 5 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: In_queue Message (inc_dec s1) (bm c0 s5 owner) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c0 s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy)) (_ : legal c0) (_ : forall (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm c0 s5 owner)), not (@eq Site s3 s5)) (s3 s5 : Site) (_ : In_queue Message (inc_dec s3) (bm (transition c0 (receive_copy3 c0 s1 s2 e n e0)) s5 owner)), not (@eq Site s3 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  apply (in_collect Message (inc_dec s1) (bm c0) owner s2).
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 6 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  case (eq_site_dec s2 s5).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite e1 in H2.
(* Goal: not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  generalize H2.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s5) s5 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_here.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  case (eq_queue_dec s1 s5 s5 owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  decompose [and] a.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  elim n.
(* Goal: not (@eq Site s s0) *)
  rewrite H3; auto.  
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite collect_elsewhere.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  generalize (H1 s0 s5).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  case (eq_site_dec s0 s1).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (@eq Site s0 s5) *)
(* Goal: forall (_ : not (@eq Site s0 s1)) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite <- e1; rewrite e2.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: forall (_ : not (@eq Site s0 s1)) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: False *)
(* Goal: forall (_ : not (@eq Site s0 s1)) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  generalize e0.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy), False *)
(* Goal: forall (_ : not (@eq Site s0 s1)) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite H5.
(* Goal: forall _ : @eq (exc Message) (first Message (bm c0 s2 s2)) (value Message copy), False *)
(* Goal: forall (_ : not (@eq Site s0 s1)) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (bm c0 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite empty_q_to_me.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.  
(* Goal: not (@eq Site s s0) *)
  auto.  
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s0 s5) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  apply H3.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  elim H4.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (bm c0 s5 owner), In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  elim n0.
(* Goal: @eq Site s0 s1 *)
(* Goal: forall _ : In_queue Message (inc_dec s0) (bm c0 s5 owner), In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: or (not (@eq Site s1 s5)) (not (@eq Site s5 owner)) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  inversion H5.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  generalize H2.
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  rewrite post_elsewhere.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: In_queue Message (inc_dec s0) (bm c0 s5 owner) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  apply (in_collect Message (inc_dec s0) (bm c0) s1 s2).
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  left; auto.

  (* 7 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: In_queue Message (inc_dec s1) (bm c0 s5 owner) *)
  apply (in_post Message (inc_dec s1) dec (bm c0) s owner).
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.

Lemma not_in_queue_post :
 forall (b : Bag_of_message) (s1 s2 s3 s4 : Site) (m1 m2 : Message),
 m1 <> m2 ->
 ~ In_queue Message m1 (b s1 s2) ->
 ~ In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2).
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
   intros.
(* Goal: not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
   case (eq_queue_dec s3 s1 s4 s2).
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
   intro; decompose [and] a.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
   rewrite H1; rewrite H2; rewrite post_here; simpl in |- *.
(* Goal: not (or (@eq Message m1 m2) (In_queue Message m1 (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2)) *)
   intuition.
(* Goal: not (@eq Site s s0) *)
   intros; rewrite post_elsewhere; auto.
Qed.

           
Lemma not_in_queue_collect :
 forall (b : Bag_of_message) (s1 s2 s3 s4 : Site) (m1 : Message),
 ~ In_queue Message m1 (b s1 s2) ->
 ~ In_queue Message m1 (Collect_message Message b s3 s4 s1 s2).
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
   intros.
(* Goal: not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
   case (eq_queue_dec s3 s1 s4 s2).
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
   intro; decompose [and] a.
(* Goal: not (In_queue Message copy (Collect_message Message (bm c) s0 owner s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (In_queue Message copy (Collect_message Message (bm c) s1 s2 s0 owner)) *)
(* Goal: or (not (@eq Site s2 s0)) (not (@eq Site owner owner)) *)
(* Goal: not (In_queue Message copy (Post_message Message dec (bm c) s owner s1 owner)) *)
   rewrite H0; rewrite H1; rewrite collect_here.
(* Goal: not (In_queue Message m1 (first_out Message (b s1 s2))) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site s4 s2)), not (In_queue Message m1 (Collect_message Message b s3 s4 s1 s2)) *)
   apply not_in_q_output.
(* Goal: not (@eq Site s s0) *)
   auto.
(* Goal: not (@eq Site s s0) *)
   intro; rewrite collect_elsewhere; auto.
Qed.


Lemma inc_dec_owner :
 forall (c : Config) (s1 s2 : Site),
 legal c ->
 s1 = owner \/ s2 <> owner ->
 forall s0 : Site, ~ In_queue Message (inc_dec s0) (bm c s1 s2).
Proof.
(* Goal: forall (c : Config) (s1 s2 : Site) (_ : legal c) (_ : or (@eq Site s1 owner) (not (@eq Site s2 owner))) (s0 : Site), not (In_queue Message (inc_dec s0) (bm c s1 s2)) *)
  intros c s1 s2 H.
(* Goal: forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
  elim H.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: not (@eq Site s s0) *)
  intros; unfold not in |- *; auto.
  
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  simple induction t; simpl in |- *; intros.
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
  
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec s4) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: or (not (@eq Site s3 s1)) (not (@eq Site owner s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
  
(* Goal: not (@eq Site s s0) *)
  apply not_in_queue_collect; auto.
  
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
  
(* Goal: not (In_queue Message (inc_dec s4) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: or (not (@eq Site s3 s1)) (not (@eq Site owner s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec s4) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: or (not (@eq Site s3 s1)) (not (@eq Site owner s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  case (eq_queue_dec s3 s1 owner s2).
(* Goal: forall _ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner)), not (@eq Site s0 s5) *)
(* Goal: forall (_ : or (not (@eq Site s1 s5)) (not (@eq Site s5 owner))) (_ : or (@eq Message (inc_dec s0) (inc_dec s1)) (In_queue Message (inc_dec s0) (Collect_message Message (bm c0) s1 s5 s5 owner))), not (@eq Site s0 s5) *)
(* Goal: forall _ : not (@eq Site s2 s5), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  intro; decompose [and] a.
(* Goal: not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  elim H2.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : not (@eq Site s2 owner), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  cut (s3 <> owner).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (@eq Site s3 owner) *)
(* Goal: forall _ : not (@eq Site s2 owner), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  elim H6.
(* Goal: not (@eq Site s s0) *)
  rewrite H3; rewrite H5; auto.
  
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  unfold not in |- *; intro.
(* Goal: False *)
(* Goal: forall _ : not (@eq Site s2 owner), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  generalize (no_copy_to_owner c0 H0 s0).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (@eq Site s s0) *)
  elim H7; rewrite <- H6; auto.
(* Goal: In_queue Message copy (bm c0 s0 s3) *)
(* Goal: forall _ : not (@eq Site s2 owner), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: forall _ : or (not (@eq Site s3 s1)) (not (@eq Site owner s2)), not (In_queue Message (inc_dec s4) (Post_message Message (inc_dec s0) (Collect_message Message (bm c0) s0 s3) s3 owner s1 s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply first_in.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (@eq Site s s0) *)
  elim H3; auto.
  
(* Goal: forall _ : In_queue Message (inc_dec s0) (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s5) *)
(* Goal: forall (s : Site) (e : @eq Z (st c0 s) Z0) (e0 : @eq bool (rt c0 s) true) (n : not (@eq Site s owner)) (_ : legal c0) (_ : forall (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm c0 s5 owner)), not (@eq Site s1 s5)) (s1 s5 : Site) (_ : In_queue Message (inc_dec s1) (bm (transition c0 (delete_entry c0 s e e0 n)) s5 owner)), not (@eq Site s1 s5) *)
  intro; rewrite post_elsewhere.
(* Goal: not (In_queue Message (inc_dec s4) (Collect_message Message (bm c0) s0 s3 s1 s2)) *)
(* Goal: or (not (@eq Site s3 s1)) (not (@eq Site owner s2)) *)
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_collect.
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (@eq Site s s0) *)
  auto.
  
(* Goal: not (In_queue Message (inc_dec s0) (Post_message Message dec (bm c0) s owner s1 s2)) *)
  apply not_in_queue_post.
(* Goal: not (@eq Message (inc_dec s0) dec) *)
(* Goal: not (In_queue Message (inc_dec s0) (bm c0 s1 s2)) *)
  discriminate.
  
(* Goal: not (@eq Site s s0) *)
  auto.
    
Qed.


Lemma inc_dec_owner2 :
 forall (c : Config) (s1 s2 : Site),
 legal c ->
 s1 <> owner ->
 s2 <> owner ->
 forall s0 : Site, ~ In_queue Message (inc_dec s0) (bm c s1 s2).
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
intros.
(* Goal: not (@eq Site s s0) *)
apply inc_dec_owner; auto.
Qed.

Lemma inc_dec_owner3 :
 forall (c : Config) (s1 s2 : Site),
 legal c ->
 s2 <> owner ->
 forall s0 : Site, ~ In_queue Message (inc_dec s0) (bm c s1 s2).
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
intros.
(* Goal: not (@eq Site s s0) *)
apply inc_dec_owner; auto.
Qed.


Lemma inc_dec_owner4 :
 forall (c : Config) (s1 s2 : Site),
 legal c ->
 s1 = owner -> forall s0 : Site, ~ In_queue Message (inc_dec s0) (bm c s1 s2).
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
intros.
(* Goal: not (@eq Site s s0) *)
apply inc_dec_owner; auto.
Qed.

Lemma empty_queue1 :
 forall c : Config,
 legal c -> forall s1 s2 : Site, s1 = s2 -> bm c s1 s2 = empty Message.
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
intros.
(* Goal: @eq (queue Message) (bm c s1 s2) (empty Message) *)
generalize (empty_q_to_me c H s1).
(* Goal: forall _ : forall _ : @eq Site s1 s2, @eq (queue Message) (bm c s1 s2) (empty Message), @eq (queue Message) (bm c s1 s2) (empty Message) *)
rewrite H0.
(* Goal: not (@eq Site s s0) *)
auto.
Qed.

Lemma empty_queue2 :
 forall c : Config,
 legal c ->
 forall s1 s2 s : Site, s1 = s -> s2 = s -> bm c s1 s2 = empty Message.
Proof.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq (queue Message) (bm c s1 s2) (empty Message) *)
  generalize (empty_queue1 c H s1 s2).
(* Goal: forall _ : forall _ : @eq Site s1 s2, @eq (queue Message) (bm c s1 s2) (empty Message), @eq (queue Message) (bm c s1 s2) (empty Message) *)
  rewrite H0.
(* Goal: forall _ : forall _ : @eq Site s s2, @eq (queue Message) (bm c s s2) (empty Message), @eq (queue Message) (bm c s s2) (empty Message) *)
  rewrite H1.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.

Lemma st_rt :
 forall (c0 : Config) (s0 : Site),
 legal c0 -> s0 <> owner -> (st c0 s0 > 0)%Z -> rt c0 s0 = true.
Proof.
(* Goal: forall (c0 : Config) (s0 : Site) (_ : legal c0) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
  intros c0 s0 H.
(* Goal: forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c0 s0) Z0), @eq bool (rt c0 s0) true *)
  elim H.
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (send_init s0) Z0), @eq bool (rec_init s0) true *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c t) s0) Z0), @eq bool (rt (transition c t) s0) true *)
  unfold send_init in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rec_init s0) true *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c t) s0) Z0), @eq bool (rt (transition c t) s0) true *)
  cut (~ (0 > 0)%Z).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (@eq Site s s0) *)
  elim H2; auto.
(* Goal: not (Z.gt Z0 Z0) *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  omega.

(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c t) s0) Z0), @eq bool (rt (transition c t) s0) true *)
  intros c t.
(* Goal: forall (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c t) s0) Z0), @eq bool (rt (transition c t) s0) true *)
  elim t.

  (* 1 *)

(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s1 s2 : Site) (_ : not (@eq Site s1 s2)) (_ : not (@eq Site s2 owner)) (_ : access s1 (rt c)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (Inc_send_table (st c) s1 s0) Z0), @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_dec c s1 s2 e)) s0) Z0), @eq bool (rt (transition c (receive_dec c s1 s2 e)) s0) true *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  intros s1 s2.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  case (eq_site_dec s0 s1); intro.
(* Goal: forall (_ : not (@eq Site s1 s2)) (_ : not (@eq Site s2 owner)) (_ : access s1 (rt c)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (Inc_send_table (st c) s1 s0) Z0), @eq bool (rt c s0) true *)
(* Goal: forall (_ : not (@eq Site s1 s2)) (_ : not (@eq Site s2 owner)) (_ : access s1 (rt c)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (Inc_send_table (st c) s1 s0) Z0), @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_dec c s1 s2 e)) s0) Z0), @eq bool (rt (transition c (receive_dec c s1 s2 e)) s0) true *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  unfold access in |- *.
(* Goal: forall (_ : not (@eq Site s1 s2)) (_ : not (@eq Site s2 owner)) (_ : or (@eq Site s1 owner) (@eq bool (rt c s1) true)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (Inc_send_table (st c) s1 s0) Z0), @eq bool (rt c s0) true *)
(* Goal: forall (_ : not (@eq Site s1 s2)) (_ : not (@eq Site s2 owner)) (_ : access s1 (rt c)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (Inc_send_table (st c) s1 s0) Z0), @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_dec c s1 s2 e)) s0) Z0), @eq bool (rt (transition c (receive_dec c s1 s2 e)) s0) true *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  rewrite e.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s1) true *)
(* Goal: forall (_ : not (@eq Site s1 s2)) (_ : not (@eq Site s2 owner)) (_ : access s1 (rt c)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (Inc_send_table (st c) s1 s0) Z0), @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_dec c s1 s2 e)) s0) Z0), @eq bool (rt (transition c (receive_dec c s1 s2 e)) s0) true *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  elim a.
(* Goal: not (@eq Site s s0) *)
  intro; elim H2; auto.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: Z.gt (st c s0) Z0 *)
(* Goal: forall (s1 s2 : Site) (e : @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_dec c s1 s2 e)) s0) Z0), @eq bool (rt (transition c (receive_dec c s1 s2 e)) s0) true *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  generalize H3; unfold Inc_send_table in |- *.
(* Goal: @eq bool (change_site bool (rt c) s false s0) true *)
  rewrite other_site.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  auto.


  (* 2 *)  

(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: Z.gt (st c s0) Z0 *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  generalize H3; unfold Dec_send_table in |- *.
(* Goal: forall _ : Z.gt (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) Z0, Z.gt (st c s0) Z0 *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  case (eq_site_dec s0 s2).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: forall _ : Z.gt (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) Z0, Z.gt (st c s0) Z0 *)
(* Goal: forall (_ : not (@eq Site s0 s2)) (_ : Z.gt (update_table Site eq_site_dec Z (st c) s2 (Z.sub (st c s2) (Zpos xH)) s0) Z0), Z.gt (st c s0) Z0 *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_inc c s1 s3 e)) s0) Z0), @eq bool (rt (transition c (receive_inc c s1 s3 e)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  rewrite e0; rewrite that_site.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: not (Z.gt Z0 Z0) *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  omega.
(* Goal: not (@eq Site s s0) *)
  intro; rewrite other_site; auto.

  (* 3 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (rt c s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy1 c s1 s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy1 c s1 s2 e e0)) s0) true *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy2 c s2 e e0)) s0) Z0), @eq bool (rt (transition c (receive_copy2 c s2 e e0)) s0) true *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (receive_copy3 c s1 s2 e n e0)) s0) Z0), @eq bool (rt (transition c (receive_copy3 c s1 s2 e n e0)) s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  apply H1.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: not (@eq Site s s0) *)
  generalize H3; unfold Inc_send_table in |- *; rewrite other_site; auto.
  
  (* 4 *)

(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: not (@eq Site s s0) *)
  apply H1; auto.

  (* 5 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (Set_rec_table (rt c) s2 s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  case (eq_site_dec s2 s0).
(* Goal: forall _ : @eq Site s2 s0, @eq bool (Set_rec_table (rt c) s2 s0) true *)
(* Goal: forall _ : not (@eq Site s2 s0), @eq bool (Set_rec_table (rt c) s2 s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  intro; unfold Set_rec_table in |- *.
(* Goal: not (@eq Site s s0) *)
  rewrite e1; rewrite that_site; auto.
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: @eq bool (change_site bool (rt c) s false s0) true *)
  unfold Set_rec_table in |- *; rewrite other_site.
(* Goal: not (@eq Site s s0) *)
  apply H1; auto.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 6 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (Set_rec_table (rt c) s2 s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  case (eq_site_dec s2 s0).
(* Goal: forall _ : @eq Site s2 s0, @eq bool (Set_rec_table (rt c) s2 s0) true *)
(* Goal: forall _ : not (@eq Site s2 s0), @eq bool (Set_rec_table (rt c) s2 s0) true *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  intro; unfold Set_rec_table in |- *.
(* Goal: not (@eq Site s s0) *)
  rewrite e1; rewrite that_site; auto.
(* Goal: @eq bool (change_site bool (rt c) s false s0) true *)
  intro; unfold Set_rec_table in |- *; rewrite other_site.
(* Goal: not (@eq Site s s0) *)
  apply H1; auto.
(* Goal: not (@eq Site s s0) *)
  auto.

  (* 7 *)
  
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st (transition c (delete_entry c s e e0 n)) s0) Z0), @eq bool (rt (transition c (delete_entry c s e e0 n)) s0) true *)
  simpl in |- *.
(* Goal: forall (s : Site) (_ : @eq Z (st c s) Z0) (_ : @eq bool (rt c s) true) (_ : not (@eq Site s owner)) (_ : legal c) (_ : forall (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (rt c s0) true) (_ : not (@eq Site s0 owner)) (_ : Z.gt (st c s0) Z0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intros.
(* Goal: @eq bool (Reset_rec_table (rt c) s s0) true *)
  case (eq_site_dec s s0).
(* Goal: forall _ : @eq Site s s0, @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro.
(* Goal: @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  rewrite <- e1 in H3.
(* Goal: @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  rewrite e in H3.
(* Goal: @eq bool (Reset_rec_table (rt c) s s0) true *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  absurd (0 > 0)%Z.
(* Goal: not (Z.gt Z0 Z0) *)
(* Goal: Z.gt Z0 Z0 *)
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  omega.
(* Goal: not (@eq Site s s0) *)
  auto.
(* Goal: forall _ : not (@eq Site s s0), @eq bool (Reset_rec_table (rt c) s s0) true *)
  intro; unfold Reset_rec_table in |- *.
(* Goal: @eq bool (change_site bool (rt c) s false s0) true *)
  rewrite other_site.
(* Goal: not (@eq Site s s0) *)
  apply H1; auto.
(* Goal: not (@eq Site s s0) *)
  auto.
Qed.



End MESSAGE.
