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

Unset Standard Proposition Elimination Names.

(* changes:
   only a few changes in ancestor_not_reflexive for
   transition  6 ,  where n0->n1, n1-> n2, n2-> n3.
*)




Section INVARIANT6.

Variable c0 : Config.

Fixpoint inc_dec_in_queue (s : Site) (q : queue Message) {struct q} : Prop :=
  match q with
  | empty => False
  | input (inc_dec s2) q' => if eq_site_dec s2 s then True else False
  | input _ q' => inc_dec_in_queue s q'
  end.
	
(* note that the contrary is not true ! *)

Lemma inc_dec_in :
 forall (s : Site) (q : queue Message),
 inc_dec_in_queue s q -> In_queue Message (inc_dec s) q.

Proof.
(* Goal: forall (q : queue Message) (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q) *)
  simple induction q.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : if eq_site_dec s0 s then True else False, or (@eq Message (inc_dec s) (inc_dec s0)) (In_queue Message (inc_dec s) q0) *)
(* Goal: forall _ : inc_dec_in_queue s q0, or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0) *)
  case (eq_site_dec s0 s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite e.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
Qed.



Lemma inc_dec_queue_equal :
 forall (q : queue Message) (s1 s2 : Site),
 inc_dec_in_queue s1 q -> inc_dec_in_queue s2 q -> s1 = s2.

Proof.
(* Goal: forall (q : queue Message) (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q) *)
  simple induction q.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (d : Message) (q : queue Message) (_ : forall (s1 s2 : Site) (_ : inc_dec_in_queue s1 q) (_ : inc_dec_in_queue s2 q), @eq Site s1 s2) (s1 s2 : Site) (_ : match d with | dec => inc_dec_in_queue s1 q | inc_dec s3 => if eq_site_dec s3 s1 then True else False | copy => inc_dec_in_queue s1 q end) (_ : match d with | dec => inc_dec_in_queue s2 q | inc_dec s3 => if eq_site_dec s3 s2 then True else False | copy => inc_dec_in_queue s2 q end), @eq Site s1 s2 *)
  intros d q0 s1 s2.
(* Goal: forall (s3 : Site) (_ : match d with | dec => inc_dec_in_queue s2 q0 | inc_dec s4 => if eq_site_dec s4 s2 then True else False | copy => inc_dec_in_queue s2 q0 end) (_ : match d with | dec => inc_dec_in_queue s3 q0 | inc_dec s2 => if eq_site_dec s2 s3 then True else False | copy => inc_dec_in_queue s3 q0 end), @eq Site s2 s3 *)
  intro s0.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (_ : if eq_site_dec s s2 then True else False) (_ : if eq_site_dec s s0 then True else False), @eq Site s2 s0 *)
(* Goal: forall (_ : inc_dec_in_queue s2 q0) (_ : inc_dec_in_queue s0 q0), @eq Site s2 s0 *)
  case (eq_site_dec s s2).
(* Goal: forall (_ : @eq Site s s2) (_ : True) (_ : if eq_site_dec s s0 then True else False), @eq Site s2 s0 *)
(* Goal: forall (_ : not (@eq Site s s2)) (_ : False) (_ : if eq_site_dec s s0 then True else False), @eq Site s2 s0 *)
(* Goal: forall (_ : inc_dec_in_queue s2 q0) (_ : inc_dec_in_queue s0 q0), @eq Site s2 s0 *)
  case (eq_site_dec s s0).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s2 s0 *)
(* Goal: forall (_ : not (@eq Site s s0)) (_ : @eq Site s s2) (_ : True) (_ : False), @eq Site s2 s0 *)
(* Goal: forall (_ : not (@eq Site s s2)) (_ : False) (_ : if eq_site_dec s s0 then True else False), @eq Site s2 s0 *)
(* Goal: forall (_ : inc_dec_in_queue s2 q0) (_ : inc_dec_in_queue s0 q0), @eq Site s2 s0 *)
  rewrite <- e; rewrite e0.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.




(* s1 is parent of s0 *)
Inductive parent : Site -> Site -> Prop :=
    parent_intro :
      forall s1 s0 : Site,
      rt c0 s0 = true -> inc_dec_in_queue s1 (bm c0 s0 owner) -> parent s1 s0.

(* s1 is ancestor of s0 *)
Inductive ancestor : Site -> Site -> Prop :=
  | short : forall s1 s0 : Site, parent s1 s0 -> ancestor s1 s0
  | long :
      forall s2 s1 s0 : Site,
      ancestor s2 s1 -> parent s1 s0 -> ancestor s2 s0.


Lemma decide_rt : forall s : Site, {rt c0 s = false} + {rt c0 s = true}.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: sumbool (@eq bool (rt c0 s) false) (@eq bool (rt c0 s) true) *)
  case (rt c0 s).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.

Lemma decide_inc_dec_in_queue :
 forall s : Site,
 {s1 : Site | inc_dec_in_queue s1 (bm c0 s owner)} +
 {(forall s1 : Site, ~ inc_dec_in_queue s1 (bm c0 s owner))}.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: sumor (@sig Site (fun s1 : Site => inc_dec_in_queue s1 (bm c0 s owner))) (forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s owner))) *)
  elim (bm c0 s owner).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: sumbool (direct_son s1) (not (direct_son s1)) *)
  left.
(* Goal: @sig Site (fun s1 : Site => if eq_site_dec s0 s1 then True else False) *)
(* Goal: sumor (@sig Site (fun s1 : Site => inc_dec_in_queue s1 (input Message copy q))) (forall s1 : Site, not (inc_dec_in_queue s1 (input Message copy q))) *)
  split with s0.
(* Goal: if eq_site_dec s0 s0 then True else False *)
(* Goal: sumor (@sig Site (fun s1 : Site => inc_dec_in_queue s1 (input Message copy q))) (forall s1 : Site, not (inc_dec_in_queue s1 (input Message copy q))) *)
  case (eq_site_dec s0 s0).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intro; elim n; auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  simpl in |- *; auto.
Qed.



Lemma decide_parent : forall s1 s3 : Site, {parent s1 s3} + {~ parent s1 s3}.

Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: sumbool (parent s1 s3) (not (parent s1 s3)) *)
  elim (decide_rt s3).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: forall _ : forall s2 : Site, not (inc_dec_in_queue s2 (bm c0 s1 owner)), sumbool (direct_son s1) (not (direct_son s1)) *)
  generalize a.
(* Goal: False *)
  elim H.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
(* Goal: forall _ : @eq bool (rt c0 s3) true, sumbool (parent s1 s3) (not (parent s1 s3)) *)
  rewrite H0 in a0.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: sumbool (parent s1 s3) (not (parent s1 s3)) *)
  elim (decide_inc_dec_in_queue s3).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s owner)), sumbool (direct_son s) (indirect_son1 s) *)
  elim a.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: sumbool (parent s1 s3) (not (parent s1 s3)) *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s3 owner)), sumbool (parent s1 s3) (not (parent s1 s3)) *)
  case (eq_site_dec x s1).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: sumbool (direct_son s1) (not (direct_son s1)) *)
  left.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: inc_dec_in_queue s1 (bm c0 s3 owner) *)
(* Goal: forall _ : not (@eq Site x s1), sumbool (parent s1 s3) (not (parent s1 s3)) *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s3 owner)), sumbool (parent s1 s3) (not (parent s1 s3)) *)
  rewrite <- e.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s3 owner)), sumbool (parent s1 s3) (not (parent s1 s3)) *)
  generalize p; generalize n.
(* Goal: False *)
  elim H.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s3 owner)), sumbool (parent s1 s3) (not (parent s1 s3)) *)
  elim n0.
(* Goal: @eq Site x s0 *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s3 owner)), sumbool (parent s1 s3) (not (parent s1 s3)) *)
  apply inc_dec_queue_equal with (q := bm c0 s2 owner).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
  generalize b0.
(* Goal: False *)
  elim H.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
  generalize (b1 s0).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H2; auto.
Qed.

Inductive direct_son : Site -> Prop :=
    direct_son_intro :
      forall s : Site,
      s <> owner ->
      rt c0 s = true ->
      (forall s1 : Site, ~ inc_dec_in_queue s1 (bm c0 s owner)) ->
      direct_son s.




Inductive indirect_son1 : Site -> Prop :=
    indirect_son1_intro :
      forall s : Site,
      s <> owner ->
      rt c0 s = true ->
      ~ (forall s1 : Site, ~ inc_dec_in_queue s1 (bm c0 s owner)) ->
      indirect_son1 s.


(*  {s1:Site | (inc_dec_in_queue s1 (bm c0 s owner))}  *)

Inductive indirect_son2 : Site -> Prop :=
    indirect_son2_intro :
      forall s s1 : Site,
      s <> owner /\ rt c0 s = true /\ direct_son s1 /\ ancestor s1 s ->
      indirect_son2 s.

(* by specifying the lemma as follows, I don't need to
   know that there is no cycle in the relation *)

Lemma decide_direct_son :
 forall s1 : Site, s1 <> owner -> {direct_son s1} + {~ direct_son s1}.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: sumbool (direct_son s1) (not (direct_son s1)) *)
  elim (decide_rt s1).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: forall _ : forall s2 : Site, not (inc_dec_in_queue s2 (bm c0 s1 owner)), sumbool (direct_son s1) (not (direct_son s1)) *)
  generalize a.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
(* Goal: forall _ : @eq bool (rt c0 s1) true, sumbool (direct_son s1) (not (direct_son s1)) *)
  rewrite H2 in a0.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: sumbool (direct_son s1) (not (direct_son s1)) *)
  elim (decide_inc_dec_in_queue s1).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: forall _ : forall s2 : Site, not (inc_dec_in_queue s2 (bm c0 s1 owner)), sumbool (direct_son s1) (not (direct_son s1)) *)
  generalize a.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
(* Goal: forall _ : forall s2 : Site, not (inc_dec_in_queue s2 (bm c0 s1 owner)), sumbool (direct_son s1) (not (direct_son s1)) *)
  elim a0.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: sumbool (direct_son s1) (not (direct_son s1)) *)
  left.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply direct_son_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.



Lemma direct_or_indirect_son1 :
 forall s : Site,
 s <> owner -> rt c0 s = true -> {direct_son s} + {indirect_son1 s}.

Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: sumbool (direct_son s) (indirect_son1 s) *)
  elim (decide_inc_dec_in_queue s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: indirect_son1 s *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s owner)), sumbool (direct_son s) (indirect_son1 s) *)
  apply (indirect_son1_intro s).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  unfold not in |- *; intros.
(* Goal: False *)
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s owner)), sumbool (direct_son s) (indirect_son1 s) *)
  elim a.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: sumbool (direct_son s1) (not (direct_son s1)) *)
  intros; left.
(* Goal: direct_son s *)
  apply (direct_son_intro s).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.


Lemma disjoint_case_for_site :
 forall s : Site,
 {s = owner} + {rt c0 s = false} + {direct_son s} + {indirect_son1 s}.
Proof.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: sumor (sumor (sumbool (@eq Site s owner) (@eq bool (rt c0 s) false)) (direct_son s)) (indirect_son1 s) *)
  case (eq_site_dec s owner).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: sumor (sumor (sumbool (@eq Site s owner) (@eq bool (rt c0 s) false)) (direct_son s)) (indirect_son1 s) *)
  generalize (direct_or_indirect_son1 s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: sumor (sumor (sumbool (@eq Site s owner) (@eq bool (rt c0 s) false)) (direct_son s)) (indirect_son1 s) *)
  elim (decide_rt s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: False *)
  elim H.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.


Lemma ancestor_transitive :
 forall s1 s2 s3 : Site, ancestor s1 s2 -> ancestor s2 s3 -> ancestor s1 s3.
Proof.
(* Goal: forall (s1 s2 s3 : Site) (_ : ancestor s1 s2) (_ : ancestor s2 s3), ancestor s1 s3 *)
  intros s1 s2 s3 H.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: inc_dec_in_queue s1 (b s0 owner) *)
  generalize H.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply long with (s1 := s0).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s5 *)
  apply long with (s1 := s4).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.


Lemma aux :
 forall s0 s1 s2 : Site,
 parent s0 s2 -> direct_son s0 -> ancestor s1 s2 -> s1 = s0.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
   intros.
(* Goal: @eq Site s1 s0 *)
  generalize H H0.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s3 s0 *)
