Commit 839bdc2e authored by jonathan julou's avatar jonathan julou

petit commit

parent bbf3dfa0
......@@ -142,7 +142,8 @@ Section CPA_temp_step.
(*final lemma: all WCRT correct for infinite traces.
It should be unnecessary to verify BCRTs at this step,
but should be easy by mimicking the WCRT proof*)
but should be easy by extracting it alongside the WCRT
in the assertion P.*)
Lemma final_result: forall tsk, tsk \in ts ->
task_response_time_upper_bound arr_seq sched tsk (task_WCRT tsk).
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment