Require Export prosa.implementation.refinements.refinements.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file paramcoq.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.definitions.arrival_bound.

(** In this section, we define a generic version of arrival bound and
    prove that it is isomorphic to the standard, natural-number-based
    definition. *)
Section Definitions.

  (** Consider a generic type [T], for which all the basic arithmetical
      operations, ordering, and equality are defined. *)
  Context {T : Type}.
  Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
            !div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.
  Context `{!eq_of (seq T)}.
  Context `{!eq_of (T * seq (T * T))}.

  (** As in the natural-numbers-based definition, an arrival curve prefix
      is composed of an horizon and a list of steps. *)
  Let ArrivalCurvePrefix : Type := T * seq (T * T).

  (** A task's arrival bound is an inductive type comprised of three types of
      arrival patterns: (a) periodic, characterized by a period between consequent
      activation of a task, (b) sporadic, characterized by a minimum inter-arrival
      time, or (c) arrival-curve prefix, characterized by a finite prefix of an
      arrival curve. *)
  Inductive task_arrivals_bound_T :=
  | Periodic_T : T -> task_arrivals_bound_T
  | Sporadic_T : T -> task_arrivals_bound_T
  | ArrivalPrefix_T : T * seq (T * T) -> task_arrivals_bound_T.

  (** Further, we define the equality for two generic tasks as the equality
        of each attribute. *)
  Definition taskab_eqdef_T (tb1 tb2 : task_arrivals_bound_T) : bool :=
    match tb1, tb2 with
    | Periodic_T p1, Periodic_T p2 => (p1 == p2)%C
    | Sporadic_T s1, Sporadic_T s2 => (s1 == s2)%C
    | ArrivalPrefix_T s1, ArrivalPrefix_T s2 => (s1 == s2)%C
    | _, _ => false
    end.

  (** The first component of arrival-curve prefix [ac_prefix] is called horizon. *)
  Definition horizon_of_T (ac_prefix_vec : T * seq (T * T)) := fst ac_prefix_vec.

  (** The second component of [ac_prefix] is called steps. *)
  Definition steps_of_T (ac_prefix_vec : T * seq (T * T)) := snd ac_prefix_vec.

  (** The time steps of [ac_prefix] are the first components of the
      steps. That is, these are time instances before the horizon
      where the corresponding arrival curve makes a step. *)
  Definition time_steps_of_T (ac_prefix_vec : T * seq (T * T)) := map fst (steps_of_T ac_prefix_vec).

  (** The function [step_at] returns the last step ([duration ×
      value]) such that [duration ≤ t]. *)
  Definition step_at_T (ac_prefix_vec : T * seq (T * T)) (t : T) :=
    (last (0, 0) [ seq step <- steps_of_T ac_prefix_vec | fst step <= t ])%C.

  (** The function [value_at] returns the _value_ of the last step
      ([duration × value]) such that [duration ≤ t] *)
  Definition value_at_T (ac_prefix_vec : T * seq (T * T)) (t : T) := snd (step_at_T ac_prefix_vec t).

  (** Finally, we define a generic version of the function [extrapolated_arrival_curve]
      that performs the periodic extension of the arrival-curve prefix (and
      hence, defines an arrival curve). *)
  Definition extrapolated_arrival_curve_T (ac_prefix_vec : T * seq (T * T)) (t : T) :=
    let h := horizon_of_T ac_prefix_vec in
    (t %/ h * value_at_T ac_prefix_vec h + value_at_T ac_prefix_vec (t %% h))%C.

  (** Steps should be strictly increasing both in time steps and values. *)
  Definition ltn_steps_T (a b : T * T) := (fst a < fst b)%C && (snd a < snd b)%C.
  Definition sorted_ltn_steps_T (ac_prefix : ArrivalCurvePrefix) :=
    sorted ltn_steps_T (steps_of_T ac_prefix).

  (** We also define a predicate for non-decreasing order that is
      more convenient for proving some of the claims. *)
  Definition leq_steps_T (a b : T * T) := (fst a <= fst b)%C && (snd a <= snd b)%C.

  (** Horizon should be positive. *)
  Definition positive_horizon_T (ac_prefix : ArrivalCurvePrefix) := (0 < horizon_of_T ac_prefix)%C.

  (** Horizon should bound time steps. *)
  Definition large_horizon_T (ac_prefix : ArrivalCurvePrefix) : bool :=
    all (fun s => s <= horizon_of_T ac_prefix)%C (time_steps_of_T ac_prefix).

  (** There should be no infinite arrivals; that is, [value_at 0 = 0]. *)
  Definition no_inf_arrivals_T (ac_prefix : ArrivalCurvePrefix) :=
    (value_at_T ac_prefix 0 == 0)%C.

  (** Bursts must be specified; that is, [steps_of] should contain a
      pair [(ε, b)]. *)
  Definition specified_bursts_T (ac_prefix : ArrivalCurvePrefix) :=
    has (fun step => step == 1)%C (time_steps_of_T ac_prefix).

  (** The conjunction of the 5 afore-defined properties defines a
      valid arrival-curve prefix. *)
  Definition valid_extrapolated_arrival_curve_T (ac_prefix : ArrivalCurvePrefix) : bool :=
    positive_horizon_T ac_prefix
    && large_horizon_T ac_prefix
    && no_inf_arrivals_T ac_prefix
    && specified_bursts_T ac_prefix
    && sorted_ltn_steps_T ac_prefix.

End Definitions.

