(* Time-stamp: "modifie le 6 Sep 2009 a 19:22 par Pierre Lescanne sur boucherotte" *) (* ~/Documents/COQ/GAMES/EXTENSIVE/escalation.v *) (********************************************************************************) (* escalation.v *) (* *) (** © Pierre Lescanne (February 2008) *) (* *) (* LIP (ENS-Lyon, CNRS, INRIA) *) (* *) (* *) (** Developed in V8.1 February 2008 --- January 2009 *) (********************************************************************************) (* --------------- *) (** * Preliminaries *) (* --------------- *) Set Implicit Arguments. Require Import Relations. Require Import Arith. Require Import Omega. (* begin hide *) Add LoadPath ".". (* end hide *) Require Import infinite_extensive_games. Require Import Le. Implicit Arguments sLeaf [Agent Utility]. Implicit Arguments sNode [Agent Utility]. Implicit Arguments s2u [Agent Utility]. Implicit Arguments LeadsToLeaf [Agent Utility]. Implicit Arguments AlwLeadsToLeaf [Agent Utility]. Implicit Arguments SGPE [Agent Utility]. (* ----------------- *) (** - Data and tools *) (* ----------------- *) Inductive Alice_Bob :Set := Alice :Alice_Bob | Bob: Alice_Bob. Definition Strat := StratProf Alice_Bob nat. Notation "s1 |-- a --| s2" := (IndAgentConv Alice_Bob nat a s1 s2) (at level 70). Notation "<< a , c , sl , sr >>" := (sNode a c sl sr) (at level 80). Notation "[ x , y ]" := (sLeaf (fun a:Alice_Bob => match a with Alice => x | Bob => y end)) (at level 80). (* A cA ---- B cB------- s | | | | add_Alice_Bob_esc(cA,cB,n,s) = | | | | | | 2n+1 2n+1 2*n 2n+2 *) (* ===================== *) (** * Illogic escalation *) (* ===================== *) (* --------------------------- *) (** ** StratProf "Never Give Up" *) (* --------------------------- *) (* A +++++++ B ++++++++ ngu n+1 | | | | ngu n = | | | | | | 2n+1 2n+1 2*n 2n+2 A +++++++ B ++++++++ A +++++++ B +++++++ A ++++++++ B +++... | | | | | | | | | | | | = | | | | | | ... | | | | | | | | | | | | 2n+1 2n+1 2n+3 2n+3 2n+5 2n+5 2*n 2n+2 2n+2 2n+4 2n+4 2n+6 *) Definition add_Alice_Bob_esc (cA cB:Choice) (n:nat) (s:Strat) := <>,[2*n+1,2*n]>>. CoFixpoint ngu (n:nat): (Strat) := add_Alice_Bob_esc l l n (ngu (S n)). Lemma ngu_decomposition: forall n:nat, (ngu n) = <>,[2*n+1,2*n]>>. Proof. intros. replace (ngu n) with (StratProf_identity Alice_Bob nat (ngu n)). simpl. trivial. apply StratProf_decomposition. Qed. CoInductive NeverLeaf: Strat -> Prop := | NvLLeft: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf sl -> NeverLeaf (<>) | NvLRight: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf sr -> NeverLeaf (<>). Lemma NLLeft: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf (<>) -> NeverLeaf sl. Proof. intros. inversion H. assumption. Qed. Lemma NLRight: forall (a:Alice_Bob) (sl sr: Strat), NeverLeaf (<>) -> NeverLeaf sr. Proof. intros. inversion H. assumption. Qed. Lemma NeverLeaf_then_not_LeadsToLeaf: forall s: Strat, NeverLeaf s -> ~LeadsToLeaf s. Proof. unfold not. intros s H_NL. induction 1. inversion H_NL. apply IHLeadsToLeaf. apply NLLeft with (a:=a) (sr:=sr). assumption. apply IHLeadsToLeaf. apply NLRight with (a:=a) (sl:=sl). assumption. Qed. Lemma NeverLeaf_ngu: forall (n:nat), NeverLeaf (ngu n). Proof. cofix H. intros. rewrite ngu_decomposition. apply NvLLeft. apply NvLLeft. apply H. Qed. Lemma Not_LeadsToLeaf_ngu: forall (n:nat), ~LeadsToLeaf (ngu n). Proof. intros. apply NeverLeaf_then_not_LeadsToLeaf. apply NeverLeaf_ngu. Qed. Lemma NotSGPE_NGU: forall (n:nat), ~SGPE ge (ngu n). Proof. unfold not. intros. elim Not_LeadsToLeaf_ngu with (n:=n). apply ALtL_then_LtL. apply SGPE_then_AlwLeadsToLeaf with (preference:=ge). assumption. Qed. Lemma Nasheq_NGU: forall (n:nat), NashEq Alice_Bob nat ge (ngu n). Proof. unfold NashEq. intros. cut False. intuition. generalize H2. apply Not_LeadsToLeaf_ngu. Qed. (* ---------------------------- *) (** ** StratProf "Always Give Up" *) (* ---------------------------- *) (* A ------- B -------- ngu n+1 + + + + ngu n = + + + + + + 2n+1 2n+1 2*n 2n+2 A ------- B -------- A ------- B ------- A -------- B ---... + + + + + + + + + + + + = + + + + + + ... + + + + + + + + + + + + 2n+1 2n+1 2n+3 2n+3 2n+5 2n+5 2*n 2n+2 2n+2 2n+4 2n+4 2n+6 *) (* --------------------------- *) (** - StratProf "always give up" *) (* --------------------------- *) CoFixpoint agu (n:nat):(Strat) := add_Alice_Bob_esc r r n (agu (S n)). (* -------------------- *) (** - Preliminary lemmas *) (* -------------------- *) Lemma AlwLeadsToLeaf_agu: forall (n:nat), AlwLeadsToLeaf (agu n). Proof. cofix H. intros. replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply H. apply ALtLeaf. apply ALtLeaf. rewrite <- StratProf_decomposition; trivial. Qed. Lemma LeadsToLeaf_agu: forall (n:nat), LeadsToLeaf (agu n). Proof. intros. apply ALtL_then_LtL. apply AlwLeadsToLeaf_agu. Qed. Lemma S2u_agu_Alice: forall (n:nat), s2u (agu n) Alice (2*n+1). Proof. intros; replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_agu_Bob: forall (n:nat), s2u (agu n) Bob (2*n). Proof. intros; replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. (* ---------------------------------------------------------- *) (** - StratProf Always Give Up is a Subgame Perfect Equilibrium *) (* ---------------------------------------------------------- *) Theorem SGPEAGU: forall (n:nat), SGPE ge (agu n). Proof. cofix H. intros n. replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. apply SGPE_right with (u:= 2*n+1) (v:=2*n+1). apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_agu. apply ALtLeaf. apply ALtLeaf. apply SGPE_right with (u:= 2*n+2) (v:=2*n+2). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_agu. apply ALtLeaf. apply H. apply SGPE_leaf. replace (2*n+2) with (2*(S n)). apply S2u_agu_Bob. auto. replace (2*n+2) with (n+(n+0)+2). apply s2uLeaf with (a:=Bob)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end). auto. auto. apply SGPE_leaf. apply s2uRight. apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) + 2 end). apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) + 1 | Bob => n + (n + 0) end). auto. rewrite <- StratProf_decomposition; trivial. Qed. (* ----------------------------------------------- *) (** - StratProf Always Give Up is a Nash Equilibrium *) (* ----------------------------------------------- *) Lemma conv_agu_s2u_Alice: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat), s|--a--| (agu n) -> s2u s Alice u -> u=2*n+1. Proof. intros n. replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. intros. destruct s. inversion H. destruct c. destruct a. apply Uniqueness_s2u with (s:=s1)(a:=a0). apply ALtL_then_LtL. apply AlwLeadsToLeaf_Preservation with (s:=<>)(a:=Alice). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_agu. apply ALtLeaf. apply IndConvSym. apply IndConvProjL with (a:=a0)(a':=Alice)(c:=l)(c':=r)(sr:=s2)(sr':=[2*n+1,2*n]). assumption. replace a0 with Alice. apply s2uLeft_rev with (a':=a0)(sr:=s2). assumption. inversion H; apply refl_equal. replace a0 with Alice. destruct s1. inversion H. inversion H4. destruct c. inversion H. inversion H4. apply s2uRight. replace s1_2 with ([2*n+1,2*n+2]). apply s2uLeaf with (f := (fun a1 : Alice_Bob => match a1 with | Alice => 2 * n + 1 | Bob => 2 * n + 2 end))(a:=Alice). inversion H. inversion H4. apply refl_equal. apply sym_equal. apply IndConvLeaf with (a:=Alice). assumption. inversion H; apply refl_equal. inversion H. apply sym_equal. apply Uniqueness_s2u with (s:=[2*n+1,2*n])(a:=a0). apply LtLLeaf. replace a0 with Alice. apply s2uLeaf with (f := (fun a1 : Alice_Bob => match a1 with | Alice => 2 * n + 1 | Bob => 2 * n end))(a:=Alice). apply sym_equal. inversion H; apply refl_equal. replace a0 with Alice. replace ([2*n+1,2*n]) with s2. apply s2uRight_rev with (a':=a0)(sl:=s1). assumption. apply IndConvLeaf with (a:=a). apply IndConvProjR with (a:=a0)(a':=Alice)(c:=r)(c':=r)(sl:=s1)(sl':=<>). assumption. apply sym_equal. apply IndConvSameHeadAgent with (a'':=a)(c:=r)(c':=r)(sl:=s1)(sr:=s2)(sl':=<>)(sr':=[2*n+1,2*n]). assumption. apply StratProf_decomposition. Qed. Lemma conv_agu_s2u_Bob: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat), s|--a--| (agu n) -> s2u s Bob u -> u=2*n \/ u=2*n+2. Proof. intros n. replace (agu n) with (StratProf_identity Alice_Bob nat (agu n)). simpl. intros. destruct s. inversion H. destruct c. destruct a. right. apply Uniqueness_s2u with (s:=s1)(a:=Bob). apply ALtL_then_LtL. apply AlwLeadsToLeaf_Preservation with (s:=<>)(a:=Alice). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_agu. apply ALtLeaf. apply IndConvSym. apply IndConvProjL with (a:=a0)(a':=Alice)(c:=l)(c':=r)(sr:=s2)(sr':=[2*n+1,2*n]). assumption. apply s2uLeft_rev with (a':=a0)(sr:=s2). assumption. destruct s1. inversion H. inversion H4. destruct c. inversion H. inversion H4. apply s2uRight. replace s1_2 with ([2*n+1,2*n+2]). apply s2uLeaf with (f := (fun a1 : Alice_Bob => match a1 with | Alice => 2 * n + 1 | Bob => 2 * n + 2 end))(a:=Bob). inversion H. inversion H4. apply refl_equal. apply sym_equal. apply IndConvLeaf with (a:=Alice). assumption. inversion H. (* right *) destruct a. left. apply Uniqueness_s2u with (s:=[2*n+1,2*n])(a:=Bob). apply LtLLeaf. replace ([2*n+1,2*n]) with s2. apply s2uRight_rev with (sl:=s1)(a':=a0). assumption. apply IndConvLeaf with (a:=Alice). apply IndConvProjR with (a:=a0)(a':=Alice)(c:=r)(c':=r)(sl:=s1)(sl':=<>). assumption. apply s2uLeaf with (f := (fun a1 : Alice_Bob => match a1 with | Alice => 2 * n + 1 | Bob => 2 * n end))(a:=Bob). left. apply Uniqueness_s2u with (s:=[2*n+1,2*n])(a:=Bob). apply LtLLeaf. replace ([2*n+1,2*n]) with s2. apply s2uRight_rev with (sl:=s1)(a':=a0). assumption. apply IndConvLeaf with (a:=Bob). apply IndConvProjR with (a:=a0)(a':=Alice)(c:=r)(c':=r)(sl:=s1)(sl':=<>). assumption. apply s2uLeaf with (f := (fun a1 : Alice_Bob => match a1 with | Alice => 2 * n + 1 | Bob => 2 * n end))(a:=Bob). apply StratProf_decomposition. Qed. Lemma NashEq_agu: forall (n:nat), NashEq Alice_Bob nat ge (agu n). Proof. unfold NashEq. intros n. intros. destruct a. replace u with (2*n+1). cut (u'=2*n+1). omega. apply conv_agu_s2u_Alice with (s:=s')(a:=Alice); assumption. apply Uniqueness_s2u with (s:=agu n)(a:=Alice). apply LeadsToLeaf_agu. apply S2u_agu_Alice. assumption. cut (u'=2*n \/ u'=2*n+2). replace u with (2*n). intuition. apply Uniqueness_s2u with (s:=agu n)(a:=Bob). apply LeadsToLeaf_agu. apply S2u_agu_Bob. assumption. apply conv_agu_s2u_Bob with (a:=Bob)(s:=s'); assumption. Qed. (* ===================== *) (** * Centiped *) (* ===================== *) (* A +++++++ B ++++++++ ngu n+1 | | | | centiped = | | | | | | 2n 2n-1 2n 2n+3 A +++++++ B ++++++++ A +++++++ B +++++++ A ++++++++ B +++... | | | | | | | | | | | | = | | | | | | ... | | | | | | | | | | | | 2n 2n-1 2n+2 2n+1 2n+4 2n+3 2n 2n+3 2n+2 2n+5 2n+4 2n+7 *) Definition add_Alice_Bob_cent (cA cB:Choice) (n:nat) (s:Strat) := <>,[2*n,2*n]>>. (* --------------------------- *) (** - StratProf "never give up" *) (* --------------------------- *) CoFixpoint cent_ngu (n:nat): (Strat) := add_Alice_Bob_cent l l n (cent_ngu (S n)). Lemma cent_ngu_decomposition: forall n:nat, (cent_ngu n) = <>,[2*n,2*n]>>. Proof. intros. replace (cent_ngu n) with (StratProf_identity Alice_Bob nat (cent_ngu n)). simpl. trivial. apply StratProf_decomposition. Qed. Lemma NeverLeaf_cent_ngu: forall (n:nat), NeverLeaf (cent_ngu n). Proof. cofix H. intros. rewrite cent_ngu_decomposition. apply NvLLeft. apply NvLLeft. apply H. Qed. Lemma Not_LeadsToLeaf_cent_ngu: forall (n:nat), ~LeadsToLeaf (cent_ngu n). Proof. intros. apply NeverLeaf_then_not_LeadsToLeaf. apply NeverLeaf_cent_ngu. Qed. Lemma Nasheq_CENT_NGU: forall (n:nat), NashEq Alice_Bob nat le (cent_ngu n). Proof. unfold NashEq. intros. cut False. intuition. generalize H2. apply Not_LeadsToLeaf_cent_ngu. Qed. (* --------------------------- *) (** - StratProf "always give up" *) (* --------------------------- *) CoFixpoint cent_agu (n:nat): (Strat) := add_Alice_Bob_cent r r n (cent_agu (S n)). Lemma AlwLeadsToLeaf_cent_agu: forall (n:nat), AlwLeadsToLeaf (cent_agu n). Proof. cofix H. intros. replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply H. apply ALtLeaf. apply ALtLeaf. apply StratProf_decomposition. Qed. Lemma LeadsToLeaf_cent_agu: forall (n:nat), LeadsToLeaf (cent_agu n). Proof. intros. apply ALtL_then_LtL. apply AlwLeadsToLeaf_cent_agu. Qed. Lemma S2u_cent_agu_Alice: forall (n:nat), s2u (cent_agu n) Alice (2*n). Proof. intros; replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => 2*n | Bob => 2*n end)(a:=Alice). rewrite <- StratProf_decomposition; trivial. Qed. Lemma S2u_cent_agu_Bob: forall (n:nat), s2u (cent_agu n) Bob (2*n). Proof. intros; replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. apply s2uRight. apply s2uLeaf with (f:=fun a : Alice_Bob => match a with | Alice => 2*n | Bob => 2*n end)(a:=Bob). rewrite <- StratProf_decomposition; trivial. Qed. Theorem SGPE_cent_AGU: forall (n:nat), SGPE le (cent_agu n). Proof. cofix H. intros n. replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. apply SGPE_right with (u:= 2*n-1) (v:=2*n). apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_cent_agu. apply ALtLeaf. apply ALtLeaf. apply SGPE_right with (u:= 2*n+2) (v:=2*n+3). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_cent_agu. apply ALtLeaf. apply H. apply SGPE_leaf. replace (2*n+2) with (2*(S n)). apply S2u_cent_agu_Bob. auto. apply s2uLeaf with (a:=Bob)(f:=fun a : Alice_Bob => match a with | Alice =>2*n-1 | Bob => 2*n+3 end). omega. apply SGPE_leaf. apply s2uRight. apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => 2*n-1 | Bob => 2*n+3 end). apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => 2*n | Bob => 2*n end). omega. rewrite <- StratProf_decomposition; trivial. Qed. Lemma conv_cent_agu_s2u_Alice: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat), s|--a--| (cent_agu n) -> s2u s Alice u -> u=2*n \/ u=2*n-1. Proof. intros n. replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. intros. destruct s. inversion H. destruct c. destruct a. right. apply Uniqueness_s2u with (s:=s1)(a:=a0). apply ALtL_then_LtL. apply AlwLeadsToLeaf_Preservation with (s:=<>)(a:=Alice). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_cent_agu. apply ALtLeaf. apply IndConvSym. apply IndConvProjL with (a:=a0)(a':=Alice)(c:=l)(c':=r)(sr:=s2)(sr':=[2*n,2*n]). assumption. replace a0 with Alice. apply s2uLeft_rev with (a':=a0)(sr:=s2). assumption. inversion H; apply refl_equal. replace a0 with Alice. destruct s1. inversion H. inversion H4. destruct c. inversion H. inversion H4. apply s2uRight. replace s1_2 with ([2*n-1,2*n+3]). apply s2uLeaf with (f := (fun a1 : Alice_Bob => match a1 with | Alice => 2 * n - 1 | Bob => 2 * n + 3 end))(a:=Alice). inversion H. inversion H4. apply refl_equal. apply sym_equal. apply IndConvLeaf with (a:=Alice). assumption. inversion H; apply refl_equal. inversion H. left. apply Uniqueness_s2u with (s:=<< a0, r, s1, s2 >>)(a:=Alice). apply ALtL_then_LtL. apply AlwLeadsToLeaf_Preservation with (s:=<< Alice, r, << Bob, r, cent_agu (S n),[2*n-1,2*n+3]>>,[2*n,2*n]>>)(a:=a). apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_cent_agu. apply ALtLeaf. apply ALtLeaf. apply IndConvSym. assumption. assumption. replace a0 with Alice. replace s2 with ([2*n,2*n]). apply s2uRight. apply s2uLeaf with (f := (fun a1 : Alice_Bob => match a1 with | Alice => 2 * n | Bob => 2 * n end))(a:=Alice). apply sym_equal. apply IndConvLeaf with (a:=a). apply IndConvProjR with (sl:= s1)(sl':=<>)(a:=a0)(a':=Alice)(c:=r)(c':=r). assumption. inversion H; apply refl_equal. apply StratProf_decomposition. Qed. Lemma conv_cent_agu_s2u_Bob: forall (n:nat)(s:Strat)(a:Alice_Bob)(u:nat), s|--a--| (cent_agu n) -> s2u s Bob u -> u=2*n \/ u=2*n+3. Proof. intros n. replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. intros. destruct s. inversion H. destruct c. destruct a. right. apply Uniqueness_s2u with (s:=s1)(a:=Bob). apply ALtL_then_LtL. apply AlwLeadsToLeaf_Preservation with (s:=<>)(a:=Alice). apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_cent_agu. apply ALtLeaf. apply IndConvSym. apply IndConvProjL with (a:=a0)(a':=Alice)(c:=l)(c':=r)(sr:=s2)(sr':=[2*n,2*n]). assumption. apply s2uLeft_rev with (a':=a0)(sr:=s2). assumption. destruct s1. inversion H. inversion H4. destruct c. inversion H. inversion H4. apply s2uRight. replace s1_2 with ([2*n-1,2*n+3]). apply s2uLeaf with (a:=Bob)(f := (fun a : Alice_Bob => match a with | Alice => n + (n + 0) - 1 | Bob => n + (n + 0) + 3 end)). apply sym_equal. apply IndConvLeaf with (a:=Alice). apply IndConvProjR with (sl:= s1_1)(sl':= cent_agu (S n))(a:=a)(a':=Bob)(c:=r)(c':=r). apply IndConvProjL with (sr:= s2)(sr':=[2*n,2*n])(a:=a0)(a':=Alice)(c:=l)(c':=r). assumption. inversion H. left. apply Uniqueness_s2u with (s:=<< a0, r, s1, s2 >>)(a:=Bob). apply ALtL_then_LtL. apply AlwLeadsToLeaf_Preservation with (s:=<>,[2*n,2*n]>>)(a:=a). apply ALtL. apply LtLRight. apply LtLLeaf. apply ALtL. apply LtLRight. apply LtLLeaf. apply AlwLeadsToLeaf_cent_agu. apply ALtLeaf. apply ALtLeaf. apply IndConvSym. assumption. assumption. destruct s2. apply s2uRight. replace (sLeaf u0) with ([2*n,2*n]). apply s2uLeaf with (a:=Bob)(f:=(fun a : Alice_Bob => match a with | Alice => n + (n + 0) | Bob => n + (n + 0) end)). apply sym_equal. apply IndConvLeaf with a. apply IndConvProjR with (a:=a0)(a':=Alice)(c:=r)(c':=r)(sl:=s1)(sl':=<>). assumption. inversion H. inversion H11. inversion H10. apply StratProf_decomposition. Qed. Lemma NashEq_cent_agu: forall (n:nat), NashEq Alice_Bob nat le (cent_agu n). Proof. unfold NashEq. intros n. intros. destruct a. replace u with (2*n). cut (u'=2*n \/ u'=2*n-1). omega. apply conv_cent_agu_s2u_Alice with (a:=Alice)(s:=s'). assumption. assumption. apply Uniqueness_s2u with (s:=cent_agu n)(a:=Alice). apply LeadsToLeaf_cent_agu. replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. apply s2uRight. apply s2uLeaf with (a:=Alice)(f:=fun a : Alice_Bob => match a with | Alice => n + (n + 0) | Bob => n + (n + 0) end). apply StratProf_decomposition. assumption. replace u with (2*n). replace u' with (2*n). auto. apply Uniqueness_s2u with (s:=s')(a:=Bob). assumption. generalize H. replace (cent_agu n) with (StratProf_identity Alice_Bob nat (cent_agu n)). simpl. intros. destruct s'. inversion H4. destruct c. inversion H4. apply s2uRight. replace s'2 with ([2*n,2*n]). apply s2uLeaf with (a:=Bob)(f:=(fun a0 : Alice_Bob => match a0 with | Alice => 2 * n | Bob => 2 * n end)). apply sym_equal. apply IndConvLeaf with (a:=Bob). apply IndConvProjR with (sl:= s'1)(sl':= <>)(a:=a)(a':=Alice)(c:=r)(c':=r). assumption. apply StratProf_decomposition. assumption. apply Uniqueness_s2u with (s:=cent_agu n)(a:=Bob). apply LeadsToLeaf_cent_agu. apply S2u_cent_agu_Bob. assumption. Qed.