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 _ other (628 entries)
Projection 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 _ other (32 entries)
Record 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 _ other (4 entries)
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 _ other (247 entries)
Section 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 _ other (25 entries)
Notation 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 _ other (19 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 _ other (58 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 _ other (15 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 _ other (176 entries)
Variable 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 _ other (45 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 _ other (7 entries)

Global Index

A

AF [inductive, in UB]
AFb [projection, in UB]
afb [definition, in UB]
AFbP [projection, in UB]
afbP [lemma, in UB]
AFb_ext [lemma, in UB]
AFs [constructor, in UB]
AF_ext [lemma, in UB]
AF_step [lemma, in UB]
AF_ [constructor, in UB]
AF0 [constructor, in UB]
AG [inductive, in Kstar]
AG [inductive, in UB]
AG [inductive, in Hstar]
AGb [definition, in Kstar]
AGb [definition, in Hstar]
AGb [definition, in UB]
AGb_ext [lemma, in Hstar]
AGb_ext [lemma, in Kstar]
AGC [lemma, in Kstar]
AGC [lemma, in Hstar]
AGP [lemma, in Hstar]
AGP [lemma, in UB]
AGP [lemma, in Kstar]
AGP_aux [lemma, in Kstar]
AGP_aux [lemma, in UB]
AGP_aux [lemma, in Hstar]
AGs [constructor, in UB]
AGs [constructor, in Hstar]
AGs [constructor, in Kstar]
AG_ [constructor, in UB]
alls [definition, in Kstar_strong]
allsP [lemma, in Kstar_strong]
And [constructor, in Hstar]
And [constructor, in Kstar]
And [constructor, in Kstar_strong]
And [constructor, in P]
AND_ [constructor, in UB]
AX [definition, in Kstar]
AX [definition, in UB]
AX [definition, in Hstar]
AXb [definition, in Kstar]
AXb [definition, in UB]
AXb [definition, in Hstar]
AXb_ext [lemma, in Hstar]
AXb_ext [lemma, in Kstar]
AXP [lemma, in UB]
AXP [lemma, in Hstar]
AXP [lemma, in Kstar]
AX_ [constructor, in UB]


B

base [library]
Box [constructor, in Kstar_strong]
Box [constructor, in Hstar]
Box [constructor, in Kstar]
Bstar [constructor, in Kstar_strong]
Bstar [constructor, in Hstar]
Bstar [constructor, in Kstar]
bstar_trans [lemma, in Kstar_strong]
Bstar_Box [lemma, in Kstar_strong]


C

cardSmC [lemma, in base]
cards_leq1P [lemma, in base]
Characterizations [section, in Kstar]
Characterizations [section, in Hstar]
Characterizations [section, in UB]
Characterizations.e [variable, in UB]
Characterizations.R [variable, in Hstar]
Characterizations.R [variable, in Kstar]
Characterizations.X [variable, in Hstar]
Characterizations.X [variable, in Kstar]
Characterizations.X [variable, in UB]
classicb [lemma, in base]
classicF [lemma, in base]
connectP' [lemma, in base]
connectTR_transD [lemma, in Kstar_strong]
connect_TR_S [lemma, in Kstar]
connect_TR_S [lemma, in Hstar]
contra' [lemma, in base]


D

D [definition, in Kstar_strong]
Ddc_unsat [lemma, in Kstar]
Ddc_unsat [lemma, in Hstar]
Ddia [definition, in Kstar]
Ddia [definition, in Hstar]
Ddia [definition, in Kstar_strong]
DdiaNE [lemma, in Hstar]
DdiaNE [lemma, in Kstar]
Ddstar [definition, in Hstar]
Ddstar [definition, in Kstar]
Ddstar [definition, in Kstar_strong]
DdstarNE [lemma, in Hstar]
DdstarNE [lemma, in Kstar]
decidability [lemma, in Hstar]
decidability [lemma, in Kstar]
decidability [lemma, in P]
decidability [lemma, in Kstar_strong]
decidable [definition, in base]
decidable_reflect [lemma, in base]
decidable2 [definition, in base]
dec_sat_val [lemma, in Kstar]
dec_valid2equiv [lemma, in P]
dec_sat2valid [lemma, in P]
dec_sat_val [lemma, in Hstar]
dec_sat_val [lemma, in Kstar_strong]
default [definition, in Hstar]
Delta [definition, in Kstar]
demo [definition, in Kstar_strong]
demo [definition, in Kstar]
demo [definition, in Hstar]
demoD [lemma, in Kstar_strong]
deMorganAb [lemma, in base]
deMorganb [lemma, in base]
deMorganE [lemma, in base]
deMorganE2 [lemma, in base]
demo_theorem [lemma, in Hstar]
demo_Delta [lemma, in Kstar]
demo_theorem [lemma, in Kstar]
Dia [constructor, in Hstar]
Dia [constructor, in Kstar]
Dia [constructor, in Kstar_strong]
dnb [lemma, in base]
Drc_unsat [lemma, in Kstar]
Drc_unsat [lemma, in Hstar]
Dstar [constructor, in Hstar]
Dstar [constructor, in Kstar]
Dstar [constructor, in Kstar_strong]
Dstar_Dia [lemma, in Kstar_strong]
Dualities [section, in UB]
Dualities.M [variable, in UB]
Dxc [definition, in Hstar]
Dxe [definition, in Hstar]


E

EF [inductive, in Hstar]
EF [inductive, in Kstar]
EF [inductive, in UB]
efb [definition, in Hstar]
efb [definition, in UB]
efb [definition, in Kstar]
EFb [projection, in UB]
EFb [projection, in Kstar]
EFb [projection, in Hstar]
efbP [lemma, in UB]
efbP [lemma, in Kstar]
EFbP [projection, in UB]
EFbP [projection, in Kstar]
EFbP [projection, in Hstar]
efbP [lemma, in Hstar]
EFb_ext [lemma, in UB]
EFb_ext [lemma, in Kstar]
EFb_ext [lemma, in Hstar]
EFC [lemma, in Hstar]
EFC [lemma, in Kstar]
EFs [constructor, in Hstar]
EFs [constructor, in UB]
EFs [constructor, in Kstar]
EF_ [constructor, in UB]
EF_ext [lemma, in UB]
EF_step [lemma, in Hstar]
EF_step [lemma, in UB]
EF_ext [lemma, in Hstar]
EF_step [lemma, in Kstar]
EF_ext [lemma, in Kstar]
EF0 [constructor, in Hstar]
EF0 [constructor, in UB]
EF0 [constructor, in Kstar]
EG [inductive, in UB]
EGb [definition, in UB]
EGP [lemma, in UB]
EGP_aux [lemma, in UB]
EGs [constructor, in UB]
EG_ [constructor, in UB]
equic_dec [lemma, in P]
equiv [definition, in Kstar_strong]
equiv [definition, in Kstar]
equiv [definition, in Hstar]
equiv [definition, in P]
equiv_valid [lemma, in Kstar]
equiv_valid [lemma, in Hstar]
equiv_dec [lemma, in Kstar_strong]
equiv_sat_valid [lemma, in P]
equiv_dec [lemma, in Hstar]
equiv_valid [lemma, in Kstar_strong]
equiv_valid [lemma, in P]
equiv_dec [lemma, in Kstar]
eq_form_dec [lemma, in P]
eq_form_dec [lemma, in Hstar]
eq_form_dec [lemma, in Kstar_strong]
eq_form_dec [lemma, in Kstar]
eval [definition, in UB]
eval [definition, in P]
eval [definition, in Kstar_strong]
eval [definition, in Hstar]
eval [definition, in Kstar]
eval_Neg [lemma, in P]
eval_Neg [lemma, in Hstar]
eval_Neg [lemma, in Kstar]
eval_Neg [lemma, in Kstar_strong]
EX [definition, in Hstar]
EX [definition, in Kstar]
EX [definition, in UB]
EXb [projection, in Kstar]
EXb [projection, in Hstar]
exb [definition, in Hstar]
exb [definition, in Kstar]
EXb [projection, in UB]
exb [definition, in UB]
EXbP [projection, in Hstar]
exbP [lemma, in Hstar]
exbP [lemma, in Kstar]
exbP [lemma, in UB]
EXbP [projection, in UB]
EXbP [projection, in Kstar]
EXb_ext [lemma, in Kstar]
EXb_ext [lemma, in Hstar]
EXb_ext [lemma, in UB]
exsD [definition, in Kstar_strong]
exsP [projection, in Kstar_strong]
exsPD [definition, in Kstar_strong]
exs' [projection, in Kstar_strong]
extension [lemma, in Kstar]
extension [lemma, in Hstar]
EX_ [constructor, in UB]
EX_ext [lemma, in Hstar]
EX_ext [lemma, in UB]
EX_ext [lemma, in Kstar]
ex2E [lemma, in base]


F

F [definition, in Hstar]
F [definition, in Kstar_strong]
F [definition, in UB]
F [definition, in P]
F [definition, in Kstar]
FiniteModel [section, in Hstar]
FiniteModel [section, in UB]
FiniteModel [section, in Kstar]
FiniteModel.e [variable, in Hstar]
FiniteModel.e [variable, in Kstar]
FiniteModel.e [variable, in UB]
FiniteModel.label [variable, in Kstar]
FiniteModel.label [variable, in Hstar]
FiniteModel.label [variable, in UB]
FiniteModel.p [variable, in UB]
FiniteModel.T [variable, in Kstar]
FiniteModel.T [variable, in UB]
FiniteModel.T [variable, in Hstar]
finset [section, in base]
finset.T [variable, in base]
finset.xs [variable, in base]
fin_choice_aux [lemma, in base]
fin_choice [lemma, in base]
FixPoint [section, in base]
FixPoint.F [variable, in base]
FixPoint.monoF [variable, in base]
FixPoint.T [variable, in base]
form [inductive, in Hstar]
form [inductive, in Kstar]
form [inductive, in P]
form [inductive, in Kstar_strong]
form [inductive, in UB]
FormulaUniverse [section, in Kstar_strong]
FormulaUniverse [section, in Hstar]
FormulaUniverse [section, in P]
FormulaUniverse [section, in Kstar]
FormulaUniverse.ModelExistence [section, in Hstar]
FormulaUniverse.ModelExistence [section, in Kstar_strong]
FormulaUniverse.ModelExistence [section, in Kstar]
FormulaUniverse.ModelExistence.D [variable, in Hstar]
FormulaUniverse.ModelExistence.D [variable, in Kstar_strong]
FormulaUniverse.ModelExistence.D [variable, in Kstar]
FormulaUniverse.ModelExistence.demoD [variable, in Hstar]
FormulaUniverse.ModelExistence.demoD [variable, in Kstar_strong]
FormulaUniverse.ModelExistence.demoD [variable, in Kstar]
FormulaUniverse.s [variable, in Hstar]
FormulaUniverse.s [variable, in Kstar_strong]
FormulaUniverse.s [variable, in P]
FormulaUniverse.s [variable, in Kstar]
FormulaUniverse.SmallModelTheorem [section, in Kstar]
FormulaUniverse.SmallModelTheorem [section, in Hstar]
FormulaUniverse.SmallModelTheorem [section, in Kstar_strong]
FormulaUniverse.SmallModelTheorem.PruningInvariant [section, in Hstar]
FormulaUniverse.SmallModelTheorem.PruningInvariant.M [variable, in Hstar]
_ |== _ [notation, in Kstar]
_ |== _ [notation, in Hstar]
form_CountType [definition, in P]
form_ChoiceType [definition, in P]
form_eqType [definition, in P]
form_CountType [definition, in Hstar]
form_ChoiceType [definition, in Hstar]
form_eqType [definition, in Hstar]
form_choiceMixin [definition, in P]
form_eqMixin [definition, in Hstar]
form_eqMixin [definition, in Kstar]
form_countMixin [definition, in Kstar_strong]
form_CountType [definition, in Kstar]
form_ChoiceType [definition, in Kstar]
form_eqType [definition, in Kstar]
form_choiceMixin [definition, in Kstar]
form_choiceMixin [definition, in Kstar_strong]
form_eqMixin [definition, in P]
form_countMixin [definition, in Hstar]
form_eqMixin [definition, in Kstar_strong]
form_countMixin [definition, in P]
form_countMixin [definition, in Kstar]
form_CountType [definition, in Kstar_strong]
form_ChoiceType [definition, in Kstar_strong]
form_eqType [definition, in Kstar_strong]
form_choiceMixin [definition, in Hstar]


G

guess [lemma, in Hstar]
guess_S [lemma, in Hstar]


H

HC [lemma, in Hstar]
HC [lemma, in Kstar]
HC [lemma, in Kstar_strong]
Hcond [definition, in P]
Hcond [definition, in Hstar]
Hcond [definition, in Kstar_strong]
Hcond [definition, in Kstar]
hintikka [definition, in Hstar]
hintikka [definition, in P]
hintikka [definition, in Kstar_strong]
hintikka [definition, in Kstar]
hintikkaD [lemma, in Hstar]
hintikkaD [lemma, in Kstar]
hintikkaD [lemma, in Kstar_strong]
Hstar [library]
HU [definition, in Hstar]
HU [definition, in Kstar]
HU [definition, in Kstar_strong]
H_at_hintikka [lemma, in Kstar]
H_at_hintikka [lemma, in Hstar]
H_at_hintikka [lemma, in Kstar_strong]
H_at [definition, in Kstar_strong]
H_at_sat [lemma, in Kstar]
H_at_sat [lemma, in Hstar]
H_at_collapse [lemma, in Hstar]
H_at [definition, in Kstar]
H_at [definition, in Hstar]


I

iffP' [lemma, in base]
introP' [lemma, in base]
inv [lemma, in Hstar]
inv [lemma, in P]
inv [lemma, in Kstar_strong]
inv [lemma, in Kstar]
invariant [definition, in Kstar]
invariant [definition, in Hstar]
invariantHU [lemma, in Kstar]
invariant_prune [lemma, in Kstar]
invariant_demo [lemma, in Kstar]
invariant_step [lemma, in Hstar]
invariant_prune [lemma, in Hstar]
invariant_Dxe [lemma, in Hstar]
invariant_demo [lemma, in Hstar]
invariant_step [lemma, in Kstar]
inv_sub [lemma, in Kstar]
inv_H_at [lemma, in Kstar]
inv_H_at [lemma, in Hstar]
inv_sub [lemma, in Hstar]
iterFsub [lemma, in base]
iterFsubn [lemma, in base]
iter_fix [lemma, in base]


K

Kstar [library]
Kstar_strong [library]


L

label [projection, in UB]
label [projection, in Kstar_strong]
label [projection, in Kstar]
label [projection, in Hstar]
labelD [definition, in Kstar]
labelD [definition, in Hstar]
labelD [definition, in Kstar_strong]
leq1 [lemma, in base]
ltn_leq_trans [lemma, in base]


M

maximal [definition, in Hstar]
MD [definition, in Kstar]
MD [definition, in Kstar_strong]
MD [definition, in Hstar]
model [record, in UB]
Model [constructor, in Kstar]
Model [constructor, in Hstar]
model [record, in Kstar]
Model [constructor, in Kstar_strong]
model [record, in Hstar]
Model [constructor, in UB]
model [record, in Kstar_strong]
model [definition, in P]
Models [section, in Hstar]
Models [section, in Kstar]
Models.M [variable, in Hstar]
Models.M [variable, in Kstar]
model_MD_aux [lemma, in Kstar_strong]
model_existence [lemma, in Kstar_strong]
model_MD_aux [lemma, in Kstar]
model_existence [lemma, in P]
model_existence [lemma, in Hstar]
model_existence [lemma, in Kstar]
model_MD_aux [lemma, in Hstar]
mono [definition, in base]
monoF [lemma, in UB]
msval [definition, in base]
msvalE [lemma, in base]
msvalP [lemma, in base]
mu [definition, in base]
muE [lemma, in base]
mu_ind [lemma, in base]


N

N [definition, in Hstar]
nedb_egb [lemma, in UB]
Neg [definition, in P]
Neg [definition, in Kstar_strong]
Neg [definition, in Kstar]
Neg [definition, in Hstar]
negb_EXb [lemma, in Hstar]
negb_AXb [lemma, in UB]
negb_EXb [lemma, in Kstar]
negb_AXb [lemma, in Hstar]
negb_EXb [lemma, in UB]
negb_AXb [lemma, in Kstar]
negb_AGb [lemma, in Hstar]
negb_afb [lemma, in UB]
negb_AGb [lemma, in Kstar]
negb_efb [lemma, in UB]
negb_agb [lemma, in UB]
negb_EFb [lemma, in Hstar]
negb_EFb [lemma, in Kstar]
NegNom [constructor, in Hstar]
NegVar [constructor, in Kstar_strong]
NegVar [constructor, in Hstar]
NegVar [constructor, in Kstar]
NegVar [constructor, in P]
Neg_involutive [lemma, in Hstar]
Neg_involutive [lemma, in Kstar]
Neg_involutive [lemma, in P]
Neg_involutive [lemma, in Kstar_strong]
nlabel [projection, in Hstar]
nlabelD [definition, in Hstar]
nlabelP [projection, in Hstar]
nlabelP' [lemma, in Hstar]
Node [constructor, in base]
Nom [constructor, in Hstar]
nominal [definition, in Hstar]
nominalE [lemma, in Hstar]
nominalI [lemma, in Hstar]
norm [inductive, in base]
normEn [lemma, in base]
normI [constructor, in base]
not_ex_all [lemma, in Kstar_strong]
not_all_ex [lemma, in Kstar_strong]
NP_ [constructor, in UB]
nseq [definition, in Hstar]
nseqP [lemma, in Hstar]
nset [definition, in Hstar]
nvar [definition, in Hstar]


O

Or [constructor, in Hstar]
Or [constructor, in Kstar]
Or [constructor, in Kstar_strong]
Or [constructor, in P]
orS [lemma, in base]
OR_ [constructor, in UB]


P

P [library]
parse_pickle_xs [lemma, in base]
path_rcons [lemma, in base]
pickle [definition, in P]
pickle [definition, in Kstar_strong]
pickle [definition, in Kstar]
pickle [definition, in Hstar]
pick_rc [definition, in Hstar]
pick_rcS [lemma, in Hstar]
pick_dcH [lemma, in Hstar]
pick_dc [definition, in Kstar]
pick_dc [definition, in Hstar]
pick_rcH [lemma, in Kstar]
pick_rcH [lemma, in Hstar]
pick_rc [definition, in Kstar]
pick_rcS [lemma, in Kstar]
pick_dcH [lemma, in Kstar]
pick_dcS [lemma, in Kstar]
pick_dcS [lemma, in Hstar]
predC_involutive [lemma, in base]
prune_subset [lemma, in Hstar]
prune_rc [lemma, in Hstar]
prune_dc [lemma, in Kstar]
prune_dc [lemma, in Hstar]
prune_Dxc [lemma, in Hstar]
prune_subset [lemma, in Kstar]
prune_rc [lemma, in Kstar]
P_ [constructor, in UB]


R

reflectPn [lemma, in base]
reflect_DN [lemma, in base]
reflect_decidable [lemma, in base]
request [definition, in Kstar]
request [definition, in Kstar_strong]
request [definition, in Hstar]


S

sat [definition, in Hstar]
sat [definition, in Kstar_strong]
sat [definition, in P]
sat [definition, in Kstar]
satF [definition, in Kstar]
satM [definition, in Hstar]
sat_dec [lemma, in Kstar]
sat_dec [lemma, in Kstar_strong]
sat_dec [lemma, in P]
sat_dec [lemma, in Hstar]
setD1id [lemma, in base]
set_op [definition, in base]
simple_tree_rect [lemma, in base]
small_models [lemma, in P]
small_model_theorem [lemma, in Kstar_strong]
sn [definition, in base]
state [projection, in Kstar_strong]
state [projection, in UB]
state [projection, in Kstar]
state [projection, in Hstar]
stateD [definition, in Kstar]
stateD [definition, in Kstar_strong]
stateD [definition, in Hstar]
stateD_model [definition, in Hstar]
stateD_model [definition, in Kstar]
stateD_model [definition, in Kstar_strong]
step [definition, in Kstar]
step [definition, in Hstar]
step_smaller [lemma, in Kstar]
step_smaller [lemma, in Hstar]
subset_step [lemma, in Kstar]
subset_step [lemma, in Hstar]
synclos [definition, in Hstar]
synclos [definition, in Kstar_strong]
synclos [definition, in P]
synclos [definition, in Kstar]
synclos_nlabelD [lemma, in Hstar]
synclos_refl [lemma, in Kstar]
synclos_trans [lemma, in Kstar]
synclos_trans [lemma, in Kstar_strong]
synclos_refl [lemma, in Kstar_strong]
synclos_refl [lemma, in P]
synclos_refl [lemma, in Hstar]
synclos_trans [lemma, in Hstar]
synclos_trans [lemma, in P]


T

tactics [library]
TR [definition, in Hstar]
TR [definition, in Kstar]
TR [definition, in Kstar_strong]
trans [projection, in Hstar]
trans [projection, in UB]
trans [projection, in Kstar_strong]
trans [projection, in Kstar]
transD [definition, in Kstar]
transD [definition, in Hstar]
transD [definition, in Kstar_strong]
trans_TR [lemma, in Kstar]
trans_star_connect [lemma, in Kstar_strong]
trans_TR [lemma, in Hstar]
trans_starPD [definition, in Kstar_strong]
trans_star_trans [lemma, in Kstar_strong]
trans_star_case [lemma, in Kstar_strong]
trans_starP [projection, in Kstar_strong]
trans_star [projection, in Kstar_strong]
trans_TR [lemma, in Kstar_strong]
trans_star1 [lemma, in Kstar_strong]
trans_star0 [lemma, in Kstar_strong]
trans_starD [definition, in Kstar_strong]
tree [inductive, in base]
TreeCountType [section, in base]
TreeCountType.SimpleTreeInd [section, in base]
TreeCountType.SimpleTreeInd.P [variable, in base]
TreeCountType.SimpleTreeInd.Pcons [variable, in base]
TreeCountType.SimpleTreeInd.Pnil [variable, in base]
TreeCountType.TreeInd [section, in base]
TreeCountType.TreeInd.P [variable, in base]
TreeCountType.TreeInd.Pcons [variable, in base]
TreeCountType.TreeInd.Pnil [variable, in base]
TreeCountType.TreeInd.P' [variable, in base]
TreeCountType.TreeInd.P'cons [variable, in base]
TreeCountType.TreeInd.P'nil [variable, in base]
TreeCountType.X [variable, in base]
tree_CountType [definition, in base]
tree_ChoiceType [definition, in base]
tree_eqType [definition, in base]
tree_countMixin [definition, in base]
tree_choiceMixin [definition, in base]
tree_eqMixin [definition, in base]
tree_eq_dec [lemma, in base]
tree_rect' [lemma, in base]
TR_transD [lemma, in Kstar_strong]
t_unpickle [definition, in base]
t_parse [definition, in base]
t_inv [lemma, in base]
t_pickle [definition, in base]


U

UB [library]
uniq_nseq [lemma, in Hstar]
unpickle [definition, in Kstar_strong]
unpickle [definition, in P]
unpickle [definition, in Kstar]
unpickle [definition, in Hstar]
unsat_inv [lemma, in Hstar]
unsat_not_H_at [lemma, in Hstar]
unsat_inv [lemma, in Kstar]


V

valid [definition, in Kstar]
valid [definition, in P]
valid [definition, in Kstar_strong]
valid [definition, in Hstar]
valid_dec [lemma, in P]
valid_dec [lemma, in Hstar]
valid_dec [lemma, in Kstar_strong]
valid_unsat [lemma, in Kstar]
valid_dec [lemma, in Kstar]
valid_unsat [lemma, in Hstar]
valid_unsat [lemma, in Kstar_strong]
valid_unsat [lemma, in P]
var [definition, in Hstar]
var [definition, in Kstar_strong]
var [definition, in Kstar]
Var [constructor, in Kstar_strong]
var [definition, in P]
Var [constructor, in P]
Var [constructor, in Hstar]
var [definition, in UB]
Var [constructor, in Kstar]


X

xchoose2_sig [definition, in base]


other

exs _ : _ , _ (type_scope) [notation, in Kstar_strong]
_ ---> _ [notation, in Hstar]
_ \in' _ [notation, in base]
_ |= _ [notation, in Hstar]
_ --->* _ [notation, in Kstar_strong]
_ ---> _ [notation, in Kstar_strong]
_ |= _ [notation, in P]
_ ---> _ [notation, in Kstar]
_ ---> _ [notation, in UB]
_ |= _ [notation, in Kstar]
_ |= _ [notation, in Kstar_strong]
alls _ , _ [notation, in Kstar_strong]
exs _ , _ [notation, in Kstar_strong]
[ss _ ; _ ] [notation, in P]
[ss _ ; _ ] [notation, in Kstar_strong]
[ss _ ; _ ] [notation, in Kstar]
[ss _ ; _ ] [notation, in Hstar]



Projection Index

A

AFb [in UB]
AFbP [in UB]


E

EFb [in UB]
EFb [in Kstar]
EFb [in Hstar]
EFbP [in UB]
EFbP [in Kstar]
EFbP [in Hstar]
EXb [in Kstar]
EXb [in Hstar]
EXb [in UB]
EXbP [in Hstar]
EXbP [in UB]
EXbP [in Kstar]
exsP [in Kstar_strong]
exs' [in Kstar_strong]


L

label [in UB]
label [in Kstar_strong]
label [in Kstar]
label [in Hstar]


N

nlabel [in Hstar]
nlabelP [in Hstar]


S

state [in Kstar_strong]
state [in UB]
state [in Kstar]
state [in Hstar]


T

trans [in Hstar]
trans [in UB]
trans [in Kstar_strong]
trans [in Kstar]
trans_starP [in Kstar_strong]
trans_star [in Kstar_strong]



Record Index

M

model [in UB]
model [in Kstar]
model [in Hstar]
model [in Kstar_strong]



Lemma Index

A

afbP [in UB]
AFb_ext [in UB]
AF_ext [in UB]
AF_step [in UB]
AGb_ext [in Hstar]
AGb_ext [in Kstar]
AGC [in Kstar]
AGC [in Hstar]
AGP [in Hstar]
AGP [in UB]
AGP [in Kstar]
AGP_aux [in Kstar]
AGP_aux [in UB]
AGP_aux [in Hstar]
allsP [in Kstar_strong]
AXb_ext [in Hstar]
AXb_ext [in Kstar]
AXP [in UB]
AXP [in Hstar]
AXP [in Kstar]


B

bstar_trans [in Kstar_strong]
Bstar_Box [in Kstar_strong]


C

cardSmC [in base]
cards_leq1P [in base]
classicb [in base]
classicF [in base]
connectP' [in base]
connectTR_transD [in Kstar_strong]
connect_TR_S [in Kstar]
connect_TR_S [in Hstar]
contra' [in base]


D

Ddc_unsat [in Kstar]
Ddc_unsat [in Hstar]
DdiaNE [in Hstar]
DdiaNE [in Kstar]
DdstarNE [in Hstar]
DdstarNE [in Kstar]
decidability [in Hstar]
decidability [in Kstar]
decidability [in P]
decidability [in Kstar_strong]
decidable_reflect [in base]
dec_sat_val [in Kstar]
dec_valid2equiv [in P]
dec_sat2valid [in P]
dec_sat_val [in Hstar]
dec_sat_val [in Kstar_strong]
demoD [in Kstar_strong]
deMorganAb [in base]
deMorganb [in base]
deMorganE [in base]
deMorganE2 [in base]
demo_theorem [in Hstar]
demo_Delta [in Kstar]
demo_theorem [in Kstar]
dnb [in base]
Drc_unsat [in Kstar]
Drc_unsat [in Hstar]
Dstar_Dia [in Kstar_strong]


E

efbP [in UB]
efbP [in Kstar]
efbP [in Hstar]
EFb_ext [in UB]
EFb_ext [in Kstar]
EFb_ext [in Hstar]
EFC [in Hstar]
EFC [in Kstar]
EF_ext [in UB]
EF_step [in Hstar]
EF_step [in UB]
EF_ext [in Hstar]
EF_step [in Kstar]
EF_ext [in Kstar]
EGP [in UB]
EGP_aux [in UB]
equic_dec [in P]
equiv_valid [in Kstar]
equiv_valid [in Hstar]
equiv_dec [in Kstar_strong]
equiv_sat_valid [in P]
equiv_dec [in Hstar]
equiv_valid [in Kstar_strong]
equiv_valid [in P]
equiv_dec [in Kstar]
eq_form_dec [in P]
eq_form_dec [in Hstar]
eq_form_dec [in Kstar_strong]
eq_form_dec [in Kstar]
eval_Neg [in P]
eval_Neg [in Hstar]
eval_Neg [in Kstar]
eval_Neg [in Kstar_strong]
exbP [in Hstar]
exbP [in Kstar]
exbP [in UB]
EXb_ext [in Kstar]
EXb_ext [in Hstar]
EXb_ext [in UB]
extension [in Kstar]
extension [in Hstar]
EX_ext [in Hstar]
EX_ext [in UB]
EX_ext [in Kstar]
ex2E [in base]


F

fin_choice_aux [in base]
fin_choice [in base]


G

guess [in Hstar]
guess_S [in Hstar]


H

HC [in Hstar]
HC [in Kstar]
HC [in Kstar_strong]
hintikkaD [in Hstar]
hintikkaD [in Kstar]
hintikkaD [in Kstar_strong]
H_at_hintikka [in Kstar]
H_at_hintikka [in Hstar]
H_at_hintikka [in Kstar_strong]
H_at_sat [in Kstar]
H_at_sat [in Hstar]
H_at_collapse [in Hstar]


I

iffP' [in base]
introP' [in base]
inv [in Hstar]
inv [in P]
inv [in Kstar_strong]
inv [in Kstar]
invariantHU [in Kstar]
invariant_prune [in Kstar]
invariant_demo [in Kstar]
invariant_step [in Hstar]
invariant_prune [in Hstar]
invariant_Dxe [in Hstar]
invariant_demo [in Hstar]
invariant_step [in Kstar]
inv_sub [in Kstar]
inv_H_at [in Kstar]
inv_H_at [in Hstar]
inv_sub [in Hstar]
iterFsub [in base]
iterFsubn [in base]
iter_fix [in base]


L

leq1 [in base]
ltn_leq_trans [in base]


M

model_MD_aux [in Kstar_strong]
model_existence [in Kstar_strong]
model_MD_aux [in Kstar]
model_existence [in P]
model_existence [in Hstar]
model_existence [in Kstar]
model_MD_aux [in Hstar]
monoF [in UB]
msvalE [in base]
msvalP [in base]
muE [in base]
mu_ind [in base]


N

nedb_egb [in UB]
negb_EXb [in Hstar]
negb_AXb [in UB]
negb_EXb [in Kstar]
negb_AXb [in Hstar]
negb_EXb [in UB]
negb_AXb [in Kstar]
negb_AGb [in Hstar]
negb_afb [in UB]
negb_AGb [in Kstar]
negb_efb [in UB]
negb_agb [in UB]
negb_EFb [in Hstar]
negb_EFb [in Kstar]
Neg_involutive [in Hstar]
Neg_involutive [in Kstar]
Neg_involutive [in P]
Neg_involutive [in Kstar_strong]
nlabelP' [in Hstar]
nominalE [in Hstar]
nominalI [in Hstar]
normEn [in base]
not_ex_all [in Kstar_strong]
not_all_ex [in Kstar_strong]
nseqP [in Hstar]


O

orS [in base]


P

parse_pickle_xs [in base]
path_rcons [in base]
pick_rcS [in Hstar]
pick_dcH [in Hstar]
pick_rcH [in Kstar]
pick_rcH [in Hstar]
pick_rcS [in Kstar]
pick_dcH [in Kstar]
pick_dcS [in Kstar]
pick_dcS [in Hstar]
predC_involutive [in base]
prune_subset [in Hstar]
prune_rc [in Hstar]
prune_dc [in Kstar]
prune_dc [in Hstar]
prune_Dxc [in Hstar]
prune_subset [in Kstar]
prune_rc [in Kstar]


R

reflectPn [in base]
reflect_DN [in base]
reflect_decidable [in base]


S

sat_dec [in Kstar]
sat_dec [in Kstar_strong]
sat_dec [in P]
sat_dec [in Hstar]
setD1id [in base]
simple_tree_rect [in base]
small_models [in P]
small_model_theorem [in Kstar_strong]
step_smaller [in Kstar]
step_smaller [in Hstar]
subset_step [in Kstar]
subset_step [in Hstar]
synclos_nlabelD [in Hstar]
synclos_refl [in Kstar]
synclos_trans [in Kstar]
synclos_trans [in Kstar_strong]
synclos_refl [in Kstar_strong]
synclos_refl [in P]
synclos_refl [in Hstar]
synclos_trans [in Hstar]
synclos_trans [in P]


T

trans_TR [in Kstar]
trans_star_connect [in Kstar_strong]
trans_TR [in Hstar]
trans_star_trans [in Kstar_strong]
trans_star_case [in Kstar_strong]
trans_TR [in Kstar_strong]
trans_star1 [in Kstar_strong]
trans_star0 [in Kstar_strong]
tree_eq_dec [in base]
tree_rect' [in base]
TR_transD [in Kstar_strong]
t_inv [in base]


U

uniq_nseq [in Hstar]
unsat_inv [in Hstar]
unsat_not_H_at [in Hstar]
unsat_inv [in Kstar]


V

valid_dec [in P]
valid_dec [in Hstar]
valid_dec [in Kstar_strong]
valid_unsat [in Kstar]
valid_dec [in Kstar]
valid_unsat [in Hstar]
valid_unsat [in Kstar_strong]
valid_unsat [in P]



Section Index

C

Characterizations [in Kstar]
Characterizations [in Hstar]
Characterizations [in UB]


D

Dualities [in UB]


F

FiniteModel [in Hstar]
FiniteModel [in UB]
FiniteModel [in Kstar]
finset [in base]
FixPoint [in base]
FormulaUniverse [in Kstar_strong]
FormulaUniverse [in Hstar]
FormulaUniverse [in P]
FormulaUniverse [in Kstar]
FormulaUniverse.ModelExistence [in Hstar]
FormulaUniverse.ModelExistence [in Kstar_strong]
FormulaUniverse.ModelExistence [in Kstar]
FormulaUniverse.SmallModelTheorem [in Kstar]
FormulaUniverse.SmallModelTheorem [in Hstar]
FormulaUniverse.SmallModelTheorem [in Kstar_strong]
FormulaUniverse.SmallModelTheorem.PruningInvariant [in Hstar]


M

Models [in Hstar]
Models [in Kstar]


T

TreeCountType [in base]
TreeCountType.SimpleTreeInd [in base]
TreeCountType.TreeInd [in base]



Notation Index

F

_ |== _ [in Kstar]
_ |== _ [in Hstar]


other

exs _ : _ , _ (type_scope) [in Kstar_strong]
_ ---> _ [in Hstar]
_ \in' _ [in base]
_ |= _ [in Hstar]
_ --->* _ [in Kstar_strong]
_ ---> _ [in Kstar_strong]
_ |= _ [in P]
_ ---> _ [in Kstar]
_ ---> _ [in UB]
_ |= _ [in Kstar]
_ |= _ [in Kstar_strong]
alls _ , _ [in Kstar_strong]
exs _ , _ [in Kstar_strong]
[ss _ ; _ ] [in P]
[ss _ ; _ ] [in Kstar_strong]
[ss _ ; _ ] [in Kstar]
[ss _ ; _ ] [in Hstar]



Constructor Index

A

AFs [in UB]
AF_ [in UB]
AF0 [in UB]
AGs [in UB]
AGs [in Hstar]
AGs [in Kstar]
AG_ [in UB]
And [in Hstar]
And [in Kstar]
And [in Kstar_strong]
And [in P]
AND_ [in UB]
AX_ [in UB]


B

Box [in Kstar_strong]
Box [in Hstar]
Box [in Kstar]
Bstar [in Kstar_strong]
Bstar [in Hstar]
Bstar [in Kstar]


D

Dia [in Hstar]
Dia [in Kstar]
Dia [in Kstar_strong]
Dstar [in Hstar]
Dstar [in Kstar]
Dstar [in Kstar_strong]


E

EFs [in Hstar]
EFs [in UB]
EFs [in Kstar]
EF_ [in UB]
EF0 [in Hstar]
EF0 [in UB]
EF0 [in Kstar]
EGs [in UB]
EG_ [in UB]
EX_ [in UB]


M

Model [in Kstar]
Model [in Hstar]
Model [in Kstar_strong]
Model [in UB]


N

NegNom [in Hstar]
NegVar [in Kstar_strong]
NegVar [in Hstar]
NegVar [in Kstar]
NegVar [in P]
Node [in base]
Nom [in Hstar]
normI [in base]
NP_ [in UB]


O

Or [in Hstar]
Or [in Kstar]
Or [in Kstar_strong]
Or [in P]
OR_ [in UB]


P

P_ [in UB]


V

Var [in Kstar_strong]
Var [in P]
Var [in Hstar]
Var [in Kstar]



Inductive Index

A

AF [in UB]
AG [in Kstar]
AG [in UB]
AG [in Hstar]


E

EF [in Hstar]
EF [in Kstar]
EF [in UB]
EG [in UB]


F

form [in Hstar]
form [in Kstar]
form [in P]
form [in Kstar_strong]
form [in UB]


N

norm [in base]


T

tree [in base]



Definition Index

A

afb [in UB]
AGb [in Kstar]
AGb [in Hstar]
AGb [in UB]
alls [in Kstar_strong]
AX [in Kstar]
AX [in UB]
AX [in Hstar]
AXb [in Kstar]
AXb [in UB]
AXb [in Hstar]


D

D [in Kstar_strong]
Ddia [in Kstar]
Ddia [in Hstar]
Ddia [in Kstar_strong]
Ddstar [in Hstar]
Ddstar [in Kstar]
Ddstar [in Kstar_strong]
decidable [in base]
decidable2 [in base]
default [in Hstar]
Delta [in Kstar]
demo [in Kstar_strong]
demo [in Kstar]
demo [in Hstar]
Dxc [in Hstar]
Dxe [in Hstar]


E

efb [in Hstar]
efb [in UB]
efb [in Kstar]
EGb [in UB]
equiv [in Kstar_strong]
equiv [in Kstar]
equiv [in Hstar]
equiv [in P]
eval [in UB]
eval [in P]
eval [in Kstar_strong]
eval [in Hstar]
eval [in Kstar]
EX [in Hstar]
EX [in Kstar]
EX [in UB]
exb [in Hstar]
exb [in Kstar]
exb [in UB]
exsD [in Kstar_strong]
exsPD [in Kstar_strong]


F

F [in Hstar]
F [in Kstar_strong]
F [in UB]
F [in P]
F [in Kstar]
form_CountType [in P]
form_ChoiceType [in P]
form_eqType [in P]
form_CountType [in Hstar]
form_ChoiceType [in Hstar]
form_eqType [in Hstar]
form_choiceMixin [in P]
form_eqMixin [in Hstar]
form_eqMixin [in Kstar]
form_countMixin [in Kstar_strong]
form_CountType [in Kstar]
form_ChoiceType [in Kstar]
form_eqType [in Kstar]
form_choiceMixin [in Kstar]
form_choiceMixin [in Kstar_strong]
form_eqMixin [in P]
form_countMixin [in Hstar]
form_eqMixin [in Kstar_strong]
form_countMixin [in P]
form_countMixin [in Kstar]
form_CountType [in Kstar_strong]
form_ChoiceType [in Kstar_strong]
form_eqType [in Kstar_strong]
form_choiceMixin [in Hstar]


H

Hcond [in P]
Hcond [in Hstar]
Hcond [in Kstar_strong]
Hcond [in Kstar]
hintikka [in Hstar]
hintikka [in P]
hintikka [in Kstar_strong]
hintikka [in Kstar]
HU [in Hstar]
HU [in Kstar]
HU [in Kstar_strong]
H_at [in Kstar_strong]
H_at [in Kstar]
H_at [in Hstar]


I

invariant [in Kstar]
invariant [in Hstar]


L

labelD [in Kstar]
labelD [in Hstar]
labelD [in Kstar_strong]


M

maximal [in Hstar]
MD [in Kstar]
MD [in Kstar_strong]
MD [in Hstar]
model [in P]
mono [in base]
msval [in base]
mu [in base]


N

N [in Hstar]
Neg [in P]
Neg [in Kstar_strong]
Neg [in Kstar]
Neg [in Hstar]
nlabelD [in Hstar]
nominal [in Hstar]
nseq [in Hstar]
nset [in Hstar]
nvar [in Hstar]


P

pickle [in P]
pickle [in Kstar_strong]
pickle [in Kstar]
pickle [in Hstar]
pick_rc [in Hstar]
pick_dc [in Kstar]
pick_dc [in Hstar]
pick_rc [in Kstar]


R

request [in Kstar]
request [in Kstar_strong]
request [in Hstar]


S

sat [in Hstar]
sat [in Kstar_strong]
sat [in P]
sat [in Kstar]
satF [in Kstar]
satM [in Hstar]
set_op [in base]
sn [in base]
stateD [in Kstar]
stateD [in Kstar_strong]
stateD [in Hstar]
stateD_model [in Hstar]
stateD_model [in Kstar]
stateD_model [in Kstar_strong]
step [in Kstar]
step [in Hstar]
synclos [in Hstar]
synclos [in Kstar_strong]
synclos [in P]
synclos [in Kstar]


T

TR [in Hstar]
TR [in Kstar]
TR [in Kstar_strong]
transD [in Kstar]
transD [in Hstar]
transD [in Kstar_strong]
trans_starPD [in Kstar_strong]
trans_starD [in Kstar_strong]
tree_CountType [in base]
tree_ChoiceType [in base]
tree_eqType [in base]
tree_countMixin [in base]
tree_choiceMixin [in base]
tree_eqMixin [in base]
t_unpickle [in base]
t_parse [in base]
t_pickle [in base]


U

unpickle [in Kstar_strong]
unpickle [in P]
unpickle [in Kstar]
unpickle [in Hstar]


V

valid [in Kstar]
valid [in P]
valid [in Kstar_strong]
valid [in Hstar]
var [in Hstar]
var [in Kstar_strong]
var [in Kstar]
var [in P]
var [in UB]


X

xchoose2_sig [in base]



Variable Index

C

Characterizations.e [in UB]
Characterizations.R [in Hstar]
Characterizations.R [in Kstar]
Characterizations.X [in Hstar]
Characterizations.X [in Kstar]
Characterizations.X [in UB]


D

Dualities.M [in UB]


F

FiniteModel.e [in Hstar]
FiniteModel.e [in Kstar]
FiniteModel.e [in UB]
FiniteModel.label [in Kstar]
FiniteModel.label [in Hstar]
FiniteModel.label [in UB]
FiniteModel.p [in UB]
FiniteModel.T [in Kstar]
FiniteModel.T [in UB]
FiniteModel.T [in Hstar]
finset.T [in base]
finset.xs [in base]
FixPoint.F [in base]
FixPoint.monoF [in base]
FixPoint.T [in base]
FormulaUniverse.ModelExistence.D [in Hstar]
FormulaUniverse.ModelExistence.D [in Kstar_strong]
FormulaUniverse.ModelExistence.D [in Kstar]
FormulaUniverse.ModelExistence.demoD [in Hstar]
FormulaUniverse.ModelExistence.demoD [in Kstar_strong]
FormulaUniverse.ModelExistence.demoD [in Kstar]
FormulaUniverse.s [in Hstar]
FormulaUniverse.s [in Kstar_strong]
FormulaUniverse.s [in P]
FormulaUniverse.s [in Kstar]
FormulaUniverse.SmallModelTheorem.PruningInvariant.M [in Hstar]


M

Models.M [in Hstar]
Models.M [in Kstar]


T

TreeCountType.SimpleTreeInd.P [in base]
TreeCountType.SimpleTreeInd.Pcons [in base]
TreeCountType.SimpleTreeInd.Pnil [in base]
TreeCountType.TreeInd.P [in base]
TreeCountType.TreeInd.Pcons [in base]
TreeCountType.TreeInd.Pnil [in base]
TreeCountType.TreeInd.P' [in base]
TreeCountType.TreeInd.P'cons [in base]
TreeCountType.TreeInd.P'nil [in base]
TreeCountType.X [in base]



Library Index

B

base


H

Hstar


K

Kstar
Kstar_strong


P

P


T

tactics


U

UB



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 _ other (628 entries)
Projection 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 _ other (32 entries)
Record 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 _ other (4 entries)
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 _ other (247 entries)
Section 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 _ other (25 entries)
Notation 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 _ other (19 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 _ other (58 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 _ other (15 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 _ other (176 entries)
Variable 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 _ other (45 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 _ other (7 entries)

This page has been generated by coqdoc