Completeness and Decidability Results for CTL in Coq

Global Index

other

(732 entries)

Notation Index

other

(18 entries)

Module Index

other

(2 entries)

Variable Index

other

(58 entries)

Library Index

other

(10 entries)

Lemma Index

other

(310 entries)

Constructor Index

other

(68 entries)

Inductive Index

other

(15 entries)

Projection Index

other

(41 entries)

Section Index

other

(25 entries)

Instance Index

other

(21 entries)

Definition Index

other

(154 entries)

Record Index

other

(10 entries)

Global Index

A

aAR [constructor, in tab_def]
aAR_inU [lemma, in tab_dec]
aAU [constructor, in tab_def]
aAU_inU [lemma, in tab_dec]
aAXR [constructor, in tab_def]
aAXR_inU [lemma, in tab_dec]
aAXU [constructor, in tab_def]
aAXU_inU [lemma, in tab_dec]
afn1 [lemma, in tab_translation]
afp1 [lemma, in tab_translation]
af1n [lemma, in tab_translation]
af1p [lemma, in tab_translation]
AG [projection, in modular_hilbert]
AG_mor [instance, in modular_hilbert]
And [definition, in modular_hilbert]
andAAU [lemma, in modular_hilbert]
andU [lemma, in modular_hilbert]
and_sub [lemma, in modular_hilbert]
And_mor [instance, in modular_hilbert]
Annot [module, in tab_def]
annot [inductive, in tab_def]
annot_CountType [definition, in tab_def]
annot_choiceType [definition, in tab_def]
annot_choiceMixin [definition, in tab_def]
annot_countMixin [definition, in tab_def]
annot_eqType [definition, in tab_def]
annot_eqMixin [definition, in tab_def]
annot_request [lemma, in tab_translation]
Annot.pickle [definition, in tab_def]
Annot.pickleP [lemma, in tab_def]
Annot.unpickle [definition, in tab_def]
aR [definition, in tab_def]
AR [projection, in modular_hilbert]
ARb [definition, in CTL_def]
ARH_sound [lemma, in tab_translation]
arP [lemma, in CTL_def]
ARs [definition, in tab_dec]
ARs [constructor, in CTL_def]
AR_mor [instance, in modular_hilbert]
AR_shift [lemma, in tab_dec]
AR_strengthen [lemma, in CTL_def]
AR0 [constructor, in CTL_def]
As [definition, in tab_dec]
AsAR [lemma, in tab_dec]
AsAU [lemma, in tab_dec]
AsAXR [lemma, in tab_dec]
AsAXU [lemma, in tab_dec]
AsV [lemma, in tab_dec]
AsX [lemma, in tab_dec]
AsX' [lemma, in tab_dec]
AU [projection, in modular_hilbert]
AUb [definition, in CTL_def]
AUb [section, in CTL_def]
AUb.e [variable, in CTL_def]
AUb.p [variable, in CTL_def]
AUb.q [variable, in CTL_def]
AUb.T [variable, in CTL_def]
AUH_sound [lemma, in tab_translation]
auP [lemma, in CTL_def]
AUs [definition, in tab_dec]
AUs [constructor, in CTL_def]
AU_mor [instance, in modular_hilbert]
AU_shift [lemma, in tab_dec]
AU_mono [lemma, in CTL_def]
AU_fun [definition, in CTL_def]
AU_ind [constructor, in CTL_def]
AU_strengthen [lemma, in CTL_def]
AU_lift [lemma, in demo]
AU_this [lemma, in demo]
AU_M [definition, in demo]
AU_ [definition, in tab_translation]
AU0 [constructor, in CTL_def]
aVoid [constructor, in tab_def]
AX [projection, in modular_hilbert]
axAA [lemma, in modular_hilbert]
axABBA [lemma, in modular_hilbert]
axAC [lemma, in modular_hilbert]
axAcase [lemma, in modular_hilbert]
axADr [lemma, in modular_hilbert]
axAEl [lemma, in modular_hilbert]
axAEr [lemma, in modular_hilbert]
axAGEl [projection, in modular_hilbert]
axAGEr [projection, in modular_hilbert]
axAGI [lemma, in modular_hilbert]
axAGN [projection, in modular_hilbert]
axAI [lemma, in modular_hilbert]
axARE [projection, in modular_hilbert]
axARE [constructor, in CTL_def]
axAReq [lemma, in modular_hilbert]
axARu [projection, in modular_hilbert]
axARu [constructor, in CTL_def]
axAsT [lemma, in modular_hilbert]
axATs [lemma, in modular_hilbert]
axAUAEr [lemma, in modular_hilbert]
axAUAw [lemma, in modular_hilbert]
axAUEGF [lemma, in modular_hilbert]
axAUERF [lemma, in modular_hilbert]
axAUf [projection, in modular_hilbert]
axAUf [constructor, in CTL_def]
axAUHu [lemma, in tab_translation]
axAUI [projection, in modular_hilbert]
axAUI [constructor, in CTL_def]
axAUu [lemma, in modular_hilbert]
axB [lemma, in modular_hilbert]
axBAAB [lemma, in modular_hilbert]
axBE [lemma, in modular_hilbert]
axBT [lemma, in modular_hilbert]
axC [lemma, in modular_hilbert]
axContra [lemma, in modular_hilbert]
axDBD [lemma, in modular_hilbert]
axDF [lemma, in modular_hilbert]
axDN [lemma, in modular_hilbert]
axDN [constructor, in CTL_def]
axDNI [lemma, in modular_hilbert]
axDN' [projection, in modular_hilbert]
axDup [lemma, in modular_hilbert]
axEEl [lemma, in modular_hilbert]
axEEr [lemma, in modular_hilbert]
axEI [lemma, in modular_hilbert]
axERu [lemma, in modular_hilbert]
axEUeq [lemma, in modular_hilbert]
axEUEr [lemma, in modular_hilbert]
axEUI [lemma, in modular_hilbert]
axEUI2 [lemma, in modular_hilbert]
axEUw [lemma, in modular_hilbert]
axEXAEl [lemma, in modular_hilbert]
axI [lemma, in modular_hilbert]
axIO [lemma, in modular_hilbert]
axK [lemma, in modular_hilbert]
axK [constructor, in CTL_def]
axK' [projection, in modular_hilbert]
AXn [definition, in tab_complete]
axN [projection, in modular_hilbert]
axN [constructor, in CTL_def]
axOC [lemma, in modular_hilbert]
axOE [lemma, in modular_hilbert]
axOF [lemma, in modular_hilbert]
axOIl [lemma, in modular_hilbert]
axOIr [lemma, in modular_hilbert]
axRot [lemma, in modular_hilbert]
AXR_shift [lemma, in tab_dec]
axS [lemma, in modular_hilbert]
axS [constructor, in CTL_def]
axsT [lemma, in modular_hilbert]
axS' [projection, in modular_hilbert]
axT [lemma, in modular_hilbert]
AXU_shift [lemma, in tab_dec]
axW [lemma, in modular_hilbert]
AX_mor [instance, in modular_hilbert]
ax_contraNN [lemma, in modular_hilbert]
ax_contra [lemma, in modular_hilbert]
ax_case [lemma, in modular_hilbert]
ax_serial [constructor, in CTL_def]
a_cond [definition, in demo]

