Commit 6f2cb4d7 authored by Vedant Chavda's avatar Vedant Chavda

change lemma name

parent 6929caa1
Pipeline #31948 failed with stages
in 20 minutes and 45 seconds
...@@ -79,7 +79,7 @@ Section JobArrivalSeparation. ...@@ -79,7 +79,7 @@ Section JobArrivalSeparation.
(** We prove that arrival of unequal jobs of a task [tsk] are (** We prove that arrival of unequal jobs of a task [tsk] are
separated by a non-zero multiple of [task_period tsk] provided separated by a non-zero multiple of [task_period tsk] provided
their index differs by a number [k]. *) their index differs by a number [k]. *)
Lemma job_sep_periodic_induction : Lemma job_arrival_separation_when_index_diff_is_k :
exists n, exists n,
n > 0 /\ n > 0 /\
job_arrival j2 = job_arrival j1 + n * task_period tsk. job_arrival j2 = job_arrival j1 + n * task_period tsk.
...@@ -140,7 +140,7 @@ Section JobArrivalSeparation. ...@@ -140,7 +140,7 @@ Section JobArrivalSeparation.
n > 0 /\ n > 0 /\
job_arrival j2 = job_arrival j1 + n * task_period tsk. job_arrival j2 = job_arrival j1 + n * task_period tsk.
Proof. Proof.
apply job_sep_periodic_induction with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done. apply job_arrival_separation_when_index_diff_is_k with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done.
- apply subnKC. - apply subnKC.
move_neq_up IND. move_neq_up IND.
eapply lower_index_implies_earlier_arrival in IND; eauto with basic_facts. eapply lower_index_implies_earlier_arrival in IND; eauto with basic_facts.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment