From 24589c66e02d444b2187c7e635751e68f82961de Mon Sep 17 00:00:00 2001 From: Gordon Stewart Date: Tue, 19 Dec 2017 15:42:10 -0500 Subject: [PATCH] Change best_response to better_response --- potential.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/potential.v b/potential.v index 9d864c8..b343153 100644 --- a/potential.v +++ b/potential.v @@ -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=> //. @@ -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