(* Goal: forall (s2 s1 s3 : Site) (_ : ancestor s2 s1) (_ : forall (_ : parent s0 s1) (_ : direct_son s0), @eq Site s2 s0) (_ : parent s1 s3) (_ : parent s0 s3) (_ : direct_son s0), @eq Site s2 s0 *)
  apply inc_dec_queue_equal with (q := bm c0 s4 owner).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H2; auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H3; auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s3 s0 *)
  cut (s0 = s4).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  rewrite <- H7 in H2.
(* Goal: @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  generalize H2.
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s3 s *)
(* Goal: @eq Site s0 s4 *)
  generalize H10.
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s owner)), @eq Site s3 s *)
(* Goal: @eq Site s0 s4 *)
  elim H11.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s6 s7 *)
(* Goal: forall (s2 s1 s0 : Site) (_ : ancestor s2 s1) (_ : forall _ : forall s3 : Site, not (inc_dec_in_queue s3 (bm c0 s1 owner)), @eq Site s2 s1) (_ : parent s1 s0) (_ : forall s3 : Site, not (inc_dec_in_queue s3 (bm c0 s0 owner))), @eq Site s2 s0 *)
(* Goal: @eq Site s0 s4 *)
  generalize H13.
(* Goal: or (or (@eq Site s4 s2) (ancestor s4 s2)) (and (not (@eq Site s4 s2)) (not (ancestor s4 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H12.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s8 s9 *)
(* Goal: forall (s2 s1 s0 : Site) (_ : ancestor s2 s1) (_ : forall _ : forall s3 : Site, not (inc_dec_in_queue s3 (bm c0 s1 owner)), @eq Site s2 s1) (_ : parent s1 s0) (_ : forall s3 : Site, not (inc_dec_in_queue s3 (bm c0 s0 owner))), @eq Site s2 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim (H16 s8).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s6 s8 *)
(* Goal: @eq Site s0 s4 *)
  generalize H15.
(* Goal: forall _ : forall s1 : Site, not (inc_dec_in_queue s1 (bm c0 s8 owner)), @eq Site s6 s8 *)
(* Goal: @eq Site s0 s4 *)
  elim H14.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq Site s6 s10 *)
(* Goal: @eq Site s0 s4 *)
  elim (H18 s9).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq Site s4 s0 *)
(* Goal: forall (s2 s1 s3 : Site) (_ : ancestor s2 s1) (_ : forall (_ : parent s0 s1) (_ : not (ancestor s2 s0)) (_ : not (@eq Site s2 s0)) (_ : not (@eq Site s2 s1)), False) (_ : parent s1 s3) (_ : parent s0 s3) (_ : not (ancestor s2 s0)) (_ : not (@eq Site s2 s0)) (_ : not (@eq Site s2 s3)), False *)
  apply inc_dec_queue_equal with (q := bm c0 s5 owner).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H5; auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H4; auto.
Qed.



Lemma decide_ancestor :
 forall x s s1 : Site,
 direct_son x ->
 ancestor x s ->
 indirect_son1 s1 -> (s1 = s \/ ancestor s1 s) \/ s1 <> s /\ ~ ancestor s1 s.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: or (or (@eq Site s1 s) (ancestor s1 s)) (and (not (@eq Site s1 s)) (not (ancestor s1 s))) *)
  generalize H H1.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  case (eq_site_dec s1 s2).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  left; left; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  case (eq_site_dec s0 s1).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  generalize H3.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite e.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: or (or (@eq Site s3 s2) (ancestor s3 s2)) (and (not (@eq Site s3 s2)) (not (ancestor s3 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  generalize H7.
(* Goal: ancestor s1 s0 *)
(* Goal: parent s0 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  elim H8.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: or (or (@eq Site s4 s2) (ancestor s4 s2)) (and (not (@eq Site s4 s2)) (not (ancestor s4 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H12.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  split; auto.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  generalize (aux s0 s1 s2 H2 H3 H5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intro; elim n0; auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  generalize (H3 H5 H1).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  elim H7.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  case (eq_site_dec s1 s3).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  left; left; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  left; right.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  case (eq_site_dec s1 s0).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite e; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply long with (s1 := s0).
(* Goal: ancestor s1 s0 *)
(* Goal: parent s0 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  elim H8.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intro; elim n0; auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  case (eq_site_dec s1 s3).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  left; left; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  right.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  split; auto.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
  decompose [and] H8.
(* Goal: False *)
  generalize H4 H11 H10 n.
(* Goal: forall (_ : parent s0 s3) (_ : not (ancestor s1 s0)) (_ : not (@eq Site s1 s0)) (_ : not (@eq Site s1 s3)), False *)
  elim H9.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
(* Goal: forall (s2 s1 s3 : Site) (_ : ancestor s2 s1) (_ : forall (_ : parent s0 s1) (_ : not (ancestor s2 s0)) (_ : not (@eq Site s2 s0)) (_ : not (@eq Site s2 s1)), False) (_ : parent s1 s3) (_ : parent s0 s3) (_ : not (ancestor s2 s0)) (_ : not (@eq Site s2 s0)) (_ : not (@eq Site s2 s3)), False *)
  elim H15.
(* Goal: @eq Site s4 s0 *)
(* Goal: forall (s2 s1 s3 : Site) (_ : ancestor s2 s1) (_ : forall (_ : parent s0 s1) (_ : not (ancestor s2 s0)) (_ : not (@eq Site s2 s0)) (_ : not (@eq Site s2 s1)), False) (_ : parent s1 s3) (_ : parent s0 s3) (_ : not (ancestor s2 s0)) (_ : not (@eq Site s2 s0)) (_ : not (@eq Site s2 s3)), False *)
  apply inc_dec_queue_equal with (q := bm c0 s5 owner).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H12; auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H13; auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
  cut (s0 = s5).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: @eq Site s0 s5 *)
  rewrite H18 in H16.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H16; auto.
  
(* Goal: @eq Site s0 s5 *)
  apply inc_dec_queue_equal with (q := bm c0 s6 owner).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H15; auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H14; auto.
Qed.

End INVARIANT6.

Section INVARIANT6_bis.


Lemma inc_dec_in_post :
 forall (b : Bag_of_message) (s0 s1 s2 s3 : Site) (m : Message),
 inc_dec_in_queue s1 (b s0 owner) ->
 (forall s4 : Site, m <> inc_dec s4) ->
 inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner).
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
   intros.
(* Goal: forall _ : inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner), inc_dec_in_queue s1 (b s0 owner) *)
   case (eq_queue_dec s2 s0 s3 owner).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
   intros.
(* Goal: inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
   decompose [and] a.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
   rewrite H1; rewrite H2.
(* Goal: forall _ : inc_dec_in_queue s1 (Post_message Message m b s0 owner s0 owner), inc_dec_in_queue s1 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s2 s0)) (not (@eq Site s3 owner))) (_ : inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner)), inc_dec_in_queue s1 (b s0 owner) *)
   rewrite post_here.
(* Goal: False *)
   generalize H0.
(* Goal: forall _ : forall s4 : Site, not (@eq Message m (inc_dec s4)), inc_dec_in_queue s1 (input Message m (b s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s3 owner)), inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner) *)
   case m.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
   simpl in |- *; auto.
   
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
   intro.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
   intro.
(* Goal: inc_dec_in_queue s1 (input Message (inc_dec s) (b s0 owner)) *)
(* Goal: forall _ : forall s4 : Site, not (@eq Message copy (inc_dec s4)), inc_dec_in_queue s1 (input Message copy (b s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s2 s0)) (not (@eq Site s3 owner)), inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner) *)
   generalize (H3 s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
   intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
   elim H4; auto.
   
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
   simpl in |- *; auto.
   
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
   intro; rewrite post_elsewhere; auto.
Qed.

Lemma inc_dec_in_post2 :
 forall (b : Bag_of_message) (s0 s1 s2 s3 : Site) (m : Message),
 inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner) ->
 m <> inc_dec s1 -> inc_dec_in_queue s1 (b s0 owner).
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: inc_dec_in_queue s1 (b s0 owner) *)
  generalize H.
