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


Require Export DistributedReferenceCounting.machine4.machine.
Require Export DistributedReferenceCounting.machine4.cardinal.
Require Export DistributedReferenceCounting.machine4.comm.

Unset Standard Proposition Elimination Names.

Section IN_Q_BEFORE.

Variable data : Set.

(* This predicate tells us if we can find a data d
   - before the first occurrence of d1, if d1 belongs to q,
   - otherwise it returns true when d1 does not belong to q.
*)
  
Hypothesis eq_data_dec : eq_dec data.

Fixpoint In_queue_before_data (d d1 : data) (q : queue data) {struct q} :
 Prop :=
  match q with
  | empty => True
  | input d' q' =>
      if eq_data_dec d' d1
      then False
      else d' = d \/ In_queue_before_data d d1 q'
  end.

(* same except that I pass a predicate to recognise d1 *)

Fixpoint In_queue_before (d : data) (f1 : data -> bool) 
 (q : queue data) {struct q} : Prop :=
  match q with
  | empty => True
  | input d' q' =>
      if eq_bool_dec (f1 d')
      then False
      else d' = d \/ In_queue_before d f1 q'
  end.


End IN_Q_BEFORE.

Section ALTERNATE.

Definition is_inc_dec (m : Message) :=
  match m with
  | inc_dec _ => true
  | _ => false
  end.



Inductive alternate : queue Message -> Prop :=
  | alt_null : alternate (empty Message)
  | alt_any_alt :
      forall (qm : queue Message) (m : Message),
      (forall s : Site, m <> inc_dec s) ->
      alternate qm -> alternate (input Message m qm)
  | alt_inc_dec :
      forall (qm : queue Message) (s0 : Site),
      alternate qm ->
      In_queue_before Message dec is_inc_dec qm ->
      alternate (input Message (inc_dec s0) qm).

Lemma dec_is_not_inc : forall s : Site, dec <> inc_dec s.
Proof.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
 intro; discriminate.
Qed.

Inductive D_queue : queue Message -> Prop :=
  | D_empty : D_queue (empty Message)
  | D_dec :
      forall qm : queue Message,
      alternate qm -> In_queue_before Message dec is_inc_dec qm -> D_queue qm.

Lemma not_D_queue :
 forall (q0 : queue Message) (m : Message),
 ~ D_queue q0 -> m <> dec -> ~ D_queue (input Message m q0).
Proof.
(* Goal: forall (q0 : queue Message) (m : Message) (_ : not (D_queue q0)) (_ : not (@eq Message m dec)), not (D_queue (input Message m q0)) *)
  intros; red in |- *; intro.
(* Goal: alternate (input Message copy (append Message q q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  inversion H1.
(* Goal: D_queue (first_out Message q0) *)
  elim H.
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  generalize H3.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  generalize H2.
(* Goal: alternate (append Message q1 q2) *)
  generalize H0.
(* Goal: forall (_ : forall _ : In_queue_before Message dec is_inc_dec q0, In_queue_before Message dec is_inc_dec (first_out Message q0)) (_ : or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q0)), In_queue_before Message dec is_inc_dec match q0 with | @empty _ => empty Message | @input _ d q => input Message copy (first_out Message q0) end *)
  case q0.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: D_queue (empty Message) *)
(* Goal: forall (m : Message) (q : queue Message) (_ : alternate (input Message m q)) (_ : In_queue_before Message dec is_inc_dec (input Message m q)), D_queue (first_out Message (input Message m q)) *)
  apply D_empty.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: D_queue (input Message copy (append Message q3 q4)) *)
  apply D_dec.
(* Goal: alternate (input Message m0 q) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message m0 q) *)
  inversion H6.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: if eq_bool_dec (is_inc_dec m0) then False else or (@eq Message m0 dec) (In_queue_before Message dec is_inc_dec q) *)
  generalize H5 H7.
