Commit 91b497aa authored by Felipe Cerqueira's avatar Felipe Cerqueira

Finish FP proof

parent d5fb86e5
This diff is collapsed.
......@@ -84,7 +84,6 @@ VFILES:=apa.v\
BertognaResponseTimeDefs.v\
BertognaResponseTimeFP.v\
divround.v\
eqtask_dec.v\
extralib.v\
ExtraRelations.v\
helper.v\
......
......@@ -546,16 +546,6 @@ Proof.
[by rewrite Rxy in XY' | by rewrite Ryx in YX'].
Qed.
Lemma leq_sum_subseq :
forall {I: eqType} r1 r2 (P : pred I) F
(SUB: subseq r1 r2),
\sum_(i <- r1 | P i) F i <= \sum_(i <- r2 | P i) F i.
Proof.
ins.
admit.
Qed.
Lemma sorted_rcons_prefix :
forall {T: eqType} (leT: rel T) s x
(SORT: sorted leT (rcons s x)),
......
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