Library probsa.rt.analysis.transformation_properties

From probsa.rt.model Require Export pRBF assumptions.basic.
From probsa.rt.analysis Require Export axiomatic_pWCET_full.

Local Open Scope nat_scope.


Properties of the Axiomatic-pWCET Transformation

This file proves that the system after replacing probabilistic execution times (pETs) with their axiomatic pWCETs satisfies key properties required for schedulability analysis.

Structure and Reading Guide

Each section follows a three-step pattern. Step 1: The property holds after one transformation step (single job). Step 2: The property holds after multiple transformation steps. Step 3: The property holds after the complete transformation (all jobs).
For understanding the main results, focus on the Step 3 lemmas in each section since they provide the final guarantees. The intermediate steps (1 and 2) are technical scaffolding for the inductive proof structure.

Preservation of the Sporadic Task Model

First, we prove that if the original system satisfies the sporadic task model, then the transformed system also satisfies the sporadic task model. Since the transformation only changes job costs and not arrival times, this property is preserved.
Section TransformationRespectsSporadicTaskModel.

Consider any type of tasks with a notion of pWCET ...
  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {T : SporadicModel Task}
          {pWCET_pmf : ProbWCET Task}.

...and their jobs.
  Context {Job : finType}
          {job_task : JobTask Job Task}.

Consider a scheduling algorithm ζ that receives two vectors: a vector of arrival times 𝗔 and a vector of job costs 𝗖.
  Variable ζ : @scheduler𝗔𝗖 Job.

Let sched denote a schedule generated by ζ for a given system S.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

First, we show that a single step of the transformation preserves the property in question.
  Section Step1.

Consider a system S.
    Variable S : @system Job.

Next, consider two arbitrary jobs: job j and job j_rep, whose pET we modify.
    Variable (j_rep : Job) (j : Job).

Suppose we use the construction replace_job_pET presented in probsa/rt/analysis/pETs_to_pWCETs to replace the execution cost of given job j_rep. Let S' denote the resulting system.
    Let S' : system := replace_job_pET j_rep S.

Then, given a task set ts, ...
    Variable ts : seq Task.

... if S respects the sporadic task model, then S' also satisfies the sporadic task model.
    Lemma sporadic_task_model_respected_step :
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts →
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts .
    Proof.
      intros × SPO; unfold S' in *; clear S' ⇒ //=.
      destruct S as [Ω μ A C].
      destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
      set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                      pmf_pos := nonneg (job_task j_rep);
                      pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
      intros [ω n].
      specialize (SPO ω).
      intros ? IN j1 j2 NEQ ARR1 ARR2 TSK1 TSK2 LE.
      by apply SPO ⇒ //.
    Qed.

  End Step1.

