Set Implicit Arguments.

Require Export Streams.
Require Export Bool.


Require Export EqD.


Lemma leb_refl :
  forall (b: bool), leb b b.
Proof.
  intros b; case b; simpl; auto.
Qed.

Lemma leb_false_2 :
  forall (b: bool), leb b false -> b = false.
Proof.
  intros b; elim b; simpl; auto.
Qed.

Lemma leb_true_2 :
  forall (b: bool), leb b true.
Proof.
  intros b; elim b; simpl; auto.
Qed.

Lemma leb_antisym :
  forall (b1 b2: bool), leb b1 b2 -> leb b2 b1 ->b1 = b2.
Proof.
  intros b1 b2; case b1; case b2; simpl; auto.
Qed.

Hint Resolve leb_refl leb_antisym leb_true_2: sampled_str.

Lemma leb_trans :
  forall (b1 b2 b3: bool), leb b1 b2 -> leb b2 b3 -> leb b1 b3.
Proof.
  intros b1 b2 b3; case b1; case b2; case b3; simpl; auto.
Qed.

Lemma EqSt_inv :
  forall (A: Set) (s1 s2: Stream A),
  EqSt s1 s2 -> hd s1 = hd s2 /\ EqSt (tl s1) (tl s2).
Proof.
  intros A s1 s2 H; case H; auto.
Qed.

Lemma unfold_Str :
  forall (A: Set) (x: Stream A), x = Cons (hd x) (tl x).
Proof.
  intros A x; case x; simpl; auto.
Qed.

Scheme and_indd:= Induction for and Sort Prop.

Section Fun_power.

Variable A: Set.

Variable f: A->A.

Fixpoint funPower (n: nat) : A -> A := fun (x: A) =>
  match n with
    | O => x
    | (S m) => (funPower m (f x))
  end.

Lemma funPower_commut :
  forall (n: nat) (x: A), f (funPower n x) = funPower (S n) x.
Proof.
 intros n; elim n; simpl; auto.
Qed.

End Fun_power.

Hint Resolve EqSt_reflex sym_EqSt: sampled_str.




Inductive samplElt (A: Set) : bool -> Set :=
  | None: samplElt A false
  | Any: A -> samplElt A true
  | Fail: samplElt A true .

Definition clock := Stream bool.

CoInductive samplStr (A: Set) : clock -> Set :=
  | sp_cons: forall (c: clock),
    samplElt A (hd c) -> samplStr A (tl c) -> samplStr A c.

Variable A: Set.

Section Sampled_streams_def.

Variable A: Set.
Definition samplElt_true_invS :
  forall (P: (samplElt A true) -> Set),
  (forall (a: A), P (Any a)) -> P (Fail A) ->
  forall (x: samplElt A true), P x :=
  fun P P_any P_fail x =>
    match x as y in samplElt _ b
       return (if b return (samplElt A b) -> Set
                     then P
                     else (fun _ => unit)) y with
      | Any a => P_any a
      | Fail _ => P_fail
      | _ => tt
  end.

Definition samplElt_false_invS :
  forall (P: samplElt A false -> Set),
  P (None A) -> forall (x: samplElt A false), (P x) :=
  fun P P_none x =>
  match x as y in samplElt _ b
    return (if b return (samplElt A b) -> Set
      then (fun _ => unit)
      else P) y with
    | None _ => P_none
    | _ => tt
  end.

Lemma samplElt_true_inv :
  forall (P: samplElt A true -> Prop),
    (forall (a: A), P (Any a)) -> P (Fail A)
    -> forall (x: samplElt A true), P x.
Proof.
  intros P H1 H2 x;
  change ((fun (b: bool) => if b return (samplElt A b) -> Prop
                                          then (fun x => P x)
                                          else (fun _ => True)) true x);
  case x; simpl; auto.
Qed.

Lemma samplElt_false_inv :
  forall (P: samplElt A false -> Prop),
    P (None A) -> forall (x: samplElt A false), P x.
Proof.
  intros P H x;
  change ((fun (b: bool) => if b return samplElt A b -> Prop
                                         then (fun _ => True)
                                         else (fun x => P x)) false x);
  case x; simpl; auto.
Qed.


Definition sp_hd := fun (c: clock) (x: samplStr A c) =>
  match x as _ in samplStr _ c0 return (samplElt A (hd c0)) with
    | sp_cons _ a _ => a
  end.

Definition sp_tl :=
  fun (c: clock) (x: samplStr A c) =>
  match x as _ in samplStr _ c return samplStr A (tl c) with
    | sp_cons _ _ s => s
  end.

Lemma unfold_samplStr :
  forall (c:clock) (s: samplStr A c),
    s = sp_cons c (sp_hd s) (sp_tl s).
Proof.
  intros c x; case x; simpl; auto.
Qed.


CoInductive sp_eq :
  forall (c1 c2: clock), samplStr A c1 -> samplStr A c2 -> Prop :=
  | sp_eq_proof :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
    ((sp_hd s1) ==<< samplElt A >>(sp_hd s2)) ->
    sp_eq (sp_tl s1) (sp_tl s2) -> sp_eq s1 s2.

Lemma sp_eq_refl :
  forall (c: clock) (s: samplStr A c), sp_eq s s.
Proof.
  cofix sp_eq_refl; intros c s; constructor; auto.
Qed.

Lemma sp_eq_inv :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
  sp_eq s1 s2 ->
  ((sp_hd s1) ==<< samplElt A >> (sp_hd s2)) /\
  sp_eq (sp_tl s1) (sp_tl s2).
Proof.
  intros c1 c2 s1 s2 H1; case H1; auto.
Qed.

Lemma sp_eq_sym :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
  sp_eq s1 s2 -> sp_eq s2 s1.
Proof.
  cofix sp_eq_sym; intros c1 c2 s1 s2 H1;
   case (sp_eq_inv H1); constructor; auto.
Qed.

Lemma sp_eq_trans :
  forall (c1 c2 c3: clock) (s1: samplStr A c1)
     (s2: samplStr A c2) (s3: samplStr A c3),
  sp_eq s1 s2 -> sp_eq s2 s3 -> sp_eq s1 s3.
Proof.
  cofix sp_eq_trans;
  intros c1 c2 c3 s1 s2 s3 H1 H2;
  case (sp_eq_inv H1);
  case (sp_eq_inv H2);
  constructor;
  [apply eq_dep_trans with (y := sp_hd s2); auto
  |apply sp_eq_trans with (s2 := sp_tl s2); auto].
Qed.

Lemma sp_eq_EqSt_clock :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
  sp_eq s1 s2 -> EqSt c1 c2.
Proof.
  cofix sp_eq_EqSt_clock;
  intros c1 c2 s1 s2 H;
  case (sp_eq_inv H);
  constructor;
  [apply eq_dep_eq_param with (P := samplElt A) (x := sp_hd s1)
                                                (y := sp_hd s2);
  auto
  |eauto].
Qed.


CoFixpoint clock_coerce :
  forall (c1 c2: clock), EqSt c1 c2 ->
  samplStr A c1 -> samplStr A c2 := fun c1 c2 H s =>
  match EqSt_inv H with
    | conj H1 H2 =>
         sp_cons c2
           (eq_rec _ (samplElt A) (sp_hd s) _ H1)
           (clock_coerce H2 (sp_tl s))
  end.

Theorem sp_eq_clock_coerce :
  forall (c1 c2: clock) (H: EqSt c1 c2) (s: samplStr A c1),
     sp_eq s (clock_coerce H s).
Proof.
  cofix sp_eq_clock_coerce; intros c1 c2 H s; constructor; simpl;
  pattern (EqSt_inv H); apply and_indd; auto.
  intros H1 H2.
  apply (eq_indd (fun (c: bool) (h: hd c1 = c) => (sp_hd s ==<< samplElt A >> eq_rec (hd c1) (samplElt A) (sp_hd s) c h))).
  auto.
Qed.

End Sampled_streams_def.


Hint Resolve sp_eq_refl sp_eq_sym: sampled_str.

CoInductive clock_inf : clock -> clock -> Prop :=
  | clock_inf_proof :
   forall (c1 c2: clock),
     leb (hd c1) (hd c2) ->
       clock_inf (tl c1) (tl c2) -> clock_inf c1 c2.

Hint Resolve clock_inf_proof : sampled_str.

Lemma clock_inf_inv :
  forall (c1 c2: clock), clock_inf c1 c2 ->
  leb (hd c1) (hd c2) /\ clock_inf (tl c1) (tl c2).
Proof.
  intros c1 c2 H; case H; auto.
Qed.

Lemma clock_inf_refl :
  forall (c1 c2: clock), EqSt c1 c2 -> clock_inf c1 c2.
Proof.
  cofix clock_inf_refl; intros c1 c2 H; case (EqSt_inv H);
  constructor;
  [rewrite H0; auto with sampled_str
  |auto].
Qed.

Hint Resolve clock_inf_refl : sampled_str.

Lemma clock_inf_antisym :
  forall (c1 c2:clock), clock_inf c1 c2 -> clock_inf c2 c1 ->
  EqSt c1 c2.
Proof.
  cofix clock_inf_antisym; intros c1 c2 H1 H2; case (clock_inf_inv H1); case (clock_inf_inv H2);
  constructor; simpl; auto with sampled_str.
Qed.

Hint Resolve clock_inf_antisym : sampled_str.

Lemma clock_inf_trans :
  forall (c1 c2 c3: clock), clock_inf c1 c2 -> clock_inf c2 c3 ->
  clock_inf c1 c3.
Proof.
  cofix clock_inf_trans; intros c1 c2 c3 H1 H2; case (clock_inf_inv H1);
  case (clock_inf_inv H2); constructor;
  [apply leb_trans with (b2 := hd c2); auto
  |apply clock_inf_trans with (c2 := tl c2); auto].
Qed.

Section Sampled_streams_props.

