Library rt.util.nondecreasing

• Non-Decreasing Sequence and Distances
• Properties of Increasing Sequence
• Properties of Non-Decreasing Sequence
• Properties of Undup of Non-Decreasing Sequence
• Properties of Distances
• Properties of Distances of Non-Decreasing Sequence

Library rt.util.counting

Library rt.util.rel

Library rt.util.notation

Library rt.util.minmax

Library rt.util.seqset

Library rt.util.list

Library rt.util.tactics

• • Exploiting a hypothesis
• Handier movement of inequalities.

Library rt.util.bigcat

Library rt.util.step_function

Library rt.util.all

Library rt.util.div_mod

Library rt.util.search_arg

Library rt.util.epsilon

Library rt.util.ssromega

Library rt.util.sum

Library rt.util.rewrite_facilities

• Rewriting

Library rt.util.nat

Library rt.classic.implementation.arrival_sequence

Library rt.classic.implementation.global.parallel.bertogna_edf_example

Library rt.classic.implementation.global.parallel.bertogna_fp_example

Library rt.classic.implementation.global.basic.schedule

Library rt.classic.implementation.global.basic.bertogna_edf_example

Library rt.classic.implementation.global.basic.bertogna_fp_example

Library rt.classic.implementation.global.jitter.schedule

Library rt.classic.implementation.global.jitter.arrival_sequence

Library rt.classic.implementation.global.jitter.bertogna_edf_example

Library rt.classic.implementation.global.jitter.job

Library rt.classic.implementation.global.jitter.bertogna_fp_example

Library rt.classic.implementation.global.jitter.task

Library rt.classic.implementation.job

Library rt.classic.implementation.apa.schedule

Library rt.classic.implementation.apa.arrival_sequence

Library rt.classic.implementation.apa.bertogna_edf_example

Library rt.classic.implementation.apa.job

Library rt.classic.implementation.apa.bertogna_fp_example

Library rt.classic.implementation.apa.task

Library rt.classic.implementation.uni.susp.schedule

Library rt.classic.implementation.uni.susp.dynamic.oblivious.fp_rta_example

Library rt.classic.implementation.uni.susp.dynamic.arrival_sequence

Library rt.classic.implementation.uni.susp.dynamic.job

Library rt.classic.implementation.uni.susp.dynamic.task

Library rt.classic.implementation.uni.basic.schedule_tdma

Library rt.classic.implementation.uni.basic.schedule

Library rt.classic.implementation.uni.basic.tdma_rta_example

Library rt.classic.implementation.uni.basic.extraction_tdma

Library rt.classic.implementation.uni.basic.fp_rta_example

Library rt.classic.implementation.uni.jitter.schedule

Library rt.classic.implementation.uni.jitter.arrival_sequence

Library rt.classic.implementation.uni.jitter.job

Library rt.classic.implementation.uni.jitter.fp_rta_example

Library rt.classic.implementation.uni.jitter.task

Library rt.classic.implementation.task

Library rt.classic.model.priority

Library rt.classic.model.suspension

Library rt.classic.model.schedule.partitioned.schedule

Library rt.classic.model.schedule.partitioned.schedulability

Library rt.classic.model.schedule.global.schedulability

Library rt.classic.model.schedule.global.workload

Library rt.classic.model.schedule.global.transformation.construction

Library rt.classic.model.schedule.global.response_time

Library rt.classic.model.schedule.global.basic.schedule

Library rt.classic.model.schedule.global.basic.constrained_deadlines

Library rt.classic.model.schedule.global.basic.interference_edf

Library rt.classic.model.schedule.global.basic.platform

Library rt.classic.model.schedule.global.basic.interference

Library rt.classic.model.schedule.global.jitter.schedule

Library rt.classic.model.schedule.global.jitter.constrained_deadlines

Library rt.classic.model.schedule.global.jitter.interference_edf

Library rt.classic.model.schedule.global.jitter.job