(* Goal: forall (_ : forall s : Site, not (@eq Message m (inc_dec s))) (_ : alternate qm) (_ : In_queue_before Message dec is_inc_dec (input Message m qm)), alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  case m.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim H8; auto.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec (inc_dec s)) then False else or (@eq Message (inc_dec s) dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  case (eq_bool_dec (is_inc_dec (inc_dec s))).
(* Goal: forall (_ : @eq bool (is_inc_dec (inc_dec s)) true) (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : False), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (_ : @eq bool (is_inc_dec (inc_dec s)) false) (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : or (@eq Message (inc_dec s) dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  intros; contradiction.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H9; intro.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim H8; auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall (_ : not (@eq Message copy dec)) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (if eq_bool_dec (is_inc_dec m0) then False else or (@eq Message m0 dec) (In_queue_before Message dec is_inc_dec q))), if eq_bool_dec (is_inc_dec m0) then False else or (@eq Message m0 dec) (In_queue_before Message dec is_inc_dec q) *)
  case (eq_bool_dec (is_inc_dec copy)).
(* Goal: forall (_ : @eq bool (is_inc_dec (inc_dec s)) true) (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : False), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (_ : @eq bool (is_inc_dec (inc_dec s)) false) (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : or (@eq Message (inc_dec s) dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  intros; contradiction.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H9; intro.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim H8; auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.

Lemma D_queue_is_alternate :
 forall q0 : queue Message, D_queue q0 -> alternate q0.
Proof.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: D_queue (first_out Message q0) *)
  elim H.
(* Goal: alternate (empty Message) *)
(* Goal: In_queue_before Message dec is_inc_dec (empty Message) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  apply alt_null.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.
	

Lemma in_q_before_first_out :
 forall q : queue Message,
 In_queue_before Message dec is_inc_dec q ->
 In_queue_before Message dec is_inc_dec (first_out Message q).
Proof.
(* Goal: forall (q : queue Message) (_ : In_queue_before Message dec is_inc_dec q), In_queue_before Message dec is_inc_dec (first_out Message q) *)
  simple induction q.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall (q2 : queue Message) (_ : In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2))), In_queue_before Message dec is_inc_dec (append Message q q2)) (q2 : queue Message) (_ : if eq_bool_dec (is_inc_dec d) then False else or (@eq Message d dec) (In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)))), if eq_bool_dec (is_inc_dec d) then False else or (@eq Message d dec) (In_queue_before Message dec is_inc_dec (append Message q q2)) *)
  case d.
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec dec) then False else or (@eq Message dec dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message dec (first_out Message q) end *)
(* Goal: forall (s : Site) (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec (inc_dec s)) then False else or (@eq Message (inc_dec s) dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  case (eq_bool_dec (is_inc_dec dec)).
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro; intro.
(* Goal: forall (_ : forall _ : In_queue_before Message dec is_inc_dec q0, In_queue_before Message dec is_inc_dec (first_out Message q0)) (_ : or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q0)), In_queue_before Message dec is_inc_dec match q0 with | @empty _ => empty Message | @input _ d q => input Message copy (first_out Message q0) end *)
  case q0.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  case (eq_bool_dec false).
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec (inc_dec s)) then False else or (@eq Message (inc_dec s) dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  case (eq_bool_dec (is_inc_dec (inc_dec s))).
(* Goal: forall (_ : @eq bool (is_inc_dec (inc_dec s)) true) (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : False), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (_ : @eq bool (is_inc_dec (inc_dec s)) false) (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : or (@eq Message (inc_dec s) dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message (inc_dec s) (first_out Message q) end *)
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  intros; contradiction.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  simpl in |- *; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q : queue Message) (_ : forall _ : In_queue_before Message dec is_inc_dec q, In_queue_before Message dec is_inc_dec (first_out Message q)) (_ : or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q)), In_queue_before Message dec is_inc_dec match q with | @empty _ => empty Message | @input _ d q0 => input Message copy (first_out Message q) end *)
  case (eq_bool_dec false).
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro; intro.
(* Goal: forall (_ : forall _ : In_queue_before Message dec is_inc_dec q0, In_queue_before Message dec is_inc_dec (first_out Message q0)) (_ : or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec q0)), In_queue_before Message dec is_inc_dec match q0 with | @empty _ => empty Message | @input _ d q => input Message copy (first_out Message q0) end *)
  case q0.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (first_out Message (input Message m q1))) *)
  elim H0.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (first_out Message (input Message m q1))) *)
  generalize (H H1).
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  right; auto.
Qed.


Lemma alt_first_out :
 forall q0 : queue Message, alternate q0 -> alternate (first_out Message q0).
