Library prosa.analysis.facts.preemption.job.limited


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.model.schedule.limited_preemptive.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.facts.model.ideal_schedule.

Throughout this file, we assume the job model with limited preemption points.
Require Import prosa.model.preemption.limited_preemptive.

Platform for Models with Limited Preemptions

In this section, we prove that instantiation of predicate [job_preemptable] to the model with limited preemptions indeed defines a valid preemption model.
Section ModelWithLimitedPreemptions.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

In addition, assume the existence of a function that maps a job to the sequence of its preemption points.
  Context `{JobPreemptionPoints Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Next, consider any limited ideal uni-processor schedule of this arrival sequence ...
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_schedule_respects_preemption_model:
    schedule_respects_preemption_model arr_seq sched.

...where jobs do not execute after their completion.
  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

Next, we assume that preemption points are defined by the job-level model with limited preemptions.
  Hypothesis H_valid_limited_preemptions_job_model:
    valid_limited_preemptions_job_model arr_seq.

First, we prove a few auxiliary lemmas.
  Section AuxiliaryLemmas.

Consider a job j.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.

Recall that 0 is a preemption point.
    Remark zero_in_preemption_points: 0 \in job_preemption_points j.

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

1 subgoal (ID 1543)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  0 \in job_preemption_points j

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

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

No more subgoals.

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

Qed.

Using the fact that [job_preemption_points] is a non-decreasing sequence, we prove that the first element of [job_preemption_points] is 0.
    Lemma zero_is_first_element: first0 (job_preemption_points j) = 0.

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

1 subgoal (ID 1548)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  first0 (job_preemption_points j) = 0

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

    Proof.
      have F := zero_in_preemption_points.

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

1 subgoal (ID 1553)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  F : 0 \in job_preemption_points j
  ============================
  first0 (job_preemption_points j) = 0

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

      destruct H_valid_limited_preemptions_job_model as [_ [_ C]]; specialize (C j H_j_arrives).

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

1 subgoal (ID 1567)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  F : 0 \in job_preemption_points j
  C : nondecreasing_sequence (job_preemption_points j)
  ============================
  first0 (job_preemption_points j) = 0

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

        by apply nondec_seq_zero_first.

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

No more subgoals.

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

    Qed.

We prove that the list of preemption points is not empty.
    Lemma list_of_preemption_point_is_not_empty:
      0 < size (job_preemption_points j).

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

1 subgoal (ID 1552)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  0 < size (job_preemption_points j)

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

    Proof.
      move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].

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

1 subgoal (ID 1575)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  0 < size (job_preemption_points j)

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

      apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; rewrite size_eq0 in CONTR.

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

1 subgoal (ID 1706)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  CONTR : job_preemption_points j == [::]
  ============================
  False

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

      specialize (BEG j H_j_arrives).

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

1 subgoal (ID 1708)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : 0 \in job_preemption_points j
  END : end_of_execution_in_preemption_points arr_seq
  CONTR : job_preemption_points j == [::]
  ============================
  False

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

        by rewrite /beginning_of_execution_in_preemption_points (eqbool_to_eqprop CONTR) in BEG.

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

No more subgoals.

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

    Qed.

Next, we prove that the cost of a job is a preemption point.
    Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.

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

1 subgoal (ID 1561)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost j \in job_preemption_points j

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

    Proof.
      move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].

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

1 subgoal (ID 1584)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  job_cost j \in job_preemption_points j

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

      move: (END _ H_j_arrives) ⇒ EQ.

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

1 subgoal (ID 1588)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  EQ : last0 (job_preemption_points j) = job_cost j
  ============================
  job_cost j \in job_preemption_points j

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

      rewrite -EQ; clear EQ.

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

1 subgoal (ID 1591)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  last0 (job_preemption_points j) \in job_preemption_points j

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

      rewrite /last0 -nth_last.

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

1 subgoal (ID 1597)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  nth 0 (job_preemption_points j) (predn (size (job_preemption_points j)))
    \in job_preemption_points j

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

      apply/(nthP 0).

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

1 focused subgoal
(shelved: 1) (ID 1625)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  exists2 i : nat,
    i < size (job_preemption_points j) &
    nth 0 (job_preemption_points j) i =
    nth 0 (job_preemption_points j) (predn (size (job_preemption_points j)))

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

      ∃ ((size (job_preemption_points j)).-1); last by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1630)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  predn (size (job_preemption_points j)) < size (job_preemption_points j)

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

      rewrite -(leq_add2r 1) !addn1 prednK //.

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

1 subgoal (ID 1647)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  0 < size (job_preemption_points j)

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

        by apply list_of_preemption_point_is_not_empty.

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

No more subgoals.

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

    Qed.

As a corollary, we prove that the sequence of non-preemptive points of a job with positive cost contains at least 2 points.
    Corollary number_of_preemption_points_at_least_two:
      job_cost_positive j →
      2 ≤ size (job_preemption_points j).

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

1 subgoal (ID 1567)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  job_cost_positive j -> 1 < size (job_preemption_points j)

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

    Proof.
      intros POS.

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

1 subgoal (ID 1568)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  ============================
  1 < size (job_preemption_points j)

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

      move: H_valid_limited_preemptions_job_model ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1591)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  1 < size (job_preemption_points j)

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

      have EQ: 2 = size [::0; job_cost j]; first by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1602)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  EQ : 2 = size [:: 0; job_cost j]
  ============================
  1 < size (job_preemption_points j)

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

      rewrite EQ; clear EQ.

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

1 subgoal (ID 1605)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  size [:: 0; job_cost j] <= size (job_preemption_points j)

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

      apply subseq_leq_size.

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

2 subgoals (ID 1607)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  uniq [:: 0; job_cost j]

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

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

      rewrite !cons_uniq.

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

2 subgoals (ID 1618)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  [&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]

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

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

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

1 subgoal (ID 1618)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  [&& 0 \notin [:: job_cost j], job_cost j \notin [::] & uniq [::]]

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

apply/andP; split.

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

2 subgoals (ID 1647)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  0 \notin [:: job_cost j]

subgoal 2 (ID 1648) is:
 (job_cost j \notin [::]) && uniq [::]

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

        rewrite in_cons negb_or; apply/andP; split; last by done.

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

2 subgoals (ID 1684)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  0 != job_cost j

subgoal 2 (ID 1648) is:
 (job_cost j \notin [::]) && uniq [::]

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

        rewrite neq_ltn; apply/orP; left; eauto 2.

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

1 subgoal (ID 1648)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  (job_cost j \notin [::]) && uniq [::]

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

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

1 subgoal (ID 1608)

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

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

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

1 subgoal (ID 1608)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  ============================
  forall x : nat_eqType,
  x \in [:: 0; job_cost j] -> x \in job_preemption_points j

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


      intros t EQ; move: EQ; rewrite !in_cons.

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

1 subgoal (ID 1763)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  t : nat_eqType
  ============================
  [|| t == 0, t == job_cost j | t \in [::]] -> t \in job_preemption_points j

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

      move ⇒ /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.

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

2 subgoals (ID 1915)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  t : nat_eqType
  EQ : t = 0
  ============================
  t \in job_preemption_points j

subgoal 2 (ID 1916) is:
 t \in job_preemption_points j

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

      - by rewrite EQ; apply zero_in_preemption_points.

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

1 subgoal (ID 1916)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  POS : job_cost_positive j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  t : nat_eqType
  EQ : t = job_cost j
  ============================
  t \in job_preemption_points j

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

      - by rewrite EQ; apply job_cost_in_nonpreemptive_points.

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

No more subgoals.

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

    Qed.

Next we prove that "anti-density" property (from [preemption.util] file) holds for [job_preemption_point j].
    Lemma antidensity_of_preemption_points:
      ∀ (ρ : work),
        ρ ≤ job_cost j →
        ~~ (ρ \in job_preemption_points j) →
        first0 (job_preemption_points j) ≤ ρ < last0 (job_preemption_points j).
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1580)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  forall ρ : work,
  ρ <= job_cost j ->
  ρ \notin job_preemption_points j ->
  first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)

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

    Proof.
      intros ρ LE NotIN.

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

1 subgoal (ID 1583)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  ============================
  first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)

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

      move: H_valid_limited_preemptions_job_model ⇒ [BEG [END NDEC]].

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

1 subgoal (ID 1605)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j)

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

      apply/andP; split.

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

2 subgoals (ID 1631)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  first0 (job_preemption_points j) <= ρ

subgoal 2 (ID 1632) is:
 ρ < last0 (job_preemption_points j)

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

      - by rewrite zero_is_first_element.

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

1 subgoal (ID 1632)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  ρ < last0 (job_preemption_points j)

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

      - rewrite END; last by done.

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

1 subgoal (ID 1640)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  ρ < job_cost j

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

        rewrite ltn_neqAle; apply/andP; split; last by done.

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

1 subgoal (ID 1671)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  ρ != job_cost j

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

        apply/negP; intros CONTR; move: CONTR ⇒ /eqP CONTR.

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

1 subgoal (ID 1730)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  CONTR : ρ = job_cost j
  ============================
  False

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

        rewrite CONTR in NotIN.

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

1 subgoal (ID 1760)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  CONTR : ρ = job_cost j
  NotIN : job_cost j \notin job_preemption_points j
  ============================
  False

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

        move: NotIN ⇒ /negP NIN; apply: NIN.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1794)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  BEG : beginning_of_execution_in_preemption_points arr_seq
  END : end_of_execution_in_preemption_points arr_seq
  NDEC : preemption_points_is_nondecreasing_sequence arr_seq
  CONTR : ρ = job_cost j
  ============================
  job_cost j \in job_preemption_points j

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

          by apply job_cost_in_nonpreemptive_points.

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

No more subgoals.

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

    Qed.

We also prove that any work that doesn't belong to preemption points of job j is placed strictly between two neighboring preemption points.
    Lemma work_belongs_to_some_nonpreemptive_segment:
      ∀ (ρ : work),
        ρ ≤ job_cost j →
        ~~ (ρ \in job_preemption_points j)→
        ∃ n,
          n.+1 < size (job_preemption_points j) ∧
          nth 0 (job_preemption_points j) n < ρ < nth 0 (job_preemption_points j) n.+1.

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

1 subgoal (ID 1600)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  forall ρ : work,
  ρ <= job_cost j ->
  ρ \notin job_preemption_points j ->
  exists n : nat,
    succn n < size (job_preemption_points j) /\
    nth 0 (job_preemption_points j) n < ρ <
    nth 0 (job_preemption_points j) (succn n)

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

    Proof.
      intros ρ LE NotIN.

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

1 subgoal (ID 1603)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  ============================
  exists n : nat,
    succn n < size (job_preemption_points j) /\
    nth 0 (job_preemption_points j) n < ρ <
    nth 0 (job_preemption_points j) (succn n)

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

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

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

2 subgoals (ID 1626)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  ZERO : job_cost j = 0
  ============================
  exists n : nat,
    succn n < size (job_preemption_points j) /\
    nth 0 (job_preemption_points j) n < ρ <
    nth 0 (job_preemption_points j) (succn n)

subgoal 2 (ID 1627) is:
 exists n : nat,
   succn n < size (job_preemption_points j) /\
   nth 0 (job_preemption_points j) n < ρ <
   nth 0 (job_preemption_points j) (succn n)

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

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

1 subgoal (ID 1626)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  ZERO : job_cost j = 0
  ============================
  exists n : nat,
    succn n < size (job_preemption_points j) /\
    nth 0 (job_preemption_points j) n < ρ <
    nth 0 (job_preemption_points j) (succn n)

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

exfalso; move: NotIN ⇒ /negP NIN; apply: NIN.

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

1 subgoal (ID 1662)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  ZERO : job_cost j = 0
  ============================
  ρ \in job_preemption_points j

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

        move: LE.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1664)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  ZERO : job_cost j = 0
  ============================
  ρ <= job_cost j -> ρ \in job_preemption_points j

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

rewrite ZERO leqn0; move ⇒ /eqP →.

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

1 subgoal (ID 1706)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  ZERO : job_cost j = 0
  ============================
  0 \in job_preemption_points j

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

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

1 subgoal (ID 1627)

subgoal 1 (ID 1627) is:
 exists n : nat,
   succn n < size (job_preemption_points j) /\
   nth 0 (job_preemption_points j) n < ρ <
   nth 0 (job_preemption_points j) (succn n)

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

}

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

1 subgoal (ID 1627)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  POS : 0 < job_cost j
  ============================
  exists n : nat,
    succn n < size (job_preemption_points j) /\
    nth 0 (job_preemption_points j) n < ρ <
    nth 0 (job_preemption_points j) (succn n)

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

      move: (belonging_to_segment_of_seq_is_total
               (job_preemption_points j) ρ (number_of_preemption_points_at_least_two POS)
               (antidensity_of_preemption_points _ LE NotIN)) ⇒ [n [SIZE2 /andP [N1 N2]]].

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

1 subgoal (ID 1771)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) n <= ρ
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  ============================
  exists n0 : nat,
    succn n0 < size (job_preemption_points j) /\
    nth 0 (job_preemption_points j) n0 < ρ <
    nth 0 (job_preemption_points j) (succn n0)

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

      ∃ n; split; first by done.

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

1 subgoal (ID 1776)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) n <= ρ
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  ============================
  nth 0 (job_preemption_points j) n < ρ <
  nth 0 (job_preemption_points j) (succn n)

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

      apply/andP; split; last by done.

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

1 subgoal (ID 1802)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N1 : nth 0 (job_preemption_points j) n <= ρ
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  ============================
  nth 0 (job_preemption_points j) n < ρ

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

      move: N1; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | G]; last by done.

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

1 subgoal (ID 1884)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  EQ : nth 0 (job_preemption_points j) n = ρ
  ============================
  nth 0 (job_preemption_points j) n < ρ

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

      exfalso.

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

1 subgoal (ID 1886)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  NotIN : ρ \notin job_preemption_points j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  EQ : nth 0 (job_preemption_points j) n = ρ
  ============================
  False

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

      move: NotIN ⇒ /negP CONTR; apply: CONTR.

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

1 subgoal (ID 1920)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  EQ : nth 0 (job_preemption_points j) n = ρ
  ============================
  ρ \in job_preemption_points j

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

      rewrite -EQ; clear EQ.

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

1 subgoal (ID 1923)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  ============================
  nth 0 (job_preemption_points j) n \in job_preemption_points j

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

      rewrite mem_nth //.

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

1 subgoal (ID 1931)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ρ : work
  LE : ρ <= job_cost j
  POS : 0 < job_cost j
  n : nat
  SIZE2 : succn n < size (job_preemption_points j)
  N2 : ρ < nth 0 (job_preemption_points j) (succn n)
  ============================
  n < size (job_preemption_points j)

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

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

No more subgoals.

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

    Qed.

Recall that file [job.parameters] also defines notion of preemption points. And note that [job.parameter.job_preemption_points] cannot have a duplicating preemption points. Therefore, we need additional lemmas to relate [job.parameter.job_preemption_points] and [limited.job_preemption_points]].
First we show that the length of the last non-preemptive segment of [job.parameter.job_preemption_points] is equal to the length of the last non-empty non-preemptive segment of [limited.job_preemption_points].
    Lemma job_parameters_last_np_to_job_limited:
        last0 (distances (parameter.job_preemption_points j)) =
        last0 (filter (fun x ⇒ 0 < x) (distances (job_preemption_points j))).

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

1 subgoal (ID 1611)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  last0 (distances (parameter.job_preemption_points j)) =
  last0 [seq x <- distances (job_preemption_points j) | 0 < x]

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

    Proof.
      destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].

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

1 subgoal (ID 1621)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  last0 (distances (parameter.job_preemption_points j)) =
  last0 [seq x <- distances (job_preemption_points j) | 0 < x]

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

      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.

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

1 subgoal (ID 1623)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  last0
    (distances
       [seq ρ <- range 0 (job_cost j) | ρ \in job_preemption_points j]) =
  last0 [seq x <- distances (job_preemption_points j) | 0 < x]

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

      intros; rewrite distances_iota_filtered; eauto.

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

1 subgoal (ID 1630)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  forall x : nat, x \in job_preemption_points j -> x <= job_cost j

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

      rewrite -A2 //.

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

1 subgoal (ID 6695)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  forall x : nat,
  x \in job_preemption_points j -> x <= last0 (job_preemption_points j)

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

        by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.

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

No more subgoals.

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

    Qed.

Next we show that the length of the max non-preemptive segment of [job.parameter.job_preemption_points] is equal to the length of the max non-preemptive segment of [limited.job_preemption_points].
    Lemma job_parameters_max_np_to_job_limited:
      max0 (distances (parameter.job_preemption_points j)) =
      max0 (distances (job_preemption_points j)).

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

1 subgoal (ID 1620)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  ============================
  max0 (distances (parameter.job_preemption_points j)) =
  max0 (distances (job_preemption_points j))

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

    Proof.
      destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].

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

1 subgoal (ID 1630)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  max0 (distances (parameter.job_preemption_points j)) =
  max0 (distances (job_preemption_points j))

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

      unfold parameter.job_preemption_points, job_preemptable, limited_preemptions_model.

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

1 subgoal (ID 1632)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  max0
    (distances
       [seq ρ <- range 0 (job_cost j) | ρ \in job_preemption_points j]) =
  max0 (distances (job_preemption_points j))

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

      intros; rewrite distances_iota_filtered; eauto 2.

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

2 subgoals (ID 1638)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  max0 [seq x <- distances (job_preemption_points j) | 0 < x] =
  max0 (distances (job_preemption_points j))

subgoal 2 (ID 1639) is:
 forall x : nat, x \in job_preemption_points j -> x <= job_cost j

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

      rewrite max0_rem0 //.

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

1 subgoal (ID 1639)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  forall x : nat, x \in job_preemption_points j -> x <= job_cost j

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

      rewrite -A2 //.

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

1 subgoal (ID 1682)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  H_j_arrives : arrives_in arr_seq j
  A1 : beginning_of_execution_in_preemption_points arr_seq
  A2 : end_of_execution_in_preemption_points arr_seq
  A3 : preemption_points_is_nondecreasing_sequence arr_seq
  ============================
  forall x : nat,
  x \in job_preemption_points j -> x <= last0 (job_preemption_points j)

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

        by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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


    Qed.

  End AuxiliaryLemmas.

We prove that the [fixed_preemption_point_model] function defines a valid preemption model.
  Lemma valid_fixed_preemption_points_model_lemma:
    valid_preemption_model arr_seq sched.

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

1 subgoal (ID 1542)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  ============================
  valid_preemption_model arr_seq sched

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

  Proof.
    intros j ARR; repeat split.
(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 1547)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  job_cannot_become_nonpreemptive_before_execution j

subgoal 2 (ID 1551) is:
 job_cannot_be_nonpreemptive_after_completion j
subgoal 3 (ID 1555) is:
 not_preemptive_implies_scheduled sched j
subgoal 4 (ID 1556) is:
 execution_starts_with_preemption_point sched j

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

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

1 subgoal (ID 1547)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  job_cannot_become_nonpreemptive_before_execution j

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

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

3 subgoals (ID 1551)

subgoal 1 (ID 1551) is:
 job_cannot_be_nonpreemptive_after_completion j
subgoal 2 (ID 1555) is:
 not_preemptive_implies_scheduled sched j
subgoal 3 (ID 1556) is:
 execution_starts_with_preemption_point sched j

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

}

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

3 subgoals (ID 1551)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  job_cannot_be_nonpreemptive_after_completion j

subgoal 2 (ID 1555) is:
 not_preemptive_implies_scheduled sched j
subgoal 3 (ID 1556) is:
 execution_starts_with_preemption_point sched j

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

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

1 subgoal (ID 1551)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  job_cannot_be_nonpreemptive_after_completion j

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

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

2 subgoals (ID 1555)

subgoal 1 (ID 1555) is:
 not_preemptive_implies_scheduled sched j
subgoal 2 (ID 1556) is:
 execution_starts_with_preemption_point sched j

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

}

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

2 subgoals (ID 1555)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  not_preemptive_implies_scheduled sched j

subgoal 2 (ID 1556) is:
 execution_starts_with_preemption_point sched j

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

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

1 subgoal (ID 1555)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  not_preemptive_implies_scheduled sched j

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

by move ⇒ t NPP; apply H_schedule_respects_preemption_model.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1556)

subgoal 1 (ID 1556) is:
 execution_starts_with_preemption_point sched j

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

}

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

1 subgoal (ID 1556)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  execution_starts_with_preemption_point sched j

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

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

1 subgoal (ID 1556)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  ============================
  execution_starts_with_preemption_point sched j

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

intros t NSCHED SCHED.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1574)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  ============================
  job_preemptable j (service sched j (succn t))

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

      have SERV: service sched j t = service sched j t.+1.

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

2 subgoals (ID 1583)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  ============================
  service sched j t = service sched j (succn t)

subgoal 2 (ID 1585) is:
 job_preemptable j (service sched j (succn t))

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

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

1 subgoal (ID 1583)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  ============================
  service sched j t = service sched j (succn t)

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

rewrite -[service sched j t]addn0 /service /service_during; apply/eqP.
(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 1662)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  ============================
  \sum_(0 <= t0 < t) service_at sched j t0 + 0 ==
  \sum_(0 <= t0 < succn t) service_at sched j t0

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

        rewrite big_nat_recr //=.

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

1 subgoal (ID 1673)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  ============================
  \sum_(0 <= t0 < t) (sched t0 == Some j) + 0 ==
  \sum_(0 <= i < t) (sched i == Some j) + (sched t == Some j)

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

        rewrite eqn_add2l eq_sym.

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

1 subgoal (ID 1706)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  ============================
  (sched t == Some j) == 0

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

        rewrite scheduled_at_def in NSCHED.

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

1 subgoal (ID 1737)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j (succn t)
  NSCHED : sched t != Some j
  ============================
  (sched t == Some j) == 0

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

          by rewrite eqb0.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1585)

subgoal 1 (ID 1585) is:
 job_preemptable j (service sched j (succn t))

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

}

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

1 subgoal (ID 1585)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  SERV : service sched j t = service sched j (succn t)
  ============================
  job_preemptable j (service sched j (succn t))

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

      rewrite -[job_preemptable _ _]Bool.negb_involutive.

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

1 subgoal (ID 1747)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  SERV : service sched j t = service sched j (succn t)
  ============================
  ~~ ~~ job_preemptable j (service sched j (succn t))

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

      apply/negP; intros CONTR.

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

1 subgoal (ID 1769)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j (succn t)
  SERV : service sched j t = service sched j (succn t)
  CONTR : ~~ job_preemptable j (service sched j (succn t))
  ============================
  False

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

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

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

1 subgoal (ID 1803)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j (succn t)
  SERV : service sched j t = service sched j (succn t)
  CONTR : ~~ job_preemptable j (service sched j (succn t))
  ============================
  scheduled_at sched j t

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

      apply H_schedule_respects_preemption_model; first by done.

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

1 subgoal (ID 1805)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  H2 : JobCost Job
  H3 : JobPreemptionPoints Job
  arr_seq : arrival_sequence Job
  sched : schedule (ideal.processor_state Job)
  H_schedule_respects_preemption_model : schedule_respects_preemption_model
                                           arr_seq sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
                                            arr_seq
  j : Job
  ARR : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j (succn t)
  SERV : service sched j t = service sched j (succn t)
  CONTR : ~~ job_preemptable j (service sched j (succn t))
  ============================
  ~~ job_preemptable j (service sched j t)

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

        by rewrite SERV.

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

No more subgoals.

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

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

No more subgoals.

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

           
  Qed.

End ModelWithLimitedPreemptions.
Hint Resolve valid_fixed_preemption_points_model_lemma : basic_facts.