B

C

D

D [definition, in tab_complete]
dags [library]
dag_D [lemma, in demo]
dag_R [lemma, in demo]
DC [definition, in demo]
decidability [lemma, in result]
demo [definition, in demo]
Demo [section, in demo]
demo [library]
DemoTrees [section, in tab_complete]
DemoTrees.LL [variable, in tab_complete]
DemoTrees.L0 [variable, in tab_complete]
DemoTrees.t [variable, in tab_complete]
Demo.D [variable, in demo]
Demo.Dl [variable, in demo]
Demo.F [variable, in demo]
Demo.sfc_F [variable, in demo]
determined [definition, in CTL_def]
DF [definition, in demo]
dgraph [definition, in demo]
Disjoint [section, in dags]
disjointness [lemma, in result]
Disjoint.G [variable, in dags]
Disjoint.I [variable, in dags]
Disjoint.L [variable, in dags]
Dl [definition, in tab_complete]
dmA [lemma, in modular_hilbert]
dmAi [lemma, in modular_hilbert]
dmAR [lemma, in modular_hilbert]
Dmatrix [definition, in demo]
DmatrixP [lemma, in demo]
dmat_ev_cond [lemma, in demo]
dmAU [lemma, in modular_hilbert]
dmAUH [lemma, in tab_translation]
dmAUi [lemma, in modular_hilbert]
dmAX [lemma, in modular_hilbert]
dmER [lemma, in modular_hilbert]
dmERi [lemma, in modular_hilbert]
dmI [lemma, in modular_hilbert]
dmO [lemma, in modular_hilbert]
D_sub_Dl [lemma, in tab_complete]

E

edge [projection, in dags]
EF [definition, in modular_hilbert]
Eqi [definition, in modular_hilbert]
EqiPrv [definition, in modular_hilbert]
EqiTheoryBase [section, in modular_hilbert]
EqiTheoryBase.pS [variable, in modular_hilbert]
EqiTheoryBase.s [variable, in modular_hilbert]
EqiTheoryBase.t [variable, in modular_hilbert]
eqi_induced_symmety [instance, in modular_hilbert]
eq_annot_dec [lemma, in tab_def]
eq_form_dec [lemma, in CTL_def]
ER [definition, in modular_hilbert]
erel [definition, in dags]
ERs [constructor, in CTL_def]
ER_mor [instance, in modular_hilbert]
ER_strengthen [lemma, in CTL_def]
ER0 [constructor, in CTL_def]
EU [definition, in modular_hilbert]
EU [definition, in CTL_def]
EUb [definition, in CTL_def]
euP [lemma, in CTL_def]
EUs [constructor, in CTL_def]
EU_ind [lemma, in modular_hilbert]
EU_mor [instance, in modular_hilbert]
EU_mono [lemma, in CTL_def]
EU_fun [definition, in CTL_def]
EU_strengthen [lemma, in CTL_def]
EU_lift [lemma, in demo]
EU_this [lemma, in demo]
EU_M [definition, in demo]
EU_ [definition, in tab_translation]
EU0 [constructor, in CTL_def]
eval [definition, in CTL_def]
evalb [definition, in CTL_def]
evalP [lemma, in CTL_def]
ev_cond [definition, in demo]
EX [definition, in modular_hilbert]
EX_mor [instance, in modular_hilbert]

F

fAR [constructor, in CTL_def]
fAU [constructor, in CTL_def]
fAX [constructor, in CTL_def]
fF [constructor, in CTL_def]
fImp [constructor, in CTL_def]
finite [inductive, in CTL_def]
finiteI [constructor, in CTL_def]
FiniteModels [section, in CTL_def]
FiniteModels.e [variable, in CTL_def]
FiniteModels.l [variable, in CTL_def]
FiniteModels.serial_e [variable, in CTL_def]
FiniteModels.T [variable, in CTL_def]
fin_finite [lemma, in CTL_def]
fin_model [definition, in CTL_def]
fin_modelP [lemma, in CTL_def]
fin_sts [definition, in CTL_def]
form [inductive, in CTL_def]
formChoice [module, in CTL_def]
formChoice.pickle [definition, in CTL_def]
formChoice.pickleP [lemma, in CTL_def]
formChoice.unpickle [definition, in CTL_def]
form_CountType [definition, in CTL_def]
form_ChoiceType [definition, in CTL_def]
form_choiceMixin [definition, in CTL_def]
form_countMixin [definition, in CTL_def]
form_eqType [definition, in CTL_def]
form_eqMixin [definition, in CTL_def]
fV [constructor, in CTL_def]
f_weight [definition, in tab_complete]

