(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Export DistributedReferenceCounting.machine4.alternate.
Require Export DistributedReferenceCounting.machine4.invariant0.
Require Export DistributedReferenceCounting.machine4.invariant1.
Require Export DistributedReferenceCounting.machine4.invariant2.
Require Export DistributedReferenceCounting.machine4.invariant3.
Require Export DistributedReferenceCounting.machine4.invariant4.

Unset Standard Proposition Elimination Names.

(* Changes
   - proof of  1  for false_rt_D_queue.
   - proof of  1  for  legal_alternate.
   - owner_st_positive and its proof.
*)

Section INVARIANT5.

(* In this file, we establish the following inequality
   Int + Sum copy + Sum dec - Sum inc_dec >= 0

*) 


(* The message queue between a site and the owner has a particular
structure.  Messages dec and inc_dec are alternated.
 *)


Lemma legal_alternate :
 forall (s : Site) (c : Config),
 legal c ->
 alternate (bm c s owner) /\ (rt c s = false -> D_queue (bm c s owner)).
Proof.  
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: and (Z.ge (Z.add (reduce Message dec_count q) (Zpos xH)) (reduce Message new_inc_count q)) (forall _ : D_queue q, Z.ge (reduce Message dec_count q) (reduce Message new_inc_count q)) *)
  elim H.
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: alternate (bm config_init s owner) *)
(* Goal: forall _ : @eq bool (rt config_init s) false, D_queue (bm config_init s owner) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : and (alternate (bm c s owner)) (forall _ : @eq bool (rt c s) false, D_queue (bm c s owner))), and (alternate (bm (transition c t) s owner)) (forall _ : @eq bool (rt (transition c t) s) false, D_queue (bm (transition c t) s owner)) *)
  apply alt_null.
  
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: D_queue (bag_init s owner) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : and (alternate (bm c s owner)) (forall _ : @eq bool (rt c s) false, D_queue (bm c s owner))), and (alternate (bm (transition c t) s owner)) (forall _ : @eq bool (rt (transition c t) s) false, D_queue (bm (transition c t) s owner)) *)
  apply D_empty.
  
  (* 1 *)

