Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** * RTA for FP-schedulers with Bounded Non-Preemptive Segments *) (** In this section we instantiate the Abstract RTA for FP-schedulers with Bounded Priority Inversion to FP-schedulers for ideal uni-processor model of real-time tasks with arbitrary arrival models _and_ bounded non-preemptive segments. *) (** Recall that Abstract RTA for FP-schedulers with Bounded Priority Inversion does not specify the cause of priority inversion. In this section, we prove that the priority inversion caused by execution of non-preemptive segments is bounded. Thus the Abstract RTA for FP-schedulers is applicable to this instantiation. *) Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves. (** Consider any type of tasks ... *) Context {Task : TaskType}. Context `{TaskCost Task}. Context `{TaskRunToCompletionThreshold Task}. Context `{TaskMaxNonpreemptiveSegment Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{Arrival : JobArrival Job}. Context `{Cost : JobCost Job}. (** Consider an FP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive. *) Context {FP : FP_policy Task}. Hypothesis H_priority_is_reflexive : reflexive_priorities. Hypothesis H_priority_is_transitive : transitive_priorities. (** Consider any arrival sequence with consistent, non-duplicate arrivals. *) Variable arr_seq : arrival_sequence Job. Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq. Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq. (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *) Variable sched : schedule (ideal.processor_state Job). (** ... allow for any work-bearing notion of job readiness, ... *) Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}. Hypothesis H_job_ready : work_bearing_readiness arr_seq sched. (** ... and assume that the schedule is valid. *) Hypothesis H_sched_valid : valid_schedule sched arr_seq. (** In addition, we assume the existence of a function mapping jobs to their preemption points ... *) Context `{JobPreemptable Job}. (** ... and assume that it defines a valid preemption model with bounded non-preemptive segments. *) Hypothesis H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched. (** Next, we assume that the schedule is a work-conserving schedule... *) Hypothesis H_work_conserving : work_conserving arr_seq sched. (** ... and the schedule respects the policy defined by the [job_preemptable] function (i.e., jobs have bounded non-preemptive segments). *) Hypothesis H_respects_policy : respects_FP_policy_at_preemption_point arr_seq sched FP. (** Assume we have sequential tasks, i.e, jobs from the same task execute in the order of their arrival. *) Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched. (** Consider an arbitrary task set ts, ... *) Variable ts : list Task. (** ... assume that all jobs come from the task set, ... *) Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts. (** ... and the cost of a job cannot be larger than the task cost. *) Hypothesis H_valid_job_cost: arrivals_have_valid_job_costs arr_seq. (** Let max_arrivals be a family of valid arrival curves, i.e., for any task [tsk] in ts [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function that equals 0 for the empty interval delta = 0. *) Context `{MaxArrivals Task}. Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals. Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts. (** Let [tsk] be any task in ts that is to be analyzed. *) Variable tsk : Task. Hypothesis H_tsk_in_ts : tsk \in ts. (** Consider a valid preemption model... *) Hypothesis H_valid_preemption_model: valid_preemption_model arr_seq sched. (** ...and a valid task run-to-completion threshold function. That is, [task_rtct tsk] is (1) no bigger than [tsk]'s cost, (2) for any job of task [tsk] [job_rtct] is bounded by [task_rtct]. *) Hypothesis H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk. (** Let's define some local names for clarity. *) Let max_length_of_priority_inversion := max_length_of_priority_inversion arr_seq. Let task_rbf := task_request_bound_function tsk. Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk. Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk. Let response_time_bounded_by := task_response_time_bound arr_seq sched. (** We also define a bound for the priority inversion caused by jobs with lower priority. *) Definition blocking_bound := \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_max_nonpreemptive_segment tsk_other - ε). (** ** Priority inversion is bounded *) (** In this section, we prove that a priority inversion for task [tsk] is bounded by the maximum length of non-preemptive segments among the tasks with lower priority. *) Section PriorityInversionIsBounded. (** First, we prove that the maximum length of a priority inversion of a job j is bounded by the maximum length of a non-preemptive section of a task with lower-priority task (i.e., the blocking term). *)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop

forall (j : Job) (t : instant), arrives_in arr_seq j -> job_of_task tsk j -> max_length_of_priority_inversion j t <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop

forall (j : Job) (t : instant), arrives_in arr_seq j -> job_of_task tsk j -> max_length_of_priority_inversion j t <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

max_length_of_priority_inversion j t <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

\max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j && (0 < job_cost j_lp)) (job_max_nonpreemptive_segment j_lp - ε) <= \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_max_nonpreemptive_segment tsk_other - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

\max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j) (job_max_nonpreemptive_segment j_lp - ε) <= \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_max_nonpreemptive_segment tsk_other - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

\max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j) (job_max_nonpreemptive_segment j_lp - ε) <= \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk) (task_max_nonpreemptive_segment (job_task j_lp) - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk) (task_max_nonpreemptive_segment (job_task j_lp) - ε) <= \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_max_nonpreemptive_segment tsk_other - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