G

ge_cond [definition, in demo]
glabels_from [definition, in demo]
glocal [definition, in dags]
graph [record, in dags]
Graph [constructor, in dags]
GraphOf [section, in dags]
GraphOf.L [variable, in dags]
GraphOf.t [variable, in dags]
GraphTheory [section, in dags]
GraphTheory.L [variable, in dags]
GraphTheory.p [variable, in dags]
graph_of_tree [definition, in dags]
graph_of_rootP [lemma, in dags]
graph_of_root [definition, in dags]
graph_of_rel [definition, in dags]
graph_of_label [definition, in dags]
graph_of_type [definition, in dags]
graph_of [projection, in dags]
graph_has [lemma, in tab_complete]
graph_of_labels [lemma, in tab_complete]

H

Hilbert [section, in CTL_def]
hilbert_soundness [lemma, in tab_translation]
_ ---> _ [notation, in CTL_def]
hist [definition, in tab_translation]
histU [lemma, in tab_translation]
hist0 [lemma, in tab_translation]
Hs [definition, in tab_dec]

I

J

JCs [definition, in tab_complete]
JC_inD [lemma, in tab_complete]
JC_inhab [lemma, in tab_complete]
JC_rcond [lemma, in tab_complete]
JC_scond [lemma, in tab_complete]
j_tree_for [lemma, in tab_complete]
j_tree_r_cond [lemma, in tab_complete]
j_tree [definition, in tab_complete]
j_leafs [definition, in tab_complete]

K

ksort [projection, in modular_hilbert]
ksort' [projection, in modular_hilbert]
ksSystem [record, in modular_hilbert]
KSSystem [constructor, in modular_hilbert]
KStarTheory [section, in modular_hilbert]
KStarTheory.ksS [variable, in modular_hilbert]
kSystem [record, in modular_hilbert]
KSystem [constructor, in modular_hilbert]
KTheory [section, in modular_hilbert]
KTheory.kS [variable, in modular_hilbert]

L

label [projection, in dags]
label [projection, in CTL_def]
labels_leaf [lemma, in tab_complete]
labels_from [definition, in tab_complete]
label_F [lemma, in demo]
label_lcon [lemma, in demo]
label_Dl [lemma, in demo]
label_root [lemma, in demo]
label_DF [lemma, in demo]
lcons [definition, in demo]
lcons_void [lemma, in tab_complete]
leaf [definition, in dags]
leaf_root' [lemma, in demo]
leaf_root [lemma, in demo]
leaf_root_aux [lemma, in demo]
liftE [lemma, in dags]
lift_connect [lemma, in dags]
lift_eqn [lemma, in dags]
lift_eq [lemma, in dags]
lift_edge [definition, in dags]
literal [definition, in demo]
literalC [definition, in demo]

M

MD [definition, in demo]
mImpPrv [definition, in modular_hilbert]
mImpPrv_rel [instance, in modular_hilbert]
mImpPrv_trans [lemma, in modular_hilbert]
mImpPrv_refl [definition, in modular_hilbert]
MLabel [definition, in demo]
model [record, in CTL_def]
Model [constructor, in CTL_def]
ModelConstruction [section, in demo]
ModelConstruction.D [variable, in demo]
ModelConstruction.DD [variable, in demo]
ModelConstruction.Dl [variable, in demo]
ModelConstruction.Dl_cond [variable, in demo]
ModelConstruction.D_cond [variable, in demo]
ModelConstruction.F [variable, in demo]
ModelConstruction.sfc_F [variable, in demo]
modelP [projection, in CTL_def]
model_existence [lemma, in demo]
modular_hilbert [library]
mono_step [lemma, in tab_dec]
mprv [projection, in modular_hilbert]
mprv_mor [instance, in modular_hilbert]
mp2 [lemma, in modular_hilbert]
MRel [definition, in demo]
MRel_D [lemma, in demo]
MRel_R [lemma, in demo]
msort [projection, in modular_hilbert]
mSystem [record, in modular_hilbert]
MSystem [constructor, in modular_hilbert]
MTheory0 [section, in modular_hilbert]
MTheory0.mS [variable, in modular_hilbert]
MType [definition, in demo]

N

Neg [definition, in modular_hilbert]
negative [definition, in CTL_def]
negatives [definition, in CTL_def]
negE [lemma, in CTL_def]
Neg_mor [instance, in modular_hilbert]

O

Or [definition, in modular_hilbert]
or_sub [lemma, in modular_hilbert]
Or_mor [instance, in modular_hilbert]

P

plainP [lemma, in tab_dec]
plain_inU [lemma, in tab_dec]
plain_soundness [lemma, in tab_translation]
posE [lemma, in CTL_def]
positive [definition, in CTL_def]
positives [definition, in CTL_def]
pr [definition, in tab_def]
PredC [definition, in CTL_def]
prV [lemma, in tab_def]
prv [inductive, in CTL_def]
prv_ctlSystem [definition, in CTL_def]
prv_kSystem [definition, in CTL_def]
prv_pSystem [definition, in CTL_def]
prv_mSystem [definition, in CTL_def]
pr_inCs [lemma, in tab_dec]
pr' [definition, in tab_def]
psort [projection, in modular_hilbert]
pSystem [record, in modular_hilbert]
PSystem [constructor, in modular_hilbert]
PTheory [section, in modular_hilbert]
PTheoryBase [section, in modular_hilbert]
PTheoryBase.pS [variable, in modular_hilbert]
PTheory.pS [variable, in modular_hilbert]

