Library prosa.analysis.facts.model.offset
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.offset.
Require Export prosa.analysis.facts.job_index.
In this module, we prove some properties of task offsets.
Consider any type of tasks with an offset ...
... and any type of jobs associated with these tasks.
Consider any arrival sequence with consistent and non-duplicate arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
... and any job [j] (that stems from the arrival sequence) of any
task [tsk] with a valid offset.
Variable tsk : Task.
Variable j : Job.
Hypothesis H_job_of_task: job_task j = tsk.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_job_from_arrseq: arrives_in arr_seq j.
Variable j : Job.
Hypothesis H_job_of_task: job_task j = tsk.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_job_from_arrseq: arrives_in arr_seq j.
We show that the if [j] is the first job of task [tsk]
then [j] arrives at [task_offset tsk].
Lemma first_job_arrival:
job_index arr_seq j = 0 →
job_arrival j = task_offset tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 358)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
============================
job_index arr_seq j = 0 -> job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
Proof.
intros INDX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
move: H_valid_offset ⇒ [BEFORE [j' [ARR' [TSK ARRIVAL]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
case: (boolP (j' == j)) ⇒ [/eqP EQ|NEQ]; first by rewrite -EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 446)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j')) as [Z | [m N]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 460)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
Z : job_index arr_seq j' = 0
============================
job_arrival j = task_offset tsk
subgoal 2 (ID 465) is:
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
- move: NEQ ⇒ /eqP NEQ; contradict NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 512)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
Z : job_index arr_seq j' = 0
============================
j' = j
subgoal 2 (ID 465) is:
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
now eapply equal_index_implies_equal_jobs; eauto;
[rewrite TSK | rewrite Z INDX].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 465)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
m : nat
N : job_index arr_seq j' = succn m
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
- have IND_LTE : (job_index arr_seq j ≤ job_index arr_seq j') by rewrite INDX N.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 550)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
m : nat
N : job_index arr_seq j' = succn m
IND_LTE : job_index arr_seq j <= job_index arr_seq j'
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
apply index_lte_implies_arrival_lte in IND_LTE ⇒ //; last by rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 555)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
m : nat
N : job_index arr_seq j' = succn m
IND_LTE : job_arrival j <= job_arrival j'
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
now apply/eqP; rewrite eqn_leq; apply/andP; split;
[ssrlia | apply H_valid_offset].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
job_index arr_seq j = 0 →
job_arrival j = task_offset tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 358)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
============================
job_index arr_seq j = 0 -> job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
Proof.
intros INDX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 359)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
move: H_valid_offset ⇒ [BEFORE [j' [ARR' [TSK ARRIVAL]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
case: (boolP (j' == j)) ⇒ [/eqP EQ|NEQ]; first by rewrite -EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 446)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j')) as [Z | [m N]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 460)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
Z : job_index arr_seq j' = 0
============================
job_arrival j = task_offset tsk
subgoal 2 (ID 465) is:
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
- move: NEQ ⇒ /eqP NEQ; contradict NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 512)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
Z : job_index arr_seq j' = 0
============================
j' = j
subgoal 2 (ID 465) is:
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
now eapply equal_index_implies_equal_jobs; eauto;
[rewrite TSK | rewrite Z INDX].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 465)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
m : nat
N : job_index arr_seq j' = succn m
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
- have IND_LTE : (job_index arr_seq j ≤ job_index arr_seq j') by rewrite INDX N.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 550)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
m : nat
N : job_index arr_seq j' = succn m
IND_LTE : job_index arr_seq j <= job_index arr_seq j'
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
apply index_lte_implies_arrival_lte in IND_LTE ⇒ //; last by rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 555)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
INDX : job_index arr_seq j = 0
BEFORE : no_jobs_before_offset tsk
j' : Job
ARR' : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk
NEQ : j' != j
m : nat
N : job_index arr_seq j' = succn m
IND_LTE : job_arrival j <= job_arrival j'
============================
job_arrival j = task_offset tsk
----------------------------------------------------------------------------- *)
now apply/eqP; rewrite eqn_leq; apply/andP; split;
[ssrlia | apply H_valid_offset].
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Consider any task set [ts].
If task [tsk] is in [ts], then its offset
is less than or equal to the maximum offset of all tasks
in [ts].
Lemma max_offset_g:
tsk \in ts →
task_offset tsk ≤ max_task_offset ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
ts : TaskSet Task
============================
tsk \in ts -> task_offset tsk <= max_task_offset ts
----------------------------------------------------------------------------- *)
Proof.
intros TSK_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 368)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
ts : TaskSet Task
TSK_IN : tsk \in ts
============================
task_offset tsk <= max_task_offset ts
----------------------------------------------------------------------------- *)
apply in_max0_le.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
ts : TaskSet Task
TSK_IN : tsk \in ts
============================
task_offset tsk \in task_offsets ts
----------------------------------------------------------------------------- *)
now apply map_f.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End OffsetLemmas.
tsk \in ts →
task_offset tsk ≤ max_task_offset ts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 367)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
ts : TaskSet Task
============================
tsk \in ts -> task_offset tsk <= max_task_offset ts
----------------------------------------------------------------------------- *)
Proof.
intros TSK_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 368)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
ts : TaskSet Task
TSK_IN : tsk \in ts
============================
task_offset tsk <= max_task_offset ts
----------------------------------------------------------------------------- *)
apply in_max0_le.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Task : TaskType
H : TaskOffset Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
j : Job
H_job_of_task : job_task j = tsk
H_valid_offset : valid_offset arr_seq tsk
H_job_from_arrseq : arrives_in arr_seq j
ts : TaskSet Task
TSK_IN : tsk \in ts
============================
task_offset tsk \in task_offsets ts
----------------------------------------------------------------------------- *)
now apply map_f.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End OffsetLemmas.