\max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j) (job_max_nonpreemptive_segment j_lp - ε) <= \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk) (task_max_nonpreemptive_segment (job_task j_lp) - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

\max_(j_lp <- arrivals_before arr_seq t | ~~ hep_task (job_task j_lp) tsk) (job_max_nonpreemptive_segment j_lp - ε) <= \max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk) (task_max_nonpreemptive_segment (job_task j_lp) - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk

job_max_nonpreemptive_segment j' - ε <= task_max_nonpreemptive_segment (job_task j') - ε
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk

job_max_nonpreemptive_segment j' <= task_max_nonpreemptive_segment (job_task j')
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk

arrives_in arr_seq j'
by eapply in_arrivals_implies_arrived; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

\max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk) (task_max_nonpreemptive_segment (job_task j_lp) - ε) <= \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_max_nonpreemptive_segment tsk_other - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk

\max_(j_lp <- arrivals_between arr_seq 0 t | ~~ hep_task (job_task j_lp) tsk) (task_max_nonpreemptive_segment (job_task j_lp) - ε) <= \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_max_nonpreemptive_segment tsk_other - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk

task_max_nonpreemptive_segment (job_task j') - ε <= \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_max_nonpreemptive_segment tsk_other - ε)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk

job_task j' \in ts
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
t: instant
ARR: arrives_in arr_seq j
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk

arrives_in arr_seq j'
by apply: in_arrivals_implies_arrived (JINB). } Qed. (** Using the above lemma, we prove that the priority inversion of the task is bounded by blocking_bound. *)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop

priority_inversion_is_bounded_by_constant arr_seq sched tsk blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop

priority_inversion_is_bounded_by_constant arr_seq sched tsk blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2

cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = true

cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = false
cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = true

cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = true

cumulative_priority_inversion sched j t1 t2 <= t2 - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = true

\sum_(t1 <= t < t2) match sched t with | Some jlp => ~~ hep_job jlp j | None => false end <= t2 - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = true

forall i : nat, true -> match sched i with | Some jlp => ~~ hep_job jlp j | None => false end <= 1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = true
t: nat

forall a : Job, ~~ hep_job a j <= 1
by intros s; case: (hep_job s j).
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
NEQ: (t2 - t1 <= blocking_bound) = false

cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1

cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
NEQ: t1 <= ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

cumulative_priority_inversion sched j t1 t2 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

ppt - t1 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 ppt <= ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

ppt - t1 <= blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 ppt <= ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

ppt <= t1 + blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 ppt <= ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

t1 + max_length_of_priority_inversion j t1 <= t1 + blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 ppt <= ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

cumulative_priority_inversion sched j t1 ppt <= ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

cumulative_priority_inversion sched j t1 ppt <= ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

\sum_(t1 <= t < ppt) match sched t with | Some jlp => ~~ hep_job jlp j | None => false end <= ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

\sum_(t1 <= t < ppt) match sched t with | Some jlp => ~~ hep_job jlp j | None => false end <= \sum_(t1 <= i < ppt) 1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat

forall a : Job, ~~ hep_job a j <= 1
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

cumulative_priority_inversion sched j t1 t2 <= cumulative_priority_inversion sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

\sum_(t1 <= t < t2) match sched t with | Some jlp => ~~ hep_job jlp j | None => false end <= \sum_(t1 <= t < ppt) match sched t with | Some jlp => ~~ hep_job jlp j | None => false end
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

ppt <= t2
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
\sum_(t1 <= i < ppt) match sched i with | Some jlp => ~~ hep_job jlp j | None => false end + \sum_(ppt <= i < t2) match sched i with | Some jlp => ~~ hep_job jlp j | None => false end <= \sum_(t1 <= t < ppt) match sched t with | Some jlp => ~~ hep_job jlp j | None => false end
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

ppt <= t2
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
BOUND: t1 + blocking_bound < t2

ppt <= t2
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
BOUND: t1 + blocking_bound < t2

ppt <= t1 + blocking_bound
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
BOUND: t1 + blocking_bound < t2

t1 + max_length_of_priority_inversion j t1 <= t1 + blocking_bound
rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

\sum_(t1 <= i < ppt) match sched i with | Some jlp => ~~ hep_job jlp j | None => false end + \sum_(ppt <= i < t2) match sched i with | Some jlp => ~~ hep_job jlp j | None => false end <= \sum_(t1 <= t < ppt) match sched t with | Some jlp => ~~ hep_job jlp j | None => false end
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1

\sum_(ppt <= i < t2) match sched i with | Some jlp => ~~ hep_job jlp j | None => false end == 0
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2

match sched t with | Some jlp => ~~ hep_job jlp j | None => false end = 0
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s

~~ hep_job s j = 0
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s

exists pr_t : instant, preemption_time sched pr_t /\ t1 <= pr_t <= t1 + (ppt - t1)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s
t1 + (ppt - t1) <= t < t2
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s
j_hp: Job
ARRB: arrived_between j_hp t1 t.+1
HP: hep_job j_hp j
SCHEDHP: scheduled_at sched j_hp t
~~ hep_job s j = 0
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s