R

R [definition, in CTL_def]
rAG_ind [projection, in modular_hilbert]
rAI [lemma, in modular_hilbert]
rApply [lemma, in modular_hilbert]
rApply2 [lemma, in modular_hilbert]
rApply3 [lemma, in modular_hilbert]
rAR_ind [projection, in modular_hilbert]
rAR_ind [constructor, in CTL_def]
rAUw [lemma, in modular_hilbert]
rAU_ind_weak [lemma, in modular_hilbert]
rAU_ind [projection, in modular_hilbert]
rDup [lemma, in modular_hilbert]
RE [lemma, in CTL_def]
relT [definition, in tab_complete]
request_cond [definition, in tab_complete]
rER_ind_weak [lemma, in modular_hilbert]
rER_ind [lemma, in modular_hilbert]
respects [definition, in dags]
restrict [definition, in dags]
result [library]
rEXn [lemma, in modular_hilbert]
rGraph [record, in dags]
RGraph [constructor, in dags]
rgraph_of_respects [lemma, in dags]
rgraph_of_acyclic [lemma, in dags]
rgraph_of_local [lemma, in dags]
rgraph_of [definition, in dags]
rgraph_of_root [lemma, in tab_complete]
rHyp [lemma, in modular_hilbert]
rHyp1 [lemma, in modular_hilbert]
rIntro [lemma, in modular_hilbert]
RinU [lemma, in tab_dec]
Rl [definition, in tab_complete]
rlab [definition, in dags]
RlconU [lemma, in tab_complete]
Rljmp [lemma, in tab_complete]
RlR [lemma, in tab_complete]
rMP [lemma, in modular_hilbert]
rMP [constructor, in CTL_def]
rMP' [projection, in modular_hilbert]
rNec [projection, in modular_hilbert]
rNec [constructor, in CTL_def]
rNecS [lemma, in modular_hilbert]
rNorm [lemma, in modular_hilbert]
rNormS [lemma, in modular_hilbert]
root [projection, in dags]
rootP [projection, in dags]
root_internal [lemma, in demo]
Rpos [lemma, in CTL_def]
rRev [lemma, in modular_hilbert]
rRev1 [lemma, in modular_hilbert]
rRot [lemma, in modular_hilbert]
RU [lemma, in CTL_def]
r_cond [definition, in demo]
R0 [lemma, in CTL_def]
R1 [lemma, in CTL_def]

S

scomplete [definition, in tab_complete]
segerberg [lemma, in modular_hilbert]
SeqSubConnect [section, in dags]
SeqSubConnect.e [variable, in dags]
SeqSubConnect.sub_closed [variable, in dags]
SeqSubConnect.T [variable, in dags]
SeqSubConnect.xs [variable, in dags]
serial [projection, in CTL_def]
serial_relT [lemma, in tab_complete]
serial_MRel [lemma, in demo]
sfc [definition, in tab_dec]
sfcU [lemma, in CTL_def]
sfc_bigcup [lemma, in tab_dec]
sfc_ssub [lemma, in CTL_def]
sform [definition, in CTL_def]
sf_AR [lemma, in tab_dec]
sf_AU [lemma, in tab_dec]
sf_ssub [lemma, in CTL_def]
sf_closed'_mon [lemma, in CTL_def]
sf_closed [definition, in CTL_def]
sf_closed' [definition, in CTL_def]
simple_tree_rect [lemma, in dags]
simple_tree [lemma, in tab_complete]
SN [constructor, in dags]
sn [inductive, in dags]
sn_restrict [lemma, in dags]
sn_edge [lemma, in demo]
soundness [lemma, in CTL_def]
ssub [definition, in CTL_def]
ssub_refl [lemma, in CTL_def]
ssub' [definition, in CTL_def]
ssub'_refl [lemma, in CTL_def]
stable [definition, in CTL_def]
star [inductive, in dags]
StarL [constructor, in dags]
Star0 [constructor, in dags]
state [projection, in CTL_def]
step [definition, in tab_dec]
stepP [lemma, in tab_dec]
step_jmp [definition, in tab_dec]
step_annot [definition, in tab_dec]
step_plain [definition, in tab_dec]
step_plain_cases [definition, in tab_dec]
sts [record, in CTL_def]
STS [constructor, in CTL_def]
sts_of [projection, in CTL_def]
subCs [lemma, in tab_dec]
subtrees [definition, in dags]
subtrees_trans [lemma, in dags]
subtrees_refl [lemma, in dags]
subtrees1 [lemma, in dags]
subU [lemma, in tab_dec]
sub_behead [lemma, in modular_hilbert]
sub_sfc [lemma, in tab_dec]
successors [definition, in tab_complete]
succ_CinU [lemma, in tab_complete]
supp [definition, in demo]
suppC [definition, in demo]
suppCD [lemma, in demo]
suppCU [lemma, in demo]
suppCWL [lemma, in demo]
suppC_sub [lemma, in demo]
suppC1 [lemma, in demo]
suppF [lemma, in demo]
support [definition, in tab_complete]
supportT [lemma, in tab_complete]
support_aux [lemma, in tab_complete]
suppxx [lemma, in demo]
supp_suppCr [lemma, in tab_complete]
supp_suppCl [lemma, in tab_complete]
supp_suppC [lemma, in tab_complete]
supp_U [lemma, in tab_complete]
supp_lit [lemma, in tab_complete]
supp_con [lemma, in tab_complete]
supp_eval [lemma, in demo]
supp_edge [lemma, in demo]
supp_mon [lemma, in demo]
supp' [definition, in demo]
sweight_lit [lemma, in tab_complete]
s_weight [definition, in tab_complete]
s_cond [definition, in demo]

T

T [projection, in modular_hilbert]
tab [inductive, in tab_def]
tabU_aAXR [lemma, in tab_dec]
tabU_foc' [lemma, in tab_dec]
tabU_ARhr [lemma, in tab_dec]
tabU_ARhl [lemma, in tab_dec]
tabU_ARnr [lemma, in tab_dec]
tabU_ARnl [lemma, in tab_dec]
tabU_ARpr [lemma, in tab_dec]
tabU_ARpl [lemma, in tab_dec]
tabU_ufoc [lemma, in tab_dec]
tabU_jmp [lemma, in tab_dec]
tabU_AUhr [lemma, in tab_dec]
tabU_AUhl [lemma, in tab_dec]
tabU_foc [lemma, in tab_dec]
tabU_AUnr [lemma, in tab_dec]
tabU_AUnl [lemma, in tab_dec]
tabU_AUpr [lemma, in tab_dec]
tabU_AUpl [lemma, in tab_dec]
tabU_AXn [lemma, in tab_dec]
tabU_aR [lemma, in tab_dec]
tabU_in [lemma, in tab_dec]
tabU_ipr [lemma, in tab_dec]
tabU_ipl [lemma, in tab_dec]
tab_aAXR [constructor, in tab_def]
tab_rep' [constructor, in tab_def]
tab_ARh [constructor, in tab_def]
tab_foc' [constructor, in tab_def]
tab_ARn [constructor, in tab_def]
tab_ARp [constructor, in tab_def]
tab_jmp [constructor, in tab_def]
tab_rep [constructor, in tab_def]
tab_AUh [constructor, in tab_def]
tab_foc [constructor, in tab_def]
tab_AUn [constructor, in tab_def]
tab_AUp [constructor, in tab_def]
tab_AXn [constructor, in tab_def]
tab_In [constructor, in tab_def]
tab_Ip [constructor, in tab_def]
tab_p [constructor, in tab_def]
tab_F [constructor, in tab_def]
tab_plain_complete [lemma, in tab_complete]
tab_demo [lemma, in tab_complete]
tab_dec [lemma, in tab_dec]
tab_decF [lemma, in tab_dec]
tab_closure.sfc_F [variable, in tab_dec]
tab_closure.F [variable, in tab_dec]
tab_closure [section, in tab_dec]
tab_complete [library]
tab_translation [library]
tab_dec [library]
tab_def [library]
terminates [definition, in dags]
tlocal [definition, in dags]
tlocalE [lemma, in dags]
tlocal_sub [lemma, in dags]
Top [definition, in modular_hilbert]
tpickle [definition, in dags]
tpickleK [lemma, in dags]
trans [projection, in CTL_def]
Tree [constructor, in dags]
tree [inductive, in dags]
TreeCountType [section, in dags]
TreeCountType.T [variable, in dags]
TreeRel [section, in dags]
TreeRel.L [variable, in dags]
tree_rel_sn [lemma, in dags]
tree_rooted [lemma, in dags]
tree_rel [definition, in dags]
tree_countType [definition, in dags]
tree_choiceType [definition, in dags]
tree_eqType [definition, in dags]
tree_countMixin [definition, in dags]
tree_rect' [lemma, in dags]
tree_demo [lemma, in tab_complete]
tree_AR [lemma, in tab_complete]
tree_ARH [lemma, in tab_complete]
tree_AU [lemma, in tab_complete]
tree_AUH [lemma, in tab_complete]
tree_for_cons [lemma, in tab_complete]
tree_forI [lemma, in tab_complete]
tree_for_0 [lemma, in tab_complete]
tree_for_and [definition, in tab_complete]
tree_for' [definition, in tab_complete]
tree_for [definition, in tab_complete]
trespects [definition, in dags]
trespectsE [lemma, in dags]
trespects_leaf [lemma, in dags]
trivial [definition, in tab_complete]
tunpickle [definition, in dags]
t_has [definition, in tab_complete]

U

U [definition, in tab_dec]
unit_model [definition, in tab_complete]
u_cond [definition, in demo]

V

var [definition, in CTL_def]
vertex [projection, in dags]

W

weight [definition, in tab_complete]
weightS [lemma, in tab_complete]
weight0 [lemma, in tab_complete]

other

Notation Index

H

_ ---> _ [in CTL_def]

other

Module Index

A

Annot [in tab_def]

F

formChoice [in CTL_def]

Variable Index

A

AUb.e [in CTL_def]
AUb.p [in CTL_def]
AUb.q [in CTL_def]
AUb.T [in CTL_def]

B

BigAnd.pS [in modular_hilbert]

C

CanonicalDemo.F [in tab_complete]
CanonicalDemo.Jumps.A [in tab_complete]
CanonicalDemo.Jumps.C_inU [in tab_complete]
CanonicalDemo.Jumps.C_cons [in tab_complete]
CanonicalDemo.sfc_F [in tab_complete]
CanonicalDemo.Support.C [in tab_complete]
CanonicalDemo.Support.con_in_U [in tab_complete]
CanonicalDemo.Support.E [in tab_complete]
CanonicalDemo.Support.suppP [in tab_complete]
Characterizations.e [in CTL_def]
Characterizations.X [in CTL_def]
CTLTheory.cS [in modular_hilbert]

D

