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

Require Export DistributedReferenceCounting.machine1.machine.
Require Export DistributedReferenceCounting.machine1.cardinal.
Require Export DistributedReferenceCounting.machine1.comm.


Section INVARIANT1.

Lemma invariant1_init :
 sigma_send_table send_init =
 (sigma_receive_table rec_init + sigma_weight bag_init)%Z.
Proof.
(* Goal: @eq Z (sigma_send_table send_init) (Z.add (sigma_receive_table rec_init) (sigma_weight bag_init)) *)
  unfold send_init, rec_init, bag_init in |- *.
(* Goal: @eq Z (sigma_send_table (fun _ : Site => Z0)) (Z.add (sigma_receive_table (fun _ : Site => false)) (sigma_weight (fun _ _ : Site => empty Message))) *)
  unfold sigma_send_table, sigma_receive_table, sigma_weight in |- *.
(* Goal: @eq Z Z0 (sigma_table Site LS Z (Z_id Site) (fun _ : Site => sigma_table Site LS (queue Message) (fun _ : Site => cardinal) (fun _ : Site => empty Message))) *)
  unfold sigma_table in |- *.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => Z0)))) Z0 *)
  rewrite sigma_null.
  replace
   (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal)
      (fun _ _ : Site => empty Message)) with 0%Z.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  omega.
  
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  unfold sigma2_table in |- *.
(* Goal: @eq Z Z0 (sigma_table Site LS Z (Z_id Site) (fun _ : Site => sigma_table Site LS (queue Message) (fun _ : Site => cardinal) (fun _ : Site => empty Message))) *)
  unfold sigma_table in |- *.
  symmetry  in |- *.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  simpl in |- *.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => Z0)))) Z0 *)
  rewrite sigma_null.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s Z0)) Z0 *)
  apply sigma_null.
Qed.


Lemma invariant1_inductive :
 forall (c : Config) (t : class_trans c),
 legal c ->
 sigma_send_table (st c) =
 (sigma_receive_table (rt c) + sigma_weight (bm c))%Z ->
 sigma_send_table (st (transition c t)) =
 (sigma_receive_table (rt (transition c t)) +
  sigma_weight (bm (transition c t)))%Z.

Proof.
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c t))) (Z.add (sigma_receive_table (rt (transition c t))) (sigma_weight (bm (transition c t)))) *)
  simple induction t.

  (* 1 *)

(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Reset_rec_table (rt c) s)) (sigma_weight (Post_message Message dec (bm c) s owner))) *)
  rewrite sigma_weight_post_message.