Library rt.classic.model.schedule.global.jitter.platform

Library rt.classic.model.schedule.global.jitter.interference

Library rt.classic.model.schedule.apa.constrained_deadlines

Library rt.classic.model.schedule.apa.interference_edf

Library rt.classic.model.schedule.apa.affinity

Library rt.classic.model.schedule.apa.platform

Library rt.classic.model.schedule.apa.interference

Library rt.classic.model.schedule.uni.schedule

Library rt.classic.model.schedule.uni.schedulability

Library rt.classic.model.schedule.uni.susp.schedule

Library rt.classic.model.schedule.uni.susp.suspension_intervals

Library rt.classic.model.schedule.uni.susp.last_execution

Library rt.classic.model.schedule.uni.susp.platform

Library rt.classic.model.schedule.uni.susp.valid_schedule

Library rt.classic.model.schedule.uni.susp.build_suspension_table

Library rt.classic.model.schedule.uni.end_time

Library rt.classic.model.schedule.uni.nonpreemptive.schedule

Library rt.classic.model.schedule.uni.nonpreemptive.platform

Library rt.classic.model.schedule.uni.workload

Library rt.classic.model.schedule.uni.service

Library rt.classic.model.schedule.uni.limited.rbf

Library rt.classic.model.schedule.uni.limited.schedule

Library rt.classic.model.schedule.uni.limited.busy_interval

• Busy Interval for JLFP-models

Library rt.classic.model.schedule.uni.limited.platform.nonpreemptive

• Platform for fully nonpreemptive model

Library rt.classic.model.schedule.uni.limited.platform.definitions

• Platform with limited preemptions

Library rt.classic.model.schedule.uni.limited.platform.limited

• Platform for models with limited preemptions

Library rt.classic.model.schedule.uni.limited.platform.priority_inversion_is_bounded

• Priority inversion is bounded

Library rt.classic.model.schedule.uni.limited.platform.preemptive

• Platform for fully premptive model

Library rt.classic.model.schedule.uni.limited.edf.response_time_bound

• Abstract RTA for EDF-schedulers
  • Filling Out Hypothesis Of Abstract RTA Theorem
  • Final Theorem

Library rt.classic.model.schedule.uni.limited.edf.nonpr_reg.concrete_models.response_time_bound

• RTA for concrete models
• RTA for fully preemptive EDF model
• RTA for fully nonpreemptive EDF model
• RTA for EDF with fixed premption points
• RTA for EDF with floating nonpreemptive regions

Library rt.classic.model.schedule.uni.limited.edf.nonpr_reg.response_time_bound

• RTA for EDF-schedulers with bounded nonpreemprive segments
  • Priority inversion is bounded
  • Response-Time Bound

Library rt.classic.model.schedule.uni.limited.jlfp_instantiation

• JLFP instantiation of Interference and Interfering Workload
  • Interference and Interfering Workload
  • Equivalences

Library rt.classic.model.schedule.uni.limited.fixed_priority.response_time_bound

• Abstract RTA for FP-schedulers
  • Filling Out Hypotheses Of Abstract RTA Theorem
  • Final Theorem

Library rt.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.concrete_models.response_time_bound

• RTA for concrete models
• RTA for fully preemptive FP model
• RTA for fully nonpreemptive FP model
• RTA for FP-schedulers with fixed premption points
• RTA for FP-schedulers with floating nonpreemptive regions

Library rt.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound

• RTA for FP-schedulers with bounded nonpreemptive segments
  • Priority inversion is bounded
  • Response-Time Bound

Library rt.classic.model.schedule.uni.limited.abstract_RTA.definitions

• Definitions for Abstract Response-Time Analysis

Library rt.classic.model.schedule.uni.limited.abstract_RTA.abstract_rta

• Abstract Response-Time Analysis

Library rt.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space

• Reduction of the serach space for Abstract RTA

Library rt.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta

• Abstract Response-Time Analysis with sequential jobs

