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]
(** * Facts about Request Bound Functions (RBFs) *) (** In this file, we prove some lemmas about request bound functions. *) (** ** RBF is a Bound on Workload *) (** First, we show that a task's RBF is indeed an upper bound on its workload. *) Section ProofWorkloadBound. (** Consider any type of tasks ... *) Context {Task : TaskType}. Context `{TaskCost Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. Context `{JobCost Job}. (** 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. (** ... any schedule corresponding to this arrival sequence, ... *) Context {PState : ProcessorState Job}. Variable sched : schedule PState. Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq. (** ... and an FP policy that indicates a higher-or-equal priority relation. *) Context `{FP_policy Task}. Let jlfp_higher_eq_priority := FP_to_JLFP Job Task. (** Further, consider a task set [ts]... *) Variable ts : list Task. (** ... and let [tsk] be any task in [ts]. *) Variable tsk : Task. Hypothesis H_tsk_in_ts : tsk \in ts. (** Assume that the job costs are no larger than the task costs ... *) Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq. (** ... and that all jobs come from the task set. *) Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts. (** Let [max_arrivals] be any arrival bound for task-set [ts]. *) Context `{MaxArrivals Task}. Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts. (** Next, recall the notions of total workload of jobs... *) Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between arr_seq t1 t2). (** ... and the workload of jobs of the same task as job j. *) Let task_workload t1 t2 := workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2). (** Finally, let us define some local names for clarity. *) Let task_rbf := task_request_bound_function tsk. Let total_rbf := total_request_bound_function ts. Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk. Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk. (** In this section, we prove that the workload of all jobs is no larger than the request bound function. *) Section WorkloadIsBoundedByRBF. (** Consider any time [t] and any interval of length [Δ]. *) Variable t : instant. Variable Δ : instant. (** First, we show that workload of task [tsk] is bounded by the number of arrivals of the task times the cost of the task. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

task_workload t (t + Δ) <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + Δ)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

task_workload t (t + Δ) <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + Δ)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk i) job_cost i <= \big[addn_addoid/0]_(i <- [seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j]) muln_muloid (task_cost tsk) 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = [::]

\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk i) job_cost i <= \big[addn_addoid/0]_(i <- [seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j]) muln_muloid (task_cost tsk) 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l
\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk i) job_cost i <= \big[addn_addoid/0]_(i <- [ seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j]) muln_muloid (task_cost tsk) 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = [::]

\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk i) job_cost i <= \big[addn_addoid/0]_(i <- [seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j]) muln_muloid (task_cost tsk) 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
TASK: [seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j] = [::]

\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk i) job_cost i <= \big[addn_addoid/0]_(i <- [seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j]) muln_muloid (task_cost tsk) 1
by rewrite -big_filter !TASK !big_nil.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l

\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk i) job_cost i <= \big[addn_addoid/0]_(i <- [seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j]) muln_muloid (task_cost tsk) 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l

\sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk i) job_cost i <= \big[addn_addoid/0]_(i <- [seq j <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk j]) muln_muloid (task_cost tsk) 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l

\sum_(i <- arrivals_between arr_seq t (t + Δ) | (i \in arrivals_between arr_seq t (t + Δ)) && job_of_task tsk i) job_cost i <= \sum_(i <- arrivals_between arr_seq t (t + Δ) | (i \in arrivals_between arr_seq t (t + Δ)) && job_of_task tsk i) task_cost tsk * 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l

forall i : Job, (i \in arrivals_between arr_seq t (t + Δ)) && job_of_task tsk i -> job_cost i <= task_cost tsk * 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l
j': Job
IN: j' \in arrivals_between arr_seq t (t + Δ)
TSKj': job_of_task tsk j'

job_cost j' <= task_cost tsk * 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l
j': Job
IN: j' \in arrivals_between arr_seq t (t + Δ)
TSKj': job_of_task tsk j'

job_cost j' <= task_cost tsk
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l
j': Job
IN: j' \in arrivals_between arr_seq t (t + Δ)
TSKj': job_task j' = tsk