Proof.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  intros; elim H; simpl in |- *.
(* Goal: alternate (empty Message) *)
(* Goal: In_queue_before Message dec is_inc_dec (empty Message) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  apply alt_null.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intros qm m; intro.
(* Goal: forall (_ : alternate qm) (_ : alternate (first_out Message qm)) (_ : In_queue_before Message dec is_inc_dec qm), alternate match qm with | @empty _ => empty Message | @input _ d q => input Message (inc_dec s0) (first_out Message qm) end *)
  case qm.
(* Goal: alternate (empty Message) *)
(* Goal: In_queue_before Message dec is_inc_dec (empty Message) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  intros; apply alt_null.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: alternate (append Message q1 q2) *)
  generalize H0.
(* Goal: forall (_ : forall s : Site, not (@eq Message m (inc_dec s))) (_ : alternate qm) (_ : In_queue_before Message dec is_inc_dec (input Message m qm)), alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  case m.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (_ : alternate qm) (_ : alternate (first_out Message qm)) (_ : In_queue_before Message dec is_inc_dec qm), alternate match qm with | @empty _ => empty Message | @input _ d q => input Message (inc_dec s0) (first_out Message qm) end *)
  case qm.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (first_out Message (input Message m q)) *)
  apply in_q_before_first_out.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.



Lemma D_first_out :
 forall q0 : queue Message, D_queue q0 -> D_queue (first_out Message q0).
Proof.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: D_queue (first_out Message q0) *)
  elim H.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: D_queue (empty Message) *)
(* Goal: forall (m : Message) (q : queue Message) (_ : alternate (input Message m q)) (_ : In_queue_before Message dec is_inc_dec (input Message m q)), D_queue (first_out Message (input Message m q)) *)
  apply D_empty.
  
(* Goal: forall (qm : queue Message) (_ : alternate qm) (_ : In_queue_before Message dec is_inc_dec qm), D_queue (first_out Message qm) *)
  simple destruct qm.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: D_queue (empty Message) *)
(* Goal: forall (m : Message) (q : queue Message) (_ : alternate (input Message m q)) (_ : In_queue_before Message dec is_inc_dec (input Message m q)), D_queue (first_out Message (input Message m q)) *)
  apply D_empty.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: D_queue (input Message copy (append Message q3 q4)) *)
  apply D_dec.
(* Goal: alternate (first_out Message (input Message m q)) *)
(* Goal: In_queue_before Message dec is_inc_dec (first_out Message (input Message m q)) *)
  apply alt_first_out.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (first_out Message (input Message m q)) *)
  apply in_q_before_first_out.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.

Lemma D_input :
 forall q : queue Message, D_queue (input Message copy q) -> D_queue q.
Proof.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate q2 *)
(* Goal: forall (d : Message) (q : queue Message) (_ : forall _ : alternate (append Message q (input Message copy q2)), alternate (append Message q q2)) (_ : alternate (append Message (input Message d q) (input Message copy q2))), alternate (append Message (input Message d q) q2) *)
  inversion H.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: D_queue (input Message copy (append Message q3 q4)) *)
  apply D_dec.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  generalize H1; simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H7; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.	

End ALTERNATE.

Section MESS_ALT.

(* consequence sur la structure alternee *)

Variable b0 : Bag_of_Data Message.

Variable s0 : Site.

Lemma D_collect :
 forall s1 s2 : Site,
 D_queue (b0 s0 owner) -> D_queue (Collect_message Message b0 s1 s2 s0 owner).
Proof.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
 intros; case (eq_queue_dec s1 s0 s2 owner); intro.
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 decompose [and] a; rewrite H0; rewrite H1.
(* Goal: D_queue (Collect_message Message b0 s0 owner s0 owner) *)
(* Goal: D_queue (Collect_message Message b0 s1 s2 s0 owner) *)
 rewrite collect_here; apply D_first_out; trivial.