(* Goal: @eq Z (sigma_send_table (Inc_send_table (st c) owner)) (Z.add (sigma_receive_table (rt c)) (Z.add (sigma_weight (Collect_message Message (bm c) s1 owner)) (cardinal_count dec))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy1 c s1 s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy1 c s1 s2 e e0)))) (sigma_weight (bm (transition c (receive_copy1 c s1 s2 e e0))))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy2 c s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy2 c s2 e e0)))) (sigma_weight (bm (transition c (receive_copy2 c s2 e e0))))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy3 c s1 s2 e n e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy3 c s1 s2 e n e0)))) (sigma_weight (bm (transition c (receive_copy3 c s1 s2 e n e0))))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_inc_send_table.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- *.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  rewrite H0; omega.

  (* 2 *)
  
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (sigma_send_table (Dec_send_table (st c) s2)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (Collect_message Message (bm c) s1 s2))) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_inc c s1 s3 e)))) (Z.add (sigma_receive_table (rt (transition c (receive_inc c s1 s3 e)))) (sigma_weight (bm (transition c (receive_inc c s1 s3 e))))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy1 c s1 s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy1 c s1 s2 e e0)))) (sigma_weight (bm (transition c (receive_copy1 c s1 s2 e e0))))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy2 c s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy2 c s2 e e0)))) (sigma_weight (bm (transition c (receive_copy2 c s2 e e0))))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy3 c s1 s2 e n e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy3 c s1 s2 e n e0)))) (sigma_weight (bm (transition c (receive_copy3 c s1 s2 e n e0))))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite (sigma_weight_collect_message dec).
(* Goal: @eq Z (sigma_send_table (Dec_send_table (st c) s2)) (Z.add (sigma_receive_table (rt c)) (Z.sub (sigma_weight (bm c)) (cardinal_count dec))) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message dec) *)
(* Goal: forall (s1 s3 : Site) (e : @eq (exc Message) (first Message (bm c s1 owner)) (value Message (inc_dec s3))) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_inc c s1 s3 e)))) (Z.add (sigma_receive_table (rt (transition c (receive_inc c s1 s3 e)))) (sigma_weight (bm (transition c (receive_inc c s1 s3 e))))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy1 c s1 s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy1 c s1 s2 e e0)))) (sigma_weight (bm (transition c (receive_copy1 c s1 s2 e e0))))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy2 c s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy2 c s2 e e0)))) (sigma_weight (bm (transition c (receive_copy2 c s2 e e0))))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy3 c s1 s2 e n e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy3 c s1 s2 e n e0)))) (sigma_weight (bm (transition c (receive_copy3 c s1 s2 e n e0))))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_dec_send_table.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- *.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  rewrite H0; omega.
(* Goal: @eq bool (rt c s) true *)
  auto.

  (* 3 *)
  
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Reset_rec_table (rt c) s)) (sigma_weight (Post_message Message dec (bm c) s owner))) *)
  rewrite sigma_weight_post_message.
(* Goal: @eq Z (sigma_send_table (Inc_send_table (st c) owner)) (Z.add (sigma_receive_table (rt c)) (Z.add (sigma_weight (Collect_message Message (bm c) s1 owner)) (cardinal_count dec))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy1 c s1 s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy1 c s1 s2 e e0)))) (sigma_weight (bm (transition c (receive_copy1 c s1 s2 e e0))))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy2 c s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy2 c s2 e e0)))) (sigma_weight (bm (transition c (receive_copy2 c s2 e e0))))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy3 c s1 s2 e n e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy3 c s1 s2 e n e0)))) (sigma_weight (bm (transition c (receive_copy3 c s1 s2 e n e0))))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_inc_send_table.
(* Goal: @eq Z (Z.add (sigma_send_table (st c)) (Zpos xH)) (Z.add (sigma_receive_table (rt c)) (Z.add (sigma_weight (Collect_message Message (bm c) s1 owner)) (cardinal_count dec))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) true) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy1 c s1 s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy1 c s1 s2 e e0)))) (sigma_weight (bm (transition c (receive_copy1 c s1 s2 e e0))))) *)
(* Goal: forall (s2 : Site) (e : @eq bool (rt c s2) false) (e0 : @eq (exc Message) (first Message (bm c owner s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy2 c s2 e e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy2 c s2 e e0)))) (sigma_weight (bm (transition c (receive_copy2 c s2 e e0))))) *)
(* Goal: forall (s1 s2 : Site) (e : @eq bool (rt c s2) false) (n : not (@eq Site s1 owner)) (e0 : @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (receive_copy3 c s1 s2 e n e0)))) (Z.add (sigma_receive_table (rt (transition c (receive_copy3 c s1 s2 e n e0)))) (sigma_weight (bm (transition c (receive_copy3 c s1 s2 e n e0))))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_weight_collect_message with (m := inc_dec s3).
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- *.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  rewrite H0; omega.
(* Goal: @eq bool (rt c s) true *)
  auto.

  (* 4 *)
  
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Reset_rec_table (rt c) s)) (sigma_weight (Post_message Message dec (bm c) s owner))) *)
  rewrite sigma_weight_post_message.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Set_rec_table (rt c) s2)) (Z.add (sigma_weight (Collect_message Message (bm c) s1 s2)) (cardinal_count (inc_dec s1)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_weight_collect_message with (m := copy).
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- *.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  rewrite H0; omega.
(* Goal: @eq bool (rt c s) true *)
  auto.

  (* 5 *)
  
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Set_rec_table (rt c) s2)) (Z.add (sigma_weight (Collect_message Message (bm c) s1 s2)) (cardinal_count (inc_dec s1)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_weight_collect_message with (m := copy).
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Set_rec_table (rt c) s2)) (Z.add (Z.sub (sigma_weight (bm c)) (cardinal_count copy)) (cardinal_count (inc_dec s1)))) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_set_receive_table.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- *.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  rewrite H0; omega.
(* Goal: @eq bool (rt c s) true *)
  auto.