(* Goal: forall _ : inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner), inc_dec_in_queue s1 (b s0 owner) *)
  case (eq_queue_dec s2 s0 s3 owner).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  decompose [and] a.
(* Goal: inc_dec_in_queue s1 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s2 s0)) (not (@eq Site s3 owner))) (_ : inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner)), inc_dec_in_queue s1 (b s0 owner) *)
  generalize H1.
(* Goal: inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
  rewrite H2; rewrite H3.
(* Goal: forall _ : inc_dec_in_queue s1 (Post_message Message m b s0 owner s0 owner), inc_dec_in_queue s1 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s2 s0)) (not (@eq Site s3 owner))) (_ : inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner)), inc_dec_in_queue s1 (b s0 owner) *)
  rewrite post_here.
(* Goal: False *)
  generalize H0.
(* Goal: forall (_ : not (@eq Message m (inc_dec s1))) (_ : inc_dec_in_queue s1 (input Message m (b s0 owner))), inc_dec_in_queue s1 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s2 s0)) (not (@eq Site s3 owner))) (_ : inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner)), inc_dec_in_queue s1 (b s0 owner) *)
  elim m.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  simpl in |- *; auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro; intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall _ : if eq_site_dec s s1 then True else False, inc_dec_in_queue s1 (b s0 owner) *)
(* Goal: forall (_ : not (@eq Message copy (inc_dec s1))) (_ : inc_dec_in_queue s1 (input Message copy (b s0 owner))), inc_dec_in_queue s1 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s2 s0)) (not (@eq Site s3 owner))) (_ : inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner)), inc_dec_in_queue s1 (b s0 owner) *)
  case (eq_site_dec s s1).
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  intro; elim H4.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite e; auto.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  simpl in |- *; auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s0 (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  rewrite post_elsewhere.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.


(* these two lemmas are just negations of the previous ones *)


Lemma inc_dec_not_in_post :
 forall (b : Bag_of_message) (s0 s1 s2 s3 : Site) (m : Message),
 ~ inc_dec_in_queue s1 (b s0 owner) ->
 (forall s4 : Site, m <> inc_dec s4) ->
 ~ inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner).
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
  elim H.
(* Goal: inc_dec_in_queue s1 (b s0 owner) *)
  apply (inc_dec_in_post2 b s0 s1 s2 s3 m).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.


Lemma inc_dec_not_in_post2 :
 forall (b : Bag_of_message) (s0 s1 s2 s3 : Site) (m : Message),
 (forall s4 : Site, m <> inc_dec s4) ->
 ~ inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner) ->
 ~ inc_dec_in_queue s1 (b s0 owner).
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner) *)
  apply inc_dec_in_post.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.

Lemma inc_dec_not_in_first_out :
 forall (q : queue Message) (m : Message) (s3 : Site),
 first Message q = value Message m ->
 m <> inc_dec s3 ->
 ~ inc_dec_in_queue s3 q -> ~ inc_dec_in_queue s3 (first_out Message q).
Proof.
(* Goal: forall (q : queue Message) (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q) *)
  simple induction q.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall (d : Message) (q : queue Message) (_ : forall (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message q) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 q), inc_dec_in_queue s3 (first_out Message q)) (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d q)) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d q)), inc_dec_in_queue s3 (first_out Message (input Message d q)) *)
  intros d q0.
(* Goal: forall (_ : forall (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message q0) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 q0), inc_dec_in_queue s3 (first_out Message q0)) (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d q0)) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d q0)), inc_dec_in_queue s3 (first_out Message (input Message d q0)) *)
  case q0.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (empty Message))) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (empty Message))), inc_dec_in_queue s3 (first_out Message (input Message d (empty Message))) *)
(* Goal: forall (m : Message) (q : queue Message) (_ : forall (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message m q)) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message m q)), inc_dec_in_queue s3 (first_out Message (input Message m q))) (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (input Message m q))) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (input Message m q))), inc_dec_in_queue s3 (first_out Message (input Message d (input Message m q))) *)
  intros m s3.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
  
(* Goal: forall (m : Message) (q : queue Message) (_ : forall (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message m q)) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message m q)), inc_dec_in_queue s3 (first_out Message (input Message m q))) (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (input Message m q))) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (input Message m q))), inc_dec_in_queue s3 (first_out Message (input Message d (input Message m q))) *)
  intros m q1 H m0 s3 H0 H1.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  generalize (H m0 s3).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m q1))) *)
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  case (eq_site_dec s3 s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite e.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: if eq_site_dec s s then True else False *)
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message copy q))) (s : Site), not (In_queue Message (inc_dec s) (input Message copy q)) *)
  case (eq_site_dec s s).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim n; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_site_dec s s3).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  generalize (H m0 s3).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  generalize (H m0 s3).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.

Lemma inc_dec_in_first_out :
 forall (q : queue Message) (m : Message) (s3 : Site),
 first Message q = value Message m ->
 m <> inc_dec s3 ->
 inc_dec_in_queue s3 q -> inc_dec_in_queue s3 (first_out Message q).
Proof.
(* Goal: forall (q : queue Message) (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q) *)
  simple induction q.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall (d : Message) (q : queue Message) (_ : forall (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message q) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 q), inc_dec_in_queue s3 (first_out Message q)) (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d q)) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d q)), inc_dec_in_queue s3 (first_out Message (input Message d q)) *)
  intros d q0.
(* Goal: forall (_ : forall (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message q0) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 q0), inc_dec_in_queue s3 (first_out Message q0)) (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d q0)) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d q0)), inc_dec_in_queue s3 (first_out Message (input Message d q0)) *)
  case q0.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (m : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (empty Message))) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (empty Message))), inc_dec_in_queue s3 (first_out Message (input Message d (empty Message))) *)
(* Goal: forall (m : Message) (q : queue Message) (_ : forall (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message m q)) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message m q)), inc_dec_in_queue s3 (first_out Message (input Message m q))) (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (input Message m q))) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (input Message m q))), inc_dec_in_queue s3 (first_out Message (input Message d (input Message m q))) *)
  intros m s3.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_site_dec s s3).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: False *)
  generalize H0.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite e.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq (exc Message) (value Message (inc_dec s3)) (value Message m), @eq Message m (inc_dec s3) *)
(* Goal: forall (_ : not (@eq Site s s3)) (_ : @eq (exc Message) (value Message (inc_dec s)) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : False), False *)
(* Goal: forall (_ : @eq (exc Message) (value Message copy) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : False), False *)
(* Goal: forall (m : Message) (q : queue Message) (_ : forall (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message m q)) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message m q)), inc_dec_in_queue s3 (first_out Message (input Message m q))) (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (input Message m q))) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (input Message m q))), inc_dec_in_queue s3 (first_out Message (input Message d (input Message m q))) *)
  generalize (inc_dec s3).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  symmetry  in |- *.
(* Goal: @eq Message m0 m *)
(* Goal: forall (_ : not (@eq Site s s3)) (_ : @eq (exc Message) (value Message (inc_dec s)) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : False), False *)
(* Goal: forall (_ : @eq (exc Message) (value Message copy) (value Message m)) (_ : not (@eq Message m (inc_dec s3))) (_ : False), False *)
(* Goal: forall (m : Message) (q : queue Message) (_ : forall (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message m q)) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message m q)), inc_dec_in_queue s3 (first_out Message (input Message m q))) (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (input Message m q))) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (input Message m q))), inc_dec_in_queue s3 (first_out Message (input Message d (input Message m q))) *)
  injection H3.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
(* Goal: forall (m : Message) (q : queue Message) (_ : forall (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message m q)) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message m q)), inc_dec_in_queue s3 (first_out Message (input Message m q))) (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (input Message m q))) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (input Message m q))), inc_dec_in_queue s3 (first_out Message (input Message d (input Message m q))) *)
  contradiction.
  
(* Goal: forall (m : Message) (q : queue Message) (_ : forall (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message m q)) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message m q)), inc_dec_in_queue s3 (first_out Message (input Message m q))) (m0 : Message) (s3 : Site) (_ : @eq (exc Message) (first Message (input Message d (input Message m q))) (value Message m0)) (_ : not (@eq Message m0 (inc_dec s3))) (_ : inc_dec_in_queue s3 (input Message d (input Message m q))), inc_dec_in_queue s3 (first_out Message (input Message d (input Message m q))) *)
  intros m q1 H m0 s3 H0 H1.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  generalize (H m0 s3).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m q1))) *)
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  case (eq_site_dec s3 s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite e.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: if eq_site_dec s s then True else False *)
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message copy q))) (s : Site), not (In_queue Message (inc_dec s) (input Message copy q)) *)
  case (eq_site_dec s s).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim n; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_site_dec s s3).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  generalize (H m0 s3).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : inc_dec_in_queue s3 (input Message copy (input Message m q1)), inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m q1))) *)
  generalize (H m0 s3).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.



Lemma inc_dec_not_in_collect :
 forall (b : Bag_of_message) (m : Message) (s0 s1 s2 s3 : Site),
 first Message (b s1 s2) = value Message m ->
 ~ inc_dec_in_queue s3 (b s0 owner) ->
 m <> inc_dec s3 ->
 ~ inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner).
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_queue_dec s1 s0 s2 owner).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  decompose [and] a.
(* Goal: inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
  rewrite H2; rewrite H3.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s0 owner s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite collect_here.
(* Goal: not (inc_dec_in_queue s3 (first_out Message (b s0 owner))) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), not (inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)) *)
  apply inc_dec_not_in_first_out with (m := m).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite <- H2; rewrite <- H3; auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite collect_elsewhere.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.


Lemma inc_dec_in_collect :
 forall (b : Bag_of_message) (s0 s1 s2 s3 : Site) (m : Message),
 first Message (b s1 s2) = value Message m ->
 inc_dec_in_queue s3 (b s0 owner) ->
 m <> inc_dec s3 ->
 inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner).
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_queue_dec s1 s0 s2 owner).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  decompose [and] a.
(* Goal: inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
  rewrite H2; rewrite H3.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s0 owner s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite collect_here.
(* Goal: inc_dec_in_queue s3 (first_out Message (b s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
  generalize (inc_dec_not_in_first_out (b s0 owner) m s3).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: inc_dec_in_queue s3 (first_out Message (b s0 owner)) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
  apply inc_dec_in_first_out with (m := m).
(* Goal: @eq (exc Message) (first Message (b s0 owner)) (value Message m) *)
(* Goal: not (@eq Message m (inc_dec s3)) *)
(* Goal: inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall _ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner)), inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) *)
  rewrite <- H2; rewrite <- H3.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite collect_elsewhere.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.

Lemma inc_dec_in_collect2 :
 forall (b : Bag_of_message) (m : Message) (s0 s1 s2 s3 : Site),
 first Message (b s1 s2) = value Message m ->
 inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner) ->
 inc_dec_in_queue s3 (b s0 owner).