(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
 rewrite collect_elsewhere; auto.
Qed.

Lemma D_post_elsewhere :
 forall (s1 s2 : Site) (m : Message),
 s1 <> s0 \/ s2 <> owner ->
 D_queue (b0 s0 owner) -> D_queue (Post_message Message m b0 s1 s2 s0 owner).
Proof.
(* Goal: forall (s1 s2 : Site) (m : Message) (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : alternate (b0 s0 owner)), alternate (Post_message Message m b0 s1 s2 s0 owner) *)
 intros; rewrite post_elsewhere; trivial.
Qed.

Lemma D_post_dec :
 alternate (b0 s0 owner) ->
 D_queue (Post_message Message dec b0 s0 owner s0 owner).
Proof.
(* Goal: forall _ : alternate (b0 s0 owner), D_queue (Post_message Message dec b0 s0 owner s0 owner) *)
  intros; rewrite post_here.
(* Goal: D_queue (input Message copy (append Message q3 q4)) *)
  apply D_dec.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.

Lemma alt_collect :
 forall s1 s2 : Site,
 alternate (b0 s0 owner) ->
 alternate (Collect_message Message b0 s1 s2 s0 owner).
Proof.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
 intros; case (eq_queue_dec s1 s0 s2 owner); intro.
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 decompose [and] a; rewrite H0; rewrite H1.
(* Goal: alternate (Collect_message Message b0 s0 owner s0 owner) *)
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 rewrite collect_here; apply alt_first_out; trivial.

(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
 rewrite collect_elsewhere; auto.
Qed.

Lemma alt_post_elsewhere :
 forall (s1 s2 : Site) (m : Message),
 s1 <> s0 \/ s2 <> owner ->
 alternate (b0 s0 owner) ->
 alternate (Post_message Message m b0 s1 s2 s0 owner).
Proof.
(* Goal: forall (s1 s2 : Site) (m : Message) (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : alternate (b0 s0 owner)), alternate (Post_message Message m b0 s1 s2 s0 owner) *)
 intros; rewrite post_elsewhere; trivial.
Qed.

Lemma alt_post_any :
 forall m : Message,
 (forall s : Site, m <> inc_dec s) ->
 alternate (b0 s0 owner) ->
 alternate (Post_message Message m b0 s0 owner s0 owner).
Proof.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
 intros; rewrite post_here; apply alt_any_alt; auto.
Qed.



Lemma alt_post_inc :
 forall s1 : Site,
 alternate (b0 s0 owner) ->
 In_queue_before Message dec is_inc_dec (b0 s0 owner) ->
 alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner).
Proof.
(* Goal: forall (s1 : Site) (_ : alternate (b0 s0 owner)) (_ : or (@eq (queue Message) (b0 s0 owner) (empty Message)) (@eq (exc Message) (last Message (b0 s0 owner)) (value Message dec))), alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner) *)
  intros s1 H; rewrite post_here.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  inversion H; intros.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (empty Message) *)
(* Goal: In_queue_before Message dec is_inc_dec (empty Message) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  apply alt_null.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  generalize H1 H2 H3.
(* Goal: forall (_ : forall s : Site, not (@eq Message m (inc_dec s))) (_ : alternate qm) (_ : In_queue_before Message dec is_inc_dec (input Message m qm)), alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  case m.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim (H4 s); auto.
  
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  generalize H3.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec true); intro.
(* Goal: forall _ : False, alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
(* Goal: forall _ : False, alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  intro; contradiction.
  
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
Qed.

(* no longer useful 'cos copy is out of band and could be last *)

Lemma alt_post_inc_old :
 forall s1 : Site,
 alternate (b0 s0 owner) ->
 b0 s0 owner = empty Message \/
 last Message (b0 s0 owner) = value Message dec ->
 alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner).
Proof.
(* Goal: forall (s1 : Site) (_ : alternate (b0 s0 owner)) (_ : or (@eq (queue Message) (b0 s0 owner) (empty Message)) (@eq (exc Message) (last Message (b0 s0 owner)) (value Message dec))), alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner) *)
  intros s1 H; rewrite post_here.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  inversion H; simpl in |- *; intros.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (empty Message) *)
(* Goal: In_queue_before Message dec is_inc_dec (empty Message) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  apply alt_null.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) qm)) *)
  replace m with dec.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H3; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
(* Goal: alternate (input Message copy (append Message q (input Message copy q2))) *)
  inversion H4.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H3; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
Qed.


Lemma in_q_before_append :
 forall q1 q2 : queue Message,
 In_queue_before Message dec is_inc_dec (append Message q1 q2) ->
 In_queue_before Message dec is_inc_dec
   (append Message q1 (input Message copy q2)).
Proof.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simple induction q1; simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  right; auto.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall (q2 : queue Message) (_ : In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2))), In_queue_before Message dec is_inc_dec (append Message q q2)) (q2 : queue Message) (_ : if eq_bool_dec (is_inc_dec d) then False else or (@eq Message d dec) (In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)))), if eq_bool_dec (is_inc_dec d) then False else or (@eq Message d dec) (In_queue_before Message dec is_inc_dec (append Message q q2)) *)
  case d.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q : queue Message) (_ : forall (q2 : queue Message) (_ : In_queue_before Message dec is_inc_dec (append Message q q2)), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2))) (_ : queue Message) (_ : False), False *)
(* Goal: forall (q : queue Message) (_ : forall (q2 : queue Message) (_ : In_queue_before Message dec is_inc_dec (append Message q q2)), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2))) (q2 : queue Message) (_ : if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), if eq_bool_dec (is_inc_dec copy) then False else or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2))) *)
  case (eq_bool_dec true).
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  right.
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H0; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.

Lemma in_q_before_append2 :
 forall q1 q2 : queue Message,
 In_queue_before Message dec is_inc_dec
   (append Message q1 (input Message copy q2)) ->
 In_queue_before Message dec is_inc_dec (append Message q1 q2).
Proof.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simple induction q1; simpl in |- *.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q : queue Message) (_ : forall (q2 : queue Message) (_ : In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2))), In_queue_before Message dec is_inc_dec (append Message q q2)) (q2 : queue Message) (_ : if eq_bool_dec (is_inc_dec d) then False else or (@eq Message d dec) (In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)))), if eq_bool_dec (is_inc_dec d) then False else or (@eq Message d dec) (In_queue_before Message dec is_inc_dec (append Message q q2)) *)
  case d.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  right.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H0; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.

Lemma alt_shuffle_copy1 :
 forall q1 q2 : queue Message,
 alternate (input Message copy (append Message q1 q2)) ->
 alternate (append Message q1 (input Message copy q2)).
Proof.
(* Goal: forall (q1 q2 : queue Message) (_ : D_queue (input Message copy (append Message q1 q2))), D_queue (append Message q1 (input Message copy q2)) *)
  intros q1 q2.
(* Goal: forall _ : D_queue (input Message copy (append Message q1 q2)), D_queue (append Message q1 (input Message copy q2)) *)
  elim q1.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  case d; intros.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  inversion H4; auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
(* Goal: alternate (input Message copy (append Message q (input Message copy q2))) *)
  inversion H4.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
(* Goal: alternate (input Message copy (append Message q (input Message copy q2))) *)
  inversion H4.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim (H11 s); auto.
  
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  intro; discriminate; auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
(* Goal: alternate (input Message copy (append Message q (input Message copy q2))) *)
  inversion H4.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim (H7 s); auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  apply in_q_before_append.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.

Lemma alt_shuffle_copy2 :
 forall q1 q2 : queue Message,
 alternate (append Message q1 (input Message copy q2)) ->
 alternate (append Message q1 q2).
Proof.
(* Goal: forall (q1 q2 : queue Message) (_ : D_queue (input Message copy (append Message q1 q2))), D_queue (append Message q1 (input Message copy q2)) *)
  intros q1 q2.
(* Goal: forall _ : D_queue (input Message copy (append Message q1 q2)), D_queue (append Message q1 (input Message copy q2)) *)
  elim q1.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: alternate q2 *)
(* Goal: forall (d : Message) (q : queue Message) (_ : forall _ : alternate (append Message q (input Message copy q2)), alternate (append Message q q2)) (_ : alternate (append Message (input Message d q) (input Message copy q2))), alternate (append Message (input Message d q) q2) *)
  inversion H.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  case d; intros.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim (H3 s); auto.
  
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 q2) *)
  apply in_q_before_append2.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: alternate (append Message q q2) *)
  apply H.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.




Lemma alt_shuffle_copy :
 forall q1 q2 q3 q4 : queue Message,
 append Message q1 q2 = append Message q3 q4 ->
 alternate (append Message q1 (input Message copy q2)) ->
 alternate (append Message q3 (input Message copy q4)).
Proof.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: alternate (append Message q (input Message copy q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  apply alt_shuffle_copy1.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  rewrite <- H.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q1 q2) *)
  generalize H0.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  elim q1; simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  inversion H1; auto.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  case d; intros.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q q2) *)
  apply H1.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  inversion H2; auto.
  
(* Goal: alternate (append Message q (input Message copy q2)) *)
  inversion H2.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  elim (H5 s); auto.
  