(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  simple induction t; simpl in |- *; intros.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_queue_dec s1 s s2 owner); intro.
(* Goal: alternate (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: alternate (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: and (alternate (Collect_message Message (bm c0) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Collect_message Message (bm c0) s1 s2 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  decompose [and] a0.
(* Goal: alternate (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: alternate (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: and (alternate (Collect_message Message (bm c0) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Collect_message Message (bm c0) s1 s2 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite H4; rewrite H5; rewrite post_here.
(* Goal: alternate (input Message copy (bm c0 s owner)) *)
(* Goal: alternate (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: and (alternate (Collect_message Message (bm c0) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Collect_message Message (bm c0) s1 s2 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply alt_any_alt; auto.
(* Goal: forall s : Site, not (@eq Message dec (inc_dec s)) *)
(* Goal: alternate (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  intro; discriminate.
  
(* Goal: D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite post_elsewhere.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s1 s); intro.
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: and (alternate (Collect_message Message (bm c0) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Collect_message Message (bm c0) s1 s2 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  generalize a; unfold access in |- *.
(* Goal: forall _ : alternate (bm c0 s owner), alternate (append Message q1 (input Message copy q2)) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite e.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: D_queue (Post_message Message copy (bm c0) s s2 s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message copy (bm c0) s1 s2 s owner) *)
(* Goal: and (alternate (Collect_message Message (bm c0) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Collect_message Message (bm c0) s1 s2 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner)) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite H4 in a0.
(* Goal: forall _ : False, Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  discriminate.
  
(* Goal: D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite post_elsewhere.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  left; auto.
  
    
    (* 2 *)
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: legal c *)
  apply alt_collect; auto.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: legal c *)
  apply D_collect; auto.
    
    (* 3 *)
  
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: alternate (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply alt_post_elsewhere.
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  right.
(* Goal: not (@eq Site s3 owner) *)
(* Goal: D_queue (Collect_message Message (bm c0) s1 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply (not_owner_inc3 c0 s1 owner H0 s3).
(* Goal: In_queue Message (inc_dec s3) (bm c0 s1 owner) *)
(* Goal: D_queue (Collect_message Message (bm c0) s1 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply first_in.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  apply alt_collect; auto.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 owner) owner s3 s owner) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply D_post_elsewhere.
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  right.
(* Goal: not (@eq Site s3 owner) *)
(* Goal: D_queue (Collect_message Message (bm c0) s1 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply (not_owner_inc3 c0 s1 owner H0 s3).
(* Goal: In_queue Message (inc_dec s3) (bm c0 s1 owner) *)
(* Goal: D_queue (Collect_message Message (bm c0) s1 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner)) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply first_in.
(* Goal: legal c *)
  auto.
  
(* Goal: D_queue (Collect_message Message (bm c0) owner s2 s owner) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply D_collect.
(* Goal: Z.ge (reduce Message dec_count q) (reduce Message new_inc_count q) *)
  apply H3.
(* Goal: legal c *)
  auto.
    
    (* 4 *)
  
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  case (eq_queue_dec s2 s s1 owner); intros.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  decompose [and] a.
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite H4; rewrite H5.
(* Goal: alternate (Post_message Message dec (Collect_message Message (bm c0) owner s) s owner s owner) *)
(* Goal: alternate (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply alt_post_any.
(* Goal: forall s : Site, not (@eq Message dec (inc_dec s)) *)
(* Goal: alternate (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  intro; discriminate.
  
(* Goal: legal c *)
  apply alt_collect; auto.
  
(* Goal: legal c *)
  apply alt_post_elsewhere; auto.
(* Goal: legal c *)
  apply alt_collect; auto.
  
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  case (eq_queue_dec s2 s s1 owner); intros; simpl in |- *.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  decompose [and] a.
(* Goal: D_queue (bm c0 s1 s2) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite H5; rewrite H6.
(* Goal: D_queue (Post_message Message dec (bm c0) s owner s owner) *)
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply D_post_dec.
(* Goal: alternate (Collect_message Message (bm c0) owner s s owner) *)
(* Goal: D_queue (Post_message Message dec (Collect_message Message (bm c0) s1 s2) s2 s1 s owner) *)
(* Goal: and (alternate (Collect_message Message (bm c0) owner s2 s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner)) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply alt_collect.
(* Goal: legal c *)
  decompose [and] H1; auto.
  
(* Goal: D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite post_elsewhere.
(* Goal: D_queue (Collect_message Message (bm c0) owner s2 s owner) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply D_collect.
(* Goal: Z.ge (reduce Message dec_count q) (reduce Message new_inc_count q) *)
  apply H3.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
    
    (* 5 *)
    
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  decompose [and] H1; split.
(* Goal: alternate (Collect_message Message (bm c0) s1 s2 s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply alt_collect; trivial.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s s2); intro.
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Collect_message Message (bm c0) owner s2 s owner) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e1; unfold Set_rec_table in |- *; rewrite that_site.
(* Goal: forall s : Site, not (@eq Message dec (inc_dec s)) *)
(* Goal: alternate (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  intro; discriminate.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: D_queue (Collect_message Message (bm c0) owner s2 s owner) *)
(* Goal: and (alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) (forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply D_collect.
(* Goal: Z.ge (reduce Message dec_count q) (reduce Message new_inc_count q) *)
  apply H3.
(* Goal: legal c *)
  generalize H4; unfold Set_rec_table in |- *; rewrite other_site; auto.
    
    (* 6 *)
  
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  decompose [and] H1; split.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s2 s); intro.
(* Goal: alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e1; apply alt_post_inc.
(* Goal: alternate (Collect_message Message (bm c0) s1 s2 s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply alt_collect; trivial.
  
(* Goal: In_queue_before Message dec is_inc_dec (Collect_message Message (bm c0) s1 s s owner) *)
(* Goal: alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite collect_elsewhere.
(* Goal: In_queue_before Message dec is_inc_dec (bm c0 s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s owner)) *)
(* Goal: alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e1 in e.
(* Goal: In_queue_before Message dec is_inc_dec (bm c0 s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s owner)) *)
(* Goal: alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  generalize (H3 e).
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: In_queue_before Message dec is_inc_dec (bm c0 s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s owner)) *)
(* Goal: alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  elim H4.
(* Goal: legal c *)
  auto.
  
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: legal c *)
  auto.

(* Goal: legal c *)
auto.
  
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s owner)) *)
(* Goal: alternate (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite <- e1.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  apply alt_post_elsewhere; auto.
(* Goal: alternate (Collect_message Message (bm c0) s1 s2 s owner) *)
(* Goal: forall _ : @eq bool (Set_rec_table (rt c0) s2 s) false, D_queue (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (bm c0) s0 owner s owner)) (forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner)) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply alt_collect; trivial.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s s2); intro.
  rewrite e1; unfold Set_rec_table in |- *; rewrite that_site; intro;
(* Goal: forall _ : False, Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
   discriminate.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: legal c *)
  apply D_post_elsewhere; auto.
(* Goal: legal c *)
  apply D_collect; auto.
(* Goal: Z.ge (reduce Message dec_count q) (reduce Message new_inc_count q) *)
  apply H3.
(* Goal: legal c *)
  generalize H4; unfold Set_rec_table in |- *; rewrite other_site; auto.
  
    (* 7 *)
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  decompose [and] H1; split.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s0 s); intro.
(* Goal: legal c *)
  rewrite e1; apply alt_post_any; auto.
(* Goal: forall s : Site, not (@eq Message dec (inc_dec s)) *)
(* Goal: alternate (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  intro; discriminate.
  
(* Goal: legal c *)
  apply alt_post_elsewhere; auto.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s0 s); intro.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e1.
(* Goal: D_queue (Post_message Message dec (bm c0) s owner s owner) *)
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply D_post_dec.
(* Goal: legal c *)
  auto.
  
(* Goal: forall _ : @eq bool (Reset_rec_table (rt c0) s0 s) false, D_queue (Post_message Message dec (bm c0) s0 owner s owner) *)
(* Goal: and (alternate (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  unfold Reset_rec_table in |- *; rewrite other_site.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: legal c *)
  apply D_post_elsewhere; auto.
  
(* Goal: legal c *)
  auto.
  
  (* optim 1 *)

(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  decompose [and] H1; split.
(* Goal: D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite post_elsewhere.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s1 s); intro.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e0.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s owner (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite that_queue.
(* Goal: alternate q *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e0 in e.
(* Goal: alternate q *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e in H2.
(* Goal: alternate q *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  inversion H2.
(* Goal: alternate q *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  inversion H7.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite other_queue.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  right.
(* Goal: not (@eq Site s2 owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply (not_owner_inc3 c0 s1 owner).
(* Goal: legal c *)
  auto.
  
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  rewrite e; simpl in |- *.
(* Goal: legal c *)
  right; left; auto.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: D_queue (Post_message Message dec (change_queue (queue Message) (bm c0) s1 owner q) s1 s2 s owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite post_elsewhere.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_site_dec s1 s); intro.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  rewrite e0.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s owner (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite that_queue.
(* Goal: D_queue q *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  generalize (H3 H4).
(* Goal: forall _ : alternate (bm c0 s owner), alternate (append Message q1 (input Message copy q2)) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite <- e0; rewrite e.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: D_queue q *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  inversion H5.
(* Goal: D_queue q *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  inversion H6.
(* Goal: D_queue q *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  inversion H12.
(* Goal: D_queue q *)
(* Goal: D_queue q *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 owner q s owner) *)
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  elim (H15 s2).
(* Goal: legal c *)
  auto.
  
(* Goal: D_queue qm *)
(* Goal: forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  apply D_dec.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite other_queue.
(* Goal: legal c *)
  apply H3; auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: or (not (@eq Site s1 s)) (not (@eq Site s2 owner)) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  right.
(* Goal: not (@eq Site s2 owner) *)
(* Goal: and (alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) (forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner)) *)
  apply (not_owner_inc3 c0 s1 owner).
(* Goal: legal c *)
  auto.
  
(* Goal: forall _ : alternate (bm c0 s owner), alternate (append Message q1 (input Message copy q2)) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite e.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: legal c *)
  right; left; auto.

  (* optim 2 *)

(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  decompose [and] H1; split.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_queue_dec s1 s s2 owner); intro.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  decompose [and] a.
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite H4; rewrite H5.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s owner (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite that_queue.
(* Goal: alternate (append Message q3 (input Message copy q4)) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  apply alt_shuffle_copy with (q1 := q1) (q2 := q2).
(* Goal: legal c *)
  auto.
  
(* Goal: alternate (append Message q1 (input Message copy q2)) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  generalize H2.
(* Goal: forall _ : alternate (bm c0 s owner), alternate (append Message q1 (input Message copy q2)) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite H4 in e; rewrite H5 in e.
(* Goal: forall _ : alternate (bm c0 s owner), alternate (append Message q1 (input Message copy q2)) *)
(* Goal: alternate (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: forall _ : @eq bool (rt c0 s) false, D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite e.
(* Goal: legal c *)
  auto.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite other_queue.
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  elim o; intro; auto.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_queue_dec s1 s s2 owner); intro.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  decompose [and] a.
(* Goal: D_queue (bm c0 s1 s2) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite H5; rewrite H6.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s owner (append Message q3 (input Message copy q4)) s owner) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite that_queue.
(* Goal: D_queue (append Message q3 (input Message copy q4)) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  apply D_shuffle_copy with (q1 := q1) (q2 := q2).
(* Goal: legal c *)
  auto.
(* Goal: D_queue (append Message q1 (input Message copy q2)) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite <- e.
(* Goal: D_queue (bm c0 s1 s2) *)
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite H5; rewrite H6.
(* Goal: legal c *)
  apply H3; auto.
(* Goal: D_queue (change_queue (queue Message) (bm c0) s1 s2 (append Message q3 (input Message copy q4)) s owner) *)
  rewrite other_queue.
(* Goal: legal c *)
  apply H3; auto.
(* Goal: legal c *)
  elim o; intro; auto.
Qed.


Lemma count_alt_queue :
 forall q : queue Message,
 alternate q ->
 (reduce Message dec_count q + 1 >= reduce Message new_inc_count q)%Z /\
 (D_queue q ->
  (reduce Message dec_count q >= reduce Message new_inc_count q)%Z).
Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: and (Z.ge (Z.add (reduce Message dec_count q) (Zpos xH)) (reduce Message new_inc_count q)) (forall _ : D_queue q, Z.ge (reduce Message dec_count q) (reduce Message new_inc_count q)) *)
  elim H.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  omega.
  
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  intro; omega.
  
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: Z.ge (Z.add (Z.add (reduce Message dec_count qm) (dec_count m)) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: forall _ : D_queue (input Message m qm), Z.ge (Z.add (reduce Message dec_count qm) (dec_count m)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  cut (dec_count m >= 0)%Z.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.add (Z.add (reduce Message dec_count qm) (dec_count m)) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: Z.ge (dec_count m) Z0 *)
(* Goal: forall _ : D_queue (input Message m qm), Z.ge (Z.add (reduce Message dec_count qm) (dec_count m)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  cut (new_inc_count m = 0%Z).
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  omega.
  
(* Goal: @eq Z (new_inc_count m) Z0 *)
(* Goal: Z.ge (dec_count m) Z0 *)
(* Goal: forall _ : D_queue (input Message m qm), Z.ge (Z.add (reduce Message dec_count qm) (dec_count m)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  unfold new_inc_count in |- *.
(* Goal: @eq Z match m with | dec => Z0 | inc_dec s => Zpos xH | copy => Z0 end Z0 *)
(* Goal: Z.ge (dec_count m) Z0 *)
(* Goal: forall _ : D_queue (input Message m qm), Z.ge (Z.add (reduce Message dec_count qm) (dec_count m)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  generalize H0.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  case m; intros.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  elim (H4 s); auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  elim m; simpl in |- *; intros; omega.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.add (reduce Message dec_count qm) (dec_count m)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  decompose [and] H2.
(* Goal: Z.ge (Z.add (reduce Message dec_count qm) (dec_count m)) (Z.add (reduce Message new_inc_count qm) (new_inc_count m)) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  generalize H0 H3.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  case m; simpl in |- *; intros.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  omega.
  
(* Goal: Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
(* Goal: Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) Z0) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  elim (H6 s).
(* Goal: legal c *)
  auto.
  
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
(* Goal: forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  cut (D_queue qm).
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (H5 H8); intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  omega.
  
(* Goal: D_queue qm *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : and (Z.ge (Z.add (reduce Message dec_count qm) (Zpos xH)) (reduce Message new_inc_count qm)) (forall _ : D_queue qm, Z.ge (reduce Message dec_count qm) (reduce Message new_inc_count qm))) (_ : In_queue_before Message dec is_inc_dec qm), and (Z.ge (Z.add (reduce Message dec_count (input Message (inc_dec s0) qm)) (Zpos xH)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (reduce Message dec_count (input Message (inc_dec s0) qm)) (reduce Message new_inc_count (input Message (inc_dec s0) qm))) *)
  apply D_input.
(* Goal: legal c *)
  auto.
  
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  simpl in |- *; intros.
(* Goal: and (Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) (forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH))) *)
  split.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: Z.ge (Z.add (Z.add (reduce Message dec_count qm) Z0) (Zpos xH)) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
(* Goal: forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  cut (D_queue qm).
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  generalize (H4 H5); omega.
  
(* Goal: D_queue qm *)
(* Goal: forall _ : D_queue (input Message (inc_dec s0) qm), Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  apply D_dec.
(* Goal: legal c *)
  auto.
  
(* Goal: legal c *)
  auto.
  
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  inversion H3.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  generalize H5; simpl in |- *.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  case (eq_bool_dec true); intro.
(* Goal: forall _ : False, Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
(* Goal: forall _ : False, Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  intro; contradiction.
  
(* Goal: forall _ : False, Z.ge (Z.add (reduce Message dec_count qm) Z0) (Z.add (reduce Message new_inc_count qm) (Zpos xH)) *)
  discriminate.
Qed.


Lemma count_inc_and_dec_alt_queue :
 forall q : queue Message,
 alternate q ->
 (reduce Message dec_count q + 1 >= reduce Message new_inc_count q)%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (count_alt_queue q H); intro.
(* Goal: Z.ge (Z.add (reduce Message dec_count q) (Zpos xH)) (reduce Message new_inc_count q) *)
  decompose [and] H0.
(* Goal: legal c *)
  auto.
Qed.


Lemma count_inc_and_dec_D_queue :
 forall q : queue Message,
 D_queue q ->
 (reduce Message dec_count q >= reduce Message new_inc_count q)%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (D_queue_is_alternate q H); intro.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (count_alt_queue q H0); intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: Z.ge (reduce Message dec_count q) (reduce Message new_inc_count q) *)
  apply H3.
(* Goal: legal c *)
  auto.
Qed.


Lemma copy_count_is_positive :
 forall q : queue Message, (reduce Message copy_count q >= 0)%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: Z.ge (reduce Message dec_count q) Z0 *)
  apply reduce_positive_or_null.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  elim a; simpl in |- *; intros; omega.
Qed.

Lemma dec_count_is_positive :
 forall q : queue Message, (reduce Message dec_count q >= 0)%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: Z.ge (reduce Message dec_count q) Z0 *)
  apply reduce_positive_or_null.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  elim a; simpl in |- *; intros; omega.
Qed.


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

Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (copy_count_is_positive (bm c owner s)); intro.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (legal_alternate s c H); intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add (Int (rt c s)) (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  case (eq_bool_dec (rt c s)); intro; rewrite e; unfold Int in |- *.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (count_inc_and_dec_alt_queue (bm c s owner) H2); intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  omega.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  decompose [and] H1.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (H3 e); intro.
(* Goal: forall a : Message, Z.ge (dec_count a) Z0 *)
  generalize (count_inc_and_dec_D_queue (bm c s owner) H4); intro.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  omega.
Qed.




Let Recv_T := Site -> bool.

Lemma other_definition_for_sigma_receive_table :
 forall t : Recv_T,
 sigma_receive_table t =
 sigma_table Site LS Z (Z_id Site) (fun s : Site => Int (t s)).
Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: @eq Z (sigma_receive_table t) (sigma_table Site LS Z (Z_id Site) (fun s : Site => Int (t s))) *)
  unfold sigma_receive_table in |- *.
(* Goal: @eq Z (sigma_table Site LS bool (fun _ : Site => Int) t) (sigma_table Site LS Z (Z_id Site) (fun s : Site => Int (t s))) *)
  unfold sigma_table in |- *.
(* Goal: Z.ge (Z.sub (sigma_table Site LS Z (Z_id Site) (fun_minus Site (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
  unfold Z_id in |- *.
(* Goal: legal c *)
  auto.
Qed.


Remark add_reduce : forall x : Z, (x + 1 - 1)%Z = x.
Proof.
(* Goal: Z.ge (Z.sub (Z.add (Z.add Z0 (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner))) Z0 *)
  intro; omega.
Qed.


Lemma owner_st_positive : forall c : Config, legal c -> (st c owner >= 0)%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), Z.ge (st c owner) Z0 *)
  intros.
(* Goal: Z.ge (st c owner) Z0 *)
  rewrite (invariant4 c H).
(* Goal: Z.ge (Z.sub (Z.sub (Z.add (Z.add (sigma_receive_table (rt c)) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
  rewrite other_definition_for_sigma_receive_table.
(* Goal: Z.ge (Z.sub (Z.sub (Z.add (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
  rewrite <- sigma_same_table.
(* Goal: Z.ge (Z.sub (Z.sub (Z.add (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner)))) (sigma_table Site LS Z (Z_id Site) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
  rewrite <- sigma_same_table.
(* Goal: Z.ge (Z.sub (Z.sub (sigma_table Site LS Z (Z_id Site) (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2)))) (sigma_table Site LS Z (Z_id Site) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
  rewrite <- sigma_same_table2.
(* Goal: Z.ge (Z.sub (sigma_table Site LS Z (Z_id Site) (fun_minus Site (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
  unfold Z_id in |- *.
(* Goal: Z.ge (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun_minus Site (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2))) (fun s1 : Site => reduce Message new_inc_count (bm c s1 owner)))) (Zpos xH)) Z0 *)
  unfold fun_minus in |- *.
(* Goal: Z.ge (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (fun_sum Site (fun_sum Site (fun s : Site => Int (rt c s)) (fun s1 : Site => reduce Message dec_count (bm c s1 owner))) (fun s2 : Site => reduce Message copy_count (bm c owner s2)) a) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) Z0 *)
  unfold fun_sum in |- *.
(* Goal: Z.ge (Z.sub (sigma_table Site LS Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) Z0 *)
  rewrite sigma_sigma_but_owner.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int (rt c owner)) (reduce Message dec_count (bm c owner owner))) (reduce Message copy_count (bm c owner owner))) (reduce Message new_inc_count (bm c owner owner)))) (Zpos xH)) Z0 *)
  rewrite owner_rt_true.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Z.sub (Z.add (Z.add (Int true) (reduce Message dec_count (bm c owner owner))) (reduce Message copy_count (bm c owner owner))) (reduce Message new_inc_count (bm c owner owner)))) (Zpos xH)) Z0 *)
(* Goal: legal c *)
  rewrite empty_q_to_me.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  simpl in |- *.
(* Goal: Z.ge (Z.sub (Z.add (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) (Zpos xH)) (Zpos xH)) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  rewrite add_reduce.
(* Goal: Z.ge (sigma_table_but_owner Z (fun (_ : Site) (x : Z) => x) (fun a : Site => Z.sub (Z.add (Z.add (Int (rt c a)) (reduce Message dec_count (bm c a owner))) (reduce Message copy_count (bm c owner a))) (reduce Message new_inc_count (bm c a owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  unfold sigma_table_but_owner in |- *.
(* Goal: Z.ge (sigma_but Site owner eq_site_dec LS (fun s : Site => Z.sub (Z.add (Z.add (Int (rt c s)) (reduce Message dec_count (bm c s owner))) (reduce Message copy_count (bm c owner s))) (reduce Message new_inc_count (bm c s owner)))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  apply sigma_but_pos.
(* Goal: forall x_ : Site, Z.ge (Z.sub (Z.add (Z.add (Int (rt c x_)) (reduce Message dec_count (bm c x_ owner))) (reduce Message copy_count (bm c owner x_))) (reduce Message new_inc_count (bm c x_ owner))) Z0 *)
(* Goal: legal c *)
(* Goal: legal c *)
  exact (invariant5 c H).
(* Goal: legal c *)
  auto.
(* Goal: legal c *)
  auto.
Qed.



End INVARIANT5.
