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)

Global Index

A

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]
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]


B

betterFor [definition, 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]


C

Choice [inductive, 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]


D

dolAcBc [definition, 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]


E

Existence_s2u [lemma, in infinite_extensive_games]
existence_then_LeadsToLeaf [lemma, in infinite_extensive_games]


F

f [constructor, 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]


G

Game [inductive, 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]


H

hasInfiniteHistory [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]


I

IndAgentConv [inductive, 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]


L

l [constructor, 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]


N

NashEq [definition, 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]


R

r [constructor, in infinite_extensive_games]


S

sBisimilar [inductive, in infinite_extensive_games]
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]


T

T_for_Always [lemma, in infinite_extensive_games]


U

uf_of_h_in_g [inductive, in infinite_extensive_games]
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

Variant_Uniqueness_s2u [lemma, in infinite_extensive_games]
v_pos [axiom, in dollar_auction]



Axiom Index

V

v_pos [in dollar_auction]



Lemma Index

A

ALtLBis [in infinite_extensive_games]
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]


B

BisStratProf_leaf [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]


C

CoIndConvRefl [in infinite_extensive_games]
CoIndConvSameGame [in infinite_extensive_games]
ConvRefl [in infinite_extensive_games]
conv_dolAsBs [in dollar_auction]


D

dolAcBc_decomposition [in dollar_auction]
dolAcBs_decomposition [in dollar_auction]
dolAsBc_decomposition [in dollar_auction]
dolAsBs_decomposition [in dollar_auction]


E

Existence_s2u [in infinite_extensive_games]
existence_then_LeadsToLeaf [in infinite_extensive_games]


F

Finite_notInfinite [in infinite_extensive_games]


G

Game_decomposition [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]


H

hasInfiniteHistory_NotFinite [in infinite_extensive_games]
hasInfiniteHistory_then_not_LeadsToLeaf [in infinite_extensive_games]
History_decomposition [in infinite_extensive_games]


I

IndConvBisAndConvThenConv [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]


L

LeadsToLeaf_dolAcBs [in dollar_auction]
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]


N

NeverLeaf_AcBc [in dollar_auction]
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]


S

SGPE_dol_Ac_Bs [in dollar_auction]
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]


T

T_for_Always [in infinite_extensive_games]


U

Uniqueness_s2u [in infinite_extensive_games]


V

Variant_Uniqueness_s2u [in infinite_extensive_games]



Constructor Index

A

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]
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]


B

bisim_gLeaf [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]


C

ConvAgent [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

f [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]


G

gLeaf [in infinite_extensive_games]
gNode [in infinite_extensive_games]
goL [in infinite_extensive_games]
goR [in infinite_extensive_games]


H

HCons [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]


I

InfHistLeft [in infinite_extensive_games]
InfHistRight [in infinite_extensive_games]


L

l [in infinite_extensive_games]
LtLLeaf [in infinite_extensive_games]
LtLLeft [in infinite_extensive_games]
LtLRight [in infinite_extensive_games]


N

NvLLeft [in dollar_auction]
NvLRight [in dollar_auction]


R

r [in infinite_extensive_games]


S

SGPE_leaf [in infinite_extensive_games]
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]


U

uhgLeaf [in infinite_extensive_games]
uhgLeft [in infinite_extensive_games]
uhgRight [in infinite_extensive_games]



Inductive Index

A

Alice_Bob [in dollar_auction]
Always [in infinite_extensive_games]
AlwLeadsToLeaf [in infinite_extensive_games]


B

BisStratProf [in infinite_extensive_games]


C

Choice [in infinite_extensive_games]
CoIndAgentConv [in infinite_extensive_games]


F

FiniteGame [in infinite_extensive_games]
FiniteStrat [in infinite_extensive_games]


G

Game [in infinite_extensive_games]
gBisimilar [in infinite_extensive_games]
GoToLeft [in infinite_extensive_games]
GoToRight [in infinite_extensive_games]


H

hasInfiniteHistory [in infinite_extensive_games]
hBisimilar [in infinite_extensive_games]
History [in infinite_extensive_games]


I

IndAgentConv [in infinite_extensive_games]
IsHistoryOf [in infinite_extensive_games]


L

LeadsToLeaf [in infinite_extensive_games]


N

NeverLeaf [in dollar_auction]


S

sBisimilar [in infinite_extensive_games]
SGPE [in infinite_extensive_games]
StratProf [in infinite_extensive_games]
s2u [in infinite_extensive_games]


U

uf_of_h_in_g [in infinite_extensive_games]



Definition Index

A

add_Alice_Bob_dol [in dollar_auction]


B

betterFor [in infinite_extensive_games]


D

dolAcBc [in dollar_auction]
dolAcBs [in dollar_auction]
dolAsBc [in dollar_auction]
dolAsBs [in dollar_auction]
dolAsBs_0' [in dollar_auction]


G

Game_identity [in infinite_extensive_games]


H

has_an_escalation [in infinite_extensive_games]
has_an_escalation_sequence [in infinite_extensive_games]
History_identity [in infinite_extensive_games]


N

NashEq [in infinite_extensive_games]


S

Strat [in dollar_auction]
StratProf_identity [in infinite_extensive_games]
s2g [in infinite_extensive_games]
s2h [in infinite_extensive_games]


U

Utility_fun [in infinite_extensive_games]



Library Index

D

dollar_auction


I

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