Skip to content
Snippets Groups Projects
Commit b84e166c authored by Sébastien Bouchard's avatar Sébastien Bouchard
Browse files

Simplification of some proof renewed (don't know why it disappeared)

parent 218dc415
No related branches found
No related tags found
No related merge requests found
......@@ -522,7 +522,7 @@ Proof using . intros k ??. subst. apply Stream.forever_compat. intros ?? Heq. no
(** A k-fair demon is fair. *)
Lemma Between_eventually_activated : forall id (d : demon) id' k,
Between id id' d k -> Stream.eventually (Stream.instant (fun da => activate da id = true)) d.
Proof using . intros * Hg. induction Hg; now constructor; trivial; firstorder. Qed.
Proof using . intros * Hg. induction Hg; constructor; assumption. Qed.
Theorem kFair_Fair : forall k (d : demon), kFair k d -> Fair d.
Proof using .
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment