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
baseH
HstarK
KstarKstar_strong
P
PT
tacticsU
UBGlobal 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