Prove one direction for fixed priority

The other direction doesn't hold since we only register completions
in network calculus derived curves.

link/static_priority.v

-From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat ssrint.
-From mathcomp Require Import choice seq path bigop ssralg ssrnum rat interval.
-From mathcomp Require Import fintype finfun.
-From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
-Require Import prosa.util.nat prosa.util.bigcat prosa.util.sum.
-Require Import prosa.model.task.concept prosa.behavior.arrival_sequence.
-Require Import prosa.model.task.arrival.request_bound_functions.
-Require Import prosa.model.priority.classes.
-Require Import prosa.analysis.definitions.completion_sequence.
-Require Export prosa.results.fixed_priority.rta.bounded_nps.
-Require Export prosa.analysis.facts.preemption.task.preemptive.
-Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
-Require Export prosa.analysis.facts.readiness.sequential.
-
-(** Throughout this file, we assume the FP priority policy, ideal uni-processor
-    schedules, and the sequential readiness model. *)
+From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
+From mathcomp.analysis Require Import reals ereal nngnum boolp.
 Require Import prosa.model.processor.ideal.
-Require Import prosa.model.readiness.sequential.
-
-(** Furthermore, we assume the fully preemptive task model. *)
-Require Import prosa.model.task.preemption.fully_preemptive.
-
+Require Import prosa.model.schedule.priority_driven.
+Require Import prosa.model.preemption.fully_preemptive.
+Require Import prosa.analysis.definitions.completion_sequence.
+Require Import prosa.analysis.facts.model.ideal_schedule.
+Require Import prosa.analysis.facts.readiness.sequential.
 From NCCoq Require Import RminStruct cumulative_curves backlog_itv.
 Require Import clock flow_cc_of_arrival_sequence rta_nc_link.fifo.
 
@@ -34,9 +20,11 @@ Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
 
 Section Static_priority.
 
+(** We assume a fully preemptive model *)
+#[local] Existing Instance fully_preemptive_job_model.
+
 (** Consider any type of tasks ... *)
 Context {Task : finType}.