Library rt.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service

• Lock-in service of a job

Library rt.classic.model.schedule.uni.transformation.construction

Library rt.classic.model.schedule.uni.response_time

Library rt.classic.model.schedule.uni.basic.platform

Library rt.classic.model.schedule.uni.basic.platform_tdma

Library rt.classic.model.schedule.uni.jitter.schedule

Library rt.classic.model.schedule.uni.jitter.busy_interval

Library rt.classic.model.schedule.uni.jitter.platform

Library rt.classic.model.schedule.uni.jitter.valid_schedule

Library rt.classic.model.schedule.uni.schedule_of_task

Library rt.classic.model.schedule.uni.sustainability

Library rt.classic.model.time

Library rt.classic.model.policy_tdma

Library rt.classic.model.arrival.curves.bounds

Library rt.classic.model.arrival.basic.arrival_sequence

Library rt.classic.model.arrival.basic.arrival_bounds

Library rt.classic.model.arrival.basic.task_arrival

Library rt.classic.model.arrival.basic.job

Library rt.classic.model.arrival.basic.task

Library rt.classic.model.arrival.jitter.arrival_sequence

Library rt.classic.model.arrival.jitter.arrival_bounds

Library rt.classic.model.arrival.jitter.task_arrival

Library rt.classic.model.arrival.jitter.job

Library rt.classic.util.powerset

Library rt.classic.util.find_seq

Library rt.classic.util.bigord

Library rt.classic.util.counting

Library rt.classic.util.fixedpoint

Library rt.classic.util.notation

Library rt.classic.util.minmax

Library rt.classic.util.induction

Library rt.classic.util.seqset

Library rt.classic.util.list

Library rt.classic.util.tactics

• Very basic automation
• Equality types
• Basic simplification tactics
  • Delineating cases in proofs
• New tactics for ssreflect

Library rt.classic.util.bigcat

Library rt.classic.util.step_function

Library rt.classic.util.all

Library rt.classic.util.div_mod

Library rt.classic.util.ord_quantifier

Library rt.classic.util.pick

Library rt.classic.util.sum

Library rt.classic.util.sorting

• Sorting

Library rt.classic.util.nat

Library rt.classic.analysis.global.parallel.interference_bound

Library rt.classic.analysis.global.parallel.bertogna_fp_comp

Library rt.classic.analysis.global.parallel.bertogna_edf_comp

Library rt.classic.analysis.global.parallel.bertogna_edf_theory

Library rt.classic.analysis.global.parallel.interference_bound_edf

Library rt.classic.analysis.global.parallel.bertogna_fp_theory

Library rt.classic.analysis.global.parallel.workload_bound

Library rt.classic.analysis.global.parallel.interference_bound_fp

Library rt.classic.analysis.global.basic.interference_bound

Library rt.classic.analysis.global.basic.bertogna_fp_comp

Library rt.classic.analysis.global.basic.bertogna_edf_comp

Library rt.classic.analysis.global.basic.bertogna_edf_theory

Library rt.classic.analysis.global.basic.interference_bound_edf

Library rt.classic.analysis.global.basic.bertogna_fp_theory

Library rt.classic.analysis.global.basic.workload_bound

Library rt.classic.analysis.global.basic.interference_bound_fp

Library rt.classic.analysis.global.jitter.interference_bound

Library rt.classic.analysis.global.jitter.bertogna_fp_comp

Library rt.classic.analysis.global.jitter.bertogna_edf_comp

Library rt.classic.analysis.global.jitter.bertogna_edf_theory

Library rt.classic.analysis.global.jitter.interference_bound_edf

Library rt.classic.analysis.global.jitter.bertogna_fp_theory

Library rt.classic.analysis.global.jitter.workload_bound

Library rt.classic.analysis.global.jitter.interference_bound_fp

Library rt.classic.analysis.apa.interference_bound

Library rt.classic.analysis.apa.bertogna_fp_comp

