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 .
Require Export prosa.analysis.definitions.blocking_bound.elf.[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.busy_interval.pi.
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.facts.model.arrival_curves.
Require Import prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.facts.priority.elf.New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default] New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default] Notation "_ - _" was already used in scope
distn_scope. [notation-overridden,parsing,default]
(** * Lower-Priority Non-Preemptive Segment is Bounded *)
(** In this file, we prove that, under the ELF scheduling policy, the
length of the maximum non-preemptive segment of a lower-priority
job (w.r.t. a job of a task [tsk]) is bounded by
[blocking_bound]. *)
Section MaxNPSegmentIsBounded .
(** Consider any type of tasks, each characterized by a WCET
[task_cost], an arrival curve [max_arrivals], a relative
deadline [task_deadline], a bound on the the task's longest
non-preemptive segment [task_max_nonpreemptive_segment] and
relative priority points, ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
Context `{PriorityPoint 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 processor state model. *)
Context `{PState : ProcessorState Job}.
(** Consider any valid arrival sequence ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** 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.
(** ... and assume that jobs have bounded non-preemptive segments. *)
Context `{JobPreemptable Job}.
Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(** Consider an arbitrary task set [ts], ... *)
Variable ts : seq Task.
(** ... assume that all jobs come from the task set, ... *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and let [tsk] be any task in [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Let [max_arrivals] be a family of arrival curves. *)
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_job_of_tsk : job_of_task tsk j.
(** Consider an FP policy that indicates a higher-or-equal priority
relation, and assume that the relation is reflexive, transitive
and total. *)
Context (FP : FP_policy Task).
Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
Hypothesis H_transitive_priorities : transitive_task_priorities FP.
Hypothesis H_total_priorities : total_task_priorities FP.
(** Then, the maximum length of a nonpreemptive segment among all
lower-priority jobs (w.r.t. the given job [j]) arrived so far is
bounded by [blocking_bound]. *)
Lemma nonpreemptive_segments_bounded_by_blocking :
forall t1 t2 ,
busy_interval_prefix arr_seq sched j t1 t2 ->
max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
forall t1 t2 : instant,
busy_interval_prefix arr_seq sched j t1 t2 ->
max_lp_nonpreemptive_segment arr_seq j t1 <=
blocking_bound ts tsk (job_arrival j - t1)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP
forall t1 t2 : instant,
busy_interval_prefix arr_seq sched j t1 t2 ->
max_lp_nonpreemptive_segment arr_seq j t1 <=
blocking_bound ts tsk (job_arrival j - t1)
move => t1 t2 BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2
\max_(j_lp <- arrivals_before arr_seq t1 | ~~
hep_job
j_lp j &&
(0 <
job_cost
j_lp))
(job_max_nonpreemptive_segment j_lp - 1 ) <=
\max_(tsk_o <- ts | [&& hp_task tsk tsk_o,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o]
|| [&& ep_task tsk tsk_o &&
((job_arrival j - t1)%:R +
task_priority_point tsk <
task_priority_point tsk_o)%R,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o])
(task_max_nonpreemptive_segment tsk_o - 1 )
apply : leq_trans; first by apply : max_np_job_segment_bounded_by_max_np_task_segment.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2
\max_(j_lp <- arrivals_between arr_seq 0 t1 | ~~
hep_job
j_lp j &&
(0 <
job_cost
j_lp))
(task_max_nonpreemptive_segment (job_task j_lp) - 1 ) <=
\max_(tsk_o <- ts | [&& hp_task tsk tsk_o,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o]
|| [&& ep_task tsk tsk_o &&
((job_arrival j - t1)%:R +
task_priority_point tsk <
task_priority_point tsk_o)%R,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o])
(task_max_nonpreemptive_segment tsk_o - 1 )
apply /bigmax_leq_seqP => j' JINB NOTHEP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : j' \in arrivals_between arr_seq 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j')
task_max_nonpreemptive_segment (job_task j') - 1 <=
\max_(tsk_o <- ts | [&& hp_task tsk tsk_o,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o]
|| [&& ep_task tsk tsk_o &&
((job_arrival j - t1)%:R +
task_priority_point tsk <
task_priority_point tsk_o)%R,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o])
(task_max_nonpreemptive_segment tsk_o - 1 )
have ARR': arrives_in arr_seq j'
by apply : in_arrivals_implies_arrived; exact : JINB.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : j' \in arrivals_between arr_seq 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j'
task_max_nonpreemptive_segment (job_task j') - 1 <=
\max_(tsk_o <- ts | [&& hp_task tsk tsk_o,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o]
|| [&& ep_task tsk tsk_o &&
((job_arrival j - t1)%:R +
task_priority_point tsk <
task_priority_point tsk_o)%R,
0 < max_arrivals tsk_o 1
& 0 < task_cost tsk_o])
(task_max_nonpreemptive_segment tsk_o - 1 )
apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1 );
first by apply H_all_jobs_from_taskset.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : j' \in arrivals_between arr_seq 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j'
[&& hp_task tsk (job_task j'),
0 < max_arrivals (job_task j') 1
& 0 < task_cost (job_task j')]
|| [&& ep_task tsk (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point tsk <
task_priority_point (job_task j'))%R,
0 < max_arrivals (job_task j') 1
& 0 < task_cost (job_task j')]
apply in_arrivals_implies_arrived_between in JINB => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : arrived_between j' 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j'
[&& hp_task tsk (job_task j'),
0 < max_arrivals (job_task j') 1
& 0 < task_cost (job_task j')]
|| [&& ep_task tsk (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point tsk <
task_priority_point (job_task j'))%R,
0 < max_arrivals (job_task j') 1
& 0 < task_cost (job_task j')]
move : JINB; move => /andP [_ TJ'].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
[&& hp_task tsk (job_task j'),
0 < max_arrivals (job_task j') 1
& 0 < task_cost (job_task j')]
|| [&& ep_task tsk (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point tsk <
task_priority_point (job_task j'))%R,
0 < max_arrivals (job_task j') 1
& 0 < task_cost (job_task j')]
have ->: (max_arrivals (job_task j') ε > 0 ) && (task_cost (job_task j') > 0 ) = true.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
(0 < max_arrivals (job_task j') 1 ) &&
(0 < task_cost (job_task j')) = true
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
(0 < max_arrivals (job_task j') 1 ) &&
(0 < task_cost (job_task j')) = true
apply /andP; split .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < max_arrivals (job_task j') 1
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < max_arrivals (job_task j') 1
apply : non_pathological_max_arrivals; last first .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
arrives_in ?Goal1 ?Goal3
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
arrives_in ?Goal1 ?Goal3
exact : ARR'.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
job_of_task (job_task j') j'
by rewrite /job_of_task.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
respects_max_arrivals arr_seq (job_task j')
(max_arrivals (job_task j'))
by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < task_cost (job_task j')
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < task_cost (job_task j')
move : NOTHEP => /andP [_ NZ].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NZ : 0 < job_cost j'
0 < task_cost (job_task j')
move : (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NZ : 0 < job_cost j'
job_cost j' <= task_cost (job_task j') ->
0 < task_cost (job_task j')
by lia . } } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
hp_task tsk (job_task j') && true
|| ep_task tsk (job_task j') &&
((job_arrival j - t1)%:R + task_priority_point tsk <
task_priority_point (job_task j'))%R && true
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
hp_task tsk (job_task j') && true
|| ep_task tsk (job_task j') &&
((job_arrival j - t1)%:R + task_priority_point tsk <
task_priority_point (job_task j'))%R && true
move : NOTHEP => /andP [/norP [NOTHP NOTEP] JCOST].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'
hp_task tsk (job_task j') && true
|| ep_task tsk (job_task j') &&
((job_arrival j - t1)%:R + task_priority_point tsk <
task_priority_point (job_task j'))%R && true
rewrite ?andbT .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'
hp_task tsk (job_task j')
|| ep_task tsk (job_task j') &&
((job_arrival j - t1)%:R + task_priority_point tsk <
task_priority_point (job_task j'))%R
move : H_job_of_tsk; rewrite /job_of_task => /eqP <-.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'
hp_task (job_task j) (job_task j')
|| ep_task (job_task j) (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
case : (boolP (hep_task (job_task j') (job_task j))) => NOTHEP_Tsk'.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j)
hp_task (job_task j) (job_task j')
|| ep_task (job_task j) (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j)
hp_task (job_task j) (job_task j')
|| ep_task (job_task j) (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
rewrite /hp_task NOTHEP_Tsk' => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j)
hep_task (job_task j) (job_task j') && false
|| ep_task (job_task j) (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
rewrite andbF orFb /ep_task.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j)
hep_task (job_task j) (job_task j') &&
hep_task (job_task j') (job_task j) &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
rewrite not_hp_hep_task in NOTHP => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j) NOTHP : hep_task (job_task j) (job_task j')
hep_task (job_task j) (job_task j') &&
hep_task (job_task j') (job_task j) &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
rewrite NOTHP NOTHEP_Tsk' //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j) NOTHP : hep_task (job_task j) (job_task j')
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
rewrite NOTHEP_Tsk' Bool.andb_true_l /hep_job /GEL /job_priority_point -ltNge in NOTEP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j) NOTHP : hep_task (job_task j) (job_task j') NOTEP : ((job_arrival j)%:R +
task_priority_point (job_task j) <
(job_arrival j')%:R +
task_priority_point (job_task j'))%R
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
have LT: ((job_arrival j)%:R + task_priority_point (job_task j)
< (t1)%:R + task_priority_point (job_task j'))%R by lia .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j) NOTHP : hep_task (job_task j) (job_task j') NOTEP : ((job_arrival j)%:R +
task_priority_point (job_task j) <
(job_arrival j')%:R +
task_priority_point (job_task j'))%R LT : ((job_arrival j)%:R +
task_priority_point (job_task j) <
t1%:R + task_priority_point (job_task j'))%R
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
rewrite natrB; first by lia .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j) NOTHP : hep_task (job_task j) (job_task j') NOTEP : ((job_arrival j)%:R +
task_priority_point (job_task j) <
(job_arrival j')%:R +
task_priority_point (job_task j'))%R LT : ((job_arrival j)%:R +
task_priority_point (job_task j) <
t1%:R + task_priority_point (job_task j'))%R
t1 <= job_arrival j
move : BUSY; rewrite /busy_interval_prefix.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j) NOTHP : hep_task (job_task j) (job_task j') NOTEP : ((job_arrival j)%:R +
task_priority_point (job_task j) <
(job_arrival j')%:R +
task_priority_point (job_task j'))%R LT : ((job_arrival j)%:R +
task_priority_point (job_task j) <
t1%:R + task_priority_point (job_task j'))%R
t1 < t2 /\
quiet_time arr_seq sched j t1 /\
(forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j t) /\
t1 <= job_arrival j < t2 -> t1 <= job_arrival j
move => [? [? [? J_ARR]]].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 JCOST : 0 < job_cost j'NOTHEP_Tsk' : hep_task (job_task j') (job_task j) NOTHP : hep_task (job_task j) (job_task j') NOTEP : ((job_arrival j)%:R +
task_priority_point (job_task j) <
(job_arrival j')%:R +
task_priority_point (job_task j'))%R LT : ((job_arrival j)%:R +
task_priority_point (job_task j) <
t1%:R + task_priority_point (job_task j'))%R _a_ : t1 < t2 _a1_ : quiet_time arr_seq sched j t1 _a2_ : forall t : nat,
t1 < t < t2 -> ~ quiet_time arr_seq sched j tJ_ARR : t1 <= job_arrival j < t2
t1 <= job_arrival j
by lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : ~~ hep_task (job_task j') (job_task j)
hp_task (job_task j) (job_task j')
|| ep_task (job_task j) (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : ~~ hep_task (job_task j') (job_task j)
hp_task (job_task j) (job_task j')
|| ep_task (job_task j) (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
rewrite not_hep_hp_task in NOTHEP_Tsk' => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskMaxNonpreemptiveSegment Task H2 : PriorityPoint Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j FP : FP_policy Task H_reflexive_priorities : reflexive_task_priorities FP H_transitive_priorities : transitive_task_priorities
FP H_total_priorities : total_task_priorities FP t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHP : ~~ hp_task (job_task j') (job_task j) NOTEP : ~~
(hep_task (job_task j') (job_task j) &&
hep_job j' j) JCOST : 0 < job_cost j'NOTHEP_Tsk' : hp_task (job_task j) (job_task j')
hp_task (job_task j) (job_task j')
|| ep_task (job_task j) (job_task j') &&
((job_arrival j - t1)%:R +
task_priority_point (job_task j) <
task_priority_point (job_task j'))%R
by rewrite NOTHEP_Tsk'. } }
Qed .
End MaxNPSegmentIsBounded .