job_cost j' <= task_cost (job_task j')
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
s: Job
l: seq Job
TASK: task_arrivals_between arr_seq tsk t (t + Δ) = s :: l
j': Job
IN: j' \in arrivals_between arr_seq t (t + Δ)
TSKj': job_task j' = tsk

arrives_in arr_seq j'
by apply in_arrivals_implies_arrived in IN. } Qed. (** As a corollary, we prove that workload of task is no larger the than task request bound function. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

task_workload t (t + Δ) <= task_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

task_workload t (t + Δ) <= task_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + Δ) <= task_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

number_of_task_arrivals arr_seq tsk t (t + Δ) <= max_arrivals tsk Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

number_of_task_arrivals arr_seq tsk t (t + Δ) <= max_arrivals tsk (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr. Qed. (** Next, we prove that total workload of tasks is no larger than the total request bound function. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

total_workload t (t + Δ) <= total_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant

total_workload t (t + Δ) <= total_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_workload t (t + Δ) <= total_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_workload t (t + Δ) <= \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
\sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= total_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_workload t (t + Δ) <= \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job

workload_of_jobs predT (arrivals_between arr_seq t (t + Δ)) <= \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
EXCHANGE: forall (T : Type) (y : T) (c : Monoid.com_law y) (T0 T1 : Type) (l : seq T0) (l0 : seq T1) (p : pred T0) (p0 : T0 -> pred T1) (F : T0 -> T1 -> T), (forall (i : T0) (j : T1), p i -> p0 i j -> predT j) -> \big[c/y]_(i <- l | p i) \big[c/y]_(j <- l0 | p0 i j) F i j = \big[c/y]_(j <- l0 | predT j) \big[c/y]_(i <- l | p i && p0 i j) F i j

workload_of_jobs predT (arrivals_between arr_seq t (t + Δ)) <= \sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job

workload_of_jobs predT (arrivals_between arr_seq t (t + Δ)) <= \sum_(j <- l) \sum_(i <- ts | job_task j == i) job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job

\sum_(i <- l | (i \in l) && predT i) job_cost i <= \sum_(i <- l | (i \in l) && true) \sum_(i0 <- ts | job_task i == i0) job_cost i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
j0: Job
IN0: j0 \in l
HP0: true

job_cost j0 <= \sum_(i <- ts | job_task j0 == i) job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
j0: Job
IN0: j0 \in l
HP0: true

job_cost j0 <= (if job_task j0 == job_task j0 then job_cost j0 else 0) + \sum_(y <- rem (T:=Task) (job_task j0) ts) (if job_task j0 == y then job_cost j0 else 0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
j0: Job
IN0: j0 \in l
HP0: true
job_task j0 \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
j0: Job
IN0: j0 \in l
HP0: true

job_task j0 \in ts
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job

\sum_(tsk' <- ts) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= total_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true
task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= \sum_(i <- l | job_of_task tsk0 i) task_cost tsk0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true
j0: Job
IN0: j0 \in l

job_cost j0 <= task_cost (job_task j0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true
j0: Job
IN0: j0 \in l

arrives_in arr_seq j0
by apply in_arrivals_implies_arrived in IN0.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= max_arrivals tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: true

size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= max_arrivals tsk0 (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr. } Qed. (** Next, we consider any job [j] of [tsk]. *) Variable j : Job. Hypothesis H_j_arrives : arrives_in arr_seq j. Hypothesis H_job_of_tsk : job_of_task tsk j. (** We say that two jobs [j1] and [j2] are in relation [other_higher_eq_priority], iff [j1] has higher or equal priority than [j2] and is produced by a different task. *) Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2). (** Recall the notion of workload of higher or equal priority jobs... *) Let total_hep_workload t1 t2 := workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2). (** ... and workload of other higher or equal priority jobs. *) Let total_ohep_workload t1 t2 := workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between arr_seq t1 t2). (** We prove that total workload of other tasks with higher-or-equal priority is no larger than the total request bound function. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat

total_ohep_workload t (t + Δ) <= total_ohep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat

total_ohep_workload t (t + Δ) <= total_ohep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_ohep_workload t (t + Δ) <= total_ohep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_ohep_workload t (t + Δ) <= \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= total_ohep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_ohep_workload t (t + Δ) <= \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk

total_ohep_workload t (t + Δ) <= \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk

\sum_(j0 <- arrivals_between arr_seq t (t + Δ) | jlfp_higher_eq_priority j0 j && ~~ same_task j0 j) job_cost j0 <= \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk

\sum_(j <- arrivals_between arr_seq t (t + Δ) | hep_task (job_task j) tsk && (job_task j != tsk)) job_cost j <= \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool

\sum_(j <- arrivals_between arr_seq t (t + Δ) | hep_task (job_task j) tsk && (job_task j != tsk)) job_cost j <= \sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool

\sum_(j <- arrivals_between arr_seq t (t + Δ) | hep_task (job_task j) tsk && (job_task j != tsk)) job_cost j <= \sum_(j <- l | P j) \sum_(i <- ts | hep_task i tsk && (i != tsk) && (job_task j == i)) job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool

\sum_(i <- l | [&& i \in l, hep_task (job_task i) tsk & job_task i != tsk]) job_cost i <= \sum_(i <- l | [&& i \in l, hep_task (job_task i) tsk & job_task i != tsk]) \sum_(i0 <- ts | hep_task i0 tsk && (i0 != tsk) && (job_task i == i0)) job_cost i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk && (job_task j0 != tsk)

job_cost j0 <= \sum_(i <- ts | hep_task i tsk && (i != tsk) && (job_task j0 == i)) job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk && (job_task j0 != tsk)

job_cost j0 <= addn_comoid (if hep_task (job_task j0) tsk && (job_task j0 != tsk) && (job_task j0 == job_task j0) then job_cost j0 else 0) (\big[addn_comoid/0]_(y <- rem (T:=Task) (job_task j0) ts) (if hep_task y tsk && (y != tsk) && (job_task j0 == y) then job_cost j0 else 0))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk && (job_task j0 != tsk)
job_task j0 \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk && (job_task j0 != tsk)

job_cost j0 <= addn_comoid (if hep_task (job_task j0) tsk && (job_task j0 != tsk) && (job_task j0 == job_task j0) then job_cost j0 else 0) (\big[addn_comoid/0]_(y <- rem (T:=Task) (job_task j0) ts) (if hep_task y tsk && (y != tsk) && (job_task j0 == y) then job_cost j0 else 0))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk && (job_task j0 != tsk)
job_task j0 \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk && (job_task j0 != tsk)

job_task j0 \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
P:= fun x : Job => hep_task (job_task x) tsk && (job_task x != tsk): Job -> bool
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk && (job_task j0 != tsk)

job_task j0 \in ts
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk)) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= total_ohep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)
task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= \sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk0 i) task_cost tsk0 * 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

