Library prosa.analysis.facts.readiness.sequential


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.task_arrivals.

Throughout this file, we assume the sequential task readiness model.
Require Export prosa.model.readiness.sequential.

In this section, we show some useful properties of the sequential task readiness model.
Section SequentialTasksReadiness.

Consider any type of job associated with any type of tasks ...
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

... and any kind of processor state.
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

Consider any arrival sequence with consistent arrivals.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

  (* As it was mentioned in the beginning of this file, 
     we assume the sequential task readiness model. *)
  Instance sequential_ready_instance : JobReady Job PState :=
    sequential.sequential_ready_instance arr_seq.

  (* Consider any valid schedule of [arr_seq]. *)
  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

Consider an FP policy that indicates a reflexive higher-or-equal priority relation.
  Context `{FP_policy Task}.
  Hypothesis H_priority_is_reflexive : reflexive_priorities.

First, we show that the sequential readiness model is non-clairvoyant.
  Fact sequential_readiness_nonclairvoyance :
    nonclairvoyant_readiness sequential_ready_instance.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  ============================
  nonclairvoyant_readiness sequential_ready_instance

----------------------------------------------------------------------------- *)

  Proof.
    intros sched1 sched2 ? ? ID ? LE; rewrite //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  ============================
  pending sched1 j t && prior_jobs_complete arr_seq sched1 j t =
  pending sched2 j t && prior_jobs_complete arr_seq sched2 j t

----------------------------------------------------------------------------- *)

    erewrite identical_prefix_pending; eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 86)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  ============================
  pending sched2 j t && prior_jobs_complete arr_seq sched1 j t =
  pending sched2 j t && prior_jobs_complete arr_seq sched2 j t

----------------------------------------------------------------------------- *)

    destruct (boolP (pending sched2 j t)) as [_ | _] ⇒ //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 150)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  ============================
  prior_jobs_complete arr_seq sched1 j t =
  prior_jobs_complete arr_seq sched2 j t

----------------------------------------------------------------------------- *)

    destruct (boolP (prior_jobs_complete arr_seq sched2 j t)) as [ALL | NOT_ALL]; apply/eqP.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 2) (ID 248)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  ALL : prior_jobs_complete arr_seq sched2 j t
  ============================
  prior_jobs_complete arr_seq sched1 j t == true

subgoal 2 (ID 303) is:
 prior_jobs_complete arr_seq sched1 j t == false

----------------------------------------------------------------------------- *)

    - rewrite eqb_id; apply/allP; intros ? IN.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 1) (ID 337)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  ALL : prior_jobs_complete arr_seq sched2 j t
  x : Job
  IN : x \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  ============================
  completed_by sched1 x t

subgoal 2 (ID 303) is:
 prior_jobs_complete arr_seq sched1 j t == false

----------------------------------------------------------------------------- *)

      move: ALL ⇒ /allP ALL; specialize (ALL x IN).

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 1) (ID 374)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  x : Job
  IN : x \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  ALL : (fun x : Job => is_true (completed_by sched2 x t)) x
  ============================
  completed_by sched1 x t

subgoal 2 (ID 303) is:
 prior_jobs_complete arr_seq sched1 j t == false

----------------------------------------------------------------------------- *)

      by erewrite identical_prefix_completed_by; eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 303)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  NOT_ALL : ~~ prior_jobs_complete arr_seq sched2 j t
  ============================
  prior_jobs_complete arr_seq sched1 j t == false

----------------------------------------------------------------------------- *)

    - move: NOT_ALL ⇒ /allPn [x IN NCOMP].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 450)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  x : Job
  IN : x \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched2 x t
  ============================
  prior_jobs_complete arr_seq sched1 j t == false

----------------------------------------------------------------------------- *)

      rewrite eqbF_neg; apply/allPn; ∃ x ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 484)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  sched1, sched2 : schedule PState
  j : Job
  h : instant
  ID : identical_prefix sched1 sched2 h
  t : nat
  LE : t <= h
  x : Job
  IN : x \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched2 x t
  ============================
  ~~ completed_by sched1 x t

----------------------------------------------------------------------------- *)

      by erewrite identical_prefix_completed_by; eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next, we show that the sequential readiness model ensures that tasks are sequential. That is, that jobs of the same task execute in order of their arrival.
  Lemma sequential_readiness_implies_sequential_tasks :
    sequential_tasks arr_seq sched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 56)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  ============================
  sequential_tasks arr_seq sched

----------------------------------------------------------------------------- *)

  Proof.
    intros j1 j2 t ARR1 ARR2 SAME LT SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 65)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j1, j2 : Job
  t : instant
  ARR1 : arrives_in arr_seq j1
  ARR2 : arrives_in arr_seq j2
  SAME : same_task j1 j2
  LT : job_arrival j1 < job_arrival j2
  SCHED : scheduled_at sched j2 t
  ============================
  completed_by sched j1 t

----------------------------------------------------------------------------- *)

    destruct (boolP (job_ready sched j2 t)) as [READY | NREADY].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 81)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j1, j2 : Job
  t : instant
  ARR1 : arrives_in arr_seq j1
  ARR2 : arrives_in arr_seq j2
  SAME : same_task j1 j2
  LT : job_arrival j1 < job_arrival j2
  SCHED : scheduled_at sched j2 t
  READY : job_ready sched j2 t
  ============================
  completed_by sched j1 t

subgoal 2 (ID 82) is:
 completed_by sched j1 t

----------------------------------------------------------------------------- *)

    - move: READY ⇒ /andP [PEND /allP ALL]; apply: ALL.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 163)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j1, j2 : Job
  t : instant
  ARR1 : arrives_in arr_seq j1
  ARR2 : arrives_in arr_seq j2
  SAME : same_task j1 j2
  LT : job_arrival j1 < job_arrival j2
  SCHED : scheduled_at sched j2 t
  PEND : pending sched j2 t
  ============================
  j1 \in task_arrivals_before arr_seq (job_task j2) (job_arrival j2)

subgoal 2 (ID 82) is:
 completed_by sched j1 t

----------------------------------------------------------------------------- *)

      rewrite mem_filter; apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 196)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j1, j2 : Job
  t : instant
  ARR1 : arrives_in arr_seq j1
  ARR2 : arrives_in arr_seq j2
  SAME : same_task j1 j2
  LT : job_arrival j1 < job_arrival j2
  SCHED : scheduled_at sched j2 t
  PEND : pending sched j2 t
  ============================
  j1 \in arrivals_between arr_seq 0 (job_arrival j2)

subgoal 2 (ID 82) is:
 completed_by sched j1 t

----------------------------------------------------------------------------- *)

      by apply arrived_between_implies_in_arrivals ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 82)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j1, j2 : Job
  t : instant
  ARR1 : arrives_in arr_seq j1
  ARR2 : arrives_in arr_seq j2
  SAME : same_task j1 j2
  LT : job_arrival j1 < job_arrival j2
  SCHED : scheduled_at sched j2 t
  NREADY : ~~ job_ready sched j2 t
  ============================
  completed_by sched j1 t

----------------------------------------------------------------------------- *)

    - by apply H_valid_schedule in SCHED; rewrite SCHED in NREADY.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  (* Finally, we show that the sequential readiness model is a
     work-bearing readiness model. That is, if a job [j] is pending
     but not ready at a time instant [t], then there exists another
     (earlier) job of the same task that is pending and ready at time
     [t]. *)
  Lemma sequential_readiness_implies_work_bearing_readiness :
    work_bearing_readiness arr_seq sched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 67)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  ============================
  work_bearing_readiness arr_seq sched

----------------------------------------------------------------------------- *)

  Proof.
    intros j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 69)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  ============================
  forall t : instant,
  arrives_in arr_seq j ->
  pending sched j t ->
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

    have EX: ∃ k, job_arrival j ≤ k by (∃ (job_arrival j)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 80)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  EX : exists k : nat, job_arrival j <= k
  ============================
  forall t : instant,
  arrives_in arr_seq j ->
  pending sched j t ->
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

    destruct EX as [k LE]; move: j LE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 89)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  ============================
  forall j : Job,
  job_arrival j <= k ->
  forall t : instant,
  arrives_in arr_seq j ->
  pending sched j t ->
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

    induction k; intros ? ? ? ARR PEND.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 101)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

subgoal 2 (ID 106) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 101)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

destruct (boolP (job_ready sched j t)) as [READY | NREADY].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 122)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  READY : job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

subgoal 2 (ID 123) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 122)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  READY : job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

by ∃ j; repeat split; eauto using (H_priority_is_reflexive 0).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 123) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
subgoal 2 (ID 106) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 123)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  NREADY : ~~ job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 123)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  NREADY : ~~ job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

move: NREADY; rewrite //= PEND Bool.andb_true_l ⇒ /allPn [jhp IN NCOMP].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 217)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  jhp : Job
  IN : jhp \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched jhp t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        apply arrives_in_task_arrivals_before_implies_arrives_before in IN; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 223)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  j : Job
  LE : job_arrival j <= 0
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  jhp : Job
  IN : job_arrival jhp < job_arrival j
  NCOMP : ~~ completed_by sched jhp t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        by exfalso; move: LE; rewrite leqn0 ⇒ /eqP EQ; rewrite EQ in IN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 106) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 106) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  LE : job_arrival j <= k.+1
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  LE : job_arrival j <= k.+1
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

move: LE; rewrite leq_eqVlt ltnS ⇒ /orP [/eqP EQ | LE]; last by apply IHk.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 402)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

      destruct (boolP (job_ready sched j t)) as [READY | NREADY].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 422)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  READY : job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

subgoal 2 (ID 423) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 422)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  READY : job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

by ∃ j; repeat split; eauto using (H_priority_is_reflexive 0).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 423) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 423)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  NREADY : ~~ job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 423)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  NREADY : ~~ job_ready sched j t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j

----------------------------------------------------------------------------- *)

move: NREADY; rewrite //= PEND Bool.andb_true_l ⇒ /allPn [j' IN NCOMP].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 517)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        have LE' : job_arrival j' ≤ k.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 520)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  ============================
  job_arrival j' <= k

subgoal 2 (ID 522) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\
   pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
   hep_job j_hp j

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 520)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  ============================
  job_arrival j' <= k

----------------------------------------------------------------------------- *)

by apply arrives_in_task_arrivals_before_implies_arrives_before in IN; rewrite // -ltnS -EQ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 522) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\
   pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
   hep_job j_hp j

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 522)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        have ARR' : arrives_in arr_seq j'.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 558)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ============================
  arrives_in arr_seq j'

subgoal 2 (ID 560) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\
   pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
   hep_job j_hp j

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 558)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ============================
  arrives_in arr_seq j'

----------------------------------------------------------------------------- *)

by eapply arrives_in_task_arrivals_implies_arrived; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 560) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\
   pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
   hep_job j_hp j

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 560)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        have PEND' : pending sched j' t.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 574)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  ============================
  pending sched j' t

subgoal 2 (ID 576) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\
   pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
   hep_job j_hp j

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 574)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  ============================
  pending sched j' t

----------------------------------------------------------------------------- *)

apply/andP; split; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 602)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  ============================
  has_arrived j' t

----------------------------------------------------------------------------- *)

          move: PEND ⇒ /andP [LE _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 644)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  LE : has_arrived j t
  ============================
  has_arrived j' t

----------------------------------------------------------------------------- *)

          by unfold has_arrived in *; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 576) is:
 exists j_hp : Job,
   arrives_in arr_seq j_hp /\
   pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
   hep_job j_hp j

----------------------------------------------------------------------------- *)

        }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 576)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  IHk : forall j : Job,
        job_arrival j <= k ->
        forall t : instant,
        arrives_in arr_seq j ->
        pending sched j t ->
        exists j_hp : Job,
          arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
  j : Job
  t : instant
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  j' : Job
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  PEND' : pending sched j' t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        specialize (IHk j' LE' t ARR' PEND').

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 800)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  t : instant
  j' : Job
  IHk : exists j_hp : Job,
          arrives_in arr_seq j_hp /\
          job_ready sched j_hp t /\ hep_job j_hp j'
  j : Job
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  PEND' : pending sched j' t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        destruct IHk as [j'' [ARR'' [READY'' HEP'']]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 819)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  t : instant
  j', j'' : Job
  ARR'' : arrives_in arr_seq j''
  READY'' : job_ready sched j'' t
  HEP'' : hep_job j'' j'
  j : Job
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  PEND' : pending sched j' t
  ============================
  exists j_hp : Job,
    arrives_in arr_seq j_hp /\
    pending sched j_hp t && prior_jobs_complete arr_seq sched j_hp t /\
    hep_job j_hp j

----------------------------------------------------------------------------- *)

        ∃ j''; repeat split; auto.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 828)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  t : instant
  j', j'' : Job
  ARR'' : arrives_in arr_seq j''
  READY'' : job_ready sched j'' t
  HEP'' : hep_job j'' j'
  j : Job
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  EQ : job_arrival j = k.+1
  IN : j' \in task_arrivals_before arr_seq (job_task j) (job_arrival j)
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  PEND' : pending sched j' t
  ============================
  hep_job j'' j

----------------------------------------------------------------------------- *)

        clear EQ; apply arrives_in_task_arrivals_implies_job_task in IN; move: IN ⇒ /eqP EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 878)
  
  Job : JobType
  Task : TaskType
  H : JobTask Job Task
  H0 : JobArrival Job
  H1 : JobCost Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H_valid_schedule : valid_schedule sched arr_seq
  H3 : FP_policy Task
  H_priority_is_reflexive : reflexive_priorities
  k : nat
  t : instant
  j', j'' : Job
  ARR'' : arrives_in arr_seq j''
  READY'' : job_ready sched j'' t
  HEP'' : hep_job j'' j'
  j : Job
  ARR : arrives_in arr_seq j
  PEND : pending sched j t
  NCOMP : ~~ completed_by sched j' t
  LE' : job_arrival j' <= k
  ARR' : arrives_in arr_seq j'
  PEND' : pending sched j' t
  EQ : job_task j' = job_task j
  ============================
  hep_job j'' j

----------------------------------------------------------------------------- *)

        by rewrite /hep_job /FP_to_JLFP -EQ.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End SequentialTasksReadiness.