Library rt.classic.analysis.apa.bertogna_edf_comp

Library rt.classic.analysis.apa.bertogna_edf_theory

Library rt.classic.analysis.apa.interference_bound_edf

Library rt.classic.analysis.apa.bertogna_fp_theory

Library rt.classic.analysis.apa.workload_bound

Library rt.classic.analysis.apa.interference_bound_fp

Library rt.classic.analysis.uni.arrival_curves.workload_bound

Library rt.classic.analysis.uni.susp.sustainability.singlecost.reduction_properties

Library rt.classic.analysis.uni.susp.sustainability.singlecost.reduction

Library rt.classic.analysis.uni.susp.sustainability.allcosts.main_claim

Library rt.classic.analysis.uni.susp.sustainability.allcosts.reduction_properties

Library rt.classic.analysis.uni.susp.sustainability.allcosts.reduction

Library rt.classic.analysis.uni.susp.dynamic.oblivious.reduction

Library rt.classic.analysis.uni.susp.dynamic.oblivious.fp_rta

Library rt.classic.analysis.uni.susp.dynamic.jitter.rta_by_reduction

• • • • Main Claim

Library rt.classic.analysis.uni.susp.dynamic.jitter.taskset_rta

Library rt.classic.analysis.uni.susp.dynamic.jitter.jitter_taskset_generation

Library rt.classic.analysis.uni.susp.dynamic.jitter.taskset_membership

Library rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_service

• • 6-(A) Less High-Priority Service Before the Arrival of Job j in sched_jitter
    • • Main Claim of Section (A)
  • 6-(B) More High-Priority Service After the Arrival of Job j in sched_jitter
    • • Main Claim of Section (B)
  • 6-(C) Conclusion: Comparing Response Times of Job j
    • • Main Claim of Section (C)

Library rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties

Library rt.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule

Library rt.classic.analysis.uni.basic.tdma_rta_theory

Library rt.classic.analysis.uni.basic.fp_rta_comp

Library rt.classic.analysis.uni.basic.workload_bound_fp

Library rt.classic.analysis.uni.basic.tdma_wcrt_analysis

Library rt.classic.analysis.uni.basic.fp_rta_theory

Library rt.classic.analysis.uni.jitter.fp_rta_comp

Library rt.classic.analysis.uni.jitter.workload_bound_fp

Library rt.classic.analysis.uni.jitter.fp_rta_theory

Library rt.restructuring.model.preemption.parameter

• Job Preemptable
• Derived Parameters
• Job Maximum and Last Non-preemptive Segment
• Platform with limited preemptions

Library rt.restructuring.model.preemption.limited_preemptive

• Platform for Models with Limited Preemptions

Library rt.restructuring.model.preemption.fully_nonpreemptive

• Platform for Fully Non-Preemptive Model

Library rt.restructuring.model.preemption.fully_preemptive

• Platform for Fully Premptive Model

Library rt.restructuring.model.priority.classes

Library rt.restructuring.model.priority.edf

Library rt.restructuring.model.task.preemption.limited_preemptive

• Platform for Models with Limited Preemptions
• Task's Run to Completion Threshold

Library rt.restructuring.model.task.preemption.fully_nonpreemptive

• Platform for Fully Non-Preemptive Model
• Task's Run to Completion Threshold

Library rt.restructuring.model.task.preemption.fully_preemptive

• Platform for Fully Preemptive Model
• Task's Run to Completion Threshold

Library rt.restructuring.model.task.preemption.floating_nonpreemptive

• Platform for Models with Floating Non-Preemptive Regions
• Task's Run to Completion Threshold

Library rt.restructuring.model.task.preemption.parameters

• Static information about preemption points
• Derived Parameters
• Task Maximum and Last Non-preemptive Segment
• Validity of a Preemption Model
• Task's Run-to-Completion Threshold

Library rt.restructuring.model.task.sequentiality

Library rt.restructuring.model.task.concept