DemoTrees.LL [in tab_complete]
DemoTrees.L0 [in tab_complete]
DemoTrees.t [in tab_complete]
Demo.D [in demo]
Demo.Dl [in demo]
Demo.F [in demo]
Demo.sfc_F [in demo]
Disjoint.G [in dags]
Disjoint.I [in dags]
Disjoint.L [in dags]

E

EqiTheoryBase.pS [in modular_hilbert]
EqiTheoryBase.s [in modular_hilbert]
EqiTheoryBase.t [in modular_hilbert]

F

FiniteModels.e [in CTL_def]
FiniteModels.l [in CTL_def]
FiniteModels.serial_e [in CTL_def]
FiniteModels.T [in CTL_def]

G

GraphOf.L [in dags]
GraphOf.t [in dags]
GraphTheory.L [in dags]
GraphTheory.p [in dags]

K

KStarTheory.ksS [in modular_hilbert]
KTheory.kS [in modular_hilbert]

M

ModelConstruction.D [in demo]
ModelConstruction.DD [in demo]
ModelConstruction.Dl [in demo]
ModelConstruction.Dl_cond [in demo]
ModelConstruction.D_cond [in demo]
ModelConstruction.F [in demo]
ModelConstruction.sfc_F [in demo]
MTheory0.mS [in modular_hilbert]

P

PTheoryBase.pS [in modular_hilbert]
PTheory.pS [in modular_hilbert]

S

SeqSubConnect.e [in dags]
SeqSubConnect.sub_closed [in dags]
SeqSubConnect.T [in dags]
SeqSubConnect.xs [in dags]

T

tab_closure.sfc_F [in tab_dec]
tab_closure.F [in tab_dec]
TreeCountType.T [in dags]
TreeRel.L [in dags]

Library Index

C

CTL_def

D

dags
demo

I

induced_sym

M

modular_hilbert

R

result

T

tab_complete
tab_translation
tab_dec
tab_def

Lemma Index

A

B

bigABBA [in modular_hilbert]
bigAdrop [in modular_hilbert]
bigAdup [in modular_hilbert]
bigAE [in modular_hilbert]
bigAI [in modular_hilbert]
bigAUA [in modular_hilbert]
bigA1 [in modular_hilbert]
bigA1E [in modular_hilbert]
bigOE [in modular_hilbert]
bigOI [in modular_hilbert]
bounded_step [in tab_dec]
box_request [in tab_translation]

C

cAR_cEU [in CTL_def]
cAU_eq [in CTL_def]
cAU_cER [in CTL_def]
cert_dec_method [in result]
cEU_eq [in CTL_def]
closed_sfc [in tab_dec]
completeness [in result]
connect_restrict [in dags]
cons_lcons [in tab_complete]
ctab1 [in tab_complete]
ctab2 [in tab_complete]

D

dag_D [in demo]
dag_R [in demo]
decidability [in result]
disjointness [in result]
dmA [in modular_hilbert]
dmAi [in modular_hilbert]
dmAR [in modular_hilbert]
DmatrixP [in demo]
dmat_ev_cond [in demo]
dmAU [in modular_hilbert]
dmAUH [in tab_translation]
dmAUi [in modular_hilbert]
dmAX [in modular_hilbert]
dmER [in modular_hilbert]
dmERi [in modular_hilbert]
dmI [in modular_hilbert]
dmO [in modular_hilbert]
D_sub_Dl [in tab_complete]

E

eq_annot_dec [in tab_def]
eq_form_dec [in CTL_def]
ER_strengthen [in CTL_def]
euP [in CTL_def]
EU_ind [in modular_hilbert]
EU_mono [in CTL_def]
EU_strengthen [in CTL_def]
EU_lift [in demo]
EU_this [in demo]
evalP [in CTL_def]

F

fin_finite [in CTL_def]
fin_modelP [in CTL_def]
formChoice.pickleP [in CTL_def]

G

graph_of_rootP [in dags]
graph_has [in tab_complete]
graph_of_labels [in tab_complete]

H

hilbert_soundness [in tab_translation]
histU [in tab_translation]
hist0 [in tab_translation]

I

induced_mor_iff2 [in induced_sym]
induced_mor_iff [in induced_sym]
induced_eqi [in induced_sym]
isBoxP [in CTL_def]
isDiaP [in CTL_def]

J

JC_inD [in tab_complete]
JC_inhab [in tab_complete]
JC_rcond [in tab_complete]
JC_scond [in tab_complete]
j_tree_for [in tab_complete]
j_tree_r_cond [in tab_complete]

L

labels_leaf [in tab_complete]
label_F [in demo]
label_lcon [in demo]
label_Dl [in demo]
label_root [in demo]
label_DF [in demo]
lcons_void [in tab_complete]
leaf_root' [in demo]
leaf_root [in demo]
leaf_root_aux [in demo]
liftE [in dags]
lift_connect [in dags]
lift_eqn [in dags]
lift_eq [in dags]

M

mImpPrv_trans [in modular_hilbert]
model_existence [in demo]
mono_step [in tab_dec]
mp2 [in modular_hilbert]
MRel_D [in demo]
MRel_R [in demo]

N

negE [in CTL_def]

O

or_sub [in modular_hilbert]

P

plainP [in tab_dec]
plain_inU [in tab_dec]
plain_soundness [in tab_translation]
posE [in CTL_def]
prV [in tab_def]
pr_inCs [in tab_dec]

R

S

T

W

weightS [in tab_complete]
weight0 [in tab_complete]

Constructor Index

A

aAR [in tab_def]
aAU [in tab_def]
aAXR [in tab_def]
aAXU [in tab_def]
ARs [in CTL_def]
AR0 [in CTL_def]
AUs [in CTL_def]
AU_ind [in CTL_def]
AU0 [in CTL_def]
aVoid [in tab_def]
axARE [in CTL_def]
axARu [in CTL_def]
axAUf [in CTL_def]
axAUI [in CTL_def]
axDN [in CTL_def]
axK [in CTL_def]
axN [in CTL_def]
axS [in CTL_def]
ax_serial [in CTL_def]

