Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (203 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (94 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (65 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (24 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (17 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (2 entries) |

a [constructor, in infinite_extensive_games]

a [constructor, in infinite_extensive_games]

a [constructor, in infinite_extensive_games]

a [constructor, in infinite_extensive_games]

a [constructor, in infinite_extensive_games]

a [constructor, in infinite_extensive_games]

add_Alice_Bob_dol [definition, in dollar_auction]

Alice [constructor, in dollar_auction]

Alice_Bob [inductive, in dollar_auction]

ALtL [constructor, in infinite_extensive_games]

ALtLBis [lemma, in infinite_extensive_games]

ALtLeaf [constructor, in infinite_extensive_games]

ALtLLeft [lemma, in infinite_extensive_games]

ALtLRight [lemma, in infinite_extensive_games]

ALtL_then_LtL [lemma, in infinite_extensive_games]

Always [inductive, in infinite_extensive_games]

AlwaysLeadToLeaf [lemma, in infinite_extensive_games]

AlwLeadsToLeaf [inductive, in infinite_extensive_games]

AlwLeadsToLeaf_dolAcBs [lemma, in dollar_auction]

AlwLeadsToLeaf_dolAsBc [lemma, in dollar_auction]

AlwLeadsToLeaf_dolAsBs [lemma, in dollar_auction]

AlwLeadsToLeaf_Preservation [lemma, in infinite_extensive_games]

AlwsLeaf [constructor, in infinite_extensive_games]

AlwsNode [constructor, in infinite_extensive_games]

bisim_gLeaf [constructor, in infinite_extensive_games]

bisim_gNode [constructor, in infinite_extensive_games]

bisim_HCons [constructor, in infinite_extensive_games]

bisim_HNil [constructor, in infinite_extensive_games]

bisim_sLeaf [constructor, in infinite_extensive_games]

bisim_sNode [constructor, in infinite_extensive_games]

BisStratProf [inductive, in infinite_extensive_games]

BisStratProf_leaf [lemma, in infinite_extensive_games]

BisStratProf_node_not_leaf [lemma, in infinite_extensive_games]

BisStratProf_refl [lemma, in infinite_extensive_games]

BisStratProf_revLeft [lemma, in infinite_extensive_games]

BisStratProf_revRight [lemma, in infinite_extensive_games]

BisStratProf_same_choice [lemma, in infinite_extensive_games]

BisStratProf_same_head [lemma, in infinite_extensive_games]

BisStratProf_sim [lemma, in infinite_extensive_games]

BisStratProf_then_Biss2g [lemma, in infinite_extensive_games]

BisStratProf_trans [lemma, in infinite_extensive_games]

BisThenCoConv [lemma, in infinite_extensive_games]

Bob [constructor, in dollar_auction]

BSLeaf [constructor, in infinite_extensive_games]

BSNode [constructor, in infinite_extensive_games]

CoIndAgentConv [inductive, in infinite_extensive_games]

CoIndConvRefl [lemma, in infinite_extensive_games]

CoIndConvSameGame [lemma, in infinite_extensive_games]

ConvAgent [constructor, in infinite_extensive_games]

ConvAgentCo [constructor, in infinite_extensive_games]

ConvBis [constructor, in infinite_extensive_games]

ConvChoice [constructor, in infinite_extensive_games]

ConvChoiceCo [constructor, in infinite_extensive_games]

ConvLeafCo [constructor, in infinite_extensive_games]

ConvRefl [lemma, in infinite_extensive_games]

conv_dolAsBs [lemma, in dollar_auction]

dolAcBc_decomposition [lemma, in dollar_auction]

dolAcBs [definition, in dollar_auction]

dolAcBs_decomposition [lemma, in dollar_auction]

dolAsBc [definition, in dollar_auction]

dolAsBc_decomposition [lemma, in dollar_auction]

dolAsBs [definition, in dollar_auction]

dolAsBs_decomposition [lemma, in dollar_auction]

dolAsBs_0' [definition, in dollar_auction]

dollar_auction [library]

existence_then_LeadsToLeaf [lemma, in infinite_extensive_games]

f [constructor, in infinite_extensive_games]

f [constructor, in infinite_extensive_games]

f [constructor, in infinite_extensive_games]

f [constructor, in infinite_extensive_games]

FiniteGame [inductive, in infinite_extensive_games]

FiniteStrat [inductive, in infinite_extensive_games]

Finite_notInfinite [lemma, in infinite_extensive_games]

Fin_gLeaf [constructor, in infinite_extensive_games]

Fin_gNode [constructor, in infinite_extensive_games]

Fin_sLeaf [constructor, in infinite_extensive_games]

Fin_sNode [constructor, in infinite_extensive_games]

Game_decomposition [lemma, in infinite_extensive_games]

Game_identity [definition, in infinite_extensive_games]

Game_Left [lemma, in infinite_extensive_games]

Game_Right [lemma, in infinite_extensive_games]

gBisimilar [inductive, in infinite_extensive_games]

gBis_refl [lemma, in infinite_extensive_games]

gBis_sym [lemma, in infinite_extensive_games]

gLeaf [constructor, in infinite_extensive_games]

gNode [constructor, in infinite_extensive_games]

goL [constructor, in infinite_extensive_games]

goR [constructor, in infinite_extensive_games]

GoToLeft [inductive, in infinite_extensive_games]

GoToRight [inductive, in infinite_extensive_games]

hasInfiniteHistory_NotFinite [lemma, in infinite_extensive_games]

hasInfiniteHistory_then_not_LeadsToLeaf [lemma, in infinite_extensive_games]

has_an_escalation [definition, in infinite_extensive_games]

has_an_escalation_sequence [definition, in infinite_extensive_games]

hBisimilar [inductive, in infinite_extensive_games]

HCons [constructor, in infinite_extensive_games]

History [inductive, in infinite_extensive_games]

History_decomposition [lemma, in infinite_extensive_games]

History_identity [definition, in infinite_extensive_games]

hist_Leaf [constructor, in infinite_extensive_games]

hist_NodeLeft [constructor, in infinite_extensive_games]

hist_NodeRight [constructor, in infinite_extensive_games]

HNil [constructor, in infinite_extensive_games]

IndConvBisAndConvThenConv [lemma, in infinite_extensive_games]

IndConvLeaf [lemma, in infinite_extensive_games]

IndConvProjL [lemma, in infinite_extensive_games]

IndConvProjR [lemma, in infinite_extensive_games]

IndConvSameHeadAgent [lemma, in infinite_extensive_games]

IndConvSym [lemma, in infinite_extensive_games]

IndConvTrans [lemma, in infinite_extensive_games]

IndConv_node_not_leaf [lemma, in infinite_extensive_games]

IndConv_then_CoIndConv [lemma, in infinite_extensive_games]

InfConvSameAgent1 [lemma, in infinite_extensive_games]

InfConvSameAgent2 [lemma, in infinite_extensive_games]

InfHistLeft [constructor, in infinite_extensive_games]

InfHistRight [constructor, in infinite_extensive_games]

infinite_extensive_games [library]

IsHistoryOf [inductive, in infinite_extensive_games]

LeadsToLeaf [inductive, in infinite_extensive_games]

LeadsToLeaf_dolAcBs [lemma, in dollar_auction]

LeadsToLeaf_dolAsBc [lemma, in dollar_auction]

LeadsToLeaf_dolAsBs [lemma, in dollar_auction]

LeadsToLeaf_dolAsBs_0' [lemma, in dollar_auction]

LeadsToLeaf_then_not_hasInfiniteHistory [lemma, in infinite_extensive_games]

LtLLeaf [constructor, in infinite_extensive_games]

LtLLeft [constructor, in infinite_extensive_games]

LtLRight [constructor, in infinite_extensive_games]

LtL_Bis [lemma, in infinite_extensive_games]

LtL_revLeft [lemma, in infinite_extensive_games]

LtL_revRight [lemma, in infinite_extensive_games]

NeverLeaf [inductive, in dollar_auction]

NeverLeaf_AcBc [lemma, in dollar_auction]

NeverLeaf_then_not_LeadsToLeaf [lemma, in dollar_auction]

NLLeft [lemma, in dollar_auction]

NLRight [lemma, in dollar_auction]

NotSGPE_dolAcBc [lemma, in dollar_auction]

NotSGPE_dolAsBs [lemma, in dollar_auction]

Not_LeadsToLeaf_AcBc [lemma, in dollar_auction]

not_LeadsToLeaf_then_hasInfiniteHistory [lemma, in infinite_extensive_games]

NvLLeft [constructor, in dollar_auction]

NvLRight [constructor, in dollar_auction]

SGPE [inductive, in infinite_extensive_games]

SGPE_dol_Ac_Bs [lemma, in dollar_auction]

SGPE_dol_As_Bc [lemma, in dollar_auction]

SGPE_implies_BetterFor [lemma, in infinite_extensive_games]

SGPE_Implies_NashEq [lemma, in infinite_extensive_games]

SGPE_leaf [constructor, in infinite_extensive_games]

SGPE_left [constructor, in infinite_extensive_games]

SGPE_rev_Left [lemma, in infinite_extensive_games]

SGPE_rev_Right [lemma, in infinite_extensive_games]

SGPE_right [constructor, in infinite_extensive_games]

SGPE_then_AlwLeadsToLeaf [lemma, in infinite_extensive_games]

SGPE_then_LtL [lemma, in infinite_extensive_games]

SGPE_then_SubStrat_SGPE [lemma, in infinite_extensive_games]

sLeaf [constructor, in infinite_extensive_games]

sNode [constructor, in infinite_extensive_games]

Strat [definition, in dollar_auction]

StratProf [inductive, in infinite_extensive_games]

StratProf_decomposition [lemma, in infinite_extensive_games]

StratProf_identity [definition, in infinite_extensive_games]

StratProf_Leaf [lemma, in infinite_extensive_games]

StratProf_Left [lemma, in infinite_extensive_games]

StratProf_Right [lemma, in infinite_extensive_games]

s2g [definition, in infinite_extensive_games]

s2g_decomp [lemma, in infinite_extensive_games]

s2g_leaf [lemma, in infinite_extensive_games]

s2h [definition, in infinite_extensive_games]

s2h_and_g [lemma, in infinite_extensive_games]

s2u [inductive, in infinite_extensive_games]

s2uLeaf [constructor, in infinite_extensive_games]

s2uLeft [constructor, in infinite_extensive_games]

s2uLeft_rev [lemma, in infinite_extensive_games]

s2uRight [constructor, in infinite_extensive_games]

s2uRight_rev [lemma, in infinite_extensive_games]

S2u_dolAcBs_Alice [lemma, in dollar_auction]

S2u_dolAcBs_Bob [lemma, in dollar_auction]

S2u_dolAsBc_Alice [lemma, in dollar_auction]

S2u_dolAsBc_Bob [lemma, in dollar_auction]

S2u_dolAsBs_Alice [lemma, in dollar_auction]

S2u_dolAsBs_Bob [lemma, in dollar_auction]

S2u_dolAsBs_0'_Alice [lemma, in dollar_auction]

uhgLeaf [constructor, in infinite_extensive_games]

uhgLeft [constructor, in infinite_extensive_games]

uhgRight [constructor, in infinite_extensive_games]

Uniqueness_s2u [lemma, in infinite_extensive_games]

Utility_fun [definition, in infinite_extensive_games]

v_pos [axiom, in dollar_auction]

ALtLLeft [in infinite_extensive_games]

ALtLRight [in infinite_extensive_games]

ALtL_then_LtL [in infinite_extensive_games]

AlwaysLeadToLeaf [in infinite_extensive_games]

AlwLeadsToLeaf_dolAcBs [in dollar_auction]

AlwLeadsToLeaf_dolAsBc [in dollar_auction]

AlwLeadsToLeaf_dolAsBs [in dollar_auction]

AlwLeadsToLeaf_Preservation [in infinite_extensive_games]

BisStratProf_node_not_leaf [in infinite_extensive_games]

BisStratProf_refl [in infinite_extensive_games]

BisStratProf_revLeft [in infinite_extensive_games]

BisStratProf_revRight [in infinite_extensive_games]

BisStratProf_same_choice [in infinite_extensive_games]

BisStratProf_same_head [in infinite_extensive_games]

BisStratProf_sim [in infinite_extensive_games]

BisStratProf_then_Biss2g [in infinite_extensive_games]

BisStratProf_trans [in infinite_extensive_games]

BisThenCoConv [in infinite_extensive_games]

CoIndConvSameGame [in infinite_extensive_games]

ConvRefl [in infinite_extensive_games]

conv_dolAsBs [in dollar_auction]

dolAcBs_decomposition [in dollar_auction]

dolAsBc_decomposition [in dollar_auction]

dolAsBs_decomposition [in dollar_auction]

existence_then_LeadsToLeaf [in infinite_extensive_games]

Game_Left [in infinite_extensive_games]

Game_Right [in infinite_extensive_games]

gBis_refl [in infinite_extensive_games]

gBis_sym [in infinite_extensive_games]

hasInfiniteHistory_then_not_LeadsToLeaf [in infinite_extensive_games]

History_decomposition [in infinite_extensive_games]

IndConvLeaf [in infinite_extensive_games]

IndConvProjL [in infinite_extensive_games]

IndConvProjR [in infinite_extensive_games]

IndConvSameHeadAgent [in infinite_extensive_games]

IndConvSym [in infinite_extensive_games]

IndConvTrans [in infinite_extensive_games]

IndConv_node_not_leaf [in infinite_extensive_games]

IndConv_then_CoIndConv [in infinite_extensive_games]

InfConvSameAgent1 [in infinite_extensive_games]

InfConvSameAgent2 [in infinite_extensive_games]

LeadsToLeaf_dolAsBc [in dollar_auction]

LeadsToLeaf_dolAsBs [in dollar_auction]

LeadsToLeaf_dolAsBs_0' [in dollar_auction]

LeadsToLeaf_then_not_hasInfiniteHistory [in infinite_extensive_games]

LtL_Bis [in infinite_extensive_games]

LtL_revLeft [in infinite_extensive_games]

LtL_revRight [in infinite_extensive_games]

NeverLeaf_then_not_LeadsToLeaf [in dollar_auction]

NLLeft [in dollar_auction]

NLRight [in dollar_auction]

NotSGPE_dolAcBc [in dollar_auction]

NotSGPE_dolAsBs [in dollar_auction]

Not_LeadsToLeaf_AcBc [in dollar_auction]

not_LeadsToLeaf_then_hasInfiniteHistory [in infinite_extensive_games]

SGPE_dol_As_Bc [in dollar_auction]

SGPE_implies_BetterFor [in infinite_extensive_games]

SGPE_Implies_NashEq [in infinite_extensive_games]

SGPE_rev_Left [in infinite_extensive_games]

SGPE_rev_Right [in infinite_extensive_games]

SGPE_then_AlwLeadsToLeaf [in infinite_extensive_games]

SGPE_then_LtL [in infinite_extensive_games]

SGPE_then_SubStrat_SGPE [in infinite_extensive_games]

StratProf_decomposition [in infinite_extensive_games]

StratProf_Leaf [in infinite_extensive_games]

StratProf_Left [in infinite_extensive_games]

StratProf_Right [in infinite_extensive_games]

s2g_decomp [in infinite_extensive_games]

s2g_leaf [in infinite_extensive_games]

s2h_and_g [in infinite_extensive_games]

s2uLeft_rev [in infinite_extensive_games]

s2uRight_rev [in infinite_extensive_games]

S2u_dolAcBs_Alice [in dollar_auction]

S2u_dolAcBs_Bob [in dollar_auction]

S2u_dolAsBc_Alice [in dollar_auction]

S2u_dolAsBc_Bob [in dollar_auction]

S2u_dolAsBs_Alice [in dollar_auction]

S2u_dolAsBs_Bob [in dollar_auction]

S2u_dolAsBs_0'_Alice [in dollar_auction]

a [in infinite_extensive_games]

a [in infinite_extensive_games]

a [in infinite_extensive_games]

a [in infinite_extensive_games]

a [in infinite_extensive_games]

a [in infinite_extensive_games]

Alice [in dollar_auction]

ALtL [in infinite_extensive_games]

ALtLeaf [in infinite_extensive_games]

AlwsLeaf [in infinite_extensive_games]

AlwsNode [in infinite_extensive_games]

bisim_gNode [in infinite_extensive_games]

bisim_HCons [in infinite_extensive_games]

bisim_HNil [in infinite_extensive_games]

bisim_sLeaf [in infinite_extensive_games]

bisim_sNode [in infinite_extensive_games]

Bob [in dollar_auction]

BSLeaf [in infinite_extensive_games]

BSNode [in infinite_extensive_games]

ConvAgentCo [in infinite_extensive_games]

ConvBis [in infinite_extensive_games]

ConvChoice [in infinite_extensive_games]

ConvChoiceCo [in infinite_extensive_games]

ConvLeafCo [in infinite_extensive_games]

f [in infinite_extensive_games]

f [in infinite_extensive_games]

f [in infinite_extensive_games]

f [in infinite_extensive_games]

Fin_gLeaf [in infinite_extensive_games]

Fin_gNode [in infinite_extensive_games]

Fin_sLeaf [in infinite_extensive_games]

Fin_sNode [in infinite_extensive_games]

gNode [in infinite_extensive_games]

goL [in infinite_extensive_games]

goR [in infinite_extensive_games]

hist_Leaf [in infinite_extensive_games]

hist_NodeLeft [in infinite_extensive_games]

hist_NodeRight [in infinite_extensive_games]

HNil [in infinite_extensive_games]

InfHistRight [in infinite_extensive_games]

LtLLeaf [in infinite_extensive_games]

LtLLeft [in infinite_extensive_games]

LtLRight [in infinite_extensive_games]

NvLRight [in dollar_auction]

SGPE_left [in infinite_extensive_games]

SGPE_right [in infinite_extensive_games]

sLeaf [in infinite_extensive_games]

sNode [in infinite_extensive_games]

s2uLeaf [in infinite_extensive_games]

s2uLeft [in infinite_extensive_games]

s2uRight [in infinite_extensive_games]

uhgLeft [in infinite_extensive_games]

uhgRight [in infinite_extensive_games]

Always [in infinite_extensive_games]

AlwLeadsToLeaf [in infinite_extensive_games]

CoIndAgentConv [in infinite_extensive_games]

FiniteStrat [in infinite_extensive_games]

gBisimilar [in infinite_extensive_games]

GoToLeft [in infinite_extensive_games]

GoToRight [in infinite_extensive_games]

hBisimilar [in infinite_extensive_games]

History [in infinite_extensive_games]

IsHistoryOf [in infinite_extensive_games]

SGPE [in infinite_extensive_games]

StratProf [in infinite_extensive_games]

s2u [in infinite_extensive_games]

dolAcBs [in dollar_auction]

dolAsBc [in dollar_auction]

dolAsBs [in dollar_auction]

dolAsBs_0' [in dollar_auction]

has_an_escalation_sequence [in infinite_extensive_games]

History_identity [in infinite_extensive_games]

StratProf_identity [in infinite_extensive_games]

s2g [in infinite_extensive_games]

s2h [in infinite_extensive_games]

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (203 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1 entry) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (94 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (65 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (24 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (17 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (2 entries) |

This page has been generated by coqdoc