Commit ab788abc authored by Vedant Chavda's avatar Vedant Chavda


parent f1d6d35d
Pipeline #32026 failed with stages
in 20 minutes and 18 seconds
......@@ -331,6 +331,21 @@ Section todo_name.
intros * ARR TSK IND T_G.
rewrite /job_index in IND.
rewrite -IND.
have EQ_IND : index j' (task_arrivals_up_to_job_arrival arr_seq j') = index j' (task_arrivals_up_to arr_seq tsk t).
{ have CAT : exists xs, task_arrivals_up_to_job_arrival arr_seq j' ++ xs = task_arrivals_up_to arr_seq tsk t.
{ rewrite /task_arrivals_up_to_job_arrival TSK.
exists (task_arrivals_between arr_seq tsk ((job_arrival j').+1) t.+1).
now rewrite -task_arrivals_cat.
move : CAT => [xs ARR_CAT].
now rewrite -ARR_CAT index_cat ifT; last by apply arrives_in_task_arrivals_up_to.
rewrite EQ_IND.
rewrite nth_index => //.
rewrite mem_filter; apply /andP.
split; first by apply /eqP.
apply mem_bigcat_nat with (j := job_arrival j'); first by ssromega.
admit. (* provable*)
Lemma exists_job_in_task_arrivals_at :
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