Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1709 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(64 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(617 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(67 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(449 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(33 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(41 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(31 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(159 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(35 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(161 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(35 entries)

---

Global Index

A

abortion_readiness_is_nonclairvoyant [lemma, in probsa.rt.analysis.scheduler_properties]
abort_ready_instance [instance, in probsa.rt.model.abort_readiness]
abort_readiness [library]
AddOp [record, in probsa.util.notation]
AddOp [inductive, in probsa.util.notation]
addrv_addmpf_respect_ltn [lemma, in probsa.probability.pmf]
addrv_addmpf_respect_stochastic_order [lemma, in probsa.probability.pmf]
addrv_respects_stochastic_order [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_7 [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_6 [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_5 [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_5a [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_4 [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_3 [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_3a [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_2 [lemma, in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_1 [lemma, in probsa.probability.stochastic_order]
addrv_leq_decomposition [lemma, in probsa.probability.stochastic_order]
addrv_eq_decomposition [lemma, in probsa.probability.stochastic_order]
addrv_comm [lemma, in probsa.probability.stochastic_order]
add_op [projection, in probsa.util.notation]
add_op [constructor, in probsa.util.notation]
allpairs_rvar [lemma, in probsa.probability.prob]
andA [lemma, in probsa.util.boolp]
andC [lemma, in probsa.util.boolp]
and_asboolP [lemma, in probsa.util.boolp]
and3_asboolP [lemma, in probsa.util.boolp]
AntiSymm [record, in probsa.util.stdpp]
AntiSymm [inductive, in probsa.util.stdpp]
anti_symm [projection, in probsa.util.stdpp]
anti_symm [constructor, in probsa.util.stdpp]
apt [definition, in probsa.probability.law_of_total_prob]
apt_double_summable_by_column [lemma, in probsa.probability.law_of_total_prob]
apt_row_rewrite [lemma, in probsa.probability.law_of_total_prob]
arrivals [library]
ArrivalsConsistentWithDeadlines [section, in probsa.rt.model.assumptions.basic]
ArrivalsConsistentWithDeadlines.H_arrivals_consistent [variable, in probsa.rt.model.assumptions.basic]
ArrivalsPartition [section, in probsa.rt.model.events]
arrivals_consistent_with_deadlines [lemma, in probsa.rt.model.assumptions.basic]
arrivals_cost_consistent [definition, in probsa.rt.model.assumptions.basic]
arrivals_from_task_set [definition, in probsa.rt.model.assumptions.basic]
arrivals_between_sorted [lemma, in probsa.util.prosa.arrival_bound]
arrivals_at_sorted [lemma, in probsa.util.prosa.arrival_bound]
arrival_of_nth_job [lemma, in probsa.util.prosa.arrival_bound]
arrival_sequence [library]
arrival_bound [library]
arrow_choiceType [definition, in probsa.util.boolp]
arrow_eqType [definition, in probsa.util.boolp]
ArrSeqAndJobArrivalAgree [section, in probsa.rt.behavior.arrival_sequence]
ArrSeqForFinTypeJobs [section, in probsa.rt.behavior.arrival_sequence]
ArrSeqUniq [section, in probsa.rt.behavior.arrival_sequence]
ArrSeqUniq.ξ [variable, in probsa.rt.behavior.arrival_sequence]
arr_seq_consistent [lemma, in probsa.rt.behavior.arrival_sequence]
arr_seq_uniq [lemma, in probsa.rt.behavior.arrival_sequence]
arr_seq_job_arrival_consistent [definition, in probsa.rt.behavior.arrival_sequence]
arr_seq [definition, in probsa.rt.behavior.arrival_sequence]
asbool [definition, in probsa.util.boolp]
asboolb [lemma, in probsa.util.boolp]
asboolE [lemma, in probsa.util.boolp]
asboolF [lemma, in probsa.util.boolp]
asboolP [lemma, in probsa.util.boolp]
asboolPn [lemma, in probsa.util.boolp]
asboolT [lemma, in probsa.util.boolp]
asboolW [lemma, in probsa.util.boolp]
asbool_existsNb [lemma, in probsa.util.boolp]
asbool_forallNb [lemma, in probsa.util.boolp]
asbool_imply [lemma, in probsa.util.boolp]
asbool_and [lemma, in probsa.util.boolp]
asbool_or [lemma, in probsa.util.boolp]
asbool_neg [lemma, in probsa.util.boolp]
asbool_eq_equiv [lemma, in probsa.util.boolp]
asbool_equiv [lemma, in probsa.util.boolp]
asbool_equiv_eqP [lemma, in probsa.util.boolp]
asbool_equiv_eq [lemma, in probsa.util.boolp]
assoc [projection, in probsa.util.stdpp]
Assoc [record, in probsa.util.stdpp]
assoc [constructor, in probsa.util.stdpp]
Assoc [inductive, in probsa.util.stdpp]
atotal [definition, in probsa.probability.law_of_total_prob]
atotal_column_rewrite [lemma, in probsa.probability.law_of_total_prob]
atotal_row_rewrite [lemma, in probsa.probability.law_of_total_prob]
atotal_double_summable_by_column [lemma, in probsa.probability.law_of_total_prob]
at_most_one_job_pending [lemma, in probsa.rt.model.workload]
AxiomaticConditionalProbability [section, in probsa.probability.conditional]
AxiomaticPWCET [section, in probsa.rt.model.axiomatic_pWCET]
AxiomaticPWCET.ξ_pr [variable, in probsa.rt.model.axiomatic_pWCET]
axiomatic_pWCET [definition, in probsa.rt.model.axiomatic_pWCET]
axiomatic_pWCET_full [library]
axiomatic_pWCET [library]
axiomatic_pWCET_step [library]

B

basic [library]
BasicLemmas [section, in probsa.probability.conditional]
BasicLemmas [section, in probsa.probability.stochastic_order]
BasicLemmas.H_independent [variable, in probsa.probability.stochastic_order]
BasicLemmas.X [variable, in probsa.probability.stochastic_order]
BasicLemmas.Y [variable, in probsa.probability.stochastic_order]
BasicReadinessWithJobAbortion [section, in probsa.rt.model.abort_readiness]
BeforeDeadline [section, in probsa.rt.model.carry_in]
before_deadline_monotone [lemma, in probsa.rt.model.carry_in]
before_deadline [definition, in probsa.rt.model.carry_in]
bigD1_seq_pred [lemma, in probsa.util.bigop]
bigop [library]
bigop_inf_option_cdf_lt [lemma, in probsa.probability.law_of_total_prob]
bigop_inf_cdf_le [lemma, in probsa.probability.law_of_total_prob]
bigop_inf [library]
bigsum_add [lemma, in probsa.util.bigop]
bigsum_distr [lemma, in probsa.util.bigop]
bigsum_upper_bound_to_indicator [lemma, in probsa.util.indicator]
boolp [library]
brvar [definition, in probsa.probability.brvar]
brvar [library]
by_arrival_times [definition, in probsa.util.prosa.arrival_bound]

C

cancel [projection, in probsa.util.stdpp]
Cancel [record, in probsa.util.stdpp]
cancel [constructor, in probsa.util.stdpp]
Cancel [inductive, in probsa.util.stdpp]
canon [lemma, in probsa.util.boolp]
canonical [abbreviation, in probsa.util.boolp]
canonical_ [abbreviation, in probsa.util.boolp]
canonical_of [definition, in probsa.util.boolp]
carry_in_workload_eq_service_of_jobs [lemma, in probsa.rt.analysis.completion_time]
carry_in [library]
cdf [definition, in probsa.probability.cdf]
cdf [library]
CDFPWCET [section, in probsa.rt.model.task]
cdf_cond_marginal21 [lemma, in probsa.probability.conditional]
cdf_cond_marginal11 [lemma, in probsa.probability.conditional]
cdf_cond_eq_cond [lemma, in probsa.probability.conditional]
cdf_cond_xpredT [lemma, in probsa.probability.conditional]
cdf_cond [definition, in probsa.probability.conditional]
cdf_to_sum_of_indicators [lemma, in probsa.probability.cdf]
cdf_to_sum_of_preq [lemma, in probsa.probability.cdf]
cdf_succ_to_cdf_preq [lemma, in probsa.probability.cdf]
cdf_nondecreasing [lemma, in probsa.probability.cdf]
cdf_nonnegative [lemma, in probsa.probability.cdf]
choice [lemma, in probsa.util.boolp]
choose_superior_default_or_in_seq [lemma, in probsa.util.seq]
cid [abbreviation, in probsa.util.boolp]
cid2 [lemma, in probsa.util.boolp]
classic [lemma, in probsa.util.boolp]
classicType [definition, in probsa.util.boolp]
classicType [section, in probsa.util.boolp]
classicType_choiceType [definition, in probsa.util.boolp]
classicType_eqType [definition, in probsa.util.boolp]
classicType.T [variable, in probsa.util.boolp]
comm [projection, in probsa.util.stdpp]
Comm [record, in probsa.util.stdpp]
comm [constructor, in probsa.util.stdpp]
Comm [inductive, in probsa.util.stdpp]
CommonAssumptions [section, in probsa.rt.model.assumptions.basic]
CommonAssumptions.pr_sched [variable, in probsa.rt.model.assumptions.basic]
CommonAssumptions.ts [variable, in probsa.rt.model.assumptions.basic]
CommonAssumptions.tsk [variable, in probsa.rt.model.assumptions.basic]
completed_by𝗔𝗖 [definition, in probsa.rt.model.scheduler]
completed_by_is_dec [lemma, in probsa.rt.behavior.response_time]
completed𝗔𝗖_is_dec [definition, in probsa.rt.model.scheduler]
completion [library]
CompletionLemmas [section, in probsa.rt.analysis.completion]
CompletionLemmas.sched [variable, in probsa.rt.analysis.completion]
CompletionTimeExists [section, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_workload_is_consumed [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_non_empty [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_jobs_come_from_arrival_sequence [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_jobs_must_arrive_to_execute [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_completed_jobs_dont_execute [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_jobs_must_be_ready_to_execute [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_respects_policy_at_preemption_point [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_work_conserving [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_arrivals_consistent [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_transitive_priorities [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.sched [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof [section, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.ARR1 [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.ARR2 [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_not_completed [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_deadline_in_future [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_arrival [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_hep_tsk [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_workload_is_consumed [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_non_empty [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.j [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.P1 [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.P2 [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step1 [section, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step2 [section, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step3 [section, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step4 [section, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step5 [section, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.t [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Δ [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.ω [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.t [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.tsk [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.V [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.Δ [variable, in probsa.rt.analysis.completion_time]
CompletionTimeExists.ω [variable, in probsa.rt.analysis.completion_time]
completion_time_exists [lemma, in probsa.rt.analysis.completion_time]
completion_monotone_prob [lemma, in probsa.rt.analysis.completion]
completion_monotone [lemma, in probsa.rt.analysis.completion]
completion_time [library]
compute_pr_schedule [definition, in probsa.rt.model.scheduler]
conditional [library]
ConditionalMeasure [section, in probsa.probability.conditional]
conditional_cost_bounded_by_pWCET [definition, in probsa.rt.model.assumptions.pr_cost]
cond_cdf_posprob_irrelevance [lemma, in probsa.probability.conditional]
cond_prob_posprob_irrelevance [lemma, in probsa.probability.conditional]
Consistent [section, in probsa.rt.behavior.arrival_sequence]
ConsistentDef [section, in probsa.rt.behavior.arrival_sequence]
constrained_deadlines [definition, in probsa.rt.model.assumptions.basic]
constructive_indefinite_description [axiom, in probsa.util.boolp]
cons_elim [lemma, in probsa.rt.behavior.arrival_sequence]
contraNP [lemma, in probsa.util.boolp]
contraPP [lemma, in probsa.util.boolp]
contraPT [lemma, in probsa.util.boolp]
contrapT [lemma, in probsa.util.boolp]
contraTP [lemma, in probsa.util.boolp]
contra_eqP [lemma, in probsa.util.boolp]
contra_neqP [lemma, in probsa.util.boolp]
contra_notT [lemma, in probsa.util.boolp]
contra_notP [lemma, in probsa.util.boolp]
CostPartition [section, in probsa.rt.model.events]
cost_causing_exceedance_of_r [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
cost_and_workload [library]
COV [projection, in probsa.probability.partition]

D

deadline_miss_implies_workload_exceeds_time [lemma, in probsa.rt.analysis.pRTA.pRTA]
demand_distrib [definition, in probsa.rt.analysis.pRTA.pRTA]
dep_arrow_choiceType [definition, in probsa.util.boolp]
dep_arrow_choiceClass [definition, in probsa.util.boolp]
dep_arrow_eqType [definition, in probsa.util.boolp]
DerivedNotions [section, in probsa.rt.behavior.job]
DIS [projection, in probsa.probability.partition]
distribution_of_prod_restrict [lemma, in probsa.probability.conditional]
div_ceil_multiple [lemma, in probsa.util.prosa.arrival_bound]
DominanceRelation [record, in probsa.probability.dominance_relation]
DominanceRelation [inductive, in probsa.probability.dominance_relation]
dominance_ndistrib_nrvar [instance, in probsa.probability.pmf]
dominance_nrvar_ndistrib [instance, in probsa.probability.pmf]
dominance_etime_rvar [instance, in probsa.probability.dominance_relation]
dominance_nrvar_funct [instance, in probsa.probability.dominance_relation]
dominance_nrvar [instance, in probsa.probability.dominance_relation]
dominance_func [instance, in probsa.probability.dominance_relation]
dominance_relation [library]
dominates [projection, in probsa.probability.dominance_relation]
dominates [constructor, in probsa.probability.dominance_relation]

E

eclassicType [definition, in probsa.util.boolp]
eclassicType [section, in probsa.util.boolp]
eclassicType_choiceType [definition, in probsa.util.boolp]
eclassicType_eqType [definition, in probsa.util.boolp]
eclassicType.T [variable, in probsa.util.boolp]
EM [lemma, in probsa.util.boolp]
empty [projection, in probsa.util.stdpp]
Empty [record, in probsa.util.stdpp]
empty [constructor, in probsa.util.stdpp]
Empty [inductive, in probsa.util.stdpp]
eqn_etime [lemma, in probsa.util.etime]
EqOp [record, in probsa.util.notation]
EqOp [inductive, in probsa.util.notation]
eqPchoice [lemma, in probsa.util.boolp]
equiv [projection, in probsa.util.stdpp]
Equiv [record, in probsa.util.stdpp]
equiv [constructor, in probsa.util.stdpp]
Equiv [inductive, in probsa.util.stdpp]
equivL [definition, in probsa.util.stdpp]
equiv_default_relation [instance, in probsa.util.stdpp]
equiv_rewrite_relation [instance, in probsa.util.stdpp]
eq_tr3 [lemma, in probsa.util.tr_eq]
eq_tr4 [lemma, in probsa.util.tr_eq]
eq_opE [lemma, in probsa.util.boolp]
eq_exist [lemma, in probsa.util.boolp]
eq_exists3 [lemma, in probsa.util.boolp]
eq_exists2 [lemma, in probsa.util.boolp]
eq_exists [lemma, in probsa.util.boolp]
eq_forall3 [lemma, in probsa.util.boolp]
eq_forall2 [lemma, in probsa.util.boolp]
eq_forall [lemma, in probsa.util.boolp]
eq_fun3 [lemma, in probsa.util.boolp]
eq_fun2 [lemma, in probsa.util.boolp]
eq_fun [lemma, in probsa.util.boolp]
eq_op [projection, in probsa.util.notation]
eq_op [constructor, in probsa.util.notation]
eq_arr_seq_impl_eq_job_arrival [lemma, in probsa.rt.behavior.arrival_sequence]
etime [inductive, in probsa.util.etime]
etime [library]
etime_dom_trans [lemma, in probsa.probability.dominance_relation]
etime_dom_refl [lemma, in probsa.probability.dominance_relation]
etime_eqType [definition, in probsa.util.etime]
etime_eqMixin [definition, in probsa.util.etime]
etime_eqdef [definition, in probsa.util.etime]
events [library]
exceeds [definition, in probsa.util.etime]
existsNE [lemma, in probsa.util.boolp]
existsNP [lemma, in probsa.util.boolp]
existsPNP [lemma, in probsa.util.boolp]
existsp_asboolPn [lemma, in probsa.util.boolp]
exists_asboolP [lemma, in probsa.util.boolp]
exists_swap [lemma, in probsa.util.boolp]
exists2P [lemma, in probsa.util.boolp]
extend_partition' [definition, in probsa.rt.analysis.partition_transfer]
extend_partition [definition, in probsa.rt.analysis.partition_transfer]
extentionality [lemma, in probsa.util.boolp]
ex_total_column_abs [lemma, in probsa.probability.law_of_total_prob]
ex_series_pr_eq_over_partition [lemma, in probsa.probability.law_of_total_prob]
ex_series_pr_eq_over_disjoint [lemma, in probsa.probability.law_of_total_prob]

F

falseE [lemma, in probsa.util.boolp]
filter_cons_eq [lemma, in probsa.rt.behavior.arrival_sequence]
filter_eq_cons_sat [lemma, in probsa.rt.behavior.arrival_sequence]
Fin [constructor, in probsa.util.etime]
foldr_choose_superior_in_seq [lemma, in probsa.util.seq]
foldr_choose_superior_not_none [lemma, in probsa.util.seq]
foldr_big [lemma, in probsa.util.bigop]
fold_prob_to_cond_cdf [lemma, in probsa.probability.conditional]
fold_prob_to_cond_prob [lemma, in probsa.probability.conditional]
forallNE [lemma, in probsa.util.boolp]
forallNP [lemma, in probsa.util.boolp]
forallPNP [lemma, in probsa.util.boolp]
forallp_asboolPn [lemma, in probsa.util.boolp]
forall_asboolP [lemma, in probsa.util.boolp]
forall_swap [lemma, in probsa.util.boolp]
forall2NP [lemma, in probsa.util.boolp]
FP_FP_sched_is_rt_monotonic [lemma, in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_jobs_must_be_ready_to_execute [lemma, in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_policy_at_preemption_point [lemma, in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_is_work_conserving [lemma, in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_jobs_come_from_arrival_sequence [lemma, in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_jobs_must_arrive_to_execute [lemma, in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_completed_jobs_dont_execute [lemma, in probsa.rt.analysis.scheduler_properties]
FP_FP_sched [definition, in probsa.rt.analysis.scheduler_properties]
frechet_bound_on_all_intervals [lemma, in probsa.rt.analysis.pRTA.pRTA]
frechet_min [lemma, in probsa.probability.prob]
functional_extensionality_dep [axiom, in probsa.util.boolp]
func_dom_trans [lemma, in probsa.probability.dominance_relation]
func_dom_refl [lemma, in probsa.probability.dominance_relation]
funeqE [lemma, in probsa.util.boolp]
funeqP [lemma, in probsa.util.boolp]
funeq2E [lemma, in probsa.util.boolp]
funeq2P [lemma, in probsa.util.boolp]
funeq3E [lemma, in probsa.util.boolp]
funeq3P [lemma, in probsa.util.boolp]
funext [lemma, in probsa.util.boolp]
FunOrder [module, in probsa.util.boolp]
FunOrder.Exports [module, in probsa.util.boolp]
FunOrder.FunLattice [section, in probsa.util.boolp]
FunOrder.FunLattice.aT [variable, in probsa.util.boolp]
FunOrder.FunLattice.d [variable, in probsa.util.boolp]
FunOrder.FunLattice.T [variable, in probsa.util.boolp]
FunOrder.FunOrder [section, in probsa.util.boolp]
FunOrder.FunOrder.aT [variable, in probsa.util.boolp]
FunOrder.FunOrder.d [variable, in probsa.util.boolp]
FunOrder.FunOrder.T [variable, in probsa.util.boolp]
_ < _ [notation, in probsa.util.boolp]
_ <= _ [notation, in probsa.util.boolp]
FunOrder.fun_display [lemma, in probsa.util.boolp]
FunOrder.joinf [definition, in probsa.util.boolp]
FunOrder.joinfA [lemma, in probsa.util.boolp]
FunOrder.joinfC [lemma, in probsa.util.boolp]
FunOrder.joinfKI [lemma, in probsa.util.boolp]
FunOrder.latticeMixin [definition, in probsa.util.boolp]
FunOrder.latticeType [definition, in probsa.util.boolp]
FunOrder.lef [definition, in probsa.util.boolp]
FunOrder.lef_meet [lemma, in probsa.util.boolp]
FunOrder.lef_trans [lemma, in probsa.util.boolp]
FunOrder.lef_anti [lemma, in probsa.util.boolp]
FunOrder.lef_refl [lemma, in probsa.util.boolp]
FunOrder.ltf [definition, in probsa.util.boolp]
FunOrder.ltf_def [lemma, in probsa.util.boolp]
FunOrder.meetf [definition, in probsa.util.boolp]
FunOrder.meetfA [lemma, in probsa.util.boolp]
FunOrder.meetfC [lemma, in probsa.util.boolp]
FunOrder.meetfKU [lemma, in probsa.util.boolp]
FunOrder.porderMixin [definition, in probsa.util.boolp]
FunOrder.porderType [definition, in probsa.util.boolp]

G

gen_eqMixin [definition, in probsa.util.boolp]
gen_eqP [lemma, in probsa.util.boolp]
gen_eq [definition, in probsa.util.boolp]
gen_choiceMixin [lemma, in probsa.util.boolp]
get_cover_index_valid [lemma, in probsa.probability.law_of_total_prob]
get_cover_index [definition, in probsa.probability.law_of_total_prob]

I

I [projection, in probsa.probability.partition]
idemp [projection, in probsa.util.stdpp]
IdemP [record, in probsa.util.stdpp]
idemp [constructor, in probsa.util.stdpp]
IdemP [inductive, in probsa.util.stdpp]
iff_not2 [lemma, in probsa.util.boolp]
iff_notr [lemma, in probsa.util.boolp]
imply_asboolPn [lemma, in probsa.util.boolp]
imply_asboolP [lemma, in probsa.util.boolp]
independence [library]
IndependentCat [section, in probsa.probability.independence]
IndependentExtend [section, in probsa.probability.independence]
IndependentExtend.F [variable, in probsa.probability.independence]
IndependentFlatten [section, in probsa.probability.independence]
IndependentFlatten.f [variable, in probsa.probability.independence]
IndependentFlatten.xs [variable, in probsa.probability.independence]
IndependentFlatten.ys [variable, in probsa.probability.independence]
IndependentMap [section, in probsa.probability.independence]
IndependentMap.F [variable, in probsa.probability.independence]
IndependentPair [section, in probsa.probability.independence]
IndependentSum [section, in probsa.probability.independence]
IndependentSum.F [variable, in probsa.probability.independence]
independent_flatten [lemma, in probsa.probability.independence]
indep_extend_consts [lemma, in probsa.probability.independence]
indep_consts [lemma, in probsa.probability.independence]
indep_pair_const_r [lemma, in probsa.probability.independence]
indep_pair_swap [lemma, in probsa.probability.independence]
indep_irr [lemma, in probsa.probability.independence]
indep_comp [lemma, in probsa.probability.independence]
indep_subset [lemma, in probsa.probability.independence]
indep_filter [lemma, in probsa.probability.independence]
indep_perm_eq [lemma, in probsa.probability.independence]
indep_cat_indep2_list_comp [lemma, in probsa.probability.independence]
indep_cat_indep2_list [lemma, in probsa.probability.independence]
indep_cat_split [lemma, in probsa.probability.independence]
indep_catC [lemma, in probsa.probability.independence]
Indep2 [section, in probsa.probability.independence]
indep2_sum_cons [lemma, in probsa.probability.independence]
indep2_sum [lemma, in probsa.probability.independence]
indep2_fn_extl [lemma, in probsa.probability.independence]
indep2_fn_ext [lemma, in probsa.probability.independence]
Indep2.IndepExt [section, in probsa.probability.independence]
Indep2.IndepExtL [section, in probsa.probability.independence]
Indep2.IndepExtL.f [variable, in probsa.probability.independence]
Indep2.IndepExtL.X1 [variable, in probsa.probability.independence]
Indep2.IndepExtL.X2 [variable, in probsa.probability.independence]
Indep2.IndepExtL.Y [variable, in probsa.probability.independence]
Indep2.IndepExt.f1 [variable, in probsa.probability.independence]
Indep2.IndepExt.f2 [variable, in probsa.probability.independence]
Indep2.IndepExt.X1 [variable, in probsa.probability.independence]
Indep2.IndepExt.X2 [variable, in probsa.probability.independence]
Indep2.IndepExt.Y1 [variable, in probsa.probability.independence]
Indep2.IndepExt.Y2 [variable, in probsa.probability.independence]
index_iota_recr [lemma, in probsa.util.iota]
indicator [library]
indicatorR [definition, in probsa.util.indicator]
indicator_pred_impl [lemma, in probsa.util.indicator]
indicator_pred_eq [lemma, in probsa.util.indicator]
indicator_andb_mult [lemma, in probsa.util.indicator]
Infty [constructor, in probsa.util.etime]
inj [projection, in probsa.util.stdpp]
Inj [record, in probsa.util.stdpp]
inj [constructor, in probsa.util.stdpp]
Inj [inductive, in probsa.util.stdpp]
inj2 [projection, in probsa.util.stdpp]
Inj2 [record, in probsa.util.stdpp]
inj2 [constructor, in probsa.util.stdpp]
Inj2 [inductive, in probsa.util.stdpp]
interference_bounded_by_task_workload_sum [lemma, in probsa.rt.analysis.pRTA.pRTA]
interference_distrib [definition, in probsa.rt.analysis.pRTA.pRTA]
intersection [projection, in probsa.util.stdpp]
Intersection [record, in probsa.util.stdpp]
intersection [constructor, in probsa.util.stdpp]
Intersection [inductive, in probsa.util.stdpp]
involutive [lemma, in probsa.util.stdpp]
Involutive [abbreviation, in probsa.util.stdpp]
iota [library]
is_some [definition, in probsa.util.bigop_inf]
is_seriesC_bump [lemma, in probsa.util.bigop_inf]
is_true_inj [lemma, in probsa.util.boolp]
is_in_cover [definition, in probsa.probability.law_of_total_prob]
iterfS [lemma, in probsa.util.boolp]
iterfSr [lemma, in probsa.util.boolp]
iter0 [lemma, in probsa.util.boolp]

J

job [library]
JobArrivalRV [record, in probsa.rt.behavior.job]
JobArrivalRV [inductive, in probsa.rt.behavior.job]
JobCostRV [record, in probsa.rt.behavior.job]
JobCostRV [inductive, in probsa.rt.behavior.job]
JobCostWorkloadIndependent [section, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.H_job_costs_cond_independent [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.H_job_of_task [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.H_tsk_in_ts [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.H_arrivals_consistent [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.INωξ [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.j [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.POS [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.t [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ts [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.tsk [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.Δ [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ξ [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ξpart [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ω [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.𝓒 [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.𝓦 [variable, in probsa.rt.analysis.independent.cost_and_workload]
JobDeadlineRV [record, in probsa.rt.behavior.job]
JobDeadlineRV [inductive, in probsa.rt.behavior.job]
jobs_rt_always_exceeds_r [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
jobs_rt_never_exceeds_r [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
job_cost_sum_condition_arrival_seq [lemma, in probsa.rt.analysis.work_bound]
job_cost_partition_dominated [definition, in probsa.rt.model.axiomatic_pWCET]
job_cost_partition_independence [definition, in probsa.rt.model.axiomatic_pWCET]
job_cost_cond_independent_respected [lemma, in probsa.rt.analysis.valid_pWCET_remains_valid]
job_cost_cond_bounded_by_pWCET_respected [lemma, in probsa.rt.analysis.valid_pWCET_remains_valid]
job_costs_independent_of_arrival_sequence [definition, in probsa.rt.model.assumptions.pr_cost]
job_costs_independent_cond_arr_seq [definition, in probsa.rt.model.assumptions.pr_cost]
job_costs_identically_distributed [definition, in probsa.rt.model.assumptions.pr_cost]
job_costs_bounded_by_pWCET [definition, in probsa.rt.model.assumptions.pr_cost]
job_costs_independent [definition, in probsa.rt.model.assumptions.pr_cost]
job_deadline_from_task_deadline [instance, in probsa.rt.model.task]
job_cost_and_ohep_workload_independent [lemma, in probsa.rt.analysis.independent.cost_and_workload]
job_cost_and_ohep_workload_indep2 [lemma, in probsa.rt.analysis.independent.cost_and_workload]
job_either_arrives_or_not [lemma, in probsa.rt.analysis.pRTA.pRTA]
job_deadline [projection, in probsa.rt.behavior.job]
job_deadline [constructor, in probsa.rt.behavior.job]
job_arrival [projection, in probsa.rt.behavior.job]
job_arrival [constructor, in probsa.rt.behavior.job]
job_cost [projection, in probsa.rt.behavior.job]
job_cost [constructor, in probsa.rt.behavior.job]
job_cost_s [instance, in probsa.rt.analysis.axiomatic_pWCET_full]
job_arrival_s [instance, in probsa.rt.analysis.axiomatic_pWCET_full]
job_arrival_between_lt [lemma, in probsa.util.prosa.arrival_bound]
job_arrival_between_ge [lemma, in probsa.util.prosa.arrival_bound]
job_arrival_at [lemma, in probsa.util.prosa.arrival_bound]
joinfE [lemma, in probsa.util.boolp]
j_completed [lemma, in probsa.rt.analysis.completion_time]
j_scheduled_at_t_in_sched2 [lemma, in probsa.rt.analysis.scheduler_properties]

L

LawOfTotalProbability [section, in probsa.probability.law_of_total_prob]
LawOfTotalProbabilityProd [section, in probsa.probability.law_of_total_prob]
LawOfTotalProbabilityProd.A [variable, in probsa.probability.law_of_total_prob]
LawOfTotalProbabilityProd.S [variable, in probsa.probability.law_of_total_prob]
LawOfTotalProbability.B [variable, in probsa.probability.law_of_total_prob]
LawOfTotalProbability.H_Bi_disjoint [variable, in probsa.probability.law_of_total_prob]
LawOfTotalProbability.H_Bi_covers [variable, in probsa.probability.law_of_total_prob]
LawOfTotalProbability.I [variable, in probsa.probability.law_of_total_prob]
LawOfTotalProbability.P [variable, in probsa.probability.law_of_total_prob]
law_of_total_probability_simple [lemma, in probsa.probability.prob]
law_of_total_probability_prod [lemma, in probsa.probability.law_of_total_prob]
law_of_total_probability [lemma, in probsa.probability.law_of_total_prob]
law_of_total_prob [library]
lefP [lemma, in probsa.util.boolp]
LeftAbsorb [record, in probsa.util.stdpp]
LeftAbsorb [inductive, in probsa.util.stdpp]
LeftId [record, in probsa.util.stdpp]
LeftId [inductive, in probsa.util.stdpp]
left_absorb [projection, in probsa.util.stdpp]
left_absorb [constructor, in probsa.util.stdpp]
left_id [projection, in probsa.util.stdpp]
left_id [constructor, in probsa.util.stdpp]
LeibnizEquiv [record, in probsa.util.stdpp]
LeibnizEquiv [inductive, in probsa.util.stdpp]
leibniz_equiv_iff [lemma, in probsa.util.stdpp]
leibniz_equiv [projection, in probsa.util.stdpp]
leibniz_equiv [constructor, in probsa.util.stdpp]
lem [lemma, in probsa.util.boolp]
LeqOp [record, in probsa.util.notation]
LeqOp [inductive, in probsa.util.notation]
leq_SeriesC [lemma, in probsa.util.bigop_inf]
leq_op [projection, in probsa.util.notation]
leq_op [constructor, in probsa.util.notation]
le_ndistrib_nrvar [definition, in probsa.probability.pmf]
le_nrvar_ndistrib [definition, in probsa.probability.pmf]
le_etime_rvar [definition, in probsa.probability.dominance_relation]
le_nrvar_func [definition, in probsa.probability.dominance_relation]
le_nrvar [definition, in probsa.probability.dominance_relation]
le_func [definition, in probsa.probability.dominance_relation]
LHS_factorization [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
lims_Λ [lemma, in probsa.rt.analysis.pRTA.pRTA]
lower_bound_on_service_of_jobs [lemma, in probsa.rt.analysis.completion_time]
LtOp [record, in probsa.util.notation]
LtOp [inductive, in probsa.util.notation]
lt_op [projection, in probsa.util.notation]
lt_op [constructor, in probsa.util.notation]

M

MainLemma [section, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.horizon [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.H_rt_monotonic [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.H_axiomatic_pWCET [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.initial_system [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.sched1 [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.sched2 [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.simplified_system [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.Ωg [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.Ωs [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.ζ [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.μg [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.μs [variable, in probsa.rt.analysis.axiomatic_pWCET_full]
MaxArrivalsSporadic [instance, in probsa.util.prosa.sporadic_as_curve]
max_sporadic_arrivals [definition, in probsa.util.prosa.arrival_bound]
mclassic [record, in probsa.util.boolp]
measure [definition, in probsa.util.notation]
meetfE [lemma, in probsa.util.boolp]
mextentionality [record, in probsa.util.boolp]
min [library]
MinimumInterArrival [section, in probsa.rt.model.min_inter_arrival]
MinimumInterArrival.ξ_pr [variable, in probsa.rt.model.min_inter_arrival]
minimum_distance_for_n_sporadic_arrivals [lemma, in probsa.util.prosa.arrival_bound]
min_default [definition, in probsa.util.min]
min_option [definition, in probsa.util.min]
min_completion_time [definition, in probsa.rt.model.scheduler]
min_completion_time [definition, in probsa.rt.behavior.response_time]
min_inter_arrival [library]
min1 [definition, in probsa.util.min]
min1_cons [lemma, in probsa.util.min]
misc [library]

N

nat_etimervar_pred_ltop [instance, in probsa.probability.dominance_relation]
nat_nat_bool_eqop [instance, in probsa.util.notation]
NegOp [record, in probsa.util.notation]
NegOp [inductive, in probsa.util.notation]
neg_pred [instance, in probsa.probability.pred]
neg_op [projection, in probsa.util.notation]
neg_op [constructor, in probsa.util.notation]
nonempty_sample_space [lemma, in probsa.probability.prob]
nonreplaced_pETs_dont_change_2_step [lemma, in probsa.rt.analysis.transformation_properties]
nonreplaced_pETs_dont_change_1_step [lemma, in probsa.rt.analysis.transformation_properties]
notation [library]
notFE [lemma, in probsa.util.boolp]
notK [lemma, in probsa.util.boolp]
notLR [lemma, in probsa.util.boolp]
notRL [lemma, in probsa.util.boolp]
notT [lemma, in probsa.util.boolp]
notTE [lemma, in probsa.util.boolp]
not_exists2P [lemma, in probsa.util.boolp]
not_forallP [lemma, in probsa.util.boolp]
not_existsP [lemma, in probsa.util.boolp]
not_implyE [lemma, in probsa.util.boolp]
not_orP [lemma, in probsa.util.boolp]
not_and3P [lemma, in probsa.util.boolp]
not_andP [lemma, in probsa.util.boolp]
not_implyP [lemma, in probsa.util.boolp]
not_inj [lemma, in probsa.util.boolp]
not_False [lemma, in probsa.util.boolp]
not_True [lemma, in probsa.util.boolp]
not_symmetry [lemma, in probsa.util.stdpp]
no_carry_in_at_task_arrival [lemma, in probsa.rt.model.carry_in]
nrvar [definition, in probsa.probability.nrvar]
nrvar [library]
nrvar_nat_pred_eqop [instance, in probsa.probability.nrvar]
nrvar_subop [instance, in probsa.probability.nrvar]
nrvar_addop [instance, in probsa.probability.nrvar]
nrvar_nrvar_brvar_leqop [instance, in probsa.probability.nrvar]
nrvar_nrvar_pred_leqop [instance, in probsa.probability.nrvar]
nrvar_addop_id [definition, in probsa.probability.nrvar]
nrvar_dom_trans [lemma, in probsa.probability.dominance_relation]
nrvar_dom_refl [lemma, in probsa.probability.dominance_relation]
NthCost [section, in probsa.rt.analysis.nth_cost]
NthCostLemmas [section, in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_tsk_in_ts [variable, in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_ts_uniq [variable, in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_job_costs_independent [variable, in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_arrivals_consistent [variable, in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_arrival_sequence_uniq [variable, in probsa.rt.analysis.nth_cost]
NthCostLemmas.pr_sched [variable, in probsa.rt.analysis.nth_cost]
NthCostLemmas.ts [variable, in probsa.rt.analysis.nth_cost]
NthCostLemmas.tsk [variable, in probsa.rt.analysis.nth_cost]
nth_cost_sum_monotone [lemma, in probsa.rt.analysis.work_bound]
nth_mem_o [lemma, in probsa.util.misc]
nth_seq_eq [lemma, in probsa.util.misc]
nth_cost [definition, in probsa.rt.analysis.nth_cost]
nth_job_cost_bounded_by_pWCET [lemma, in probsa.rt.analysis.pRTA.pRTA]
nth_cost_sum_rewrite [lemma, in probsa.rt.analysis.pRTA.pRTA]
nth_cost [library]

O

odflt0 [definition, in probsa.probability.nrvar]
onat_onat_bool_ltop [instance, in probsa.util.notation]
onat_nat_bool_leqop [instance, in probsa.util.notation]
onat_onat_bool_leqop [instance, in probsa.util.notation]
onrvar_onat_pred_leqop [instance, in probsa.probability.nrvar]
onrvar_nrvar_brvar_leqop [instance, in probsa.probability.nrvar]
onrvar_onat_pred_eqop [instance, in probsa.probability.nrvar]
orA [lemma, in probsa.util.boolp]
orC [lemma, in probsa.util.boolp]
or_asboolP [lemma, in probsa.util.boolp]
or3_asboolP [lemma, in probsa.util.boolp]

P

p [projection, in probsa.probability.partition]
partition [library]
PartitionExtend [section, in probsa.probability.partition]
PartitionIntoSingletons [section, in probsa.probability.partition]
PartitionProduct [section, in probsa.probability.partition]
PartitionTransfer [section, in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition [section, in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition [section, in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition.j [variable, in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition.P [variable, in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition.S [variable, in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition.S' [variable, in probsa.rt.analysis.partition_transfer]
partition_into_singletons_partition_dominated [lemma, in probsa.rt.analysis.WCET_is_pWCET]
partition_into_singletons_partition_intependent [lemma, in probsa.rt.analysis.WCET_is_pWCET]
partition_ext [definition, in probsa.probability.partition]
partition_prod [definition, in probsa.probability.partition]
partition_id [definition, in probsa.probability.partition]
partition_into_singletons [definition, in probsa.probability.partition]
partition_on_𝓒s [definition, in probsa.rt.model.events]
partition_on_𝓒 [definition, in probsa.rt.model.events]
partition_on_ξ [definition, in probsa.rt.model.events]
partition_transfer [library]
Pchoice [lemma, in probsa.util.boolp]
pdegen [lemma, in probsa.util.boolp]
Peq [lemma, in probsa.util.boolp]
perm_eq_allpairs_flatten [lemma, in probsa.util.misc]
perm_eq_zippable [lemma, in probsa.util.zip]
perm_zip1 [lemma, in probsa.util.zip]
pETs_have_same_distribution [lemma, in probsa.rt.analysis.transformation_properties]
pETs_to_pWCETs [library]
pickle_bij [definition, in probsa.util.bigop_inf]
pickle_cover_of [definition, in probsa.probability.law_of_total_prob]
pmf [library]
pmf_restricted_pred [lemma, in probsa.probability.conditional]
pmf_sums_to_1 [lemma, in probsa.probability.conditional]
pmf_nonnegative [lemma, in probsa.probability.conditional]
pmf_restricted [definition, in probsa.probability.conditional]
pmf_sum [definition, in probsa.probability.pmf]
pmf_zero [definition, in probsa.probability.pmf]
pointwise_leq_zip_impl_in_leq [lemma, in probsa.util.zip]
pointwise_min1_zip [lemma, in probsa.util.zip]
PosProb [record, in probsa.probability.conditional]
PosProb [inductive, in probsa.probability.conditional]
posprob_xpredT [instance, in probsa.probability.conditional]
pos_prob [projection, in probsa.probability.conditional]
pos_prob [constructor, in probsa.probability.conditional]
PrArrivalLemmas [section, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.H_valid_arrival_curve [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.H_respects_arrival_curve [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.H_tsk_in_ts [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.ts [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.tsk [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.Ω [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.μ [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.ξ [variable, in probsa.rt.analysis.arrivals]
PrArrivalLemmas.ξpart [variable, in probsa.rt.analysis.arrivals]
PrArrivalsBetween [section, in probsa.rt.behavior.arrival_sequence]
PrArrivalsBetween.ξ [variable, in probsa.rt.behavior.arrival_sequence]
pRBF [definition, in probsa.rt.model.pRBF]
pRBF [library]
PrCarryInWorkload [section, in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts [section, in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.H_arrivals_consistent [variable, in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.H_arrivals_from_ts [variable, in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.H_tsk_in_ts [variable, in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.pr_sched [variable, in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.ts [variable, in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.tsk [variable, in probsa.rt.model.carry_in]
PrCarryInWorkload.pr_sched [variable, in probsa.rt.model.carry_in]
PrCostAssumptions [section, in probsa.rt.model.assumptions.pr_cost]
pred [library]
predeqE [lemma, in probsa.util.boolp]
predeqP [lemma, in probsa.util.boolp]
predeq2E [lemma, in probsa.util.boolp]
predeq2P [lemma, in probsa.util.boolp]
predeq3E [lemma, in probsa.util.boolp]
predeq3P [lemma, in probsa.util.boolp]
predp [definition, in probsa.util.boolp]
pred_cap_and [lemma, in probsa.probability.pred]
pred_cap_assoc [lemma, in probsa.probability.pred]
pred_intersection [instance, in probsa.probability.pred]
pred_union [instance, in probsa.probability.pred]
pred0p [definition, in probsa.util.boolp]
pred0pP [lemma, in probsa.util.boolp]
PrioAwareUniprocessorScheduler [section, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.arr_seq [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_transitive [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_total [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_reflexive_priorities [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_valid_preemption_behavior [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_nonclairvoyant_job_readiness [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_consistent_arrival_times [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.idle_state [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.policy [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.prefix [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.PState [variable, in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.schedule [variable, in probsa.util.prosa.prio_aware]
prio_aware [library]
PrMustBeReadyToExecture [section, in probsa.rt.model.assumptions.pr_must_be_ready]
PrMustBeReadyToExecture.JobReadyRV [variable, in probsa.rt.model.assumptions.pr_must_be_ready]
PrMustBeReadyToExecture.sched [variable, in probsa.rt.model.assumptions.pr_must_be_ready]
prob [library]
ProbabilisticResponseTimeMonotonicity [section, in probsa.rt.model.rt_monotonic]
ProbabilisticResponseTimeMonotonicity.horizon [variable, in probsa.rt.model.rt_monotonic]
ProbabilisticResponseTimeMonotonicity.pr_sched_Ωs [variable, in probsa.rt.model.rt_monotonic]
ProbabilisticResponseTimeMonotonicity.pr_sched_Ωg [variable, in probsa.rt.model.rt_monotonic]
ProbabilisticRTA [section, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.h [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_job_of_task [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_axiomatic_pWCET [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_sporadic [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_all_jobs_from_ts [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_horizon_after_deadlines [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_arrivals_agree_with_costs [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_tsk_in_ts [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_valid_sporadic [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_constrained_deadlines [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_ts_uniq [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_priority_is_transitive [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_priority_is_reflexive [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_priority_is_total [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.j [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.ts [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.tsk [variable, in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.𝓡 [variable, in probsa.rt.analysis.pRTA.pRTA_full]
probabilistic_response_time_monotone_transformation [definition, in probsa.rt.model.rt_monotonic]
probabilistic_rta_fp [lemma, in probsa.rt.analysis.pRTA.pRTA]
probabilistic_rt_monotonicity_of_iid_pWCET' [lemma, in probsa.rt.analysis.axiomatic_pWCET_full]
probabilistic_rt_monotonicity_of_iid_pWCET [lemma, in probsa.rt.analysis.axiomatic_pWCET_full]
probabilistic_rta_fp_fp [lemma, in probsa.rt.analysis.pRTA.pRTA_full]
ProbBasicReadinessWithJobAbortion [section, in probsa.rt.model.abort_readiness]
ProbMassFunction [section, in probsa.probability.pmf]
ProbRBF [section, in probsa.rt.model.pRBF]
ProbWCET [record, in probsa.rt.model.task]
prob_rt_monotonic_axiomatic_pWCET_replace_all_pETs [lemma, in probsa.rt.analysis.valid_pWCET_remains_valid]
prob_rt_monotonic_axiomatic_pWCET_replace_pET [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
proj1 [definition, in probsa.rt.analysis.partition_transfer]
proj2 [definition, in probsa.rt.analysis.partition_transfer]
projω [definition, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.horizon [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.H_axiomatic_pWCET [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.H_rt_monotonic [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.j [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.j_rep [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.S [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.sched [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.S' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.ζ [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.𝓡j [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.𝓡j' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
propeqE [lemma, in probsa.util.boolp]
propeqP [lemma, in probsa.util.boolp]
propext [lemma, in probsa.util.boolp]
propF [lemma, in probsa.util.boolp]
propositional_extensionality [axiom, in probsa.util.boolp]
propT [lemma, in probsa.util.boolp]
Prop_choiceType [definition, in probsa.util.boolp]
Prop_eqType [definition, in probsa.util.boolp]
Prop_irrelevance [lemma, in probsa.util.boolp]
PrPendWorkload [section, in probsa.rt.model.carry_in]
PrPendWorkload.pr_sched [variable, in probsa.rt.model.carry_in]
PrRespectsPolicyAtPreemptionPoint [section, in probsa.rt.model.assumptions.pr_respects_policy]
PrRespectsPolicyAtPreemptionPoint.JobReadyRV [variable, in probsa.rt.model.assumptions.pr_respects_policy]
PrRespectsPolicyAtPreemptionPoint.sched [variable, in probsa.rt.model.assumptions.pr_respects_policy]
PrResponseTime [section, in probsa.rt.behavior.response_time]
PrResponseTime.horizon [variable, in probsa.rt.behavior.response_time]
PrResponseTime.LPO_ResponseTime [section, in probsa.rt.behavior.response_time]
PrResponseTime.sched [variable, in probsa.rt.behavior.response_time]
PrServiceBounded [section, in probsa.rt.model.assumptions.basic]
PrServiceBounded.H_pr_completed_jobs_dont_execute [variable, in probsa.rt.model.assumptions.basic]
PrServiceBounded.H_unit_service_proc_model [variable, in probsa.rt.model.assumptions.basic]
PrServiceBounded.pr_sched [variable, in probsa.rt.model.assumptions.basic]
pRTA [library]
PrTaskWorkloadBoundedNthCost [section, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_job_costs_identically_distr [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_job_costs_independent [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_job_costs_independent_arr_seq [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_arrival_sequence_uniq [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_arrivals_consistent [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.tsk [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.ξ [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.ξpart [variable, in probsa.rt.analysis.work_bound]
PrTaskWorkloadIndependence [section, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_arrivals_consistent [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_arrival_sequence_uniq [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_tsk_in_ts [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_jobs_from_ts [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_ts_uniq [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.job_costs_cond_independent [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.pr_task_workload [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.ts [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.tsk [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.t1 [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.t2 [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.ξ [variable, in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.ξpart [variable, in probsa.rt.analysis.independent.task_workload]
pRTA_full [library]
PrWorkConservation [section, in probsa.rt.model.assumptions.pr_work_conserving]
PrWorkConservation.JobReadyRV [variable, in probsa.rt.model.assumptions.pr_work_conserving]
PrWorkConservation.sched [variable, in probsa.rt.model.assumptions.pr_work_conserving]
PrWorkload [section, in probsa.rt.model.workload]
PrWorkloadCat [section, in probsa.rt.model.workload]
PrWorkloadCat.tsk [variable, in probsa.rt.model.workload]
PrWorkloadFacts [section, in probsa.rt.model.workload]
PrWorkloadFacts.H_arrivals_from_ts [variable, in probsa.rt.model.workload]
PrWorkloadFacts.H_tsk_in_ts [variable, in probsa.rt.model.workload]
PrWorkloadFacts.ts [variable, in probsa.rt.model.workload]
PrWorkloadFacts.tsk [variable, in probsa.rt.model.workload]
pr_arrivals_task_between_respect_arrival_curve_mid [lemma, in probsa.rt.analysis.arrivals]
pr_arrivals_task_between_respect_arrival_curve [lemma, in probsa.rt.analysis.arrivals]
pr_arrivals_between_fixed_in_partition [lemma, in probsa.rt.analysis.arrivals]
pr_arrivals_task_between_eq [lemma, in probsa.rt.analysis.arrivals]
pr_arrivals_between_eq [lemma, in probsa.rt.analysis.arrivals]
pr_service_of_jobs_cat [lemma, in probsa.rt.analysis.completion_time]
pr_hep_workload_pr_task_workload_split [lemma, in probsa.rt.model.workload]
pr_workload_of_task_cat [lemma, in probsa.rt.model.workload]
pr_workload_of_hep_tasks [definition, in probsa.rt.model.workload]
pr_workload_of_task [definition, in probsa.rt.model.workload]
pr_workload_of_jobs [definition, in probsa.rt.model.workload]
pr_workload_bounded_by_nth_cost_sum [lemma, in probsa.rt.analysis.work_bound]
pr_cond_joint_pred_eq_cond_eq [lemma, in probsa.probability.conditional]
pr_joint_pred_eq [lemma, in probsa.probability.conditional]
pr_cond_mono_pred [lemma, in probsa.probability.conditional]
pr_cond_eq_pred_0 [lemma, in probsa.probability.conditional]
pr_cond_eq_cond [lemma, in probsa.probability.conditional]
pr_cond_eq_pred [lemma, in probsa.probability.conditional]
pr_cond_xpred1 [lemma, in probsa.probability.conditional]
pr_cond_xpredT [lemma, in probsa.probability.conditional]
pr_cond_axiomatic' [lemma, in probsa.probability.conditional]
pr_cond_axiomatic [lemma, in probsa.probability.conditional]
pr_cond [definition, in probsa.probability.conditional]
pr_task_workload_independence [lemma, in probsa.rt.analysis.independent.task_workload]
pr_schedule [definition, in probsa.rt.behavior.schedule]
pr_completes_at [definition, in probsa.rt.behavior.service]
pr_completed_by [definition, in probsa.rt.behavior.service]
pr_remaining_service [definition, in probsa.rt.behavior.service]
pr_service [definition, in probsa.rt.behavior.service]
pr_work_conserving [definition, in probsa.rt.model.assumptions.pr_work_conserving]
pr_abort_ready_instance [definition, in probsa.rt.model.abort_readiness]
pr_ineq_compl [lemma, in probsa.probability.prob]
pr_pred_compl [lemma, in probsa.probability.prob]
pr_eq_pred_pos [lemma, in probsa.probability.prob]
pr_mono_pred_pos [lemma, in probsa.probability.prob]
pr_eq_measure [lemma, in probsa.probability.prob]
pr_bool_move [lemma, in probsa.probability.prob]
pr_of_union [lemma, in probsa.probability.prob]
pr_leq_intersectionr [lemma, in probsa.probability.prob]
pr_leq_intersectionl [lemma, in probsa.probability.prob]
pr_pos_or_zero [lemma, in probsa.probability.prob]
pr_pos_inv [lemma, in probsa.probability.prob]
pr_xpredT_ext [lemma, in probsa.probability.prob]
pr_zero [lemma, in probsa.probability.prob]
pr_pos [lemma, in probsa.probability.prob]
pr_service_bounded_by_pr_job_cost [lemma, in probsa.rt.model.assumptions.basic]
pr_jobs_come_from_arrival_sequence [definition, in probsa.rt.model.assumptions.basic]
pr_completed_jobs_dont_execute [definition, in probsa.rt.model.assumptions.basic]
pr_jobs_must_arrive_to_execute [definition, in probsa.rt.model.assumptions.basic]
pr_taskset_respects_sporadic_task_model [definition, in probsa.rt.model.assumptions.basic]
pr_arrival_sequence_uniq [definition, in probsa.rt.model.assumptions.basic]
pr_eq_over_partition_is_series [lemma, in probsa.probability.law_of_total_prob]
pr_carry_in_workload_bounded_pr_pend_workload [lemma, in probsa.rt.model.carry_in]
pr_hep_carry_in_workload_split [lemma, in probsa.rt.model.carry_in]
pr_carry_in_workload_of_hep_jobs [definition, in probsa.rt.model.carry_in]
pr_carry_in_workload_of_task [definition, in probsa.rt.model.carry_in]
pr_carry_in_workload [definition, in probsa.rt.model.carry_in]
pr_pend_workload_of_hep_jobs [definition, in probsa.rt.model.carry_in]
pr_pend_workload_of_task [definition, in probsa.rt.model.carry_in]
pr_pend_workload [definition, in probsa.rt.model.carry_in]
pr_cond_indep2 [lemma, in probsa.probability.independence]
pr_jobs_must_be_ready_to_execute [definition, in probsa.rt.model.assumptions.pr_must_be_ready]
pr_respects_policy_at_preemption_point [definition, in probsa.rt.model.assumptions.pr_respects_policy]
pr_consistent_arrival_times [lemma, in probsa.rt.behavior.arrival_sequence]
pr_arrivals_task_between [definition, in probsa.rt.behavior.arrival_sequence]
pr_arrivals_between [definition, in probsa.rt.behavior.arrival_sequence]
pr_arrival_sequence [definition, in probsa.rt.behavior.arrival_sequence]
pr_respects_policy [library]
pr_cost [library]
pr_work_conserving [library]
pr_must_be_ready [library]
pselect [lemma, in probsa.util.boolp]
pselectT [lemma, in probsa.util.boolp]
pWCETs_bounded_by_replaced_pETs [lemma, in probsa.rt.analysis.transformation_properties]
pWCETs_bounded_by_replaced_pETs_steps [lemma, in probsa.rt.analysis.transformation_properties]
pWCETs_bounded_by_replaced_pETs_step [lemma, in probsa.rt.analysis.transformation_properties]
pWCET_to_RVpWCET [definition, in probsa.rt.analysis.pETs_to_pWCETs]
pWCET_cdf [definition, in probsa.rt.model.task]
pWCET_sum1 [projection, in probsa.rt.model.task]
pWCET_nonnegative [projection, in probsa.rt.model.task]
pWCET_pmf [projection, in probsa.rt.model.task]

R

reflect_eq [lemma, in probsa.util.boolp]
relp [definition, in probsa.util.boolp]
replaced_cond_pETs_bounded_by_pWCETs [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_cond_independent [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_from_arr_seq_partition [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_from_arr_seq_partition_steps [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_steps [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_step [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_bounded_by_pWCETs [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_bounded_by_pWCETs_steps [lemma, in probsa.rt.analysis.transformation_properties]
replaced_pETs_bounded_by_pWCETs_step [lemma, in probsa.rt.analysis.transformation_properties]
replace_all_pETs [definition, in probsa.rt.analysis.pETs_to_pWCETs]
replace_all_jobs_pETs [definition, in probsa.rt.analysis.pETs_to_pWCETs]
replace_job_pET [definition, in probsa.rt.analysis.pETs_to_pWCETs]
respects_arrival_curve [lemma, in probsa.rt.analysis.pRTA.pRTA]
response_time𝗔𝗖 [definition, in probsa.rt.model.scheduler]
response_time_exceeds [definition, in probsa.rt.behavior.response_time]
response_time [definition, in probsa.rt.behavior.response_time]
response_time [library]
restrict [definition, in probsa.probability.conditional]
RHS_factorization [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
RightAbsorb [record, in probsa.util.stdpp]
RightAbsorb [inductive, in probsa.util.stdpp]
RightId [record, in probsa.util.stdpp]
RightId [inductive, in probsa.util.stdpp]
right_absorb [projection, in probsa.util.stdpp]
right_absorb [constructor, in probsa.util.stdpp]
right_id [projection, in probsa.util.stdpp]
right_id [constructor, in probsa.util.stdpp]
Rle_min_compat [lemma, in probsa.util.min]
Rmult_comoid [definition, in probsa.util.r_mult]
Rmult_monoid [definition, in probsa.util.r_mult]
Rmult_commutative [lemma, in probsa.util.r_mult]
Rmult_right_id [lemma, in probsa.util.r_mult]
Rmult_left_id [lemma, in probsa.util.r_mult]
Rmult_associative [lemma, in probsa.util.r_mult]
Rmult_eq_compat [lemma, in probsa.util.r_mult]
RTMonotonicScheduler [section, in probsa.rt.model.scheduler]
RTMonotonicScheduler.horizon [variable, in probsa.rt.model.scheduler]
RTMonotonicScheduler.sched [variable, in probsa.rt.model.scheduler]
RTMonotonicScheduler.ζ [variable, in probsa.rt.model.scheduler]
RTMonotonicScheduler.𝓡 [variable, in probsa.rt.model.scheduler]
rt_monotonic_scheduler [definition, in probsa.rt.model.scheduler]
rt_monotonic [library]
rvar_nat_pred_leqop [instance, in probsa.probability.nrvar]
rvar_intersection [instance, in probsa.probability.brvar]
rvar_union [instance, in probsa.probability.brvar]
rvar_neg [instance, in probsa.probability.brvar]
r_mult [library]

S

sample_deadlines [definition, in probsa.rt.behavior.job]
sample_costs [definition, in probsa.rt.behavior.job]
sample_arrivals [definition, in probsa.rt.behavior.job]
sample0_deadlines [definition, in probsa.rt.behavior.job]
sample0_costs [definition, in probsa.rt.behavior.job]
sample0_arrivals [definition, in probsa.rt.behavior.job]
SchedImpliesArrivalTime [section, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime [section, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.A [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.arrived_between [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_j_scheduled_at [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_t_interval [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_j_arrival [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_pr_jobs_must_arrive_to_execute [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_jobs_come_from_arrival_sequence [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.j [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.pr_sched [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.pr_sched [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.t [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.t' [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.Δ [variable, in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.ω [variable, in probsa.rt.model.assumptions.basic]
Schedule [section, in probsa.rt.model.scheduler]
schedule [library]
scheduled_if_before_deadline [lemma, in probsa.rt.analysis.completion_time]
scheduled_at_implies_arrived_between'' [lemma, in probsa.rt.model.assumptions.basic]
scheduled_at_implies_arrived_between' [lemma, in probsa.rt.model.assumptions.basic]
scheduled_at_implies_arrived_between [lemma, in probsa.rt.model.assumptions.basic]
scheduled_at_implies_exists_arrival_time [lemma, in probsa.rt.model.assumptions.basic]
scheduled_job_is_supremum_new [lemma, in probsa.util.prosa.prio_aware]
scheduler [library]
SchedulerHardcoded [section, in probsa.rt.model.scheduler]
SchedulerHardcoded.horizon [variable, in probsa.rt.model.scheduler]
SchedulerHardcoded.ResponseTimeFromScheduler [section, in probsa.rt.model.scheduler]
SchedulerHardcoded.ResponseTimeFromScheduler.completed_by [variable, in probsa.rt.model.scheduler]
SchedulerHardcoded.ResponseTimeFromScheduler.ζ [variable, in probsa.rt.model.scheduler]
SchedulerProperties [section, in probsa.rt.analysis.scheduler_properties]
SchedulerProperties.H_transitive [variable, in probsa.rt.analysis.scheduler_properties]
SchedulerProperties.H_reflexive [variable, in probsa.rt.analysis.scheduler_properties]
SchedulerProperties.H_total [variable, in probsa.rt.analysis.scheduler_properties]
SchedulerProperties.pr_sched [variable, in probsa.rt.analysis.scheduler_properties]
scheduler_properties [library]
scheduler𝗔𝗖 [definition, in probsa.rt.model.scheduler]
scheduler𝗔𝗖_to_rt𝗔𝗖 [definition, in probsa.rt.model.scheduler]
scheduler𝗔𝗖_to_completed𝗔𝗖 [definition, in probsa.rt.model.scheduler]
scheduler𝗔𝗖_to_service𝗔𝗖 [definition, in probsa.rt.model.scheduler]
seq [library]
seq_split [lemma, in probsa.util.seq]
seq_split_take_drop [lemma, in probsa.util.seq]
seq_filter_singleton [lemma, in probsa.util.misc]
SeriesCf_bump [lemma, in probsa.util.bigop_inf]
SeriesC_pos [lemma, in probsa.util.bigop_inf]
SeriesC_scal_l [lemma, in probsa.util.bigop_inf]
Service [section, in probsa.rt.behavior.service]
service [library]
service_monotone_wrt_sched [lemma, in probsa.rt.analysis.scheduler_properties]
Service.pr_sched [variable, in probsa.rt.behavior.service]
service𝗔𝗖 [definition, in probsa.rt.model.scheduler]
some_job_scheduled [lemma, in probsa.rt.analysis.completion_time]
SporadicArrivalBound [section, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.ArrivalTimes [section, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.arr_seq [variable, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.H_valid_inter_min_arrival [variable, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.H_sporadic_model [variable, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.H_valid_arrival_sequence [variable, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.NthJob [section, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.NthJob.dummy [variable, in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.tsk [variable, in probsa.util.prosa.arrival_bound]
SporadicArrivalCurve [section, in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.arr_seq [variable, in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.H_valid_arrival_sequence [variable, in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity [section, in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity.H_valid_inter_min_arrival [variable, in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity.H_sporadic_model [variable, in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity.tsk [variable, in probsa.util.prosa.sporadic_as_curve]
SporadicFacts [section, in probsa.rt.model.carry_in]
SporadicFacts.H_constrained_deadlines [variable, in probsa.rt.model.carry_in]
SporadicFacts.H_sporadic_tasks [variable, in probsa.rt.model.carry_in]
SporadicFacts.H_arrivals_consistent [variable, in probsa.rt.model.carry_in]
SporadicFacts.H_tsk_in_ts [variable, in probsa.rt.model.carry_in]
SporadicFacts.pr_sched [variable, in probsa.rt.model.carry_in]
SporadicFacts.ts [variable, in probsa.rt.model.carry_in]
SporadicFacts.tsk [variable, in probsa.rt.model.carry_in]
sporadic_task_sets_respects_max_arrivals [lemma, in probsa.util.prosa.sporadic_as_curve]
sporadic_arrival_curve_respects_max_arrivals [lemma, in probsa.util.prosa.sporadic_as_curve]
sporadic_task_sets_arrival_curve_valid [lemma, in probsa.util.prosa.sporadic_as_curve]
sporadic_arrival_curve_valid [lemma, in probsa.util.prosa.sporadic_as_curve]
sporadic_task_model_respected [lemma, in probsa.rt.analysis.transformation_properties]
sporadic_task_model_respected_steps [lemma, in probsa.rt.analysis.transformation_properties]
sporadic_task_model_respected_step [lemma, in probsa.rt.analysis.transformation_properties]
sporadic_task_arrivals_bound [lemma, in probsa.util.prosa.arrival_bound]
sporadic_as_curve [library]
stdpp [library]
StepByStepProof [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Cpart [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Cpart' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Cs [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.CsEQU [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.CSpart [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.CSpart' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Cs' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.c0 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Exc [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Exc' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.horizon [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_c0_causes_exceedance [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_ωo_in_Cs [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_cond_independence [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_pWCET_bounds_cond_cdf [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_ξ_pos_prob [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_axiomatic_pWCET [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_rt_monotonic [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Idx [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.j [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.j_rep [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.part [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Pi [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.r [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.S [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.sample_costs' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.sample_costs [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.sched [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Sf [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Sf' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1.H_ineq_ξ_partitioned [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1.ξpart [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1.ξpart' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step10 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step10.H_ineq_without_other_costs [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step11 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step11.H_ineq_c0_causes_exceedance [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step12 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step12.H_almost_pWCET_bounds_cond_cdf [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step13 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.H_ineq_ξ_fixed [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.H_part_unpack_ξ [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξ [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξf [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξf' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξi [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξi' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξpart [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξpart' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξ_equivalence [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step3 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step3.H_ineq_Ω_part [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step4 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step4.H_ineq_conditional [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step5 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step5.H_ineq_algorithmic_𝓡 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step6 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step6.H_ineq_costs_partitioned [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step7 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step7.H_ineq_cost_partitioned [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step8 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step8.H_ineq_cost_partitioned [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step9 [section, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step9.H_ineq_introduce_independence [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.S' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.tsk [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Ω [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ζ [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μ [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μr [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μr' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μ_tsk [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ξ [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ξf [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ξf' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ρ1 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ρ2 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ωo [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓐 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒r [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒r' [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒_pWCET [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓡 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝗔 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝗖 [variable, in probsa.rt.analysis.axiomatic_pWCET_step]
StochasticDomination [section, in probsa.probability.stochastic_order]
StochasticDominationSum [section, in probsa.probability.stochastic_order]
StochasticDominationSum.F1 [variable, in probsa.probability.stochastic_order]
StochasticDominationSum.F2 [variable, in probsa.probability.stochastic_order]
StochasticDominationSum.H_xs2_doms_xs1 [variable, in probsa.probability.stochastic_order]
StochasticDominationSum.H_eq_size [variable, in probsa.probability.stochastic_order]
StochasticDominationSum.H_independent2 [variable, in probsa.probability.stochastic_order]
StochasticDominationSum.H_independent1 [variable, in probsa.probability.stochastic_order]
StochasticDominationSum.xs1 [variable, in probsa.probability.stochastic_order]
StochasticDominationSum.xs2 [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers [section, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_independent' [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_independent [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_dominates_Y [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_dominates_X [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.t [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.X [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.X' [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.Y [variable, in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.Y' [variable, in probsa.probability.stochastic_order]
StochasticOrder [section, in probsa.probability.pmf]
StochasticOrderSum [section, in probsa.probability.pmf]
StochasticOrderSum.F [variable, in probsa.probability.pmf]
StochasticOrderSum.H_bound [variable, in probsa.probability.pmf]
StochasticOrderSum.H_independent [variable, in probsa.probability.pmf]
StochasticOrderSum.p [variable, in probsa.probability.pmf]
StochasticOrderSum.P [variable, in probsa.probability.pmf]
StochasticOrderSum.xs [variable, in probsa.probability.pmf]
StochasticOrder.H_X2_bounded_by_p2 [variable, in probsa.probability.pmf]
StochasticOrder.H_X1_bounded_by_p1 [variable, in probsa.probability.pmf]
StochasticOrder.H_independent [variable, in probsa.probability.pmf]
StochasticOrder.p1 [variable, in probsa.probability.pmf]
StochasticOrder.p2 [variable, in probsa.probability.pmf]
StochasticOrder.X1 [variable, in probsa.probability.pmf]
StochasticOrder.X2 [variable, in probsa.probability.pmf]
stochastic_order [library]
SubOp [record, in probsa.util.notation]
SubOp [inductive, in probsa.util.notation]
subseq_filter [lemma, in probsa.util.seq]
sub_op [projection, in probsa.util.notation]
sub_op [constructor, in probsa.util.notation]
summand_wise_bound_implies_eq [lemma, in probsa.rt.analysis.completion_time]
SumOfDisjointEventsExists [section, in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.B [variable, in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.H_Bi_disjoint [variable, in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.I [variable, in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.Ω [variable, in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.μ [variable, in probsa.probability.law_of_total_prob]
SumOfPartitionEventsExists [section, in probsa.probability.law_of_total_prob]
SumOverPartitions [section, in probsa.util.bigop]
SumOverPartitions.f [variable, in probsa.util.bigop]
SumOverPartitions.H_no_partition_missing [variable, in probsa.util.bigop]
SumOverPartitions.P [variable, in probsa.util.bigop]
SumOverPartitions.sum_of_partition [variable, in probsa.util.bigop]
SumOverPartitions.X [variable, in probsa.util.bigop]
SumOverPartitions.xs [variable, in probsa.util.bigop]
SumOverPartitions.x_to_y [variable, in probsa.util.bigop]
SumOverPartitions.Y [variable, in probsa.util.bigop]
SumOverPartitions.ys [variable, in probsa.util.bigop]
sumrv_sumpmf_respect_stochastic_order [lemma, in probsa.probability.pmf]
sumrv_respects_stochastic_order [lemma, in probsa.probability.stochastic_order]
sum_nrvar_sum_nat [lemma, in probsa.probability.nrvar]
sum_over_partitions_le [lemma, in probsa.util.bigop]
supremum_monotone_wrt_subset [lemma, in probsa.util.seq]
surj [projection, in probsa.util.stdpp]
Surj [record, in probsa.util.stdpp]
surj [constructor, in probsa.util.stdpp]
Surj [inductive, in probsa.util.stdpp]
SustainableUniFPFP [section, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.arr_seq [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_transitive [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_reflexive [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_total [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_arrival_sequence_uniq [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_consistent_arrival_times [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_cost_monotone [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.job_ready2 [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.job_ready1 [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone [section, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.H_service_monotone_wrt_schedules [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.H_j_not_completed_sched2 [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.H_j_sched1 [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.j [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.t [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.sched1 [variable, in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.sched2 [variable, in probsa.rt.analysis.scheduler_properties]
sustainable_uni_fp_fp [lemma, in probsa.rt.analysis.scheduler_properties]
swithing_point_of_monotone_function [lemma, in probsa.util.misc]
symmetry_iff [lemma, in probsa.util.stdpp]
system [record, in probsa.rt.analysis.pETs_to_pWCETs]

T

task [library]
TaskWorkloadBounded [section, in probsa.rt.model.workload]
TaskWorkloadBounded.A [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_j_arrives_at_A [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_job_of_task [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrives_in [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_constrained_deadlines [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_sporadic_arrivals [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_inter_arrival_pos [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrivals_from_ts [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_tsk_in_ts [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrival_sequence_uniq [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrivals_cost_consistent [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrivals_consistent [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.j [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.pr_sched [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.ts [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.tsk [variable, in probsa.rt.model.workload]
TaskWorkloadBounded.ω [variable, in probsa.rt.model.workload]
task_job_cost_independence_ac [lemma, in probsa.rt.analysis.nth_cost]
task_job_cost_independence [lemma, in probsa.rt.analysis.nth_cost]
task_job_cost_independence_aux [lemma, in probsa.rt.analysis.nth_cost]
task_job [definition, in probsa.rt.analysis.nth_cost]
task_workload_bounded_by_nth_cost_sum [lemma, in probsa.rt.analysis.pRTA.pRTA]
task_cost_is_WCET [definition, in probsa.rt.model.WCET]
task_arrivals_between_subset [lemma, in probsa.util.prosa.arrival_bound]
task_arrivals_between_uniq [lemma, in probsa.util.prosa.arrival_bound]
task_arrivals_between_sorted [lemma, in probsa.util.prosa.arrival_bound]
task_workload [library]
TDFPBound [section, in probsa.rt.analysis.pRTA.pRTA]
TDFPBound.ts [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPBound.tsk [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded [section, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.h [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_of_task [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_tsk_in_ts [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_conditional_cost_bounded_by_pWCET [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_independent_arr_seq [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_independent_cond_arr_seq [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_identically_distr [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_bounded_by_pWCET [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_independent [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_constrained_deadlines [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_task_min_inter_arrival_time_valid [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_sporadic_arrivals [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_arrivals_from_ts [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_arrivals_and_costs_consistent [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_from_ts [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_ts_uniq [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_must_be_ready_to_execute [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_must_arrive_to_execute [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_completed_jobs_dont_execute [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_come_from_arrival_sequence [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_respects_policy_at_preemption_point [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_work_conserving [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_horizon_far_enough [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_axiomatic_pWCET [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_transitive_priorities [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_priority_is_reflexive [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.j [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.sched [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep [section, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.A [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.cond_cost_j [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_neq [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_tsko_hep [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_tsko_in_ts [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_arrivals_unique [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_arrivals_consistent [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_Δ_in_range [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_job_arrives_at [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_ω_in_ξ [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.i [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.interfering_workload [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.lengths [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.task_workload [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.tsko [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.V [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.workload_exceeds_time [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.Δ [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ξ [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ξpart [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ρ [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ω [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.ts [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.tsk [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.ζ [variable, in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.𝓡 [variable, in probsa.rt.analysis.pRTA.pRTA]
tdfp_zero_when_job_does_not_arrive [lemma, in probsa.rt.analysis.pRTA.pRTA]
to_fintype [definition, in probsa.util.misc]
to_distrib [definition, in probsa.rt.model.pRBF]
Transformation [section, in probsa.rt.analysis.pETs_to_pWCETs]
TransformationEnsuresCondCostsBounded [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ζ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ξ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ξpart [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ρ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeqPartition [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeqPartition.H_jrep_notin_jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeqPartition.jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.H_jrep_notin_jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.ξa [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.ξf [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.ξf' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.j_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.H_jrep_notin_jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.jobs_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.ξ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.ξpart [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.ξ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.ξpart [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.ρ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.ζ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBoundedByPWCET [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBoundedByPWCET.H_job_of_task [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBoundedByPWCET.tsk [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBounds [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBounds.H_jobs_neq [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.j_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.H_job_of_task [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.H_j_in_reps [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.H_jobs_uniq [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.jobs_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.tsk [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step3 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step3.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step3.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.ζ [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.H_jrep_notin_jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.j_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.H_jobs_uniq [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.jobs_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step3 [section, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step3.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step3.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.ζ [variable, in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence [section, in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.j_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.ζ [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.j_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2.jobs_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step3 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step3.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step3.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.ζ [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.job_deadline [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.BIG [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.h [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.j_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.h [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.H_horizon_big [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.h [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.H_horizon_big [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.ζ [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.sched [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.j [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.j_rep [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.ts [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.jobs [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.ts [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3 [section, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3.S [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3.S' [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3.ts [variable, in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.ζ [variable, in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_remove_part_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_eq_part_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_remove_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_eq_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_cons_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_independence_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_preserves_arr_seq [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_consistent_arrivals [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_consistent_arrivals_steps [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_consistent_arrivals_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_big_horizon [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_big_horizon_steps [lemma, in probsa.rt.analysis.transformation_properties]
transformation_respects_big_horizon_step [lemma, in probsa.rt.analysis.transformation_properties]
transformation_is_pRT_monotone_step13 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step12 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step11 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step10 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step9 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step8 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step7 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step6 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step5 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step4 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step3 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step2 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step1 [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_properties [library]
trichotomy [projection, in probsa.util.stdpp]
Trichotomy [record, in probsa.util.stdpp]
trichotomy [constructor, in probsa.util.stdpp]
Trichotomy [inductive, in probsa.util.stdpp]
trichotomyT [projection, in probsa.util.stdpp]
TrichotomyT [record, in probsa.util.stdpp]
trichotomyT [constructor, in probsa.util.stdpp]
TrichotomyT [inductive, in probsa.util.stdpp]
trueE [lemma, in probsa.util.boolp]
tr_eq [library]

U

Undef [constructor, in probsa.util.etime]
union [projection, in probsa.util.stdpp]
Union [record, in probsa.util.stdpp]
union [constructor, in probsa.util.stdpp]
Union [inductive, in probsa.util.stdpp]
union_list [definition, in probsa.util.stdpp]
union_disj_eq_sum_prob [lemma, in probsa.probability.prob]
UniScheduleAsSchedulerAC [section, in probsa.rt.analysis.scheduler_properties]
UniScheduleAsSchedulerAC.arr_seq [variable, in probsa.rt.analysis.scheduler_properties]
UniScheduleAsSchedulerAC.JLDP [variable, in probsa.rt.analysis.scheduler_properties]
UniScheduleAsSchedulerAC.job_deadline [variable, in probsa.rt.analysis.scheduler_properties]
UniScheduleAsSchedulerAC.readiness [variable, in probsa.rt.analysis.scheduler_properties]
unzip1_map_nth_zip [lemma, in probsa.util.zip]
update [definition, in probsa.rt.model.scheduler]

V

ValidpWCETRemainsValid [section, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.horizon [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.H_rt_monotonic [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas [section, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalBoundedness [section, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalBoundedness.H_job_cost_cond_bounded_by_pWCET [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence [section, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.H_job_cost_cond_independent [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.𝓒_fix' [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.𝓒_fix [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.𝗖 [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.j [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.j_rep [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.P [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.P' [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.S [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.S' [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.Ω [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.μ [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ξ [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ξf [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ξf' [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.𝓐 [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.𝓒 [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.sched [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ζ [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.𝓡 [variable, in probsa.rt.analysis.valid_pWCET_remains_valid]
valid_min_inter_arrival [definition, in probsa.rt.model.min_inter_arrival]
valid_axiomatic_pWCET_remains_valid [lemma, in probsa.rt.analysis.valid_pWCET_remains_valid]
valid_arrival_curve [lemma, in probsa.rt.analysis.pRTA.pRTA]
valid_𝓡 [lemma, in probsa.rt.model.scheduler]
valid_pWCET_remains_valid [library]

W

WCATDFPtoTDFP [section, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.h [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_WCA_TDFP_bounded [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_Λ_bounded [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_job_of_task [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_tsk_in_ts [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.j [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.sched [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.ts [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.tsk [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.Λ [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.ζ [variable, in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.𝓡 [variable, in probsa.rt.analysis.pRTA.pRTA]
WCA_TDFP_bounded_implies_TDFP_bounded [lemma, in probsa.rt.analysis.pRTA.pRTA]
WCET [section, in probsa.rt.model.WCET]
WCET [library]
WCETisAxiomaticPWCET [section, in probsa.rt.analysis.WCET_is_pWCET]
WCETisAxiomaticPWCET.H_task_cost_is_valid_WCET [variable, in probsa.rt.analysis.WCET_is_pWCET]
WCET_is_axiomatic_pWCET [lemma, in probsa.rt.analysis.WCET_is_pWCET]
WCET_pmf [instance, in probsa.rt.analysis.WCET_is_pWCET]
WCET_is_pWCET [library]
wlog_neg [lemma, in probsa.util.boolp]
workload [library]
WorkloadLemmasDetCostStocArr [section, in probsa.rt.model.workload]
WorkloadLemmasDetCostStocArr.tsk [variable, in probsa.rt.model.workload]
workload_le_service [lemma, in probsa.rt.analysis.completion_time]
workload_of_jobs_widen [lemma, in probsa.rt.model.workload]
workload_of_jobs_xpredT [lemma, in probsa.rt.model.workload]
workload_bounded_by_cost_plus_interference [lemma, in probsa.rt.analysis.pRTA.pRTA]
work_bound [library]

X

xpredpC [abbreviation, in probsa.util.boolp]
xpredpD [abbreviation, in probsa.util.boolp]
xpredpI [abbreviation, in probsa.util.boolp]
xpredpT [abbreviation, in probsa.util.boolp]
xpredpU [abbreviation, in probsa.util.boolp]
xpredp0 [abbreviation, in probsa.util.boolp]
xpreimp [abbreviation, in probsa.util.boolp]
xrelpU [abbreviation, in probsa.util.boolp]

Z

Zip [section, in probsa.util.zip]
zip [library]
zip_map_pr_eq [lemma, in probsa.util.zip]
zip_map_rvar_eq [lemma, in probsa.util.zip]
zip_foldr_andb_seq_eq [lemma, in probsa.util.zip]
zip_map [lemma, in probsa.util.zip]

other

`[< _ >] (bool_scope) [notation, in probsa.util.boolp]
𝔽< _ , _ >{[ _ | _ ]} (probability_scope) [notation, in probsa.probability.conditional]
𝔽< _ , _ >{[ _ | _ ]}( _ ) (probability_scope) [notation, in probsa.probability.conditional]
𝔽< _ >{[ _ | _ ]}( _ ) (probability_scope) [notation, in probsa.probability.conditional]
ℙ< _ , _ >{[ _ | _ ]} (probability_scope) [notation, in probsa.probability.conditional]
ℙ< _ >{[ _ | _ ]} (probability_scope) [notation, in probsa.probability.conditional]
∑[rv]_{ _ < _ } _ (probability_scope) [notation, in probsa.probability.nrvar]
∑[rv]_{ _ <- _ } _ (probability_scope) [notation, in probsa.probability.nrvar]
∑[rv]_{ _ <- _ | _ } _ (probability_scope) [notation, in probsa.probability.nrvar]
⨁_{ _ < _ } _ (probability_scope) [notation, in probsa.probability.pmf]
⨁_{ _ <= _ < _ } _ (probability_scope) [notation, in probsa.probability.pmf]
⨁_{ _ <- _ | _ } _ (probability_scope) [notation, in probsa.probability.pmf]
_ ⪯ _ (probability_scope) [notation, in probsa.probability.dominance_relation]
𝔽< _ >{[ _ ]} (probability_scope) [notation, in probsa.probability.cdf]
𝔽< _ >{[ _ ]}( _ ) (probability_scope) [notation, in probsa.probability.cdf]
_ ◁{ _ } (probability_scope) [notation, in probsa.probability.partition]
I[ _ ] (probability_scope) [notation, in probsa.util.indicator]
∑[∞]_{ _ <- _ } _ (probability_scope) [notation, in probsa.util.notation]
∑_{ _ <= _ <= _ } _ (probability_scope) [notation, in probsa.util.notation]
∑_{ _ <= _ < _ } _ (probability_scope) [notation, in probsa.util.notation]
ℙ< _ >{[ _ ]} (probability_scope) [notation, in probsa.util.notation]
(.∩ _ ) (stdpp_scope) [notation, in probsa.util.stdpp]
( _ ∩.) (stdpp_scope) [notation, in probsa.util.stdpp]
(∩) (stdpp_scope) [notation, in probsa.util.stdpp]
_ ∩ _ (stdpp_scope) [notation, in probsa.util.stdpp]
⋃ _ (stdpp_scope) [notation, in probsa.util.stdpp]
(.∪ _ ) (stdpp_scope) [notation, in probsa.util.stdpp]
( _ ∪.) (stdpp_scope) [notation, in probsa.util.stdpp]
(∪) (stdpp_scope) [notation, in probsa.util.stdpp]
_ ∪ _ (stdpp_scope) [notation, in probsa.util.stdpp]
∅ (stdpp_scope) [notation, in probsa.util.stdpp]
_ ≢@{ _ } _ (stdpp_scope) [notation, in probsa.util.stdpp]
(≢@{ _ } ) (stdpp_scope) [notation, in probsa.util.stdpp]
(≡@{ _ } ) (stdpp_scope) [notation, in probsa.util.stdpp]
(.≢ _ ) (stdpp_scope) [notation, in probsa.util.stdpp]
( _ ≢.) (stdpp_scope) [notation, in probsa.util.stdpp]
_ ≢ _ (stdpp_scope) [notation, in probsa.util.stdpp]
(≢) (stdpp_scope) [notation, in probsa.util.stdpp]
(.≡ _ ) (stdpp_scope) [notation, in probsa.util.stdpp]
( _ ≡.) (stdpp_scope) [notation, in probsa.util.stdpp]
(≡) (stdpp_scope) [notation, in probsa.util.stdpp]
_ ≡@{ _ } _ (stdpp_scope) [notation, in probsa.util.stdpp]
_ ≡ _ (stdpp_scope) [notation, in probsa.util.stdpp]
_ ≠@{ _ } _ (stdpp_scope) [notation, in probsa.util.stdpp]
(≠@{ _ } ) (stdpp_scope) [notation, in probsa.util.stdpp]
(=@{ _ } ) (stdpp_scope) [notation, in probsa.util.stdpp]
_ =@{ _ } _ (stdpp_scope) [notation, in probsa.util.stdpp]
(.≠ _ ) (stdpp_scope) [notation, in probsa.util.stdpp]
( _ ≠.) (stdpp_scope) [notation, in probsa.util.stdpp]
(≠) (stdpp_scope) [notation, in probsa.util.stdpp]
(.= _ ) (stdpp_scope) [notation, in probsa.util.stdpp]
( _ =.) (stdpp_scope) [notation, in probsa.util.stdpp]
(=) (stdpp_scope) [notation, in probsa.util.stdpp]
_ ⟨-⟩ _ (stdpp_scope) [notation, in probsa.util.notation]
_ ⟨+⟩ _ (stdpp_scope) [notation, in probsa.util.notation]
! _ (stdpp_scope) [notation, in probsa.util.notation]
_ ⟨<⟩ _ (stdpp_scope) [notation, in probsa.util.notation]
_ ⟨<=⟩ _ (stdpp_scope) [notation, in probsa.util.notation]
_ ⟨=⟩ _ (stdpp_scope) [notation, in probsa.util.notation]
{eclassic _ } (type_scope) [notation, in probsa.util.boolp]
{classic _ } (type_scope) [notation, in probsa.util.boolp]
_ ⊕ _ [notation, in probsa.probability.pmf]
Λ [definition, in probsa.rt.analysis.pRTA.pRTA]
Ω_of [projection, in probsa.rt.analysis.pETs_to_pWCETs]
Ω_partition [record, in probsa.probability.partition]
μ_of [projection, in probsa.rt.analysis.pETs_to_pWCETs]
ξf_and_Sf_eq_prob [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
ξi_eq_ξ' [lemma, in probsa.rt.analysis.axiomatic_pWCET_step]
ξ_fix [definition, in probsa.rt.model.events]
σpt [definition, in probsa.probability.law_of_total_prob]
σpt_cov [lemma, in probsa.probability.law_of_total_prob]
σpt_inj [lemma, in probsa.probability.law_of_total_prob]
𝓐_of [projection, in probsa.rt.analysis.pETs_to_pWCETs]
𝓒_of [projection, in probsa.rt.analysis.pETs_to_pWCETs]
𝓒_fix [definition, in probsa.rt.model.events]

---

Notation Index

F

_ < _ [in probsa.util.boolp]
_ <= _ [in probsa.util.boolp]

other

`[< _ >] (bool_scope) [in probsa.util.boolp]
𝔽< _ , _ >{[ _ | _ ]} (probability_scope) [in probsa.probability.conditional]
𝔽< _ , _ >{[ _ | _ ]}( _ ) (probability_scope) [in probsa.probability.conditional]
𝔽< _ >{[ _ | _ ]}( _ ) (probability_scope) [in probsa.probability.conditional]
ℙ< _ , _ >{[ _ | _ ]} (probability_scope) [in probsa.probability.conditional]
ℙ< _ >{[ _ | _ ]} (probability_scope) [in probsa.probability.conditional]
∑[rv]_{ _ < _ } _ (probability_scope) [in probsa.probability.nrvar]
∑[rv]_{ _ <- _ } _ (probability_scope) [in probsa.probability.nrvar]
∑[rv]_{ _ <- _ | _ } _ (probability_scope) [in probsa.probability.nrvar]
⨁_{ _ < _ } _ (probability_scope) [in probsa.probability.pmf]
⨁_{ _ <= _ < _ } _ (probability_scope) [in probsa.probability.pmf]
⨁_{ _ <- _ | _ } _ (probability_scope) [in probsa.probability.pmf]
_ ⪯ _ (probability_scope) [in probsa.probability.dominance_relation]
𝔽< _ >{[ _ ]} (probability_scope) [in probsa.probability.cdf]
𝔽< _ >{[ _ ]}( _ ) (probability_scope) [in probsa.probability.cdf]
_ ◁{ _ } (probability_scope) [in probsa.probability.partition]
I[ _ ] (probability_scope) [in probsa.util.indicator]
∑[∞]_{ _ <- _ } _ (probability_scope) [in probsa.util.notation]
∑_{ _ <= _ <= _ } _ (probability_scope) [in probsa.util.notation]
∑_{ _ <= _ < _ } _ (probability_scope) [in probsa.util.notation]
ℙ< _ >{[ _ ]} (probability_scope) [in probsa.util.notation]
(.∩ _ ) (stdpp_scope) [in probsa.util.stdpp]
( _ ∩.) (stdpp_scope) [in probsa.util.stdpp]
(∩) (stdpp_scope) [in probsa.util.stdpp]
_ ∩ _ (stdpp_scope) [in probsa.util.stdpp]
⋃ _ (stdpp_scope) [in probsa.util.stdpp]
(.∪ _ ) (stdpp_scope) [in probsa.util.stdpp]
( _ ∪.) (stdpp_scope) [in probsa.util.stdpp]
(∪) (stdpp_scope) [in probsa.util.stdpp]
_ ∪ _ (stdpp_scope) [in probsa.util.stdpp]
∅ (stdpp_scope) [in probsa.util.stdpp]
_ ≢@{ _ } _ (stdpp_scope) [in probsa.util.stdpp]
(≢@{ _ } ) (stdpp_scope) [in probsa.util.stdpp]
(≡@{ _ } ) (stdpp_scope) [in probsa.util.stdpp]
(.≢ _ ) (stdpp_scope) [in probsa.util.stdpp]
( _ ≢.) (stdpp_scope) [in probsa.util.stdpp]
_ ≢ _ (stdpp_scope) [in probsa.util.stdpp]
(≢) (stdpp_scope) [in probsa.util.stdpp]
(.≡ _ ) (stdpp_scope) [in probsa.util.stdpp]
( _ ≡.) (stdpp_scope) [in probsa.util.stdpp]
(≡) (stdpp_scope) [in probsa.util.stdpp]
_ ≡@{ _ } _ (stdpp_scope) [in probsa.util.stdpp]
_ ≡ _ (stdpp_scope) [in probsa.util.stdpp]
_ ≠@{ _ } _ (stdpp_scope) [in probsa.util.stdpp]
(≠@{ _ } ) (stdpp_scope) [in probsa.util.stdpp]
(=@{ _ } ) (stdpp_scope) [in probsa.util.stdpp]
_ =@{ _ } _ (stdpp_scope) [in probsa.util.stdpp]
(.≠ _ ) (stdpp_scope) [in probsa.util.stdpp]
( _ ≠.) (stdpp_scope) [in probsa.util.stdpp]
(≠) (stdpp_scope) [in probsa.util.stdpp]
(.= _ ) (stdpp_scope) [in probsa.util.stdpp]
( _ =.) (stdpp_scope) [in probsa.util.stdpp]
(=) (stdpp_scope) [in probsa.util.stdpp]
_ ⟨-⟩ _ (stdpp_scope) [in probsa.util.notation]
_ ⟨+⟩ _ (stdpp_scope) [in probsa.util.notation]
! _ (stdpp_scope) [in probsa.util.notation]
_ ⟨<⟩ _ (stdpp_scope) [in probsa.util.notation]
_ ⟨<=⟩ _ (stdpp_scope) [in probsa.util.notation]
_ ⟨=⟩ _ (stdpp_scope) [in probsa.util.notation]
{eclassic _ } (type_scope) [in probsa.util.boolp]
{classic _ } (type_scope) [in probsa.util.boolp]
_ ⊕ _ [in probsa.probability.pmf]

---

Module Index

F

FunOrder [in probsa.util.boolp]
FunOrder.Exports [in probsa.util.boolp]

---

Variable Index

A

ArrivalsConsistentWithDeadlines.H_arrivals_consistent [in probsa.rt.model.assumptions.basic]
ArrSeqUniq.ξ [in probsa.rt.behavior.arrival_sequence]
AxiomaticPWCET.ξ_pr [in probsa.rt.model.axiomatic_pWCET]

B

BasicLemmas.H_independent [in probsa.probability.stochastic_order]
BasicLemmas.X [in probsa.probability.stochastic_order]
BasicLemmas.Y [in probsa.probability.stochastic_order]

C

classicType.T [in probsa.util.boolp]
CommonAssumptions.pr_sched [in probsa.rt.model.assumptions.basic]
CommonAssumptions.ts [in probsa.rt.model.assumptions.basic]
CommonAssumptions.tsk [in probsa.rt.model.assumptions.basic]
CompletionLemmas.sched [in probsa.rt.analysis.completion]
CompletionTimeExists.H_workload_is_consumed [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_non_empty [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_jobs_come_from_arrival_sequence [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_jobs_must_arrive_to_execute [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_completed_jobs_dont_execute [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_pr_jobs_must_be_ready_to_execute [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_respects_policy_at_preemption_point [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_work_conserving [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_arrivals_consistent [in probsa.rt.analysis.completion_time]
CompletionTimeExists.H_transitive_priorities [in probsa.rt.analysis.completion_time]
CompletionTimeExists.sched [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.ARR1 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.ARR2 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_not_completed [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_deadline_in_future [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_arrival [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_hep_tsk [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_workload_is_consumed [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.H_non_empty [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.j [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.P1 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.P2 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.t [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Δ [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.ω [in probsa.rt.analysis.completion_time]
CompletionTimeExists.t [in probsa.rt.analysis.completion_time]
CompletionTimeExists.tsk [in probsa.rt.analysis.completion_time]
CompletionTimeExists.V [in probsa.rt.analysis.completion_time]
CompletionTimeExists.Δ [in probsa.rt.analysis.completion_time]
CompletionTimeExists.ω [in probsa.rt.analysis.completion_time]

E

eclassicType.T [in probsa.util.boolp]

F

FunOrder.FunLattice.aT [in probsa.util.boolp]
FunOrder.FunLattice.d [in probsa.util.boolp]
FunOrder.FunLattice.T [in probsa.util.boolp]
FunOrder.FunOrder.aT [in probsa.util.boolp]
FunOrder.FunOrder.d [in probsa.util.boolp]
FunOrder.FunOrder.T [in probsa.util.boolp]

I

IndependentExtend.F [in probsa.probability.independence]
IndependentFlatten.f [in probsa.probability.independence]
IndependentFlatten.xs [in probsa.probability.independence]
IndependentFlatten.ys [in probsa.probability.independence]
IndependentMap.F [in probsa.probability.independence]
IndependentSum.F [in probsa.probability.independence]
Indep2.IndepExtL.f [in probsa.probability.independence]
Indep2.IndepExtL.X1 [in probsa.probability.independence]
Indep2.IndepExtL.X2 [in probsa.probability.independence]
Indep2.IndepExtL.Y [in probsa.probability.independence]
Indep2.IndepExt.f1 [in probsa.probability.independence]
Indep2.IndepExt.f2 [in probsa.probability.independence]
Indep2.IndepExt.X1 [in probsa.probability.independence]
Indep2.IndepExt.X2 [in probsa.probability.independence]
Indep2.IndepExt.Y1 [in probsa.probability.independence]
Indep2.IndepExt.Y2 [in probsa.probability.independence]

J

JobCostWorkloadIndependent.H_job_costs_cond_independent [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.H_job_of_task [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.H_tsk_in_ts [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.H_arrivals_consistent [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.INωξ [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.j [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.POS [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.t [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ts [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.tsk [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.Δ [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ξ [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ξpart [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.ω [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.𝓒 [in probsa.rt.analysis.independent.cost_and_workload]
JobCostWorkloadIndependent.𝓦 [in probsa.rt.analysis.independent.cost_and_workload]

L

LawOfTotalProbabilityProd.A [in probsa.probability.law_of_total_prob]
LawOfTotalProbabilityProd.S [in probsa.probability.law_of_total_prob]
LawOfTotalProbability.B [in probsa.probability.law_of_total_prob]
LawOfTotalProbability.H_Bi_disjoint [in probsa.probability.law_of_total_prob]
LawOfTotalProbability.H_Bi_covers [in probsa.probability.law_of_total_prob]
LawOfTotalProbability.I [in probsa.probability.law_of_total_prob]
LawOfTotalProbability.P [in probsa.probability.law_of_total_prob]

M

MainLemma.horizon [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.H_rt_monotonic [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.H_axiomatic_pWCET [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.initial_system [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.sched1 [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.sched2 [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.simplified_system [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.Ωg [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.Ωs [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.ζ [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.μg [in probsa.rt.analysis.axiomatic_pWCET_full]
MainLemma.μs [in probsa.rt.analysis.axiomatic_pWCET_full]
MinimumInterArrival.ξ_pr [in probsa.rt.model.min_inter_arrival]

N

NthCostLemmas.H_tsk_in_ts [in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_ts_uniq [in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_job_costs_independent [in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_arrivals_consistent [in probsa.rt.analysis.nth_cost]
NthCostLemmas.H_arrival_sequence_uniq [in probsa.rt.analysis.nth_cost]
NthCostLemmas.pr_sched [in probsa.rt.analysis.nth_cost]
NthCostLemmas.ts [in probsa.rt.analysis.nth_cost]
NthCostLemmas.tsk [in probsa.rt.analysis.nth_cost]

P

PartitionTransfer.ExtendPartition.j [in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition.P [in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition.S [in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition.S' [in probsa.rt.analysis.partition_transfer]
PrArrivalLemmas.H_valid_arrival_curve [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.H_respects_arrival_curve [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.H_tsk_in_ts [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.ts [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.tsk [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.Ω [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.μ [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.ξ [in probsa.rt.analysis.arrivals]
PrArrivalLemmas.ξpart [in probsa.rt.analysis.arrivals]
PrArrivalsBetween.ξ [in probsa.rt.behavior.arrival_sequence]
PrCarryInWorkloadFacts.H_arrivals_consistent [in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.H_arrivals_from_ts [in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.H_tsk_in_ts [in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.pr_sched [in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.ts [in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts.tsk [in probsa.rt.model.carry_in]
PrCarryInWorkload.pr_sched [in probsa.rt.model.carry_in]
PrioAwareUniprocessorScheduler.arr_seq [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_transitive [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_total [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_reflexive_priorities [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_valid_preemption_behavior [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_nonclairvoyant_job_readiness [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.H_consistent_arrival_times [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.idle_state [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.policy [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.prefix [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.PState [in probsa.util.prosa.prio_aware]
PrioAwareUniprocessorScheduler.schedule [in probsa.util.prosa.prio_aware]
PrMustBeReadyToExecture.JobReadyRV [in probsa.rt.model.assumptions.pr_must_be_ready]
PrMustBeReadyToExecture.sched [in probsa.rt.model.assumptions.pr_must_be_ready]
ProbabilisticResponseTimeMonotonicity.horizon [in probsa.rt.model.rt_monotonic]
ProbabilisticResponseTimeMonotonicity.pr_sched_Ωs [in probsa.rt.model.rt_monotonic]
ProbabilisticResponseTimeMonotonicity.pr_sched_Ωg [in probsa.rt.model.rt_monotonic]
ProbabilisticRTA.h [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_job_of_task [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_axiomatic_pWCET [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_sporadic [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_all_jobs_from_ts [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_horizon_after_deadlines [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_arrivals_agree_with_costs [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_tsk_in_ts [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_valid_sporadic [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_constrained_deadlines [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_ts_uniq [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_priority_is_transitive [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_priority_is_reflexive [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.H_priority_is_total [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.j [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.ts [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.tsk [in probsa.rt.analysis.pRTA.pRTA_full]
ProbabilisticRTA.𝓡 [in probsa.rt.analysis.pRTA.pRTA_full]
ProofOfTheorem1.horizon [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.H_axiomatic_pWCET [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.H_rt_monotonic [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.j [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.j_rep [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.S [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.sched [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.S' [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.ζ [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.𝓡j [in probsa.rt.analysis.axiomatic_pWCET_step]
ProofOfTheorem1.𝓡j' [in probsa.rt.analysis.axiomatic_pWCET_step]
PrPendWorkload.pr_sched [in probsa.rt.model.carry_in]
PrRespectsPolicyAtPreemptionPoint.JobReadyRV [in probsa.rt.model.assumptions.pr_respects_policy]
PrRespectsPolicyAtPreemptionPoint.sched [in probsa.rt.model.assumptions.pr_respects_policy]
PrResponseTime.horizon [in probsa.rt.behavior.response_time]
PrResponseTime.sched [in probsa.rt.behavior.response_time]
PrServiceBounded.H_pr_completed_jobs_dont_execute [in probsa.rt.model.assumptions.basic]
PrServiceBounded.H_unit_service_proc_model [in probsa.rt.model.assumptions.basic]
PrServiceBounded.pr_sched [in probsa.rt.model.assumptions.basic]
PrTaskWorkloadBoundedNthCost.H_job_costs_identically_distr [in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_job_costs_independent [in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_job_costs_independent_arr_seq [in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_arrival_sequence_uniq [in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.H_arrivals_consistent [in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.tsk [in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.ξ [in probsa.rt.analysis.work_bound]
PrTaskWorkloadBoundedNthCost.ξpart [in probsa.rt.analysis.work_bound]
PrTaskWorkloadIndependence.H_arrivals_consistent [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_arrival_sequence_uniq [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_tsk_in_ts [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_jobs_from_ts [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.H_ts_uniq [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.job_costs_cond_independent [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.pr_task_workload [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.ts [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.tsk [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.t1 [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.t2 [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.ξ [in probsa.rt.analysis.independent.task_workload]
PrTaskWorkloadIndependence.ξpart [in probsa.rt.analysis.independent.task_workload]
PrWorkConservation.JobReadyRV [in probsa.rt.model.assumptions.pr_work_conserving]
PrWorkConservation.sched [in probsa.rt.model.assumptions.pr_work_conserving]
PrWorkloadCat.tsk [in probsa.rt.model.workload]
PrWorkloadFacts.H_arrivals_from_ts [in probsa.rt.model.workload]
PrWorkloadFacts.H_tsk_in_ts [in probsa.rt.model.workload]
PrWorkloadFacts.ts [in probsa.rt.model.workload]
PrWorkloadFacts.tsk [in probsa.rt.model.workload]

R

RTMonotonicScheduler.horizon [in probsa.rt.model.scheduler]
RTMonotonicScheduler.sched [in probsa.rt.model.scheduler]
RTMonotonicScheduler.ζ [in probsa.rt.model.scheduler]
RTMonotonicScheduler.𝓡 [in probsa.rt.model.scheduler]

S

SchedImpliesArrivalTime.A [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.arrived_between [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_j_scheduled_at [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_t_interval [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_j_arrival [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_pr_jobs_must_arrive_to_execute [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.H_jobs_come_from_arrival_sequence [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.j [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.pr_sched [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.pr_sched [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.t [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.t' [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.Δ [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime.ω [in probsa.rt.model.assumptions.basic]
SchedulerHardcoded.horizon [in probsa.rt.model.scheduler]
SchedulerHardcoded.ResponseTimeFromScheduler.completed_by [in probsa.rt.model.scheduler]
SchedulerHardcoded.ResponseTimeFromScheduler.ζ [in probsa.rt.model.scheduler]
SchedulerProperties.H_transitive [in probsa.rt.analysis.scheduler_properties]
SchedulerProperties.H_reflexive [in probsa.rt.analysis.scheduler_properties]
SchedulerProperties.H_total [in probsa.rt.analysis.scheduler_properties]
SchedulerProperties.pr_sched [in probsa.rt.analysis.scheduler_properties]
Service.pr_sched [in probsa.rt.behavior.service]
SporadicArrivalBound.arr_seq [in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.H_valid_inter_min_arrival [in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.H_sporadic_model [in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.H_valid_arrival_sequence [in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.NthJob.dummy [in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.tsk [in probsa.util.prosa.arrival_bound]
SporadicArrivalCurve.arr_seq [in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.H_valid_arrival_sequence [in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity.H_valid_inter_min_arrival [in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity.H_sporadic_model [in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity.tsk [in probsa.util.prosa.sporadic_as_curve]
SporadicFacts.H_constrained_deadlines [in probsa.rt.model.carry_in]
SporadicFacts.H_sporadic_tasks [in probsa.rt.model.carry_in]
SporadicFacts.H_arrivals_consistent [in probsa.rt.model.carry_in]
SporadicFacts.H_tsk_in_ts [in probsa.rt.model.carry_in]
SporadicFacts.pr_sched [in probsa.rt.model.carry_in]
SporadicFacts.ts [in probsa.rt.model.carry_in]
SporadicFacts.tsk [in probsa.rt.model.carry_in]
StepByStepProof.Cpart [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Cpart' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Cs [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.CsEQU [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.CSpart [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.CSpart' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Cs' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.c0 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Exc [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Exc' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.horizon [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_c0_causes_exceedance [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_ωo_in_Cs [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_cond_independence [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_pWCET_bounds_cond_cdf [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_ξ_pos_prob [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_axiomatic_pWCET [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.H_rt_monotonic [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Idx [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.j [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.j_rep [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.part [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Pi [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.r [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.S [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.sample_costs' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.sample_costs [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.sched [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Sf [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Sf' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1.H_ineq_ξ_partitioned [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1.ξpart [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1.ξpart' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step10.H_ineq_without_other_costs [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step11.H_ineq_c0_causes_exceedance [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step12.H_almost_pWCET_bounds_cond_cdf [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.H_ineq_ξ_fixed [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.H_part_unpack_ξ [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξ [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξf [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξf' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξi [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξi' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξpart [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξpart' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2.ξ_equivalence [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step3.H_ineq_Ω_part [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step4.H_ineq_conditional [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step5.H_ineq_algorithmic_𝓡 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step6.H_ineq_costs_partitioned [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step7.H_ineq_cost_partitioned [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step8.H_ineq_cost_partitioned [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step9.H_ineq_introduce_independence [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.S' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.tsk [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Ω [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ζ [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μ [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μr [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μr' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.μ_tsk [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ξ [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ξf [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ξf' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ρ1 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ρ2 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.ωo [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓐 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒r [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒r' [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓒_pWCET [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝓡 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝗔 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.𝗖 [in probsa.rt.analysis.axiomatic_pWCET_step]
StochasticDominationSum.F1 [in probsa.probability.stochastic_order]
StochasticDominationSum.F2 [in probsa.probability.stochastic_order]
StochasticDominationSum.H_xs2_doms_xs1 [in probsa.probability.stochastic_order]
StochasticDominationSum.H_eq_size [in probsa.probability.stochastic_order]
StochasticDominationSum.H_independent2 [in probsa.probability.stochastic_order]
StochasticDominationSum.H_independent1 [in probsa.probability.stochastic_order]
StochasticDominationSum.xs1 [in probsa.probability.stochastic_order]
StochasticDominationSum.xs2 [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_independent' [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_independent [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_dominates_Y [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.H_dominates_X [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.t [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.X [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.X' [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.Y [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers.Y' [in probsa.probability.stochastic_order]
StochasticOrderSum.F [in probsa.probability.pmf]
StochasticOrderSum.H_bound [in probsa.probability.pmf]
StochasticOrderSum.H_independent [in probsa.probability.pmf]
StochasticOrderSum.p [in probsa.probability.pmf]
StochasticOrderSum.P [in probsa.probability.pmf]
StochasticOrderSum.xs [in probsa.probability.pmf]
StochasticOrder.H_X2_bounded_by_p2 [in probsa.probability.pmf]
StochasticOrder.H_X1_bounded_by_p1 [in probsa.probability.pmf]
StochasticOrder.H_independent [in probsa.probability.pmf]
StochasticOrder.p1 [in probsa.probability.pmf]
StochasticOrder.p2 [in probsa.probability.pmf]
StochasticOrder.X1 [in probsa.probability.pmf]
StochasticOrder.X2 [in probsa.probability.pmf]
SumOfDisjointEventsExists.B [in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.H_Bi_disjoint [in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.I [in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.Ω [in probsa.probability.law_of_total_prob]
SumOfDisjointEventsExists.μ [in probsa.probability.law_of_total_prob]
SumOverPartitions.f [in probsa.util.bigop]
SumOverPartitions.H_no_partition_missing [in probsa.util.bigop]
SumOverPartitions.P [in probsa.util.bigop]
SumOverPartitions.sum_of_partition [in probsa.util.bigop]
SumOverPartitions.X [in probsa.util.bigop]
SumOverPartitions.xs [in probsa.util.bigop]
SumOverPartitions.x_to_y [in probsa.util.bigop]
SumOverPartitions.Y [in probsa.util.bigop]
SumOverPartitions.ys [in probsa.util.bigop]
SustainableUniFPFP.arr_seq [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_transitive [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_reflexive [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_total [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_arrival_sequence_uniq [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_consistent_arrival_times [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.H_cost_monotone [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.job_ready2 [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.job_ready1 [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.H_service_monotone_wrt_schedules [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.H_j_not_completed_sched2 [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.H_j_sched1 [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.j [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone.t [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.sched1 [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.sched2 [in probsa.rt.analysis.scheduler_properties]

T

TaskWorkloadBounded.A [in probsa.rt.model.workload]
TaskWorkloadBounded.H_j_arrives_at_A [in probsa.rt.model.workload]
TaskWorkloadBounded.H_job_of_task [in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrives_in [in probsa.rt.model.workload]
TaskWorkloadBounded.H_constrained_deadlines [in probsa.rt.model.workload]
TaskWorkloadBounded.H_sporadic_arrivals [in probsa.rt.model.workload]
TaskWorkloadBounded.H_inter_arrival_pos [in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrivals_from_ts [in probsa.rt.model.workload]
TaskWorkloadBounded.H_tsk_in_ts [in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrival_sequence_uniq [in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrivals_cost_consistent [in probsa.rt.model.workload]
TaskWorkloadBounded.H_arrivals_consistent [in probsa.rt.model.workload]
TaskWorkloadBounded.j [in probsa.rt.model.workload]
TaskWorkloadBounded.pr_sched [in probsa.rt.model.workload]
TaskWorkloadBounded.ts [in probsa.rt.model.workload]
TaskWorkloadBounded.tsk [in probsa.rt.model.workload]
TaskWorkloadBounded.ω [in probsa.rt.model.workload]
TDFPBound.ts [in probsa.rt.analysis.pRTA.pRTA]
TDFPBound.tsk [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.h [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_of_task [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_tsk_in_ts [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_conditional_cost_bounded_by_pWCET [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_independent_arr_seq [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_independent_cond_arr_seq [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_identically_distr [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_bounded_by_pWCET [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_job_costs_independent [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_constrained_deadlines [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_task_min_inter_arrival_time_valid [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_sporadic_arrivals [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_arrivals_from_ts [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_arrivals_and_costs_consistent [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_from_ts [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_ts_uniq [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_must_be_ready_to_execute [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_must_arrive_to_execute [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_completed_jobs_dont_execute [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_jobs_come_from_arrival_sequence [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_respects_policy_at_preemption_point [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_work_conserving [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_horizon_far_enough [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_axiomatic_pWCET [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_transitive_priorities [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.H_priority_is_reflexive [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.j [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.sched [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.A [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.cond_cost_j [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_neq [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_tsko_hep [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_tsko_in_ts [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_arrivals_unique [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_arrivals_consistent [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_Δ_in_range [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_job_arrives_at [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.H_ω_in_ξ [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.i [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.interfering_workload [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.lengths [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.task_workload [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.tsko [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.V [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.workload_exceeds_time [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.Δ [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ξ [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ξpart [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ρ [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep.ω [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.ts [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.tsk [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.ζ [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.𝓡 [in probsa.rt.analysis.pRTA.pRTA]
TransformationEnsuresCondCostsBounded.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.sched [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ζ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ξ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ξpart [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCondCostsBounded.ρ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.sched [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeqPartition.H_jrep_notin_jobs [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeqPartition.jobs [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.H_jrep_notin_jobs [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.jobs [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.ξa [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.ξf [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq.ξf' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.j [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.j_rep [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.H_jrep_notin_jobs [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.jobs_rep [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.ξ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2.ξpart [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.ξ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.ξpart [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3.ρ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.ζ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.sched [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBoundedByPWCET.H_job_of_task [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBoundedByPWCET.tsk [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBounds.H_jobs_neq [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.j [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.j_rep [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.H_job_of_task [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.H_j_in_reps [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.H_jobs_uniq [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.j [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.jobs_rep [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2.tsk [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step3.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step3.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.ζ [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.sched [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.H_jrep_notin_jobs [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.j [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.jobs [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.j_rep [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.H_jobs_uniq [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.jobs_rep [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step3.S [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step3.S' [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.ζ [in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.j_rep [in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.S [in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.sched [in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.S' [in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence.ζ [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.sched [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.j [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.j_rep [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2.jobs_rep [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step3.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step3.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.ζ [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.job_deadline [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.sched [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.BIG [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.h [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.j [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.j_rep [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.h [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.H_horizon_big [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.j [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.jobs [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.h [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.H_horizon_big [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.ζ [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.sched [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.j [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.j_rep [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1.ts [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.jobs [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2.ts [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3.S [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3.S' [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3.ts [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.ζ [in probsa.rt.analysis.transformation_properties]

U

UniScheduleAsSchedulerAC.arr_seq [in probsa.rt.analysis.scheduler_properties]
UniScheduleAsSchedulerAC.JLDP [in probsa.rt.analysis.scheduler_properties]
UniScheduleAsSchedulerAC.job_deadline [in probsa.rt.analysis.scheduler_properties]
UniScheduleAsSchedulerAC.readiness [in probsa.rt.analysis.scheduler_properties]

V

ValidpWCETRemainsValid.horizon [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.H_rt_monotonic [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalBoundedness.H_job_cost_cond_bounded_by_pWCET [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.H_job_cost_cond_independent [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.𝓒_fix' [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.𝓒_fix [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence.𝗖 [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.j [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.j_rep [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.P [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.P' [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.S [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.S' [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.Ω [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.μ [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ξ [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ξf [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ξf' [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.𝓐 [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.𝓒 [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.sched [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ζ [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.𝓡 [in probsa.rt.analysis.valid_pWCET_remains_valid]

W

WCATDFPtoTDFP.h [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_WCA_TDFP_bounded [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_Λ_bounded [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_job_of_task [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.H_tsk_in_ts [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.j [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.sched [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.ts [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.tsk [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.Λ [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.ζ [in probsa.rt.analysis.pRTA.pRTA]
WCATDFPtoTDFP.𝓡 [in probsa.rt.analysis.pRTA.pRTA]
WCETisAxiomaticPWCET.H_task_cost_is_valid_WCET [in probsa.rt.analysis.WCET_is_pWCET]
WorkloadLemmasDetCostStocArr.tsk [in probsa.rt.model.workload]

---

Library Index

A

abort_readiness
arrivals
arrival_sequence
arrival_bound
axiomatic_pWCET_full
axiomatic_pWCET
axiomatic_pWCET_step

B

basic
bigop
bigop_inf
boolp
brvar

C

carry_in
cdf
completion
completion_time
conditional
cost_and_workload

D

dominance_relation

E

etime
events

I

independence
indicator
iota

J

job

L

law_of_total_prob

M

min
min_inter_arrival
misc

N

notation
nrvar
nth_cost

P

partition
partition_transfer
pETs_to_pWCETs
pmf
pRBF
pred
prio_aware
prob
pRTA
pRTA_full
pr_respects_policy
pr_cost
pr_work_conserving
pr_must_be_ready

R

response_time
rt_monotonic
r_mult

S

schedule
scheduler
scheduler_properties
seq
service
sporadic_as_curve
stdpp
stochastic_order

T

task
task_workload
transformation_properties
tr_eq

V

valid_pWCET_remains_valid

W

WCET
WCET_is_pWCET
workload
work_bound

Z

zip

---

Lemma Index

A

abortion_readiness_is_nonclairvoyant [in probsa.rt.analysis.scheduler_properties]
addrv_addmpf_respect_ltn [in probsa.probability.pmf]
addrv_addmpf_respect_stochastic_order [in probsa.probability.pmf]
addrv_respects_stochastic_order [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_7 [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_6 [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_5 [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_5a [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_4 [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_3 [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_3a [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_2 [in probsa.probability.stochastic_order]
addrv_respects_stochastic_order_step_1 [in probsa.probability.stochastic_order]
addrv_leq_decomposition [in probsa.probability.stochastic_order]
addrv_eq_decomposition [in probsa.probability.stochastic_order]
addrv_comm [in probsa.probability.stochastic_order]
allpairs_rvar [in probsa.probability.prob]
andA [in probsa.util.boolp]
andC [in probsa.util.boolp]
and_asboolP [in probsa.util.boolp]
and3_asboolP [in probsa.util.boolp]
apt_double_summable_by_column [in probsa.probability.law_of_total_prob]
apt_row_rewrite [in probsa.probability.law_of_total_prob]
arrivals_consistent_with_deadlines [in probsa.rt.model.assumptions.basic]
arrivals_between_sorted [in probsa.util.prosa.arrival_bound]
arrivals_at_sorted [in probsa.util.prosa.arrival_bound]
arrival_of_nth_job [in probsa.util.prosa.arrival_bound]
arr_seq_consistent [in probsa.rt.behavior.arrival_sequence]
arr_seq_uniq [in probsa.rt.behavior.arrival_sequence]
asboolb [in probsa.util.boolp]
asboolE [in probsa.util.boolp]
asboolF [in probsa.util.boolp]
asboolP [in probsa.util.boolp]
asboolPn [in probsa.util.boolp]
asboolT [in probsa.util.boolp]
asboolW [in probsa.util.boolp]
asbool_existsNb [in probsa.util.boolp]
asbool_forallNb [in probsa.util.boolp]
asbool_imply [in probsa.util.boolp]
asbool_and [in probsa.util.boolp]
asbool_or [in probsa.util.boolp]
asbool_neg [in probsa.util.boolp]
asbool_eq_equiv [in probsa.util.boolp]
asbool_equiv [in probsa.util.boolp]
asbool_equiv_eqP [in probsa.util.boolp]
asbool_equiv_eq [in probsa.util.boolp]
atotal_column_rewrite [in probsa.probability.law_of_total_prob]
atotal_row_rewrite [in probsa.probability.law_of_total_prob]
atotal_double_summable_by_column [in probsa.probability.law_of_total_prob]
at_most_one_job_pending [in probsa.rt.model.workload]

B

before_deadline_monotone [in probsa.rt.model.carry_in]
bigD1_seq_pred [in probsa.util.bigop]
bigop_inf_option_cdf_lt [in probsa.probability.law_of_total_prob]
bigop_inf_cdf_le [in probsa.probability.law_of_total_prob]
bigsum_add [in probsa.util.bigop]
bigsum_distr [in probsa.util.bigop]
bigsum_upper_bound_to_indicator [in probsa.util.indicator]

C

canon [in probsa.util.boolp]
carry_in_workload_eq_service_of_jobs [in probsa.rt.analysis.completion_time]
cdf_cond_marginal21 [in probsa.probability.conditional]
cdf_cond_marginal11 [in probsa.probability.conditional]
cdf_cond_eq_cond [in probsa.probability.conditional]
cdf_cond_xpredT [in probsa.probability.conditional]
cdf_to_sum_of_indicators [in probsa.probability.cdf]
cdf_to_sum_of_preq [in probsa.probability.cdf]
cdf_succ_to_cdf_preq [in probsa.probability.cdf]
cdf_nondecreasing [in probsa.probability.cdf]
cdf_nonnegative [in probsa.probability.cdf]
choice [in probsa.util.boolp]
choose_superior_default_or_in_seq [in probsa.util.seq]
cid2 [in probsa.util.boolp]
classic [in probsa.util.boolp]
completed_by_is_dec [in probsa.rt.behavior.response_time]
completion_time_exists [in probsa.rt.analysis.completion_time]
completion_monotone_prob [in probsa.rt.analysis.completion]
completion_monotone [in probsa.rt.analysis.completion]
cond_cdf_posprob_irrelevance [in probsa.probability.conditional]
cond_prob_posprob_irrelevance [in probsa.probability.conditional]
cons_elim [in probsa.rt.behavior.arrival_sequence]
contraNP [in probsa.util.boolp]
contraPP [in probsa.util.boolp]
contraPT [in probsa.util.boolp]
contrapT [in probsa.util.boolp]
contraTP [in probsa.util.boolp]
contra_eqP [in probsa.util.boolp]
contra_neqP [in probsa.util.boolp]
contra_notT [in probsa.util.boolp]
contra_notP [in probsa.util.boolp]
cost_causing_exceedance_of_r [in probsa.rt.analysis.axiomatic_pWCET_step]

D

deadline_miss_implies_workload_exceeds_time [in probsa.rt.analysis.pRTA.pRTA]
distribution_of_prod_restrict [in probsa.probability.conditional]
div_ceil_multiple [in probsa.util.prosa.arrival_bound]

E

EM [in probsa.util.boolp]
eqn_etime [in probsa.util.etime]
eqPchoice [in probsa.util.boolp]
eq_tr3 [in probsa.util.tr_eq]
eq_tr4 [in probsa.util.tr_eq]
eq_opE [in probsa.util.boolp]
eq_exist [in probsa.util.boolp]
eq_exists3 [in probsa.util.boolp]
eq_exists2 [in probsa.util.boolp]
eq_exists [in probsa.util.boolp]
eq_forall3 [in probsa.util.boolp]
eq_forall2 [in probsa.util.boolp]
eq_forall [in probsa.util.boolp]
eq_fun3 [in probsa.util.boolp]
eq_fun2 [in probsa.util.boolp]
eq_fun [in probsa.util.boolp]
eq_arr_seq_impl_eq_job_arrival [in probsa.rt.behavior.arrival_sequence]
etime_dom_trans [in probsa.probability.dominance_relation]
etime_dom_refl [in probsa.probability.dominance_relation]
existsNE [in probsa.util.boolp]
existsNP [in probsa.util.boolp]
existsPNP [in probsa.util.boolp]
existsp_asboolPn [in probsa.util.boolp]
exists_asboolP [in probsa.util.boolp]
exists_swap [in probsa.util.boolp]
exists2P [in probsa.util.boolp]
extentionality [in probsa.util.boolp]
ex_total_column_abs [in probsa.probability.law_of_total_prob]
ex_series_pr_eq_over_partition [in probsa.probability.law_of_total_prob]
ex_series_pr_eq_over_disjoint [in probsa.probability.law_of_total_prob]

F

falseE [in probsa.util.boolp]
filter_cons_eq [in probsa.rt.behavior.arrival_sequence]
filter_eq_cons_sat [in probsa.rt.behavior.arrival_sequence]
foldr_choose_superior_in_seq [in probsa.util.seq]
foldr_choose_superior_not_none [in probsa.util.seq]
foldr_big [in probsa.util.bigop]
fold_prob_to_cond_cdf [in probsa.probability.conditional]
fold_prob_to_cond_prob [in probsa.probability.conditional]
forallNE [in probsa.util.boolp]
forallNP [in probsa.util.boolp]
forallPNP [in probsa.util.boolp]
forallp_asboolPn [in probsa.util.boolp]
forall_asboolP [in probsa.util.boolp]
forall_swap [in probsa.util.boolp]
forall2NP [in probsa.util.boolp]
FP_FP_sched_is_rt_monotonic [in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_jobs_must_be_ready_to_execute [in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_policy_at_preemption_point [in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_is_work_conserving [in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_jobs_come_from_arrival_sequence [in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_jobs_must_arrive_to_execute [in probsa.rt.analysis.scheduler_properties]
FP_FP_sched_respects_completed_jobs_dont_execute [in probsa.rt.analysis.scheduler_properties]
frechet_bound_on_all_intervals [in probsa.rt.analysis.pRTA.pRTA]
frechet_min [in probsa.probability.prob]
func_dom_trans [in probsa.probability.dominance_relation]
func_dom_refl [in probsa.probability.dominance_relation]
funeqE [in probsa.util.boolp]
funeqP [in probsa.util.boolp]
funeq2E [in probsa.util.boolp]
funeq2P [in probsa.util.boolp]
funeq3E [in probsa.util.boolp]
funeq3P [in probsa.util.boolp]
funext [in probsa.util.boolp]
FunOrder.fun_display [in probsa.util.boolp]
FunOrder.joinfA [in probsa.util.boolp]
FunOrder.joinfC [in probsa.util.boolp]
FunOrder.joinfKI [in probsa.util.boolp]
FunOrder.lef_meet [in probsa.util.boolp]
FunOrder.lef_trans [in probsa.util.boolp]
FunOrder.lef_anti [in probsa.util.boolp]
FunOrder.lef_refl [in probsa.util.boolp]
FunOrder.ltf_def [in probsa.util.boolp]
FunOrder.meetfA [in probsa.util.boolp]
FunOrder.meetfC [in probsa.util.boolp]
FunOrder.meetfKU [in probsa.util.boolp]

G

gen_eqP [in probsa.util.boolp]
gen_choiceMixin [in probsa.util.boolp]
get_cover_index_valid [in probsa.probability.law_of_total_prob]

I

iff_not2 [in probsa.util.boolp]
iff_notr [in probsa.util.boolp]
imply_asboolPn [in probsa.util.boolp]
imply_asboolP [in probsa.util.boolp]
independent_flatten [in probsa.probability.independence]
indep_extend_consts [in probsa.probability.independence]
indep_consts [in probsa.probability.independence]
indep_pair_const_r [in probsa.probability.independence]
indep_pair_swap [in probsa.probability.independence]
indep_irr [in probsa.probability.independence]
indep_comp [in probsa.probability.independence]
indep_subset [in probsa.probability.independence]
indep_filter [in probsa.probability.independence]
indep_perm_eq [in probsa.probability.independence]
indep_cat_indep2_list_comp [in probsa.probability.independence]
indep_cat_indep2_list [in probsa.probability.independence]
indep_cat_split [in probsa.probability.independence]
indep_catC [in probsa.probability.independence]
indep2_sum_cons [in probsa.probability.independence]
indep2_sum [in probsa.probability.independence]
indep2_fn_extl [in probsa.probability.independence]
indep2_fn_ext [in probsa.probability.independence]
index_iota_recr [in probsa.util.iota]
indicator_pred_impl [in probsa.util.indicator]
indicator_pred_eq [in probsa.util.indicator]
indicator_andb_mult [in probsa.util.indicator]
interference_bounded_by_task_workload_sum [in probsa.rt.analysis.pRTA.pRTA]
involutive [in probsa.util.stdpp]
is_seriesC_bump [in probsa.util.bigop_inf]
is_true_inj [in probsa.util.boolp]
iterfS [in probsa.util.boolp]
iterfSr [in probsa.util.boolp]
iter0 [in probsa.util.boolp]

J

jobs_rt_always_exceeds_r [in probsa.rt.analysis.axiomatic_pWCET_step]
jobs_rt_never_exceeds_r [in probsa.rt.analysis.axiomatic_pWCET_step]
job_cost_sum_condition_arrival_seq [in probsa.rt.analysis.work_bound]
job_cost_cond_independent_respected [in probsa.rt.analysis.valid_pWCET_remains_valid]
job_cost_cond_bounded_by_pWCET_respected [in probsa.rt.analysis.valid_pWCET_remains_valid]
job_cost_and_ohep_workload_independent [in probsa.rt.analysis.independent.cost_and_workload]
job_cost_and_ohep_workload_indep2 [in probsa.rt.analysis.independent.cost_and_workload]
job_either_arrives_or_not [in probsa.rt.analysis.pRTA.pRTA]
job_arrival_between_lt [in probsa.util.prosa.arrival_bound]
job_arrival_between_ge [in probsa.util.prosa.arrival_bound]
job_arrival_at [in probsa.util.prosa.arrival_bound]
joinfE [in probsa.util.boolp]
j_completed [in probsa.rt.analysis.completion_time]
j_scheduled_at_t_in_sched2 [in probsa.rt.analysis.scheduler_properties]

L

law_of_total_probability_simple [in probsa.probability.prob]
law_of_total_probability_prod [in probsa.probability.law_of_total_prob]
law_of_total_probability [in probsa.probability.law_of_total_prob]
lefP [in probsa.util.boolp]
leibniz_equiv_iff [in probsa.util.stdpp]
lem [in probsa.util.boolp]
leq_SeriesC [in probsa.util.bigop_inf]
LHS_factorization [in probsa.rt.analysis.axiomatic_pWCET_step]
lims_Λ [in probsa.rt.analysis.pRTA.pRTA]
lower_bound_on_service_of_jobs [in probsa.rt.analysis.completion_time]

M

meetfE [in probsa.util.boolp]
minimum_distance_for_n_sporadic_arrivals [in probsa.util.prosa.arrival_bound]
min1_cons [in probsa.util.min]

N

nonempty_sample_space [in probsa.probability.prob]
nonreplaced_pETs_dont_change_2_step [in probsa.rt.analysis.transformation_properties]
nonreplaced_pETs_dont_change_1_step [in probsa.rt.analysis.transformation_properties]
notFE [in probsa.util.boolp]
notK [in probsa.util.boolp]
notLR [in probsa.util.boolp]
notRL [in probsa.util.boolp]
notT [in probsa.util.boolp]
notTE [in probsa.util.boolp]
not_exists2P [in probsa.util.boolp]
not_forallP [in probsa.util.boolp]
not_existsP [in probsa.util.boolp]
not_implyE [in probsa.util.boolp]
not_orP [in probsa.util.boolp]
not_and3P [in probsa.util.boolp]
not_andP [in probsa.util.boolp]
not_implyP [in probsa.util.boolp]
not_inj [in probsa.util.boolp]
not_False [in probsa.util.boolp]
not_True [in probsa.util.boolp]
not_symmetry [in probsa.util.stdpp]
no_carry_in_at_task_arrival [in probsa.rt.model.carry_in]
nrvar_dom_trans [in probsa.probability.dominance_relation]
nrvar_dom_refl [in probsa.probability.dominance_relation]
nth_cost_sum_monotone [in probsa.rt.analysis.work_bound]
nth_mem_o [in probsa.util.misc]
nth_seq_eq [in probsa.util.misc]
nth_job_cost_bounded_by_pWCET [in probsa.rt.analysis.pRTA.pRTA]
nth_cost_sum_rewrite [in probsa.rt.analysis.pRTA.pRTA]

O

orA [in probsa.util.boolp]
orC [in probsa.util.boolp]
or_asboolP [in probsa.util.boolp]
or3_asboolP [in probsa.util.boolp]

P

partition_into_singletons_partition_dominated [in probsa.rt.analysis.WCET_is_pWCET]
partition_into_singletons_partition_intependent [in probsa.rt.analysis.WCET_is_pWCET]
Pchoice [in probsa.util.boolp]
pdegen [in probsa.util.boolp]
Peq [in probsa.util.boolp]
perm_eq_allpairs_flatten [in probsa.util.misc]
perm_eq_zippable [in probsa.util.zip]
perm_zip1 [in probsa.util.zip]
pETs_have_same_distribution [in probsa.rt.analysis.transformation_properties]
pmf_restricted_pred [in probsa.probability.conditional]
pmf_sums_to_1 [in probsa.probability.conditional]
pmf_nonnegative [in probsa.probability.conditional]
pointwise_leq_zip_impl_in_leq [in probsa.util.zip]
pointwise_min1_zip [in probsa.util.zip]
predeqE [in probsa.util.boolp]
predeqP [in probsa.util.boolp]
predeq2E [in probsa.util.boolp]
predeq2P [in probsa.util.boolp]
predeq3E [in probsa.util.boolp]
predeq3P [in probsa.util.boolp]
pred_cap_and [in probsa.probability.pred]
pred_cap_assoc [in probsa.probability.pred]
pred0pP [in probsa.util.boolp]
probabilistic_rta_fp [in probsa.rt.analysis.pRTA.pRTA]
probabilistic_rt_monotonicity_of_iid_pWCET' [in probsa.rt.analysis.axiomatic_pWCET_full]
probabilistic_rt_monotonicity_of_iid_pWCET [in probsa.rt.analysis.axiomatic_pWCET_full]
probabilistic_rta_fp_fp [in probsa.rt.analysis.pRTA.pRTA_full]
prob_rt_monotonic_axiomatic_pWCET_replace_all_pETs [in probsa.rt.analysis.valid_pWCET_remains_valid]
prob_rt_monotonic_axiomatic_pWCET_replace_pET [in probsa.rt.analysis.axiomatic_pWCET_step]
propeqE [in probsa.util.boolp]
propeqP [in probsa.util.boolp]
propext [in probsa.util.boolp]
propF [in probsa.util.boolp]
propT [in probsa.util.boolp]
Prop_irrelevance [in probsa.util.boolp]
pr_arrivals_task_between_respect_arrival_curve_mid [in probsa.rt.analysis.arrivals]
pr_arrivals_task_between_respect_arrival_curve [in probsa.rt.analysis.arrivals]
pr_arrivals_between_fixed_in_partition [in probsa.rt.analysis.arrivals]
pr_arrivals_task_between_eq [in probsa.rt.analysis.arrivals]
pr_arrivals_between_eq [in probsa.rt.analysis.arrivals]
pr_service_of_jobs_cat [in probsa.rt.analysis.completion_time]
pr_hep_workload_pr_task_workload_split [in probsa.rt.model.workload]
pr_workload_of_task_cat [in probsa.rt.model.workload]
pr_workload_bounded_by_nth_cost_sum [in probsa.rt.analysis.work_bound]
pr_cond_joint_pred_eq_cond_eq [in probsa.probability.conditional]
pr_joint_pred_eq [in probsa.probability.conditional]
pr_cond_mono_pred [in probsa.probability.conditional]
pr_cond_eq_pred_0 [in probsa.probability.conditional]
pr_cond_eq_cond [in probsa.probability.conditional]
pr_cond_eq_pred [in probsa.probability.conditional]
pr_cond_xpred1 [in probsa.probability.conditional]
pr_cond_xpredT [in probsa.probability.conditional]
pr_cond_axiomatic' [in probsa.probability.conditional]
pr_cond_axiomatic [in probsa.probability.conditional]
pr_task_workload_independence [in probsa.rt.analysis.independent.task_workload]
pr_ineq_compl [in probsa.probability.prob]
pr_pred_compl [in probsa.probability.prob]
pr_eq_pred_pos [in probsa.probability.prob]
pr_mono_pred_pos [in probsa.probability.prob]
pr_eq_measure [in probsa.probability.prob]
pr_bool_move [in probsa.probability.prob]
pr_of_union [in probsa.probability.prob]
pr_leq_intersectionr [in probsa.probability.prob]
pr_leq_intersectionl [in probsa.probability.prob]
pr_pos_or_zero [in probsa.probability.prob]
pr_pos_inv [in probsa.probability.prob]
pr_xpredT_ext [in probsa.probability.prob]
pr_zero [in probsa.probability.prob]
pr_pos [in probsa.probability.prob]
pr_service_bounded_by_pr_job_cost [in probsa.rt.model.assumptions.basic]
pr_eq_over_partition_is_series [in probsa.probability.law_of_total_prob]
pr_carry_in_workload_bounded_pr_pend_workload [in probsa.rt.model.carry_in]
pr_hep_carry_in_workload_split [in probsa.rt.model.carry_in]
pr_cond_indep2 [in probsa.probability.independence]
pr_consistent_arrival_times [in probsa.rt.behavior.arrival_sequence]
pselect [in probsa.util.boolp]
pselectT [in probsa.util.boolp]
pWCETs_bounded_by_replaced_pETs [in probsa.rt.analysis.transformation_properties]
pWCETs_bounded_by_replaced_pETs_steps [in probsa.rt.analysis.transformation_properties]
pWCETs_bounded_by_replaced_pETs_step [in probsa.rt.analysis.transformation_properties]

R

reflect_eq [in probsa.util.boolp]
replaced_cond_pETs_bounded_by_pWCETs [in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_cond_independent [in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_from_arr_seq_partition [in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_from_arr_seq_partition_steps [in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent [in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_steps [in probsa.rt.analysis.transformation_properties]
replaced_pETs_are_independent_step [in probsa.rt.analysis.transformation_properties]
replaced_pETs_bounded_by_pWCETs [in probsa.rt.analysis.transformation_properties]
replaced_pETs_bounded_by_pWCETs_steps [in probsa.rt.analysis.transformation_properties]
replaced_pETs_bounded_by_pWCETs_step [in probsa.rt.analysis.transformation_properties]
respects_arrival_curve [in probsa.rt.analysis.pRTA.pRTA]
RHS_factorization [in probsa.rt.analysis.axiomatic_pWCET_step]
Rle_min_compat [in probsa.util.min]
Rmult_commutative [in probsa.util.r_mult]
Rmult_right_id [in probsa.util.r_mult]
Rmult_left_id [in probsa.util.r_mult]
Rmult_associative [in probsa.util.r_mult]
Rmult_eq_compat [in probsa.util.r_mult]

S

scheduled_if_before_deadline [in probsa.rt.analysis.completion_time]
scheduled_at_implies_arrived_between'' [in probsa.rt.model.assumptions.basic]
scheduled_at_implies_arrived_between' [in probsa.rt.model.assumptions.basic]
scheduled_at_implies_arrived_between [in probsa.rt.model.assumptions.basic]
scheduled_at_implies_exists_arrival_time [in probsa.rt.model.assumptions.basic]
scheduled_job_is_supremum_new [in probsa.util.prosa.prio_aware]
seq_split [in probsa.util.seq]
seq_split_take_drop [in probsa.util.seq]
seq_filter_singleton [in probsa.util.misc]
SeriesCf_bump [in probsa.util.bigop_inf]
SeriesC_pos [in probsa.util.bigop_inf]
SeriesC_scal_l [in probsa.util.bigop_inf]
service_monotone_wrt_sched [in probsa.rt.analysis.scheduler_properties]
some_job_scheduled [in probsa.rt.analysis.completion_time]
sporadic_task_sets_respects_max_arrivals [in probsa.util.prosa.sporadic_as_curve]
sporadic_arrival_curve_respects_max_arrivals [in probsa.util.prosa.sporadic_as_curve]
sporadic_task_sets_arrival_curve_valid [in probsa.util.prosa.sporadic_as_curve]
sporadic_arrival_curve_valid [in probsa.util.prosa.sporadic_as_curve]
sporadic_task_model_respected [in probsa.rt.analysis.transformation_properties]
sporadic_task_model_respected_steps [in probsa.rt.analysis.transformation_properties]
sporadic_task_model_respected_step [in probsa.rt.analysis.transformation_properties]
sporadic_task_arrivals_bound [in probsa.util.prosa.arrival_bound]
subseq_filter [in probsa.util.seq]
summand_wise_bound_implies_eq [in probsa.rt.analysis.completion_time]
sumrv_sumpmf_respect_stochastic_order [in probsa.probability.pmf]
sumrv_respects_stochastic_order [in probsa.probability.stochastic_order]
sum_nrvar_sum_nat [in probsa.probability.nrvar]
sum_over_partitions_le [in probsa.util.bigop]
supremum_monotone_wrt_subset [in probsa.util.seq]
sustainable_uni_fp_fp [in probsa.rt.analysis.scheduler_properties]
swithing_point_of_monotone_function [in probsa.util.misc]
symmetry_iff [in probsa.util.stdpp]

T

task_job_cost_independence_ac [in probsa.rt.analysis.nth_cost]
task_job_cost_independence [in probsa.rt.analysis.nth_cost]
task_job_cost_independence_aux [in probsa.rt.analysis.nth_cost]
task_workload_bounded_by_nth_cost_sum [in probsa.rt.analysis.pRTA.pRTA]
task_arrivals_between_subset [in probsa.util.prosa.arrival_bound]
task_arrivals_between_uniq [in probsa.util.prosa.arrival_bound]
task_arrivals_between_sorted [in probsa.util.prosa.arrival_bound]
tdfp_zero_when_job_does_not_arrive [in probsa.rt.analysis.pRTA.pRTA]
transformation_respects_pET_indep_arr_seq_remove_part_step [in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_eq_part_step [in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_remove_step [in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_eq_step [in probsa.rt.analysis.transformation_properties]
transformation_respects_pET_indep_arr_seq_cons_step [in probsa.rt.analysis.transformation_properties]
transformation_respects_independence_step [in probsa.rt.analysis.transformation_properties]
transformation_preserves_arr_seq [in probsa.rt.analysis.transformation_properties]
transformation_respects_consistent_arrivals [in probsa.rt.analysis.transformation_properties]
transformation_respects_consistent_arrivals_steps [in probsa.rt.analysis.transformation_properties]
transformation_respects_consistent_arrivals_step [in probsa.rt.analysis.transformation_properties]
transformation_respects_big_horizon [in probsa.rt.analysis.transformation_properties]
transformation_respects_big_horizon_steps [in probsa.rt.analysis.transformation_properties]
transformation_respects_big_horizon_step [in probsa.rt.analysis.transformation_properties]
transformation_is_pRT_monotone_step13 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step12 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step11 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step10 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step9 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step8 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step7 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step6 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step5 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step4 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step3 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step2 [in probsa.rt.analysis.axiomatic_pWCET_step]
transformation_is_pRT_monotone_step1 [in probsa.rt.analysis.axiomatic_pWCET_step]
trueE [in probsa.util.boolp]

U

union_disj_eq_sum_prob [in probsa.probability.prob]
unzip1_map_nth_zip [in probsa.util.zip]

V

valid_axiomatic_pWCET_remains_valid [in probsa.rt.analysis.valid_pWCET_remains_valid]
valid_arrival_curve [in probsa.rt.analysis.pRTA.pRTA]
valid_𝓡 [in probsa.rt.model.scheduler]

W

WCA_TDFP_bounded_implies_TDFP_bounded [in probsa.rt.analysis.pRTA.pRTA]
WCET_is_axiomatic_pWCET [in probsa.rt.analysis.WCET_is_pWCET]
wlog_neg [in probsa.util.boolp]
workload_le_service [in probsa.rt.analysis.completion_time]
workload_of_jobs_widen [in probsa.rt.model.workload]
workload_of_jobs_xpredT [in probsa.rt.model.workload]
workload_bounded_by_cost_plus_interference [in probsa.rt.analysis.pRTA.pRTA]

Z

zip_map_pr_eq [in probsa.util.zip]
zip_map_rvar_eq [in probsa.util.zip]
zip_foldr_andb_seq_eq [in probsa.util.zip]
zip_map [in probsa.util.zip]

other

ξf_and_Sf_eq_prob [in probsa.rt.analysis.axiomatic_pWCET_step]
ξi_eq_ξ' [in probsa.rt.analysis.axiomatic_pWCET_step]
σpt_cov [in probsa.probability.law_of_total_prob]
σpt_inj [in probsa.probability.law_of_total_prob]

---

Constructor Index

A

add_op [in probsa.util.notation]
anti_symm [in probsa.util.stdpp]
assoc [in probsa.util.stdpp]

C

cancel [in probsa.util.stdpp]
comm [in probsa.util.stdpp]

D

dominates [in probsa.probability.dominance_relation]

E

empty [in probsa.util.stdpp]
equiv [in probsa.util.stdpp]
eq_op [in probsa.util.notation]

F

Fin [in probsa.util.etime]

I

idemp [in probsa.util.stdpp]
Infty [in probsa.util.etime]
inj [in probsa.util.stdpp]
inj2 [in probsa.util.stdpp]
intersection [in probsa.util.stdpp]

J

job_deadline [in probsa.rt.behavior.job]
job_arrival [in probsa.rt.behavior.job]
job_cost [in probsa.rt.behavior.job]

L

left_absorb [in probsa.util.stdpp]
left_id [in probsa.util.stdpp]
leibniz_equiv [in probsa.util.stdpp]
leq_op [in probsa.util.notation]
lt_op [in probsa.util.notation]

N

neg_op [in probsa.util.notation]

P

pos_prob [in probsa.probability.conditional]

R

right_absorb [in probsa.util.stdpp]
right_id [in probsa.util.stdpp]

S

sub_op [in probsa.util.notation]
surj [in probsa.util.stdpp]

T

trichotomy [in probsa.util.stdpp]
trichotomyT [in probsa.util.stdpp]

U

Undef [in probsa.util.etime]
union [in probsa.util.stdpp]

---

Axiom Index

C

constructive_indefinite_description [in probsa.util.boolp]

F

functional_extensionality_dep [in probsa.util.boolp]

P

propositional_extensionality [in probsa.util.boolp]

---

Projection Index

A

add_op [in probsa.util.notation]
anti_symm [in probsa.util.stdpp]
assoc [in probsa.util.stdpp]

C

cancel [in probsa.util.stdpp]
comm [in probsa.util.stdpp]
COV [in probsa.probability.partition]

D

DIS [in probsa.probability.partition]
dominates [in probsa.probability.dominance_relation]

E

empty [in probsa.util.stdpp]
equiv [in probsa.util.stdpp]
eq_op [in probsa.util.notation]

I

I [in probsa.probability.partition]
idemp [in probsa.util.stdpp]
inj [in probsa.util.stdpp]
inj2 [in probsa.util.stdpp]
intersection [in probsa.util.stdpp]

J

job_deadline [in probsa.rt.behavior.job]
job_arrival [in probsa.rt.behavior.job]
job_cost [in probsa.rt.behavior.job]

L

left_absorb [in probsa.util.stdpp]
left_id [in probsa.util.stdpp]
leibniz_equiv [in probsa.util.stdpp]
leq_op [in probsa.util.notation]
lt_op [in probsa.util.notation]

N

neg_op [in probsa.util.notation]

P

p [in probsa.probability.partition]
pos_prob [in probsa.probability.conditional]
pWCET_sum1 [in probsa.rt.model.task]
pWCET_nonnegative [in probsa.rt.model.task]
pWCET_pmf [in probsa.rt.model.task]

R

right_absorb [in probsa.util.stdpp]
right_id [in probsa.util.stdpp]

S

sub_op [in probsa.util.notation]
surj [in probsa.util.stdpp]

T

trichotomy [in probsa.util.stdpp]
trichotomyT [in probsa.util.stdpp]

U

union [in probsa.util.stdpp]

other

Ω_of [in probsa.rt.analysis.pETs_to_pWCETs]
μ_of [in probsa.rt.analysis.pETs_to_pWCETs]
𝓐_of [in probsa.rt.analysis.pETs_to_pWCETs]
𝓒_of [in probsa.rt.analysis.pETs_to_pWCETs]

---

Inductive Index

A

AddOp [in probsa.util.notation]
AntiSymm [in probsa.util.stdpp]
Assoc [in probsa.util.stdpp]

C

Cancel [in probsa.util.stdpp]
Comm [in probsa.util.stdpp]

D

DominanceRelation [in probsa.probability.dominance_relation]

E

Empty [in probsa.util.stdpp]
EqOp [in probsa.util.notation]
Equiv [in probsa.util.stdpp]
etime [in probsa.util.etime]

I

IdemP [in probsa.util.stdpp]
Inj [in probsa.util.stdpp]
Inj2 [in probsa.util.stdpp]
Intersection [in probsa.util.stdpp]

J

JobArrivalRV [in probsa.rt.behavior.job]
JobCostRV [in probsa.rt.behavior.job]
JobDeadlineRV [in probsa.rt.behavior.job]

L

LeftAbsorb [in probsa.util.stdpp]
LeftId [in probsa.util.stdpp]
LeibnizEquiv [in probsa.util.stdpp]
LeqOp [in probsa.util.notation]
LtOp [in probsa.util.notation]

N

NegOp [in probsa.util.notation]

P

PosProb [in probsa.probability.conditional]

R

RightAbsorb [in probsa.util.stdpp]
RightId [in probsa.util.stdpp]

S

SubOp [in probsa.util.notation]
Surj [in probsa.util.stdpp]

T

Trichotomy [in probsa.util.stdpp]
TrichotomyT [in probsa.util.stdpp]

U

Union [in probsa.util.stdpp]

---

Section Index

A

ArrivalsConsistentWithDeadlines [in probsa.rt.model.assumptions.basic]
ArrivalsPartition [in probsa.rt.model.events]
ArrSeqAndJobArrivalAgree [in probsa.rt.behavior.arrival_sequence]
ArrSeqForFinTypeJobs [in probsa.rt.behavior.arrival_sequence]
ArrSeqUniq [in probsa.rt.behavior.arrival_sequence]
AxiomaticConditionalProbability [in probsa.probability.conditional]
AxiomaticPWCET [in probsa.rt.model.axiomatic_pWCET]

B

BasicLemmas [in probsa.probability.conditional]
BasicLemmas [in probsa.probability.stochastic_order]
BasicReadinessWithJobAbortion [in probsa.rt.model.abort_readiness]
BeforeDeadline [in probsa.rt.model.carry_in]

C

CDFPWCET [in probsa.rt.model.task]
classicType [in probsa.util.boolp]
CommonAssumptions [in probsa.rt.model.assumptions.basic]
CompletionLemmas [in probsa.rt.analysis.completion]
CompletionTimeExists [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step1 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step2 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step3 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step4 [in probsa.rt.analysis.completion_time]
CompletionTimeExists.StepByStepProof.Step5 [in probsa.rt.analysis.completion_time]
ConditionalMeasure [in probsa.probability.conditional]
Consistent [in probsa.rt.behavior.arrival_sequence]
ConsistentDef [in probsa.rt.behavior.arrival_sequence]
CostPartition [in probsa.rt.model.events]

D

DerivedNotions [in probsa.rt.behavior.job]

E

eclassicType [in probsa.util.boolp]

F

FunOrder.FunLattice [in probsa.util.boolp]
FunOrder.FunOrder [in probsa.util.boolp]

I

IndependentCat [in probsa.probability.independence]
IndependentExtend [in probsa.probability.independence]
IndependentFlatten [in probsa.probability.independence]
IndependentMap [in probsa.probability.independence]
IndependentPair [in probsa.probability.independence]
IndependentSum [in probsa.probability.independence]
Indep2 [in probsa.probability.independence]
Indep2.IndepExt [in probsa.probability.independence]
Indep2.IndepExtL [in probsa.probability.independence]

J

JobCostWorkloadIndependent [in probsa.rt.analysis.independent.cost_and_workload]

L

LawOfTotalProbability [in probsa.probability.law_of_total_prob]
LawOfTotalProbabilityProd [in probsa.probability.law_of_total_prob]

M

MainLemma [in probsa.rt.analysis.axiomatic_pWCET_full]
MinimumInterArrival [in probsa.rt.model.min_inter_arrival]

N

NthCost [in probsa.rt.analysis.nth_cost]
NthCostLemmas [in probsa.rt.analysis.nth_cost]

P

PartitionExtend [in probsa.probability.partition]
PartitionIntoSingletons [in probsa.probability.partition]
PartitionProduct [in probsa.probability.partition]
PartitionTransfer [in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition [in probsa.rt.analysis.partition_transfer]
PartitionTransfer.ExtendPartition [in probsa.rt.analysis.partition_transfer]
PrArrivalLemmas [in probsa.rt.analysis.arrivals]
PrArrivalsBetween [in probsa.rt.behavior.arrival_sequence]
PrCarryInWorkload [in probsa.rt.model.carry_in]
PrCarryInWorkloadFacts [in probsa.rt.model.carry_in]
PrCostAssumptions [in probsa.rt.model.assumptions.pr_cost]
PrioAwareUniprocessorScheduler [in probsa.util.prosa.prio_aware]
PrMustBeReadyToExecture [in probsa.rt.model.assumptions.pr_must_be_ready]
ProbabilisticResponseTimeMonotonicity [in probsa.rt.model.rt_monotonic]
ProbabilisticRTA [in probsa.rt.analysis.pRTA.pRTA_full]
ProbBasicReadinessWithJobAbortion [in probsa.rt.model.abort_readiness]
ProbMassFunction [in probsa.probability.pmf]
ProbRBF [in probsa.rt.model.pRBF]
ProofOfTheorem1 [in probsa.rt.analysis.axiomatic_pWCET_step]
PrPendWorkload [in probsa.rt.model.carry_in]
PrRespectsPolicyAtPreemptionPoint [in probsa.rt.model.assumptions.pr_respects_policy]
PrResponseTime [in probsa.rt.behavior.response_time]
PrResponseTime.LPO_ResponseTime [in probsa.rt.behavior.response_time]
PrServiceBounded [in probsa.rt.model.assumptions.basic]
PrTaskWorkloadBoundedNthCost [in probsa.rt.analysis.work_bound]
PrTaskWorkloadIndependence [in probsa.rt.analysis.independent.task_workload]
PrWorkConservation [in probsa.rt.model.assumptions.pr_work_conserving]
PrWorkload [in probsa.rt.model.workload]
PrWorkloadCat [in probsa.rt.model.workload]
PrWorkloadFacts [in probsa.rt.model.workload]

R

RTMonotonicScheduler [in probsa.rt.model.scheduler]

S

SchedImpliesArrivalTime [in probsa.rt.model.assumptions.basic]
SchedImpliesArrivalTime [in probsa.rt.model.assumptions.basic]
Schedule [in probsa.rt.model.scheduler]
SchedulerHardcoded [in probsa.rt.model.scheduler]
SchedulerHardcoded.ResponseTimeFromScheduler [in probsa.rt.model.scheduler]
SchedulerProperties [in probsa.rt.analysis.scheduler_properties]
Service [in probsa.rt.behavior.service]
SporadicArrivalBound [in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.ArrivalTimes [in probsa.util.prosa.arrival_bound]
SporadicArrivalBound.NthJob [in probsa.util.prosa.arrival_bound]
SporadicArrivalCurve [in probsa.util.prosa.sporadic_as_curve]
SporadicArrivalCurve.Validity [in probsa.util.prosa.sporadic_as_curve]
SporadicFacts [in probsa.rt.model.carry_in]
StepByStepProof [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step1 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step10 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step11 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step12 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step13 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step2 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step3 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step4 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step5 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step6 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step7 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step8 [in probsa.rt.analysis.axiomatic_pWCET_step]
StepByStepProof.Step9 [in probsa.rt.analysis.axiomatic_pWCET_step]
StochasticDomination [in probsa.probability.stochastic_order]
StochasticDominationSum [in probsa.probability.stochastic_order]
StochasticDomination.AddrvRespectsStochasticOrderHelpers [in probsa.probability.stochastic_order]
StochasticOrder [in probsa.probability.pmf]
StochasticOrderSum [in probsa.probability.pmf]
SumOfDisjointEventsExists [in probsa.probability.law_of_total_prob]
SumOfPartitionEventsExists [in probsa.probability.law_of_total_prob]
SumOverPartitions [in probsa.util.bigop]
SustainableUniFPFP [in probsa.rt.analysis.scheduler_properties]
SustainableUniFPFP.ScheduledAtMonotone [in probsa.rt.analysis.scheduler_properties]

T

TaskWorkloadBounded [in probsa.rt.model.workload]
TDFPBound [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded [in probsa.rt.analysis.pRTA.pRTA]
TDFPIsBounded.StepByStep [in probsa.rt.analysis.pRTA.pRTA]
Transformation [in probsa.rt.analysis.pETs_to_pWCETs]
TransformationEnsuresCondCostsBounded [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeq [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step1.IndependentArrSeqPartition [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step2 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresCostsIndependentFromArrivals.Step3 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBoundedByPWCET [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step1.CostBounds [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step2 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIdenticalCosts.Step3 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step1 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step2 [in probsa.rt.analysis.transformation_properties]
TransformationEnsuresIndependentCosts.Step3 [in probsa.rt.analysis.transformation_properties]
TransformationPreservesArrivalSequence [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step1 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step2 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsArrivalsCostConsistent.Step3 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step1 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step2 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsBigHorizon.Step3 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step1 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step2 [in probsa.rt.analysis.transformation_properties]
TransformationRespectsSporadicTaskModel.Step3 [in probsa.rt.analysis.transformation_properties]

U

UniScheduleAsSchedulerAC [in probsa.rt.analysis.scheduler_properties]

V

ValidpWCETRemainsValid [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalBoundedness [in probsa.rt.analysis.valid_pWCET_remains_valid]
ValidpWCETRemainsValid.ProofOfLemmas.ConditionalIndependence [in probsa.rt.analysis.valid_pWCET_remains_valid]

W

WCATDFPtoTDFP [in probsa.rt.analysis.pRTA.pRTA]
WCET [in probsa.rt.model.WCET]
WCETisAxiomaticPWCET [in probsa.rt.analysis.WCET_is_pWCET]
WorkloadLemmasDetCostStocArr [in probsa.rt.model.workload]

Z

Zip [in probsa.util.zip]

---

Instance Index

A

abort_ready_instance [in probsa.rt.model.abort_readiness]

D

dominance_ndistrib_nrvar [in probsa.probability.pmf]
dominance_nrvar_ndistrib [in probsa.probability.pmf]
dominance_etime_rvar [in probsa.probability.dominance_relation]
dominance_nrvar_funct [in probsa.probability.dominance_relation]
dominance_nrvar [in probsa.probability.dominance_relation]
dominance_func [in probsa.probability.dominance_relation]

E

equiv_default_relation [in probsa.util.stdpp]
equiv_rewrite_relation [in probsa.util.stdpp]

J

job_deadline_from_task_deadline [in probsa.rt.model.task]
job_cost_s [in probsa.rt.analysis.axiomatic_pWCET_full]
job_arrival_s [in probsa.rt.analysis.axiomatic_pWCET_full]

M

MaxArrivalsSporadic [in probsa.util.prosa.sporadic_as_curve]

N

nat_etimervar_pred_ltop [in probsa.probability.dominance_relation]
nat_nat_bool_eqop [in probsa.util.notation]
neg_pred [in probsa.probability.pred]
nrvar_nat_pred_eqop [in probsa.probability.nrvar]
nrvar_subop [in probsa.probability.nrvar]
nrvar_addop [in probsa.probability.nrvar]
nrvar_nrvar_brvar_leqop [in probsa.probability.nrvar]
nrvar_nrvar_pred_leqop [in probsa.probability.nrvar]

O

onat_onat_bool_ltop [in probsa.util.notation]
onat_nat_bool_leqop [in probsa.util.notation]
onat_onat_bool_leqop [in probsa.util.notation]
onrvar_onat_pred_leqop [in probsa.probability.nrvar]
onrvar_nrvar_brvar_leqop [in probsa.probability.nrvar]
onrvar_onat_pred_eqop [in probsa.probability.nrvar]

P

posprob_xpredT [in probsa.probability.conditional]
pred_intersection [in probsa.probability.pred]
pred_union [in probsa.probability.pred]

R

rvar_nat_pred_leqop [in probsa.probability.nrvar]
rvar_intersection [in probsa.probability.brvar]
rvar_union [in probsa.probability.brvar]
rvar_neg [in probsa.probability.brvar]

W

WCET_pmf [in probsa.rt.analysis.WCET_is_pWCET]

---

Abbreviation Index

C

canonical [in probsa.util.boolp]
canonical_ [in probsa.util.boolp]
cid [in probsa.util.boolp]

I

Involutive [in probsa.util.stdpp]

X

xpredpC [in probsa.util.boolp]
xpredpD [in probsa.util.boolp]
xpredpI [in probsa.util.boolp]
xpredpT [in probsa.util.boolp]
xpredpU [in probsa.util.boolp]
xpredp0 [in probsa.util.boolp]
xpreimp [in probsa.util.boolp]
xrelpU [in probsa.util.boolp]

---

Definition Index

A

apt [in probsa.probability.law_of_total_prob]
arrivals_cost_consistent [in probsa.rt.model.assumptions.basic]
arrivals_from_task_set [in probsa.rt.model.assumptions.basic]
arrow_choiceType [in probsa.util.boolp]
arrow_eqType [in probsa.util.boolp]
arr_seq_job_arrival_consistent [in probsa.rt.behavior.arrival_sequence]
arr_seq [in probsa.rt.behavior.arrival_sequence]
asbool [in probsa.util.boolp]
atotal [in probsa.probability.law_of_total_prob]
axiomatic_pWCET [in probsa.rt.model.axiomatic_pWCET]

B

before_deadline [in probsa.rt.model.carry_in]
brvar [in probsa.probability.brvar]
by_arrival_times [in probsa.util.prosa.arrival_bound]

C

canonical_of [in probsa.util.boolp]
cdf [in probsa.probability.cdf]
cdf_cond [in probsa.probability.conditional]
classicType [in probsa.util.boolp]
classicType_choiceType [in probsa.util.boolp]
classicType_eqType [in probsa.util.boolp]
completed_by𝗔𝗖 [in probsa.rt.model.scheduler]
completed𝗔𝗖_is_dec [in probsa.rt.model.scheduler]
compute_pr_schedule [in probsa.rt.model.scheduler]
conditional_cost_bounded_by_pWCET [in probsa.rt.model.assumptions.pr_cost]
constrained_deadlines [in probsa.rt.model.assumptions.basic]

D

demand_distrib [in probsa.rt.analysis.pRTA.pRTA]
dep_arrow_choiceType [in probsa.util.boolp]
dep_arrow_choiceClass [in probsa.util.boolp]
dep_arrow_eqType [in probsa.util.boolp]

E

eclassicType [in probsa.util.boolp]
eclassicType_choiceType [in probsa.util.boolp]
eclassicType_eqType [in probsa.util.boolp]
equivL [in probsa.util.stdpp]
etime_eqType [in probsa.util.etime]
etime_eqMixin [in probsa.util.etime]
etime_eqdef [in probsa.util.etime]
exceeds [in probsa.util.etime]
extend_partition' [in probsa.rt.analysis.partition_transfer]
extend_partition [in probsa.rt.analysis.partition_transfer]

F

FP_FP_sched [in probsa.rt.analysis.scheduler_properties]
FunOrder.joinf [in probsa.util.boolp]
FunOrder.latticeMixin [in probsa.util.boolp]
FunOrder.latticeType [in probsa.util.boolp]
FunOrder.lef [in probsa.util.boolp]
FunOrder.ltf [in probsa.util.boolp]
FunOrder.meetf [in probsa.util.boolp]
FunOrder.porderMixin [in probsa.util.boolp]
FunOrder.porderType [in probsa.util.boolp]

G

gen_eqMixin [in probsa.util.boolp]
gen_eq [in probsa.util.boolp]
get_cover_index [in probsa.probability.law_of_total_prob]

I

indicatorR [in probsa.util.indicator]
interference_distrib [in probsa.rt.analysis.pRTA.pRTA]
is_some [in probsa.util.bigop_inf]
is_in_cover [in probsa.probability.law_of_total_prob]

J

job_cost_partition_dominated [in probsa.rt.model.axiomatic_pWCET]
job_cost_partition_independence [in probsa.rt.model.axiomatic_pWCET]
job_costs_independent_of_arrival_sequence [in probsa.rt.model.assumptions.pr_cost]
job_costs_independent_cond_arr_seq [in probsa.rt.model.assumptions.pr_cost]
job_costs_identically_distributed [in probsa.rt.model.assumptions.pr_cost]
job_costs_bounded_by_pWCET [in probsa.rt.model.assumptions.pr_cost]
job_costs_independent [in probsa.rt.model.assumptions.pr_cost]

L

le_ndistrib_nrvar [in probsa.probability.pmf]
le_nrvar_ndistrib [in probsa.probability.pmf]
le_etime_rvar [in probsa.probability.dominance_relation]
le_nrvar_func [in probsa.probability.dominance_relation]
le_nrvar [in probsa.probability.dominance_relation]
le_func [in probsa.probability.dominance_relation]

M

max_sporadic_arrivals [in probsa.util.prosa.arrival_bound]
measure [in probsa.util.notation]
min_default [in probsa.util.min]
min_option [in probsa.util.min]
min_completion_time [in probsa.rt.model.scheduler]
min_completion_time [in probsa.rt.behavior.response_time]
min1 [in probsa.util.min]

N

nrvar [in probsa.probability.nrvar]
nrvar_addop_id [in probsa.probability.nrvar]
nth_cost [in probsa.rt.analysis.nth_cost]

O

odflt0 [in probsa.probability.nrvar]

P

partition_ext [in probsa.probability.partition]
partition_prod [in probsa.probability.partition]
partition_id [in probsa.probability.partition]
partition_into_singletons [in probsa.probability.partition]
partition_on_𝓒s [in probsa.rt.model.events]
partition_on_𝓒 [in probsa.rt.model.events]
partition_on_ξ [in probsa.rt.model.events]
pickle_bij [in probsa.util.bigop_inf]
pickle_cover_of [in probsa.probability.law_of_total_prob]
pmf_restricted [in probsa.probability.conditional]
pmf_sum [in probsa.probability.pmf]
pmf_zero [in probsa.probability.pmf]
pRBF [in probsa.rt.model.pRBF]
predp [in probsa.util.boolp]
pred0p [in probsa.util.boolp]
probabilistic_response_time_monotone_transformation [in probsa.rt.model.rt_monotonic]
proj1 [in probsa.rt.analysis.partition_transfer]
proj2 [in probsa.rt.analysis.partition_transfer]
projω [in probsa.rt.analysis.axiomatic_pWCET_step]
Prop_choiceType [in probsa.util.boolp]
Prop_eqType [in probsa.util.boolp]
pr_workload_of_hep_tasks [in probsa.rt.model.workload]
pr_workload_of_task [in probsa.rt.model.workload]
pr_workload_of_jobs [in probsa.rt.model.workload]
pr_cond [in probsa.probability.conditional]
pr_schedule [in probsa.rt.behavior.schedule]
pr_completes_at [in probsa.rt.behavior.service]
pr_completed_by [in probsa.rt.behavior.service]
pr_remaining_service [in probsa.rt.behavior.service]
pr_service [in probsa.rt.behavior.service]
pr_work_conserving [in probsa.rt.model.assumptions.pr_work_conserving]
pr_abort_ready_instance [in probsa.rt.model.abort_readiness]
pr_jobs_come_from_arrival_sequence [in probsa.rt.model.assumptions.basic]
pr_completed_jobs_dont_execute [in probsa.rt.model.assumptions.basic]
pr_jobs_must_arrive_to_execute [in probsa.rt.model.assumptions.basic]
pr_taskset_respects_sporadic_task_model [in probsa.rt.model.assumptions.basic]
pr_arrival_sequence_uniq [in probsa.rt.model.assumptions.basic]
pr_carry_in_workload_of_hep_jobs [in probsa.rt.model.carry_in]
pr_carry_in_workload_of_task [in probsa.rt.model.carry_in]
pr_carry_in_workload [in probsa.rt.model.carry_in]
pr_pend_workload_of_hep_jobs [in probsa.rt.model.carry_in]
pr_pend_workload_of_task [in probsa.rt.model.carry_in]
pr_pend_workload [in probsa.rt.model.carry_in]
pr_jobs_must_be_ready_to_execute [in probsa.rt.model.assumptions.pr_must_be_ready]
pr_respects_policy_at_preemption_point [in probsa.rt.model.assumptions.pr_respects_policy]
pr_arrivals_task_between [in probsa.rt.behavior.arrival_sequence]
pr_arrivals_between [in probsa.rt.behavior.arrival_sequence]
pr_arrival_sequence [in probsa.rt.behavior.arrival_sequence]
pWCET_to_RVpWCET [in probsa.rt.analysis.pETs_to_pWCETs]
pWCET_cdf [in probsa.rt.model.task]

R

relp [in probsa.util.boolp]
replace_all_pETs [in probsa.rt.analysis.pETs_to_pWCETs]
replace_all_jobs_pETs [in probsa.rt.analysis.pETs_to_pWCETs]
replace_job_pET [in probsa.rt.analysis.pETs_to_pWCETs]
response_time𝗔𝗖 [in probsa.rt.model.scheduler]
response_time_exceeds [in probsa.rt.behavior.response_time]
response_time [in probsa.rt.behavior.response_time]
restrict [in probsa.probability.conditional]
Rmult_comoid [in probsa.util.r_mult]
Rmult_monoid [in probsa.util.r_mult]
rt_monotonic_scheduler [in probsa.rt.model.scheduler]

S

sample_deadlines [in probsa.rt.behavior.job]
sample_costs [in probsa.rt.behavior.job]
sample_arrivals [in probsa.rt.behavior.job]
sample0_deadlines [in probsa.rt.behavior.job]
sample0_costs [in probsa.rt.behavior.job]
sample0_arrivals [in probsa.rt.behavior.job]
scheduler𝗔𝗖 [in probsa.rt.model.scheduler]
scheduler𝗔𝗖_to_rt𝗔𝗖 [in probsa.rt.model.scheduler]
scheduler𝗔𝗖_to_completed𝗔𝗖 [in probsa.rt.model.scheduler]
scheduler𝗔𝗖_to_service𝗔𝗖 [in probsa.rt.model.scheduler]
service𝗔𝗖 [in probsa.rt.model.scheduler]

T

task_job [in probsa.rt.analysis.nth_cost]
task_cost_is_WCET [in probsa.rt.model.WCET]
to_fintype [in probsa.util.misc]
to_distrib [in probsa.rt.model.pRBF]

U

union_list [in probsa.util.stdpp]
update [in probsa.rt.model.scheduler]

V

valid_min_inter_arrival [in probsa.rt.model.min_inter_arrival]

other

Λ [in probsa.rt.analysis.pRTA.pRTA]
ξ_fix [in probsa.rt.model.events]
σpt [in probsa.probability.law_of_total_prob]
𝓒_fix [in probsa.rt.model.events]

---

Record Index

A

AddOp [in probsa.util.notation]
AntiSymm [in probsa.util.stdpp]
Assoc [in probsa.util.stdpp]

C

Cancel [in probsa.util.stdpp]
Comm [in probsa.util.stdpp]

D

DominanceRelation [in probsa.probability.dominance_relation]

E

Empty [in probsa.util.stdpp]
EqOp [in probsa.util.notation]
Equiv [in probsa.util.stdpp]

I

IdemP [in probsa.util.stdpp]
Inj [in probsa.util.stdpp]
Inj2 [in probsa.util.stdpp]
Intersection [in probsa.util.stdpp]

J

JobArrivalRV [in probsa.rt.behavior.job]
JobCostRV [in probsa.rt.behavior.job]
JobDeadlineRV [in probsa.rt.behavior.job]

L

LeftAbsorb [in probsa.util.stdpp]
LeftId [in probsa.util.stdpp]
LeibnizEquiv [in probsa.util.stdpp]
LeqOp [in probsa.util.notation]
LtOp [in probsa.util.notation]

M

mclassic [in probsa.util.boolp]
mextentionality [in probsa.util.boolp]

N

NegOp [in probsa.util.notation]

P

PosProb [in probsa.probability.conditional]
ProbWCET [in probsa.rt.model.task]

R

RightAbsorb [in probsa.util.stdpp]
RightId [in probsa.util.stdpp]

S

SubOp [in probsa.util.notation]
Surj [in probsa.util.stdpp]
system [in probsa.rt.analysis.pETs_to_pWCETs]

T

Trichotomy [in probsa.util.stdpp]
TrichotomyT [in probsa.util.stdpp]

U

Union [in probsa.util.stdpp]

other

Ω_partition [in probsa.probability.partition]

---

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1709 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(64 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(617 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(67 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(449 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(33 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(41 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(31 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(159 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(35 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(161 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(35 entries)

---

This page has been generated by coqdoc