Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.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.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing. Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Require Export prosa.analysis.facts.model.restricted_supply.schedule. Require Import prosa.analysis.facts.priority.fifo. Require Import prosa.analysis.facts.model.rbf. (** * Higher-or-Equal-Priority Interference Bound under FIFO *) (** In this file, we introduce a bound on the cumulative interference from higher- and equal-priority under FIFO scheduling. *) Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves. (** Consider any type of tasks, each characterized by a WCET [task_cost] and an arrival curve [max_arrivals] ... *) Context {Task : TaskType}. Context `{TaskCost Task}. Context `{MaxArrivals Task}. (** ... and any type of jobs associated with these tasks, where each job has a task [job_task], a cost [job_cost], and an arrival time [job_arrival]. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobCost Job}. Context `{JobArrival Job}. (** Consider any kind of unit-supply uniprocessor model. *) Context `{PState : ProcessorState Job}. Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState. Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState. (** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *) Variable arr_seq : arrival_sequence Job. Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq. (** We further require that a job's cost cannot exceed its task's stated WCET. *) Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq. (** We consider an arbitrary task set [ts] ... *) Variable ts : seq Task. (** ... and assume that all jobs stem from tasks in this task set. *) Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts. (** We assume that [max_arrivals] is a family of valid arrival curves that constrains the arrival sequence [arr_seq], i.e., for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival bound of [tsk], and ... *) Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts. (** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *) Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals. (** Let [tsk] be any task in [ts] that is to be analyzed. *) Variable tsk : Task. Hypothesis H_tsk_in_ts : tsk \in ts. (** Consider any schedule ... *) Variable sched : schedule PState. (** ... where jobs do not execute before their arrival nor after completion. *) Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched. (** Next, we establish a bound on the interference produced by higher- and equal-priority jobs. *) (** Consider a job [j] of the task under analysis [tsk] with a positive cost. *) Variable j : Job. Hypothesis H_job_of_task : job_of_task tsk j. Hypothesis H_j_in_arrivals : arrives_in arr_seq j. Hypothesis H_job_cost_positive : job_cost_positive j. (** Consider the busy window of [j] and denote it as <<[t1, t2)>>. *) Variable t1 t2 : instant. Hypothesis H_busy_window : classical.busy_interval arr_seq sched j t1 t2. (** Consider any arbitrary sub-interval <<[t1, Δ)>> within the busy window of [j]. *) Variable Δ : instant. Hypothesis H_in_busy : t1 + Δ < t2. (** The cumulative interference from higher- and equal-priority jobs during <<[t1, Δ)>> is bounded as follows. *)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2

cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2

cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

quiet_time arr_seq sched j t1
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
service_of_other_hep_jobs arr_seq sched j t1 (t1 + Δ) <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

quiet_time arr_seq sched j t1
by move: (H_busy_window) => [[_ [Q _]] _].
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

service_of_other_hep_jobs arr_seq sched j t1 (t1 + Δ) <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

workload_of_jobs (another_hep_job^~ j) (arrivals_between arr_seq t1 (t1 + Δ)) <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

workload_of_jobs (fun j0 : Job => j0 != j) (arrivals_between arr_seq t1 (job_arrival j + 1)) <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

workload_of_jobs predT (arrivals_between arr_seq t1 (job_arrival j + 1)) - job_cost j <= \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j - job_cost j <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + task_request_bound_function tsk (job_arrival j - t1 + 1) - task_cost tsk
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

