Skip to content

Commit

Permalink
Change best_response to better_response
Browse files Browse the repository at this point in the history
  • Loading branch information
gstew5 committed Dec 19, 2017
1 parent 91c7947 commit 24589c6
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions potential.v
Expand Up @@ -171,7 +171,7 @@ Section BestResponseDynamics.
by subst t'; rewrite H3 H4.
Qed.

Lemma best_response_safe t :
Lemma better_response_safe t :
safe step halted t.
Proof.
move=> t''; induction 1=> //.
Expand All @@ -189,18 +189,18 @@ Section BestResponseDynamics.
by rewrite ltrNge; apply/negP.
Qed.

Lemma best_response_everywhere_halts t :
Lemma better_response_everywhere_halts t :
everywhere_halts step halted t.
Proof.
apply: (step_everywhere_halts_or_stuck P).
apply: init_P.
apply: step_P.
apply: halted_doesnt_step.
apply: best_response_safe.
apply: better_response_safe.
Qed.
End BestResponseDynamics.

Print Assumptions best_response_everywhere_halts.
Print Assumptions better_response_everywhere_halts.

Section PriceOfStabilityBound.
(** The following section proves a bound on the Price of Stability
Expand Down

0 comments on commit 24589c6

Please sign in to comment.