In the next step, we apply the transformation to an arbitrary subset of jobs jobs.
  Section Step2.

    Variables (ts : seq Task) (jobs : seq Job) (S : @system Job).
    Let S' : system := foldr replace_job_pET S jobs.

    Lemma sporadic_task_model_respected_steps :
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts →
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts.
    Proof.
      induction jobs as [| j_rep jobs']; destruct S as [Ω μ 𝓐 𝓒]; first by done.
      intros SPO ? ?.
      unfold S' in *; clear S'.
      simpl in ω.
      apply sporadic_task_model_respected_step.
      apply IHjobs'.
      by apply SPO.
    Qed.

  End Step2.

Finally, we apply the previous lemma to a set of jobs that coincides with the set of all jobs.
  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Variable ts : seq Task.

    Lemma sporadic_task_model_respected :
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts →
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts.
    Proof.
      by intros; apply sporadic_task_model_respected_steps.
    Qed.

  End Step3.

End TransformationRespectsSporadicTaskModel.

Preservation of the Horizon Property

We prove that if all job deadlines fall before a horizon h in the original system, they also fall before h in the transformed system. Since the transformation does not modify arrival times or task deadlines, this property is trivially preserved.
Section TransformationRespectsBigHorizon.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {T : SporadicModel Task}
          {pWCET_pmf : ProbWCET Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Let job_deadline (S : system) (j : Job) :=
    @job_deadline _ _ _ (@job_deadline_from_task_deadline _ _ _ _ D (𝓐_of S) _) j.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Variable h : instant.
    Hypothesis BIG : ∀ (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.

    Lemma transformation_respects_big_horizon_step :
      ∀ (ω : Ω_of S'), odflt0 (job_deadline S' j) ω < h.
    Proof.
      unfold S' in *; clear S' ⇒ //=.
      destruct S as [Ω μ A C].
      destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
      set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                      pmf_pos := nonneg (job_task j_rep);
                      pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
      intros [ω a].
      by apply BIG.
    Qed.

  End Step1.

  Section Step2.

    Variables (S : @system Job) (jobs : seq Job) (j : Job).
    Let S' : system := foldr replace_job_pET S jobs.

    Variable h : instant.
    Hypothesis H_horizon_big : ∀ (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.

    Lemma transformation_respects_big_horizon_steps :
      ∀ ω, odflt0 (job_deadline S' j) ω < h.
    Proof.
      induction jobs as [| j_rep jobs']; first by done.
      unfold S' in *; clear S'.
      intros ω ⇒ //=.
      apply transformation_respects_big_horizon_step.
      by intros; apply IHjobs'.
    Qed.

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' : system := replace_all_pETs S.

    Variable h : instant.
    Hypothesis H_horizon_big : ∀ (j : Job) (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.

    Lemma transformation_respects_big_horizon :
      ∀ (j : Job) (ω : Ω_of S'),
        odflt0 (job_deadline S' j) ω < h.
    Proof.
      by intros; apply transformation_respects_big_horizon_steps.
    Qed.

  End Step3.

End TransformationRespectsBigHorizon.

Preservation of Arrival-Cost Consistency

We prove that if arrivals and costs are consistent in the original system (i.e., jobs with no arrival have no cost), this consistency is preserved in the transformed system.
Section TransformationRespectsArrivalsCostConsistent.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {T : SporadicModel Task}
          {pWCET_pmf : ProbWCET Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Lemma transformation_respects_consistent_arrivals_step :
      arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
      arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
    Proof.
      intros SOME × ARR; unfold S' in *; clear S' ⇒ //=.
      destruct S as [Ω μ A C].
      destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
      set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                      pmf_pos := nonneg (job_task j_rep);
                      pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
      destruct ω as [ω n].
      destruct (_ == _) eqn:EQ; first by done.
      by apply SOME.
    Qed.

  End Step1.

  Section Step2.

    Variables (jobs_rep : seq Job) (S : @system Job).
    Let S' : system := foldr replace_job_pET S jobs_rep.

    Lemma transformation_respects_consistent_arrivals_steps :
      arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
      arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
    Proof.
      induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒].
      { by simpl in ×. }
      { simpl; intros.
        apply transformation_respects_consistent_arrivals_step.
        by apply IHjobs, H.
      }
    Qed.

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Lemma transformation_respects_consistent_arrivals :
      arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
      arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').
    Proof.
      by intros; apply transformation_respects_consistent_arrivals_steps.
    Qed.

  End Step3.

End TransformationRespectsArrivalsCostConsistent.

Preservation of Arrival Sequences

We prove that the transformation preserves arrival sequences: every arrival sequence in the transformed system corresponds to an arrival sequence in the original system. Since the transformation only modifies costs and not arrivals, the set of possible arrival sequences remains unchanged.
Section TransformationPreservesArrivalSequence.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Variable (S : @system Job) (j_rep : Job).
  Let S' : system := replace_job_pET j_rep S.

  Lemma transformation_preserves_arr_seq :
    ∀ ξ' : imgT (arr_seq (job_arrival := 𝓐_of S')),
    ∃ ξ : imgT (arr_seq (job_arrival := 𝓐_of S)),
    ∀ t, proj1_sig ξ t = proj1_sig ξ' t.
  Proof.
    intros [ξ INS'].
    unshelve econstructor.
    { unshelve econstructor; first by apply ξ.
      unfold S' in *; clear S'.
      destruct S as [Ω μ A C], pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
      move: (INS'); rewrite !unfold_in ⇒ /exCP [[ω n] /eqP EQ].
      apply/exCP; ∃ ω; rewrite -EQ; apply/eqP.
      have FE := @FunctionalExtensionality.functional_extensionality nat (seq Job) (arr_seq ω) (arr_seq (ω, n)).
      by apply: FE ⇒ t; reflexivity.
    }
    { by simpl; intros; reflexivity. }
  Qed.

End TransformationPreservesArrivalSequence.

Identical Distributions and Stochastic Bounds

We prove that after the transformation two new properties hold. (1) All jobs of the same task have identically distributed costs. And (2) job costs are stochastically dominated by (and dominate) their task's pWCET.
Section TransformationEnsuresIdenticalCosts.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' := replace_job_pET j_rep S.

    Section CostBoundedByPWCET.

      Variable tsk : Task.
      Hypothesis H_job_of_task : job_of_task tsk j_rep.

      Lemma replaced_pETs_bounded_by_pWCETs_step :
        odflt0 (𝓒_of S' j_rep) ⪯ to_distrib pWCET_pmf tsk.
      Proof.
        unfold S' in *; clear S' ⇒ //=.
        destruct S as [Ω μ A C].
        destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                        pmf_pos := nonneg (job_task j_rep);
                        pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
        rewrite eq_refl ⇒ k.
        rewrite (pr_joint_pred_eq _ _ _ (fun ω ⇒ true) (fun ω ⇒ ω ≤ k)).
        { rewrite pr_xpredT Rmult_1_l.
          by move: H_job_of_task ⇒ /eqP TSK2; rewrite /μ_tsk -TSK2; apply Rge_refl. }
        { by intros [ω n]. }
      Qed.

      Lemma pWCETs_bounded_by_replaced_pETs_step :
        to_distrib pWCET_pmf tsk ⪯ odflt0 (𝓒_of S' j_rep).
      Proof.
        unfold S' in *; clear S' ⇒ //=.
        destruct S as [Ω μ A C].
        destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                        pmf_pos := nonneg (job_task j_rep);
                        pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
        rewrite eq_refl ⇒ k.
        rewrite (pr_joint_pred_eq _ _ _ (fun ω ⇒ true) (fun ω ⇒ ω ≤ k)).
        { rewrite pr_xpredT Rmult_1_l.
          by move: H_job_of_task ⇒ /eqP TSKo; rewrite /μ_tsk -TSKo; apply Rge_refl. }
        { by intros [ω n]. }
      Qed.

    End CostBoundedByPWCET.

    Section CostBounds.

      Hypothesis H_jobs_neq : j_rep != j.

      Lemma nonreplaced_pETs_dont_change_1_step :
        odflt0 (𝓒_of S' j) ⪯ odflt0 (𝓒_of S j).
      Proof.
        unfold S' in *; clear S' ⇒ //=.
        destruct S as [Ω μ A C].
        destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                        pmf_pos := nonneg (job_task j_rep);
                        pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
        have NEQ2 : (j_rep == j) = false by apply/eqP/eqP.
        rewrite NEQ2 ⇒ k; rewrite /cdf.
        rewrite (pr_joint_pred_eq _ _ _ (odflt0 (C j) ⟨<=⟩ k) (fun ω ⇒ true)).
        { by rewrite pr_xpredT Rmult_1_r; apply Rge_refl. }
        { by intros [ω n]; rewrite andbT. }
      Qed.

      Lemma nonreplaced_pETs_dont_change_2_step :
        odflt0 (𝓒_of S j) ⪯ odflt0 (𝓒_of S' j).
      Proof.
        unfold S' in *; clear S' ⇒ //=.
        destruct S as [Ω μ A C].
        destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                        pmf_pos := nonneg (job_task j_rep);
                        pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
        have NEQ2 : (j_rep == j) = false by apply/eqP/eqP.
        rewrite NEQ2 ⇒ k; rewrite /cdf.
        rewrite (pr_joint_pred_eq _ _ _ (odflt0 (C j) ⟨<=⟩ k) (fun ω ⇒ true)).
        { by rewrite pr_xpredT Rmult_1_r; apply Rge_refl. }
        { by intros [ω n]; rewrite andbT. }
      Qed.

    End CostBounds.

  End Step1.

  Section Step2.

    Variable jobs_rep : seq Job.
    Hypothesis H_jobs_uniq : uniq jobs_rep.

    Variable S : @system Job.
    Let S' := foldr replace_job_pET S jobs_rep.

    Variables (j : Job) (tsk : Task).
    Hypothesis H_j_in_reps : j \in jobs_rep.
    Hypothesis H_job_of_task : job_of_task tsk j.

    Lemma replaced_pETs_bounded_by_pWCETs_steps :
      odflt0 (𝓒_of S' j) ⪯ to_distrib pWCET_pmf tsk.
    Proof.
      induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒]; first by done.
      unfold S' in *; clear S'.
      move: H_j_in_reps; rewrite in_cons ⇒ /orP [/eqP EQ | IN] TSK.
      { by subst j_rep; apply replaced_pETs_bounded_by_pWCETs_step ⇒ //. }
      { apply: Rge_trans; first apply nonreplaced_pETs_dont_change_1_step.
        { by apply/eqP ⇒ EQ; subst; move: H_jobs_uniq; rewrite //= IN andFb. }
        apply IHjobs ⇒ //.
        by move: H_jobs_uniq; simpl ⇒ /andP [_ UNIQo]; apply: UNIQo.
      }
    Qed.

    Lemma pWCETs_bounded_by_replaced_pETs_steps :
      to_distrib pWCET_pmf tsk ⪯ odflt0 (𝓒_of S' j).
    Proof.
      induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒]; first by done.
      unfold S' in *; clear S'.
      move: H_j_in_reps; rewrite in_cons ⇒ /orP [/eqP EQ | IN] TSK.
      { by subst j_rep; apply pWCETs_bounded_by_replaced_pETs_step ⇒ //. }
      { apply: Rge_trans; last apply nonreplaced_pETs_dont_change_2_step; last first.
        { by apply/eqP ⇒ EQ; subst; move: H_jobs_uniq; rewrite //= IN andFb. }
        apply IHjobs ⇒ //.
        by move: H_jobs_uniq; simpl ⇒ /andP [_ UNIQo]; apply: UNIQo.
      }
    Qed.

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Lemma replaced_pETs_bounded_by_pWCETs :
      ∀ (j : Job) (tsko : Task),
        job_of_task tsko j →
        odflt0 (𝓒_of S' j) ⪯ to_distrib pWCET_pmf tsko.
    Proof.
      intros; apply replaced_pETs_bounded_by_pWCETs_steps ⇒ //.
      - by apply index_enum_uniq.
      - by apply mem_index_enum.
    Qed.

    Lemma pWCETs_bounded_by_replaced_pETs :
      ∀ (j : Job) (tsko : Task),
        job_of_task tsko j →
        to_distrib pWCET_pmf tsko ⪯ odflt0 (𝓒_of S' j).
    Proof.
      intros; apply pWCETs_bounded_by_replaced_pETs_steps ⇒ //.
      - by apply index_enum_uniq.
      - by apply mem_index_enum.
    Qed.

    Lemma pETs_have_same_distribution :
      ∀ (j1 j2 : Job),
        job_task j1 = job_task j2 →
        odflt0 (𝓒_of S' j1) ⪯ odflt0 (𝓒_of S' j2).
    Proof.
      intros × TSK.
      apply: func_dom_trans.
      { apply replaced_pETs_bounded_by_pWCETs_steps.
        - by apply index_enum_uniq.
        - by apply mem_index_enum.
        - by rewrite /job_of_task /concept.job_task.
      }
      { apply pWCETs_bounded_by_replaced_pETs_steps.
        - by apply index_enum_uniq.
        - by apply mem_index_enum.
        - by rewrite TSK /job_of_task /concept.job_task.
      }
    Qed.

  End Step3.

End TransformationEnsuresIdenticalCosts.

Independence of Job Costs

We prove that all job costs are jointly independent in the transformed system. This property is established by the transformation itself: since each job's cost is sampled independently from its task's pWCET distribution, the costs are independent regardless of whether the original pETs were independent.
Section TransformationEnsuresIndependentCosts.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Variable jobs : seq Job.
    Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.

    Lemma replaced_pETs_are_independent_step :
      indep2 (𝓒_of S' j_rep) (rvar_list [seq 𝓒_of S' j | j <- jobs]).
    Proof.
      unfold S' in *; clear S' ⇒ //=.
      destruct S as [Ω μ A C].
      destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
      set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                      pmf_pos := nonneg (job_task j_rep);
                      pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
      intros a b; rewrite /pr_eq.
      have EQ : ∀ a b c, a = b → ((a == c) = (b == c)).
      { clear. intros. subst. by done. }
      rewrite (pr_joint_pred_eq
                 _ _ _
                 (fun (ω : Ω) ⇒ (rvar_list [seq C j | j <- jobs]) ω == b)
                 (fun (ω : nat) ⇒ Some ω == a)); last first.
      { intros [ω n]; rewrite eq_refl andbC; f_equal.
        simpl; apply: EQ.
        induction jobs as [ | jo jobso]; first by done.
        rewrite //= IHjobso; clear IHjobso; last first.
        { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
        apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
        have NEQ: j_rep == jo = false.
        { by apply/negP ⇒ /eqP EQ; subst; move: (H_jrep_notin_jobs); rewrite in_cons eq_refl orTb. }
        by rewrite NEQ.
      }
      rewrite (pr_joint_pred_eq _ _ _ xpredT (fun ω ⇒ Some ω == a)); last first.
      { by rewrite eq_refl //=; intros [ω n]. }
      rewrite (pr_joint_pred_eq
                 _ _ _ (fun (ω : Ω) ⇒ (rvar_list [seq C j | j <- jobs]) ω == b) xpredT
              ); last first.
      { intros [ω n]; rewrite //= andbT; apply: EQ.
        induction jobs as [ | jo jobso]; first by done.
        rewrite //= IHjobso; clear IHjobso; last first.
        { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
        apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
        have NEQ: j_rep == jo = false.
        { by apply/negP ⇒ /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb. }
        by rewrite NEQ.
      }
      by rewrite !pr_xpredT Rmult_1_l Rmult_1_r Rmult_comm.
    Qed.

    Lemma transformation_respects_independence_step :
      independent [seq 𝓒_of S j | j <- jobs] →
      independent [seq 𝓒_of S' j | j <- jobs].
    Proof.
      intros IND cs LEN; unfold S' in *; clear S' ⇒ //=.
      destruct S as [Ω μ A C].
      destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
      set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                      pmf_pos := nonneg (job_task j_rep);
                      pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
      apply: eq_tr4.
      { apply IND.
        rewrite -!seq_ext.size_legacy size_map; rewrite -!seq_ext.size_legacy size_map in LEN.
        by apply LEN.
      }
      { rewrite (pr_joint_pred_eq
                   _ _ _ (fun (ω : Ω) ⇒ (rvar_list [seq C j | j <- jobs]) ω == cs) xpredT
                ); last first.
        { intros [ω n]; rewrite andbT zip_foldr_andb_seq_eq; last first.
          { by move: LEN; rewrite -!seq_ext.size_legacy !size_map ⇒ →. }
          move: cs LEN; clear IND.
          induction jobs as [ | jo jobso]; first by intros [].
          intros []; first by done.
          rewrite -!seq_ext.size_legacy !size_map //= ⇒ LEN; apply eq_add_S in LEN.
          rewrite IHjobso; f_equal.
          { by have ->: j_rep == jo = false
              by apply/negP ⇒ /eqP EQ; subst; move: (H_jrep_notin_jobs); rewrite in_cons eq_refl orTb. }
          { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
          { by rewrite -!seq_ext.size_legacy !size_map. }
        }
        { rewrite !pr_xpredT Rmult_1_r.
          apply pr_eq_pred ⇒ ω; rewrite !unfold_in zip_foldr_andb_seq_eq; last first.
          { by move: LEN; rewrite -!seq_ext.size_legacy !size_map ⇒ →. }
          f_equal; rewrite !zip_map_rvar_eq; f_equal; f_equal.
          by clear; induction jobs as [ | jo jobso]; [done | rewrite //= -IHjobso].
        }
      }
      { f_equal; rewrite !zip_map_pr_eq.
        move: cs LEN; clear IND; induction jobs as [ | jo jobso]; first by intros [].
        intros []; first by done.
        rewrite -!seq_ext.size_legacy !size_map //= ⇒ LEN; apply eq_add_S in LEN.
        rewrite IHjobso; f_equal.
        { have NEQ: j_rep == jo = false.
          { by apply/negP ⇒ /eqP EQ; subst; move: (H_jrep_notin_jobs); rewrite in_cons eq_refl orTb. }
          rewrite /pr_eq (pr_joint_pred_eq _ _ _ (fun ω ⇒ C jo ω == o) xpredT); last first.
          { by rewrite NEQ //=; intros [ω n]; rewrite andbT. }
          by rewrite pr_xpredT Rmult_1_r.
        }
        { by apply/negP; intros IN; move: (H_jrep_notin_jobs); rewrite in_cons IN orbT. }
        { by rewrite -!seq_ext.size_legacy !size_map. }
      }
    Qed.

  End Step1.

  Section Step2.

    Variable jobs_rep : seq Job.
    Hypothesis H_jobs_uniq : uniq jobs_rep.

    Variable S : @system Job.
    Let S' : system := foldr replace_job_pET S jobs_rep.

    Lemma replaced_pETs_are_independent_steps :
      independent [seq 𝓒_of S' j | j <- jobs_rep].
    Proof.
      induction jobs_rep as [| j_rep jobs]; destruct S as [Ω μ 𝓐 𝓒].
      { by intros; apply independent_nil. }
      { intros; simpl.
        apply indep2_independent_cons.
        { by apply replaced_pETs_are_independent_step; move: H_jobs_uniq ⇒ /andP [H _]. }
        { apply transformation_respects_independence_step ⇒ //.
          by move: H_jobs_uniq ⇒ /andP [H _].
          apply IHjobs.
          by move: H_jobs_uniq ⇒ /andP [_ H].
        }
      }
    Qed.

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' : system := replace_all_pETs S.

    Lemma replaced_pETs_are_independent :
      independent [seq 𝓒_of S' j | j <- index_enum Job].
    Proof.
      intros; apply replaced_pETs_are_independent_steps.
      by apply index_enum_uniq.
    Qed.

  End Step3.

End TransformationEnsuresIndependentCosts.

Independence from Arrival Sequences and Conditional Independence

We prove that in the transformed system three new properties hold. (1) Job costs are independent of the arrival sequence. (2) Job costs are jointly independent when conditioned on any fixed arrival sequence. (3) Conditional job costs are bounded by pWCETs. These properties are established by the transformation: each job's cost is sampled from its task's pWCET distribution independently of arrivals.
Section TransformationEnsuresCostsIndependentFromArrivals.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Section IndependentArrSeq.

      Variable ξa : arrival_sequence Job.
      Let ξf := ξ_fix (arr_seq (job_arrival := 𝓐_of S)) ξa.
      Let ξf' := ξ_fix (arr_seq (job_arrival := 𝓐_of S')) ξa.

      Variable jobs : seq Job.
      Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.

      Lemma transformation_respects_pET_indep_arr_seq_cons_step :
        @indep2 _ _ _ (μ_of S)
                {| rvar_fun := λ ω, [seq 𝓒_of S j0 ω | j0 <- jobs] |}
                {| rvar_fun := ξf |} →
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- j_rep :: jobs] |}
                {| rvar_fun := ξf' |}.
      Proof.
        intros IND; unfold S' in *; clear S'.
        destruct S as [Ω μ A C]; destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        intros [ | c cs] b.
        { rewrite //= pr_xpred0 /pr_eq eq_refl //=; symmetry.
          by apply Rmult_eq_0_compat_r; apply pr_zero ⇒ [ω n]. }
        { rewrite (pr_joint_pred_eq
                     _ _ _
                     (fun (ω : Ω) ⇒ ((rvar_list [seq C j | j <- jobs]) ω == cs) && (ξf ω == b))
                     (fun (ω : nat) ⇒ Some ω == c)); last first.
          { intros [ω n] ⇒ //=; rewrite eq_refl eqseq_cons -andbA andbC; do 3 f_equal.
            clear IND; induction jobs as [ | jo jobso]; first by done.
            rewrite //= IHjobso; clear IHjobso; last first.
            { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
            apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
            have NEQ: j_rep == jo = false.
            { by apply/negP ⇒ /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb. }
            by rewrite NEQ.
          }
          rewrite /pr_eq (pr_joint_pred_eq
                            _ _ _
                            (fun ω ⇒ ((rvar_list [seq C j | j <- jobs]) ω == cs))
                            (fun ω ⇒ Some ω == c)); last first.
          { intros [ω n] ⇒ //=; rewrite eq_refl eqseq_cons andbC; do 2 f_equal.
            clear IND; induction jobs as [ | jo jobso]; first by done.
            rewrite //= IHjobso; clear IHjobso; last first.
            { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
            apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
            by have ->: j_rep == jo = false
              by apply/negP ⇒ /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb.
          }
          rewrite /pr_eq (pr_joint_pred_eq
                            _ _ _ (fun (ω : Ω) ⇒ (ξf ω == b)) (xpredT)); last first.
          { by intros [ω n]; rewrite andbT; reflexivity. }
          rewrite pr_xpredT Rmult_1_r Rmult_comm.
          symmetry; rewrite Rmult_assoc Rmult_comm Rmult_assoc; apply Rmult_eq_compat_l; symmetry.
          apply: eq_tr4; first apply (IND cs b).
          { apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=.
            by do 2 f_equal; clear IND H_jrep_notin_jobs;
            induction jobs as [ | jo jobso]; [ | rewrite //= IHjobso].
          }
          { rewrite Rmult_comm; apply Rmult_eq_compat_r.
            apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=.
            by do 2 f_equal; clear IND H_jrep_notin_jobs;
            induction jobs as [ | jo jobso]; [ | rewrite //= IHjobso].
          }
        }
      Qed.

      Lemma transformation_respects_pET_indep_arr_seq_eq_step :
        @indep2 _ _ _ (μ_of S)
                {| rvar_fun := λ ω, [seq 𝓒_of S j ω | j <- jobs] |}
                {| rvar_fun := ξf |} →
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω, [seq 𝓒_of S' j ω | j <- jobs] |}
                {| rvar_fun := ξf' |}.
      Proof.
        intros IND; unfold S' in *; clear S'.
        destruct S as [Ω μ A C]; destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        intros cs b.
        rewrite (pr_joint_pred_eq
                   _ _ _ (fun ω ⇒ ((rvar_list [seq C j | j <- jobs]) ω == cs) && (ξf ω == b)) xpredT
                ); last first.
        { intros [ω n] ⇒ //=. rewrite andbT; do 2 f_equal.
          clear IND; induction jobs as [ | jo jobso]; first by done.
          rewrite //= IHjobso; clear IHjobso; last first.
          { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
          apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
          by have ->: j_rep == jo = false
            by apply/negP ⇒ /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb.
        }
        rewrite /pr_eq (pr_joint_pred_eq
                          _ _ _ (fun ω ⇒ ((rvar_list [seq C j | j <- jobs]) ω == cs)) xpredT
                       ); last first.
        { intros [ω n] ⇒ //=; rewrite andbT; do 2 f_equal.
          clear IND; induction jobs as [ | jo jobso]; first by done.
          rewrite //= IHjobso; clear IHjobso; last first.
          { by apply/negP; intros IN; move: H_jrep_notin_jobs; rewrite in_cons IN orbT. }
          apply/eqP; rewrite eqseq_cons; apply/andP; split; last by done.
          by have ->: j_rep == jo = false
            by apply/negP ⇒ /eqP EQ; subst; move: H_jrep_notin_jobs; rewrite in_cons eq_refl orTb.
        }
        rewrite /pr_eq (pr_joint_pred_eq _ _ _ (fun ω ⇒ (ξf ω == b)) (xpredT)); last first.
        { by intros [ω n]; rewrite andbT; reflexivity. }
        rewrite pr_xpredT Rmult_comm !Rmult_1_r !Rmult_1_l.
        apply: eq_tr4; first apply (IND cs b).
        { apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=.
          by do 2 f_equal; clear IND H_jrep_notin_jobs;
          induction jobs as [| jo jobso] ; [ | rewrite //= IHjobso]. }
        { apply Rmult_eq_compat_r.
          apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=.
          by do 2 f_equal; clear IND H_jrep_notin_jobs;
          induction jobs as [| jo jobso]; [ | rewrite //= IHjobso]. }
      Qed.

      Lemma transformation_respects_pET_indep_arr_seq_remove_step :
          @indep2 _ _ _ (μ_of S)
                  {| rvar_fun := λ ω, [seq 𝓒_of S j0 ω | j0 <- jobs & predC1 j0 j_rep] |}
                  {| rvar_fun := ξf |} →
          @indep2 _ _ _ (μ_of S')
                  {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                  {| rvar_fun := ξf' |}.
      Proof.
        intros IND; unfold S' in *; clear S'.
        destruct S as [Ω μ A C]; destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        intros cs b.
        have [/eqP SEQ|SNEQ] := boolP (size cs == size jobs); last first.
        { apply eq_tr3 with 0%R.
          { apply pr_zero ⇒ [ω n]; apply/eqP.
            rewrite eqbF_neg negb_and; apply/orP; left.
            apply/negP ⇒ /eqP EQ; subst cs.
            move: SNEQ ⇒ /negP SNEQ; apply: SNEQ.
            by rewrite size_map.
          }
          { symmetry; apply Rmult_eq_0_compat_r.
            apply pr_zero ⇒ [ω n]; apply/eqP ⇒ EQ; subst cs.
            move: SNEQ ⇒ /negP SNEQ; apply: SNEQ.
            by rewrite size_map.
          }
        }
        set (csN := [seq p.2 | p <- zip jobs cs & j_rep != p.1]).
        set (csE := [seq p.2 | p <- zip jobs cs & j_rep == p.1]).
        rewrite /pr_eq (pr_joint_pred_eq
                   _ _ _
                   (fun (ω : Ω) ⇒ ((rvar_list [seq C j | j <- jobs & j_rep != j]) ω == csN) && (ξf ω == b))
                   (fun (n : nat) ⇒ [seq Some n | j <- jobs & j_rep == j] == csE)
                ); last first.
        { intros [ω n]; symmetry; rewrite andbC andbA.
          f_equal; unfold csN, csE; clear csN csE H_jrep_notin_jobs IND.
          move: cs SEQ; induction jobs as [|jo jobso]; first by intros [].
          intros []; first by done.
          intros; simpl.
          have [/eqP EQa | NEQa] := boolP (j_rep == jo).
          { by rewrite //= !eqseq_cons -IHjobso;
            [rewrite andbA; f_equal | apply eq_add_S, SEQ]. }
          { by rewrite //= !eqseq_cons -IHjobso;
              [rewrite andbC -!andbA; f_equal; rewrite andbC; f_equal
              | apply eq_add_S, SEQ]. }
        }
        rewrite (pr_joint_pred_eq
                   _ _ _
                   (fun (ω : Ω) ⇒ ((rvar_list [seq C j | j <- jobs & j_rep != j]) ω == csN))
                   (fun (n : nat) ⇒ [seq Some n | j <- jobs & j_rep == j] == csE)
                ); last first.
        { intros [ω n]; symmetry.
          unfold csN, csE; clear csN csE H_jrep_notin_jobs IND; move: cs SEQ.
          induction jobs as [ | jo jobso]; first by intros [].
          intros []; [by done | intros; simpl].
          have [/eqP EQa | NEQa] := boolP (j_rep == jo).
          { by rewrite //= !eqseq_cons -IHjobso;
            [rewrite andbC -!andbA; f_equal; rewrite andbC; f_equal
            | apply eq_add_S, SEQ]. }
          { by rewrite //= !eqseq_cons -IHjobso;
            [rewrite andbA; f_equal | apply eq_add_S, SEQ]. }
        }
        rewrite /pr_eq (pr_joint_pred_eq _ _ _ (fun ω ⇒ ξf ω == b) xpredT); last first.
        { by intros [ω n]; rewrite andbT; reflexivity. }
        rewrite pr_xpredT Rmult_comm !Rmult_1_r.
        set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                        pmf_pos := nonneg (job_task j_rep);
                        pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
        symmetry; rewrite Rmult_assoc Rmult_comm Rmult_assoc; apply Rmult_eq_compat_l; symmetry.
        apply: eq_tr4; first apply (IND csN b).
        { apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=; unfold csN in ×.
          do 2 f_equal; clear IND H_jrep_notin_jobs csN csE; move: cs SEQ.
          induction jobs as [| jo jobso]; first by done.
          intros []; [by done | intros; simpl].
          (have [/eqP EQa | NEQa] := boolP (j_rep == jo));
            by simpl; erewrite IHjobso; [reflexivity | apply eq_add_S, SEQ].
        }
        { rewrite Rmult_comm; apply Rmult_eq_compat_r.
          rewrite /pr_eq; apply pr_eq_pred ⇒ ω; rewrite !unfold_in //=; unfold csN in ×.
          do 2 f_equal; clear IND H_jrep_notin_jobs csN csE; move: cs SEQ.
          induction jobs as [| jo jobso]; first by done.
          intros []; [by done | intros; simpl].
          (have [/eqP EQa | NEQa] := boolP (j_rep == jo));
            by simpl; erewrite IHjobso; [reflexivity | apply eq_add_S, SEQ].
        }
      Qed.

    End IndependentArrSeq.

    Section IndependentArrSeqPartition.

      Variable jobs : seq Job.
      Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.

      Lemma transformation_respects_pET_indep_arr_seq_eq_part_step :
        (∀ (ξpart := @partition_on_ξ (Ω_of S) (μ_of S) Job (𝓐_of S)) (ξ : I ξpart),
            @indep2 _ _ _ (μ_of S)
                    {| rvar_fun := λ ω : Ω_of S, [seq 𝓒_of S j0 ω | j0 <- jobs] |}
                    {| rvar_fun := [eta ξpart◁{ξ}] |}
        ) →
        ∀ (ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S')) (ξ : I ξpart),
          @indep2 _ _ _ (μ_of S')
                  {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                  {| rvar_fun := [eta ξpart◁{ξ}] |}.
      Proof.
        intros IND *; apply transformation_respects_pET_indep_arr_seq_eq_step ⇒ //.
        rename ξ into ξs'.
        have [ξs EQ] := transformation_preserves_arr_seq _ _ ξs'; simpl in EQ.
        destruct S as [Ω μ A C].
        destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                        pmf_pos := nonneg (job_task j_rep);
                        pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
        specialize (IND ξs); destruct ξs' as [ξ' INξ'], ξs as [ξ INξ].
        intros ? ?; apply: eq_tr4; first by apply IND.
        { apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
          f_equal ⇒ //=; unfold ξ_fix; do 2 f_equal.
          simpl in EQ; clear INξ' IND INξ.
          apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
          by intros; symmetry; apply EQ.
        }
        { f_equal; apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
          f_equal ⇒ //=; unfold ξ_fix; f_equal.
          apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
          by intros; symmetry; apply EQ.
        }
      Qed.

      Lemma transformation_respects_pET_indep_arr_seq_remove_part_step :
        (∀ (ξpart := @partition_on_ξ (Ω_of S) (μ_of S) Job (𝓐_of S)) (ξ : I ξpart),
            @indep2 _ _ _ (μ_of S)
                    {| rvar_fun := λ ω : Ω_of S, [seq 𝓒_of S j0 ω | j0 <- jobs & predC1 j0 j_rep] |}
                    {| rvar_fun := [eta ξpart◁{ξ}] |}
        ) →
        ∀ (ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S')) (ξ : I ξpart),
          @indep2 _ _ _ (μ_of S')
                  {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                  {| rvar_fun := [eta ξpart◁{ξ}] |}.
      Proof.
        intros IND *; apply transformation_respects_pET_indep_arr_seq_remove_step ⇒ //.
        rename ξ into ξs'.
        have [ξs EQ] := transformation_preserves_arr_seq _ _ ξs'; simpl in EQ.
        destruct S as [Ω μ A C].
        destruct pWCET_pmf as [pWCET nonneg sum1]; simpl in ×.
        set (μ_tsk := {| pmf := pWCET (job_task j_rep);
                        pmf_pos := nonneg (job_task j_rep);
                        pmf_sum1 := sum1 (job_task j_rep) |}) in ×.
        specialize (IND ξs); destruct ξs' as [ξ' INξ'], ξs as [ξ INξ].
        intros ? ?; apply: eq_tr4; first by apply IND.
        { apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
          f_equal ⇒ //=; unfold ξ_fix; do 2 f_equal.
          simpl in EQ; clear INξ' IND INξ.
          apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
          by intros; symmetry; apply EQ.
        }
        { f_equal; apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
          f_equal ⇒ //=; unfold ξ_fix; f_equal.
          apply (@FunctionalExtensionality.functional_extensionality _ _ ξ' ξ).
          by intros; symmetry; apply EQ.
        }
      Qed.

    End IndependentArrSeqPartition.

  End Step1.

  Section Step2.

    Variable jobs_rep : seq Job.
    Hypothesis H_jrep_notin_jobs : uniq jobs_rep.

    Variable S : @system Job.
    Let S' : system := foldr replace_job_pET S jobs_rep.

    Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
    Variable (ξ : I ξpart).

    Lemma replaced_pETs_are_independent_from_arr_seq_partition_steps :
      ∀ (jobs : seq Job),
        (∀ j, j \in jobs → j \in jobs_rep) →
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                {| rvar_fun := [eta ξpart◁{ξ}] |}.
    Proof.
      induction jobs_rep as [| j_rep jobs_repo]; destruct S as [Ω μ 𝓐 𝓒].
      { intros; destruct jobs.
        { intros [] ?; simpl.
          { by symmetry; rewrite /pr_eq //= pr_xpredT_ext // Rmult_1_l. }
          { by rewrite //= pr_xpred0; symmetry; apply Rmult_eq_0_compat_r, pr_zero. }
        }
        { exfalso; specialize (H s); feed H; last by done.
          by rewrite in_cons eq_refl orTb.
        }
      }
      { intros × SUB; set (ξe := {| rvar_fun := [eta ξpart◁{ξ}] |}).
        have [IN|NIN] := boolP (j_rep \in jobs).
        { apply transformation_respects_pET_indep_arr_seq_remove_part_step ⇒ //; intros.
          apply IHjobs_repo; first by move: H_jrep_notin_jobs ⇒ /andP [_ T].
          intros *; rewrite mem_filter /predC1.
          move ⇒ /andP [NEQ INj]; specialize (SUB _ INj).
          move: SUB; rewrite in_cons.
          move ⇒ /orP [/eqP EQ| INr] ⇒ //; subst.
          by simpl in NEQ; rewrite eq_refl in NEQ.
        }
        { apply transformation_respects_pET_indep_arr_seq_eq_part_step ⇒ //; intros.
          apply IHjobs_repo; first by move: H_jrep_notin_jobs ⇒ /andP [_ T].
          intros; specialize (SUB _ H).
          move: SUB; rewrite in_cons.
          move ⇒ /orP [/eqP EQ| INr] ⇒ //.
          by subst; move: NIN; rewrite H.
        }
      }
    Qed.

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
    Variable (ξ : I ξpart).
    Variable (ρ : PosProb (μ_of S') (ξpart◁{ξ})).

We prove that job costs (as a collection) are independent of the arrival sequence partition indicator. That is, knowing which arrival sequence ξ occurred doesn't provide information about job costs, and vice versa.
    Lemma replaced_pETs_are_independent_from_arr_seq_partition :
      ∀ (jobs : seq Job),
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                {| rvar_fun := [eta ξpart◁{ξ}] |}.
    Proof.
      intros.
      apply replaced_pETs_are_independent_from_arr_seq_partition_steps.
      apply index_enum_uniq.
      by intros; apply mem_index_enum.
    Qed.

Job costs remain jointly independent when conditioned on a fixed arrival sequence ξ. That is, even after observing which arrival pattern occurred, the job costs are still independent of each other.
    Lemma replaced_pETs_are_cond_independent :
      @independent
        _ _ (restrict (μ_of S') (ξpart◁{ξ}))
        [seq mkRvar _ (𝓒_of S' j) | j <- index_enum Job].
    Proof.
      intros ? LEN.
      rewrite -!seq_ext.size_legacy size_map in LEN.
      rewrite fold_prob_to_cond_prob pr_cond_indep2; last first.
      { eapply indep2_fn_extl with
          (X1 := {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- index_enum Job] |})
          (f := fun X1 ⇒ fold_right andb true [seq Xb.1 == Xb.2 | Xb <- seq.zip X1 lb]).
        { by intros; rewrite //= zip_map_rvar_eq; reflexivity. }
        { by apply replaced_pETs_are_independent_from_arr_seq_partition. }
      }
      apply: eq_tr4.
      { by apply replaced_pETs_are_independent; rewrite -!seq_ext.size_legacy size_map; apply LEN. }
      { apply pr_eq_pred ⇒ ω; rewrite !unfold_in.
        by f_equal; rewrite !zip_map_rvar_eq; f_equal.
      }
      { rewrite !zip_map_pr_eq !foldr_big !big_map; apply eq_big; first by done.
        intros [j t] _; rewrite /pr_eq fold_prob_to_cond_prob pr_cond_indep2; first by reflexivity.
        eapply indep2_fn_extl with
          (X1 := {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- [::j]] |})
          (f := fun X1 ⇒ fold_right andb true [seq Xb.1 == Xb.2 | Xb <- seq.zip X1 [::t]]).
        { by intros; rewrite //= andbT; reflexivity. }
        { by apply replaced_pETs_are_independent_from_arr_seq_partition. }
      }
    Qed.

  End Step3.

End TransformationEnsuresCostsIndependentFromArrivals.

Conditional Cost Bounds

In the last section, we prove that job costs conditioned on a fixed arrival sequence are still bounded by their task's pWCET distribution in the transformed system.
Section TransformationEnsuresCondCostsBounded.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Variable S : @system Job.
  Let S' := replace_all_pETs S.

  Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
  Variable (ξ : I ξpart).
  Variable (ρ : PosProb (μ_of S') (ξpart◁{ξ})).

The cost of job j, conditioned on arrival sequence ξ, is stochastically dominated by the pWCET of its task.
  Lemma replaced_cond_pETs_bounded_by_pWCETs :
    ∀ (j : Job) (tsk : Task),
      job_of_task tsk j →
      mkRvar (restrict (μ_of S') (ξpart◁{ξ})) [eta odflt0 (𝓒_of S' j)] ⪯ to_distrib pWCET_pmf tsk.
  Proof.
    intros; intros ?.
    rewrite fold_prob_to_cond_prob.
    rewrite pr_cond_indep2; last first.
    { apply indep2_fn_extl with (X1 := {| rvar_fun := [eta odflt0 (𝓒_of S' j)] |}) (f := fun X1 ⇒ X1 ≤ h).
      { by intros; reflexivity. }
      apply indep2_fn_extl with (X1 := 𝓒_of S' j) (f := odflt 0).
      { by intros; reflexivity. }
      apply indep2_fn_extl with
        (X1 := {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- [::j]] |})
        (f := head None).
      { by intros; reflexivity. }
      apply replaced_pETs_are_independent_from_arr_seq_partition.
    }
    by eapply Rge_trans, replaced_pETs_bounded_by_pWCETs, H; apply Rge_refl.
  Qed.

End TransformationEnsuresCondCostsBounded.