# Library prosa.analysis.facts.preemption.job.preemptive

Require Export prosa.model.task.preemption.parameters.

Require Export prosa.model.preemption.fully_preemptive.

Require Export prosa.model.preemption.fully_preemptive.

# Preemptions in Fully Preemptive Model

In this section, we prove that instantiation of predicate job_preemptable to the fully preemptive model indeed defines a valid preemption model.
We assume that jobs are fully preemptive.

#[local] Existing Instance fully_preemptive_job_model.

Consider any type of jobs.

Consider any kind of processor state model, ...

... any job arrival sequence, ...

... and any given schedule.

Then, we prove that fully_preemptive_model is a valid preemption model.

We also prove that under the fully preemptive model
job_max_nonpreemptive_segment j is equal to 0, when job_cost
j = 0 ...

Lemma job_max_nps_is_ε:

∀ j,

job_cost j > 0 →

job_max_nonpreemptive_segment j = ε.

End FullyPreemptiveModel.

Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.

∀ j,

job_cost j > 0 →

job_max_nonpreemptive_segment j = ε.

End FullyPreemptiveModel.

Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.