Constructive Pruning-Based Completeness Proofs for K*
| 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 | (350 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 | (9 entries) |
| Module 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 | (3 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 | (21 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 | (6 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 | (118 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 | (62 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 | (14 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 | (12 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 | (12 entries) |
| Abbreviation 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 | (6 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 | (83 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) |
Global Index
A
aAG [constructor, in Kstar.gen_def]aAXG [constructor, in Kstar.gen_def]
AGb [definition, in Kstar.Kstar_def]
agP [lemma, in Kstar.Kstar_def]
AGs [constructor, in Kstar.Kstar_def]
AG_fun [definition, in Kstar.Kstar_def]
AG_strengthen [lemma, in Kstar.Kstar_def]
Annot [module, in Kstar.gen_def]
annot [inductive, in Kstar.gen_def]
annot_choiceMixin [definition, in Kstar.gen_def]
annot_countMixin [definition, in Kstar.gen_def]
annot_eqMixin [definition, in Kstar.gen_def]
Annot.pickle [definition, in Kstar.gen_def]
Annot.pickleP [lemma, in Kstar.gen_def]
Annot.unpickle [definition, in Kstar.gen_def]
AR_mono [lemma, in Kstar.Kstar_def]
aVoid [constructor, in Kstar.gen_def]
axAGEl [constructor, in Kstar.Kstar_def]
axAGEr [constructor, in Kstar.Kstar_def]
axDN [constructor, in Kstar.Kstar_def]
axK [constructor, in Kstar.Kstar_def]
axN [constructor, in Kstar.Kstar_def]
AXn [definition, in Kstar.gen_ref]
axS [constructor, in Kstar.Kstar_def]
ax_lcons [lemma, in Kstar.hilbert_ref]
B
baseP [lemma, in Kstar.hilbert_ref]base0 [definition, in Kstar.hilbert_ref]
base0P [lemma, in Kstar.hilbert_ref]
body [definition, in Kstar.Kstar_def]
box_request [lemma, in Kstar.Kstar_def]
C
cAG [inductive, in Kstar.Kstar_def]cAG_cEF [lemma, in Kstar.Kstar_def]
cAG_crt [lemma, in Kstar.Kstar_def]
cAX [definition, in Kstar.Kstar_def]
cEF [inductive, in Kstar.Kstar_def]
cEX [definition, in Kstar.Kstar_def]
Characterizations [section, in Kstar.Kstar_def]
Characterizations.e [variable, in Kstar.Kstar_def]
Characterizations.X [variable, in Kstar.Kstar_def]
clause [definition, in Kstar.Kstar_def]
closed_sfc [lemma, in Kstar.Kstar_def]
cls [projection, in Kstar.demo]
cmodel [record, in Kstar.Kstar_def]
CModel [constructor, in Kstar.Kstar_def]
cmodel_of_fmodel [definition, in Kstar.Kstar_def]
coref [definition, in Kstar.demo]
coref [definition, in Kstar.gen_ref]
corefD1 [lemma, in Kstar.demo]
corefD1 [lemma, in Kstar.gen_ref]
coref_DD [lemma, in Kstar.demo]
coref_S [lemma, in Kstar.gen_ref]
D
DD [definition, in Kstar.demo]DD [definition, in Kstar.gen_ref]
DD_refute [lemma, in Kstar.demo]
Decidability [section, in Kstar.gen_ref]
DecidabilityAndAgreement [section, in Kstar.Kstar_def]
DecidabilityAndAgreement.e [variable, in Kstar.Kstar_def]
DecidabilityAndAgreement.p [variable, in Kstar.Kstar_def]
DecidabilityAndAgreement.T [variable, in Kstar.Kstar_def]
Decidability.S [variable, in Kstar.gen_ref]
Decidability.S0 [variable, in Kstar.gen_ref]
demo [record, in Kstar.demo]
Demo [constructor, in Kstar.demo]
demo [library]
demoD0 [projection, in Kstar.demo]
demoD1 [projection, in Kstar.demo]
demoD2 [projection, in Kstar.demo]
dsatH [definition, in Kstar.gen_def]
dsatU1 [lemma, in Kstar.gen_def]
dsat0 [lemma, in Kstar.gen_def]
D0 [definition, in Kstar.demo]
D1 [definition, in Kstar.demo]
D2 [definition, in Kstar.demo]
E
EFs [constructor, in Kstar.Kstar_def]EF_strengthen [lemma, in Kstar.Kstar_def]
EF0 [constructor, in Kstar.Kstar_def]
eq_form_dec [lemma, in Kstar.Kstar_def]
eq_annot_dec [lemma, in Kstar.gen_def]
eval [definition, in Kstar.Kstar_def]
evalb [definition, in Kstar.Kstar_def]
evalbAG [lemma, in Kstar.gen_def]
evalP [lemma, in Kstar.Kstar_def]
F
fAG [constructor, in Kstar.Kstar_def]fAX [constructor, in Kstar.Kstar_def]
fF [constructor, in Kstar.Kstar_def]
fImp [constructor, in Kstar.Kstar_def]
FiniteModels [section, in Kstar.Kstar_def]
FiniteModels.M [variable, in Kstar.Kstar_def]
finite_soundness [lemma, in Kstar.Kstar_def]
fin_modelP [lemma, in Kstar.Kstar_def]
flabel [projection, in Kstar.Kstar_def]
fmodel [record, in Kstar.Kstar_def]
FModel [constructor, in Kstar.Kstar_def]
form [inductive, in Kstar.Kstar_def]
formChoice [module, in Kstar.Kstar_def]
formChoice.pickle [definition, in Kstar.Kstar_def]
formChoice.pickleP [lemma, in Kstar.Kstar_def]
formChoice.unpickle [definition, in Kstar.Kstar_def]
form_slClass [definition, in Kstar.Kstar_def]
form_choiceMixin [definition, in Kstar.Kstar_def]
form_countMixin [definition, in Kstar.Kstar_def]
form_eqMixin [definition, in Kstar.Kstar_def]
fstate [projection, in Kstar.Kstar_def]
ftrans [projection, in Kstar.Kstar_def]
fulfillAG [inductive, in Kstar.demo]
fulfillAG [inductive, in Kstar.gen_ref]
fulfillAGb [definition, in Kstar.demo]
fulfillAGb [definition, in Kstar.gen_ref]
fulfillAGE [lemma, in Kstar.demo]
fulfillAGE [lemma, in Kstar.gen_ref]
fulfillAGEn [lemma, in Kstar.demo]
fulfillAGn [constructor, in Kstar.demo]
fulfillAGn [constructor, in Kstar.gen_ref]
fulfillAGP [lemma, in Kstar.demo]
fulfillAGP [lemma, in Kstar.gen_ref]
fulfillAG_fun_bounded [lemma, in Kstar.demo]
fulfillAG_fun_mono [lemma, in Kstar.demo]
fulfillAG_fun [definition, in Kstar.demo]
fulfillAG_Req [lemma, in Kstar.gen_ref]
fulfillAG_fun_bounded [lemma, in Kstar.gen_ref]
fulfillAG_fun_mono [lemma, in Kstar.gen_ref]
fulfillAG_fun [definition, in Kstar.gen_ref]
fulfillAG1 [constructor, in Kstar.demo]
fulfillAG1 [constructor, in Kstar.gen_ref]
funsat [definition, in Kstar.gen_def]
funsat1 [lemma, in Kstar.gen_def]
funsat2 [lemma, in Kstar.gen_def]
fV [constructor, in Kstar.Kstar_def]
f_size [definition, in Kstar.Kstar_def]
f_weight [definition, in Kstar.Kstar_def]
G
gen [inductive, in Kstar.gen_def]gen_correctness [lemma, in Kstar.results]
gen_completeness [lemma, in Kstar.results]
gen_rep [constructor, in Kstar.gen_def]
gen_AGh [constructor, in Kstar.gen_def]
gen_foc [constructor, in Kstar.gen_def]
gen_AGn [constructor, in Kstar.gen_def]
gen_AGp [constructor, in Kstar.gen_def]
gen_AXH [constructor, in Kstar.gen_def]
gen_AXn [constructor, in Kstar.gen_def]
gen_In [constructor, in Kstar.gen_def]
gen_Ip [constructor, in Kstar.gen_def]
gen_p [constructor, in Kstar.gen_def]
gen_F [constructor, in Kstar.gen_def]
gen_correctness [lemma, in Kstar.gen_ref]
gen_plain_sound [lemma, in Kstar.gen_ref]
gen_completeness [lemma, in Kstar.gen_ref]
gen_ref [library]
gen_def [library]
H
Hilbert [section, in Kstar.Kstar_def]hilbert_ref [library]
_ ---> _ [notation, in Kstar.Kstar_def]
hist [inductive, in Kstar.gen_def]
histS [constructor, in Kstar.gen_def]
hist_dsatH [lemma, in Kstar.gen_def]
hist0 [constructor, in Kstar.gen_def]
href_of [lemma, in Kstar.hilbert_ref]
I
informative_completeness [lemma, in Kstar.hilbert_ref]informative_completeness [lemma, in Kstar.results]
isBox [definition, in Kstar.Kstar_def]
isBoxP [lemma, in Kstar.Kstar_def]
isBox_false [constructor, in Kstar.Kstar_def]
isBox_true [constructor, in Kstar.Kstar_def]
isBox_spec [inductive, in Kstar.Kstar_def]
isDia [definition, in Kstar.Kstar_def]
isDiaP [lemma, in Kstar.Kstar_def]
isDia_false [constructor, in Kstar.Kstar_def]
isDia_true [constructor, in Kstar.Kstar_def]
isDia_spec [inductive, in Kstar.Kstar_def]
K
Kstar_def [library]L
label [projection, in Kstar.Kstar_def]LCF [lemma, in Kstar.demo]
lcons [definition, in Kstar.Kstar_def]
lcons_gen [lemma, in Kstar.gen_ref]
ldec [definition, in Kstar.Kstar_def]
literal [definition, in Kstar.Kstar_def]
M
Mlabel [definition, in Kstar.demo]ModelExistience [section, in Kstar.demo]
ModelExistience.S [variable, in Kstar.demo]
modelP [projection, in Kstar.Kstar_def]
model_of [definition, in Kstar.demo]
Mtrans [definition, in Kstar.demo]
Mtype [definition, in Kstar.demo]
N
negative [definition, in Kstar.Kstar_def]negatives [definition, in Kstar.Kstar_def]
negE [lemma, in Kstar.Kstar_def]
P
pcond [definition, in Kstar.demo]pcond [definition, in Kstar.gen_ref]
posE [lemma, in Kstar.Kstar_def]
positive [definition, in Kstar.Kstar_def]
positives [definition, in Kstar.Kstar_def]
PredC [definition, in Kstar.Kstar_def]
prf_ref_sound [lemma, in Kstar.hilbert_ref]
prune_D2 [lemma, in Kstar.demo]
prune_D1 [lemma, in Kstar.demo]
prune_D0 [lemma, in Kstar.demo]
prune_D2 [lemma, in Kstar.gen_ref]
prune_D2_S [lemma, in Kstar.gen_ref]
prune_S_aux [lemma, in Kstar.gen_ref]
prune_D1 [lemma, in Kstar.gen_ref]
prune_D1_strong [lemma, in Kstar.gen_ref]
prune_D0 [lemma, in Kstar.gen_ref]
Pruning [section, in Kstar.demo]
Pruning [section, in Kstar.gen_ref]
pruning_completeness [lemma, in Kstar.demo]
Pruning.F [variable, in Kstar.demo]
Pruning.F [variable, in Kstar.gen_ref]
Pruning.Fs [variable, in Kstar.gen_ref]
Pruning.sfc_F [variable, in Kstar.demo]
Pruning.sfc_F [variable, in Kstar.gen_ref]
prv [inductive, in Kstar.Kstar_def]
prv_dec [lemma, in Kstar.hilbert_ref]
prv_Sprv [lemma, in Kstar.results]
prv_dec [lemma, in Kstar.results]
prv_Sprv [lemma, in Kstar.Kstar_def]
P1 [definition, in Kstar.demo]
P1 [definition, in Kstar.gen_ref]
P2 [definition, in Kstar.demo]
P2 [definition, in Kstar.gen_ref]
R
R [definition, in Kstar.Kstar_def]rAG_ind [constructor, in Kstar.Kstar_def]
RE [lemma, in Kstar.Kstar_def]
ref [definition, in Kstar.hilbert_ref]
ref [inductive, in Kstar.demo]
ref [inductive, in Kstar.gen_ref]
refE1n [lemma, in Kstar.hilbert_ref]
refI1n [lemma, in Kstar.hilbert_ref]
RefPred [section, in Kstar.hilbert_ref]
RefPred [section, in Kstar.gen_ref]
refpred_tref [lemma, in Kstar.gen_ref]
RefPred.ContextRefutations [section, in Kstar.hilbert_ref]
RefPred.ContextRefutations.coref_S [variable, in Kstar.hilbert_ref]
RefPred.ContextRefutations.S [variable, in Kstar.hilbert_ref]
RefPred.ContextRefutations.sub_S [variable, in Kstar.hilbert_ref]
RefPred.F [variable, in Kstar.hilbert_ref]
RefPred.F [variable, in Kstar.gen_ref]
RefPred.sfc_F [variable, in Kstar.hilbert_ref]
RefPred.sfc_F [variable, in Kstar.gen_ref]
Req [definition, in Kstar.gen_ref]
results [library]
RinU [lemma, in Kstar.Kstar_def]
rMP [constructor, in Kstar.Kstar_def]
rNec [constructor, in Kstar.Kstar_def]
Rpos [lemma, in Kstar.Kstar_def]
rtrans [definition, in Kstar.demo]
RU [lemma, in Kstar.Kstar_def]
R0 [lemma, in Kstar.Kstar_def]
R1 [lemma, in Kstar.hilbert_ref]
R1 [constructor, in Kstar.demo]
R1 [lemma, in Kstar.Kstar_def]
R1 [constructor, in Kstar.gen_ref]
R1inU [lemma, in Kstar.demo]
R1inU [lemma, in Kstar.gen_ref]
R2 [lemma, in Kstar.hilbert_ref]
R2 [constructor, in Kstar.demo]
R2 [constructor, in Kstar.gen_ref]
R3 [lemma, in Kstar.hilbert_ref]
R3 [constructor, in Kstar.demo]
R3 [constructor, in Kstar.gen_ref]
S
S [module, in Kstar.Kstar_def]S [definition, in Kstar.gen_ref]
sat [definition, in Kstar.demo]
satA [lemma, in Kstar.Kstar_def]
satA [definition, in Kstar.gen_def]
satC [definition, in Kstar.gen_def]
satCA [definition, in Kstar.gen_def]
satCR [lemma, in Kstar.gen_def]
satCU [lemma, in Kstar.gen_def]
satC1 [lemma, in Kstar.gen_def]
satU1P [lemma, in Kstar.gen_def]
sat_dec [lemma, in Kstar.hilbert_ref]
sat_dec [lemma, in Kstar.results]
sat_hist0 [lemma, in Kstar.gen_def]
sfc [definition, in Kstar.Kstar_def]
sfcU [lemma, in Kstar.Kstar_def]
sfc_bigcup [lemma, in Kstar.Kstar_def]
sfc_ssub [lemma, in Kstar.Kstar_def]
sform [definition, in Kstar.Kstar_def]
sf_ssub [lemma, in Kstar.Kstar_def]
sf_closed'_mon [lemma, in Kstar.Kstar_def]
sf_closed [definition, in Kstar.Kstar_def]
sf_closed' [definition, in Kstar.Kstar_def]
size_ssub [lemma, in Kstar.Kstar_def]
small_models [lemma, in Kstar.hilbert_ref]
small_models [lemma, in Kstar.results]
soundness [lemma, in Kstar.results]
soundness [lemma, in Kstar.Kstar_def]
soundness [lemma, in Kstar.gen_def]
ssub [definition, in Kstar.Kstar_def]
ssub_refl [lemma, in Kstar.Kstar_def]
ssub' [definition, in Kstar.Kstar_def]
ssub'_refl [lemma, in Kstar.Kstar_def]
stable [definition, in Kstar.Kstar_def]
state [projection, in Kstar.Kstar_def]
sts_of [projection, in Kstar.Kstar_def]
sub_sfc [lemma, in Kstar.Kstar_def]
supp [definition, in Kstar.Kstar_def]
suppC1 [lemma, in Kstar.Kstar_def]
suppS [definition, in Kstar.demo]
supp_eval [lemma, in Kstar.demo]
supp_lit [lemma, in Kstar.Kstar_def]
supp_mon [lemma, in Kstar.Kstar_def]
supp_S_sat [lemma, in Kstar.gen_ref]
sweight_lit [lemma, in Kstar.Kstar_def]
S_refute [lemma, in Kstar.gen_ref]
S.axAGEl [constructor, in Kstar.Kstar_def]
S.axAGEr [constructor, in Kstar.Kstar_def]
S.axDN [constructor, in Kstar.Kstar_def]
S.axK [constructor, in Kstar.Kstar_def]
S.axN [constructor, in Kstar.Kstar_def]
S.axNS [constructor, in Kstar.Kstar_def]
S.axS [constructor, in Kstar.Kstar_def]
S.axSeg [constructor, in Kstar.Kstar_def]
S.prv [inductive, in Kstar.Kstar_def]
S.rMP [constructor, in Kstar.Kstar_def]
S.rNec [constructor, in Kstar.Kstar_def]
S.rNecS [constructor, in Kstar.Kstar_def]
S.Seg [section, in Kstar.Kstar_def]
_ ---> _ [notation, in Kstar.Kstar_def]
S0 [abbreviation, in Kstar.hilbert_ref]
S0 [definition, in Kstar.demo]
S0 [abbreviation, in Kstar.gen_ref]
S0 [definition, in Kstar.gen_ref]
T
T [definition, in Kstar.gen_ref]trans [projection, in Kstar.Kstar_def]
tref [definition, in Kstar.gen_ref]
tref_R3 [lemma, in Kstar.gen_ref]
tref_R2 [lemma, in Kstar.gen_ref]
tref_R1 [lemma, in Kstar.gen_ref]
tref_R0 [lemma, in Kstar.gen_ref]
ts [record, in Kstar.Kstar_def]
TS [constructor, in Kstar.Kstar_def]
U
U [abbreviation, in Kstar.hilbert_ref]U [definition, in Kstar.demo]
U [abbreviation, in Kstar.gen_ref]
U [definition, in Kstar.gen_ref]
V
valid [definition, in Kstar.Kstar_def]valid_dec [lemma, in Kstar.hilbert_ref]
valid_dec [lemma, in Kstar.results]
var [definition, in Kstar.Kstar_def]
X
xaf [abbreviation, in Kstar.hilbert_ref]xaf [abbreviation, in Kstar.gen_ref]
xm_soundness [lemma, in Kstar.Kstar_def]
other
_ |> _ [notation, in Kstar.Kstar_def]_ |> _ ^- [notation, in Kstar.Kstar_def]
_ |> _ ^+ [notation, in Kstar.Kstar_def]
_ |> _ ^ _ [notation, in Kstar.Kstar_def]
_ ^+ [notation, in Kstar.Kstar_def]
_ ^- [notation, in Kstar.Kstar_def]
_ =p _ [notation, in Kstar.Kstar_def]
Notation Index
H
_ ---> _ [in Kstar.Kstar_def]S
_ ---> _ [in Kstar.Kstar_def]other
_ |> _ [in Kstar.Kstar_def]_ |> _ ^- [in Kstar.Kstar_def]
_ |> _ ^+ [in Kstar.Kstar_def]
_ |> _ ^ _ [in Kstar.Kstar_def]
_ ^+ [in Kstar.Kstar_def]
_ ^- [in Kstar.Kstar_def]
_ =p _ [in Kstar.Kstar_def]
Module Index
A
Annot [in Kstar.gen_def]F
formChoice [in Kstar.Kstar_def]S
S [in Kstar.Kstar_def]Variable Index
C
Characterizations.e [in Kstar.Kstar_def]Characterizations.X [in Kstar.Kstar_def]
D
DecidabilityAndAgreement.e [in Kstar.Kstar_def]DecidabilityAndAgreement.p [in Kstar.Kstar_def]
DecidabilityAndAgreement.T [in Kstar.Kstar_def]
Decidability.S [in Kstar.gen_ref]
Decidability.S0 [in Kstar.gen_ref]
F
FiniteModels.M [in Kstar.Kstar_def]M
ModelExistience.S [in Kstar.demo]P
Pruning.F [in Kstar.demo]Pruning.F [in Kstar.gen_ref]
Pruning.Fs [in Kstar.gen_ref]
Pruning.sfc_F [in Kstar.demo]
Pruning.sfc_F [in Kstar.gen_ref]
R
RefPred.ContextRefutations.coref_S [in Kstar.hilbert_ref]RefPred.ContextRefutations.S [in Kstar.hilbert_ref]
RefPred.ContextRefutations.sub_S [in Kstar.hilbert_ref]
RefPred.F [in Kstar.hilbert_ref]
RefPred.F [in Kstar.gen_ref]
RefPred.sfc_F [in Kstar.hilbert_ref]
RefPred.sfc_F [in Kstar.gen_ref]
Library Index
D
demoG
gen_refgen_def
H
hilbert_refK
Kstar_defR
resultsLemma Index
A
agP [in Kstar.Kstar_def]AG_strengthen [in Kstar.Kstar_def]
Annot.pickleP [in Kstar.gen_def]
AR_mono [in Kstar.Kstar_def]
ax_lcons [in Kstar.hilbert_ref]
B
baseP [in Kstar.hilbert_ref]base0P [in Kstar.hilbert_ref]
box_request [in Kstar.Kstar_def]
C
cAG_cEF [in Kstar.Kstar_def]cAG_crt [in Kstar.Kstar_def]
closed_sfc [in Kstar.Kstar_def]
corefD1 [in Kstar.demo]
corefD1 [in Kstar.gen_ref]
coref_DD [in Kstar.demo]
coref_S [in Kstar.gen_ref]
D
DD_refute [in Kstar.demo]dsatU1 [in Kstar.gen_def]
dsat0 [in Kstar.gen_def]
E
EF_strengthen [in Kstar.Kstar_def]eq_form_dec [in Kstar.Kstar_def]
eq_annot_dec [in Kstar.gen_def]
evalbAG [in Kstar.gen_def]
evalP [in Kstar.Kstar_def]
F
finite_soundness [in Kstar.Kstar_def]fin_modelP [in Kstar.Kstar_def]
formChoice.pickleP [in Kstar.Kstar_def]
fulfillAGE [in Kstar.demo]
fulfillAGE [in Kstar.gen_ref]
fulfillAGEn [in Kstar.demo]
fulfillAGP [in Kstar.demo]
fulfillAGP [in Kstar.gen_ref]
fulfillAG_fun_bounded [in Kstar.demo]
fulfillAG_fun_mono [in Kstar.demo]
fulfillAG_Req [in Kstar.gen_ref]
fulfillAG_fun_bounded [in Kstar.gen_ref]
fulfillAG_fun_mono [in Kstar.gen_ref]
funsat1 [in Kstar.gen_def]
funsat2 [in Kstar.gen_def]
G
gen_correctness [in Kstar.results]gen_completeness [in Kstar.results]
gen_correctness [in Kstar.gen_ref]
gen_plain_sound [in Kstar.gen_ref]
gen_completeness [in Kstar.gen_ref]
H
hist_dsatH [in Kstar.gen_def]href_of [in Kstar.hilbert_ref]
I
informative_completeness [in Kstar.hilbert_ref]informative_completeness [in Kstar.results]
isBoxP [in Kstar.Kstar_def]
isDiaP [in Kstar.Kstar_def]
L
LCF [in Kstar.demo]lcons_gen [in Kstar.gen_ref]
N
negE [in Kstar.Kstar_def]P
posE [in Kstar.Kstar_def]prf_ref_sound [in Kstar.hilbert_ref]
prune_D2 [in Kstar.demo]
prune_D1 [in Kstar.demo]
prune_D0 [in Kstar.demo]
prune_D2 [in Kstar.gen_ref]
prune_D2_S [in Kstar.gen_ref]
prune_S_aux [in Kstar.gen_ref]
prune_D1 [in Kstar.gen_ref]
prune_D1_strong [in Kstar.gen_ref]
prune_D0 [in Kstar.gen_ref]
pruning_completeness [in Kstar.demo]
prv_dec [in Kstar.hilbert_ref]
prv_Sprv [in Kstar.results]
prv_dec [in Kstar.results]
prv_Sprv [in Kstar.Kstar_def]
R
RE [in Kstar.Kstar_def]refE1n [in Kstar.hilbert_ref]
refI1n [in Kstar.hilbert_ref]
refpred_tref [in Kstar.gen_ref]
RinU [in Kstar.Kstar_def]
Rpos [in Kstar.Kstar_def]
RU [in Kstar.Kstar_def]
R0 [in Kstar.Kstar_def]
R1 [in Kstar.hilbert_ref]
R1 [in Kstar.Kstar_def]
R1inU [in Kstar.demo]
R1inU [in Kstar.gen_ref]
R2 [in Kstar.hilbert_ref]
R3 [in Kstar.hilbert_ref]
S
satA [in Kstar.Kstar_def]satCR [in Kstar.gen_def]
satCU [in Kstar.gen_def]
satC1 [in Kstar.gen_def]
satU1P [in Kstar.gen_def]
sat_dec [in Kstar.hilbert_ref]
sat_dec [in Kstar.results]
sat_hist0 [in Kstar.gen_def]
sfcU [in Kstar.Kstar_def]
sfc_bigcup [in Kstar.Kstar_def]
sfc_ssub [in Kstar.Kstar_def]
sf_ssub [in Kstar.Kstar_def]
sf_closed'_mon [in Kstar.Kstar_def]
size_ssub [in Kstar.Kstar_def]
small_models [in Kstar.hilbert_ref]
small_models [in Kstar.results]
soundness [in Kstar.results]
soundness [in Kstar.Kstar_def]
soundness [in Kstar.gen_def]
ssub_refl [in Kstar.Kstar_def]
ssub'_refl [in Kstar.Kstar_def]
sub_sfc [in Kstar.Kstar_def]
suppC1 [in Kstar.Kstar_def]
supp_eval [in Kstar.demo]
supp_lit [in Kstar.Kstar_def]
supp_mon [in Kstar.Kstar_def]
supp_S_sat [in Kstar.gen_ref]
sweight_lit [in Kstar.Kstar_def]
S_refute [in Kstar.gen_ref]
T
tref_R3 [in Kstar.gen_ref]tref_R2 [in Kstar.gen_ref]
tref_R1 [in Kstar.gen_ref]
tref_R0 [in Kstar.gen_ref]
V
valid_dec [in Kstar.hilbert_ref]valid_dec [in Kstar.results]
X
xm_soundness [in Kstar.Kstar_def]Constructor Index
A
aAG [in Kstar.gen_def]aAXG [in Kstar.gen_def]
AGs [in Kstar.Kstar_def]
aVoid [in Kstar.gen_def]
axAGEl [in Kstar.Kstar_def]
axAGEr [in Kstar.Kstar_def]
axDN [in Kstar.Kstar_def]
axK [in Kstar.Kstar_def]
axN [in Kstar.Kstar_def]
axS [in Kstar.Kstar_def]
C
CModel [in Kstar.Kstar_def]D
Demo [in Kstar.demo]E
EFs [in Kstar.Kstar_def]EF0 [in Kstar.Kstar_def]
F
fAG [in Kstar.Kstar_def]fAX [in Kstar.Kstar_def]
fF [in Kstar.Kstar_def]
fImp [in Kstar.Kstar_def]
FModel [in Kstar.Kstar_def]
fulfillAGn [in Kstar.demo]
fulfillAGn [in Kstar.gen_ref]
fulfillAG1 [in Kstar.demo]
fulfillAG1 [in Kstar.gen_ref]
fV [in Kstar.Kstar_def]
G
gen_rep [in Kstar.gen_def]gen_AGh [in Kstar.gen_def]
gen_foc [in Kstar.gen_def]
gen_AGn [in Kstar.gen_def]
gen_AGp [in Kstar.gen_def]
gen_AXH [in Kstar.gen_def]
gen_AXn [in Kstar.gen_def]
gen_In [in Kstar.gen_def]
gen_Ip [in Kstar.gen_def]
gen_p [in Kstar.gen_def]
gen_F [in Kstar.gen_def]
H
histS [in Kstar.gen_def]hist0 [in Kstar.gen_def]
I
isBox_false [in Kstar.Kstar_def]isBox_true [in Kstar.Kstar_def]
isDia_false [in Kstar.Kstar_def]
isDia_true [in Kstar.Kstar_def]
R
rAG_ind [in Kstar.Kstar_def]rMP [in Kstar.Kstar_def]
rNec [in Kstar.Kstar_def]
R1 [in Kstar.demo]
R1 [in Kstar.gen_ref]
R2 [in Kstar.demo]
R2 [in Kstar.gen_ref]
R3 [in Kstar.demo]
R3 [in Kstar.gen_ref]
S
S.axAGEl [in Kstar.Kstar_def]S.axAGEr [in Kstar.Kstar_def]
S.axDN [in Kstar.Kstar_def]
S.axK [in Kstar.Kstar_def]
S.axN [in Kstar.Kstar_def]
S.axNS [in Kstar.Kstar_def]
S.axS [in Kstar.Kstar_def]
S.axSeg [in Kstar.Kstar_def]
S.rMP [in Kstar.Kstar_def]
S.rNec [in Kstar.Kstar_def]
S.rNecS [in Kstar.Kstar_def]
T
TS [in Kstar.Kstar_def]Inductive Index
A
annot [in Kstar.gen_def]C
cAG [in Kstar.Kstar_def]cEF [in Kstar.Kstar_def]
F
form [in Kstar.Kstar_def]fulfillAG [in Kstar.demo]
fulfillAG [in Kstar.gen_ref]
G
gen [in Kstar.gen_def]H
hist [in Kstar.gen_def]I
isBox_spec [in Kstar.Kstar_def]isDia_spec [in Kstar.Kstar_def]
P
prv [in Kstar.Kstar_def]R
ref [in Kstar.demo]ref [in Kstar.gen_ref]
S
S.prv [in Kstar.Kstar_def]Projection Index
C
cls [in Kstar.demo]D
demoD0 [in Kstar.demo]demoD1 [in Kstar.demo]
demoD2 [in Kstar.demo]
F
flabel [in Kstar.Kstar_def]fstate [in Kstar.Kstar_def]
ftrans [in Kstar.Kstar_def]
L
label [in Kstar.Kstar_def]M
modelP [in Kstar.Kstar_def]S
state [in Kstar.Kstar_def]sts_of [in Kstar.Kstar_def]
T
trans [in Kstar.Kstar_def]Section Index
C
Characterizations [in Kstar.Kstar_def]D
Decidability [in Kstar.gen_ref]DecidabilityAndAgreement [in Kstar.Kstar_def]
F
FiniteModels [in Kstar.Kstar_def]H
Hilbert [in Kstar.Kstar_def]M
ModelExistience [in Kstar.demo]P
Pruning [in Kstar.demo]Pruning [in Kstar.gen_ref]
R
RefPred [in Kstar.hilbert_ref]RefPred [in Kstar.gen_ref]
RefPred.ContextRefutations [in Kstar.hilbert_ref]
S
S.Seg [in Kstar.Kstar_def]Abbreviation Index
S
S0 [in Kstar.hilbert_ref]S0 [in Kstar.gen_ref]
U
U [in Kstar.hilbert_ref]U [in Kstar.gen_ref]
X
xaf [in Kstar.hilbert_ref]xaf [in Kstar.gen_ref]
Definition Index
A
AGb [in Kstar.Kstar_def]AG_fun [in Kstar.Kstar_def]
annot_choiceMixin [in Kstar.gen_def]
annot_countMixin [in Kstar.gen_def]
annot_eqMixin [in Kstar.gen_def]
Annot.pickle [in Kstar.gen_def]
Annot.unpickle [in Kstar.gen_def]
AXn [in Kstar.gen_ref]
B
base0 [in Kstar.hilbert_ref]body [in Kstar.Kstar_def]
C
cAX [in Kstar.Kstar_def]cEX [in Kstar.Kstar_def]
clause [in Kstar.Kstar_def]
cmodel_of_fmodel [in Kstar.Kstar_def]
coref [in Kstar.demo]
coref [in Kstar.gen_ref]
D
DD [in Kstar.demo]DD [in Kstar.gen_ref]
dsatH [in Kstar.gen_def]
D0 [in Kstar.demo]
D1 [in Kstar.demo]
D2 [in Kstar.demo]
E
eval [in Kstar.Kstar_def]evalb [in Kstar.Kstar_def]
F
formChoice.pickle [in Kstar.Kstar_def]formChoice.unpickle [in Kstar.Kstar_def]
form_slClass [in Kstar.Kstar_def]
form_choiceMixin [in Kstar.Kstar_def]
form_countMixin [in Kstar.Kstar_def]
form_eqMixin [in Kstar.Kstar_def]
fulfillAGb [in Kstar.demo]
fulfillAGb [in Kstar.gen_ref]
fulfillAG_fun [in Kstar.demo]
fulfillAG_fun [in Kstar.gen_ref]
funsat [in Kstar.gen_def]
f_size [in Kstar.Kstar_def]
f_weight [in Kstar.Kstar_def]
I
isBox [in Kstar.Kstar_def]isDia [in Kstar.Kstar_def]
L
lcons [in Kstar.Kstar_def]ldec [in Kstar.Kstar_def]
literal [in Kstar.Kstar_def]
M
Mlabel [in Kstar.demo]model_of [in Kstar.demo]
Mtrans [in Kstar.demo]
Mtype [in Kstar.demo]
N
negative [in Kstar.Kstar_def]negatives [in Kstar.Kstar_def]
P
pcond [in Kstar.demo]pcond [in Kstar.gen_ref]
positive [in Kstar.Kstar_def]
positives [in Kstar.Kstar_def]
PredC [in Kstar.Kstar_def]
P1 [in Kstar.demo]
P1 [in Kstar.gen_ref]
P2 [in Kstar.demo]
P2 [in Kstar.gen_ref]
R
R [in Kstar.Kstar_def]ref [in Kstar.hilbert_ref]
Req [in Kstar.gen_ref]
rtrans [in Kstar.demo]
S
S [in Kstar.gen_ref]sat [in Kstar.demo]
satA [in Kstar.gen_def]
satC [in Kstar.gen_def]
satCA [in Kstar.gen_def]
sfc [in Kstar.Kstar_def]
sform [in Kstar.Kstar_def]
sf_closed [in Kstar.Kstar_def]
sf_closed' [in Kstar.Kstar_def]
ssub [in Kstar.Kstar_def]
ssub' [in Kstar.Kstar_def]
stable [in Kstar.Kstar_def]
supp [in Kstar.Kstar_def]
suppS [in Kstar.demo]
S0 [in Kstar.demo]
S0 [in Kstar.gen_ref]
T
T [in Kstar.gen_ref]tref [in Kstar.gen_ref]
U
U [in Kstar.demo]U [in Kstar.gen_ref]
V
valid [in Kstar.Kstar_def]var [in Kstar.Kstar_def]
Record Index
C
cmodel [in Kstar.Kstar_def]D
demo [in Kstar.demo]F
fmodel [in Kstar.Kstar_def]T
ts [in Kstar.Kstar_def]| 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 | (350 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 | (9 entries) |
| Module 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 | (3 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 | (21 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 | (6 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 | (118 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 | (62 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 | (14 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 | (12 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 | (12 entries) |
| Abbreviation 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 | (6 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 | (83 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) |