Library prosa.analysis.facts.shifted_job_costs


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.facts.periodic.task_arrivals_size.
Require Export prosa.model.task.concept.
Require Export prosa.analysis.facts.hyperperiod.

In this file we define a new function for job costs in an observation interval and prove its validity.
Section ValidJobCostsShifted.

Consider any type of periodic tasks ...
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.
  Context `{TaskCost Task}.

... and any type of jobs.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobDeadline Job}.

Consider a consistent arrival sequence with 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.

Furthermore, assume that arrivals have valid job costs.
  Hypothesis H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq.

Consider a periodic task set [ts] such that all tasks in [ts] have valid periods and offsets.
  Variable ts : TaskSet Task.
  Hypothesis H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts.
  Hypothesis H_valid_periods_in_taskset: valid_periods ts.
  Hypothesis H_valid_offsets_in_taskset: valid_offsets arr_seq ts.

Consider a job [j] that stems from the arrival sequence.
  Variable j : Job.
  Hypothesis H_j_from_arrival_sequence: arrives_in arr_seq j.

Let [O_max] denote the maximum task offset of all tasks in [ts] ...
  Let O_max := max_task_offset ts.
... and let [HP] denote the hyperperiod of all tasks in [ts].
  Let HP := hyperperiod ts.

We now define a new function for job costs in the observation interval.
Given that job [j] arrives after [O_max], the cost of a job [j'] that arrives in the interval [O_max + HP, O_max + 2HP) is defined to be the same as the job cost of its corresponding job in [j]'s hyperperiod.
  Definition job_costs_shifted (j' : Job) :=
    if (job_arrival j ≥ O_max) && (O_max + HP ≤ job_arrival j' < O_max + 2 × HP) then
      job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j'))
    else job_cost j'.

Assume that we have an infinite sequence of jobs.
  Hypothesis H_infinite_jobs: infinite_jobs arr_seq.

Assume all jobs in the arrival sequence [arr_seq] belong to some task in [ts].
  Hypothesis H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts.

We assign the job costs as defined by the [job_costs_shifted] function.
  Instance job_costs_in_oi : JobCost Job :=
    job_costs_shifted.

We show that the [job_costs_shifted] function is valid.
  Lemma job_costs_shifted_valid: arrivals_have_valid_job_costs arr_seq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 990)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  ============================
  arrivals_have_valid_job_costs arr_seq

----------------------------------------------------------------------------- *)

  Proof.
    rewrite /arrivals_have_valid_job_costs /valid_job_cost.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1012)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  ============================
  forall j0 : Job,
  arrives_in arr_seq j0 -> job_cost j0 <= task_cost (job_task j0)

----------------------------------------------------------------------------- *)

    intros j' ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1014)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  ============================
  job_cost j' <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    unfold job_cost; rewrite /job_costs_in_oi /job_costs_shifted.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1018)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  ============================
  (if
    [&& O_max <= job_arrival j, O_max + HP <= job_arrival j'
      & job_arrival j' < O_max + 2 * HP]
   then
    job_cost
      (corresponding_job_in_hyperperiod ts arr_seq j'
         (starting_instant_of_corresponding_hyperperiod ts j) 
         (job_task j'))
   else job_cost j') <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    destruct (leqP O_max (job_arrival j)) as [A | B].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1043)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  ============================
  (if
    [&& true, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
   then
    job_cost
      (corresponding_job_in_hyperperiod ts arr_seq j'
         (starting_instant_of_corresponding_hyperperiod ts j) 
         (job_task j'))
   else job_cost j') <= task_cost (job_task j')

subgoal 2 (ID 1044) is:
 (if
   [&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
  then
   job_cost
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod ts j) 
        (job_task j'))
  else job_cost j') <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    destruct (leqP (O_max + HP) (job_arrival j')) as [NEQ | NEQ].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1069)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  ============================
  (if [&& true, true & job_arrival j' < O_max + 2 * HP]
   then
    job_cost
      (corresponding_job_in_hyperperiod ts arr_seq j'
         (starting_instant_of_corresponding_hyperperiod ts j) 
         (job_task j'))
   else job_cost j') <= task_cost (job_task j')

subgoal 2 (ID 1070) is:
 (if [&& true, false & job_arrival j' < O_max + 2 * HP]
  then
   job_cost
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod ts j) 
        (job_task j'))
  else job_cost j') <= task_cost (job_task j')
subgoal 3 (ID 1044) is:
 (if
   [&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
  then
   job_cost
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod ts j) 
        (job_task j'))
  else job_cost j') <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    destruct (leqP (O_max + 2 × HP) (job_arrival j')) as [LT | LT].

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 1095)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : O_max + 2 * HP <= job_arrival j'
  ============================
  (if [&& true, true & false]
   then
    job_cost
      (corresponding_job_in_hyperperiod ts arr_seq j'
         (starting_instant_of_corresponding_hyperperiod ts j) 
         (job_task j'))
   else job_cost j') <= task_cost (job_task j')

subgoal 2 (ID 1096) is:
 (if [&& true, true & true]
  then
   job_cost
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod ts j) 
        (job_task j'))
  else job_cost j') <= task_cost (job_task j')
subgoal 3 (ID 1070) is:
 (if [&& true, false & job_arrival j' < O_max + 2 * HP]
  then
   job_cost
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod ts j) 
        (job_task j'))
  else job_cost j') <= task_cost (job_task j')
subgoal 4 (ID 1044) is:
 (if
   [&& false, O_max + HP <= job_arrival j' & job_arrival j' < O_max + 2 * HP]
  then
   job_cost
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod ts j) 
        (job_task j'))
  else job_cost j') <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    all : try by apply H_arrivals_have_valid_job_costs ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1096)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  ============================
  (if [&& true, true & true]
   then
    job_cost
      (corresponding_job_in_hyperperiod ts arr_seq j'
         (starting_instant_of_corresponding_hyperperiod ts j) 
         (job_task j'))
   else job_cost j') <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    simpl.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1101)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  ============================
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod ts j) 
       (job_task j')) <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    specialize (corresponding_jobs_have_same_task arr_seq ts j' j) ⇒ TSK.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1110)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  TSK : job_task
          (corresponding_job_in_hyperperiod ts arr_seq j'
             (starting_instant_of_corresponding_hyperperiod ts j)
             (job_task j')) = job_task j'
  ============================
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod ts j) 
       (job_task j')) <= task_cost (job_task j')

----------------------------------------------------------------------------- *)

    rewrite -[in X in _ ≤ task_cost X]TSK.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1123)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  TSK : job_task
          (corresponding_job_in_hyperperiod ts arr_seq j'
             (starting_instant_of_corresponding_hyperperiod ts j)
             (job_task j')) = job_task j'
  ============================
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod ts j) 
       (job_task j')) <=
  task_cost
    (job_task
       (corresponding_job_in_hyperperiod ts arr_seq j'
          (starting_instant_of_corresponding_hyperperiod ts j) 
          (job_task j')))

----------------------------------------------------------------------------- *)

    have IN : job_task j' \in ts by apply H_jobs_from_taskset.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1134)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  TSK : job_task
          (corresponding_job_in_hyperperiod ts arr_seq j'
             (starting_instant_of_corresponding_hyperperiod ts j)
             (job_task j')) = job_task j'
  IN : job_task j' \in ts
  ============================
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod ts j) 
       (job_task j')) <=
  task_cost
    (job_task
       (corresponding_job_in_hyperperiod ts arr_seq j'
          (starting_instant_of_corresponding_hyperperiod ts j) 
          (job_task j')))

----------------------------------------------------------------------------- *)

    apply H_arrivals_have_valid_job_costs, corresponding_job_arrives ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 1146)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  TSK : job_task
          (corresponding_job_in_hyperperiod ts arr_seq j'
             (starting_instant_of_corresponding_hyperperiod ts j)
             (job_task j')) = job_task j'
  IN : job_task j' \in ts
  ============================
  valid_offset arr_seq (job_task j')

subgoal 2 (ID 1147) is:
 valid_period (job_task j')
subgoal 3 (ID 1148) is:
 respects_periodic_task_model arr_seq (job_task j')
subgoal 4 (ID 1152) is:
 max_task_offset ts <= job_arrival j'

----------------------------------------------------------------------------- *)

    + now apply H_valid_offsets_in_taskset.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1147)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  TSK : job_task
          (corresponding_job_in_hyperperiod ts arr_seq j'
             (starting_instant_of_corresponding_hyperperiod ts j)
             (job_task j')) = job_task j'
  IN : job_task j' \in ts
  ============================
  valid_period (job_task j')

subgoal 2 (ID 1148) is:
 respects_periodic_task_model arr_seq (job_task j')
subgoal 3 (ID 1152) is:
 max_task_offset ts <= job_arrival j'

----------------------------------------------------------------------------- *)

    + now apply H_valid_periods_in_taskset.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1148)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  TSK : job_task
          (corresponding_job_in_hyperperiod ts arr_seq j'
             (starting_instant_of_corresponding_hyperperiod ts j)
             (job_task j')) = job_task j'
  IN : job_task j' \in ts
  ============================
  respects_periodic_task_model arr_seq (job_task j')

subgoal 2 (ID 1152) is:
 max_task_offset ts <= job_arrival j'

----------------------------------------------------------------------------- *)


    + now apply H_periodic_taskset.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1152)
  
  Task : TaskType
  H : TaskOffset Task
  H0 : PeriodicModel Task
  H1 : TaskCost Task
  Job : JobType
  H2 : JobTask Job Task
  H3 : JobArrival Job
  H4 : JobCost Job
  H5 : JobDeadline Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq
  ts : TaskSet Task
  H_periodic_taskset : taskset_respects_periodic_task_model arr_seq ts
  H_valid_periods_in_taskset : valid_periods ts
  H_valid_offsets_in_taskset : valid_offsets arr_seq ts
  j : Job
  H_j_from_arrival_sequence : arrives_in arr_seq j
  O_max := max_task_offset ts : nat
  HP := hyperperiod ts : duration
  H_infinite_jobs : infinite_jobs arr_seq
  H_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
  j' : Job
  ARR : arrives_in arr_seq j'
  A : O_max <= job_arrival j
  NEQ : O_max + HP <= job_arrival j'
  LT : job_arrival j' < O_max + 2 * HP
  TSK : job_task
          (corresponding_job_in_hyperperiod ts arr_seq j'
             (starting_instant_of_corresponding_hyperperiod ts j)
             (job_task j')) = job_task j'
  IN : job_task j' \in ts
  ============================
  max_task_offset ts <= job_arrival j'

----------------------------------------------------------------------------- *)

    + now ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End ValidJobCostsShifted.