Variable A: Set.


Fixpoint clock_nth_tl (n: nat) : clock -> clock :=
  fun (c: clock) => match n with
    | O => c
    | S m => tl (clock_nth_tl m c)
  end.

Definition clock_nth : nat -> clock -> bool :=
  fun (n: nat) (s: clock) => hd (clock_nth_tl n s).

Lemma clock_tl_nth_tl :
  forall (n: nat) (c: clock),
  tl (clock_nth_tl n c) = clock_nth_tl n (tl c).
Proof.
  fix clock_tl_nth_tl 1; intros n; case n;
  [simpl; auto
  |simpl; intros m c'; rewrite <- clock_tl_nth_tl; auto].
Qed.

Fixpoint sp_nth_tl (n: nat) :
  forall (c: clock), samplStr A c -> samplStr A (clock_nth_tl n c) :=
    fun (c: clock) (s: samplStr A c) =>
    match n as m return samplStr A (clock_nth_tl m c) with
         | O => s
         | S m => sp_tl (sp_nth_tl m s)
     end.

Definition sp_nth :
  forall (n: nat) (c: clock), samplStr A c ->
      samplElt A (clock_nth n c) :=
  fun n c s => sp_hd (sp_nth_tl n s).

Lemma sp_tl_nth_tl :
  forall (n: nat) (c: clock) (s: samplStr A c),
   (sp_tl (sp_nth_tl n s))
         ==<<samplStr A>> (sp_nth_tl n (sp_tl s)).
Proof.
  induction n; simpl; auto with eqD.
Qed.

Hint Resolve sp_tl_nth_tl : sampled_str.

Lemma sp_nth_tl_plus :
  forall (n m: nat) (c: clock) (s: samplStr A c),
  (sp_nth_tl n (sp_nth_tl m s))
      ==<<samplStr A>>(sp_nth_tl (plus n m) s).
Proof.
  induction n; simpl; intros; auto with eqD sampled_str.
Qed.

Lemma sp_nth_plus :
  forall (n m: nat) (c: clock) (s: samplStr A c),
  (sp_nth n (sp_nth_tl m s))
        ==<<samplElt A>> (sp_nth (plus n m) s).
Proof.
  intros n m c s;
  unfold sp_nth;
  apply eq_dep_ind_l with (x := sp_nth_tl n (sp_nth_tl m s))
   (F := samplStr A) (y := sp_nth_tl (n + m) s)
   (b := clock_nth_tl (n+m) c) (U := clock)
   (a := clock_nth_tl n (clock_nth_tl m c))
   (P := fun (d: clock) (z: samplStr A d) => sp_hd (sp_nth_tl n (sp_nth_tl m s)) ==<< samplElt A >> sp_hd z);
  [constructor
  |apply sp_nth_tl_plus].
Qed.

Hint Resolve sp_nth_plus : sampled_str.

Lemma sp_eq_sp_nth :
  forall (n: nat) (c1 c2: clock) (s1: samplStr A c1)
      (s2: samplStr A c2),
  sp_eq s1 s2 -> (sp_nth n s1 ==<< samplElt A >> sp_nth n s2).
Proof.
  unfold sp_nth; induction n; simpl.
  intros c1 c2 s1 s2 H; case (sp_eq_inv H); auto.
  intros c1 c2 s1 s2 H; case (sp_eq_inv H); intros H1 H2.
  apply eq_dep_ind_l with (x := sp_nth_tl n (sp_tl s1))
 (y := sp_tl (sp_nth_tl n s1)) (F := samplStr A) (U := clock)
 (P := fun (d: clock) (z: samplStr A d) => (sp_hd z ==<< samplElt A >> sp_hd (sp_tl (sp_nth_tl n s2))));
  auto with sampled_str eqD.
  apply eq_dep_ind_l with (x := sp_nth_tl n (sp_tl s2))
 (y := sp_tl (sp_nth_tl n s2)) (F := samplStr A) (U := clock)
 (P := fun (d: clock) (z: samplStr A d) => (sp_hd (sp_nth_tl n (sp_tl s1)) ==<< samplElt A >> sp_hd z));
  auto with sampled_str eqD.
  apply (IHn (tl c1) (tl c2) (sp_tl s1) (sp_tl s2) H2).
Qed.

Lemma sp_nth_sp_eq :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
  (forall (n: nat), (sp_nth n s1)==<< samplElt A >>(sp_nth n s2))
    -> sp_eq s1 s2.
Proof.
 unfold sp_nth;
 cofix sp_nth_sp_eq;
 intros c1 c2 s1 s2 H;
 constructor.
 apply (H O).
 apply sp_nth_sp_eq; intros n.
 apply eq_dep_ind_l with (x := sp_tl (sp_nth_tl n s1))
  (y := sp_nth_tl n (sp_tl s1)) (F := samplStr A) (U := clock)
  (P := fun (d: clock) (z: samplStr A d) => sp_hd z ==<< samplElt A >>
 sp_hd (sp_nth_tl n (sp_tl s2))); auto with sampled_str eqD.
 apply eq_dep_ind_l with (x := sp_tl (sp_nth_tl n s2))
  (y := sp_nth_tl n (sp_tl s2)) (F := samplStr A) (U := clock)
  (P := fun (d: clock) (z: samplStr A d) => sp_hd (sp_tl (sp_nth_tl n s1)) ==<< samplElt A >>
 sp_hd z); auto with sampled_str eqD.
  apply (H (S n)).
Qed.

Hint Resolve sp_eq_sp_nth sp_nth_sp_eq : sampled_str.



Definition is_no_Fail (b: bool) (s: samplElt A b) : Prop :=
  match s with
    | Fail _ => False
    | _ => True
  end.

CoInductive sp_wf : forall (c: clock), (samplStr A c) -> Prop :=
  sp_wf_proof : forall (c: clock) (s: samplStr A c),
    is_no_Fail (sp_hd s) -> sp_wf (sp_tl s) -> sp_wf s.

Lemma sp_wf_inv :
  forall (c: clock) (s: samplStr A c), sp_wf s ->
   is_no_Fail (sp_hd s) /\ sp_wf (sp_tl s).
Proof.
  intros c s H; case H; auto.
Qed.


Require Export Arith.


CoInductive loc_nfstwf : forall (n: nat) (c: clock), samplStr A c -> Prop :=
 | loc_nfstwf_O :
    forall (c: clock) (s: samplStr A c), loc_nfstwf O s
 | loc_nfstwf_false :
    forall (n: nat) (c: clock) (s: samplStr A c),
      hd c = false -> loc_nfstwf n (sp_tl s) -> loc_nfstwf n s
 | loc_nfstwf_true :
    forall (n: nat) (c: clock) (s: samplStr A c),
      hd c = true ->
         is_no_Fail (sp_hd s) ->
         loc_nfstwf n (sp_tl s) -> loc_nfstwf (S n) s.

Hint Resolve loc_nfstwf_O loc_nfstwf_false loc_nfstwf_true : sampled_str.

Lemma loc_nfstwf_S_n_inv :
  forall (P: Prop) (n: nat) (c: clock) (s: samplStr A c),
  loc_nfstwf (S n) s ->
   (hd c = false -> loc_nfstwf (S n) (sp_tl s) -> P) ->
   (hd c = true -> is_no_Fail (sp_hd s) ->
                             loc_nfstwf n (sp_tl s) -> P) -> P.
Proof.
  intros P n c s H.
  change (
  (fun (m: nat) => match m return Prop with
    | O => True
    | S n => (hd c = false -> loc_nfstwf (S n) (sp_tl s) -> P) ->
      (hd c = true -> is_no_Fail (sp_hd s) ->
             loc_nfstwf n (sp_tl s) -> P) -> P
    end) (S n)
  ).
  case H; simpl; auto.
  intros n0; case n0; simpl; auto.
Qed.

Lemma loc_nfstwf_is_no_Fail :
  forall (n: nat) (c: clock) (s: samplStr A c),
    loc_nfstwf (S n) s -> is_no_Fail (sp_hd s).
Proof.
  intros n c s H; apply loc_nfstwf_S_n_inv with (n := n) (s := s); auto.
  intros H1 H2; generalize s.
  rewrite (unfold_Str c); rewrite H1.
  intros s'; pattern (sp_hd s'); apply samplElt_false_inv; simpl; auto.
Qed.

Lemma loc_nfstwf_false_inv :
  forall (n: nat) (c: clock) (s: samplStr A c),
   hd c = false ->
     loc_nfstwf n s -> loc_nfstwf n (sp_tl s).
Proof.
  intros n; case n; auto with sampled_str.
  intros m c s H1 H2; apply loc_nfstwf_S_n_inv with (n := m) (s := s); auto.
  intros H3; rewrite H1 in H3; discriminate H3.
Qed.

Lemma loc_nfstwf_S_n_true_inv :
  forall (n: nat) (c: clock) (s: samplStr A c),
   hd c = true ->
     loc_nfstwf (S n) s -> loc_nfstwf n (sp_tl s).
Proof.
  intros n c s H1 H2; apply loc_nfstwf_S_n_inv with (n := n) (s := s); auto.
  intros H3; rewrite H1 in H3; discriminate H3.
Qed.

Hint Resolve loc_nfstwf_false_inv loc_nfstwf_S_n_true_inv : sampled_str.

Lemma loc_nfstwf_true_inv :
  forall (n: nat) (c: clock) (s: samplStr A c),
   hd c = true ->
     loc_nfstwf n s -> loc_nfstwf (pred n) (sp_tl s).
Proof.
  intros n c s H1; case n; simpl; auto with sampled_str.
Qed.

Hint Resolve loc_nfstwf_true_inv : sampled_str.

Lemma eq_false_dec :
  forall (b: bool), {b = false} + {b = true}.
Proof.
  intros b; case b; simpl; auto.
Qed.

Definition pseudo_S :=
  fun (n: nat) (b: bool) => if b then (S n) else n.