Proof.
(* Goal: forall (b : Bag_of_message) (m : Message) (s0 s1 s2 s3 : Site) (_ : @eq (exc Message) (first Message (b s1 s2)) (value Message m)) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  intros b m s0 s1 s2 s3 H.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_queue_dec s1 s0 s2 owner).
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  decompose [and] a.
(* Goal: False *)
  generalize H0.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite H1; rewrite H2.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s0 owner s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite collect_here.
(* Goal: forall _ : inc_dec_in_queue s3 (first_out Message (b s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  elim (b s0 owner).
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall (d : Message) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message q), inc_dec_in_queue s3 q) (_ : inc_dec_in_queue s3 (first_out Message (input Message d q))), inc_dec_in_queue s3 (input Message d q) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  intros d q.
(* Goal: forall (_ : forall _ : inc_dec_in_queue s3 (first_out Message q), inc_dec_in_queue s3 q) (_ : inc_dec_in_queue s3 (first_out Message (input Message d q))), inc_dec_in_queue s3 (input Message d q) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  case q.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_site_dec s s3).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite e.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  case (eq_site_dec s3 s3).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (_ : not (@eq Site s s3)) (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message (inc_dec s) (input Message m0 q)))), inc_dec_in_queue s3 (input Message (inc_dec s) (input Message m0 q)) *)
(* Goal: forall (q : queue Message) (_ : forall _ : inc_dec_in_queue s3 (first_out Message (input Message m0 q)), inc_dec_in_queue s3 (input Message m0 q)) (_ : inc_dec_in_queue s3 (first_out Message (input Message copy (input Message m0 q)))), inc_dec_in_queue s3 (input Message copy (input Message m0 q)) *)
(* Goal: forall (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner)), inc_dec_in_queue s3 (b s0 owner) *)
  elim n.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall _ : inc_dec_in_queue s3 (Collect_message Message b s1 s2 s0 owner), inc_dec_in_queue s3 (b s0 owner) *)
  rewrite collect_elsewhere.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.



Lemma not_inc_dec_in :
 forall q : queue Message,
 (forall s : Site, ~ inc_dec_in_queue s q) ->
 forall s : Site, ~ In_queue Message (inc_dec s) q.

Proof.
(* Goal: forall (q : queue Message) (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q) *)
  simple induction q.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message d q))) (s : Site), not (In_queue Message (inc_dec s) (input Message d q)) *)
  case d.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  eauto.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (In_queue Message (inc_dec s0) (input Message (inc_dec s) q0)) *)
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message copy q))) (s : Site), not (In_queue Message (inc_dec s) (input Message copy q)) *)
  generalize (H0 s).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: if eq_site_dec s s then True else False *)
(* Goal: forall (q : queue Message) (_ : forall (_ : forall s : Site, not (inc_dec_in_queue s q)) (s : Site), not (In_queue Message (inc_dec s) q)) (_ : forall s : Site, not (inc_dec_in_queue s (input Message copy q))) (s : Site), not (In_queue Message (inc_dec s) (input Message copy q)) *)
  case (eq_site_dec s s).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intro; elim n; auto.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  intro; simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  eauto.
Qed.


Lemma joining_node :
 forall (c : Config) (s2 : Site),
 legal c ->
 rt c s2 = false -> forall s3 s4 : Site, parent c s3 s4 -> s2 <> s3.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
  rewrite H2 in H0.
(* Goal: False *)
  generalize H0.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: False *)
  generalize (inc_dec_in s1 (bm c s0 owner) H4).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
  generalize (not_owner_inc3 c s0 owner H s1 H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
  generalize (positive_st c s1 s0 H7 H H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
  generalize (st_rt c s1 H H7 H8).
(* Goal: forall _ : @eq bool (rt c s1) true, False *)
  rewrite H5.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
Qed.


Lemma ancestor_rt :
 forall c : Config,
 legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> rt c s1 = true.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq bool (rt c s4) true *)
(* Goal: forall (s2 s1 s0 : Site) (_ : ancestor c s2 s1) (_ : @eq bool (rt c s2) true) (_ : parent c s1 s0), @eq bool (rt c s2) true *)
  generalize (inc_dec_in s4 (bm c s5 owner) H3).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq bool (rt c s4) true *)
(* Goal: forall (s2 s1 s0 : Site) (_ : ancestor c s2 s1) (_ : @eq bool (rt c s2) true) (_ : parent c s1 s0), @eq bool (rt c s2) true *)
  generalize (not_owner_inc3 c s5 owner H s4 H4).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq bool (rt c s4) true *)
(* Goal: forall (s2 s1 s0 : Site) (_ : ancestor c s2 s1) (_ : @eq bool (rt c s2) true) (_ : parent c s1 s0), @eq bool (rt c s2) true *)
  generalize (positive_st c s4 s5 H5 H H4).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq bool (rt c s4) true *)
(* Goal: forall (s2 s1 s0 : Site) (_ : ancestor c s2 s1) (_ : @eq bool (rt c s2) true) (_ : parent c s1 s0), @eq bool (rt c s2) true *)
  generalize (st_rt c s4 H H5 H6).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.


Lemma ancestor_rt2 :
 forall c : Config,
 legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> rt c s2 = true.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  elim H3; auto.
Qed.

(* the parent of a node cannot be the which receives 
   a gp for the first time *)

Lemma parent_does_not_join :
 forall (c0 : Config) (s2 s3 s4 : Site),
 legal c0 ->
 legal (rec_copy2_trans c0 s2) ->
 parent (rec_copy2_trans c0 s2) s3 s4 ->
 rt c0 s2 = false ->
 first Message (bm c0 owner s2) = value Message copy -> s3 <> s2.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s1 s2) *)
  generalize (inc_dec_in s1 (bm (rec_copy2_trans c0 s2) s0 owner) H5).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
  generalize (not_reflexive (rec_copy2_trans c0 s2) H0 s1 s0 H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
  cut (s1 <> owner).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (positive_st (rec_copy2_trans c0 s2) s1 s0 H8 H0 H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (st_rt (rec_copy2_trans c0 s2) s1 H0 H8 H9).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H5.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (inc_dec_in_collect2 (bm c0) copy s0 owner s2 s1 H3 H11).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (inc_dec_in s1 (bm c0 s0 owner) H12).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (positive_st c0 s1 s0 H8 H H13).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: not (@eq Site s1 owner) *)
  generalize (st_rt c0 s1 H H8 H14).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: not (@eq Site s1 owner) *)
  rewrite H16 in H15.