-Context `{TaskCost Task}.
 
 (**  ... and any type of jobs associated with these tasks. *)
 Context {Job : JobType}.
@@ -44,42 +32,26 @@ Context {jt : JobTask Job Task}.
 Context {ja : JobArrival Job}.
 Context {jc : JobCost Job}.
 
-(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
-Variable arr_seq : arrival_sequence Job.
-Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-
-(* TODO: hypothèse peu courante ? *)
+(** We assume all job costs are positive. *)
 Hypothesis H_job_cost_positive : forall j, job_cost_positive j.
 
-(** ... and the cost of a job cannot be larger than the task cost. *)
-Hypothesis H_valid_job_cost :
-  arrivals_have_valid_job_costs arr_seq.
-
-(* (** Consider an arbitrary task set ts, ... *) *)
-(* Variable ts : list Task. *)
-
-(* (** ... assume that all jobs come from the task set, ... *) *)
-(* Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts. *)
+(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+Variable arr_seq : arrival_sequence Job.
+Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
 
-(** Recall that we assume sequential readiness. *)
-Instance sequential_readiness : JobReady Job (processor_state Job) :=
+(** We assume sequential readiness. *)
+#[local] Instance sequential_readiness : JobReady Job (processor_state Job) :=
   sequential_ready_instance arr_seq.
 
-(** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+(** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
 Variable sched : schedule (ideal.processor_state Job).
 Hypothesis H_sched_valid : valid_schedule sched arr_seq.
 
-(* Hypothesis H_jobs_come_from_arrival_sequence: *)
-(*   jobs_come_from_arrival_sequence sched arr_seq. *)
-
 (** We assume each job is given a different priority
-    (lower value means higher priority) *)
-(* TODO: mettre plutôt ça sous forme d'une relation comme dans PROSA
-   (et en déduire la fonction prior) *)
+    (lower value means higher priority). *)
 Variable prior : Task -> nat.
-Hypothesis H_prior_injective : injective prior.
-Instance FP_prior : FP_policy Task := fun t1 t2 => (prior t1 <= prior t2)%nat.
+#[local] Instance FP_prior : FP_policy Task :=
+  fun t1 t2 => (prior t1 <= prior t2)%N.
 
 Lemma priority_is_reflexive : reflexive_priorities.
 Proof.
@@ -91,77 +63,84 @@ Qed.
 Lemma priority_is_transitive : transitive_priorities.
 Proof. move=> t j1 j2 j3; exact: leq_trans. Qed.
 
-#[local] Existing Instance fully_preemptive_job_model.
-
-(** Next, we assume that the schedule is a work-conserving schedule... *)
-(* Hypothesis H_work_conserving : work_conserving arr_seq sched. *)
-
-(** ... and the schedule respects the policy defined by the [job_preemptable]
-    function (i.e., jobs have bounded non-preemptive segments). *)
-Definition respects_FP_policy :=
-  respects_FP_policy_at_preemption_point arr_seq sched FP_prior.
+Lemma in_completion_sequence_completed :
+  forall j t,
+    arrives_in arr_seq j ->
+    completed_by sched j t ->
+    j \in arrivals_up_to (completion_sequence arr_seq sched) t.
+Proof.
+move=> j t jarr jcompl.
+rewrite /completion_sequence.
+pose P (t' : 'I_t.+1) := @completed_by _ _ sched jc j t'.
+have Pt : P ord_max by [].
+have [t' Pt' Pget'] := arg_minP id Pt.
+have must_arrive : jobs_must_arrive_to_execute sched.
+{ exact: (valid_schedule_implies_jobs_must_arrive_to_execute sched arr_seq). }
+have [t'' [/andP[arrt'' t''ltt'] _]] := completed_implies_scheduled_before
+  sched j (H_job_cost_positive j) must_arrive _ Pt'.
+have t'gt0 : (0 < t')%N by case: t' t''ltt' {Pt' Pget'} => -[].
+apply: (mem_bigcat_nat _ _ _ _ _ t'); first by rewrite /= ltn_ord.
+rewrite mem_filter.
+apply/andP; split.
+{ rewrite /completes_at -/(P t') Pt' andbT; apply/negP => jcomplt'.
+  have: (t'.-1 < t')%N by rewrite prednK.
+  apply/negP; rewrite -leqNgt.
+  have Ok : (t'.-1 < t.+1)%N by rewrite prednK// ltnW// ltn_ord.
+  exact/(Pget' (Ordinal Ok))/jcomplt'. }
+apply: job_in_arrivals_between => //=.
+{ exact: consistent_times_valid_arrival. }
+exact/(leq_ltn_trans arrt'')/(ltn_trans t''ltt').
+Qed.
 
 Lemma FP_arrival_sequences_to_flow_cc (c : uclock) :
-  respects_FP_policy ->
+  respects_FP_policy_at_preemption_point arr_seq sched FP_prior ->
   let A := flow_cc_of_arrival_sequence arr_seq c in
   let D := flow_cc_of_arrival_sequence (completion_sequence arr_seq sched) c in
   (* static_priority.preemptive_SP *)
-  forall i, forall s t : {nonneg R},
+  forall i, forall s t : {nonneg R}, s%:nngnum <= t%:nngnum ->
     backlog_itv
-      (\sum_(j | (prior j < prior i)%nat) A j)%C
-      (\sum_(j | (prior j < prior i)%nat) D j)%C
+      (\sum_(j | (prior j < prior i)%N) A j)%C
+      (\sum_(j | (prior j < prior i)%N) D j)%C
       `[s, t] ->
     (D i) s = (D i) t.
 Proof.
