Library prosa.analysis.facts.preemption.rtc_threshold.job_preemptable


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

Welcome to Coq 8.13.0 (January 2021)

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


Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.model.task.preemption.parameters.

Run-to-Completion Threshold

In this section, we provide a few basic properties of run-to-completion-threshold-compliant schedules.
Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

In addition, we assume existence of a function mapping jobs to theirs preemption points.
  Context `{JobPreemptable Job}.

Consider any kind of processor state model, ...
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

... any job arrival sequence, ...
  Variable arr_seq: arrival_sequence Job.

... and any given schedule.
  Variable sched: schedule PState.

Assume that the preemption model is valid.
Consider an arbitrary job j from the arrival sequence.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.

First we prove a few auxiliary lemmas about [job_preemption_points].
  Section AuxiliaryLemmas.

We prove that the sequence of preemption points of a zero-cost job consists of one element -- 0.
    Lemma preemption_points_of_zero_cost_job:
      job_cost j = 0
      job_preemption_points j = [::0].

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

1 subgoal (ID 33)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost j = 0 -> job_preemption_points j = [:: 0]

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


    Proof.
      intros ZERO.

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

1 subgoal (ID 34)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ZERO : job_cost j = 0
  ============================
  job_preemption_points j = [:: 0]

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


      destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.

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

1 subgoal (ID 50)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ZERO : job_cost j = 0
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  job_preemption_points j = [:: 0]

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


      unfold job_preemption_points; rewrite ZERO; simpl.

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

1 subgoal (ID 65)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ZERO : job_cost j = 0
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  (if job_preemptable j 0 then [:: 0] else [::]) = [:: 0]

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


      simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.

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

1 subgoal (ID 68)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ZERO : job_cost j = 0
  A1 : job_preemptable j 0
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  (if job_preemptable j 0 then [:: 0] else [::]) = [:: 0]

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


        by rewrite A1.

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

No more subgoals.

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


    Qed.

For a positive-cost job, 0 ...
    Lemma zero_in_preemption_points:
      0 < job_cost j
      0 \in job_preemption_points j.

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

1 subgoal (ID 43)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  0 < job_cost j -> 0 \in job_preemption_points j

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


    Proof.
      intros POS.

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

1 subgoal (ID 44)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  0 \in job_preemption_points j

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


      unfold job_preemption_points, range.

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

1 subgoal (ID 45)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]

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


      destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.

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

1 subgoal (ID 61)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]

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


      unfold job_cannot_become_nonpreemptive_before_execution in ×.

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

1 subgoal (ID 70)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  A1 : job_preemptable j 0
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  0 \in [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]

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


      rewrite index_iota_lt_step; last by done.

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

1 subgoal (ID 75)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  A1 : job_preemptable j 0
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  0 \in [seq ρ <- 0 :: index_iota 1 (job_cost j).+1 | job_preemptable j ρ]

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


        by simpl; rewrite A1 in_cons eq_refl.

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

No more subgoals.

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


    Qed.

... and [job_cost] are in preemption points.
    Lemma job_cost_in_preemption_points:
      0 < job_cost j
      job_cost j \in job_preemption_points j.

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

1 subgoal (ID 55)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  0 < job_cost j -> job_cost j \in job_preemption_points j

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


    Proof.
      intros POS.

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

1 subgoal (ID 56)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  job_cost j \in job_preemption_points j

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


      unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.

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

1 subgoal (ID 65)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  job_cost j \in [seq ρ <- iota 0 (job_cost j + 1) | job_preemptable j ρ]

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


      rewrite iota_add add0n filter_cat mem_cat.

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

1 subgoal (ID 87)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  (job_cost j \in [seq ρ <- iota 0 (job_cost j) | job_preemptable j ρ])
  || (job_cost j \in [seq ρ <- iota (job_cost j) 1 | job_preemptable j ρ])

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


      apply/orP; right; simpl.

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

1 subgoal (ID 123)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  job_cost j
    \in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])

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


      destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.

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

1 subgoal (ID 139)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  job_cost j
    \in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])

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


      unfold job_cannot_be_nonpreemptive_after_completion in ×.

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

1 subgoal (ID 148)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_preemptable j (job_cost j)
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  job_cost j
    \in (if job_preemptable j (job_cost j) then [:: job_cost j] else [::])

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


        by rewrite A2 in_cons eq_refl.

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

No more subgoals.

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


    Qed.

Therefore, for a positive-cost job size of the sequence of preemption points is at least two.
    Lemma size_of_preemption_points:
      0 < job_cost j
      2 size (job_preemption_points j).

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

1 subgoal (ID 62)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  0 < job_cost j -> 1 < size (job_preemption_points j)

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


    Proof.
      intros POS.

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

1 subgoal (ID 63)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  1 < size (job_preemption_points j)

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


      replace 2 with (size [::0; job_cost j]); last by done.

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

1 subgoal (ID 73)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  size [:: 0; job_cost j] <= size (job_preemption_points j)

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


      apply subseq_leq_size.

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

2 subgoals (ID 76)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  uniq [:: 0; job_cost j]

subgoal 2 (ID 77) is:
 forall x : nat_eqType,
 x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


      - apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 103)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  0 \notin [:: job_cost j]

subgoal 2 (ID 104) is:
 (job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
 forall x : nat_eqType,
 x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


rewrite !in_cons Bool.negb_orb.

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

3 subgoals (ID 118)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  (0 != job_cost j) && (0 \notin [::])

subgoal 2 (ID 104) is:
 (job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
 forall x : nat_eqType,
 x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


        + apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 144)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  0 != job_cost j

subgoal 2 (ID 145) is:
 0 \notin [::]
subgoal 3 (ID 104) is:
 (job_cost j \notin [::]) && true
subgoal 4 (ID 77) is:
 forall x : nat_eqType,
 x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


by rewrite neq_ltn POS.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 145)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  0 \notin [::]

subgoal 2 (ID 104) is:
 (job_cost j \notin [::]) && true
subgoal 3 (ID 77) is:
 forall x : nat_eqType,
 x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


by done.

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

2 subgoals (ID 104)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  (job_cost j \notin [::]) && true

subgoal 2 (ID 77) is:
 forall x : nat_eqType,
 x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


        + apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ============================
  forall x : nat_eqType,
  x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


      - intros ρ; rewrite !in_cons; move ⇒ /orP [/eqP EQ| /orP [/eqP Cost | C]].

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

3 subgoals (ID 339)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ρ : nat_eqType
  EQ : ρ = 0
  ============================
  ρ \in job_preemption_points j

subgoal 2 (ID 340) is:
 ρ \in job_preemption_points j
subgoal 3 (ID 341) is:
 ρ \in job_preemption_points j

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


        + by subst; apply zero_in_preemption_points.

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

2 subgoals (ID 340)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ρ : nat_eqType
  Cost : ρ = job_cost j
  ============================
  ρ \in job_preemption_points j

subgoal 2 (ID 341) is:
 ρ \in job_preemption_points j

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


        + by subst; apply job_cost_in_preemption_points.

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

1 subgoal (ID 341)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : 0 < job_cost j
  ρ : nat_eqType
  C : ρ \in [::]
  ============================
  ρ \in job_preemption_points j

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


        + by done.

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

No more subgoals.

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


    Qed.

Next we show that the sequence of preemption points is a non-decreasing sequence.
    Lemma preemption_points_nondecreasing:
      nondecreasing_sequence (job_preemption_points j).

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

1 subgoal (ID 66)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  nondecreasing_sequence (job_preemption_points j)

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


    Proof. by apply increasing_implies_nondecreasing, iota_is_increasing_sequence.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


Qed.

Next, we prove that the last element of the sequence of preemption points is [job_cost].
    Lemma job_cost_is_last_element_of_preemption_points:
      job_cost j = last0 (job_preemption_points j).

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

1 subgoal (ID 73)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost j = last0 (job_preemption_points j)

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


    Proof.
      unfold job_preemption_points.

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

1 subgoal (ID 74)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost j = last0 [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]

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


      edestruct H_valid_preemption_model as [A1 [A2 [A3 A4]]]; eauto 2.

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

1 subgoal (ID 92)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  job_cost j = last0 [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]

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


      erewrite last0_filter.

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

4 focused subgoals
(shelved: 1) (ID 96)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  job_cost j = ?x

subgoal 2 (ID 97) is:
 range 0 (job_cost j) <> [::]
subgoal 3 (ID 98) is:
 last0 (range 0 (job_cost j)) = ?x
subgoal 4 (ID 99) is:
 job_preemptable j ?x

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


      + by apply/eqP; apply eq_refl.

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

3 subgoals (ID 97)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  range 0 (job_cost j) <> [::]

subgoal 2 (ID 98) is:
 last0 (range 0 (job_cost j)) = job_cost j
subgoal 3 (ID 99) is:
 job_preemptable j (job_cost j)

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


      + unfold range, index_iota; rewrite subn0 -addn1.

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

3 subgoals (ID 163)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  iota 0 (job_cost j + 1) <> [::]

subgoal 2 (ID 98) is:
 last0 (range 0 (job_cost j)) = job_cost j
subgoal 3 (ID 99) is:
 job_preemptable j (job_cost j)

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


          by rewrite iota_add; destruct (iota 0 (job_cost j)).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 98)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  last0 (range 0 (job_cost j)) = job_cost j

subgoal 2 (ID 99) is:
 job_preemptable j (job_cost j)

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


      + unfold range, index_iota; rewrite subn0 -addn1.

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

2 subgoals (ID 243)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  last0 (iota 0 (job_cost j + 1)) = job_cost j

subgoal 2 (ID 99) is:
 job_preemptable j (job_cost j)

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


          by rewrite iota_add last0_cat //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 99)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  job_preemptable j (job_cost j)

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


      + by apply A2.

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

No more subgoals.

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


    Qed.

Last non-preemptive segment of a positive-cost job has positive length.
    Lemma job_last_nonpreemptive_segment_positive:
      job_cost_positive j
      0 < job_last_nonpreemptive_segment j.

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

1 subgoal (ID 79)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost_positive j -> 0 < job_last_nonpreemptive_segment j

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


    Proof.
      intros COST.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 80)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < job_last_nonpreemptive_segment j

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


unfold job_last_nonpreemptive_segment.

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

1 subgoal (ID 81)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < last0 (lengths_of_segments j)

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


      rewrite last0_nth function_of_distances_is_correct subn_gt0.

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

1 subgoal (ID 92)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  nth 0 (job_preemption_points j) (size (lengths_of_segments j)).-1 <
  nth 0 (job_preemption_points j) (size (lengths_of_segments j)).-1.+1

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


      rewrite [size _]pred_Sn -addn1-addn1.

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

1 subgoal (ID 104)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  nth 0 (job_preemption_points j) (size (lengths_of_segments j) + 1).-2 + 1 <=
  nth 0 (job_preemption_points j) (size (lengths_of_segments j) + 1).-2.+1

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


      rewrite -size_of_seq_of_distances ?addn1; last by apply size_of_preemption_points.

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

1 subgoal (ID 112)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1

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


      rewrite prednK; last first.

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

2 subgoals (ID 120)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < (size (job_preemption_points j)).-1

subgoal 2 (ID 119) is:
 nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
 nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1

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


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

1 subgoal (ID 120)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < (size (job_preemption_points j)).-1

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


rewrite -(leq_add2r 1) !addn1 prednK.

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

2 subgoals (ID 135)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  1 < size (job_preemption_points j)

subgoal 2 (ID 136) is:
 0 < size (job_preemption_points j)

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


        - apply size_of_preemption_points; eauto.

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

1 subgoal (ID 136)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < size (job_preemption_points j)

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


        - rewrite ltnW //; apply size_of_preemption_points; eauto.

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

1 subgoal

subgoal 1 (ID 119) is:
 nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
 nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1

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


      }

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

1 subgoal (ID 119)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-1

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


      apply iota_is_increasing_sequence; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 198)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  (size (job_preemption_points j)).-2 < (size (job_preemption_points j)).-1

subgoal 2 (ID 199) is:
 (size (job_preemption_points j)).-1 <
 size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]

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


      - rewrite -(leq_add2r 2) !addn2.

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

2 subgoals (ID 209)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  (size (job_preemption_points j)).-2.+2 <
  (size (job_preemption_points j)).-1.+2

subgoal 2 (ID 199) is:
 (size (job_preemption_points j)).-1 <
 size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]

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


        rewrite prednK; first by done.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 215)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < (size (job_preemption_points j)).-1

subgoal 2 (ID 199) is:
 (size (job_preemption_points j)).-1 <
 size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]

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


        rewrite -(leq_add2r 1) !addn1.

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

2 subgoals (ID 225)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  1 < (size (job_preemption_points j)).-1.+1

subgoal 2 (ID 199) is:
 (size (job_preemption_points j)).-1 <
 size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]

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


        rewrite prednK.

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

3 subgoals (ID 230)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  1 < size (job_preemption_points j)

subgoal 2 (ID 231) is:
 0 < size (job_preemption_points j)
subgoal 3 (ID 199) is:
 (size (job_preemption_points j)).-1 <
 size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]

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


        + by apply size_of_preemption_points.

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

2 subgoals (ID 231)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < size (job_preemption_points j)

subgoal 2 (ID 199) is:
 (size (job_preemption_points j)).-1 <
 size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]

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


        + by rewrite ltnW //; apply size_of_preemption_points.

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

1 subgoal (ID 199)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  (size (job_preemption_points j)).-1 <
  size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]

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


      - rewrite -(leq_add2r 1) !addn1.

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

1 subgoal (ID 270)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  (size (job_preemption_points j)).-1.+1 <
  (size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]).+1

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


        unfold job_preemption_points, range.

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

1 subgoal (ID 272)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  (size [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]).-1.+1 <
  (size [seq x <- index_iota 0 (job_cost j).+1 | job_preemptable j x]).+1

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


        rewrite prednK ?ltnS; first by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 277)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < size [seq ρ <- index_iota 0 (job_cost j).+1 | job_preemptable j ρ]

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


          by rewrite ltnW //; apply size_of_preemption_points.

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

No more subgoals.

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


    Qed.

Max nonpreemptive segment of a positive-cost job has positive length.
    Lemma job_max_nonpreemptive_segment_positive:
      job_cost_positive j
      0 < job_max_nonpreemptive_segment j.

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

1 subgoal (ID 85)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost_positive j -> 0 < job_max_nonpreemptive_segment j

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


    Proof.
      intros COST.

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

1 subgoal (ID 86)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < job_max_nonpreemptive_segment j

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


      eapply leq_trans.

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

2 focused subgoals
(shelved: 1) (ID 88)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < ?n

subgoal 2 (ID 89) is:
 ?n <= job_max_nonpreemptive_segment j

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


      - by apply job_last_nonpreemptive_segment_positive.

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

1 subgoal (ID 89)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  job_last_nonpreemptive_segment j <= job_max_nonpreemptive_segment j

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


      - by apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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



    Qed.

Next we show that max nonpreemptive segment is at most the cost of a job.
    Lemma job_max_nonpreemptive_segment_le_job_cost:
      job_max_nonpreemptive_segment j job_cost j.

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

1 subgoal (ID 91)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_max_nonpreemptive_segment j <= job_cost j

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


    Proof.
      eapply leq_trans.

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

2 focused subgoals
(shelved: 1) (ID 93)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_max_nonpreemptive_segment j <= ?n

subgoal 2 (ID 94) is:
 ?n <= job_cost j

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


      apply max_distance_in_seq_le_last_element_of_seq; apply preemption_points_nondecreasing.

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

1 subgoal (ID 94)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  last0 (job_preemption_points j) <= job_cost j

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


      destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.

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

1 subgoal (ID 111)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ============================
  last0 (job_preemption_points j) <= job_cost j

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


      case: (posnP (job_cost j)) ⇒ [ZERO|POSt].

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

2 subgoals (ID 159)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ZERO : job_cost j = 0
  ============================
  last0 (job_preemption_points j) <= job_cost j

subgoal 2 (ID 160) is:
 last0 (job_preemption_points j) <= job_cost j

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


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

1 subgoal (ID 159)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ZERO : job_cost j = 0
  ============================
  last0 (job_preemption_points j) <= job_cost j

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


unfold job_preemption_points; rewrite ZERO.

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

1 subgoal (ID 163)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ZERO : job_cost j = 0
  ============================
  last0 [seq ρ <- range 0 0 | job_preemptable j ρ] <= 0

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


        simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.

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

1 subgoal (ID 176)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_preemptable j 0
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  ZERO : job_cost j = 0
  ============================
  last0 (if job_preemptable j 0 then [:: 0] else [::]) <= 0

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


          by rewrite A1.

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

1 subgoal

subgoal 1 (ID 160) is:
 last0 (job_preemption_points j) <= job_cost j

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


      }

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

1 subgoal (ID 160)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  POSt : 0 < job_cost j
  ============================
  last0 (job_preemption_points j) <= job_cost j

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


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

1 subgoal (ID 160)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  POSt : 0 < job_cost j
  ============================
  last0 (job_preemption_points j) <= job_cost j

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


eapply leq_trans; first apply last_of_seq_le_max_of_seq.

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

1 subgoal (ID 181)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  POSt : 0 < job_cost j
  ============================
  max0 (job_preemption_points j) <= job_cost j

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


        rewrite job_cost_is_last_element_of_preemption_points.

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

1 subgoal (ID 183)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  POSt : 0 < job_cost j
  ============================
  max0 (job_preemption_points j) <= last0 (job_preemption_points j)

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


        apply last_is_max_in_nondecreasing_seq; first by apply preemption_points_nondecreasing.

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

1 subgoal (ID 185)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  POSt : 0 < job_cost j
  ============================
  max0 (job_preemption_points j) \in job_preemption_points j

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


        apply max0_in_seq.

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

1 subgoal (ID 186)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  POSt : 0 < job_cost j
  ============================
  job_preemption_points j <> [::]

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


        have LL := size_of_preemption_points POSt.

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

1 subgoal (ID 191)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : job_cannot_become_nonpreemptive_before_execution j
  A2 : job_cannot_be_nonpreemptive_after_completion j
  A3 : not_preemptive_implies_scheduled sched j
  A4 : execution_starts_with_preemption_point sched j
  POSt : 0 < job_cost j
  LL : 1 < size (job_preemption_points j)
  ============================
  job_preemption_points j <> [::]

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


          by destruct (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


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

No more subgoals.

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



    Qed.

We also show that last nonpreemptive segment is at most the cost of a job.
    Lemma job_last_nonpreemptive_segment_le_job_cost:
      job_last_nonpreemptive_segment j job_cost j.

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

1 subgoal (ID 97)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_last_nonpreemptive_segment j <= job_cost j

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


    Proof.
      eapply leq_trans.

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

2 focused subgoals
(shelved: 1) (ID 99)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_last_nonpreemptive_segment j <= ?n

subgoal 2 (ID 100) is:
 ?n <= job_cost j

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


      - apply last_of_seq_le_max_of_seq.

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

1 subgoal (ID 100)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  max0 (lengths_of_segments j) <= job_cost j

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


      - apply job_max_nonpreemptive_segment_le_job_cost.

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

No more subgoals.

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


    Qed.

  End AuxiliaryLemmas.

We prove that the run-to-completion threshold is positive for any job with positive cost. I.e., in order to become non-preemptive a job must receive at least one unit of service.
  Lemma job_run_to_completion_threshold_positive:
    job_cost_positive j
    0 < job_rtct j.

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

1 subgoal (ID 29)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost_positive j -> 0 < job_rtct j

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


  Proof.
    intros COST; unfold job_rtct, ε.

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

1 subgoal (ID 31)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  ============================
  0 < job_cost j - (job_last_nonpreemptive_segment j - 1)

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


    have N1 := job_last_nonpreemptive_segment_positive COST.

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

1 subgoal (ID 36)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  N1 : 0 < job_last_nonpreemptive_segment j
  ============================
  0 < job_cost j - (job_last_nonpreemptive_segment j - 1)

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


    have N2 := job_last_nonpreemptive_segment_le_job_cost.

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

1 subgoal (ID 41)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  COST : job_cost_positive j
  N1 : 0 < job_last_nonpreemptive_segment j
  N2 : job_last_nonpreemptive_segment j <= job_cost j
  ============================
  0 < job_cost j - (job_last_nonpreemptive_segment j - 1)

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


    ssrlia.

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

No more subgoals.

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


  Qed.

Next we show that the run-to-completion threshold is at most the cost of a job.
  Lemma job_run_to_completion_threshold_le_job_cost:
    job_rtct j job_cost j.

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

1 subgoal (ID 35)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_rtct j <= job_cost j

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


  Proof. by apply leq_subr.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


Qed.


We prove that a job cannot be preempted during execution of the last segment.
  Lemma job_cannot_be_preempted_within_last_segment:
     (ρ : duration),
      job_rtct j ρ < job_cost j
      ~~ job_preemptable j ρ.

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

1 subgoal (ID 43)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  forall ρ : duration, job_rtct j <= ρ < job_cost j -> ~~ job_preemptable j ρ

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


  Proof.
    move ⇒ ρ /andP [GE LT].

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

1 subgoal (ID 83)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  GE : job_rtct j <= ρ
  LT : ρ < job_cost j
  ============================
  ~~ job_preemptable j ρ

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


    apply/negP; intros C.

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

1 subgoal (ID 105)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  GE : job_rtct j <= ρ
  LT : ρ < job_cost j
  C : job_preemptable j ρ
  ============================
  False

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


    have POS : 0 < job_cost j; first by ssrlia.

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

1 subgoal (ID 110)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  GE : job_rtct j <= ρ
  LT : ρ < job_cost j
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  ============================
  False

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


    rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.

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

1 subgoal (ID 290)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  LT : ρ < job_cost j
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  GE : job_cost j + ε - job_last_nonpreemptive_segment j <= ρ
  ============================
  False

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


    rewrite -subh1 in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 383)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  LT : ρ < job_cost j
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  GE : job_cost j - job_last_nonpreemptive_segment j < ρ
  ============================
  False

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


    rewrite job_cost_is_last_element_of_preemption_points in LT, GE.

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

1 subgoal (ID 409)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : last0 (job_preemption_points j) - job_last_nonpreemptive_segment j < ρ
  ============================
  False

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


    rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.

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

1 subgoal (ID 437)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  ============================
  False

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


    have EQ := antidensity_of_nondecreasing_seq.

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

1 subgoal (ID 460)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : forall (xs : seq nat) (x n : nat),
       nondecreasing_sequence xs ->
       nth 0 xs n < x < nth 0 xs n.+1 -> x \notin xs
  ============================
  False

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


    specialize (EQ (job_preemption_points j) ρ (size (job_preemption_points j)).-2 ).

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

1 subgoal (ID 469)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : nondecreasing_sequence (job_preemption_points j) ->
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ <
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
       ρ \notin job_preemption_points j
  ============================
  False

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


    feed_n 2 EQ; first by apply preemption_points_nondecreasing.

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

2 subgoals (ID 476)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ <
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
       ρ \notin job_preemption_points j
  ============================
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 < ρ <
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1

subgoal 2 (ID 481) is:
 False

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


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

1 subgoal (ID 476)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ <
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
       ρ \notin job_preemption_points j
  ============================
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 < ρ <
  nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1

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


apply/andP; split; first by done.

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

1 subgoal (ID 508)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ <
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
       ρ \notin job_preemption_points j
  ============================
  ρ < nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1

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


      rewrite prednK; first by rewrite -last0_nth.

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

1 subgoal (ID 513)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ <
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
       ρ \notin job_preemption_points j
  ============================
  0 < (size (job_preemption_points j)).-1

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


      rewrite -(leq_add2r 1) !addn1 prednK.

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

2 subgoals (ID 531)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ <
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
       ρ \notin job_preemption_points j
  ============================
  1 < size (job_preemption_points j)

subgoal 2 (ID 532) is:
 0 < size (job_preemption_points j)

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


      - by apply size_of_preemption_points.

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

1 subgoal (ID 532)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ <
       nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2.+1 ->
       ρ \notin job_preemption_points j
  ============================
  0 < size (job_preemption_points j)

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


      - by eapply leq_trans; last apply size_of_preemption_points.

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

1 subgoal

subgoal 1 (ID 481) is:
 False

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


    }

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

1 subgoal (ID 481)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  EQ : ρ \notin job_preemption_points j
  ============================
  False

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


    move: EQ ⇒ /negP EQ; apply: EQ.

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

1 subgoal (ID 570)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  ============================
  ρ \in job_preemption_points j

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


    apply conversion_preserves_equivalence; try done.

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

1 subgoal (ID 582)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  ============================
  ρ <= job_cost j

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


    eapply leq_trans; first by apply ltnW; exact LT.

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

1 subgoal (ID 607)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : duration
  C : job_preemptable j ρ
  POS : 0 < job_cost j
  LT : ρ < last0 (job_preemption_points j)
  GE : nth 0 (job_preemption_points j) (size (job_preemption_points j)).-2 <
       ρ
  ============================
  last0 (job_preemption_points j) <= job_cost j

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


      by rewrite job_cost_is_last_element_of_preemption_points.

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

No more subgoals.

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


  Qed.

In order to get a consistent schedule, the scheduler should respect the notion of run-to-completion threshold. We assume that, after a job reaches its run-to-completion threshold, it cannot be preempted until its completion.
  Lemma job_nonpreemptive_after_run_to_completion_threshold:
     t t',
      t t'
      job_rtct j service sched j t
      ~~ completed_by sched j t'
      scheduled_at sched j t'.

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

1 subgoal (ID 59)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  forall t t' : nat,
  t <= t' ->
  job_rtct j <= service sched j t ->
  ~~ completed_by sched j t' -> scheduled_at sched j t'

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


  Proof.
    intros ? ? LE TH COM.

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

1 subgoal (ID 64)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  t, t' : nat
  LE : t <= t'
  TH : job_rtct j <= service sched j t
  COM : ~~ completed_by sched j t'
  ============================
  scheduled_at sched j t'

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


    apply H_valid_preemption_model; first by done.

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

1 subgoal (ID 80)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  t, t' : nat
  LE : t <= t'
  TH : job_rtct j <= service sched j t
  COM : ~~ completed_by sched j t'
  ============================
  ~~ job_preemptable j (service sched j t')

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


    apply job_cannot_be_preempted_within_last_segment; apply/andP; split.

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

2 subgoals (ID 107)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  t, t' : nat
  LE : t <= t'
  TH : job_rtct j <= service sched j t
  COM : ~~ completed_by sched j t'
  ============================
  job_rtct j <= service sched j t'

subgoal 2 (ID 108) is:
 service sched j t' < job_cost j

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


    - by apply leq_trans with (service sched j t); last apply service_monotonic.

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

1 subgoal (ID 108)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  H1 : JobPreemptable Job
  PState : Type
  H2 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  H_valid_preemption_model : valid_preemption_model arr_seq sched
  j : Job
  H_j_arrives : arrives_in arr_seq j
  t, t' : nat
  LE : t <= t'
  TH : job_rtct j <= service sched j t
  COM : ~~ completed_by sched j t'
  ============================
  service sched j t' < job_cost j

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


    - by rewrite ltnNge.

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

No more subgoals.

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


  Qed.

End RunToCompletionThreshold.

We add the above lemmas into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.