Library rt.restructuring.model.task.absolute_deadline

Library rt.restructuring.model.schedule.nonpreemptive

Library rt.restructuring.model.schedule.work_conserving

Library rt.restructuring.model.schedule.limited_preemptive

• Schedule with Limited Preemptions

Library rt.restructuring.model.schedule.edf

Library rt.restructuring.model.schedule.priority_driven

Library rt.restructuring.model.schedule.preemption_time

• Preemption Time in Ideal Uni-Processor Model

Library rt.restructuring.model.schedule.tdma

Library rt.restructuring.model.processor.multiprocessor

Library rt.restructuring.model.processor.ideal

Library rt.restructuring.model.processor.varspeed

Library rt.restructuring.model.processor.platform_properties

Library rt.restructuring.model.processor.spin

Library rt.restructuring.model.readiness.basic

Library rt.restructuring.model.readiness.jitter

Library rt.restructuring.model.aggregate.service_of_jobs

• Service Received by Sets of Jobs

Library rt.restructuring.model.aggregate.workload

• Workload of Sets of Jobs

Library rt.restructuring.model.aggregate.task_arrivals

Library rt.restructuring.model.arrival.arrival_curves

Library rt.restructuring.model.arrival.sporadic

Library rt.restructuring.behavior.schedule

• Generic Processor State
• Schedule Representation

Library rt.restructuring.behavior.arrival_sequence

• Notion of an Arrival Sequence
• Arrival of a Job
• Validity of an Arrival Sequence
• Arrival Time Predicates
• Finite Arrival Sequence Prefixes

Library rt.restructuring.behavior.all

Library rt.restructuring.behavior.ready

• Readiness of a Job
• Backlogged Jobs
• Validity of a Schedule

Library rt.restructuring.behavior.service

• Service of a Job
• Job Completion and Response Time
• Pending or Incomplete Jobs

Library rt.restructuring.behavior.job

• Notion of a Job Type
• Unit of Work
• Basic Job Parameters — Cost, Arrival Time, and Absolute Deadline

Library rt.restructuring.behavior.time

• Model of Time

Library rt.restructuring.analysis.transform.prefix

Library rt.restructuring.analysis.transform.edf_trans

Library rt.restructuring.analysis.transform.swap

Library rt.restructuring.analysis.transform.facts.edf_opt

Library rt.restructuring.analysis.transform.facts.swaps

Library rt.restructuring.analysis.transform.facts.replace_at

Library rt.restructuring.analysis.schedulability

Library rt.restructuring.analysis.definitions.no_carry_in

• No Carry-In

Library rt.restructuring.analysis.definitions.busy_interval

• Busy Interval for JLFP-models

Library rt.restructuring.analysis.definitions.job_properties

Library rt.restructuring.analysis.definitions.priority_inversion

• Cumulative Priority Inversion for JLFP-models

Library rt.restructuring.analysis.facts.busy_interval_exists

• Existence of Busy Interval for JLFP-models

Library rt.restructuring.analysis.facts.priority_inversion_is_bounded

• Priority inversion is bounded
• Processor Executes HEP jobs after Preemption Point
• Preemption Time Exists

Library rt.restructuring.analysis.facts.edf

Library rt.restructuring.analysis.facts.tdma

Library rt.restructuring.analysis.facts.no_carry_in_exists

• Existence of No Carry-In Instant

Library rt.restructuring.analysis.facts.readiness.basic

Library rt.restructuring.analysis.edf.optimality

Library rt.restructuring.analysis.edf.rta.response_time_bound

• Abstract RTA for EDF-schedulers with Bounded Priority Inversion
  • Filling Out Hypothesis Of Abstract RTA Theorem
  • Final Theorem

Library rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.nonpreemptive

• RTA for Fully Non-Preemptive FP Model

Library rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.limited

• RTA for EDF-schedulers with Fixed Premption Points

Library rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.preemptive

• RTA for Fully Preemptive EDF Model

