From 2bba515797e56de72f5efdaa62285c29c3553a9f Mon Sep 17 00:00:00 2001 From: Xiaojie Guo Date: Mon, 26 Aug 2019 11:10:29 +0200 Subject: [PATCH] minor --- restructuring/analysis/fpp_implicit_deadline/intermediate.v | 3 ++- restructuring/analysis/fpp_implicit_deadline/main_theorem.v | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/restructuring/analysis/fpp_implicit_deadline/intermediate.v b/restructuring/analysis/fpp_implicit_deadline/intermediate.v index d5dda20..0781ca2 100644 --- a/restructuring/analysis/fpp_implicit_deadline/intermediate.v +++ b/restructuring/analysis/fpp_implicit_deadline/intermediate.v @@ -435,7 +435,8 @@ Proof. (n:=service sched j (end_of_analyse_interval)); auto. have /eqP<-: (t2 == end_of_analyse_interval); auto. have /eqP->: (len == t2 - t1); auto. - rewrite addnBCA. apply incr_service. apply leq_addr. + rewrite addnBA. rewrite addnC -addnBA. + apply incr_service. apply leq_addr. apply start_inf_arrival. rewrite ltnW; auto. apply start_inf_end. Qed. diff --git a/restructuring/analysis/fpp_implicit_deadline/main_theorem.v b/restructuring/analysis/fpp_implicit_deadline/main_theorem.v index bf772ac..e4f8eae 100644 --- a/restructuring/analysis/fpp_implicit_deadline/main_theorem.v +++ b/restructuring/analysis/fpp_implicit_deadline/main_theorem.v @@ -93,7 +93,8 @@ Section exists_t2. Let workload_bound := formula. Lemma exists_t2 : forall delta, - delta > 0 -> workload_bound delta = delta + delta > 0 -> workload_bound delta = delta + -> delta <= task_deadline tsk -> (forall j, arrives_in arr_seq j -> job_task j = tsk -> exists t2, job_arrival j < t2 /\ completes_at sched j t2). Proof. -- GitLab