tighten response-time recurrence for EDF

When we were writing the paper on Abstract RTA, we noticed that the response-time recurrence for EDF does not match the known bound.

This merge request tightens the analysis in Prosa to match the known bound.
6 jobs for master in 5 minutes and 14 seconds
Status Job ID Name Coverage
  Build
passed #39880
1.8.0-coq-8.8

00:02:02

passed #39882
1.9.0-coq-8.9

00:01:46

failed #39881
allowed to fail
1.9.0-coq-dev

00:00:13

 
  Process
passed #39884
doc

00:00:22

passed #39885
proof-length

00:00:15

passed #39883
validate

00:01:25

 
Name Stage Failure
failed
1.9.0-coq-dev Build There is an unknown failure, please try again
COQC util/powerset.v
COQC util/seqset.v
File "./util/seqset.v", line 19, characters 42-52:
Error: The reference mkPredType was not found in the current environment.

make[1]: *** [Makefile:659: util/seqset.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:321: all] Error 2
ERROR: Job failed: exit code 1