Require Import ZArith.
Require Import Time.
Require Import TimeSyntax.
Require Import Timebase.
Require Import Omega.
Require Import Evenements.

Set Implicit Arguments.
Unset Strict Implicit.

Parameter tau2 tau3 : Time.
Axiom Tlt_tau3_tau2 : tau3 </ tau2.
Axiom tau3_pos : T0 </ tau3.

Hint Resolve Tlt_tau3_tau2 tau3_pos: abr.


Lemma tau2_pos : T0 </ tau2.
apply Tlt_trans with tau3; auto with abr.
Qed.

Hint Resolve tau2_pos: abr.

Lemma Tlt_plus_tau3_tau2 : ∀ t : Time, t +/ tau3 </ t +/ tau2.
auto with time abr.
Qed.

Hint Resolve Tlt_plus_tau3_tau2: abr.

Lemma Tlt_plus_tau2_immediate :
 ∀ t1 t2 : Time, t1 </ t2 +/ tau3 → t1 </ t2 +/ tau2.
eauto with time abr.
Qed.

Lemma Tlt_plus_tau3_immediate :
 ∀ t1 t2 : Time, t1 +/ tau2 </ t2 → t1 +/ tau3 </ t2.
eauto with time abr.
Qed.

Lemma Tlt_plus_tau3_Tle_immediate :
 ∀ t1 t2 : Time, t1 +/ tau3 </ t2 → t1 <=/ t2.
eauto with time abr.
Qed.

Hint Immediate Tlt_plus_tau2_immediate Tlt_plus_tau3_immediate
  Tlt_plus_tau3_Tle_immediate: abr.

Lemma Tle_plus_tau2_immediate :
 ∀ t1 t2 : Time, t1 <=/ t2 +/ tau3 → t1 <=/ t2 +/ tau2.
intros; apply Tle_trans with (t2 +/ tau3); auto with time abr.
Qed.

Lemma Tle_plus_tau3_immediate :
 ∀ t1 t2 : Time, t1 +/ tau2 <=/ t2 → t1 +/ tau3 <=/ t2.
intros; apply Tle_trans with (t1 +/ tau2); auto with time abr.
Qed.

Hint Immediate Tle_plus_tau2_immediate Tle_plus_tau3_immediate: abr.


Definition pertinent (l : schedule) (t v : Time) :=
  v +/ tau3 <=/ t ∧
  forall_sch (fun (u : Time) (_ : RM) ⇒ u <=/ v ∨ t </ u +/ tau2) l.

Hint Unfold pertinent: abr.


Lemma pertinent_add_simpl :
 ∀ (l : schedule) (t v t' : Time) (r : RM),
 pertinent (add_sch t' r l) t v → pertinent l t v.
intros.
case H; split; trivial.
inversion H1; trivial.
Qed.

Lemma pertinent_add_simpl_hd :
 ∀ (l : schedule) (t v t' : Time) (r : RM),
 pertinent (add_sch t' r l) t v → t' <=/ v ∨ t </ t' +/ tau2.
intros l t v t' r (prop1, prop2).
inversion prop2; trivial.
Qed.

Lemma pertinent_add :
 ∀ (l : schedule) (t v t' : Time) (r : RM),
 pertinent l t v →
 t' <=/ v ∨ t </ t' +/ tau2 → pertinent (add_sch t' r l) t v.
intros l t v t' r (prop1, prop2) H.
split; auto with eve.
Qed.
Hint Resolve pertinent_add: abr.

Lemma pertinent_last :
 ∀ (l : schedule) (t t' : Time),
 t' +/ tau3 <=/ t → Tle_sch l t' → pertinent l t t'.
split; trivial.
apply forall_incl_sch with (2 := H0); auto with time.
Qed.

Definition ACRA (l : schedule) (t : Time) (x : RM) :=
  forall_sch (fun (v : Time) (rv : RM) ⇒ pertinent l t v → (rv ≤ x)%Z) l ∧
  exists_sch (fun (u : Time) (ru : RM) ⇒ ru = x ∧ pertinent l t u) l.

Hint Unfold ACRA: abr.

Lemma ACRA_exists_last :
 ∀ (l : schedule) (t t' : Time) (x : RM),
 t' +/ tau3 <=/ t →
 Tlt_sch l t' →
 exists_sch
   (fun (u : Time) (r : RM) ⇒ r = x ∧ pertinent (add_sch t' x l) t u)
   (add_sch t' x l).

intros; apply exists_add_head_sch; split; trivial.
apply pertinent_last; trivial.
constructor; auto with time.
apply forall_incl_sch with (2 := H0); auto with time.
Qed.

Lemma ACRA_forall_add :
 ∀ (l : schedule) (t t' : Time) (r x : RM),
 (t' +/ tau3 <=/ t → (r ≤ x)%Z) →
 forall_sch (fun (v : Time) (rv : RM) ⇒ pertinent l t v → (rv ≤ x)%Z) l →
 forall_sch
   (fun (v : Time) (rv : RM) ⇒ pertinent (add_sch t' r l) t v → (rv ≤ x)%Z)
   (add_sch t' r l).
constructor.
intros (prop1, prop2); auto.
apply forall_incl_sch with (2 := H0); intros.
apply H1; apply pertinent_add_simpl with t' r; trivial.
Qed.

Lemma ACRA_inf_tau3 :
 ∀ (l : schedule) (t : Time) (x : RM),
 ACRA l t x →
 ∀ (t' : Time) (r : RM), t </ t' +/ tau3 → ACRA (add_sch t' r l) t x.
intros l t x (prop1, prop2) t' r Hle.
split.
apply ACRA_forall_add; trivial.
intro; absurd (t </ t' +/ tau3); auto with time.

apply exists_add_tail_sch.
apply exists_incl_sch with (2 := prop2).
intros t0 r0 (prop3, (prop4, prop5)); auto with eve abr time.
Qed.

Lemma ACRA_sup_tau2 :
 ∀ (l : schedule) (t t' : Time) (r : RM),
 t' +/ tau2 <=/ t → Tlt_sch l t' → ACRA (add_sch t' r l) t r.

intros l t t' r Hlt flt.
cut (∀ v : Time, pertinent (add_sch t' r l) t v → t' <=/ v).
intro.
split.
constructor; auto with zarith.
apply forall_incl_sch with (2 := flt).
intros t0 r0 H1 H2; absurd (t0 </ t'); auto with time.
apply ACRA_exists_last; auto with abr time.
intros v (prop1, prop2).
inversion_clear prop2.
case H; intro; trivial.
absurd (t' +/ tau2 <=/ t); auto with time.
Qed.

Lemma ACRA_add_sup :
 ∀ (l : schedule) (t t' : Time) (r : RM),
 t' +/ tau3 <=/ t →
 Tlt_sch l t' →
 ∀ x : RM, ACRA l t x → (x ≤ r)%Z → ACRA (add_sch t' r l) t r.

intros l t t' r Hlt flt x (fall, exi) infxr.
split.
apply ACRA_forall_add; auto with zarith.
apply forall_incl_sch with (2 := fall).
intros; apply Zle_trans with x; auto.
apply ACRA_exists_last; auto.
Qed.

Lemma ACRA_add_inf :
 ∀ (l : schedule) (t t' : Time) (r : RM),
 t' +/ tau3 <=/ t →
 t </ t' +/ tau2 →
 Tlt_sch l t' →
 ∀ x : RM, ACRA l t x → (x ≥ r)%Z → ACRA (add_sch t' r l) t x.

intros l t t' r Hlt Hle flt x (fall, exi) infyr.

split.
apply ACRA_forall_add; auto with zarith.

apply exists_add_tail_sch.
apply exists_incl_sch with (2 := exi).
intros t0 r0 (prop1, (prop2, prop3)); auto with abr time.
Qed.

Lemma ACRA_decr :
 ∀ (t : Time) (l : schedule),
 Tle_sch l t →
 ∀ (u v : Time) (x y : RM),
 t +/ tau3 <=/ u → u <=/ v → ACRA l u x → ACRA l v y → (y ≤ x)%Z.
intros t l flt u v x y Hlt Hle (fallu, exu) (fallv, exv).
elim exists_forall_exists with (1 := exv).

intros w (rw, (p1, p2), p3).
rewrite <- p1.
apply
 (p3 (fun (v : Time) (rv : RM) ⇒ pertinent l u v → (rv ≤ x)%Z))
  with (1 := fallu).

case p2; intros; split.
apply Tle_trans with (t +/ tau3); trivial.
apply Tle_compatibility_r.
apply p3 with (1 := flt).
apply forall_incl_sch with (2 := H0).
intros r0 r [C1| C2]; auto.
right; apply Tle_lt_trans with v; trivial.
Qed.


Inductive ACR_rel (acrt : RM) (t : Time) : schedule → RM → Prop :=
  | ACR_rel_vide : ACR_rel acrt t vide acrt
  | ACR_rel_add_le :
      ∀ (t' : Time) (r : RM) (l : schedule),
      t' <=/ t → ACR_rel acrt t (add_sch t' r l) r
  | ACR_rel_add_gt :
      ∀ (t' : Time) (r : RM) (l : schedule),
      t </ t' →
      ∀ x : RM, ACR_rel acrt t l x → ACR_rel acrt t (add_sch t' r l) x.

Hint Constructors ACR_rel: abr.

Fixpoint ACR (acrt : RM) (t : Time) (l : schedule) {struct l} : RM :=
  match l with
  | vide ⇒ acrt
  | add_sch t' r l' ⇒
      if Tle_lt_dec t' t then r else ACR acrt t l'
  end.


Lemma ACR_add_le :
 ∀ (acrt : RM) (t t' : Time) (r : RM) (l : schedule),
 t' <=/ t → ACR acrt t (add_sch t' r l) = r.
simpl in |- *; intros.
case (Tle_lt_dec t' t); trivial.
intro; absurd (t </ t'); auto with time.
Qed.

Lemma ACR_add_gt :
 ∀ (acrt : RM) (t t' : Time) (r : RM) (l : schedule),
 t </ t' → ACR acrt t (add_sch t' r l) = ACR acrt t l.
simpl in |- *; intros.
case (Tle_lt_dec t' t); trivial.
intro; absurd (t </ t'); auto with time.
Qed.

Hint Resolve ACR_add_le ACR_add_gt.

Lemma ACR_rel_ACR :
 ∀ (acrt : RM) (t : Time) (l : schedule),
 ACR_rel acrt t l (ACR acrt t l).
simple induction l; simpl in |- *; auto with abr.
intros; case (Tle_lt_dec t0 t); auto with abr.
Qed.


Definition last_val (actr : RM) (ech : schedule) : RM :=
  match ech with
  | vide ⇒ actr
  | add_sch _ ru _ ⇒ ru
  end.

Inductive decr_from (acrt : RM) (t0 : Time) : schedule → Prop :=
  | decr_from_vide : decr_from acrt t0 vide
  | decr_from_add_stop :
      ∀ (t : Time) (r : RM) (ech : schedule),
      t <=/ t0 → decr_from acrt t0 (add_sch t r ech)
  | decr_from_add_rec :
      ∀ (t : Time) (r : RM) (ech : schedule),
      (r < last_val acrt ech)%Z →
      decr_from acrt t0 ech → decr_from acrt t0 (add_sch t r ech).

Hint Constructors decr_from: abr.

Lemma decr_from_ACR_sup_last :
 ∀ (acrt : RM) (t0 u : Time),
 t0 <=/ u →
 ∀ ech : schedule,
 decr_from acrt t0 ech → (last_val acrt ech ≤ ACR acrt u ech)%Z.

simple induction 2.
simpl in |- *; auto with zarith.
intros.
rewrite ACR_add_le; auto with zarith.
apply Tle_trans with t0; auto with time.
intros.
simpl in |- *; case (Tle_lt_dec t u); auto with zarith.
Qed.

Lemma decr_from_ACR_add :
 ∀ (acrt r : RM) (t0 t u : Time),
 t0 <=/ u →
 ∀ ech : schedule,
 decr_from acrt t0 (add_sch t r ech) → (r ≤ ACR acrt u (add_sch t r ech))%Z.

intros.
pattern r at 1 in |- *; replace r with (last_val acrt (add_sch t r ech));
 auto.
apply decr_from_ACR_sup_last with t0; trivial.
Qed.

Lemma decr_from_last :
 ∀ (acrt : RM) (t0 : Time) (ech : schedule),
 Tlt_sch ech t0 → decr_from acrt t0 ech.
simple induction 1; auto with abr time.
Qed.

Lemma decr_from_inf :
 ∀ (acrt : RM) (t0 t1 : Time) (ech : schedule),
 t1 </ t0 → decr_from acrt t1 ech → decr_from acrt t0 ech.
simple induction 2; intros; auto with abr.
constructor; apply Tle_trans with t1; auto with time.
Qed.

Lemma decr_from_inv :
 ∀ (acrt : RM) (t0 t : Time) (r : RM) (ech : schedule),
 decr_from acrt t0 (add_sch t r ech) →
 sorted_sch (add_sch t r ech) → decr_from acrt t0 ech.
intros.
inversion_clear H; trivial.
inversion_clear H0.
apply decr_from_last.
red in |- *; apply forall_incl_sch with (2 := H).
intros; apply Tlt_le_trans with t; trivial.
Qed.

Lemma decr_from_ACR_decr :
 ∀ (acrt : RM) (t0 u v : Time),
 u <=/ v →
 t0 <=/ u →
 ∀ ech : schedule,
 decr_from acrt t0 ech → (ACR acrt v ech ≤ ACR acrt u ech)%Z.
simple induction 3.
simpl in |- *; auto with zarith.
intros.
rewrite ACR_add_le.
rewrite ACR_add_le; auto with zarith.
apply Tle_trans with u; auto with time.
apply Tle_trans with t0; auto with time.
apply Tle_trans with t0; auto with time.
apply Tle_trans with u; auto with time.
intros.
case (Tle_lt_dec t u); intros.
rewrite ACR_add_le; trivial.
rewrite ACR_add_le; auto with zarith.
apply Tle_trans with u; auto with time.
rewrite ACR_add_gt with (t := u); auto with Time.
case (Tle_lt_dec t v); intros.
rewrite ACR_add_le; auto with zarith.
apply Zle_trans with (last_val acrt ech0); auto with zarith.
apply decr_from_ACR_sup_last with (2 := H3); trivial.
rewrite ACR_add_gt; auto with zarith.
Qed.


Record ACR_inv (acrt : RM) (ech : schedule) (t : Time) : Prop :=
  {Acr_sorted : sorted_sch ech;
   Acr_pertinent :
    forall_sch (fun (t' : Time) (_ : RM) ⇒ t <=/ t' ∧ t' <=/ t +/ tau2) ech;
   Acr_decr : decr_from acrt (t +/ tau3) ech}.

Hint Resolve Build_ACR_inv: abr.

Lemma ACR_inv_inv :
 ∀ (acrt : RM) (t0 t : Time) (r : RM) (ech : schedule),
 ACR_inv acrt (add_sch t r ech) t0 → ACR_inv acrt ech t0.
simple destruct 1; split.
inversion Acr_sorted0; trivial.
inversion Acr_pertinent0; trivial.
apply decr_from_inv with (1 := Acr_decr0); trivial.
Qed.


Record trunc_spec (t : Time) (acrt : RM) (ech : schedule) : Set :=
  {trunc_RM : RM;
   trunc_sched : schedule;
   trunc_ACR :
    ∀ t' : Time,
    t <=/ t' → ACR acrt t' ech = ACR trunc_RM t' trunc_sched;
   trunc_prefix : prefix trunc_sched ech;
   trunc_inv : ACR_inv trunc_RM trunc_sched t;
   trunc_lt : Tlt_sch trunc_sched (t +/ tau2);
   trunc_last : last_val acrt ech = last_val trunc_RM trunc_sched}.

Lemma trunc :
 ∀ t u : Time,
 u </ t →
 ∀ (acrt : RM) (ech : schedule),
 ACR_inv acrt ech u → trunc_spec t acrt ech.
simple induction ech; clear ech.
intros; ∃ acrt vide; auto with abr eve.
intros tn rn echn recn invn.
case (Tle_lt_dec tn t); intro.
∃ rn vide; auto with abr eve.
intros; rewrite ACR_add_le; trivial.
apply Tle_trans with t; trivial.
case recn; clear recn.
apply ACR_inv_inv with (1 := invn).
case invn;
 intros P1 P2 P3 acrt' ech' prop1 prop2 (prop3, prop4, prop5) prop6 prop7.
∃ acrt' (add_sch tn rn ech'); intros.
simpl in |- *; case (Tle_lt_dec tn t'); auto.
auto with abr eve.
repeat split; auto with abr eve.

apply prefix_sorted with (2 := P1); auto with eve.
constructor; auto with time.
split; auto with time.
inversion_clear P2.
case H0; intros; apply Tle_trans with (u +/ tau2); auto with time.
inversion_clear P3.
apply decr_from_add_stop.
apply Tle_trans with (u +/ tau3); auto with time.
constructor 3; trivial.
rewrite <- prop7; auto.
constructor; auto with abr time eve.
inversion P2; intros.
case H2; intros; apply Tle_lt_trans with (u +/ tau2); auto with time.
simpl in |- *; trivial.
Qed.


Record add_sup_spec (u t : Time) (r acrt : RM) (ech : schedule) : Set :=
  {sup_sched : schedule;
   sup_inv : ACR_inv acrt sup_sched u;
   sup_lt :
    ∀ t' : Time, t' </ t → ACR acrt t' sup_sched = ACR acrt t' ech;
   sup_ge : ∀ t' : Time, t <=/ t' → ACR acrt t' sup_sched = r}.

Lemma add_sup :
 ∀ (t : Time) (r acrt : RM) (ech : schedule),
 ACR_inv acrt ech t → add_sup_spec t (t +/ tau3) r acrt ech.

simple induction ech; clear ech.
case (Z_eq_dec acrt r); intro.
∃ vide; auto with abr eve.
∃ (add_sch (t +/ tau3) r vide); auto with abr eve time.
split; auto with abr eve time.
intros t0 r0 ech prop inv.
set (inv_ech := ACR_inv_inv inv) in ×.
case prop; clear prop; trivial.
intros ech' prop1 prop2 prop3.
case (Tle_lt_dec (t +/ tau3) t0); intro.
∃ ech'; auto with abr; intros.
rewrite ACR_add_gt; auto.
apply Tlt_le_trans with (t +/ tau3); auto with time.
case (Z_eq_dec r0 r); intro.
∃ (add_sch t0 r0 ech); auto with abr eve time; intros.
rewrite ACR_add_le; trivial.
apply Tle_trans with (t +/ tau3); auto with time.
∃ (add_sch (t +/ tau3) r (add_sch t0 r0 ech)); auto with abr; intros.
case inv; intros inv1 inv2 inv3; split; auto with abr eve time.
Qed.


Record add_inf_spec (t u : Time) (r acrt : RM) (ech : schedule) : Set :=
  {inf_sched : schedule;
   inf_inv : ACR_inv acrt inf_sched t;
   inf_lt_tau3 :
    ∀ t' : Time,
    t' </ t +/ tau3 → ACR acrt t' inf_sched = ACR acrt t' ech;
   inf_lt_tau2_inf :
    ∀ t' : Time,
    t' </ u →
    (r ≤ ACR acrt t' ech)%Z → ACR acrt t' inf_sched = ACR acrt t' ech;
   inf_lt_tau2_sup :
    ∀ t' : Time,
    t +/ tau3 <=/ t' →
    t' </ u → (r > ACR acrt t' ech)%Z → ACR acrt t' inf_sched = r;
   inf_ge_tau2 : ∀ t' : Time, u <=/ t' → ACR acrt t' inf_sched = r}.

Lemma add_inf :
 ∀ (t : Time) (r acrt : RM) (ech : schedule),
 ACR_inv acrt ech t →
 (r < ACR acrt (t +/ tau3) ech)%Z →
 ∀ u : Time,
 t +/ tau3 </ u →
 u <=/ t +/ tau2 → Tlt_sch ech u → add_inf_spec t u r acrt ech.

simple induction ech; clear ech.
case (Z_eq_dec acrt r); intro.
∃ vide; auto with abr eve.
intros; ∃ (add_sch u r vide); auto with abr eve time.
intros; rewrite ACR_add_gt; auto with abr time.
apply Tlt_trans with (t +/ tau3); trivial.
intros; rewrite ACR_add_gt; auto with abr time.
intros; simpl in H0; absurd (r > acrt)%Z; auto with zarith.

intros t0 r0 ech prop inv inf u ltu1 ltu2 tlt.
case inv; intros inv1 inv2 inv3.

case (Tle_lt_dec t0 (t +/ tau3)); intro.
rewrite ACR_add_le in inf; auto.
intros; ∃ (add_sch u r (add_sch t0 r0 ech)); auto with abr eve time.
intros; rewrite ACR_add_gt; auto with abr time.
apply Tlt_trans with (t +/ tau3); trivial.
intros; rewrite (ACR_add_gt acrt (t:=t') (t':=u)); auto with abr time.
rewrite ACR_add_le in H1.
absurd (r < r0)%Z; omega.
apply Tle_trans with (t +/ tau3); auto.
case (Z_le_gt_dec r r0); intro infsup.
case (Z_le_lt_eq_dec r r0); auto; clear infsup; intro infeq.
intros; ∃ (add_sch u r (add_sch t0 r0 ech)); auto with abr eve time.
intros; rewrite ACR_add_gt; auto with time abr.
apply Tlt_trans with (t +/ tau3); trivial.
intros; absurd (r < r0)%Z; trivial.
cut (r0 ≤ ACR acrt t' (add_sch t0 r0 ech))%Z; auto with abr.
omega.
apply decr_from_ACR_add with (t +/ tau3); auto with zarith abr.
intros; ∃ (add_sch t0 r0 ech); auto with abr eve time.
intros; absurd (r = r0); trivial.
cut (r0 ≤ ACR acrt t' (add_sch t0 r0 ech))%Z; auto with abr.
omega.
apply decr_from_ACR_add with (t +/ tau3); auto with zarith abr.
intros; rewrite infeq; auto with abr.
rewrite ACR_add_le; auto with abr time.
apply Tle_trans with u; auto.
inversion tlt; auto with time.
set (inv_ech := ACR_inv_inv inv) in ×.
rewrite ACR_add_gt in inf; trivial.
case prop with t0; auto with abr time; clear prop.
inversion inv2; intros.
case H1; auto.
inversion inv1; auto.
intros ech' prop1 prop2 prop3 prop4 prop5.
∃ ech'; auto with abr time; intros.
rewrite ACR_add_gt; auto with abr.
apply Tlt_trans with (t +/ tau3); trivial.
case (Tle_lt_dec t0 t'); intro infeq.
rewrite ACR_add_le in H0; trivial.
absurd (r > r0)%Z; omega.
rewrite ACR_add_gt; trivial.
rewrite ACR_add_gt in H0; auto with abr.
case (Tle_lt_dec t0 t'); auto with abr time; intro infeq.
rewrite ACR_add_gt in H1; auto with abr.
apply prop5.
apply Tle_trans with u; auto.
inversion tlt; auto with time.
Qed.



Record ACR_res (t : Time) (l : schedule) : Set :=
  {Acrt : RM;
   Ech : schedule;
   Acra_corr :
    ∀ t' : Time,
    t <=/ t' → first_time t l +/ tau3 </ t' → ACRA l t' (ACR Acrt t' Ech);
   Acr_preserved : ACR_inv Acrt Ech t}.

Lemma ACRI : ∀ (t : Time) (l : schedule), events t l → ACR_res t l.

simple induction 1; clear H l t.
intros; ∃ r vide; simpl in |- *; auto 10 with abr eve time zarith.
intros tk t rk Tlt_t_tk l eve (acrt, ech, prop1, prop2).
case (trunc Tlt_t_tk (acrt:=acrt) (ech:=ech)); trivial.
intros acrt' ech' prop1' prop2' prop3' prop4' prop5'.
case prop3'; intros inv1 inv2 inv3.
case (Z_le_gt_dec (ACR acrt' (tk +/ tau3) ech') rk); intro.
case (add_sup (t:=tk) rk (acrt:=acrt') (ech:=ech')); trivial.
intros ech'' prop1'' prop2'' prop3''.
∃ acrt' ech''; trivial.
intros.
set (Tlt_t_t' := Tlt_le_trans _ _ _ Tlt_t_tk H) in ×.
set (falltlt := forall_eve_Tlt Tlt_t_tk eve) in ×.

cut (first_time t l +/ tau3 </ t').
intro ft.
case (Tle_lt_dec (tk +/ tau3) t'); intro.
rewrite prop3''; trivial.
apply ACRA_add_sup with (ACR acrt' t' ech'); trivial.
rewrite <- prop1'; trivial.
apply prop1; auto with time.
apply Zle_trans with (ACR acrt' (tk +/ tau3) ech'); trivial.
apply decr_from_ACR_decr with (3 := inv3); auto with time.
rewrite prop2''; trivial.
rewrite <- (prop1' t'); trivial.
apply ACRA_inf_tau3; auto.
apply prop1; auto with time.
rewrite <- first_time_eve_add with t l tk tk rk; trivial.
case add_inf with tk rk acrt' ech' (tk +/ tau2); auto with time abr.
omega.
intros ech'' prop1'' prop2'' prop3'' prop4'' prop5''.
∃ acrt' ech''; intros; auto with abr time.
set (Tlt_t_t' := Tlt_le_trans _ _ _ Tlt_t_tk H) in ×.
set (falltlt := forall_eve_Tlt Tlt_t_tk eve) in ×.
cut (first_time t l +/ tau3 </ t').
intro ft.
case (Tle_lt_dec (tk +/ tau2) t'); intro.
rewrite prop5''; trivial.
apply ACRA_sup_tau2; auto with abr.
case (Tle_lt_dec (tk +/ tau3) t'); intro.
case (Z_le_gt_dec rk (ACR acrt' t' ech')); intro.
rewrite prop3''; trivial.
apply ACRA_add_inf; auto with abr time.
rewrite <- prop1'; auto with abr time.
omega.
rewrite prop4''; trivial.
apply ACRA_add_sup with (ACR acrt' t' ech'); auto with abr time.
rewrite <- prop1'; auto with abr time.
omega.
rewrite prop2''; trivial.
apply ACRA_inf_tau3; auto with abr time.
rewrite <- prop1'; auto with abr time.
rewrite <- first_time_eve_add with t l tk tk rk; trivial.

Qed.