task_cost tsk <= task_request_bound_function tsk (job_arrival j - t1 + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j - job_cost j <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + (task_request_bound_function tsk (job_arrival j - t1 + 1) - task_cost tsk)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

task_cost tsk <= task_request_bound_function tsk (job_arrival j - t1 + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

task_cost tsk <= task_request_bound_function tsk 1
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
task_request_bound_function tsk 1 <= task_request_bound_function tsk (job_arrival j - t1 + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

task_cost tsk <= task_request_bound_function tsk 1
by apply: task_rbf_1_ge_task_cost; exact: non_pathological_max_arrivals.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

task_request_bound_function tsk 1 <= task_request_bound_function tsk (job_arrival j - t1 + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

task_request_bound_function tsk 1 <= task_request_bound_function tsk (job_arrival j - t1 + 1)
by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j - job_cost j <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + (task_request_bound_function tsk (job_arrival j - t1 + 1) - task_cost tsk)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

?n <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + (task_request_bound_function tsk (job_arrival j - t1 + 1) - task_cost tsk)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j - job_cost j <= ?n
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

?n <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + (task_request_bound_function tsk (job_arrival j - t1 + 1) - task_cost tsk)
by erewrite leq_add2l; apply task_rbf_without_job_under_analysis; (try apply ARR1) => //; lia.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j - job_cost j <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + (task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1)) - job_cost j)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j - job_cost j <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1)) - job_cost j
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
job_cost j <= task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j - job_cost j <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1)) - job_cost j
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j <= ?n
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
?n <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(j <- arrivals_between arr_seq t1 (job_arrival j + 1)) job_cost j <= ?n
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
j': Job
inJOBS: j' \in arrivals_between arr_seq t1 (job_arrival j + 1)

?x_to_y j' \in ?ys
by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(y <- ts) \sum_(x <- arrivals_between arr_seq t1 (job_arrival j + 1) | xpredT x && ([eta job_task] x == y)) job_cost x <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1) + task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(y <- rem (T:=Task) tsk ts) \sum_(x <- arrivals_between arr_seq t1 (job_arrival j + 1) | job_task x == y) job_cost x <= \sum_(y <- rem (T:=Task) tsk ts) task_request_bound_function y (job_arrival j - t1 + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

\sum_(i <- rem (T:=Task) tsk ts) (if (i \in rem (T:=Task) tsk ts) && true then \sum_(x <- arrivals_between arr_seq t1 (job_arrival j + 1) | job_task x == i) job_cost x else 0) <= \sum_(i <- rem (T:=Task) tsk ts) (if (i \in rem (T:=Task) tsk ts) && true then task_request_bound_function i (job_arrival j - t1 + 1) else 0)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
tsk': Task

(if tsk' \in rem (T:=Task) tsk ts then \sum_(x <- arrivals_between arr_seq t1 (job_arrival j + 1) | job_task x == tsk') job_cost x else 0) <= (if tsk' \in rem (T:=Task) tsk ts then task_request_bound_function tsk' (job_arrival j - t1 + 1) else 0)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
tsk': Task
IN: (tsk' \in rem (T:=Task) tsk ts) = true

\sum_(x <- arrivals_between arr_seq t1 (job_arrival j + 1) | job_task x == tsk') job_cost x <= task_request_bound_function tsk' (job_arrival j - t1 + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
tsk': Task
IN: tsk' \in ts

\sum_(x <- arrivals_between arr_seq t1 (job_arrival j + 1) | job_task x == tsk') job_cost x <= task_request_bound_function tsk' (job_arrival j - t1 + 1)
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
tsk': Task
IN: tsk' \in ts

\sum_(x <- arrivals_between arr_seq t1 (job_arrival j + 1) | job_task x == tsk') job_cost x <= workload_of_jobs (job_of_task tsk') (arrivals_between arr_seq t1 (t1 + (job_arrival j - t1 + 1)))
by rewrite addnBAC //= subnKC //= addn1; apply leqW.
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2

job_cost j <= task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
TSKj: job_of_task tsk j

job_cost j <= task_workload_between arr_seq tsk t1 (t1 + (job_arrival j - t1 + 1))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
TSKj: job_of_task tsk j

j \in arrivals_between arr_seq t1 (t1 + (job_arrival j - t1 + 1))
Task: TaskType
H: TaskCost Task
H0: MaxArrivals Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
H3: JobArrival Job
PState: ProcessorState Job
H_uniprocessor_proc_model: uniprocessor_model PState
H_unit_supply_proc_model: unit_supply_proc_model PState
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence arr_seq
H_valid_job_cost: arrivals_have_valid_job_costs arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
H_is_arrival_curve: taskset_respects_max_arrivals arr_seq ts
H_valid_arrival_curve: valid_taskset_arrival_curve ts max_arrivals
tsk: Task
H_tsk_in_ts: tsk \in ts
sched: schedule PState
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute: completed_jobs_dont_execute sched
j: Job
H_job_of_task: job_of_task tsk j
H_j_in_arrivals: arrives_in arr_seq j
H_job_cost_positive: job_cost_positive j
t1, t2: instant
H_busy_window: busy_interval arr_seq sched j t1 t2
Δ: instant
H_in_busy: t1 + Δ < t2
ARR1: t1 <= job_arrival j
ARR2: job_arrival j < t2
TSKj: job_of_task tsk j

job_arrival j < t1 + (job_arrival j - t1 + 1)
by lia. Qed. End RTAforFullyPreemptiveFIFOModelwithArrivalCurves.