\sum_(j0 <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t | job_task j0 == tsk0) job_cost j0 <= \sum_(i <- \cat_(t<=t<t + Δ)arrivals_at arr_seq t | job_of_task tsk0 i) task_cost tsk0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)
j0: Job
IN0: j0 \in \cat_(t<=t<t + Δ)arrivals_at arr_seq t
EQ: job_task j0 = tsk0

job_cost j0 <= task_cost tsk0
by rewrite -EQ; apply H_valid_job_cost; apply in_arrivals_implies_arrived in IN0.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= max_arrivals tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk && (tsk0 != tsk)

size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= max_arrivals tsk0 (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr. } Qed. (** Next, we prove that total workload of all tasks with higher-or-equal priority is no larger than the total request bound function. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat

total_hep_workload t (t + Δ) <= total_hep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat

total_hep_workload t (t + Δ) <= total_hep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_hep_workload t (t + Δ) <= total_hep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_hep_workload t (t + Δ) <= \sum_(tsk' <- ts | hep_task tsk' tsk) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
\sum_(tsk' <- ts | hep_task tsk' tsk) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= total_hep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

total_hep_workload t (t + Δ) <= \sum_(tsk' <- ts | hep_task tsk' tsk) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk

total_hep_workload t (t + Δ) <= \sum_(tsk' <- ts | hep_task tsk' tsk) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk

workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk) (arrivals_between arr_seq t (t + Δ)) <= \sum_(tsk' <- ts | hep_task tsk' tsk) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
EXCHANGE: forall (T : Type) (y : T) (c : Monoid.com_law y) (T0 : Type) (j : JobType) (l : seq T0) (l0 : seq j) (p : pred T0) (p0 : T0 -> pred j) (f : FP_policy Task) (j0 : JobTask j Task) (F : T0 -> j -> T), (forall (i : T0) (j1 : j), p i -> p0 i j1 -> hep_task (job_task j1) tsk) -> \big[c/y]_(i <- l | p i) \big[c/y]_(j1 <- l0 | p0 i j1) F i j1 = \big[c/y]_(j1 <- l0 | hep_task (job_task j1) tsk) \big[c/y]_(i <- l | p i && p0 i j1) F i j1

workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk) (arrivals_between arr_seq t (t + Δ)) <= \sum_(tsk' <- ts | hep_task tsk' tsk) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk

workload_of_jobs (fun j_other : Job => hep_task (job_task j_other) tsk) (arrivals_between arr_seq t (t + Δ)) <= \sum_(j <- l | hep_task (job_task j) tsk) \sum_(i <- ts | hep_task i tsk && (job_task j == i)) job_cost j
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk

\sum_(i <- l | (i \in l) && hep_task (job_task i) tsk) job_cost i <= \sum_(i <- l | (i \in l) && hep_task (job_task i) tsk) \sum_(i0 <- ts | hep_task i0 tsk && (job_task i == i0)) job_cost i
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk

job_cost j0 <= \sum_(i <- ts | hep_task i tsk && (job_task j0 == i)) job_cost j0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk

job_cost j0 <= addn_comoid (if hep_task (job_task j0) tsk && (job_task j0 == job_task j0) then job_cost j0 else 0) (\big[addn_comoid/0]_(y <- rem (T:=Task) (job_task j0) ts) (if hep_task y tsk && (job_task j0 == y) then job_cost j0 else 0))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk
job_task j0 \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk

job_cost j0 <= addn_comoid (if hep_task (job_task j0) tsk && (job_task j0 == job_task j0) then job_cost j0 else 0) (\big[addn_comoid/0]_(y <- rem (T:=Task) (job_task j0) ts) (if hep_task y tsk && (job_task j0 == y) then job_cost j0 else 0))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk
job_task j0 \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk

job_task j0 \in ts
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
TSK: job_task j = tsk
j0: Job
IN0: j0 \in l
HP0: hep_task (job_task j0) tsk

job_task j0 \in ts
by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job

\sum_(tsk' <- ts | hep_task tsk' tsk) \sum_(j0 <- l | job_task j0 == tsk') job_cost j0 <= total_hep_rbf Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk
task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= \sum_(i <- arrivals_between arr_seq t (t + Δ) | job_of_task tsk0 i) task_cost tsk0 * 1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

\sum_(j0 <- l | job_task j0 == tsk0) job_cost j0 <= \sum_(i <- l | job_of_task tsk0 i) task_cost tsk0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk
j0: Job
IN0: j0 \in l

job_cost j0 <= task_cost (job_task j0)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk
j0: Job
IN0: j0 \in l

arrives_in arr_seq j0
by apply in_arrivals_implies_arrived in IN0.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= task_request_bound_function tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= max_arrivals tsk0 Δ
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
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
PState: ProcessorState Job
sched: schedule PState
H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq
H3: FP_policy Task
jlfp_higher_eq_priority:= Task H0 H3: JLFP_policy Job
ts: seq Task
tsk: Task
H_tsk_in_ts: tsk \in ts
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H4: MaxArrivals Task
H_is_arrival_bound: taskset_respects_max_arrivals arr_seq ts
total_workload:= fun t1 t2 : instant => workload_of_jobs predT (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_workload:= fun t1 t2 : instant => workload_of_jobs (job_of_task tsk) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
task_rbf:= task_request_bound_function tsk: duration -> nat
total_rbf:= total_request_bound_function ts: 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
t, Δ: instant
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
other_higher_eq_priority:= fun j1 j2 : Job => jlfp_higher_eq_priority j1 j2 && ~~ same_task j1 j2: Job -> Job -> bool
total_hep_workload:= fun t1 t2 : instant => workload_of_jobs (jlfp_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
total_ohep_workload:= fun t1 t2 : instant => workload_of_jobs (other_higher_eq_priority^~ j) (arrivals_between arr_seq t1 t2): instant -> instant -> nat
l:= arrivals_between arr_seq t (t + Δ): seq Job
tsk0: Task
INtsk0: tsk0 \in ts
HP0: hep_task tsk0 tsk

size (task_arrivals_between arr_seq tsk0 t (t + Δ)) <= max_arrivals tsk0 (t + Δ - t)
by apply H_is_arrival_bound; last rewrite leq_addr. } Qed. End WorkloadIsBoundedByRBF. End ProofWorkloadBound. (** ** RBF Properties *) (** In this section, we prove simple properties and identities of RBFs. *) Section RequestBoundFunctions. (** Consider any type of tasks ... *) Context {Task : TaskType}. Context `{TaskCost Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. (** Consider any arrival sequence. *) Variable arr_seq : arrival_sequence Job. Hypothesis H_arrival_times_are_consistent: consistent_arrival_times arr_seq. (** Let [tsk] be any task. *) Variable tsk : Task. (** 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 Δ = 0. *) Context `{MaxArrivals Task}. Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk). Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk). (** Let's define some local names for clarity. *) Let task_rbf := task_request_bound_function tsk. (** We prove that [task_rbf 0] is equal to [0]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat

task_rbf 0 = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat

task_rbf 0 = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat

task_cost tsk * max_arrivals tsk 0 = 0
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat

max_arrivals tsk 0 = 0
by move: H_valid_arrival_curve => [T1 T2]. Qed. (** We prove that [task_rbf] is monotone. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat

monotone leq task_rbf
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat

monotone leq task_rbf
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
x, y: nat
LE: x <= y

task_rbf x <= task_rbf y
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
x, y: nat
LE: x <= y

(task_cost tsk == 0) || (max_arrivals tsk x <= max_arrivals tsk y)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
x, y: nat
LE: x <= y

max_arrivals tsk x <= max_arrivals tsk y
by move: H_valid_arrival_curve => [_ T]; apply T. Qed. (** Consider any job [j] of [tsk]. This guarantees that there exists at least one job of task [tsk]. *) Variable j : Job. Hypothesis H_j_arrives : arrives_in arr_seq j. Hypothesis H_job_of_tsk : job_of_task tsk j. (** Then we prove that [task_rbf] at [ε] is greater than or equal to the task's WCET. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j

task_cost tsk <= task_rbf ε
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j

task_cost tsk <= task_rbf ε
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
ALT: forall n : nat, n = 0 \/ 0 < n

task_cost tsk <= task_rbf ε
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk

task_cost tsk <= task_rbf ε
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: task_rbf ε < task_cost tsk

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: task_rbf ε < task_cost tsk
ARRB: respects_max_arrivals arr_seq tsk (max_arrivals tsk)

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: task_rbf ε < task_cost tsk
ARRB: job_arrival j <= job_arrival j + ε -> number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + ε) <= max_arrivals tsk (job_arrival j + ε - job_arrival j)

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: task_rbf ε < task_cost tsk
ARRB: number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + ε) <= max_arrivals tsk (job_arrival j + ε - job_arrival j)

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
ARRB: number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + ε) <= max_arrivals tsk (job_arrival j + ε - job_arrival j)

task_cost tsk * max_arrivals tsk ε < task_cost tsk -> False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
ARRB: number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + ε) <= max_arrivals tsk (job_arrival j + ε - job_arrival j)
CONTR: max_arrivals tsk ε < 1

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
ARRB: number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + ε) <= max_arrivals tsk (job_arrival j + ε - job_arrival j)
CONTR: max_arrivals tsk ε = 0

False
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0

0 < number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + ε)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0

has predT [seq j <- arrivals_between arr_seq (job_arrival j) (job_arrival j + ε) | job_of_task tsk j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0

j \in [seq j <- arrivals_between arr_seq (job_arrival j) (job_arrival j + ε) | job_of_task tsk j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0

j \in [seq j <- arrivals_at arr_seq (job_arrival j) ++ \cat_(job_arrival j<=i<job_arrival j) arrivals_at arr_seq i.+1 | job_of_task tsk j]
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0

job_of_task tsk j && (j \in arrivals_at arr_seq (job_arrival j))
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0

j \in arrivals_at arr_seq (job_arrival j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0
t: instant
ARR, CONS: j \in arrivals_at arr_seq t

j \in arrivals_at arr_seq (job_arrival j)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
POS: 0 < task_cost tsk
CONTR: max_arrivals tsk ε = 0
t: instant
ARR: j \in arrivals_at arr_seq t
CONS: job_arrival j = t

j \in arrivals_at arr_seq (job_arrival j)
by rewrite CONS. Qed. (** As a corollary, we prove that the [task_rbf] at any point [A] greater than [0] is no less than the task's WCET. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j

forall A : nat, 0 < A -> task_cost tsk <= task_rbf A
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j

forall A : nat, 0 < A -> task_cost tsk <= task_rbf A
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
A: nat
GEQ: 0 < A.+1

task_cost tsk <= task_rbf A.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
A: nat
GEQ: 0 < A.+1

task_rbf ε <= task_rbf A.+1
exact: task_rbf_monotone. Qed. (** Assume that [tsk] has a positive cost. *) Hypothesis H_positive_cost : 0 < task_cost tsk. (** Then, we prove that [task_rbf] at [ε] is greater than [0]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk

0 < task_rbf ε
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk

0 < task_rbf ε
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk

task_cost tsk <= task_rbf ε
by eapply task_rbf_1_ge_task_cost; eauto. Qed. (** Consider a set of tasks [ts] containing the task [tsk]. *) Variable ts : seq Task. Hypothesis H_tsk_in_ts : tsk \in ts. (** Next, we prove that cost of [tsk] is less than or equal to the [total_request_bound_function]. *)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts

forall t : nat, 0 < t -> task_cost tsk <= total_request_bound_function ts t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts

forall t : nat, 0 < t -> task_cost tsk <= total_request_bound_function ts t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts
t: nat
GE: 0 < t

task_cost tsk <= total_request_bound_function ts t
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts
t: nat
GE: 0 < t.+1

task_cost tsk <= total_request_bound_function ts t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts
t: nat
GE: 0 < t.+1

task_rbf ε <= total_request_bound_function ts t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts
t: nat
GE: 0 < t.+1

task_rbf ε <= \sum_(tsk <- ts) task_request_bound_function tsk t.+1
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts
t: nat
GE: 0 < t.+1

task_rbf ε <= addn_comoid (task_request_bound_function tsk t.+1) (\big[addn_comoid/0]_(y <- rem (T:=Task) tsk ts) task_request_bound_function y t.+1)
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times arr_seq
tsk: Task
H2: MaxArrivals Task
H_valid_arrival_curve: valid_arrival_curve (max_arrivals tsk)
H_is_arrival_curve: respects_max_arrivals arr_seq tsk (max_arrivals tsk)
task_rbf:= task_request_bound_function tsk: duration -> nat
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_positive_cost: 0 < task_cost tsk
ts: seq Task
H_tsk_in_ts: tsk \in ts
t: nat
GE: 0 < t.+1

task_rbf ε <= task_request_bound_function tsk t.+1
by apply task_rbf_monotone. Qed. End RequestBoundFunctions.