Library prosa.analysis.facts.preemption.rtc_threshold.limited
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.preemption.task.limited.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Furthermore, we assume the task model with fixed preemption points.
Require Import prosa.model.task.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
Task's Run to Completion Threshold
In this section, we prove that instantiation of function [task run to completion threshold] to the model with limited preemptions indeed defines a valid run-to-completion threshold function.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptionPoints Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptionPoints Job}.
Consider any arrival sequence with consistent arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Next, consider any ideal uniprocessor schedule of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_schedule_respects_preemption_model:
schedule_respects_preemption_model arr_seq sched.
Hypothesis H_schedule_respects_preemption_model:
schedule_respects_preemption_model arr_seq sched.
... where jobs do not execute before their arrival or 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.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Consider an arbitrary task set ts.
Assume that a job cost cannot be larger than a task cost.
Consider the model with fixed preemption points. I.e., each task
is divided into a number of non-preemptive segments by inserting
statically predefined preemption points.
And consider any task from task set ts with positive cost.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_positive_cost : 0 < task_cost tsk.
Hypothesis H_tsk_in_ts : tsk \in ts.
Hypothesis H_positive_cost : 0 < task_cost tsk.
We start by proving an auxiliary lemma. Note that since [tsk]
has a positive cost, [task_preemption_points tsk] contains [0]
and [task_cost tsk]. Thus, [2 <= size (task_preemption_points tsk)].
Remark number_of_preemption_points_in_task_at_least_two: 2 ≤ size (task_preemption_points tsk).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 968)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
Proof.
move: (H_valid_fixed_preemption_points_model) ⇒ [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1030)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
have Fact2: 0 < size (task_preemption_points tsk).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1034)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
============================
0 < size (task_preemption_points tsk)
subgoal 2 (ID 1036) is:
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1034)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
============================
0 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR ⇒ /eqP CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1175)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
CONTR : size (task_preemption_points tsk) = 0
============================
False
----------------------------------------------------------------------------- *)
move: (END _ H_tsk_in_ts) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1179)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
CONTR : size (task_preemption_points tsk) = 0
EQ : last0 (task_preemption_points tsk) = task_cost tsk
============================
False
----------------------------------------------------------------------------- *)
move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1194)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
CONTR : size (task_preemption_points tsk) = 0
============================
0 = task_cost tsk -> False
----------------------------------------------------------------------------- *)
by intros; move: (H_positive_cost); rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1036)
subgoal 1 (ID 1036) is:
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1036)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
have EQ: 2 = size [::0; task_cost tsk]; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1244)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
EQ : 2 = size [:: 0; task_cost tsk]
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1247)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
size [:: 0; task_cost tsk] <= size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
apply subseq_leq_size.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1249)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
uniq [:: 0; task_cost tsk]
subgoal 2 (ID 1250) is:
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite !cons_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1260)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
[&& 0 \notin [:: task_cost tsk], task_cost tsk \notin [::] & uniq [::]]
subgoal 2 (ID 1250) is:
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1260)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
[&& 0 \notin [:: task_cost tsk], task_cost tsk \notin [::] & uniq [::]]
----------------------------------------------------------------------------- *)
apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1289)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
0 \notin [:: task_cost tsk]
subgoal 2 (ID 1290) is:
(task_cost tsk \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite in_cons negb_or; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1326)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
0 != task_cost tsk
subgoal 2 (ID 1290) is:
(task_cost tsk \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite neq_ltn; apply/orP; left; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1290)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
(task_cost tsk \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1250)
subgoal 1 (ID 1250) is:
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1250)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
intros t EQ; move: EQ; rewrite !in_cons.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1405)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
[|| t == 0, t == task_cost tsk | t \in [::]] ->
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
move ⇒ /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1557)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = 0
============================
t \in task_preemption_points tsk
subgoal 2 (ID 1558) is:
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1557)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = 0
============================
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1584)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
0 \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
move: (BEG _ H_tsk_in_ts) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1588)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : first0 (task_preemption_points tsk) = 0
============================
0 \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1591)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
first0 (task_preemption_points tsk) \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite /first0 -nth0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1597)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
nth 0 (task_preemption_points tsk) 0 \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
apply/(nthP 0).
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1625)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
exists2 i : nat,
i < size (task_preemption_points tsk) &
nth 0 (task_preemption_points tsk) i =
nth 0 (task_preemption_points tsk) 0
----------------------------------------------------------------------------- *)
∃ 0; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
subgoal 1 (ID 1558) is:
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = task_cost tsk
============================
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = task_cost tsk
============================
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1631)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
task_cost tsk \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
move: (END _ H_tsk_in_ts) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1635)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : last0 (task_preemption_points tsk) = task_cost tsk
============================
task_cost tsk \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1638)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
last0 (task_preemption_points tsk) \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite /last0 -nth_last.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1644)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
nth 0 (task_preemption_points tsk)
(predn (size (task_preemption_points tsk)))
\in task_preemption_points tsk
----------------------------------------------------------------------------- *)
apply/(nthP 0).
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1672)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
exists2 i : nat,
i < size (task_preemption_points tsk) &
nth 0 (task_preemption_points tsk) i =
nth 0 (task_preemption_points tsk)
(predn (size (task_preemption_points tsk)))
----------------------------------------------------------------------------- *)
∃ ((size (task_preemption_points tsk)).-1); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1677)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
predn (size (task_preemption_points tsk)) <
size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
by rewrite -(leq_add2r 1) !addn1 prednK //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 968)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
Proof.
move: (H_valid_fixed_preemption_points_model) ⇒ [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1030)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
have Fact2: 0 < size (task_preemption_points tsk).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1034)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
============================
0 < size (task_preemption_points tsk)
subgoal 2 (ID 1036) is:
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1034)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
============================
0 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR ⇒ /eqP CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1175)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
CONTR : size (task_preemption_points tsk) = 0
============================
False
----------------------------------------------------------------------------- *)
move: (END _ H_tsk_in_ts) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1179)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
CONTR : size (task_preemption_points tsk) = 0
EQ : last0 (task_preemption_points tsk) = task_cost tsk
============================
False
----------------------------------------------------------------------------- *)
move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1194)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
CONTR : size (task_preemption_points tsk) = 0
============================
0 = task_cost tsk -> False
----------------------------------------------------------------------------- *)
by intros; move: (H_positive_cost); rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1036)
subgoal 1 (ID 1036) is:
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1036)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
have EQ: 2 = size [::0; task_cost tsk]; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1244)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
EQ : 2 = size [:: 0; task_cost tsk]
============================
1 < size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1247)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
size [:: 0; task_cost tsk] <= size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
apply subseq_leq_size.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1249)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
uniq [:: 0; task_cost tsk]
subgoal 2 (ID 1250) is:
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite !cons_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1260)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
[&& 0 \notin [:: task_cost tsk], task_cost tsk \notin [::] & uniq [::]]
subgoal 2 (ID 1250) is:
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1260)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
[&& 0 \notin [:: task_cost tsk], task_cost tsk \notin [::] & uniq [::]]
----------------------------------------------------------------------------- *)
apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1289)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
0 \notin [:: task_cost tsk]
subgoal 2 (ID 1290) is:
(task_cost tsk \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite in_cons negb_or; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1326)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
0 != task_cost tsk
subgoal 2 (ID 1290) is:
(task_cost tsk \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
rewrite neq_ltn; apply/orP; left; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1290)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
(task_cost tsk \notin [::]) && uniq [::]
----------------------------------------------------------------------------- *)
apply/andP; split; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1250)
subgoal 1 (ID 1250) is:
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1250)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
============================
forall x : nat_eqType,
x \in [:: 0; task_cost tsk] -> x \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
intros t EQ; move: EQ; rewrite !in_cons.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1405)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
[|| t == 0, t == task_cost tsk | t \in [::]] ->
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
move ⇒ /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1557)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = 0
============================
t \in task_preemption_points tsk
subgoal 2 (ID 1558) is:
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1557)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = 0
============================
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1584)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
0 \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
move: (BEG _ H_tsk_in_ts) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1588)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : first0 (task_preemption_points tsk) = 0
============================
0 \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1591)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
first0 (task_preemption_points tsk) \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite /first0 -nth0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1597)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
nth 0 (task_preemption_points tsk) 0 \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
apply/(nthP 0).
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1625)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
exists2 i : nat,
i < size (task_preemption_points tsk) &
nth 0 (task_preemption_points tsk) i =
nth 0 (task_preemption_points tsk) 0
----------------------------------------------------------------------------- *)
∃ 0; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
subgoal 1 (ID 1558) is:
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = task_cost tsk
============================
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1558)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : t = task_cost tsk
============================
t \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1631)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
task_cost tsk \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
move: (END _ H_tsk_in_ts) ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1635)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
EQ : last0 (task_preemption_points tsk) = task_cost tsk
============================
task_cost tsk \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite -EQ; clear EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1638)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
last0 (task_preemption_points tsk) \in task_preemption_points tsk
----------------------------------------------------------------------------- *)
rewrite /last0 -nth_last.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1644)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
nth 0 (task_preemption_points tsk)
(predn (size (task_preemption_points tsk)))
\in task_preemption_points tsk
----------------------------------------------------------------------------- *)
apply/(nthP 0).
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 1672)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
exists2 i : nat,
i < size (task_preemption_points tsk) &
nth 0 (task_preemption_points tsk) i =
nth 0 (task_preemption_points tsk)
(predn (size (task_preemption_points tsk)))
----------------------------------------------------------------------------- *)
∃ ((size (task_preemption_points tsk)).-1); last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1677)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
MLP : valid_limited_preemptions_job_model arr_seq
BEG : task_beginning_of_execution_in_preemption_points ts
END : task_end_of_execution_in_preemption_points ts
INCR : nondecreasing_task_preemption_points ts
HYP1 : consistent_job_segment_count arr_seq
HYP2 : job_respects_segment_lengths arr_seq
HYP3 : task_segments_are_nonempty ts
Fact2 : 0 < size (task_preemption_points tsk)
t : nat_eqType
============================
predn (size (task_preemption_points tsk)) <
size (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
by rewrite -(leq_add2r 1) !addn1 prednK //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Then, we prove that [task_run_to_completion_threshold] function
defines a valid task's run to completion threshold.
Lemma limited_valid_task_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 979)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
============================
valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 982)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
============================
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
intros ? ARR__j TSK__j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 997)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
move: (H_valid_fixed_preemption_points_model) ⇒ [LJ LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1009)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
move: (LJ) (LT) ⇒ [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1083)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
rewrite /job_run_to_completion_threshold /task_run_to_completion_threshold /limited_preemptions
/job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1121)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [Z|POS]; first by rewrite Z; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1145)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
by eapply job_last_nonpreemptive_segment_positive; eauto using valid_fixed_preemption_points_model_lemma.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1179)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have T_RTCT__pos : 0 < task_last_nonpr_segment tsk.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1182)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < task_last_nonpr_segment tsk
subgoal 2 (ID 1184) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1182)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < task_last_nonpr_segment tsk
----------------------------------------------------------------------------- *)
unfold job_respects_segment_lengths, task_last_nonpr_segment in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1186)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite last0_nth; apply T6; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1191)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
have F: 1 ≤ size (distances (task_preemption_points tsk)).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1208)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < size (distances (task_preemption_points tsk))
subgoal 2 (ID 1210) is:
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1208)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
apply leq_trans with (size (task_preemption_points tsk) - 1).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1214)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < size (task_preemption_points tsk) - 1
subgoal 2 (ID 1215) is:
size (task_preemption_points tsk) - 1 <=
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
- have F := number_of_preemption_points_in_task_at_least_two; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1215)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
size (task_preemption_points tsk) - 1 <=
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
- rewrite [in X in X - 1]size_of_seq_of_distances; [ssrlia | apply number_of_preemption_points_in_task_at_least_two].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1210)
subgoal 1 (ID 1210) is:
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
subgoal 2 (ID 1184) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1210)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
F : 0 < size (distances (task_preemption_points tsk))
============================
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1184)
subgoal 1 (ID 1184) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1184)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have J_RTCT__le : job_last_nonpreemptive_segment j ≤ job_cost j
by eapply job_last_nonpreemptive_segment_le_job_cost; eauto using valid_fixed_preemption_points_model_lemma.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2020)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have T_RTCT__le : task_last_nonpr_segment tsk ≤ task_cost tsk.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2025)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
task_last_nonpr_segment tsk <= task_cost tsk
subgoal 2 (ID 2027) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2025)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
task_last_nonpr_segment tsk <= task_cost tsk
----------------------------------------------------------------------------- *)
unfold task_last_nonpr_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2029)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
last0 (distances (task_preemption_points tsk)) <= task_cost tsk
----------------------------------------------------------------------------- *)
rewrite -COST__task //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2035)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
last0 (distances (task_preemption_points tsk)) <=
last0 (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
eapply leq_trans; last by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2060)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
last0 (distances (task_preemption_points tsk)) <=
max0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
by apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2027)
subgoal 1 (ID 2027) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2027)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
rewrite subnBA // subnBA // -addnBAC // -addnBAC // !addn1 ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2192)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - last0 (distances (parameter.job_preemption_points j)) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
erewrite job_parameters_last_np_to_job_limited; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2197)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - last0 [seq x <- distances (job_preemption_points j) | 0 < x] <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite distances_positive_undup //; last by apply SORT__job.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2223)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - last0 (distances (undup (job_preemption_points j))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
have → : job_cost j = last0 (undup (job_preemption_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2298)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
last0 (undup (job_preemption_points j)) -
last0 (distances (undup (job_preemption_points j))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite last_seq_minus_last_distance_seq; last by apply nondecreasing_sequence_undup, SORT__job.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2302)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (undup (job_preemption_points j))
(predn (predn (size (undup (job_preemption_points j))))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
apply leq_trans with( nth 0 (job_preemption_points j) ((size (job_preemption_points j)).-2)); first by apply undup_nth_le; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2313)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
have → : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2334)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
last0 (task_preemption_points tsk) -
last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2338)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
nth 0 (task_preemption_points tsk)
(predn (predn (size (task_preemption_points tsk))))
----------------------------------------------------------------------------- *)
rewrite -TSK__j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2342)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
nth 0 (task_preemption_points (job_task j))
(predn (predn (size (task_preemption_points (job_task j)))))
----------------------------------------------------------------------------- *)
rewrite T4; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2348)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (task_preemption_points (job_task j))))) <=
nth 0 (task_preemption_points (job_task j))
(predn (predn (size (task_preemption_points (job_task j)))))
----------------------------------------------------------------------------- *)
apply domination_of_distances_implies_domination_of_seq; try eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 2350)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
first0 (job_preemption_points j) <=
first0 (task_preemption_points (job_task j))
subgoal 2 (ID 2351) is:
1 < size (job_preemption_points j)
subgoal 3 (ID 2352) is:
1 < size (task_preemption_points (job_task j))
subgoal 4 (ID 2355) is:
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- erewrite zero_is_first_element; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 2351)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 2352) is:
1 < size (task_preemption_points (job_task j))
subgoal 3 (ID 2355) is:
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- eapply number_of_preemption_points_at_least_two; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2352)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
1 < size (task_preemption_points (job_task j))
subgoal 2 (ID 2355) is:
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- by rewrite TSK__j; eapply number_of_preemption_points_in_task_at_least_two.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2355)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- by apply SORT__task; rewrite TSK__j.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdLimitedPreemptions.
Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.
valid_task_run_to_completion_threshold arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 979)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
============================
valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 982)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
============================
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
intros ? ARR__j TSK__j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 997)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
move: (H_valid_fixed_preemption_points_model) ⇒ [LJ LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1009)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
move: (LJ) (LT) ⇒ [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1083)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
rewrite /job_run_to_completion_threshold /task_run_to_completion_threshold /limited_preemptions
/job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1121)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [Z|POS]; first by rewrite Z; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1145)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
by eapply job_last_nonpreemptive_segment_positive; eauto using valid_fixed_preemption_points_model_lemma.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1179)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have T_RTCT__pos : 0 < task_last_nonpr_segment tsk.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1182)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < task_last_nonpr_segment tsk
subgoal 2 (ID 1184) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1182)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < task_last_nonpr_segment tsk
----------------------------------------------------------------------------- *)
unfold job_respects_segment_lengths, task_last_nonpr_segment in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1186)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite last0_nth; apply T6; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1191)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
have F: 1 ≤ size (distances (task_preemption_points tsk)).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1208)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < size (distances (task_preemption_points tsk))
subgoal 2 (ID 1210) is:
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1208)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
apply leq_trans with (size (task_preemption_points tsk) - 1).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1214)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
0 < size (task_preemption_points tsk) - 1
subgoal 2 (ID 1215) is:
size (task_preemption_points tsk) - 1 <=
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
- have F := number_of_preemption_points_in_task_at_least_two; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1215)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
============================
size (task_preemption_points tsk) - 1 <=
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
- rewrite [in X in X - 1]size_of_seq_of_distances; [ssrlia | apply number_of_preemption_points_in_task_at_least_two].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1210)
subgoal 1 (ID 1210) is:
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
subgoal 2 (ID 1184) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1210)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : forall (j : Job) (n : nat),
arrives_in arr_seq j ->
nth 0 (distances (job_preemption_points j)) n <=
nth 0 (distances (task_preemption_points (job_task j))) n
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
F : 0 < size (distances (task_preemption_points tsk))
============================
predn (size (distances (task_preemption_points tsk))) <
size (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1184)
subgoal 1 (ID 1184) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1184)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have J_RTCT__le : job_last_nonpreemptive_segment j ≤ job_cost j
by eapply job_last_nonpreemptive_segment_le_job_cost; eauto using valid_fixed_preemption_points_model_lemma.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2020)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
have T_RTCT__le : task_last_nonpr_segment tsk ≤ task_cost tsk.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2025)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
task_last_nonpr_segment tsk <= task_cost tsk
subgoal 2 (ID 2027) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2025)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
task_last_nonpr_segment tsk <= task_cost tsk
----------------------------------------------------------------------------- *)
unfold task_last_nonpr_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2029)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
last0 (distances (task_preemption_points tsk)) <= task_cost tsk
----------------------------------------------------------------------------- *)
rewrite -COST__task //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2035)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
last0 (distances (task_preemption_points tsk)) <=
last0 (task_preemption_points tsk)
----------------------------------------------------------------------------- *)
eapply leq_trans; last by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2060)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
============================
last0 (distances (task_preemption_points tsk)) <=
max0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
by apply last_of_seq_le_max_of_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2027)
subgoal 1 (ID 2027) is:
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2027)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - (last0 (distances (parameter.job_preemption_points j)) - ε) <=
task_cost tsk - (last0 (distances (task_preemption_points tsk)) - ε)
----------------------------------------------------------------------------- *)
rewrite subnBA // subnBA // -addnBAC // -addnBAC // !addn1 ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2192)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - last0 (distances (parameter.job_preemption_points j)) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
erewrite job_parameters_last_np_to_job_limited; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2197)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - last0 [seq x <- distances (job_preemption_points j) | 0 < x] <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite distances_positive_undup //; last by apply SORT__job.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2223)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
job_cost j - last0 (distances (undup (job_preemption_points j))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
have → : job_cost j = last0 (undup (job_preemption_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2298)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
last0 (undup (job_preemption_points j)) -
last0 (distances (undup (job_preemption_points j))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite last_seq_minus_last_distance_seq; last by apply nondecreasing_sequence_undup, SORT__job.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2302)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (undup (job_preemption_points j))
(predn (predn (size (undup (job_preemption_points j))))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
apply leq_trans with( nth 0 (job_preemption_points j) ((size (job_preemption_points j)).-2)); first by apply undup_nth_le; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2313)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
task_cost tsk - last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
have → : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2334)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
last0 (task_preemption_points tsk) -
last0 (distances (task_preemption_points tsk))
----------------------------------------------------------------------------- *)
rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2338)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
nth 0 (task_preemption_points tsk)
(predn (predn (size (task_preemption_points tsk))))
----------------------------------------------------------------------------- *)
rewrite -TSK__j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2342)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (job_preemption_points j)))) <=
nth 0 (task_preemption_points (job_task j))
(predn (predn (size (task_preemption_points (job_task j)))))
----------------------------------------------------------------------------- *)
rewrite T4; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2348)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nth 0 (job_preemption_points j)
(predn (predn (size (task_preemption_points (job_task j))))) <=
nth 0 (task_preemption_points (job_task j))
(predn (predn (size (task_preemption_points (job_task j)))))
----------------------------------------------------------------------------- *)
apply domination_of_distances_implies_domination_of_seq; try eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 2350)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
first0 (job_preemption_points j) <=
first0 (task_preemption_points (job_task j))
subgoal 2 (ID 2351) is:
1 < size (job_preemption_points j)
subgoal 3 (ID 2352) is:
1 < size (task_preemption_points (job_task j))
subgoal 4 (ID 2355) is:
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- erewrite zero_is_first_element; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 2351)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
1 < size (job_preemption_points j)
subgoal 2 (ID 2352) is:
1 < size (task_preemption_points (job_task j))
subgoal 3 (ID 2355) is:
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- eapply number_of_preemption_points_at_least_two; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2352)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
1 < size (task_preemption_points (job_task j))
subgoal 2 (ID 2355) is:
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- by rewrite TSK__j; eapply number_of_preemption_points_in_task_at_least_two.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2355)
Task : TaskType
H : TaskCost Task
H0 : TaskPreemptionPoints Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
ts : seq Task
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
H_positive_cost : 0 < task_cost tsk
j : Job
ARR__j : arrives_in arr_seq j
TSK__j : job_task j = tsk
LJ : valid_limited_preemptions_job_model arr_seq
LT : valid_fixed_preemption_points_task_model arr_seq ts
ZERO__job : beginning_of_execution_in_preemption_points arr_seq
COST__job : end_of_execution_in_preemption_points arr_seq
SORT__job : preemption_points_is_nondecreasing_sequence arr_seq
ZERO__task : task_beginning_of_execution_in_preemption_points ts
COST__task : task_end_of_execution_in_preemption_points ts
SORT__task : nondecreasing_task_preemption_points ts
T4 : consistent_job_segment_count arr_seq
T5 : job_respects_segment_lengths arr_seq
T6 : task_segments_are_nonempty ts
POS : 0 < job_cost j
J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
T_RTCT__pos : 0 < task_last_nonpr_segment tsk
J_RTCT__le : job_last_nonpreemptive_segment j <= job_cost j
T_RTCT__le : task_last_nonpr_segment tsk <= task_cost tsk
============================
nondecreasing_sequence (task_preemption_points (job_task j))
----------------------------------------------------------------------------- *)
- by apply SORT__task; rewrite TSK__j.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdLimitedPreemptions.
Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.