Library rt.restructuring.analysis.edf.rta.nonpr_reg.concrete_models.floating

• RTA for Model with Floating Non-Preemptive Regions

Library rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound

• RTA for EDF-schedulers with Bounded Non-Preemprive Segments
  • Priority inversion is bounded
  • Response-Time Bound

Library rt.restructuring.analysis.fixed_priority.rta.response_time_bound

• Abstract RTA for FP-schedulers with Bounded Priority Inversion
  • Filling Out Hypotheses Of Abstract RTA Theorem
  • Final Theorem

Library rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.nonpreemptive

• RTA for Fully Non-Preemptive FP Model

Library rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.limited

• RTA for FP-schedulers with Fixed Premption Points

Library rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.preemptive

• RTA for Fully Preemptive FP Model

Library rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.concrete_models.floating

• RTA for Model with Floating Non-Preemptive Regions

Library rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound

• RTA for FP-schedulers with Bounded Non-Preemprive Segments
  • Priority inversion is bounded
  • Response-Time Bound

Library rt.restructuring.analysis.task_schedule

• Schedule of task

Library rt.restructuring.analysis.abstract.core.definitions

• Definitions for Abstract Response-Time Analysis

Library rt.restructuring.analysis.abstract.core.abstract_rta

• Abstract Response-Time Analysis

Library rt.restructuring.analysis.abstract.core.sufficient_condition_for_run_to_completion_threshold

• Run-to-Completion Threshold of a job

Library rt.restructuring.analysis.abstract.core.reduction_of_search_space

• Reduction of the serach space for Abstract RTA

Library rt.restructuring.analysis.abstract.core.abstract_seq_rta

• Abstract Response-Time Analysis with sequential tasks

Library rt.restructuring.analysis.abstract.core.run_to_completion_threshold

Library rt.restructuring.analysis.abstract.instantiations.ideal_processor

• JLFP instantiation of Interference and Interfering Workload for ideal uni-processor.
  • Interference and Interfering Workload
  • Equivalences

Library rt.restructuring.analysis.basic_facts.deadlines

Library rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive

• Platform for Fully Non-Premptive Model

Library rt.restructuring.analysis.basic_facts.preemption.task.limited

• Platform for Models with Limited Preemptions

Library rt.restructuring.analysis.basic_facts.preemption.task.preemptive

• Platform for Fully Premptive Model

Library rt.restructuring.analysis.basic_facts.preemption.task.floating

• Platform for Floating Non-Premptive Regions Model

Library rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive

• Platform for Fully Non-Preemptive model

Library rt.restructuring.analysis.basic_facts.preemption.job.limited

• Platform for Models with Limited Preemptions

Library rt.restructuring.analysis.basic_facts.preemption.job.preemptive

• Preemptions in Fully Premptive Model

Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive

• Task's Run to Completion Threshold

Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited

• Task's Run to Completion Threshold

Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive

• Task's Run to Completion Threshold

Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating

• Task's Run to Completion Threshold

Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable

• Run-to-Completion Threshold

Library rt.restructuring.analysis.basic_facts.ideal_schedule

• Automation

Library rt.restructuring.analysis.basic_facts.service_of_jobs

• Lemmas about Service Received by Sets of Jobs

Library rt.restructuring.analysis.basic_facts.completion

Library rt.restructuring.analysis.basic_facts.all

Library rt.restructuring.analysis.basic_facts.workload

• Lemmas about Workload of Sets of Jobs

Library rt.restructuring.analysis.basic_facts.service

• Incremental Service in Ideal Schedule

Library rt.restructuring.analysis.basic_facts.arrivals

Library rt.restructuring.analysis.basic_facts.task_arrivals

Library rt.restructuring.analysis.basic_facts.sequential

Library rt.restructuring.analysis.arrival.rbf

• Request Bound Functions (RBF)

Library rt.restructuring.analysis.arrival.workload_bound

• Task Workload Bounded by Arrival Curves