Section Translation.

  (** First, we define the function that maps a generic arrival-curve prefix to a natural-number
      one... *)
  Definition ACPrefixT_to_ACPrefix (ac_prefix_vec_T : N * seq (N * N)) : ArrivalCurvePrefix :=
    (nat_of_bin (horizon_of_T ac_prefix_vec_T), m_tb2tn (steps_of_T ac_prefix_vec_T)).

  (** ... and its function relationship. *)
  Definition RArrivalCurvePrefix := fun_hrel ACPrefixT_to_ACPrefix.

  (** Next, we define the converse function, mapping a natural-number arrival-curve prefix
      task to a generic one. *)
  Definition ACPrefix_to_ACPrefixT (ac_prefix_vec : ArrivalCurvePrefix) : (N * seq (N * N)) :=
    (bin_of_nat (horizon_of ac_prefix_vec), m_tn2tb (steps_of ac_prefix_vec)).

  (** Further, we define the function that maps a generic task arrival-bound to a natural-number
      one... *)
  Definition task_abT_to_task_ab (ab : @task_arrivals_bound_T N) : task_arrivals_bound :=
    match ab with
    | Periodic_T p => Periodic p
    | Sporadic_T m => Sporadic m
    | ArrivalPrefix_T ac_prefix_vec => ArrivalPrefix (ACPrefixT_to_ACPrefix ac_prefix_vec)
    end.

  (** ... and its function relationship. *)
  Definition Rtask_ab := fun_hrel task_abT_to_task_ab.

  (** Finally, we define the converse function, mapping a natural-number task arrival-bound
      task to a generic one. *)
  Definition task_ab_to_task_abT (ab : task_arrivals_bound) : @task_arrivals_bound_T N :=
    match ab with
    | Periodic p => Periodic_T (bin_of_nat p)
    | Sporadic m => Sporadic_T (bin_of_nat m)
    | ArrivalPrefix ac_prefix_vec => ArrivalPrefix_T (ACPrefix_to_ACPrefixT ac_prefix_vec)
    end.

End Translation.

Section Lemmas.

  (** We prove that [leq_steps_T] is transitive... *)
  Lemma leq_stepsT_is_transitive:
    transitive (@leq_steps_T N leq_N).
transitive (T:=N * N) leq_steps_T
  Proof.
transitive (T:=N * N) leq_steps_T
    move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
a, b, c: (N * N)%type
FSTab: (b.1 <= a.1)%C
SNDab: (b.2 <= a.2)%C
FSTbc: (a.1 <= c.1)%C
SNDbc: (a.2 <= c.2)%C
leq_steps_T b c
    rewrite /leq_steps_T.
a, b, c: (N * N)%type
FSTab: (b.1 <= a.1)%C
SNDab: (b.2 <= a.2)%C
FSTbc: (a.1 <= c.1)%C
SNDbc: (a.2 <= c.2)%C
(b.1 <= c.1)%C && (b.2 <= c.2)%C
    destruct a as [a1 a2], b as [b1 b2], c as [c1 c2]; simpl in *.
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 <= a1)%C
SNDab: (b2 <= a2)%C
FSTbc: (a1 <= c1)%C
SNDbc: (a2 <= c2)%C
(b1 <= c1)%C && (b2 <= c2)%C
    apply/andP; split.
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 <= a1)%C
SNDab: (b2 <= a2)%C
FSTbc: (a1 <= c1)%C
SNDbc: (a2 <= c2)%C
(b1 <= c1)%C
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 <= a1)%C
SNDab: (b2 <= a2)%C
FSTbc: (a1 <= c1)%C
SNDbc: (a2 <= c2)%C
(b2 <= c2)%C
    -
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 <= a1)%C
SNDab: (b2 <= a2)%C
FSTbc: (a1 <= c1)%C
SNDbc: (a2 <= c2)%C
(b1 <= c1)%C by apply /N.leb_spec0; eapply N.le_trans;
      [apply /N.leb_spec0; apply FSTab
      | apply /N.leb_spec0; apply FSTbc].
    -
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 <= a1)%C
SNDab: (b2 <= a2)%C
FSTbc: (a1 <= c1)%C
SNDbc: (a2 <= c2)%C
(b2 <= c2)%C by apply /N.leb_spec0; eapply N.le_trans;
      [apply /N.leb_spec0; apply SNDab
      | apply /N.leb_spec0; apply SNDbc].
  Qed.

  (** ... and so is [ltn_steps_T]. *)
  Lemma ltn_stepsT_is_transitive:
    transitive (@ltn_steps_T N lt_N).
transitive (T:=N * N) ltn_steps_T
  Proof.
transitive (T:=N * N) ltn_steps_T
    move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
a, b, c: (N * N)%type
FSTab: (b.1 < a.1)%C
SNDab: (b.2 < a.2)%C
FSTbc: (a.1 < c.1)%C
SNDbc: (a.2 < c.2)%C
ltn_steps_T b c
    rewrite /ltn_steps_T.
a, b, c: (N * N)%type
FSTab: (b.1 < a.1)%C
SNDab: (b.2 < a.2)%C
FSTbc: (a.1 < c.1)%C
SNDbc: (a.2 < c.2)%C
(b.1 < c.1)%C && (b.2 < c.2)%C
    destruct a as [a1 a2], b as [b1 b2], c as [c1 c2]; simpl in *.
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 < a1)%C
SNDab: (b2 < a2)%C
FSTbc: (a1 < c1)%C
SNDbc: (a2 < c2)%C
(b1 < c1)%C && (b2 < c2)%C
    apply/andP; split.
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 < a1)%C
SNDab: (b2 < a2)%C
FSTbc: (a1 < c1)%C
SNDbc: (a2 < c2)%C
(b1 < c1)%C
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 < a1)%C
SNDab: (b2 < a2)%C
FSTbc: (a1 < c1)%C
SNDbc: (a2 < c2)%C
(b2 < c2)%C
    -
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 < a1)%C
SNDab: (b2 < a2)%C
FSTbc: (a1 < c1)%C
SNDbc: (a2 < c2)%C
(b1 < c1)%C by apply /N.ltb_spec0; eapply N.lt_trans;
      [apply /N.ltb_spec0; apply FSTab
      | apply /N.ltb_spec0; apply FSTbc].
    -