exists pr_t : instant, preemption_time sched pr_t /\ t1 <= pr_t <= t1 + (ppt - t1)
by exists ppt; split; [done | rewrite subnKC //; apply/andP].
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s

t1 + (ppt - t1) <= t < t2
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s
j_hp: Job
ARRB: arrived_between j_hp t1 t.+1
HP: hep_job j_hp j
SCHEDHP: scheduled_at sched j_hp t
~~ hep_job s j = 0
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s

t1 + (ppt - t1) <= t < t2
by rewrite subnKC //; apply/andP; split.
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s
j_hp: Job
ARRB: arrived_between j_hp t1 t.+1
HP: hep_job j_hp j
SCHEDHP: scheduled_at sched j_hp t

~~ hep_job s j = 0
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s
j_hp: Job
ARRB: arrived_between j_hp t1 t.+1
HP: hep_job j_hp j
SCHEDHP: scheduled_at sched j_hp t

hep_job s j
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s
j_hp: Job
ARRB: arrived_between j_hp t1 t.+1
HP: hep_job j_hp j
SCHEDHP: scheduled_at sched j_hp t

s = j_hp
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
BOUND: blocking_bound < t2 - t1
ppt: instant
PPT: preemption_time sched ppt
GE: t1 <= ppt
LE: ppt <= t1 + priority_inversion.max_length_of_priority_inversion arr_seq j t1
t: nat
GEt: ppt <= t
LTt: t < t2
s: Job
SCHED: sched t = Some s
j_hp: Job
ARRB: arrived_between j_hp t1 t.+1
HP: hep_job j_hp j
SCHEDHP: scheduled_at sched j_hp t

scheduled_at sched s t
by rewrite scheduled_at_def SCHED. Qed. End PriorityInversionIsBounded. (** ** Response-Time Bound *) (** In this section, we prove that the maximum among the solutions of the response-time bound recurrence is a response-time bound for [tsk]. *) Section ResponseTimeBound. (** Let L be any positive fixed point of the busy interval recurrence. *) Variable L : duration. Hypothesis H_L_positive : L > 0. Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L. (** To reduce the time complexity of the analysis, recall the notion of search space. *) Let is_in_search_space := is_in_search_space tsk L. (** Next, consider any value R, and assume that for any given arrival offset A from the search space there is a solution of the response-time bound recurrence that is bounded by R. *) Variable R : duration. Hypothesis H_R_is_maximum: forall (A : duration), is_in_search_space A -> exists (F : duration), A + F >= blocking_bound + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + total_ohep_rbf (A + F) /\ F + (task_cost tsk - task_rtct tsk) <= R. (** Then, using the results for the general RTA for FP-schedulers, we establish a response-time bound for the more concrete model of bounded nonpreemptive segments. Note that in case of the general RTA for FP-schedulers, we just _assume_ that the priority inversion is bounded. In this module we provide the preemption model with bounded nonpreemptive segments and _prove_ that the priority inversion is bounded. *)
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
L: duration
H_L_positive: 0 < L
H_fixed_point: L = blocking_bound + total_hep_rbf L
is_in_search_space:= bounded_pi.is_in_search_space tsk L: nat -> bool
R: duration
H_R_is_maximum: forall A : duration, is_in_search_space A -> exists F : duration, blocking_bound + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + total_ohep_rbf (A + F) <= A + F /\ F + (task_cost tsk - task_rtct tsk) <= R

response_time_bounded_by tsk R
Task: TaskType
H: TaskCost Task
H0: TaskRunToCompletionThreshold Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
FP: FP_policy Task
H_priority_is_reflexive: reflexive_priorities
H_priority_is_transitive: transitive_priorities
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments arr_seq sched
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_FP_policy_at_preemption_point arr_seq sched FP
H_sequential_tasks: sequential_tasks arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H5: MaxArrivals Task
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_valid_run_to_completion_threshold: valid_task_run_to_completion_threshold arr_seq tsk
max_length_of_priority_inversion:= priority_inversion.max_length_of_priority_inversion arr_seq: Job -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_hep_rbf:= total_hep_request_bound_function_FP ts tsk: duration -> nat
total_ohep_rbf:= total_ohep_request_bound_function_FP ts tsk: duration -> nat
response_time_bounded_by:= task_response_time_bound arr_seq sched: Task -> duration -> Prop
L: duration
H_L_positive: 0 < L
H_fixed_point: L = blocking_bound + total_hep_rbf L
is_in_search_space:= bounded_pi.is_in_search_space tsk L: nat -> bool
R: duration
H_R_is_maximum: forall A : duration, is_in_search_space A -> exists F : duration, blocking_bound + (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + total_ohep_rbf (A + F) <= A + F /\ F + (task_cost tsk - task_rtct tsk) <= R

response_time_bounded_by tsk R
eapply uniprocessor_response_time_bound_fp; eauto using priority_inversion_is_bounded with basic_rt_facts. Qed. End ResponseTimeBound. End RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.