C

CTLSystem [in modular_hilbert]

E

ERs [in CTL_def]
ER0 [in CTL_def]
EUs [in CTL_def]
EU0 [in CTL_def]

F

fAR [in CTL_def]
fAU [in CTL_def]
fAX [in CTL_def]
fF [in CTL_def]
fImp [in CTL_def]
finiteI [in CTL_def]
fV [in CTL_def]

G

Graph [in dags]

I

induced_iff [in induced_sym]
isBox_false [in CTL_def]
isBox_true [in CTL_def]
isDia_false [in CTL_def]
isDia_true [in CTL_def]

K

KSSystem [in modular_hilbert]
KSystem [in modular_hilbert]

M

Model [in CTL_def]
MSystem [in modular_hilbert]

P

PSystem [in modular_hilbert]

R

rAR_ind [in CTL_def]
RGraph [in dags]
rMP [in CTL_def]
rNec [in CTL_def]

S

SN [in dags]
StarL [in dags]
Star0 [in dags]
STS [in CTL_def]

T

tab_aAXR [in tab_def]
tab_rep' [in tab_def]
tab_ARh [in tab_def]
tab_foc' [in tab_def]
tab_ARn [in tab_def]
tab_ARp [in tab_def]
tab_jmp [in tab_def]
tab_rep [in tab_def]
tab_AUh [in tab_def]
tab_foc [in tab_def]
tab_AUn [in tab_def]
tab_AUp [in tab_def]
tab_AXn [in tab_def]
tab_In [in tab_def]
tab_Ip [in tab_def]
tab_p [in tab_def]
tab_F [in tab_def]
Tree [in dags]

Inductive Index

A

annot [in tab_def]

C

cAR [in CTL_def]
cAU [in CTL_def]
cER [in CTL_def]
cEU [in CTL_def]

F

finite [in CTL_def]
form [in CTL_def]

I

InducedSym [in induced_sym]
isBox_spec [in CTL_def]
isDia_spec [in CTL_def]

P

prv [in CTL_def]

S

sn [in dags]
star [in dags]

T

tab [in tab_def]
tree [in dags]

Projection Index

A

AG [in modular_hilbert]
AR [in modular_hilbert]
AU [in modular_hilbert]
AX [in modular_hilbert]
axAGEl [in modular_hilbert]
axAGEr [in modular_hilbert]
axAGN [in modular_hilbert]
axARE [in modular_hilbert]
axARu [in modular_hilbert]
axAUf [in modular_hilbert]
axAUI [in modular_hilbert]
axDN' [in modular_hilbert]
axK' [in modular_hilbert]
axN [in modular_hilbert]
axS' [in modular_hilbert]

B

Bot [in modular_hilbert]

E

edge [in dags]

G

graph_of [in dags]

I

Imp [in modular_hilbert]
induced_iff [in induced_sym]

K

ksort [in modular_hilbert]
ksort' [in modular_hilbert]

L

label [in dags]
label [in CTL_def]

M

modelP [in CTL_def]
mprv [in modular_hilbert]
msort [in modular_hilbert]

P

psort [in modular_hilbert]

R

rAG_ind [in modular_hilbert]
rAR_ind [in modular_hilbert]
rAU_ind [in modular_hilbert]
rMP' [in modular_hilbert]
rNec [in modular_hilbert]
root [in dags]
rootP [in dags]

S

serial [in CTL_def]
state [in CTL_def]
sts_of [in CTL_def]

T

T [in modular_hilbert]
trans [in CTL_def]

V

vertex [in dags]

Section Index

A

AUb [in CTL_def]

B

BigAnd [in modular_hilbert]

C

CanonicalDemo [in tab_complete]
CanonicalDemo.Jumps [in tab_complete]
CanonicalDemo.Support [in tab_complete]
Characterizations [in CTL_def]
CTLTheory [in modular_hilbert]

D

Demo [in demo]
DemoTrees [in tab_complete]
Disjoint [in dags]

E

EqiTheoryBase [in modular_hilbert]

F

FiniteModels [in CTL_def]

G

GraphOf [in dags]
GraphTheory [in dags]

H

Hilbert [in CTL_def]

K

KStarTheory [in modular_hilbert]
KTheory [in modular_hilbert]

M

ModelConstruction [in demo]
MTheory0 [in modular_hilbert]

P

PTheory [in modular_hilbert]
PTheoryBase [in modular_hilbert]

S

SeqSubConnect [in dags]

T

tab_closure [in tab_dec]
TreeCountType [in dags]
TreeRel [in dags]

Instance Index

A

AG_mor [in modular_hilbert]
And_mor [in modular_hilbert]
AR_mor [in modular_hilbert]
AU_mor [in modular_hilbert]
AX_mor [in modular_hilbert]

E

eqi_induced_symmety [in modular_hilbert]
ER_mor [in modular_hilbert]
EU_mor [in modular_hilbert]
EX_mor [in modular_hilbert]

I

Imp_mor [in modular_hilbert]
induced_eqi [in modular_hilbert]
induced_mor_np [in induced_sym]
induced_mor_pn [in induced_sym]
induced_mor_pp [in induced_sym]
induced_mor_n [in induced_sym]
induced_mor_p [in induced_sym]
induced_sub [in induced_sym]

M

mImpPrv_rel [in modular_hilbert]
mprv_mor [in modular_hilbert]

N

Neg_mor [in modular_hilbert]

O

Or_mor [in modular_hilbert]