(* Goal: @eq bool (rt c s) true *)
  auto.

  (* 6 *)
  
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Reset_rec_table (rt c) s)) (sigma_weight (Post_message Message dec (bm c) s owner))) *)
  rewrite sigma_weight_post_message.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Set_rec_table (rt c) s2)) (Z.add (sigma_weight (Collect_message Message (bm c) s1 s2)) (cardinal_count (inc_dec s1)))) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_weight_collect_message with (m := copy).
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Set_rec_table (rt c) s2)) (Z.add (Z.sub (sigma_weight (bm c)) (cardinal_count copy)) (cardinal_count (inc_dec s1)))) *)
(* Goal: @eq (exc Message) (first Message (bm c s1 s2)) (value Message copy) *)
(* Goal: forall (s : Site) (e : @eq Z (st c s) Z0) (e0 : @eq bool (rt c s) true) (n : not (@eq Site s owner)) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c (delete_entry c s e e0 n)))) (Z.add (sigma_receive_table (rt (transition c (delete_entry c s e e0 n)))) (sigma_weight (bm (transition c (delete_entry c s e e0 n))))) *)
  rewrite sigma_set_receive_table.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- *.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  rewrite H0; omega.
(* Goal: @eq bool (rt c s) true *)
  auto.
(* Goal: @eq bool (rt c s) true *)
  auto.
  
  (* 7 *)

(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  intros; simpl in |- *.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Reset_rec_table (rt c) s)) (sigma_weight (Post_message Message dec (bm c) s owner))) *)
  rewrite sigma_weight_post_message.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (Reset_rec_table (rt c) s)) (Z.add (sigma_weight (bm c)) (cardinal_count dec))) *)
  rewrite sigma_reset_receive_table.
(* Goal: @eq Z (sigma Site LS (fun s : Site => Z_id Site s (sigma Site LS (fun _ : Site => cardinal (empty Message))))) Z0 *)
  unfold cardinal_count in |- *; unfold fun_sum in |- *; simpl in |- *.
(* Goal: @eq Z Z0 (Z.add Z0 Z0) *)
(* Goal: @eq Z Z0 (sigma2_table Site LS LS (queue Message) (fun _ _ : Site => cardinal) (fun _ _ : Site => empty Message)) *)
  rewrite H0; omega.
(* Goal: @eq bool (rt c s) true *)
  auto.
Qed.


Lemma invariant1 :
 forall c : Config,
 legal c ->
 sigma_send_table (st c) =
 (sigma_receive_table (rt c) + sigma_weight (bm c))%Z.
Proof.
(* Goal: forall (c : Config) (_ : legal c), @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) *)
  intros.
(* Goal: @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c))) *)
  elim H.
(* Goal: @eq Z (sigma_send_table (st config_init)) (Z.add (sigma_receive_table (rt config_init)) (sigma_weight (bm config_init))) *)
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c t))) (Z.add (sigma_receive_table (rt (transition c t))) (sigma_weight (bm (transition c t)))) *)
  apply invariant1_init.
(* Goal: forall (c : Config) (t : class_trans c) (_ : legal c) (_ : @eq Z (sigma_send_table (st c)) (Z.add (sigma_receive_table (rt c)) (sigma_weight (bm c)))), @eq Z (sigma_send_table (st (transition c t))) (Z.add (sigma_receive_table (rt (transition c t))) (sigma_weight (bm (transition c t)))) *)
  exact invariant1_inductive.
Qed.




End INVARIANT1.