a1, a2, b1, b2, c1, c2: N
FSTab: (b1 < a1)%C
SNDab: (b2 < a2)%C
FSTbc: (a1 < c1)%C
SNDbc: (a2 < c2)%C
(b2 < c2)%C by apply /N.ltb_spec0; eapply N.lt_trans;
      [apply /N.ltb_spec0; apply SNDab
      | apply /N.ltb_spec0; apply SNDbc].
  Qed.

End Lemmas.

(** In this fairly technical section, we prove a series of refinements
    aimed to be able to convert between a standard natural-number task
    and a generic task. *)
Section Refinements.

  (** We prove the refinement for the [leq_steps] function. *)
  Global Instance refine_leq_steps :
    refines (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel leq_steps leq_steps_T.
refines
  (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)
  leq_steps leq_steps_T
  Proof.
refines
  (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)
  leq_steps leq_steps_T
    rewrite /leq_steps /leq_steps_T refinesE => a a' Ra b b' Rb.
a: (nat * nat)%type
a': (N * N)%type
Ra: prod_R Rnat Rnat a a'
b: (nat * nat)%type
b': (N * N)%type
Rb: prod_R Rnat Rnat b b'
bool_R ((a.1 <= b.1) && (a.2 <= b.2))
  ((a'.1 <= b'.1)%C && (a'.2 <= b'.2)%C)
    by apply refinesP; refines_apply.
  Qed.

  (** Next, we prove the refinement for the [ltn_steps] function. *)
  Global Instance refine_ltn_steps :
    refines (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel ltn_steps ltn_steps_T.
refines
  (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)
  ltn_steps ltn_steps_T
  Proof.
refines
  (prod_R Rnat Rnat ==> prod_R Rnat Rnat ==> bool_R)
  ltn_steps ltn_steps_T
    rewrite /ltn_steps /ltn_steps_T refinesE => a a' Ra b b' Rb.
a: (nat * nat)%type
a': (N * N)%type
Ra: prod_R Rnat Rnat a a'
b: (nat * nat)%type
b': (N * N)%type
Rb: prod_R Rnat Rnat b b'
bool_R ((a.1 < b.1) && (a.2 < b.2))
  ((a'.1 < b'.1)%C && (a'.2 < b'.2)%C)
    destruct a as [a1 a2], a' as [a1' a2'], b as [b1 b2], b' as [b1' b2']; simpl in *.
a1, a2: nat
a1', a2': N
Ra: prod_R Rnat Rnat (a1, a2) (a1', a2')
b1, b2: nat
b1', b2': N
Rb: prod_R Rnat Rnat (b1, b2) (b1', b2')
bool_R ((a1 < b1) && (a2 < b2))
  ((a1' < b1')%C && (a2' < b2')%C)
    inversion Ra; subst.
a1, a2: nat
a1', a2': N
Ra: prod_R Rnat Rnat (a1, a2) (a1', a2')
b1, b2: nat
b1', b2': N
Rb: prod_R Rnat Rnat (b1, b2) (b1', b2')
a_R: Rnat a1 a1'
b_R: Rnat a2 a2'
bool_R ((a1 < b1) && (a2 < b2))
  ((a1' < b1')%C && (a2' < b2')%C)
    inversion Rb; subst.
a1, a2: nat
a1', a2': N
Ra: prod_R Rnat Rnat (a1, a2) (a1', a2')
b1, b2: nat
b1', b2': N
Rb: prod_R Rnat Rnat (b1, b2) (b1', b2')
a_R: Rnat a1 a1'
b_R: Rnat a2 a2'
a_R0: Rnat b1 b1'
b_R0: Rnat b2 b2'
bool_R ((a1 < b1) && (a2 < b2))
  ((a1' < b1')%C && (a2' < b2')%C)
    by apply andb_R; apply refine_ltn.
  Qed.

  (** Next, we prove the refinement for the [ACPrefixT_to_ACPrefix] function. *)
  Local Instance refine_ACPrefixT_to_ACPrefix :
    refines (unify (A:=N * seq (N * N)) ==> prod_R Rnat (list_R (prod_R Rnat Rnat)))%rel ACPrefixT_to_ACPrefix id.
refines
  (unify (A:=N * seq (N * N)) ==>
   prod_R Rnat (list_R (prod_R Rnat Rnat)))
  ACPrefixT_to_ACPrefix id
  Proof.
refines
  (unify (A:=N * seq (N * N)) ==>
   prod_R Rnat (list_R (prod_R Rnat Rnat)))
  ACPrefixT_to_ACPrefix id
    rewrite refinesE => evec evec' Revec.
evec, evec': (N * seq (N * N))%type
Revec: unify evec evec'
prod_R Rnat (list_R (prod_R Rnat Rnat))
  (ACPrefixT_to_ACPrefix evec) evec'
    unfold unify  in *; subst evec'.
evec: (N * seq (N * N))%type
prod_R Rnat (list_R (prod_R Rnat Rnat))
  (ACPrefixT_to_ACPrefix evec) evec
    destruct evec as [h st].
h: N
st: seq (N * N)
prod_R Rnat (list_R (prod_R Rnat Rnat))
  (ACPrefixT_to_ACPrefix (h, st)) (h, st)
    apply prod_R_pair_R.
h: N
st: seq (N * N)
Rnat (horizon_of_T (h, st)) h
h: N
st: seq (N * N)
list_R (prod_R Rnat Rnat)
  (m_tb2tn (steps_of_T (h, st))) st
    -
h: N
st: seq (N * N)
Rnat (horizon_of_T (h, st)) h by compute.
    -
h: N
st: seq (N * N)
list_R (prod_R Rnat Rnat)
  (m_tb2tn (steps_of_T (h, st))) st simpl; clear h; elim: st => [|a st IHst].
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::]
a: (N * N)%type
st: seq (N * N)
IHst: list_R (prod_R Rnat Rnat) (m_tb2tn st) st
list_R (prod_R Rnat Rnat) (m_tb2tn (a :: st))
  (a :: st)
      +
list_R (prod_R Rnat Rnat) (m_tb2tn [::]) [::] apply list_R_nil_R.
      +
a: (N * N)%type
st: seq (N * N)
IHst: list_R (prod_R Rnat Rnat) (m_tb2tn st) st
list_R (prod_R Rnat Rnat) (m_tb2tn (a :: st))
  (a :: st) simpl; apply list_R_cons_R; last by done.
a: (N * N)%type
st: seq (N * N)
IHst: list_R (prod_R Rnat Rnat) (m_tb2tn st) st
prod_R Rnat Rnat (tb2tn a) a
        destruct a; unfold tb2tn, tmap; simpl.
n, n0: N
st: seq (N * N)
IHst: list_R (prod_R Rnat Rnat) (m_tb2tn st) st
prod_R Rnat Rnat (n, n0) (n, n0)
        by apply refinesP; refines_apply.
  Qed.

  (** Next, we prove the refinement for the [ltn_steps_sorted] function. *)
  Global Instance refine_ltn_steps_sorted :
    forall xs xs',
      refines ( list_R (prod_R Rnat Rnat) )%rel xs xs' ->
      refines ( bool_R )%rel (sorted ltn_steps xs) (sorted ltn_steps_T xs').
forall (xs : seq (nat * nat)) (xs' : seq (N * N)),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
  Proof.
forall (xs : seq (nat * nat)) (xs' : seq (N * N)),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
    elim=> [|x xs IHxs] xs' Rxs.
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) [::] xs'
refines bool_R (sorted ltn_steps [::])
  (sorted ltn_steps_T xs')
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) xs'
refines bool_R (sorted ltn_steps (x :: xs))
  (sorted ltn_steps_T xs')
    {
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) [::] xs'
refines bool_R (sorted ltn_steps [::])
  (sorted ltn_steps_T xs') destruct xs' as [ | x' xs']; first by tc.
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) [::] (x' :: xs')
refines bool_R (sorted ltn_steps [::])
  (sorted ltn_steps_T (x' :: xs'))
      by rewrite refinesE in Rxs; inversion Rxs. }
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) xs'
refines bool_R (sorted ltn_steps (x :: xs))
  (sorted ltn_steps_T xs')
    {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) xs'
refines bool_R (sorted ltn_steps (x :: xs))
  (sorted ltn_steps_T xs') destruct xs' as [ | x' xs']; first by rewrite refinesE in Rxs; inversion Rxs.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R (sorted ltn_steps (x :: xs))
  (sorted ltn_steps_T (x' :: xs'))
      rewrite //= !path_sortedE; first last.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=nat * nat) ltn_steps
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=N * N) ltn_steps_T
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (ltn_steps x) xs && sorted ltn_steps xs)
  (all (ltn_steps_T x') xs' && sorted ltn_steps_T xs')
      {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=nat * nat) ltn_steps by apply ltn_steps_is_transitive. }
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=N * N) ltn_steps_T
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (ltn_steps x) xs && sorted ltn_steps xs)
  (all (ltn_steps_T x') xs' && sorted ltn_steps_T xs')
      {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=N * N) ltn_steps_T by apply ltn_stepsT_is_transitive. }
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (ltn_steps x) xs && sorted ltn_steps xs)
  (all (ltn_steps_T x') xs' && sorted ltn_steps_T xs')
      {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (ltn_steps x) xs && sorted ltn_steps xs)
  (all (ltn_steps_T x') xs' && sorted ltn_steps_T xs') rewrite refinesE in Rxs; inversion Rxs; subst.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
refines bool_R
  (all (ltn_steps x) xs && sorted ltn_steps xs)
  (all (ltn_steps_T x') xs' && sorted ltn_steps_T xs')
        rewrite refinesE; apply andb_R.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (all (ltn_steps x) xs)
  (all (ltn_steps_T x') xs')
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (sorted ltn_steps xs) (sorted ltn_steps_T xs')
        -
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (all (ltn_steps x) xs)
  (all (ltn_steps_T x') xs') apply refinesP; refines_apply.
        -
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted ltn_steps xs)
  (sorted ltn_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (sorted ltn_steps xs) (sorted ltn_steps_T xs') by apply refinesP; apply IHxs; rewrite refinesE. } }
  Qed.

  (** Next, we prove the refinement for the [leq_steps_sorted] function. *)
  Global Instance refine_leq_steps_sorted :
    forall xs xs',
      refines ( list_R (prod_R Rnat Rnat) )%rel xs xs' ->
      refines ( bool_R )%rel (sorted leq_steps xs) (sorted leq_steps_T xs').
forall (xs : seq (nat * nat)) (xs' : seq (N * N)),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
  Proof.
forall (xs : seq (nat * nat)) (xs' : seq (N * N)),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
    elim=> [|x xs IHxs] xs' Rxs.
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) [::] xs'
refines bool_R (sorted leq_steps [::])
  (sorted leq_steps_T xs')
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) xs'
refines bool_R (sorted leq_steps (x :: xs))
  (sorted leq_steps_T xs')
    {
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) [::] xs'
refines bool_R (sorted leq_steps [::])
  (sorted leq_steps_T xs') destruct xs' as [ | x' xs']; first by tc.
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) [::] (x' :: xs')
refines bool_R (sorted leq_steps [::])
  (sorted leq_steps_T (x' :: xs'))
      by rewrite refinesE in Rxs; inversion Rxs. }
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) xs'
refines bool_R (sorted leq_steps (x :: xs))
  (sorted leq_steps_T xs')
    {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) xs'
refines bool_R (sorted leq_steps (x :: xs))
  (sorted leq_steps_T xs') destruct xs' as [ | x' xs']; first by rewrite refinesE in Rxs; inversion Rxs.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R (sorted leq_steps (x :: xs))
  (sorted leq_steps_T (x' :: xs'))
      rewrite //= !path_sortedE; first last.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=nat * nat) leq_steps
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=N * N) leq_steps_T
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (leq_steps x) xs && sorted leq_steps xs)
  (all (leq_steps_T x') xs' && sorted leq_steps_T xs')
      {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=nat * nat) leq_steps by apply leq_steps_is_transitive. }
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=N * N) leq_steps_T
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (leq_steps x) xs && sorted leq_steps xs)
  (all (leq_steps_T x') xs' && sorted leq_steps_T xs')
      {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
transitive (T:=N * N) leq_steps_T by apply leq_stepsT_is_transitive. }
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (leq_steps x) xs && sorted leq_steps xs)
  (all (leq_steps_T x') xs' && sorted leq_steps_T xs')
      {
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: refines (list_R (prod_R Rnat Rnat)) 
  (x :: xs) (x' :: xs')
refines bool_R
  (all (leq_steps x) xs && sorted leq_steps xs)
  (all (leq_steps_T x') xs' && sorted leq_steps_T xs') rewrite refinesE in Rxs; inversion Rxs; subst.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
refines bool_R
  (all (leq_steps x) xs && sorted leq_steps xs)
  (all (leq_steps_T x') xs' && sorted leq_steps_T xs')
        rewrite refinesE; apply andb_R.
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (all (leq_steps x) xs)
  (all (leq_steps_T x') xs')
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (sorted leq_steps xs) (sorted leq_steps_T xs')
        -
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (all (leq_steps x) xs)
  (all (leq_steps_T x') xs') by apply refinesP; refines_apply.
        -
x: (nat * nat)%type
xs: seq (nat * nat)
IHxs: forall xs' : seq (N * N),
refines (list_R (prod_R Rnat Rnat)) xs xs' ->
refines bool_R (sorted leq_steps xs)
  (sorted leq_steps_T xs')
x': (N * N)%type
xs': seq (N * N)
Rxs: list_R (prod_R Rnat Rnat) (x :: xs) (x' :: xs')
a_R: prod_R Rnat Rnat x x'
l_R: list_R (prod_R Rnat Rnat) xs xs'
bool_R (sorted leq_steps xs) (sorted leq_steps_T xs') by apply refinesP; apply IHxs; rewrite refinesE. } }
  Qed.

  (** Next, we prove the refinement for the [value_at] function. *)
  Global Instance refine_value_at :
    refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> Rnat ==> Rnat)%rel value_at value_at_T.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   Rnat ==> Rnat) value_at value_at_T
  Proof.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   Rnat ==> Rnat) value_at value_at_T
    rewrite refinesE => evec evec' Revec δ δ' Rδ.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat (value_at evec δ) (value_at_T evec' δ')
    unfold value_at, value_at_T, step_at, step_at_T.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat
  (last (0, 0)
     [seq step <- steps_of evec | step.1 <= δ]).2
  (last (0%C, 0%C)
     [seq step <- steps_of_T evec' | (step.1 <= δ')%C]).2
    have RP := refines_snd_R Rnat Rnat.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
RP: refines (prod_R Rnat Rnat ==> Rnat) snd snd
Rnat
  (last (0, 0)
     [seq step <- steps_of evec | step.1 <= δ]).2
  (last (0%C, 0%C)
     [seq step <- steps_of_T evec' | (step.1 <= δ')%C]).2
    rewrite refinesE in RP.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
RP: (prod_R Rnat Rnat ==> Rnat)%rel snd snd
Rnat
  (last (0, 0)
     [seq step <- steps_of evec | step.1 <= δ]).2
  (last (0%C, 0%C)
     [seq step <- steps_of_T evec' | (step.1 <= δ')%C]).2
    eapply RP; clear RP.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
prod_R Rnat Rnat
  (last (0, 0)
     [seq step <- steps_of evec | step.1 <= δ])
  (last (0%C, 0%C)
     [seq step <- steps_of_T evec' | (step.1 <= δ')%C])
    have RL := @refine_last _ _ (prod_R Rnat Rnat).
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
RL: refines
  (prod_R Rnat Rnat ==>
   list_R (prod_R Rnat Rnat) ==> prod_R Rnat Rnat)
  last last
prod_R Rnat Rnat
  (last (0, 0)
     [seq step <- steps_of evec | step.1 <= δ])
  (last (0%C, 0%C)
     [seq step <- steps_of_T evec' | (step.1 <= δ')%C])
    rewrite refinesE in RL.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
RL: (prod_R Rnat Rnat ==>
 list_R (prod_R Rnat Rnat) ==> prod_R Rnat Rnat)%rel
  last last
prod_R Rnat Rnat
  (last (0, 0)
     [seq step <- steps_of evec | step.1 <= δ])
  (last (0%C, 0%C)
     [seq step <- steps_of_T evec' | (step.1 <= δ')%C])
    apply RL; clear RL.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
prod_R Rnat Rnat (0, 0) (0%C, 0%C)
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
list_R (prod_R Rnat Rnat)
  [seq step <- steps_of evec | step.1 <= δ]
  [seq step <- steps_of_T evec' | (step.1 <= δ')%C]
    -
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
prod_R Rnat Rnat (0, 0) (0%C, 0%C) by apply refinesP; refines_apply.
    -
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
list_R (prod_R Rnat Rnat)
  [seq step <- steps_of evec | step.1 <= δ]
  [seq step <- steps_of_T evec' | (step.1 <= δ')%C] apply filter_R.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
forall (t₁ : nat * nat) (t₂ : N * N),
prod_R Rnat Rnat t₁ t₂ ->
bool_R (t₁.1 <= δ) (t₂.1 <= δ')%C
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
list_R (prod_R Rnat Rnat) 
  (steps_of evec) (steps_of_T evec')
      +
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
forall (t₁ : nat * nat) (t₂ : N * N),
prod_R Rnat Rnat t₁ t₂ ->
bool_R (t₁.1 <= δ) (t₂.1 <= δ')%C move=> _ _ [n1 n1' Rn1 _ _ _] /=.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
n1: nat
n1': N
Rn1: Rnat n1 n1'
bool_R (n1 <= δ) (n1' <= δ')%C
        by apply: refinesP; apply: refines_apply.
      +
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
list_R (prod_R Rnat Rnat) (steps_of evec)
  (steps_of_T evec') unfold steps_of, steps_of_T.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
list_R (prod_R Rnat Rnat) evec.2 evec'.2
        by apply refinesP; refines_apply.
  Qed.

  (** Next, we prove the refinement for the [time_steps_of] function. *)
  Global Instance refine_get_time_steps :
    refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> list_R Rnat)%rel time_steps_of time_steps_of_T.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   list_R Rnat) time_steps_of time_steps_of_T
  Proof.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   list_R Rnat) time_steps_of time_steps_of_T
    rewrite refinesE => evec evec' Revec.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
list_R Rnat (time_steps_of evec)
  (time_steps_of_T evec')
    destruct evec as [h st], evec' as [h' st'].
h: nat
st: seq (nat * nat)
h': N
st': seq (N * N)
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat))
  (h, st) (h', st')
list_R Rnat (time_steps_of (h, st))
  (time_steps_of_T (h', st'))
    case: Revec => n1 n1' Rn1 n2 n2' Rn2.
h: nat
st: seq (nat * nat)
h': N
st': seq (N * N)
n1: nat
n1': N
Rn1: Rnat n1 n1'
n2: seq (nat * nat)
n2': seq (N * N)
Rn2: list_R (prod_R Rnat Rnat) n2 n2'
list_R Rnat (time_steps_of (n1, n2))
  (time_steps_of_T (n1', n2'))
    by apply: refinesP; apply: refines_apply.
  Qed.

  (** Next, we prove the refinement for the [extrapolated_arrival_curve] function. *)
  Global Instance refine_arrival_curve_prefix :
    refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> Rnat ==> Rnat)%rel extrapolated_arrival_curve extrapolated_arrival_curve_T.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   Rnat ==> Rnat) extrapolated_arrival_curve
  extrapolated_arrival_curve_T
  Proof.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   Rnat ==> Rnat) extrapolated_arrival_curve
  extrapolated_arrival_curve_T
    rewrite refinesE => evec evec' Revec δ δ' Rδ.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat (extrapolated_arrival_curve evec δ)
  (extrapolated_arrival_curve_T evec' δ')
    unfold extrapolated_arrival_curve, extrapolated_arrival_curve_T.
evec: (nat * seq (nat * nat))%type
evec': (N * seq (N * N))%type
Revec: prod_R Rnat (list_R (prod_R Rnat Rnat)) evec
  evec'
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat
  (δ %/ horizon_of evec *
   value_at evec (horizon_of evec) +
   value_at evec (δ %% horizon_of evec))
  (δ' %/ horizon_of_T evec' *
   value_at_T evec' (horizon_of_T evec') +
   value_at_T evec' (δ' %% horizon_of_T evec'))%C
    by apply refinesP; refines_apply.
  Qed.

  (** Next, we prove the refinement for the [ArrivalCurvePrefix] function. *)
  Global Instance refine_ArrivalPrefix:
    refines (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==> Rtask_ab)%rel ArrivalPrefix ArrivalPrefix_T.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   Rtask_ab) ArrivalPrefix ArrivalPrefix_T
  Proof.
refines
  (prod_R Rnat (list_R (prod_R Rnat Rnat)) ==>
   Rtask_ab) ArrivalPrefix ArrivalPrefix_T
    rewrite refinesE => arrival_curve_prefix arrival_curve_prefix' Rarrival_curve_prefix.
arrival_curve_prefix: (nat * seq (nat * nat))%type
arrival_curve_prefix': (N * seq (N * N))%type
Rarrival_curve_prefix: prod_R Rnat
  (list_R (prod_R Rnat Rnat))
  arrival_curve_prefix
  arrival_curve_prefix'
Rtask_ab (ArrivalPrefix arrival_curve_prefix)
  (ArrivalPrefix_T arrival_curve_prefix')
    destruct arrival_curve_prefix as [h steps], arrival_curve_prefix' as [h' steps'].
h: nat
steps: seq (nat * nat)
h': N
steps': seq (N * N)
Rarrival_curve_prefix: prod_R Rnat
  (list_R (prod_R Rnat Rnat))
  (h, steps) (h', steps')
Rtask_ab (ArrivalPrefix (h, steps))
  (ArrivalPrefix_T (h', steps'))
    case: Rarrival_curve_prefix => {}h {}h' Rh {}steps {}steps' Rsteps.
h: nat
h': N
Rh: Rnat h h'
steps: seq (nat * nat)
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) steps steps'
Rtask_ab (ArrivalPrefix (h, steps))
  (ArrivalPrefix_T (h', steps'))
    rewrite /Rtask_ab /fun_hrel /task_abT_to_task_ab /ACPrefixT_to_ACPrefix /=.
h: nat
h': N
Rh: Rnat h h'
steps: seq (nat * nat)
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) steps steps'
ArrivalPrefix (h', m_tb2tn steps') =
ArrivalPrefix (h, steps)
    have ->: nat_of_bin h' = h by rewrite -Rh.
h: nat
h': N
Rh: Rnat h h'
steps: seq (nat * nat)
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) steps steps'
ArrivalPrefix (h, m_tb2tn steps') =
ArrivalPrefix (h, steps)
    have ->: m_tb2tn steps' = steps; last by done.
h: nat
h': N
Rh: Rnat h h'
steps: seq (nat * nat)
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) steps steps'
m_tb2tn steps' = steps
    clear h h' Rh; elim: steps steps' Rsteps => [|a steps IHsteps] steps' Rsteps.
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) [::] steps'
m_tb2tn steps' = [::]
a: (nat * nat)%type
steps: seq (nat * nat)
IHsteps: forall steps' : seq (N * N),
list_R (prod_R Rnat Rnat) steps steps' ->
m_tb2tn steps' = steps
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) (a :: steps) steps'
m_tb2tn steps' = a :: steps
    -
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) [::] steps'
m_tb2tn steps' = [::] by destruct steps'; [done | inversion Rsteps].
    -
a: (nat * nat)%type
steps: seq (nat * nat)
IHsteps: forall steps' : seq (N * N),
list_R (prod_R Rnat Rnat) steps steps' ->
m_tb2tn steps' = steps
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) (a :: steps) steps'
m_tb2tn steps' = a :: steps destruct steps' as [|p steps']; first by inversion Rsteps.
a: (nat * nat)%type
steps: seq (nat * nat)
IHsteps: forall steps' : seq (N * N),
list_R (prod_R Rnat Rnat) steps steps' ->
m_tb2tn steps' = steps
p: (N * N)%type
steps': seq (N * N)
Rsteps: list_R (prod_R Rnat Rnat) 
  (a :: steps) (p :: steps')
m_tb2tn (p :: steps') = a :: steps
      inversion_clear Rsteps as [|? ? Rap ? ? Rstep].
a: (nat * nat)%type
steps: seq (nat * nat)
IHsteps: forall steps' : seq (N * N),
list_R (prod_R Rnat Rnat) steps steps' ->
m_tb2tn steps' = steps
p: (N * N)%type
steps': seq (N * N)
Rap: prod_R Rnat Rnat a p
Rstep: list_R (prod_R Rnat Rnat) steps steps'
m_tb2tn (p :: steps') = a :: steps
      rewrite /m_tb2tn/= /tb2tn/tmap/=.
a: (nat * nat)%type
steps: seq (nat * nat)
IHsteps: forall steps' : seq (N * N),
list_R (prod_R Rnat Rnat) steps steps' ->
m_tb2tn steps' = steps
p: (N * N)%type
steps': seq (N * N)
Rap: prod_R Rnat Rnat a p
Rstep: list_R (prod_R Rnat Rnat) steps steps'
(p.1, p.2) :: [seq (t.1, t.2) | t <- steps'] =
a :: steps
      congr cons; first by case: Rap => _ {}a <- _ b <-.
a: (nat * nat)%type
steps: seq (nat * nat)
IHsteps: forall steps' : seq (N * N),
list_R (prod_R Rnat Rnat) steps steps' ->
m_tb2tn steps' = steps
p: (N * N)%type
steps': seq (N * N)
Rap: prod_R Rnat Rnat a p
Rstep: list_R (prod_R Rnat Rnat) steps steps'
[seq (t.1, t.2) | t <- steps'] = steps
      exact: IHsteps.
  Qed.

  (** Next, we define some useful equality functions to guide the typeclass engine. *)
  Global Instance eq_listN : eq_of (seq N) := fun x y => x == y.
  Global Instance eq_NlistNN : eq_of (prod N (seq (prod N N))) := fun x y => x == y.
  Global Instance eq_taskab : eq_of (@task_arrivals_bound_T N) := taskab_eqdef_T.

  (** Finally, we prove the refinement for the [ArrivalCurvePrefix] function. *)
  Global Instance refine_task_ab_eq :
    refines (Rtask_ab ==> Rtask_ab ==> bool_R)%rel eqtype.eq_op eq_taskab.
refines (Rtask_ab ==> Rtask_ab ==> bool_R) eq_op
  eq_taskab
  Proof.
refines (Rtask_ab ==> Rtask_ab ==> bool_R) eq_op
  eq_taskab
    rewrite refinesE => tb1 tb1' Rtb1 tb2 tb2' Rtb2.
tb1: task_arrivals_bound
tb1': task_arrivals_bound_T
Rtb1: Rtask_ab tb1 tb1'
tb2: task_arrivals_bound
tb2': task_arrivals_bound_T
Rtb2: Rtask_ab tb2 tb2'
bool_R (tb1 == tb2) (eq_taskab tb1' tb2')
    destruct tb1 as [per1 | spor1 | evec1], tb1' as [per1' | spor1' | evec1'];
      destruct tb2 as [per2 | spor2 | evec2], tb2' as [per2' | spor2' | evec2'].
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
per1: nat
spor1': N
Rtb1: Rtask_ab (Periodic per1) (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
per1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Periodic per1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (Periodic per1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
spor1: nat
per1': N
Rtb1: Rtask_ab (Sporadic spor1) (Periodic_T per1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
spor1: nat
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (Sporadic spor1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (Sporadic spor1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
per1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Periodic_T per1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (Periodic_T per1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1') (Periodic_T per2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
spor1': N
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (Sporadic_T spor1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (Sporadic_T spor1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
per2: nat
spor2': N
Rtb2: Rtask_ab (Periodic per2) (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
per2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Periodic per2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == Periodic per2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
spor2: nat
per2': N
Rtb2: Rtask_ab (Sporadic spor2) (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
spor2: nat
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (Sporadic spor2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == Sporadic spor2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
per2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Periodic_T per2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Periodic_T per2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
spor2': N
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (Sporadic_T spor2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
    all: try (inversion Rtb1; fail); try (inversion Rtb2; fail); try (compute; constructor).
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
    {
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (Periodic per1 == Periodic per2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2')) replace (Periodic per1 == Periodic per2) with (per1 == per2) by constructor.
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (per1 == per2)
  (eq_taskab (Periodic_T per1') (Periodic_T per2'))
      replace (eq_taskab(Periodic_T per1')(Periodic_T per2'))%C with (per1' == per2') by constructor.
per1: nat
per1': N
Rtb1: Rtask_ab (Periodic per1) (Periodic_T per1')
per2: nat
per2': N
Rtb2: Rtask_ab (Periodic per2) (Periodic_T per2')
bool_R (per1 == per2) (per1' == per2')
      inversion Rtb1; inversion Rtb2; subst; clear.
per1', per2': N
bool_R (per1' == per2') (per1' == per2')
      by apply refinesP; refines_apply. }
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
    {
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (Sporadic spor1 == Sporadic spor2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2')) replace (Sporadic spor1 == Sporadic spor2) with (spor1 == spor2) by constructor.
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (spor1 == spor2)
  (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))
      have ->: (eq_taskab (Sporadic_T spor1') (Sporadic_T spor2'))%C = (spor1' == spor2') by constructor.
spor1: nat
spor1': N
Rtb1: Rtask_ab (Sporadic spor1) (Sporadic_T spor1')
spor2: nat
spor2': N
Rtb2: Rtask_ab (Sporadic spor2) (Sporadic_T spor2')
bool_R (spor1 == spor2) (spor1' == spor2')
      inversion Rtb1; inversion Rtb2; subst; clear.
spor1', spor2': N
bool_R (spor1' == spor2') (spor1' == spor2')
      by apply refinesP; refines_apply. }
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
    {
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (ArrivalPrefix evec1 == ArrivalPrefix evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2')) replace (ArrivalPrefix evec1 == ArrivalPrefix evec2) with (evec1 == evec2) by constructor.
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (evec1 == evec2)
  (eq_taskab (ArrivalPrefix_T evec1')
     (ArrivalPrefix_T evec2'))
      replace (eq_taskab (ArrivalPrefix_T evec1') (ArrivalPrefix_T evec2'))%C with (evec1' == evec2')%C by constructor.
evec1: ArrivalCurvePrefix
evec1': (N * seq (N * N))%type
Rtb1: Rtask_ab (ArrivalPrefix evec1)
  (ArrivalPrefix_T evec1')
evec2: ArrivalCurvePrefix
evec2': (N * seq (N * N))%type
Rtb2: Rtask_ab (ArrivalPrefix evec2)
  (ArrivalPrefix_T evec2')
bool_R (evec1 == evec2) (evec1' == evec2')%C
      inversion Rtb1; inversion Rtb2; subst; clear.
evec1', evec2': (N * seq (N * N))%type
bool_R
  (ACPrefixT_to_ACPrefix evec1' ==
   ACPrefixT_to_ACPrefix evec2') (evec1' == evec2')%C
      rename evec1' into evec1, evec2' into evec2.
evec1, evec2: (N * seq (N * N))%type
bool_R
  (ACPrefixT_to_ACPrefix evec1 ==
   ACPrefixT_to_ACPrefix evec2) (evec1 == evec2)%C
      destruct evec1 as [h1 evec1], evec2 as [h2 evec2].
h1: N
evec1: seq (N * N)
h2: N
evec2: seq (N * N)
bool_R
  (ACPrefixT_to_ACPrefix (h1, evec1) ==
   ACPrefixT_to_ACPrefix (h2, evec2))
  ((h1, evec1) == (h2, evec2))%C
      rewrite /ACPrefixT_to_ACPrefix //= !xpair_eqE.
h1: N
evec1: seq (N * N)
h2: N
evec2: seq (N * N)
bool_R
  ((h1 == h2) && (m_tb2tn evec1 == m_tb2tn evec2))
  ((h1, evec1) == (h2, evec2))%C
      have -> : ((h1, evec1) == (h2, evec2))%C = ((h1 == h2) && (evec1 == evec2))%C by constructor.
h1: N
evec1: seq (N * N)
h2: N
evec2: seq (N * N)
bool_R
  ((h1 == h2) && (m_tb2tn evec1 == m_tb2tn evec2))
  ((h1 == h2) && (evec1 == evec2))
      apply andb_R; first by apply refinesP; refines_apply.
h1: N
evec1: seq (N * N)
h2: N
evec2: seq (N * N)
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
      clear h1 h2; move: evec2; elim: evec1 => [[] //|h1 evec1 IHevec1].
h1: (N * N)%type
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
forall evec2 : seq (N * N),
bool_R (m_tb2tn (h1 :: evec1) == m_tb2tn evec2)
  (h1 :: evec1 == evec2)
      case=> [//|h2 evec2].
h1: (N * N)%type
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
h2: (N * N)%type
evec2: seq (N * N)
bool_R
  (m_tb2tn (h1 :: evec1) == m_tb2tn (h2 :: evec2))
  (h1 :: evec1 == h2 :: evec2)
      rewrite //= !eqseq_cons.
h1: (N * N)%type
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
h2: (N * N)%type
evec2: seq (N * N)
bool_R
  ((tb2tn h1 == tb2tn h2) &&
   (m_tb2tn evec1 == m_tb2tn evec2))
  ((h1 == h2) && (evec1 == evec2))
      apply andb_R; last by apply IHevec1.
h1: (N * N)%type
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
h2: (N * N)%type
evec2: seq (N * N)
bool_R (tb2tn h1 == tb2tn h2) (h1 == h2)
      move: h1 h2 => [n n0] [n1 n2].
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
evec2: seq (N * N)
n, n0, n1, n2: N
bool_R (tb2tn (n, n0) == tb2tn (n1, n2))
  ((n, n0) == (n1, n2))
      rewrite /tb2tn /tmap /=.
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
evec2: seq (N * N)
n, n0, n1, n2: N
bool_R ((n, n0) == (n1, n2)) ((n, n0) == (n1, n2))
      replace ((n, n0) == (n1, n2)) with ((n == n1) && (n0 == n2)) by constructor.
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
evec2: seq (N * N)
n, n0, n1, n2: N
bool_R ((n, n0) == (n1, n2)) ((n == n1) && (n0 == n2))
      replace ((nat_of_bin n, nat_of_bin n0) == (nat_of_bin n1, nat_of_bin n2)) with
          ((nat_of_bin n == nat_of_bin n1) && (nat_of_bin n0 == nat_of_bin n2)) by constructor.
evec1: seq (N * N)
IHevec1: forall evec2 : seq (N * N),
bool_R (m_tb2tn evec1 == m_tb2tn evec2)
  (evec1 == evec2)
evec2: seq (N * N)
n, n0, n1, n2: N
bool_R ((n == n1) && (n0 == n2))
  ((n == n1) && (n0 == n2))
      apply refinesP; refines_apply. }
  Qed.

End Refinements.