Definition Index

A

And [in modular_hilbert]
annot_CountType [in tab_def]
annot_choiceType [in tab_def]
annot_choiceMixin [in tab_def]
annot_countMixin [in tab_def]
annot_eqType [in tab_def]
annot_eqMixin [in tab_def]
Annot.pickle [in tab_def]
Annot.unpickle [in tab_def]
aR [in tab_def]
ARb [in CTL_def]
ARs [in tab_dec]
As [in tab_dec]
AUb [in CTL_def]
AUs [in tab_dec]
AU_fun [in CTL_def]
AU_M [in demo]
AU_ [in tab_translation]
AXn [in tab_complete]
a_cond [in demo]

B

body [in CTL_def]

C

cAX [in CTL_def]
cEX [in CTL_def]
clause [in CTL_def]
consistent [in tab_complete]
Cs [in tab_dec]

D

D [in tab_complete]
DC [in demo]
demo [in demo]
determined [in CTL_def]
DF [in demo]
dgraph [in demo]
Dl [in tab_complete]
Dmatrix [in demo]

E

EF [in modular_hilbert]
Eqi [in modular_hilbert]
EqiPrv [in modular_hilbert]
ER [in modular_hilbert]
erel [in dags]
EU [in modular_hilbert]
EU [in CTL_def]
EUb [in CTL_def]
EU_fun [in CTL_def]
EU_M [in demo]
EU_ [in tab_translation]
eval [in CTL_def]
evalb [in CTL_def]
ev_cond [in demo]
EX [in modular_hilbert]

F

fin_model [in CTL_def]
fin_sts [in CTL_def]
formChoice.pickle [in CTL_def]
formChoice.unpickle [in CTL_def]
form_CountType [in CTL_def]
form_ChoiceType [in CTL_def]
form_choiceMixin [in CTL_def]
form_countMixin [in CTL_def]
form_eqType [in CTL_def]
form_eqMixin [in CTL_def]
f_weight [in tab_complete]

G

ge_cond [in demo]
glabels_from [in demo]
glocal [in dags]
graph_of_tree [in dags]
graph_of_root [in dags]
graph_of_rel [in dags]
graph_of_label [in dags]
graph_of_type [in dags]

H

hist [in tab_translation]
Hs [in tab_dec]

I

Imp_op [in modular_hilbert]
interp [in CTL_def]
interp_a [in tab_translation]
isBox [in CTL_def]
isDia [in CTL_def]

J

JCs [in tab_complete]
j_tree [in tab_complete]
j_leafs [in tab_complete]

L

labels_from [in tab_complete]
lcons [in demo]
leaf [in dags]
lift_edge [in dags]
literal [in demo]
literalC [in demo]

M

MD [in demo]
mImpPrv [in modular_hilbert]
mImpPrv_refl [in modular_hilbert]
MLabel [in demo]
MRel [in demo]
MType [in demo]

N

Neg [in modular_hilbert]
negative [in CTL_def]
negatives [in CTL_def]

O

Or [in modular_hilbert]

P

positive [in CTL_def]
positives [in CTL_def]
pr [in tab_def]
PredC [in CTL_def]
prv_ctlSystem [in CTL_def]
prv_kSystem [in CTL_def]
prv_pSystem [in CTL_def]
prv_mSystem [in CTL_def]
pr' [in tab_def]

R

R [in CTL_def]
relT [in tab_complete]
request_cond [in tab_complete]
respects [in dags]
restrict [in dags]
rgraph_of [in dags]
Rl [in tab_complete]
rlab [in dags]
r_cond [in demo]

S

scomplete [in tab_complete]
sfc [in tab_dec]
sform [in CTL_def]
sf_closed [in CTL_def]
sf_closed' [in CTL_def]
ssub [in CTL_def]
ssub' [in CTL_def]
stable [in CTL_def]
step [in tab_dec]
step_jmp [in tab_dec]
step_annot [in tab_dec]
step_plain [in tab_dec]
step_plain_cases [in tab_dec]
subtrees [in dags]
successors [in tab_complete]
supp [in demo]
suppC [in demo]
support [in tab_complete]
supp' [in demo]
s_weight [in tab_complete]
s_cond [in demo]

T

terminates [in dags]
tlocal [in dags]
Top [in modular_hilbert]
tpickle [in dags]
tree_rel [in dags]
tree_countType [in dags]
tree_choiceType [in dags]
tree_eqType [in dags]
tree_countMixin [in dags]
tree_for_and [in tab_complete]
tree_for' [in tab_complete]
tree_for [in tab_complete]
trespects [in dags]
trivial [in tab_complete]
tunpickle [in dags]
t_has [in tab_complete]

U

U [in tab_dec]
unit_model [in tab_complete]
u_cond [in demo]

V

var [in CTL_def]

W

weight [in tab_complete]

Record Index

C

ctlSystem [in modular_hilbert]

G

graph [in dags]

I

InducedSym [in induced_sym]

K

ksSystem [in modular_hilbert]
kSystem [in modular_hilbert]

M

model [in CTL_def]
mSystem [in modular_hilbert]

P

pSystem [in modular_hilbert]

R

rGraph [in dags]

S

sts [in CTL_def]

Global Index

other

(732 entries)

Notation Index

other

(18 entries)

Module Index

other

(2 entries)

Variable Index

other

(58 entries)

Library Index

other

(10 entries)

Lemma Index

other

(310 entries)

Constructor Index

other

(68 entries)

Inductive Index

other

(15 entries)

Projection Index

other

(41 entries)

Section Index

other

(25 entries)

Instance Index

other

(21 entries)

Definition Index

other

(154 entries)

Record Index

other

(10 entries)

This page has been generated by coqdoc