(* Goal: False *)
(* Goal: not (@eq Site s1 owner) *)
  rewrite H15 in H2.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: not (@eq Site s1 owner) *)
  apply (not_owner_inc3 (rec_copy2_trans c0 s2) s0 owner H0).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.

(* the ancestor of a node cannot be the which receives 
   a gp for the first time *)

Lemma ancestor_does_not_join :
 forall (c0 : Config) (s2 s3 s4 : Site),
 legal c0 ->
 legal (rec_copy2_trans c0 s2) ->
 ancestor (rec_copy2_trans c0 s2) s3 s4 ->
 rt c0 s2 = false ->
 first Message (bm c0 owner s2) = value Message copy -> s3 <> s2.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s1 s2) *)
(* Goal: forall (s3 s1 s0 : Site) (_ : ancestor (rec_copy2_trans c0 s2) s3 s1) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy2_trans c0 s2) s1 s0), not (@eq Site s3 s2) *)
  apply (parent_does_not_join c0 s2 s1 s0).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.

Lemma parent_does_not_join2 :
 forall (c0 : Config) (s1 s2 s3 s4 : Site),
 legal c0 ->
 legal (rec_copy3_trans c0 s1 s2) ->
 parent (rec_copy3_trans c0 s1 s2) s3 s4 ->
 rt c0 s2 = false ->
 first Message (bm c0 s1 s2) = value Message copy -> s3 <> s2.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s0 s2) *)
  generalize (inc_dec_in s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner) H5).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
  generalize (not_reflexive (rec_copy3_trans c0 s1 s2) H0 s0 s5 H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
  cut (s0 <> owner).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (positive_st (rec_copy3_trans c0 s1 s2) s0 s5 H8 H0 H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (st_rt (rec_copy3_trans c0 s1 s2) s0 H0 H8 H9).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H5.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  case (eq_site_dec s2 s5).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite e; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H11.
(* Goal: forall _ : inc_dec_in_queue s0 (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  rewrite post_elsewhere.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (inc_dec_in_collect2 (bm c0) copy s5 s1 s2 s0 H3 H12).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (inc_dec_in s0 (bm c0 s5 owner) H13).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (positive_st c0 s0 s5 H8 H H14).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize (st_rt c0 s0 H H8 H15).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  unfold not in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  rewrite H17 in H16.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  rewrite H16 in H2.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  left; auto.
  
(* Goal: not (@eq Site s0 owner) *)
  apply (not_owner_inc3 (rec_copy3_trans c0 s1 s2) s5 owner H0).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
Qed.

Lemma ancestor_does_not_join2 :
 forall (c0 : Config) (s1 s2 s3 s4 : Site),
 legal c0 ->
 legal (rec_copy3_trans c0 s1 s2) ->
 ancestor (rec_copy3_trans c0 s1 s2) s3 s4 ->
 rt c0 s2 = false ->
 first Message (bm c0 s1 s2) = value Message copy -> s3 <> s2.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s0 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  apply (parent_does_not_join2 c0 s1 s2 s0 s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros; auto.
Qed.


Lemma ancestor_not_reflexive :
 forall c : Config,
 legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> s1 <> s2.
Proof.
  intros c H.
(* Goal: inc_dec_in_queue s1 (b s0 owner) *)
  generalize H.
(* Goal: False *)
  elim H.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  elim H2.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: not (or (@eq Message (inc_dec s) copy) (In_queue Message (inc_dec s) q0)) *)
  intuition.
  
  simple induction t.

(*  1*)
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  elim H3.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H5; simpl in |- *; auto.
  
  apply (inc_dec_in_post2 (bm c0) s7 s6 s1 s2 copy).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H6; simpl in |- *; auto.
  
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply long with (s1 := s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H7; simpl in |- *; auto.
  
  apply (inc_dec_in_post2 (bm c0) s8 s7 s1 s2 copy).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H8; simpl in |- *; auto.
  
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* 2 *)
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  elim H3.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H5; simpl in |- *; auto.
  
  apply (inc_dec_in_collect2 (bm c0) dec s7 s1 s2 s6).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H6; simpl in |- *; auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply long with (s1 := s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H7; simpl in |- *; auto.
  
  apply (inc_dec_in_collect2 (bm c0) dec s8 s1 s2 s7).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H8; simpl in |- *; auto.
  
(* 3 *)
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  elim H3.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H5; simpl in |- *; auto.
  
  apply (inc_dec_in_collect2 (bm c0) (inc_dec s3) s7 s1 owner s6).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  apply
   (inc_dec_in_post2 (Collect_message Message (bm c0) s1 owner) s7 s6 owner
      s3 dec).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H6; simpl in |- *; auto.
  
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply long with (s1 := s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H7; simpl in |- *; auto.
  
  apply (inc_dec_in_collect2 (bm c0) (inc_dec s3) s8 s1 owner s7).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  apply
   (inc_dec_in_post2 (Collect_message Message (bm c0) s1 owner) s8 s7 owner
      s3 dec).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H8; simpl in |- *; auto.
  
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* 4 *)
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  elim H3.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H5; simpl in |- *; auto.
  
  apply (inc_dec_in_collect2 (bm c0) copy s7 s1 s2 s6).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  apply
   (inc_dec_in_post2 (Collect_message Message (bm c0) s1 s2) s7 s6 s2 s1 dec).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H6; simpl in |- *; auto.
  
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply long with (s1 := s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H7; simpl in |- *; auto.
  
  apply (inc_dec_in_collect2 (bm c0) copy s8 s1 s2 s7).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  apply
   (inc_dec_in_post2 (Collect_message Message (bm c0) s1 s2) s8 s7 s2 s1 dec).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H8; simpl in |- *; auto.
  
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  

  (*  5 *)
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  case (eq_site_dec s0 s2).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  generalize e e0 e1.
  elim H3.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro; intro; intro.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  rewrite e4 in H5.
  rewrite e4 in H6.
  rewrite e4.
  generalize (inc_dec_in s5 (bm (rec_copy2_trans c0 s2) s2 owner) H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply not_reflexive with (c := rec_copy2_trans c0 s2).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.

  apply (ancestor_does_not_join c0 s5 s3 s4).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite e4; auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite e4; auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite e4; auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite e4; auto.


   (* base case when s0!=s2*)
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  generalize e.
  generalize n.
  elim H3.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
  generalize n0.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H5; simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  unfold Set_rec_table in |- *; rewrite other_site; auto.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H6; simpl in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply (inc_dec_in_collect2 (bm c0) copy s6 owner s2 s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.

      (* inductive case when s0!=s1*)
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s5 *)
  apply long with (s1 := s4).
  apply H5.
  apply (parent_does_not_join c0 s2 s4 s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.

  
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  generalize n0; elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H7; simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  unfold Set_rec_table in |- *; rewrite other_site; auto.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H8; simpl in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply (inc_dec_in_collect2 (bm c0) copy s7 owner s2 s6).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
 

  (*  6 *)

  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  case (eq_site_dec s2 s3).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  generalize e e0 e1.
  elim H3.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro; intro; intro.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  generalize (inc_dec_in s6 (bm (rec_copy3_trans c0 s1 s2) s7 owner) H6).
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply not_reflexive with (c := rec_copy3_trans c0 s1 s2).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  rewrite <- e4.
  apply (ancestor_does_not_join2 c0 s1 s2 s4 s5).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  generalize e.
  generalize n.
  generalize n1.
  elim H3.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
  generalize n2 n3 e1.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H5; simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  unfold Set_rec_table in |- *; rewrite other_site; auto.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H6; simpl in |- *.
(* Goal: forall _ : inc_dec_in_queue s0 (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  rewrite post_elsewhere.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply (inc_dec_in_collect2 (bm c0) copy s7 s1 s2 s6).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  left; auto.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply long with (s1 := s5).
  apply H5.
  generalize (parent_does_not_join2 c0 s1 s2 s5 s6 H0 H2 H6 e1 e0).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  generalize n2.
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H7; simpl in |- *.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  unfold Set_rec_table in |- *; rewrite other_site; auto.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H8; simpl in |- *.
(* Goal: forall _ : inc_dec_in_queue s0 (Post_message Message (inc_dec s1) (Collect_message Message (bm c0) s1 s2) s2 owner s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  rewrite post_elsewhere.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply (inc_dec_in_collect2 (bm c0) copy s8 s1 s2 s7).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  left; auto.

  (* 7 *)
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply H1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
  elim H3.
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  simpl in |- *.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: ancestor s1 s3 *)
(* Goal: forall _ : not (@eq Site s1 s0), ancestor s1 s3 *)
(* Goal: forall _ : and (not (@eq Site s1 s0)) (not (ancestor s1 s0)), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3))) *)
  apply short.
(* Goal: forall _ : direct_son s1, or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall _ : not (@eq Site s0 s1), or (or (@eq Site s1 s2) (ancestor s1 s2)) (and (not (@eq Site s1 s2)) (not (ancestor s1 s2))) *)
(* Goal: forall (s2 s3 s0 : Site) (_ : ancestor s2 s3) (_ : forall (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s3) (ancestor s1 s3)) (and (not (@eq Site s1 s3)) (not (ancestor s1 s3)))) (_ : parent s3 s0) (_ : direct_son s2) (_ : indirect_son1 s1), or (or (@eq Site s1 s0) (ancestor s1 s0)) (and (not (@eq Site s1 s0)) (not (ancestor s1 s0))) *)
  elim H4.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H5; simpl in |- *; auto.
  unfold Reset_rec_table in |- *.
  case (eq_site_dec s s5).
  intro; rewrite e1.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  rewrite that_site; auto.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro; discriminate.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intro; rewrite other_site; auto.
  
(* Goal: forall _ : inc_dec_in_queue s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner), not (@eq Site s0 s2) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H6; simpl in |- *.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro.
  apply (inc_dec_in_post2 (bm c0) s5 s4 s owner dec).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
  
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  apply long with (s1 := s3).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.
  
(* Goal: forall _ : ancestor s3 s0, @eq Site s3 s0 *)
(* Goal: @eq Site s0 s4 *)
  elim H6.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  apply parent_intro.
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  generalize H7; simpl in |- *; auto.
  case (eq_site_dec s s6).
  intro; rewrite e1; unfold Reset_rec_table in |- *; rewrite that_site.
(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  intro; discriminate.
  
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intro; unfold Reset_rec_table in |- *; rewrite other_site; auto.
  
(* Goal: forall _ : @eq Site s0 s2, False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  generalize H8; simpl in |- *; intro.
  apply (inc_dec_in_post2 (bm c0) s6 s5 s owner dec).
(* Goal: @eq (exc Message) (first Message (bm c0 s1 s2)) (value Message copy) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  auto.

(* Goal: False *)
(* Goal: or (not (@eq Site s2 s5)) (not (@eq Site owner owner)) *)
(* Goal: not (@eq Site s0 owner) *)
  discriminate.
(* Not completed *)
Admitted.

(*
Lemma ancestor_has_positive_st :
 forall c : Config,
 legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> (st c s1 > 0)%Z.
Proof.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: @eq bool (rt c s2) true *)
  elim H0.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
(* Goal: not (@eq Site s3 s2) *)
  elim H1.
(* Goal: forall (s3 s0 : Site) (_ : parent (rec_copy3_trans c0 s1 s2) s3 s0), not (@eq Site s3 s2) *)
(* Goal: forall (s3 s4 s0 : Site) (_ : ancestor (rec_copy3_trans c0 s1 s2) s3 s4) (_ : not (@eq Site s3 s2)) (_ : parent (rec_copy3_trans c0 s1 s2) s4 s0), not (@eq Site s3 s2) *)
  intros.
  generalize (inc_dec_in c s4 (bm c s5 owner) H3).
*)

End INVARIANT6_bis.
