### /restructuring/analysis/analysis_up_to_t/schedulability_up_to_t.v

It defines what it means to be a upper or lower response time bound until t, - and then shows the equivalence between being a bound up ot t for all t and - being a general time bound. + and then shows the equivalence between being a bound up ot t for all t and being a general time bound.

### /restructuring/analysis/analysis_up_to_t/cpa_temporal_step.v

- It defines what it means to be a upper or lower response time bound until t, - and then shows the equivalence between being a bound up ot t for all t and - being a general time bound. + It uses the abstract model defined in simple_abstracted.v. + The redundant definition of task_input_model and task_model_correct_until_t + should allow tasks to follow different types of arrival models. + + Its purpose is the "final result", which states that if all conditions are met, + the WCRTs given by CPA will indeed be upper bounds on the response time for each task. + + This uses 2 hypothesis meant to provide analysis on a propagationnal property of the schedule, and an analysis on WCRT. + They have yet to be proved in the exemple of the periodic_jitter_model. + +

### /restructuring/analysis/analysis_up_to_t/periodic_jitter_propagation_up_to_t.v

+ + There are two sections here. + + In the first one, there is a proof of the propagatability of the finite + periodic jitter model, very similar to the one in periodic_jitter_same_law. + However the third hypothesis of that model is thrown away since we use the + 2 hypothesis finite model. + + In the second one, the above result is used to prove that if all task follow a + periodic with jitter arrival model, and the system verify some reasonnable hypothesis, + then the result of CPA will be correct. + + The analysis giving the correction of WCRTs is not done yet. + +

### /restructuring/analysis/analysis_up_to_t/up_to_t_definitions.v

+ + some definitions of properties that were defined indefinitely that now + have an equivalent up to t.