Commit 4c3c0d95 authored by jonathan julou's avatar jonathan julou

message

parent c8dafa7c
......@@ -327,11 +327,11 @@ Section Transformation.
(*if the base schedule is valid up to t, the completed_schedule
is always valid with the completed arrival_sequence*)
Lemma valid_schedule_to_prefixed_sched :
(*valid_arrival_sequence_up_to_t arr_seq t ->*)
valid_arrival_sequence_up_to_t arr_seq t ->
valid_schedule_up_to_t State sched arr_seq t ->
valid_schedule_up_to_t State sched arr_seq_prefixed t.
Proof.
intros VS.
intros VAS VS.
unfold valid_schedule_up_to_t in VS. destruct VS as [A B]. destruct B as [B C].
unfold valid_schedule_up_to_t. split. 2: split.
- unfold jobs_come_from_arrival_sequence_up_to_t in A.
......@@ -341,9 +341,11 @@ Section Transformation.
destruct D as [y P].
unfold arrivals_at. unfold arr_seq_prefixed.
exists y. destruct (y<=t) eqn:E. unfold arrivals_at in P. exact P.
unfold valid_arrival_sequence_up_to_t in VAS. destruct VAS as [N M].
unfold consistent_arrival_times_up_to_t in N.
admit.
- admit.
- admit.
- exact B.
- exact C.
Admitted.
(*if the base schedule is valid up to t, the completed_schedule
......@@ -355,7 +357,7 @@ Section Transformation.
Proof.
intros VAS VS0.
assert (VS : valid_schedule_up_to_t State sched arr_seq_prefixed t).
apply valid_schedule_to_prefixed_sched. exact VS0.
apply valid_schedule_to_prefixed_sched; auto.
unfold valid_schedule_up_to_t in VS. destruct VS as [A B]. destruct B as [B C].
apply complete_schedule_valid; auto.
- apply valid_arrival_sequence_completion. exact VAS.
......
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