Definition pseudo_pred :=
  fun (n: nat) (b: bool) => if b then (pred n) else n.

Lemma pseudo_pred_S :
  forall (n: nat) (b: bool), n = pseudo_pred (pseudo_S n b) b.
Proof.
  intros n b; case b; simpl; auto.
Qed.

Lemma pseudo_S_pred :
  forall (n: nat) (b: bool), S n = pseudo_S (pseudo_pred (S n) b) b.
Proof.
  intros n b; case b; simpl; auto.
Qed.

Lemma pseudo_pred_S_eq :
  forall (n: nat) (b: bool),
    pseudo_pred (S n) b = pseudo_S n (negb b).
Proof.
  intros n b; case b; simpl; auto.
Qed.

Lemma pseudo_S_O_discr :
  forall (n: nat) (b: bool), O = pseudo_S n b -> n=O /\ b=false.
Proof.
  intros n b; case b; simpl; auto.
  intros H; discriminate H.
Qed.

Lemma pseudo_S_le :
  forall (b: bool) (n1 n2: nat), le n1 n2 -> le n1 (pseudo_S n2 b).
Proof.
  intros b; case b; simpl; auto with arith.
Qed.

Lemma pseudo_pred_le :
  forall (b: bool) (n1 n2: nat), le n1 n2 ->
     le n1 (pseudo_pred (S n2) b).
Proof.
  intros; rewrite pseudo_pred_S_eq; apply pseudo_S_le; auto.
Qed.

Hint Resolve pseudo_pred_le pseudo_S_le : sp_aux.

Lemma loc_nfstwf_inv :
  forall (n: nat) (c: clock) (s: samplStr A c),
    loc_nfstwf n s -> loc_nfstwf (pseudo_pred n (hd c)) (sp_tl s).
Proof.
  intros n c s H; case (eq_false_dec (hd c)); intro H1; rewrite H1; simpl; auto with sampled_str.
Qed.

Lemma loc_nfstwf_S_n_n :
  forall (n: nat) (c: clock) (s: samplStr A c),
    loc_nfstwf (S n) s -> loc_nfstwf n s.
Proof.
  cofix loc_nfstwf_S_n_n; intros n; case n.
  intros; apply loc_nfstwf_O.
  intros n0 c s H; case (eq_false_dec (hd c)).
    intros H1; apply loc_nfstwf_false; auto with sampled_str.
    intros H1; apply loc_nfstwf_true; auto with sampled_str.
    eapply loc_nfstwf_is_no_Fail; eauto.
Qed.

Hint Resolve loc_nfstwf_S_n_n : sampled_str.

Lemma loc_nfstwf_n_le :
  forall (n m: nat) (c: clock) (s: samplStr A c),
   loc_nfstwf n s -> le m n -> loc_nfstwf m s.
Proof.
  intros n m c s H1 H; generalize c s H1; elim H; simpl; auto with sampled_str.
Qed.

Lemma loc_nfstwf_S_n_n_tl :
  forall (n: nat) (c: clock) (s: samplStr A c),
    loc_nfstwf (S n) s -> loc_nfstwf n (sp_tl s).
Proof.
  intros n c s H; case (eq_false_dec (hd c)); auto with sampled_str.
Qed.

Hint Resolve loc_nfstwf_S_n_n_tl : sampled_str.

Lemma loc_nfstwf_sp_eq :
  forall (n: nat) (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
   sp_eq s1 s2 -> loc_nfstwf n s1 -> loc_nfstwf n s2.
Proof.
  cofix loc_nfstwf_sp_eq.
  intros n c1 c2 s1 s2 H1 H2; case (eq_false_dec (hd c2)).
    intros H3; apply loc_nfstwf_false; auto.
     apply loc_nfstwf_sp_eq with (s1 := sp_tl s1).
     case H1; auto.
     apply loc_nfstwf_false_inv; auto.
     rewrite <- H3; case (EqSt_inv (sp_eq_EqSt_clock H1)); auto.
   intros H3; generalize H2; case n.
     intros; apply loc_nfstwf_O.
     intros n' H2'; apply loc_nfstwf_true; auto.
  apply eq_dep_ind_l with (x := sp_hd s1) (y := sp_hd s2)
   (F := samplElt A)
   (P := fun b (z: samplElt A b) => is_no_Fail z).
        apply loc_nfstwf_is_no_Fail with (n := n'); auto.
        case H1; auto.
     apply loc_nfstwf_sp_eq with (s1 := sp_tl s1).
     case H1; auto.
     apply loc_nfstwf_S_n_true_inv; auto.
     rewrite <- H3; case (EqSt_inv (sp_eq_EqSt_clock H1)); auto.
Qed.

Lemma loc_nfstwf_nth :
  forall (n: nat) (c: clock) (s: samplStr A c),
   loc_nfstwf (S n) s -> is_no_Fail (sp_nth n s).
Proof.
   intros n; elim n.
   intros; apply loc_nfstwf_is_no_Fail with (n := O) (s := s); auto.
   unfold sp_nth; intros m HR c s; intros H1.
   apply eq_dep_ind_l with (x := sp_nth_tl m (sp_tl s))
     (y := sp_tl (sp_nth_tl m s))
     (P := fun b (z: samplStr A b) => is_no_Fail (sp_hd z)).
   apply (HR (tl c) (sp_tl s)); auto with sampled_str.
   apply eq_dep_sym, sp_tl_nth_tl.
Qed.

Hint Resolve loc_nfstwf_nth : sampled_str.

Lemma loc_nfstwf_lt_is_no_Fail :
  forall (n: nat) (c: clock) (s: samplStr A c),
  loc_nfstwf n s -> forall (m: nat), lt m n ->
     is_no_Fail (sp_nth m s).
Proof.
 unfold lt; intros n; elim n.
  intros c s H1 m H2; inversion H2.
  intros n' HR c s H1 m H2; inversion H2; auto with sampled_str.
Qed.

Lemma loc_nfstwf_sp_wf :
  forall (c: clock) (s: samplStr A c),
         (forall (n: nat), loc_nfstwf n s) -> sp_wf s.
Proof.
  cofix loc_nfstwf_sp_wf.
  intros c s H; constructor 1.
   apply loc_nfstwf_is_no_Fail with (n := S O); auto.
   apply loc_nfstwf_sp_wf; auto with sampled_str.
Qed.

Lemma sp_wf_loc_nfstwf :
  forall (c: clock) (s: samplStr A c), sp_wf s ->
      forall (n: nat), loc_nfstwf n s.
Proof.
  cofix sp_wf_loc_nfstwf.
  intros c s H n; case (sp_wf_inv H); case (eq_false_dec (hd c)); intros.
    apply loc_nfstwf_false; auto.
    case n.
      apply loc_nfstwf_O.
      intros; apply loc_nfstwf_true; auto.
Qed.

Hint Resolve sp_wf_loc_nfstwf loc_nfstwf_sp_wf : sampled_str.


Fixpoint glob2loc (n: nat) : clock -> nat :=
  fun (c: clock) => match n with
     | O => O
     | S m => pseudo_S (glob2loc m (tl c)) (hd c)
  end.

Lemma glob2loc_clock_nth :
  forall (n: nat) (c: clock),
   glob2loc (S n) c = pseudo_S (glob2loc n c) (clock_nth n c).
Proof.
  intros n; elim n.
    simpl; auto.
    unfold clock_nth; intros m HR c.
    simpl; rewrite (clock_tl_nth_tl m c);
    case (hd c); simpl.
    cut ((S (glob2loc (S m) (tl c)))
      =(S (pseudo_S (glob2loc m (tl c))
                    (hd (clock_nth_tl m (tl c)))))); auto.
    case (hd (clock_nth_tl m (tl c))); simpl; auto.
    apply HR with (c := tl c).
Qed.

Lemma glob2loc_S_le :
  forall (n: nat) (c: clock),
   le (glob2loc (S n) c) (S (glob2loc n c)).
Proof.
  intros n c; rewrite glob2loc_clock_nth;
  case (clock_nth n c); simpl; auto.
Qed.

Lemma glob2loc_le :
  forall (n: nat) (c: clock),
   le (glob2loc n c) n.
Proof.
  intros n; elim n; simpl; auto.
  intros m HR c; case (hd c); simpl; auto with arith.
Qed.

Hint Resolve glob2loc_le : sampled_str.

Lemma glob2loc_preserves_le :
  forall (n m: nat), le n m ->
      forall (c: clock), le (glob2loc n c) (glob2loc m c).
Proof.
  intros n; elim n; simpl; auto with arith.
  intros n0 HR m H1 c; inversion H1; simpl; auto.
  case (hd c); simpl; auto with arith.
Qed.

Lemma loc_nfstwf_lt_is_no_Fail_strong :
  forall (n: nat) (c: clock) (s: samplStr A c),
   loc_nfstwf (glob2loc n c) s ->
      forall (m: nat), lt m n -> is_no_Fail (sp_nth m s).
Proof.
  intros n; elim n.
  simpl; intros c s H1 m H2; inversion_clear H2.
  intros n0 HR c s H1 m H2; inversion_clear H2.
    generalize HR H1; case n0; unfold sp_nth; simpl.
    generalize s; clear HR H1 s; rewrite (unfold_Str c); case (hd c).
     simpl; intros; apply loc_nfstwf_is_no_Fail with (n := O) (s := s); auto.
     simpl; intros; pattern (sp_hd s); apply samplElt_false_inv; simpl; auto.
    clear HR H1; intros n1 HR H1; simpl.
    apply eq_dep_ind_l with (x := sp_nth_tl n1 (sp_tl s))
       (y := sp_tl (sp_nth_tl n1 s))
       (P := fun b (z: samplStr A b) => is_no_Fail (sp_hd z));
       auto with sampled_str eqD.
    apply HR with (m := n1) (s := sp_tl s); auto.
    case (eq_false_dec (hd c)); intros H2; rewrite H2 in H1; simpl in H1;
    auto with sampled_str.
   apply HR; auto.
   rewrite glob2loc_clock_nth in H1; case (eq_false_dec (clock_nth n0 c)); intros H2;
   rewrite H2 in H1; auto with sampled_str.
Qed.

CoInductive locle : nat -> nat -> clock -> clock -> Prop :=
  | locle_O : forall (n: nat) (c1 c2: clock), locle O n c1 c2
  | locle_S : forall (n1 m1 n2 m2: nat) (c1 c2: clock),
     le m1 (pseudo_S n1 (hd c1)) ->
      m2 = pseudo_S n2 (hd c2) ->
        le n1 n2 ->
          Bool.leb (hd c1) (hd c2) ->
            locle n1 n2 (tl c1) (tl c2) -> locle m1 m2 c1 c2.

Lemma locle_le :
  forall (n1 n2: nat) (c1 c2: clock),
   locle n1 n2 c1 c2 -> le n1 n2.
Proof.
  intros n1 n2 c1 c2 H; case H; auto with arith.
  intros n1' m1 n2' m2 c1' c2' H1 H2 H3 H4 H5;
  rewrite H2; generalize H1 H4; case (hd c1'); simpl.
    intros H6 H7; rewrite H7; simpl; apply le_trans with (m := S n1'); auto with arith.
    intros; apply le_trans with (m := n2').
      eapply le_trans; eauto.
      case (hd c2'); simpl; auto.
Qed.

Hint Resolve locle_le : sp_aux.

Lemma locle_S_false_false :
  forall (n1 n2: nat) (c1 c2: clock),
   hd c1 = false ->
     hd c2 = false ->
        locle n1 n2 (tl c1) (tl c2) -> locle n1 n2 c1 c2.
Proof.
  intros n1 n2 c1 c2 H1 H2 H3; apply locle_S with (n1 := n1) (n2 := n2); auto;
  try (rewrite H1); try (rewrite H2); simpl; auto.
  eapply locle_le; eauto.
Qed.

Lemma locle_S_false_true :
  forall (n1 n2: nat) (c1 c2: clock),
    hd c1 = false ->
     hd c2 = true ->
         locle n1 n2 (tl c1) (tl c2) -> locle n1 (S n2) c1 c2.
Proof.
  intros n1 n2 c1 c2 H1 H2 H3; apply locle_S with (n1 := n1) (n2 := n2); auto;
  try (rewrite H1); try (rewrite H2); simpl; auto.
  eapply locle_le; eauto.
Qed.

Lemma locle_S_true_true :
  forall (n1 n2: nat) (c1 c2: clock),
   hd c1 = true ->
     hd c2 = true ->
        locle n1 n2 (tl c1) (tl c2) -> locle (S n1) (S n2) c1 c2.
Proof.
  intros n1 n2 c1 c2 H1 H2 H3; apply locle_S with (n1 := n1) (n2 := n2); auto;
  try (rewrite H1); try (rewrite H2); simpl; auto.
  eapply locle_le; eauto.
Qed.

Hint Resolve locle_O locle_S_false_false locle_S_false_true locle_S_true_true : sp_aux.

Lemma locle_le_1:
  forall (n1 m1 n2: nat) (c1 c2: clock),
    locle n1 n2 c1 c2 -> le m1 n1 -> locle m1 n2 c1 c2.
Proof.
  intros n1 m1 n2 c1 c2 H; case H; clear H n1 n2 c1 c2.
   intros n c1 c2 H; inversion H; auto with sp_aux.
   intros; eapply locle_S; eauto.
   eapply le_trans; eauto.
Qed.

Lemma locle_le_2 :
  forall (n1 n2 m2: nat) (c1 c2: clock),
     locle n1 n2 c1 c2 -> le n2 m2 -> locle n1 m2 c1 c2.
Proof.
  cofix locle_le_2.
  intros n1 n2 m2 c1 c2 H; case H; clear H n1 n2 c1 c2.
   intros; auto with sp_aux.
   intros n1 m1 n2 m3 c1 c2 H1 H2 H3 H4 H5 H6; case H6.
     intros; eapply locle_S; eauto.
     intros m2' H7; apply locle_S with (n1 := n1) (n2 := pseudo_pred (S m2') (hd c2)) ; auto.
     rewrite <- pseudo_S_pred; auto.
     apply le_trans with (m := m3).
       rewrite H2; auto with sp_aux.
       auto with sp_aux.
     apply locle_le_2 with (n1 := n1) (n2 := n2); auto.
     generalize H7; rewrite H2; case (hd c2); simpl; auto with arith.
Qed.

Lemma locle_glob2loc_le :
  forall (n m: nat) (c: clock), le n (glob2loc m c) -> locle n m c (const true).
Proof.
  cofix locle_glob2loc_le.
  intros n m c; case n; simpl.
  intros; apply locle_O.
  intros n0; case m; simpl.
    intro H; inversion H.
    intros m0 H.
      apply locle_S with (n1 := pseudo_pred (S n0) (hd c))
       (n2 := m0); simpl; auto.
      rewrite <- pseudo_S_pred; auto.
      generalize H; case (hd c); simpl;
      intros; apply le_trans with (m := glob2loc m0 (tl c));
      auto with sampled_str arith.
      intros; case (hd c); simpl; auto.
      apply locle_glob2loc_le; generalize H; case (hd c); simpl;
      auto with sampled_str arith.
Qed.

Lemma glob2loc_le_locle :
  forall (m n: nat) (c: clock),
    locle n m c (const true) -> le n (glob2loc m c).
Proof.
  intros m; elim m.
  intros n c H; generalize (locle_le H); intro H'; inversion H'; auto with arith.
  intros m0 HR n c H; inversion_clear H; auto with arith.
  simpl; apply le_trans with (m := pseudo_S n1 (hd c)); auto.
  simpl in H1; injection H1; intro H5; rewrite <- H5 in H4.
  case (hd c); simpl; auto with arith.
Qed.

Lemma glob2loc_clock_inf :
  forall (n: nat) (c1 c2: clock),
     clock_inf c1 c2 -> le (glob2loc n c1) (glob2loc n c2).
Proof.
  intros n; elim n; simpl; auto.
  intros m HR c1 c2 H; inversion_clear H.
  generalize H0; case (hd c2); simpl; case (hd c1); simpl; auto with arith.
  intro H; discriminate H.
Qed.

Lemma locle_clock_inf :
  forall (n: nat) (c1 c2: clock),
     clock_inf c1 c2 -> locle (glob2loc n c1) (glob2loc n c2) c1 c2.
Proof.
  cofix locle_clock_inf; intros n; case n; simpl.
  intros; apply locle_O.
  intros n0 c1 c2 H;
    apply locle_S with (n1 := glob2loc n0 (tl c1))
      (n2 := glob2loc n0 (tl c2)); inversion_clear H; auto.
  apply glob2loc_clock_inf; auto.
Qed.

Lemma locle_trans :
  forall (n1 n2 n3: nat) (c1 c2 c3: clock),
    locle n1 n2 c1 c2 -> locle n2 n3 c2 c3 -> locle n1 n3 c1 c3.
Proof.
  cofix locle_trans.
  intros n1; case n1.
   intros; apply locle_O.
   intros n1' n2 n3 c1 c2 c3 H1 H2; generalize H1; case H2.
     intros n2' c2' c3' H; generalize (locle_le H); intro H'; inversion H'.
     intros n2' m2' n3' m3' c2' c3' h1 h2 h3 h4 h5 h6;
     apply locle_S with (n1 := pseudo_pred (S n1') (hd c1))
       (n2 := n3'); auto.
       rewrite <- pseudo_S_pred; auto.
       inversion_clear h6; rewrite H0 in h1.
        apply le_trans with (m := n2'); auto.
        apply le_trans with (m := n4); auto.
        apply le_trans with (m := n0); auto.
        generalize H; case (hd c1); auto with arith.
        generalize h1; case (hd c2'); auto with arith.
       inversion_clear h6; eapply leb_trans; eauto.
       apply locle_trans with (n2 := n2') (c2 := tl c2'); auto.
        inversion_clear h6.
        apply locle_le_1 with (n1 := n0).
        apply locle_le_2 with (n2 := n4); auto.
        generalize h1; rewrite H0; case (hd c2'); simpl; auto with arith.
        generalize H; case (hd c1); auto with arith.
Qed.

Lemma locle_glob2loc_trans :
  forall (n1 n2 m: nat) (c1 c2: clock),
     locle n1 n2 c1 c2 -> le n2 (glob2loc m c2) -> le n1 (glob2loc m c1).
Proof.
  intros n1 n2 m c1 c2 H1 H2; apply glob2loc_le_locle;
  apply locle_trans with (n2 := n2) (c2 := c2); auto.
  apply locle_glob2loc_le; auto.
Qed.

Require Import Lia.

Lemma locle_S_S :
  forall (n1 n2: nat) (c1 c2: clock),
      locle (S n1) (S n2) c1 c2 -> locle n1 n2 c1 c2.
Proof.
  cofix locle_S_S; intros n1 n2 c1 c2; case n1.
  intros; apply locle_O.
  intros n1'; case n2.
   intros H1; generalize (locle_le H1); intros H2; inversion H2. inversion H0.
   intros n2' H1.
   apply locle_S with (n1 := pseudo_pred (S n1') (hd c1))
    (n2 := pseudo_pred (S n2') (hd c2)).
    rewrite <- pseudo_S_pred; auto.
    rewrite <- pseudo_S_pred; auto.
    inversion_clear H1; generalize H H3; case (hd c1); simpl.
    intros H5 H6; rewrite H6 in H0; simpl in H0; rewrite H6; simpl; lia.
    intros H5 H6; generalize H0; case (hd c2); simpl; intros; lia.
    inversion_clear H1; auto.
   apply locle_S_S; inversion_clear H1; generalize H H3; case (hd c1); simpl.
    intros H5 H6; rewrite H6 in H0; rewrite H6; simpl; simpl in H0; injection H0;
     clear H0; intro H0; rewrite H0; apply locle_le_1 with (n1 := n0); auto with arith.
    intros H5 H6; generalize H0; case (hd c2); simpl; intros H7.
     injection H7; clear H7; intro H7; rewrite H7; eapply locle_le_1; eauto.
     rewrite H7; eapply locle_le_1; eauto.
Qed.


Definition flat_ord (b1 b2: bool) (x: samplElt A b1) (y: samplElt A b2) :=
  match x with
   | Fail _ => True
   | _ => x ==<< samplElt A >> y
  end.

Lemma flat_ord_inv_leb :
  forall (b1 b2: bool) (x: samplElt A b1) (y: samplElt A b2),
    flat_ord x y -> Bool.leb b2 b1.
Proof.
  intros b1 b2 x y; case x; simpl; auto with sampled_str.
  intros; rewrite <- eq_dep_eq_param with (P := samplElt A)
              (x := None A) (y := y); simpl; auto.
Qed.


Lemma flat_ord_is_no_Fail :
  forall (b1 b2: bool) (x: samplElt A b1) (y: samplElt A b2),
    flat_ord x y -> is_no_Fail x -> is_no_Fail y.
Proof.
  intros b1 b2 x y; case x; case y; simpl; auto.
  intros H; inversion_clear H.
  intros a H; inversion_clear H.
Qed.

Lemma flat_ord_refl :
  forall (b1 b2: bool) (x: samplElt A b1) (y: samplElt A b2),
       (x ==<< samplElt A >> y) -> flat_ord x y.
Proof.
   intros b1 b2 x y H; case H; simpl; auto with sampled_str.
   case x; simpl; auto with eqD.
Qed.

Lemma flat_ord_antisym :
  forall (b1 b2: bool) (x: samplElt A b1) (y: samplElt A b2),
       flat_ord x y -> flat_ord y x -> (x ==<< samplElt A >> y).
Proof.
  intros b1 b2 x; case x; simpl; auto with eqD.
    intros y; case y; simpl; auto with eqD.
Qed.

Lemma flat_ord_trans :
  forall (b1 b2 b3: bool) (x: samplElt A b1) (y: samplElt A b2) (z: samplElt A b3),
      flat_ord x y -> flat_ord y z -> flat_ord x z.
Proof.
  intros b1 b2 b3 x; case x; simpl; auto.
  intros y z H;
  apply eq_dep_ind_l with (x := None A) (y := y)
         (P := fun (b: bool) (q: samplElt A b) => flat_ord q z -> (None A ==<< samplElt A >> z)); simpl; auto with eqD.
  intros a y z H;
  apply eq_dep_ind_l with (x := Any a) (y := y)
        (P := fun (b: bool) (q: samplElt A b) => flat_ord q z -> (Any a ==<< samplElt A >> z)); simpl; auto with eqD.
Qed.

Hint Resolve flat_ord_refl flat_ord_antisym : sampled_str.

Definition sp_inf (n: nat) (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2) :=
   forall (m: nat), le m n -> flat_ord (sp_nth m s1) (sp_nth m s2).

Lemma sp_inf_refl :
  forall (c: clock) (s: samplStr A c) (n: nat), sp_inf n s s.
Proof.
   unfold sp_inf; auto with sampled_str.
Qed.

Lemma sp_inf_trans :
  forall (c1 c2 c3: clock) (s1: samplStr A c1) (s2: samplStr A c2)
  (s3: samplStr A c3) (n: nat),
      sp_inf n s1 s2 -> sp_inf n s2 s3 -> sp_inf n s1 s3.
Proof.
   unfold sp_inf; intros c1 c2 c3 s1 s2 s3 n H1 H2 m H;
     apply flat_ord_trans with (y := sp_nth m s2); auto.
Qed.

Lemma sp_inf_proof_O :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
    flat_ord (sp_hd s1) (sp_hd s2) -> sp_inf O s1 s2.
Proof.
  unfold sp_inf; intros c1 c2 s1 s2 H m H1; inversion H1;
  unfold sp_nth; simpl; auto with sampled_str.
Qed.

Lemma sp_inf_O_inv :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
      sp_inf O s1 s2 -> flat_ord (sp_hd s1) (sp_hd s2).
Proof.
  unfold sp_inf; intros c1 c2 s1 s2 H; apply H with (m := O); auto with arith.
Qed.

Lemma sp_inf_proof_S_n :
  forall (n: nat) (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
    flat_ord (sp_hd s1) (sp_hd s2) -> sp_inf n (sp_tl s1) (sp_tl s2)
         -> sp_inf (S n) s1 s2.
Proof.
  unfold sp_inf; unfold sp_nth; intros n c1 c2 s1 s2 H HR m; case m; simpl; auto with arith.
  intros m0 H1;
   apply eq_dep_ind_l with (x := sp_nth_tl m0 (sp_tl s1))
         (y := sp_tl (sp_nth_tl m0 s1))
         (P := fun (b: clock) (z: samplStr A b) => flat_ord (sp_hd z) (sp_hd (sp_tl (sp_nth_tl m0 s2)))); auto with eqD sampled_str;
   apply eq_dep_ind_l with (x := sp_nth_tl m0 (sp_tl s2))
         (y := sp_tl (sp_nth_tl m0 s2))
         (P := fun (b: clock) (z: samplStr A b) => flat_ord (sp_hd (sp_nth_tl m0 (sp_tl s1))) (sp_hd z)); auto with eqD sampled_str.
   apply (HR m0);
   auto with arith.
Qed.

Lemma sp_inf_S_n_inv :
  forall (n: nat) (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
    sp_inf (S n) s1 s2 ->
    flat_ord (sp_hd s1) (sp_hd s2) /\ sp_inf n (sp_tl s1) (sp_tl s2).
Proof.
 unfold sp_inf; unfold sp_nth; intros n c1 c2 s1 s2 H; constructor 1.
   apply H with (m := O); auto with arith.
   intros m H'.
   apply eq_dep_ind_l with (x := sp_tl (sp_nth_tl m s1))
       (y := sp_nth_tl m (sp_tl s1))
       (P := fun (c: clock) (z: samplStr A c) => flat_ord (sp_hd z) (sp_hd (sp_nth_tl m (sp_tl s2)))); auto with arith sampled_str eqD.
   apply eq_dep_ind_l with (x := sp_tl (sp_nth_tl m s2))
       (y := sp_nth_tl m (sp_tl s2))
       (P := fun (c: clock) (z: samplStr A c) => flat_ord (sp_hd (sp_tl (sp_nth_tl m s1))) (sp_hd z)); auto with arith sampled_str eqD.
   apply H with (m := S m); auto with arith.
Qed.

Lemma sp_inf_loc_nfstwf :
  forall (n p: nat) (c1: clock) (s1: samplStr A c1),
     loc_nfstwf (glob2loc n c1) s1 -> forall (c2: clock) (s2: samplStr A c2),
     sp_inf n s1 s2 -> p= glob2loc n c2 -> loc_nfstwf p s2.
Proof.
  cofix sp_inf_loc_nfstwf.
  intros n p; case p; simpl.
  intros; apply loc_nfstwf_O.
  clear p; intro p; case n; simpl.
  intros c1 s1 H1 c2 s2 H2 H3; inversion H3.
  intros n0 c1 s1 H1 c2 s2 H2 H3; case (sp_inf_S_n_inv H2); intros H5 H6;
  generalize (flat_ord_inv_leb _ _ H5); intros H7; case (eq_false_dec (hd c2)).
  intros H4; apply loc_nfstwf_false.
    auto.
    apply sp_inf_loc_nfstwf with (n := n0) (s1 := sp_tl s1); auto.
    case (eq_false_dec (hd c1)); intro H8; rewrite H8 in H1; simpl in H1; auto with sampled_str.
    rewrite H4 in H3; auto.
  intros H4; apply loc_nfstwf_true.
     auto.
     apply flat_ord_is_no_Fail with (x := sp_hd s1); auto;
     rewrite H4 in H7; simpl in H7; rewrite H7 in H1;
     apply loc_nfstwf_is_no_Fail with (n := glob2loc n0 (tl c1)); auto.
     apply sp_inf_loc_nfstwf with (n := n0) (s1 := sp_tl s1); auto.
     rewrite H4 in H7; simpl in H7; rewrite H7 in H1; apply loc_nfstwf_S_n_true_inv; auto.
     rewrite H4 in H3; auto.
Qed.

Lemma sp_inf_loc_nfstwf_ext :
  forall (n: nat) (c1: clock) (s1: samplStr A c1),
     loc_nfstwf (S n) s1 -> forall (c2: clock) (s2: samplStr A c2),
     sp_inf n s1 s2 -> forall (m: nat), le m n ->
     (sp_nth m s1 ==<< samplElt A >> sp_nth m s2).
Proof.
  unfold sp_inf; intros n c1 s1 H1 c2 s2 H2 m H3;
    generalize (H2 m H3); lapply (loc_nfstwf_lt_is_no_Fail H1 (m := m)); auto with arith.
    generalize (clock_nth m c1) (sp_nth m s1) (clock_nth m c2) (sp_nth m s2).
    intros b x; case x; simpl; auto.
    intros b' y H; elim H.
Qed.

Lemma sp_inf_S_n :
  forall (n: nat) (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
      sp_inf (S n) s1 s2 -> sp_inf n s1 s2.
Proof.
  unfold sp_inf; unfold sp_nth; intros n c1 c2 s1 s2 H1 m H2; auto with arith.
Qed.

Lemma sp_nth_tl_inf :
  forall (n m: nat) (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
      sp_inf (plus n m) s1 s2 -> sp_inf n (sp_nth_tl m s1) (sp_nth_tl m s2).
Proof.
   unfold sp_inf; intros n m c1 c2 s1 s2 H m0 H0.
   apply eq_dep_ind_l with (x := sp_nth (plus m0 m) s1)
         (y := sp_nth m0 (sp_nth_tl m s1))
         (P := fun (b: bool) (z: samplElt A b) => flat_ord z (sp_nth m0 (sp_nth_tl m s2))); auto with arith sampled_str eqD.
   apply eq_dep_ind_l with (x := sp_nth (plus m0 m) s2)
         (y := sp_nth m0 (sp_nth_tl m s2))
         (P := fun (b: bool) (z: samplElt A b) => flat_ord (sp_nth (m0 + m) s1) z); auto with arith sampled_str eqD.
Qed.

Lemma sp_inf_le_eq_refl :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2) (n: nat),
      (forall (m: nat), le m n -> (sp_nth m s1 ==<< samplElt A >> sp_nth m s2))
      -> sp_inf n s1 s2.
Proof.
  unfold sp_inf; intros c1 c2 s1 s2 n H m H1.
  apply eq_dep_ind_l with (x := sp_nth m s1) (y :=sp_nth m s2)
       (P := fun (b: bool) (z: samplElt A b) => flat_ord (sp_nth m s1) z) ; auto with arith sampled_str eqD.
Qed.

Lemma sp_inf_sp_eq :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
       sp_eq s1 s2 -> forall (n: nat), sp_inf n s1 s2.
Proof.
  unfold sp_inf; intros; auto with sampled_str.
Qed.

Hint Resolve sp_inf_sp_eq sp_inf_proof_O sp_inf_proof_S_n sp_inf_S_n
  sp_inf_refl sp_inf_O_inv sp_inf_S_n_inv : sampled_str.

Lemma sp_inf_wf_eq :
  forall (c1 c2: clock) (s1: samplStr A c1) (s2: samplStr A c2),
      (forall (n: nat), sp_inf n s1 s2) -> sp_wf s1 -> sp_eq s1 s2.
Proof.
  intros; apply sp_nth_sp_eq; intros n; apply sp_inf_loc_nfstwf_ext with (n := n); auto with
  sampled_str arith.
Qed.

Definition elt_fail (b: bool) :=
  match b as c return (samplElt A c) with
    | true => (Fail A)
    | false => (None A)
  end.

CoFixpoint undef (c:clock) : samplStr A c :=
  sp_cons _ (elt_fail (hd c)) (undef (tl c)).

Lemma undef_min :
  forall (n: nat) (c: clock) (s: samplStr A c), sp_inf n (undef c) s.
Proof.
  intros n; elim n.
    intros c s; apply sp_inf_proof_O; simpl; case (sp_hd s); simpl; auto.
    intros m HR c s; apply sp_inf_proof_S_n; simpl; auto.
       case (sp_hd s); simpl; auto.
Qed.

Hint Resolve undef_min : sampled_str.



Fixpoint sp_app_n (c: clock) (s1: samplStr A c) (n: nat) {struct n}:
  samplStr A (clock_nth_tl n c) -> samplStr A c :=
   match n as p return samplStr A (clock_nth_tl p c) -> samplStr A c with
     | O => fun s2 => s2
     | S m => fun s2 => sp_app_n s1 _ (sp_cons _ (sp_nth m s1) s2)
   end.

Lemma sp_app_nth_tl :
  forall (n: nat) (c: clock) (s1: samplStr A c) (s2: samplStr A (clock_nth_tl n c)),
      sp_nth_tl n (sp_app_n s1 _ s2) = s2.
Proof.
  intros n; elim n; simpl; auto.
  intros m HR c' s1 s2; rewrite HR; auto.
Qed.

Lemma sp_nth_app_lt :
  forall (n m: nat) (c: clock) (s1: samplStr A c) (s2: samplStr A (clock_nth_tl m c)),
      lt n m -> sp_nth n (sp_app_n s1 _ s2) = sp_nth n s1.
Proof.
intros n m; generalize n; clear n; elim m; simpl.
  intros n c s1 s2 H; inversion H.
  unfold sp_nth; intros m' HR n c s1 s2 H; inversion_clear H.
    rewrite sp_app_nth_tl; simpl; auto.
    rewrite HR; auto with arith.
Qed.

Lemma sp_app_eq_1 :
  forall (n: nat) (c: clock) (s1 s2: samplStr A c) (s3: samplStr A (clock_nth_tl n c)),
     (forall (m: nat), lt m n -> sp_nth m s1 = sp_nth m s2) ->
     sp_app_n s1 _ s3 = sp_app_n s2 _ s3.
Proof.
  intros n; elim n; simpl; auto.
  intros m HR c s1 s2 s3 H; rewrite H; auto with arith.
Qed.

Lemma sp_app_sp_inf_1 :
  forall (n: nat) (c: clock) (s1: samplStr A c) (s2: samplStr A (clock_nth_tl (S n) c)),
    sp_inf n s1 (sp_app_n s1 _ s2).
Proof.
  unfold sp_inf; intros; rewrite sp_nth_app_lt; auto with arith sampled_str.
Qed.


Fixpoint glob_nfstwf (n: nat) : forall (c: clock), samplStr A c -> Prop :=
  fun c s => match n with
    | O => True
    | S m => is_no_Fail (sp_hd s) /\ glob_nfstwf m (sp_tl s)
  end.

Lemma glob_nfstwf_p1 :
  forall (c: clock) (s: samplStr A c), glob_nfstwf O s.
Proof.
  simpl; auto.
Qed.

Lemma glob_nfstwf_p2 :
  forall (n: nat) (c: clock) (s: samplStr A c),
    is_no_Fail (sp_hd s) -> glob_nfstwf n (sp_tl s) -> glob_nfstwf (S n) s.
Proof.
  intros n c s; simpl; auto.
Qed.

Hint Resolve glob_nfstwf_p2 : sampled_str.

Lemma glob_nfstwf_S_n_n :
  forall (n: nat) (c: clock) (s: samplStr A c),
     glob_nfstwf (S n) s -> glob_nfstwf n s.
Proof.
   intros n; elim n.
     simpl; auto.
     intros m HR c s H1; apply glob_nfstwf_p2; case H1; auto.
Qed.

Hint Resolve glob_nfstwf_S_n_n : sampled_str.

Lemma glob_nfstwf_n_le :
  forall (n m: nat) (c: clock) (s: samplStr A c),
      glob_nfstwf n s -> le m n -> glob_nfstwf m s.
Proof.
  intros n m c s H1 H; generalize c s H1; elim H; simpl; auto with sampled_str.
Qed.

Lemma sp_wf_glob_nfstwf :
  forall (c: clock) (s: samplStr A c), sp_wf s -> forall (n: nat), glob_nfstwf n s.
Proof.
  intros c s H n; generalize c s H; elim n; clear H s c.
   simpl; auto.
   intros m HR c s H; case H; auto with sampled_str.
Qed.

Lemma glob_nfstwf_sp_wf :
  forall (c: clock) (s: samplStr A c), (forall (n: nat), glob_nfstwf n s) -> sp_wf s.
Proof.
  cofix glob_nfstwf_sp_wf.
  intros c s H; constructor 1.
   case (H (S O)); simpl; auto.
   apply glob_nfstwf_sp_wf.
   intros n; case (H (S n)); auto.
Qed.


Lemma loc_nfstwf_glob_nfstwf :
  forall (n: nat) (c: clock) (s: samplStr A c),
      loc_nfstwf (glob2loc n c) s -> glob_nfstwf n s.
Proof.
  intros n; elim n; simpl; auto.
  intros m HR c; rewrite (unfold_Str c); case (hd c);
  simpl; intros s H; constructor 1; auto.
   apply loc_nfstwf_is_no_Fail with
       (n := glob2loc m (tl c))
       (s := s); auto.
    apply HR; apply loc_nfstwf_S_n_true_inv with (s := s); simpl; auto.
   pattern (sp_hd s); apply samplElt_false_inv; simpl; auto.
   apply HR; apply loc_nfstwf_false_inv with (s := s); simpl; auto.
Qed.

Lemma glob_nfstwf_loc_nfstwf :
  forall (n: nat) (c: clock) (s: samplStr A c),
     glob_nfstwf n s -> loc_nfstwf (glob2loc n c) s.
Proof.
  cut (forall (n m: nat) (c: clock) (s: samplStr A c),
  glob_nfstwf n s
   -> m = glob2loc n c
   -> loc_nfstwf m s); eauto.
  cofix glob_nfstwf_loc_nfstwf; intros n; case n; simpl.
   intros m c s H H0; rewrite H0; apply loc_nfstwf_O.
   intros n' m c s H H0; case (eq_false_dec (hd c)).
    intros H1; apply loc_nfstwf_false.
      auto.
      apply glob_nfstwf_loc_nfstwf with (n := n').
        case H; auto.
        rewrite H0; rewrite H1; simpl; auto.
    intros H1; generalize H0; case m.
     intros; apply loc_nfstwf_O.
     intros m' H'; apply loc_nfstwf_true.
       auto.
       case H; auto.
       apply glob_nfstwf_loc_nfstwf with (n := n').
        case H; auto.
        rewrite H1 in H'; simpl in H'.
        injection H'; auto.
Qed.

Hint Resolve glob2loc_S_le glob2loc_preserves_le : sampled_str.

Require Peano_dec.

Fixpoint loc2glob_x (n: nat) (c: clock) (m k: nat) {struct k} : nat :=
  match k with
    | O => m - k
    | S x =>
        match (eq_nat_dec n (glob2loc (m - (S x)) c)) with
          | (left _) => m - (S x)
          | (right _) => loc2glob_x n c m x
        end
  end.

Definition loc2glob (n: nat) (c: clock) (m: nat) := loc2glob_x n c m m.

Lemma minus_le_pred :
  forall (n m: nat), S m <= n -> S (n - (S m)) = n - m.
Proof.
  intros n; elim n; simpl; auto.
    intros m H; inversion H.
    intros n' HR m; case m; simpl.
      intros; rewrite <- minus_n_O; auto.
      auto with arith.
Qed.

Lemma loc2glob_x_prop :
  forall (c: clock) (n m k: nat), k <= m -> n <= glob2loc m c ->
      glob2loc (minus m k) c <= n -> glob2loc (loc2glob_x n c m k) c = n.
Proof.
  intros c n m k; elim k.
  simpl; rewrite <- minus_n_O; auto with arith.
  intros k' HR H1 H2 H3; simpl; case
   (eq_nat_dec n (glob2loc (minus m (S k')) c)).
   auto.
   intros H'; apply HR; auto with arith.
     inversion H3.
     case H'; auto.
     apply le_trans with (m := S (glob2loc (minus m (S k')) c));
     auto with arith.
     rewrite <- (minus_le_pred H1); auto with sampled_str.
Qed.

Lemma loc2glob_prop :
  forall (c: clock) (n m: nat), n <= glob2loc m c ->
       glob2loc (loc2glob n c m) c = n.
Proof.
  unfold loc2glob; intros; apply loc2glob_x_prop; auto;
  rewrite <- minus_n_n; auto with arith.
Qed.

Lemma loc2glob_x_inv_le :
  forall (c: clock) (n m k: nat), k <= m -> m - k <= n ->
     loc2glob_x (glob2loc n c) c m k <= n.
Proof.
  intros c n m k; elim k; simpl; auto with arith.
  intros k' HR H1 H2;
   case (eq_nat_dec (glob2loc n c)
          (glob2loc (minus m (S k')) c)); auto.
   intros H; apply HR; auto with arith.
   inversion H2.
    case H; rewrite H0; auto.
    rewrite <- (minus_le_pred H1); auto with arith.
Qed.

Lemma loc2glob_inv_le :
  forall (c: clock) (n m: nat), loc2glob (glob2loc n c) c m <= n.
Proof.
  unfold loc2glob; intros; apply loc2glob_x_inv_le.
  auto with arith.
  rewrite <- minus_n_n; auto with arith.
Qed.

Lemma loc2glob_x_le :
  forall (c: clock) (n m k: nat), k <= m -> m - k <= loc2glob_x n c m k.
Proof.
  intros c n m k; elim k; simpl; auto.
  intros k' HR H1; case (eq_nat_dec n (glob2loc (minus m (S k')) c));
  auto with arith.
  intro H; apply le_trans with (m := minus m k'); auto with arith.
  rewrite <- (minus_le_pred H1); auto with arith.
Qed.

Lemma loc2glob_x_le' :
  forall (c: clock) (n m k: nat), loc2glob_x n c m k <= m.
Proof.
  intros c n m k; elim k; simpl.
   rewrite <- minus_n_O; auto.
   intros n0 HR; case (eq_nat_dec n (glob2loc (minus m (S n0)) c)); simpl; auto.
   intros; lia.
Qed.

Lemma loc2glob_le :
  forall (c: clock) (n m: nat), loc2glob n c m <= m.
Proof.
  intros c n m; unfold loc2glob; apply loc2glob_x_le'.
Qed.

Hint Resolve loc2glob_le : sampled_str.

Lemma loc2glob_x_S_m_eq :
  forall (c: clock) (n m k: nat), k <= m -> n <= glob2loc m c ->
      glob2loc (m - k) c <= n ->
      loc2glob_x n c m k = loc2glob_x n c (S m) (S k).
Proof.
  intros c n m k; elim k; simpl.
  rewrite <- minus_n_O; simpl.
    intros H1 H2 H3; case (eq_nat_dec n (glob2loc m c)); auto.
    intros H4; case H4; auto with arith.
  intros k' HR H1 H2; generalize HR; clear HR.
  rewrite <- (minus_le_pred H1); intros HR H3.
  case (eq_nat_dec n (glob2loc (minus m (S k')) c)); auto.
  intro H4; apply HR; auto with arith.
     apply le_trans with (m := S (glob2loc (minus m (S k')) c)); auto with sampled_str.
     lia.
Qed.

Lemma loc2glob_S_m_eq :
  forall (c: clock) (n m: nat), n <= glob2loc m c ->
        loc2glob n c m = loc2glob n c (S m).
Proof.
  unfold loc2glob; intros; apply loc2glob_x_S_m_eq; auto.
  rewrite <- minus_n_n; auto with arith.
Qed.

Lemma loc2glob_x_n_S_lt :
  forall (c: clock) (n m k: nat), k <= m -> glob2loc (m - k) c <= n ->
       n < glob2loc m c -> loc2glob_x n c m k < loc2glob_x (S n) c m k.
Proof.
  intros c n m k; elim k; simpl; auto.
    rewrite <- minus_n_O; intros H1 H2 H3; case (lt_not_le n (glob2loc m c));
    auto.
  intros k' HR H1 H2 H3;
  case (eq_nat_dec (S n) (glob2loc (minus m (S k')) c)).
  intro H; rewrite <- H in H2; case (le_Sn_n n); auto.
  intro H; case (Nat.eq_dec n (glob2loc (minus m (S k')) c)).
    intros H0; apply lt_le_trans with (m := minus m k').
    rewrite <- (minus_le_pred H1); auto with arith.
    case (match glob2loc (m - S k') c as n0 return ({S n = n0} + {S n <> n0}) with
    | 0 => _
    | S n0 => _
    end).
    intro h; rewrite <- h in H; elim H; reflexivity.
    intro h; apply loc2glob_x_le; auto with arith.
    case (match glob2loc (m - S k') c as n1 return ({S n = n1} + {S n <> n1}) with
    | 0 => _
    | S m0 => _
    end).
    intro h; rewrite <- h in H; elim H; reflexivity.
    intros _ H'; apply HR; auto with arith.
   inversion H2.
     case H'; auto.
   rewrite <- (minus_le_pred H1);
   apply le_trans with (m := S (glob2loc (minus m (S k')) c));
    auto with arith sampled_str.
Qed.

Lemma loc2glob_S_lt :
  forall (c: clock) (n m: nat),
       lt n (glob2loc m c) -> lt (loc2glob n c m) (loc2glob (S n) c m).
Proof.
  unfold loc2glob; intros; apply loc2glob_x_n_S_lt; auto.
  rewrite <- minus_n_n; simpl; auto with arith.
Qed.

Lemma loc2glob_O :
  forall (c: clock) (m: nat), loc2glob O c m = O.
Proof.
  unfold loc2glob; intros c m; case m; simpl; auto with arith.
  intros m'; rewrite <- (minus_n_n m'); simpl; case (eq_nat_dec O O); auto.
Qed.

Lemma loc2glob_x_tl_true :
  forall (c: clock) (n m k: nat), hd c = true -> le k m ->
      loc2glob_x (S n) c (S m) k = S (loc2glob_x n (tl c) m k).
Proof.
  intros c n m k H2; elim k.
  simpl; rewrite <- minus_n_O; simpl; auto.
  simpl; intros k' HR H3.
   rewrite <- (minus_le_pred H3); simpl; rewrite H2; simpl.
   case (eq_nat_dec n (glob2loc (minus m (S k')) (tl c))).
   intro H5.
   case (sumbool_rec
      (fun
         _ : {n = glob2loc (m - S k') (tl c)} +
             {n <> glob2loc (m - S k') (tl c)} =>
       {S n = S (glob2loc (m - S k') (tl c))} +
       {S n <> S (glob2loc (m - S k') (tl c))})
      (fun a : n = glob2loc (m - S k') (tl c) =>
       left (S n <> S (glob2loc (m - S k') (tl c))) (f_equal S a))
      (fun b : n <> glob2loc (m - S k') (tl c) =>
       right (S n = S (glob2loc (m - S k') (tl c)))
         (not_eq_S n (glob2loc (m - S k') (tl c)) b))
      (left (n <> glob2loc (m - S k') (tl c)) H5)).
      intros _; reflexivity.
      intro h; rewrite <- H5 in h; elim h; reflexivity.
      intro H6.
      case (sumbool_rec
      (fun
         _ : {n = glob2loc (m - S k') (tl c)} +
             {n <> glob2loc (m - S k') (tl c)} =>
       {S n = S (glob2loc (m - S k') (tl c))} +
       {S n <> S (glob2loc (m - S k') (tl c))})
      (fun a : n = glob2loc (m - S k') (tl c) =>
       left (S n <> S (glob2loc (m - S k') (tl c))) (f_equal S a))
      (fun b : n <> glob2loc (m - S k') (tl c) =>
       right (S n = S (glob2loc (m - S k') (tl c)))
         (not_eq_S n (glob2loc (m - S k') (tl c)) b))
      (right (n = glob2loc (m - S k') (tl c)) H6)).
      intro h; inversion h as [h']; rewrite <- h' in H6; elim H6; reflexivity.
      intros; apply HR; auto with arith.
Qed.

Lemma loc2glob_tl_true :
  forall (c: clock) (n m: nat), hd c = true ->
     loc2glob (S n) c (S m) = S (loc2glob n (tl c) m).
Proof.
  intros c n m H1; unfold loc2glob; simpl.
  rewrite <- (minus_n_n m); simpl.
  case (eq_nat_dec (S n) (0)).
  intro H; discriminate H.
  intros; apply loc2glob_x_tl_true; auto with arith.
Qed.

End Sampled_streams_props.

Hint Resolve loc_nfstwf_O loc_nfstwf_false loc_nfstwf_true : sampled_str.

Hint Resolve sp_wf_loc_nfstwf loc_nfstwf_sp_wf : sampled_str.

Hint Resolve sp_inf_proof_O sp_inf_proof_S_n sp_inf_S_n
  sp_inf_refl sp_inf_O_inv sp_inf_sp_eq : sampled_str.

Hint Resolve loc2glob_le : sampled_str.

Hint Resolve glob2loc_S_le glob2loc_preserves_le : sampled_str.

Section nfstwf_conversion.

Hint Resolve loc_nfstwf_false_inv loc_nfstwf_S_n_n_tl : sampled_str.
Hint Resolve loc_nfstwf_glob_nfstwf glob_nfstwf_loc_nfstwf : sampled_str.

Variable A B: Set.

Lemma nfstwf_function_convert :
  forall (c: clock) (f: samplStr A c -> samplStr B c) (n: nat),
     (forall (m: nat) (s: samplStr A c),
        le m (glob2loc n c) -> loc_nfstwf m s -> loc_nfstwf m (f s))
  -> forall (m: nat) (s: samplStr A c),
      le m n -> glob_nfstwf m s -> glob_nfstwf m (f s).
Proof.
  auto with sampled_str.
Qed.

Lemma nfstwf_function_convert_inf :
  forall (c1 c2: clock) (f: samplStr A c1 -> samplStr B c2) (n: nat),
   (forall (m: nat) (s: samplStr A c1),
     le m (glob2loc n c2) ->
       (forall (k: nat), locle k m c1 c2 -> loc_nfstwf k s)
       -> loc_nfstwf m (f s))
  -> forall (m: nat) (s: samplStr A c1),
      le m n
        -> glob_nfstwf m s -> glob_nfstwf m (f s).
Proof.
  intros c1 c2 f n H m s H0 H1; apply loc_nfstwf_glob_nfstwf.
  apply H; auto with sampled_str.
  intros k H2; assert (glob2loc (loc2glob k c1 m) c1 = k).
  apply loc2glob_prop.
  apply locle_glob2loc_trans with (n2 := glob2loc m c2) (c2 := c2); auto.
  rewrite <- H3.
  apply glob_nfstwf_loc_nfstwf.
  apply glob_nfstwf_n_le with (n := m); auto with sampled_str.
Qed.

Lemma nfstwf_function_convert_sup :
  forall (c1 c2: clock) (f: samplStr A c1 -> samplStr B c2) (n: nat),
  clock_inf c2 c1 ->
   (forall (m k: nat) (s: samplStr A c1),
     le m (glob2loc n c1) ->
       loc_nfstwf m s ->
          locle k m c2 c1
       -> loc_nfstwf k (f s))
  -> forall (m: nat) (s: samplStr A c1),
      le m n
        -> glob_nfstwf m s -> glob_nfstwf m (f s).
Proof.
  intros c1 c2 f n H' H m s H0 H1; apply loc_nfstwf_glob_nfstwf.
  apply H with (m := glob2loc m c1); auto with sampled_str.
  apply locle_clock_inf; auto.
Qed.

Lemma nfstwf_function_convert_S :
  forall (c: clock) (f: samplStr A c -> samplStr B c) (n: nat),
  (forall (m: nat) (s: samplStr A c),
    le (S m) (glob2loc (S n) c) -> loc_nfstwf m s -> loc_nfstwf (S m) (f s))
  -> forall (m: nat) (s: samplStr A c),
      le m n
        -> glob_nfstwf m s -> glob_nfstwf (S m) (f s).
Proof.
  intros c f n H1 m s H2 H3.
    apply loc_nfstwf_glob_nfstwf.
    case (Peano_dec.O_or_S (glob2loc (S m) c)).
    intros H; case H; intros m_l H4; rewrite <- H4.
    apply H1.
     rewrite H4; auto with arith sampled_str.
     assert (glob2loc (loc2glob m_l c m) c = m_l).
     apply loc2glob_prop.
     apply le_S_n; rewrite H4; auto with sampled_str.
     rewrite <- H0.
     apply glob_nfstwf_loc_nfstwf; apply glob_nfstwf_n_le with (n := m);
     auto with sampled_str.
    intro H4; rewrite <- H4; simpl; auto with sampled_str.
Qed.

Lemma nfstwf_function_convert_S_recip :
  forall (c: clock) (f: samplStr A c -> samplStr B c) (n: nat),
  (forall (m: nat) (s: samplStr A c),
    lt m n -> glob_nfstwf m s -> glob_nfstwf (S m) (f s))
  -> forall (m: nat) (s: samplStr A c),
      le (S m) (glob2loc n c)
        -> loc_nfstwf m s -> loc_nfstwf (S m) (f s).
Proof.
 cut (forall (c: clock) (f: samplStr A c -> samplStr B c) (n: nat),
  (forall (m: nat) (s: samplStr A c),
    lt m n -> glob_nfstwf m s -> glob_nfstwf (S m) (f s))
  ->forall (m: nat) (s: samplStr A c) (t: samplStr B c),
    le (S m) (glob2loc n c)
        -> loc_nfstwf m s -> t = f s -> loc_nfstwf (S m) t).
  eauto.
  cofix foo; intros c f n H1 m s t Hl H2 H3; case (eq_false_dec (hd c)).
   intros H4; apply loc_nfstwf_false; auto.
    apply foo with (f := fun (x: samplStr A (tl c)) => sp_tl (f (sp_cons _ (sp_hd s) x)))
     (s := sp_tl s) (n := pred n); auto with sampled_str.
    intros m' s' Hl' H; case (H1 (S m') (sp_cons _ (sp_hd s) s')); auto.
      generalize Hl Hl'; case n; simpl; auto with arith.
       intro H'; inversion H'.
      apply glob_nfstwf_p2; simpl; auto.
       generalize (sp_hd s); rewrite H4; intros x; pattern x;
       apply samplElt_false_inv; simpl; auto.
      generalize Hl; case n; simpl.
       intro H'; inversion H'.
       rewrite H4; simpl; auto with arith.
      rewrite <- unfold_samplStr; rewrite H3; auto.
   intros H4; apply loc_nfstwf_true; auto.
     rewrite H3; case (H1 O s); simpl; auto with arith.
      generalize Hl; case n; simpl; auto with arith.
       intro H'; inversion H'.
     generalize Hl H2; case m; simpl; auto with sampled_str.
     intros m1 Hl' H2';
     apply foo with (f := fun (x: samplStr A (tl c)) => sp_tl (f (sp_cons _ (sp_hd s) x)))
       (s := sp_tl s) (n := loc2glob (S m1) (tl c) (pred n)) ; auto with sampled_str.
     intros m' s' H5 H6; case (H1 (S m') (sp_cons _ (sp_hd s) s')); auto.
     generalize Hl' H5; case n; simpl.
      intro H7; inversion H7.
      rewrite H4; simpl; intros n' h1 h2.
      apply Lt.lt_n_S; apply Lt.lt_le_trans with (m := loc2glob (S m1) (tl c) n');
       auto with sampled_str.
      apply glob_nfstwf_p2; simpl; auto.
      apply loc_nfstwf_is_no_Fail with (n := m1); auto.
      rewrite loc2glob_prop; auto.
       generalize Hl'; case n; simpl.
        intro H7; inversion H7.
        rewrite H4; simpl; auto with arith.
     rewrite <- unfold_samplStr; rewrite H3; auto.
Qed.

Theorem rec0_nfstwf_inc_loc2glob :
  forall (c: clock) (f: samplStr A c -> samplStr B c),
  (forall (n: nat) (s: samplStr A c),
    loc_nfstwf n s -> loc_nfstwf (S n) (f s))
  -> forall (n: nat) (s: samplStr A c), glob_nfstwf n s -> glob_nfstwf (S n) (f s).
Proof.
  intros c f H1 n s H2; apply nfstwf_function_convert_S with (n := n); auto.
Qed.

Theorem rec0_nfstwf_inc_glob2loc :
  forall (c: clock) (f: samplStr A c -> samplStr B c),
  (forall (n: nat) (s: samplStr A c),
    glob_nfstwf n s -> glob_nfstwf (S n) (f s))
  -> forall (n: nat) (s: samplStr A c), loc_nfstwf n s -> loc_nfstwf (S n) (f s).
Proof.
 cut (forall (c: clock) (f: samplStr A c -> samplStr B c),
  (forall (n: nat) (s: samplStr A c),
    glob_nfstwf n s -> glob_nfstwf (S n) (f s))
  -> forall (n: nat) (s: samplStr A c) (t: samplStr B c),
    loc_nfstwf n s -> t = f s -> loc_nfstwf (S n) t).
  eauto.
  cofix foo; intros c f H1 n s t H2 H3; case (eq_false_dec (hd c)).
   intros H4; apply loc_nfstwf_false; auto.
    apply foo with (f := fun (x: samplStr A (tl c)) => sp_tl (f (sp_cons _ (sp_hd s) x)))
     (s := sp_tl s); auto with sampled_str.
    intros m s' H; case (H1 (S m) (sp_cons _ (sp_hd s) s')); auto.
      apply glob_nfstwf_p2; simpl; auto.
       generalize (sp_hd s); rewrite H4; intros x; pattern x;
       apply samplElt_false_inv; simpl; auto.
       rewrite <- unfold_samplStr; rewrite H3; auto.
   intros H4; apply loc_nfstwf_true; auto.
     rewrite H3; case (H1 O s); simpl; auto.
     generalize H2; case n; simpl; auto with sampled_str.
     intros n1 H5;
     apply foo with (f := fun (x: samplStr A (tl c)) => sp_tl (f (sp_cons _ (sp_hd s) x)))
       (s := sp_tl s); auto with sampled_str.
     intros m s' H6; case (H1 (S m) (sp_cons _ (sp_hd s) s')); auto.
      apply glob_nfstwf_p2; simpl; auto.
      apply loc_nfstwf_is_no_Fail with (n := n1); auto.
     rewrite <- unfold_samplStr; rewrite H3; auto.
Qed.

End nfstwf_conversion.

Unset Implicit Arguments.