(* Goal: alternate (input Message (inc_dec s) (append Message q q2)) *)
(* Goal: alternate (input Message copy (append Message q q2)) *)
  apply alt_inc_dec.
(* Goal: alternate (append Message q q2) *)
  apply H1.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 q2) *)
  apply in_q_before_append2.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q q2) *)
  apply H1.
(* Goal: alternate (append Message q (input Message copy q2)) *)
  inversion H2.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.


Lemma D_shuffle_copy1 :
 forall q1 q2 : queue Message,
 D_queue (input Message copy (append Message q1 q2)) ->
 D_queue (append Message q1 (input Message copy q2)).
Proof.
(* Goal: forall (q1 q2 : queue Message) (_ : D_queue (input Message copy (append Message q1 q2))), D_queue (append Message q1 (input Message copy q2)) *)
  intros q1 q2.
(* Goal: forall _ : D_queue (input Message copy (append Message q1 q2)), D_queue (append Message q1 (input Message copy q2)) *)
  elim q1.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  case d; intros.
(* Goal: D_queue (input Message copy (append Message q3 q4)) *)
  apply D_dec.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q (input Message copy q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  apply alt_shuffle_copy1.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: alternate (input Message copy (append Message q q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  inversion H1.
(* Goal: alternate (input Message copy (append Message q q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  inversion H7.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  generalize H2.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec true); intro.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H4; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: D_queue (input Message (inc_dec s) (append Message q (input Message copy q2))) *)
(* Goal: forall _ : or (@eq Message copy dec) False, D_queue (input Message (inc_dec s) (append Message q (input Message copy q2))) *)
(* Goal: D_queue (input Message copy (append Message q (input Message copy q2))) *)
  contradiction.
  
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: D_queue (input Message copy (append Message q3 q4)) *)
  apply D_dec.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q (input Message copy q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  apply alt_shuffle_copy1.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: alternate (input Message copy (append Message q q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  inversion H1.
(* Goal: alternate (input Message copy (append Message q q2)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q (input Message copy q2))) *)
  inversion H7.
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  right.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  generalize H2.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  intro.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H4; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  elim H5; intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  apply in_q_before_append.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.



Lemma D_shuffle_copy :
 forall q1 q2 q3 q4 : queue Message,
 append Message q1 q2 = append Message q3 q4 ->
 D_queue (append Message q1 (input Message copy q2)) ->
 D_queue (append Message q3 (input Message copy q4)).
Proof.
(* Goal: forall (q1 q2 q3 q4 : queue Message) (_ : @eq (queue Message) (append Message q1 q2) (append Message q3 q4)) (_ : D_queue (append Message q1 (input Message copy q2))), D_queue (append Message q3 (input Message copy q4)) *)
  intros.
(* Goal: D_queue (append Message q3 (input Message copy q4)) *)
  apply D_shuffle_copy1.
(* Goal: D_queue (input Message copy (append Message q3 q4)) *)
  apply D_dec.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  generalize H2.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  case q1; simpl in |- *.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  intros; discriminate.
  
(* Goal: alternate (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_any_alt.
(* Goal: forall s : Site, not (@eq Message copy (inc_dec s)) *)
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  intro; discriminate.
  
(* Goal: alternate (append Message q3 q4) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_shuffle_copy2.
(* Goal: alternate (append Message q3 (input Message copy q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  apply alt_shuffle_copy with (q1 := q1) (q2 := q2).
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  inversion H0.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  generalize H2.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  case q1; simpl in |- *; intros; discriminate.
  
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q3 q4)) *)
  rewrite <- H.
(* Goal: In_queue_before Message dec is_inc_dec (input Message copy (append Message q1 q2)) *)
  simpl in |- *.
(* Goal: forall _ : or (@eq Message copy dec) (or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q q2))), In_queue_before Message dec is_inc_dec (append Message q (input Message copy q2)) *)
  case (eq_bool_dec false); intro.
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  discriminate.
  
(* Goal: or (@eq Message copy dec) (In_queue_before Message dec is_inc_dec (append Message q1 q2)) *)
  right.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 q2) *)
  apply in_q_before_append2.
(* Goal: In_queue_before Message dec is_inc_dec (append Message q1 (input Message copy q2)) *)
  auto.
Qed.




End MESS_ALT.