-Abort.
-(* That's wrong, counter example:
-   take a job j_h of high priority arriving at instant 3,
-   then, (3, 6] is a backlog period for D j_h and A j_h
-   however, a low priority job j_l arrived before could perfectly complete
-   at instant 3 (last execution at instant 2) meaning D_l would be
-   t |-> 0 if t <= 3 and 1 otherwise
-   and D j_l 3 = 0 != 1 = D j_l 6 *)
-
-(*
 set compl_seq := completion_sequence arr_seq sched.
-have arr_uniq := arrivals_uniq
-                   _ H_arrival_times_are_consistent H_arr_seq_is_a_set 0%nat.
-have compl_uniq := completions_uniq
-  sched H_arrival_times_are_consistent H_arr_seq_is_a_set 0%nat.
-move=> FP_pol /= tsk s t [+ Hbacklog].
+have arr_consistent := consistent_times_valid_arrival _ H_valid_arr_seq.
+have arr_set := uniq_valid_arrival _ H_valid_arr_seq.
+have arr_uniq := arrivals_uniq _ arr_consistent arr_set 0%N.
+move=> FP_pol /= tsk s t + Hbacklog.
 rewrite le_eqVlt => /orP[/eqP/val_inj -> //|sltt].
 set ns := next_tick c s.
 set nt := next_tick c t.
 pose arrivals_of_tsk arr_seq tsk t1 t2 :=
-  [seq j <- arrivals_between arr_seq t1 t2 | H0 j == tsk].
-have {}Hbacklog : forall n, (ns < n <= nt)%nat ->
-  (\sum_(ts | (prior ts < prior tsk)%nat)
+  [seq j <- arrivals_between arr_seq t1 t2 | @job_task _ _ jt j == tsk].
+have {}Hbacklog : forall n, (ns <= n <= nt)%N ->
+  (\sum_(ts | (prior ts < prior tsk)%N)
     (\sum_(j <- arrivals_of_tsk compl_seq ts 0 n) job_cost j)
-   < \sum_(ts | (prior ts < prior tsk)%nat)
-      (\sum_(j <- arrivals_of_tsk arr_seq ts 0 n) job_cost j))%nat.
-{ move=> n /andP[nsltn nlent].
+   < \sum_(ts | (prior ts < prior tsk)%N)
+      (\sum_(j <- arrivals_of_tsk arr_seq ts 0 n) job_cost j))%N.
+{ move=> n /andP[nslen nlent].
   have: ((\sum_(j | (prior j < prior tsk)%N)
            flow_cc_of_arrival_sequence compl_seq c j)%C (c n)
          < (\sum_(j | (prior j < prior tsk)%N)
              flow_cc_of_arrival_sequence arr_seq c j)%C (c n))%E.
   { move: nlent; rewrite leq_eqVlt => /orP[/eqP ->|nltnt].
     { set fa := flow_cc_of_arrival_sequence.
-      pose su := fun s => (\sum_(j | (prior j < prior tsk)%nat) fa s c j)%C.
+      pose su := fun s => (\sum_(j | (prior j < prior tsk)%N) fa s c j)%C.
       have rew : forall s, su s (c nt) = su s t.
       { move=> seq.
         by rewrite !flow_cc_sumE; apply: eq_bigr => i _; rewrite /= uclockK. }
-      by rewrite !rew; apply: Hbacklog; rewrite sltt /=. }
+      by rewrite !rew; apply: Hbacklog; rewrite in_itv/= lexx andbT ltW. }
     apply/Hbacklog/andP; split.
-    { apply: (le_lt_trans (uclock_next_tick_gt c _)).
-      by apply: uclock_lt_next_tick; rewrite uclockK. }
+    { exact/(le_trans (uclock_next_tick_gt c _))/uclock_le. }
     exact/ltW/uclock_lt_next_tick. }
   rewrite !flow_cc_sumE /= !dsumEFin lte_fin !sumrMnr ltr_nat.
   by rewrite !uclockK. }
 apply/f_equal/f_equal.
-have nslent : (ns <= nt)%nat by exact/next_tick_leq/ltW.
+have nslent : (ns <= nt)%N by exact/next_tick_leq/ltW.
 move: ns nt nslent Hbacklog => {}s {}t + Hbacklog {sltt c}.
 rewrite leq_eqVlt => /orP[/eqP -> //|sltt].
-rewrite (arrivals_between_cat _ 0%nat s t)// 1?ltnW//.
+rewrite (arrivals_between_cat _ 0%N s t)// 1?ltnW//.
 rewrite filter_cat big_cat /=.
 set se := [seq j <- arrivals_between _ s t | _].
 suff -> : se = [::] by rewrite big_nil addn0.
@@ -169,156 +148,81 @@ apply: filter_in_pred0 => j jcomplt {se}.
 have [t' []] := mem_bigcat_exists _ _ _ _ _ jcomplt.
 rewrite mem_iota subnKC => [/andP[slet' t'ltt]|]; [|exact: ltnW].
 rewrite mem_filter => /andP[jcomplt' jarrt'].
-have [ts [priorts Hts]] : exists ts, (prior ts < prior tsk)%nat
-  /\ (\sum_(j <- arrivals_of_tsk compl_seq ts 0 t'.+1) job_cost j
-      < \sum_(j <- arrivals_of_tsk arr_seq ts 0 t'.+1) job_cost j)%N.
+apply/eqP => jtsk.
+have t'gt0 : (0 < t')%N.
+{ case: t' jcomplt' {slet' t'ltt jarrt'} => [|//].
+  by rewrite /completes_at => /andP[] /[swap] ->. }
+have [ts [priorts Hts]] : exists ts, (prior ts < prior tsk)%N
+  /\ (\sum_(j <- arrivals_of_tsk compl_seq ts 0 t') job_cost j
+      < \sum_(j <- arrivals_of_tsk arr_seq ts 0 t') job_cost j)%N.
 { rewrite not_existsP => Hall.
-  move: (Hbacklog t'.+1); rewrite ltnS slet' t'ltt /= => /(_ erefl).
+  move: (Hbacklog t'); rewrite slet'/= => /(_ (ltnW t'ltt)).
   rewrite ltnNge => /negP; apply.
   apply: leq_sum => ts priorts.
   by move: (Hall ts); rewrite not_andP => -[//|/negP]; rewrite -leqNgt. }
-have [j' [+ j'Ncomplt']] :
-  exists j', j' \in arrivals_of_tsk arr_seq ts 0%nat t'.+1
-    /\ ~ (j' \in arrivals_of_tsk compl_seq ts 0%nat t'.+1).
-{ rewrite not_existsP => Hall.
-  move: Hts; apply/negP; rewrite -leqNgt.
-  apply: leq_sum_sub_uniq; [exact/filter_uniq/arr_uniq|].
-  by move=> j' arrj'; move: (Hall j'); rewrite not_andP => -[|/contrapT]. }
+have [j' [+ [j'Ncomplt' prior_jobs]]] :
+  exists j', j' \in arrivals_of_tsk arr_seq ts 0%N t'
+    /\ ~ (j' \in arrivals_of_tsk compl_seq ts 0%N t')
+    /\ prior_jobs_complete arr_seq sched j' t'.-1.
+{ pose P (i : 'I_t'.+1) :=
+    has (fun j' => ~~ (j' \in arrivals_of_tsk compl_seq ts O t'))
+        (arrivals_of_tsk arr_seq ts O i).
+  have Pt : P ord_max.
+  { apply/hasP; rewrite not_exists2P => Hall.
+    move: Hts; apply/negP; rewrite -leqNgt.
+    apply: leq_sum_sub_uniq; [exact/filter_uniq/arr_uniq|].
+    by move=> j' arrj'; move: (Hall j') => -[//|/negP/negPn]. }
+  have [t'' /hasP[j' j'arrt'' j'Ncomplt'] Pget''] := arg_minP id Pt.
+  exists j'; split; [|split].
+  { move: j'arrt''; rewrite !mem_filter => /andP[->] /=.
+    apply: arrivals_between_sub => //; exact: leq_ord. }
+  { exact/negP. }
+  apply/allP => j'' j''arr; apply/negPn/negP => j''Ncompl.
+  have j'ts : job_task j' = ts.
+  { by move: j'arrt''; rewrite mem_filter => /andP[/eqP]. }
+  have j''ts : job_task j'' = ts.
+  { by move: j''arr; rewrite mem_filter => /andP[/eqP]; rewrite j'ts. }
+  have arrj'ltt'' : (job_arrival j' < t'')%N.
+  { move: j'arrt''; rewrite mem_filter => /andP[_].
+    exact: job_arrival_between_lt. }
+  pose i:= Ordinal (ltn_trans arrj'ltt'' (ltn_ord t'')).
+  have: (i < t'')%N by []; apply/negP; rewrite -leqNgt; apply: Pget''.
+  apply/hasP; exists j''; first by rewrite -j'ts.
+  apply/negP.
+  rewrite mem_filter => /andP[_] /mem_bigcat_nat_exists[tc [+ /= tcltt']].
+  rewrite mem_filter => /andP[/andP[_ +] _]; apply/negP.
+  apply: incompletion_monotonic j''Ncompl.
+  by rewrite -ltnS prednK. }
 rewrite mem_filter => /andP[/eqP j'ts j'arrt'].
+have jschedt' : scheduled_at sched j t'.-1.
+{ apply: service_delta_implies_scheduled; rewrite prednK//.
+  by move: jcomplt' => /andP[?]; apply: leq_trans; rewrite ltnNge. }
+have j'Nbacklogt' : ~~ backlogged sched j' t'.-1.
+{ apply/negP => j'bl; move: priorts; apply/negP; rewrite -leqNgt.
+  rewrite -jtsk -j'ts; apply: FP_pol jschedt' => //.
+  - exact/in_arrivals_implies_arrived/j'arrt'.
+  - by rewrite /preemption_time; case: (sched t'.-1). }
+have j'read : job_ready sched j' t'.-1.
+{ do 2![apply/andP; split=> [|//]].
+  { have [t'' [j't'' /= t''ltt']] := mem_bigcat_nat_exists _ _ _ _ _ j'arrt'.
+    by rewrite /has_arrived (job_arrival_at _ _ j't'')// -ltnS prednK. }
+  apply/negP => j'compl; move: j'Ncomplt'; apply/negP.
+  rewrite mem_filter j'ts eqxx/=.
+  have j'arr : arrives_in arr_seq j'.
+  { exact: in_arrivals_implies_arrived j'arrt'. }
+  move=> {slet' t'ltt jcomplt' jarrt' Hts prior_jobs j'arrt' jschedt'}.
+  case: t' t'gt0 j'compl {j'Nbacklogt'} => [//|t' _].
+  exact: in_completion_sequence_completed. }
+have j'schedt' : scheduled_at sched j' t'.-1.
+{ by move: j'Nbacklogt'; rewrite /backlogged j'read/= => /negPn. }
+move: jschedt' j'schedt'.
+rewrite /scheduled_at !scheduled_in_def => /eqP-> /eqP[] jj'.
+by move: priorts; apply/negP; rewrite -leqNgt -jtsk -j'ts jj'.
+Qed.
 
-
-
-
-
-have jschedpt' := completes_at_implies_scheduled_just_before jcomplt'.
-Print completion_sequence.
-
-About positive_service_implies_scheduled_since_arrival.
-
-
-rewrite mem_filter => /andP[/andP[jNcomplpt' jcomplt'] jarr].
-
-
-
-have H_jobs_must_arrive := valid_schedule_implies_jobs_must_arrive_to_execute
-                             _ _ H_sched_valid.
-have [t'' [/andP[arrlet'' t''ltt'] jschedt'']] :=
-  completed_implies_scheduled_before
-    sched j (H_job_cost_positive j) H_jobs_must_arrive _ jcomplt'.
-Check completed_implies_scheduled_before.
-
-
-
-
-
-
-
-elim: t slet Hbacklog => [|t IHt + Hbacklog]; first by case: s.
-rewrite leq_eqVlt => /orP[/eqP -> //|]; rewrite ltnS => slet.
-rewrite {}IHt => [|//|n' /andP[sltn' n'let]].
-2:{ by apply: Hbacklog; rewrite sltn' leqW. }
-have sst: (s < t.+1 <= t.+1)%nat by rewrite ltnS leqnn andbT.
-have {}Hbacklog := Hbacklog t.+1 sst => {s slet sst}.
-have -> : arrivals_between compl_seq 0%nat t.+1
-          = arrivals_between compl_seq 0%nat t ++ arrivals_at compl_seq t.
-{ by rewrite /arrivals_between big_nat_recr. }
-rewrite filter_cat big_cat /=.
-set se := [seq j <- arrivals_at compl_seq t | _].
-suff -> : se = [::] by rewrite big_nil addn0.
-apply: filter_in_pred0 => j jcomplt {se}.
-have [ts [priorts Hts]] : exists ts, (prior ts < prior tsk)%nat
-  /\ (\sum_(j <- arrivals_of_tsk compl_seq ts 0 t.+1) job_cost j
-      < \sum_(j <- arrivals_of_tsk arr_seq ts 0 t.+1) job_cost j)%N.
-{ rewrite not_existsP => Hall.
-  move: Hbacklog; rewrite ltnNge => /negP; apply.
-  apply: leq_sum => ts priorts.
-  by move: (Hall ts); rewrite not_andP => -[//|/negP]; rewrite -leqNgt. }
-have [j' []] :
-  exists j', j' \in arrivals_of_tsk arr_seq ts 0%nat t.+1
-    /\ ~ (j' \in arrivals_of_tsk compl_seq ts 0%nat t.+1).
-{ rewrite not_existsP => Hall.
-  move: Hts; apply/negP; rewrite -leqNgt.
-  apply: leq_sum_sub_uniq; [exact/filter_uniq/arr_uniq|].
-  by move=> j' arrj'; move: (Hall j'); rewrite not_andP => -[|/contrapT]. }
-rewrite !mem_filter => /andP[/[dup] /eqP j'ts -> /= j'arr] j'Ncompl {Hts}.
-apply/negP => /eqP jtsk.
-move: priorts; apply/negP; rewrite -leqNgt.
-have {}j'Ncompl : ~~ completed_by sched j' t.
-{ set compl := completed_by _.
-  apply/negP => j'compl; apply: j'Ncompl.  (* TODO: faire un lemme séparé: completed_by t -> in arrivals_between completion_sequence 0 t.+1 *)
-  pose tc := [seq t' <- iota 0 t.+1 | compl j' t'].
-  pose mtc := head 0%nat tc.
-  have stc : (0 < size tc)%nat.
-  { rewrite -has_predT; apply/hasP.
-    by exists t => //; rewrite mem_filter j'compl mem_iota add0n /= ltnS. }
-  have mtccompl : compl j' mtc.
-  { rewrite /mtc -nth0; move: stc; exact/all_nthP/filter_all. }
-  have mtcin : mtc \in tc; [by rewrite /mtc -nth0; exact: mem_nth|].
-  have mtcltSt : (mtc < t.+1)%nat.
-  { by move: mtcin; rewrite mem_filter mem_iota add0n => /and3P[]. }
-  have tcsorted : sorted leq tc.
-  { apply: sorted_filter; [exact: leq_trans|exact: iota_sorted]. }
-  have j'Ncompl : ~~ compl j' mtc.-1.
-  { apply/negP => j'compl'.
-    have mtc'in : mtc.-1 \in tc.
-    { rewrite mem_filter mem_iota j'compl' add0n /=.
-      apply: leq_ltn_trans mtcltSt; exact: leq_pred. }
-    have: (mtc.-1 < mtc)%nat.
-    { rewrite ltn_predL.
-      have: ~~ compl j' 0%nat.  (* TODO: lemme intermédiaire ~~ completed_by _ 0 *)
-      { rewrite /compl /completed_by service0 -ltnNge.
-        exact: H_job_cost_positive. }
-      by case: mtc mtccompl {mtcin mtcltSt j'compl' mtc'in} => [->|]. }
-    apply/negP; rewrite -leqNgt {1}/mtc -nth0.
-    have /(nthP 0%nat)[imtc' imtc'lestc <-] := mtc'in.
-    apply: sorted_leq_nth => //; exact: leq_trans. }
-  apply: (mem_bigcat _ _ _ mtc); [by rewrite mem_iota add0n subn0|].
-  rewrite mem_filter /completes_at j'Ncompl -/(compl j' mtc) mtccompl /=.
-  have H_jobs_must_arrive := valid_schedule_implies_jobs_must_arrive_to_execute
-                               _ _ H_sched_valid.
-  have [t'' [/andP[arrlet'' t''ltmtc] _]] := completed_implies_scheduled_before
-    sched j' (H_job_cost_positive j') H_jobs_must_arrive _ mtccompl.
-  apply: arrived_between_implies_in_arrivals => //.
-  { exact: in_arrivals_implies_arrived j'arr. }
-  exact/(leq_trans arrlet'')/ltnW. }
-move: jcomplt; rewrite mem_filter => /andP[/andP[jNcompl jcompl] jarr].
-Print backlogged.
-
-have j'arrin : arrives_in arr_seq j'.
-{ exact: in_arrivals_implies_arrived j'arr. }
-have tpreempt : preemption_time sched t.
-{ by rewrite /preemption_time; case: (sched t). }
-have jsched: scheduled_at sched j t.
-{ Print scheduled_at.
-  rewrite /scheduled_at.
-  Search scheduled_in.
-completed_implies_scheduled_before
-  admit. }
-have j'tback : backlogged sched j' t.
-{ (* j scheduled et uniproc -> j' not scheduled *)
-  admit. }
-rewrite -jtsk -j'ts.
-exact: FP_pol jsched.
-
-
-Print respects_FP_policy.
-Print respects_policy_at_preemption_point.
-
-
-Print completion_sequence.
-Print completes_at.
-Search completed_by.
-completed_implies_not_scheduled:
-  forall {Job : JobType} {H : JobCost Job} {PState : Type}
-    {H1 : ProcessorState Job PState} (sched : schedule PState) 
-    (j : Job),
-  completed_jobs_dont_execute sched ->
-  forall t : instant, completed_by sched j t -> ~~ scheduled_at sched j t
-
-
-Admitted.
-*)
-
+(* The other direction doesn't hold because we only register
+   completion of jobs, so we can't guarantee that the fixed priority policy
+   is respected at each instant of job executions. *)
 Lemma FP_flow_cc_to_arrival_sequences (c : uclock) :
   (* we must assume FIFO inside each sequence (for network calculus
      says nothing about individual jobs in sequences) *)
@@ -326,14 +230,14 @@ Lemma FP_flow_cc_to_arrival_sequences (c : uclock) :
   let A := flow_cc_of_arrival_sequence arr_seq c in
   let D := flow_cc_of_arrival_sequence (completion_sequence arr_seq sched) c in
   (* static_priority.preemptive_SP *)
-  (forall i, forall s t : {nonneg R},
+  (forall i, forall s t : {nonneg R}, s%:nngnum <= t%:nngnum ->
       backlog_itv
-        (\sum_(j | (prior j < prior i)%nat) A j)%C
-        (\sum_(j | (prior j < prior i)%nat) D j)%C
+        (\sum_(j | (prior j < prior i)%N) A j)%C
+        (\sum_(j | (prior j < prior i)%N) D j)%C
         `[s, t] ->
       (D i) s = (D i) t) ->
-  respects_FP_policy.
+  respects_FP_policy_at_preemption_point arr_seq sched FP_prior.
 Proof.
-Admitted.
+Abort.
 
 End Static_priority.