Completeness and Decidability Results for CTL in Coq
| 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 | (738 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 | (18 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 | (6 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 | (54 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 | (15 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 | (317 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 | (97 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 | (16 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 | (31 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 | (24 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 | (8 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 | (144 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 | (8 entries) |
Global Index
A
aAR [constructor, in CTL.gen_def]aAR_inU [lemma, in CTL.gen_dec]
aAU [constructor, in CTL.gen_def]
aAU_inU [lemma, in CTL.gen_dec]
aAXR [constructor, in CTL.gen_def]
aAXR_inU [lemma, in CTL.gen_dec]
aAXU [constructor, in CTL.gen_def]
aAXU_inU [lemma, in CTL.gen_dec]
Agreement [section, in CTL.agreement]
agreement [library]
Agreement.e [variable, in CTL.agreement]
Agreement.p [variable, in CTL.agreement]
Agreement.q [variable, in CTL.agreement]
Agreement.serial_e [variable, in CTL.agreement]
Agreement.T [variable, in CTL.agreement]
Annot [module, in CTL.gen_def]
annot [inductive, in CTL.gen_def]
annot_request [lemma, in CTL.gen_hsound]
annot_choiceMixin [definition, in CTL.gen_def]
annot_countMixin [definition, in CTL.gen_def]
annot_eqMixin [definition, in CTL.gen_def]
Annot.pickle [definition, in CTL.gen_def]
Annot.pickleP [lemma, in CTL.gen_def]
Annot.unpickle [definition, in CTL.gen_def]
aR [definition, in CTL.gen_def]
ARb [definition, in CTL.CTL_def]
ARb [abbreviation, in CTL.agreement]
ARel [lemma, in CTL.hilbert_LS]
ARH_hil [lemma, in CTL.hilbert_hist]
ARl [definition, in CTL.demo]
ARlE [lemma, in CTL.demo]
arP [lemma, in CTL.CTL_def]
arP2 [lemma, in CTL.agreement]
ARr [definition, in CTL.demo]
ARs [constructor, in CTL.CTL_def]
ARs [definition, in CTL.gen_dec]
AR_mono [lemma, in CTL.CTL_def]
AR_fun [definition, in CTL.CTL_def]
AR_strengthen [lemma, in CTL.CTL_def]
AR_shift [lemma, in CTL.gen_dec]
AR_rel_supp [lemma, in CTL.demo]
AR_ev_cond [lemma, in CTL.demo]
AR_rel_term [lemma, in CTL.demo]
AR_rel_succ [lemma, in CTL.demo]
AR_label [definition, in CTL.demo]
AR_rel [definition, in CTL.demo]
AR_T0 [definition, in CTL.demo]
AR_level [definition, in CTL.demo]
AR0 [constructor, in CTL.CTL_def]
AR1 [lemma, in CTL.agreement]
AR2 [lemma, in CTL.agreement]
AR3_0 [lemma, in CTL.agreement]
As [definition, in CTL.gen_dec]
AsAR [lemma, in CTL.gen_dec]
AsAU [lemma, in CTL.gen_dec]
AsAXR [lemma, in CTL.gen_dec]
AsAXU [lemma, in CTL.gen_dec]
AsV [lemma, in CTL.gen_dec]
AsX [lemma, in CTL.gen_dec]
AsX' [lemma, in CTL.gen_dec]
AUb [definition, in CTL.CTL_def]
AUb [abbreviation, in CTL.agreement]
AUH_hil [lemma, in CTL.hilbert_hist]
AUl [definition, in CTL.demo]
AUlE [lemma, in CTL.demo]
auP [lemma, in CTL.CTL_def]
auP2 [lemma, in CTL.agreement]
AUr [definition, in CTL.demo]
AUs [constructor, in CTL.CTL_def]
AUs [definition, in CTL.gen_dec]
AU_mono [lemma, in CTL.CTL_def]
AU_fun [definition, in CTL.CTL_def]
AU_strengthen [lemma, in CTL.CTL_def]
AU_shift [lemma, in CTL.gen_dec]
AU_ [definition, in CTL.hilbert_hist]
AU_rel_supp [lemma, in CTL.demo]
AU_rel_term [lemma, in CTL.demo]
AU_rel_succ [lemma, in CTL.demo]
AU_rel [definition, in CTL.demo]
AU_label [definition, in CTL.demo]
AU_T0 [definition, in CTL.demo]
AU_level [definition, in CTL.demo]
AU0 [constructor, in CTL.CTL_def]
AU1 [lemma, in CTL.agreement]
AU2 [lemma, in CTL.agreement]
aVoid [constructor, in CTL.gen_def]
axARdef [lemma, in CTL.hilbert_Eme90]
axARf [lemma, in CTL.hilbert_LS]
axAUcmp [lemma, in CTL.hilbert_LS]
axAUeq [lemma, in CTL.hilbert_Eme90]
axAUr [lemma, in CTL.hilbert_Eme90]
axAXdef [lemma, in CTL.hilbert_Eme90]
axAXT [lemma, in CTL.hilbert_Eme90]
axERf [lemma, in CTL.hilbert_LS]
axEUeq [lemma, in CTL.hilbert_Eme90]
axEUr [lemma, in CTL.hilbert_Eme90]
axEXAXI [lemma, in CTL.hilbert_Eme90]
axEXD [lemma, in CTL.hilbert_Eme90]
AXn [definition, in CTL.demo]
AXn_complete_DD [lemma, in CTL.relaxed_pruning]
AXn_complete [definition, in CTL.demo]
axReg [lemma, in CTL.hilbert_Eme90]
AXR_shift [lemma, in CTL.gen_dec]
axSer [lemma, in CTL.hilbert_LS]
axSer [lemma, in CTL.hilbert_Eme90]
AXU_shift [lemma, in CTL.gen_dec]
ax_ReqR [lemma, in CTL.hilbert_ref]
ax_Req [lemma, in CTL.hilbert_ref]
ax_lcons [lemma, in CTL.hilbert_ref]
B
baseP [lemma, in CTL.hilbert_ref]base0P [lemma, in CTL.hilbert_ref]
body [definition, in CTL.CTL_def]
bounded_step [lemma, in CTL.gen_dec]
bounded_demo [definition, in CTL.demo]
bounded_fulfillAR_step [lemma, in CTL.demo]
bounded_fulfillAU_step [lemma, in CTL.demo]
C
cAR [inductive, in CTL.CTL_def]cAR_cEU [lemma, in CTL.CTL_def]
cAU [inductive, in CTL.CTL_def]
cAU_eq [lemma, in CTL.CTL_def]
cAU_cER [lemma, in CTL.CTL_def]
cAX [definition, in CTL.CTL_def]
cER [inductive, in CTL.CTL_def]
cEU [inductive, in CTL.CTL_def]
cEU_eq [lemma, in CTL.CTL_def]
cEX [definition, in CTL.CTL_def]
Characterizations [section, in CTL.CTL_def]
Characterizations.e [variable, in CTL.CTL_def]
Characterizations.X [variable, in CTL.CTL_def]
clause [definition, in CTL.CTL_def]
closed_sfc [lemma, in CTL.CTL_def]
cmodel [record, in CTL.CTL_def]
CModel [constructor, in CTL.CTL_def]
cmodel_of_fmodel [definition, in CTL.CTL_def]
connect_subtype [lemma, in CTL.dags]
coref [definition, in CTL.relaxed_pruning]
corefD1 [lemma, in CTL.relaxed_pruning]
coref_supp [lemma, in CTL.hilbert_ref]
coref_DD [lemma, in CTL.relaxed_pruning]
Cs [definition, in CTL.gen_dec]
CTL_def [library]
D
dags [library]DC [definition, in CTL.CTL_def]
DC_required [lemma, in CTL.results]
DC_ [definition, in CTL.CTL_def]
DC_required [lemma, in CTL.agreement]
DD [definition, in CTL.relaxed_pruning]
DD_refute [lemma, in CTL.relaxed_pruning]
DD_sat [lemma, in CTL.relaxed_pruning]
DD_small_model [lemma, in CTL.relaxed_pruning]
DD_size [lemma, in CTL.relaxed_pruning]
DD_fragment_bound [lemma, in CTL.demo]
DD_demo [definition, in CTL.demo]
DD_demo_aux [lemma, in CTL.demo]
DD_bounded_demo [lemma, in CTL.demo]
Decidability [section, in CTL.CTL_def]
Decidability.e [variable, in CTL.CTL_def]
Decidability.p [variable, in CTL.CTL_def]
Decidability.q [variable, in CTL.CTL_def]
Decidability.T [variable, in CTL.CTL_def]
demo [record, in CTL.demo]
Demo [constructor, in CTL.demo]
demo [library]
demoDD_S0 [lemma, in CTL.relaxed_pruning]
demoSsubT [projection, in CTL.demo]
demoT [projection, in CTL.demo]
DemoToFragment [section, in CTL.demo]
DemoToFragment.demoST [variable, in CTL.demo]
DemoToFragment.Fragments [section, in CTL.demo]
DemoToFragment.Fragments.s [variable, in CTL.demo]
DemoToFragment.Fragments.t [variable, in CTL.demo]
DemoToFragment.S [variable, in CTL.demo]
DemoToFragment.T [variable, in CTL.demo]
demo1 [projection, in CTL.demo]
demo2 [projection, in CTL.demo]
demo3 [projection, in CTL.demo]
DG1 [projection, in CTL.demo]
DG2 [projection, in CTL.demo]
DG3 [projection, in CTL.demo]
DG4 [projection, in CTL.demo]
DG5 [projection, in CTL.demo]
DG6 [projection, in CTL.demo]
DG7 [projection, in CTL.demo]
Disjoint [section, in CTL.dags]
Disjoint.G [variable, in CTL.dags]
Disjoint.I [variable, in CTL.dags]
Disjoint.L [variable, in CTL.dags]
dmAll [lemma, in CTL.agreement]
dmAR [lemma, in CTL.agreement]
dmAU [lemma, in CTL.agreement]
dmpAR [lemma, in CTL.agreement]
dn [lemma, in CTL.agreement]
E
edge [projection, in CTL.dags]Eme90 [module, in CTL.hilbert_Eme90]
Eme90_sound [lemma, in CTL.hilbert_Eme90]
Eme90_translation [lemma, in CTL.hilbert_Eme90]
Eme90.AR_ind [lemma, in CTL.hilbert_Eme90]
Eme90.AU_ind [lemma, in CTL.hilbert_Eme90]
Eme90.AU_ind_aux [lemma, in CTL.hilbert_Eme90]
Eme90.axABBA [lemma, in CTL.hilbert_Eme90]
Eme90.axARdef [lemma, in CTL.hilbert_Eme90]
Eme90.axARdef' [constructor, in CTL.hilbert_Eme90]
Eme90.axARE [lemma, in CTL.hilbert_Eme90]
Eme90.axARu [lemma, in CTL.hilbert_Eme90]
Eme90.axAUeq [lemma, in CTL.hilbert_Eme90]
Eme90.axAUeq' [constructor, in CTL.hilbert_Eme90]
Eme90.axAUf [lemma, in CTL.hilbert_Eme90]
Eme90.axAUI [lemma, in CTL.hilbert_Eme90]
Eme90.axAUr [lemma, in CTL.hilbert_Eme90]
Eme90.axAUr' [constructor, in CTL.hilbert_Eme90]
Eme90.axAXdef [lemma, in CTL.hilbert_Eme90]
Eme90.axAXdef' [constructor, in CTL.hilbert_Eme90]
Eme90.axAXT [constructor, in CTL.hilbert_Eme90]
Eme90.axDN [constructor, in CTL.hilbert_Eme90]
Eme90.axEUeq [lemma, in CTL.hilbert_Eme90]
Eme90.axEUeq' [constructor, in CTL.hilbert_Eme90]
Eme90.axEUr [lemma, in CTL.hilbert_Eme90]
Eme90.axEUr' [constructor, in CTL.hilbert_Eme90]
Eme90.axEXD [lemma, in CTL.hilbert_Eme90]
Eme90.axEXD' [constructor, in CTL.hilbert_Eme90]
Eme90.axK [constructor, in CTL.hilbert_Eme90]
Eme90.axN [lemma, in CTL.hilbert_Eme90]
Eme90.axReg [lemma, in CTL.hilbert_Eme90]
Eme90.axReg' [constructor, in CTL.hilbert_Eme90]
Eme90.axS [constructor, in CTL.hilbert_Eme90]
Eme90.axSer [lemma, in CTL.hilbert_Eme90]
Eme90.axSer' [constructor, in CTL.hilbert_Eme90]
Eme90.ax_serial [lemma, in CTL.hilbert_Eme90]
Eme90.fAG [definition, in CTL.hilbert_Eme90]
Eme90.fEU [definition, in CTL.hilbert_Eme90]
Eme90.fEX [definition, in CTL.hilbert_Eme90]
Eme90.Hilbert [section, in CTL.hilbert_Eme90]
_ <--> _ [notation, in CTL.hilbert_Eme90]
_ :/\: _ [notation, in CTL.hilbert_Eme90]
_ :\/: _ [notation, in CTL.hilbert_Eme90]
_ ---> _ [notation, in CTL.hilbert_Eme90]
~~: _ [notation, in CTL.hilbert_Eme90]
Eme90.prv [inductive, in CTL.hilbert_Eme90]
Eme90.rGen [constructor, in CTL.hilbert_Eme90]
Eme90.rMP [constructor, in CTL.hilbert_Eme90]
Eme90.rNec [lemma, in CTL.hilbert_Eme90]
Eme90.rRegAX [lemma, in CTL.hilbert_Eme90]
Eme90.rRegEX [lemma, in CTL.hilbert_Eme90]
eq_form_dec [lemma, in CTL.CTL_def]
eq_annot_dec [lemma, in CTL.gen_def]
ERel [lemma, in CTL.hilbert_LS]
erel [definition, in CTL.dags]
ERs [constructor, in CTL.CTL_def]
ER_strengthen [lemma, in CTL.CTL_def]
ER0 [constructor, in CTL.CTL_def]
ER1 [lemma, in CTL.agreement]
ER2 [lemma, in CTL.agreement]
EUs [constructor, in CTL.CTL_def]
EU_strengthen [lemma, in CTL.CTL_def]
EU_ [definition, in CTL.hilbert_hist]
EU0 [constructor, in CTL.CTL_def]
EU1 [lemma, in CTL.agreement]
EU2 [lemma, in CTL.agreement]
eval [definition, in CTL.CTL_def]
evalb [definition, in CTL.CTL_def]
evalP [lemma, in CTL.CTL_def]
evalP2 [lemma, in CTL.results]
evalP2 [lemma, in CTL.agreement]
evP [lemma, in CTL.demo]
ev_x [constructor, in CTL.demo]
ev_AU [constructor, in CTL.demo]
ev_AR [constructor, in CTL.demo]
ev_case [inductive, in CTL.demo]
ev_cond [definition, in CTL.demo]
F
fAR [constructor, in CTL.CTL_def]fAU [constructor, in CTL.CTL_def]
fAX [constructor, in CTL.CTL_def]
fd_lcons [projection, in CTL.demo]
fd_sub [projection, in CTL.demo]
fd_trees [projection, in CTL.demo]
fF [constructor, in CTL.CTL_def]
fImp [constructor, in CTL.CTL_def]
FiniteModels [section, in CTL.CTL_def]
FiniteModels.M [variable, in CTL.CTL_def]
fin_path_soundness [lemma, in CTL.results]
fin_completeness [lemma, in CTL.results]
fin_modelP [lemma, in CTL.CTL_def]
fin_completeness [lemma, in CTL.hilbert_ref]
flabel [projection, in CTL.CTL_def]
fmodel [record, in CTL.CTL_def]
FModel [constructor, in CTL.CTL_def]
form [inductive, in CTL.CTL_def]
formChoice [module, in CTL.CTL_def]
formChoice.pickle [definition, in CTL.CTL_def]
formChoice.pickleP [lemma, in CTL.CTL_def]
formChoice.unpickle [definition, in CTL.CTL_def]
form_slClass [definition, in CTL.CTL_def]
form_choiceMixin [definition, in CTL.CTL_def]
form_countMixin [definition, in CTL.CTL_def]
form_eqMixin [definition, in CTL.CTL_def]
fragment [record, in CTL.demo]
FragmentDemo [constructor, in CTL.demo]
FragmentDemo [section, in CTL.demo]
FragmentDemo.S [variable, in CTL.demo]
FragmentDemo.T [variable, in CTL.demo]
fragment_bound [definition, in CTL.demo]
fragment_demo [record, in CTL.demo]
frag_AR [lemma, in CTL.demo]
frag_AU [lemma, in CTL.demo]
Fs [definition, in CTL.demo]
fser [projection, in CTL.CTL_def]
fstate [projection, in CTL.CTL_def]
Fsub [lemma, in CTL.relaxed_pruning]
Fs_size [lemma, in CTL.relaxed_pruning]
ftrans [projection, in CTL.CTL_def]
fulfillAR_step [definition, in CTL.demo]
fulfillAU_step [definition, in CTL.demo]
Fulfillment [section, in CTL.demo]
Fulfillment.S [variable, in CTL.demo]
Fulfillment.T [variable, in CTL.demo]
fulfillsAR [definition, in CTL.demo]
fulfillsARE [definition, in CTL.demo]
fulfillsAREn [lemma, in CTL.gen_ref]
fulfillsAR_DD [lemma, in CTL.relaxed_pruning]
fulfillsAU [definition, in CTL.demo]
fulfillsAUE [definition, in CTL.demo]
fulfillsAUEn [lemma, in CTL.gen_ref]
fulfillsAU_DD [lemma, in CTL.relaxed_pruning]
fV [constructor, in CTL.CTL_def]
f_size [definition, in CTL.CTL_def]
f_weight [definition, in CTL.CTL_def]
G
gen [inductive, in CTL.gen_def]genU_aAXR [lemma, in CTL.gen_dec]
genU_foc' [lemma, in CTL.gen_dec]
genU_ARhr [lemma, in CTL.gen_dec]
genU_ARhl [lemma, in CTL.gen_dec]
genU_ARnr [lemma, in CTL.gen_dec]
genU_ARnl [lemma, in CTL.gen_dec]
genU_ARpr [lemma, in CTL.gen_dec]
genU_ARpl [lemma, in CTL.gen_dec]
genU_jmp [lemma, in CTL.gen_dec]
genU_AUhr [lemma, in CTL.gen_dec]
genU_AUhl [lemma, in CTL.gen_dec]
genU_foc [lemma, in CTL.gen_dec]
genU_AUnr [lemma, in CTL.gen_dec]
genU_AUnl [lemma, in CTL.gen_dec]
genU_AUpr [lemma, in CTL.gen_dec]
genU_AUpl [lemma, in CTL.gen_dec]
genU_AXn [lemma, in CTL.gen_dec]
genU_aR [lemma, in CTL.gen_dec]
genU_in [lemma, in CTL.gen_dec]
genU_ipr [lemma, in CTL.gen_dec]
genU_ipl [lemma, in CTL.gen_dec]
gen_dec [lemma, in CTL.results]
gen_complete [lemma, in CTL.results]
gen_complete [lemma, in CTL.gen_ref]
gen_dec [lemma, in CTL.gen_dec]
gen_decF [lemma, in CTL.gen_dec]
gen_closure.RinU [variable, in CTL.gen_dec]
gen_closure.sfc_F [variable, in CTL.gen_dec]
gen_closure.F [variable, in CTL.gen_dec]
gen_closure [section, in CTL.gen_dec]
gen_jmp [constructor, in CTL.gen_def]
gen_aAXR [constructor, in CTL.gen_def]
gen_ARrep [constructor, in CTL.gen_def]
gen_ARh [constructor, in CTL.gen_def]
gen_ARfoc [constructor, in CTL.gen_def]
gen_ARn [constructor, in CTL.gen_def]
gen_ARp [constructor, in CTL.gen_def]
gen_AUrep [constructor, in CTL.gen_def]
gen_AUh [constructor, in CTL.gen_def]
gen_AUfoc [constructor, in CTL.gen_def]
gen_AUn [constructor, in CTL.gen_def]
gen_AUp [constructor, in CTL.gen_def]
gen_AXn [constructor, in CTL.gen_def]
gen_In [constructor, in CTL.gen_def]
gen_Ip [constructor, in CTL.gen_def]
gen_p [constructor, in CTL.gen_def]
gen_F [constructor, in CTL.gen_def]
gen_ref [library]
gen_hsound [library]
gen_dec [library]
gen_def [library]
glabels_from [definition, in CTL.demo]
glocal [definition, in CTL.dags]
graph [record, in CTL.dags]
Graph [constructor, in CTL.dags]
GraphTheory [section, in CTL.dags]
GraphTheory.L [variable, in CTL.dags]
GraphTheory.p [variable, in CTL.dags]
graph_of [projection, in CTL.dags]
H
hilbert [library]hilbert_soundness [lemma, in CTL.gen_hsound]
hilbert_hist [library]
hilbert_ref [library]
hilbert_Eme90 [library]
hilbert_LS [library]
hist [definition, in CTL.gen_hsound]
histU [lemma, in CTL.gen_hsound]
hist0 [lemma, in CTL.gen_hsound]
href [definition, in CTL.hilbert_ref]
href_translation [lemma, in CTL.hilbert_ref]
Hs [definition, in CTL.gen_dec]
I
IC [module, in CTL.hilbert]IC_Eme90_equivalence [lemma, in CTL.results]
IC_LS_equivalence [lemma, in CTL.results]
IC_soundness [lemma, in CTL.results]
IC.AU_ind [constructor, in CTL.hilbert]
IC.axARE [constructor, in CTL.hilbert]
IC.axARu [constructor, in CTL.hilbert]
IC.axAUf [constructor, in CTL.hilbert]
IC.axAUI [constructor, in CTL.hilbert]
IC.axDN [constructor, in CTL.hilbert]
IC.axK [constructor, in CTL.hilbert]
IC.axN [constructor, in CTL.hilbert]
IC.axS [constructor, in CTL.hilbert]
IC.ax_serial [constructor, in CTL.hilbert]
IC.box_request [lemma, in CTL.hilbert]
IC.Hilbert [section, in CTL.hilbert]
_ ---> _ [notation, in CTL.hilbert]
IC.prv [inductive, in CTL.hilbert]
IC.rAR_ind [constructor, in CTL.hilbert]
IC.rMP [constructor, in CTL.hilbert]
IC.rNec [constructor, in CTL.hilbert]
IC.soundness [lemma, in CTL.hilbert]
informative_completeness [lemma, in CTL.results]
informative_completeness [lemma, in CTL.hilbert_ref]
inhab_Req [lemma, in CTL.demo]
interp_a [definition, in CTL.gen_hsound]
interp' [definition, in CTL.demo]
in_Req [lemma, in CTL.demo]
isBox [definition, in CTL.CTL_def]
isBoxP [lemma, in CTL.CTL_def]
isBox_false [constructor, in CTL.CTL_def]
isBox_true [constructor, in CTL.CTL_def]
isBox_spec [inductive, in CTL.CTL_def]
isDia [definition, in CTL.CTL_def]
isDiaP [lemma, in CTL.CTL_def]
isDia_false [constructor, in CTL.CTL_def]
isDia_true [constructor, in CTL.CTL_def]
isDia_spec [inductive, in CTL.CTL_def]
L
label [projection, in CTL.CTL_def]label [projection, in CTL.dags]
lcons [definition, in CTL.CTL_def]
lcons_gen [lemma, in CTL.gen_ref]
ldec [definition, in CTL.CTL_def]
leaf [definition, in CTL.dags]
liftE [lemma, in CTL.dags]
lift_connect [lemma, in CTL.dags]
lift_eqn [lemma, in CTL.dags]
lift_eq [lemma, in CTL.dags]
lift_edge [definition, in CTL.dags]
literal [definition, in CTL.CTL_def]
LPO [section, in CTL.results]
LPO [section, in CTL.agreement]
LPO_of_disjunctive_AR [lemma, in CTL.results]
LPO_of_disjunctive_AR [lemma, in CTL.agreement]
LPO.f [variable, in CTL.agreement]
LPO.hyp_AR [variable, in CTL.results]
LPO.hyp_AR [variable, in CTL.agreement]
LS [module, in CTL.hilbert_LS]
LS_sound [lemma, in CTL.hilbert_LS]
LS_translation [lemma, in CTL.hilbert_LS]
LS.ARel [lemma, in CTL.hilbert_LS]
LS.ARel' [constructor, in CTL.hilbert_LS]
LS.ARI [lemma, in CTL.hilbert_LS]
LS.AR_ind [lemma, in CTL.hilbert_LS]
LS.AU_ind [lemma, in CTL.hilbert_LS]
LS.axARE [lemma, in CTL.hilbert_LS]
LS.axARf [lemma, in CTL.hilbert_LS]
LS.axARf' [constructor, in CTL.hilbert_LS]
LS.axARu [lemma, in CTL.hilbert_LS]
LS.axAUcmp [lemma, in CTL.hilbert_LS]
LS.axAUcmp' [constructor, in CTL.hilbert_LS]
LS.axAUf [lemma, in CTL.hilbert_LS]
LS.axAUI [lemma, in CTL.hilbert_LS]
LS.axDN [constructor, in CTL.hilbert_LS]
LS.axERf [lemma, in CTL.hilbert_LS]
LS.axERf' [constructor, in CTL.hilbert_LS]
LS.axK [constructor, in CTL.hilbert_LS]
LS.axN [constructor, in CTL.hilbert_LS]
LS.axS [constructor, in CTL.hilbert_LS]
LS.axSer [constructor, in CTL.hilbert_LS]
LS.ax_serial [lemma, in CTL.hilbert_LS]
LS.ERel [lemma, in CTL.hilbert_LS]
LS.ERel' [constructor, in CTL.hilbert_LS]
LS.ERI [lemma, in CTL.hilbert_LS]
LS.fER [definition, in CTL.hilbert_LS]
LS.fEX [definition, in CTL.hilbert_LS]
LS.Hilbert [section, in CTL.hilbert_LS]
_ <--> _ [notation, in CTL.hilbert_LS]
_ :/\: _ [notation, in CTL.hilbert_LS]
_ :\/: _ [notation, in CTL.hilbert_LS]
_ ---> _ [notation, in CTL.hilbert_LS]
~~: _ [notation, in CTL.hilbert_LS]
LS.prv [inductive, in CTL.hilbert_LS]
LS.rMP [constructor, in CTL.hilbert_LS]
LS.rNec [constructor, in CTL.hilbert_LS]
L3 [definition, in CTL.agreement]
M
ModelConstruction [module, in CTL.demo]ModelConstruction.AU_lift [lemma, in CTL.demo]
ModelConstruction.AU_this [lemma, in CTL.demo]
ModelConstruction.AU_M [definition, in CTL.demo]
ModelConstruction.dag_D [lemma, in CTL.demo]
ModelConstruction.dag_R [lemma, in CTL.demo]
ModelConstruction.DC [definition, in CTL.demo]
ModelConstruction.DF [definition, in CTL.demo]
ModelConstruction.dmat_ev_cond [lemma, in CTL.demo]
ModelConstruction.EU_lift [lemma, in CTL.demo]
ModelConstruction.EU_this [lemma, in CTL.demo]
ModelConstruction.EU_M [definition, in CTL.demo]
ModelConstruction.Frag [definition, in CTL.demo]
ModelConstruction.FragP [lemma, in CTL.demo]
ModelConstruction.label_lcon [lemma, in CTL.demo]
ModelConstruction.label_Dl [lemma, in CTL.demo]
ModelConstruction.label_root [lemma, in CTL.demo]
ModelConstruction.label_DF [lemma, in CTL.demo]
ModelConstruction.leaf_root' [lemma, in CTL.demo]
ModelConstruction.leaf_root [lemma, in CTL.demo]
ModelConstruction.leaf_root_aux [lemma, in CTL.demo]
ModelConstruction.MD [definition, in CTL.demo]
ModelConstruction.MD_size [lemma, in CTL.demo]
ModelConstruction.MLabel [definition, in CTL.demo]
ModelConstruction.ModelConstruction [section, in CTL.demo]
ModelConstruction.ModelConstruction.D [variable, in CTL.demo]
ModelConstruction.ModelConstruction.Dl [variable, in CTL.demo]
ModelConstruction.ModelConstruction.FD [variable, in CTL.demo]
ModelConstruction.model_existence [lemma, in CTL.demo]
ModelConstruction.MRel [definition, in CTL.demo]
ModelConstruction.MRel_D [lemma, in CTL.demo]
ModelConstruction.MRel_R [lemma, in CTL.demo]
ModelConstruction.Mstate [definition, in CTL.demo]
ModelConstruction.MType [definition, in CTL.demo]
ModelConstruction.rlabel_Fs [lemma, in CTL.demo]
ModelConstruction.root_internal [lemma, in CTL.demo]
ModelConstruction.serial_MRel [lemma, in CTL.demo]
ModelConstruction.small_model_existence [lemma, in CTL.demo]
ModelConstruction.sn_edge [lemma, in CTL.demo]
ModelConstruction.supp_eval [lemma, in CTL.demo]
ModelConstruction.supp_edge [lemma, in CTL.demo]
modelP [projection, in CTL.CTL_def]
monotone_fulfillAR_step [lemma, in CTL.demo]
monotone_fulfillAU_step [lemma, in CTL.demo]
mono_step [lemma, in CTL.gen_dec]
M3 [definition, in CTL.agreement]
N
negative [definition, in CTL.CTL_def]negatives [definition, in CTL.CTL_def]
negE [lemma, in CTL.CTL_def]
nImp [lemma, in CTL.agreement]
P
pAR [definition, in CTL.CTL_def]pAR [definition, in CTL.relaxed_pruning]
pARE1 [lemma, in CTL.agreement]
pARE2 [lemma, in CTL.agreement]
pAR_strengthen [lemma, in CTL.CTL_def]
pAR_pEU [lemma, in CTL.CTL_def]
pAR' [definition, in CTL.agreement]
path [definition, in CTL.CTL_def]
Paths [section, in CTL.agreement]
Paths.P [variable, in CTL.agreement]
Paths.Q [variable, in CTL.agreement]
Paths.R [variable, in CTL.agreement]
Paths.R_serial [variable, in CTL.agreement]
Paths.X [variable, in CTL.agreement]
Paths2 [section, in CTL.agreement]
Paths2.R [variable, in CTL.agreement]
Paths2.R_serial [variable, in CTL.agreement]
Paths2.X [variable, in CTL.agreement]
path_ptail [lemma, in CTL.CTL_def]
path_pcons [lemma, in CTL.CTL_def]
path_pi3 [lemma, in CTL.agreement]
pAU [definition, in CTL.CTL_def]
pAU [definition, in CTL.relaxed_pruning]
pAU_strengthen [lemma, in CTL.CTL_def]
pAU_pER [lemma, in CTL.CTL_def]
pAXn [definition, in CTL.relaxed_pruning]
pcond [definition, in CTL.relaxed_pruning]
pcons [definition, in CTL.CTL_def]
pER [definition, in CTL.CTL_def]
pER_strengthen [lemma, in CTL.CTL_def]
pEU [definition, in CTL.CTL_def]
pEU_strengthen [lemma, in CTL.CTL_def]
pi3 [definition, in CTL.agreement]
plainP [lemma, in CTL.gen_dec]
plain_soundness [lemma, in CTL.results]
plain_soundness [lemma, in CTL.gen_hsound]
plain_inU [lemma, in CTL.gen_dec]
posE [lemma, in CTL.CTL_def]
positive [definition, in CTL.CTL_def]
positives [definition, in CTL.CTL_def]
PredC [definition, in CTL.CTL_def]
Prune [section, in CTL.relaxed_pruning]
Prune.F [variable, in CTL.relaxed_pruning]
Prune.sfc_F [variable, in CTL.relaxed_pruning]
prv_dec [lemma, in CTL.results]
prv_dec [lemma, in CTL.hilbert_ref]
prv_ER [lemma, in CTL.agreement]
ptail [definition, in CTL.CTL_def]
p_release [definition, in CTL.CTL_def]
p_until [definition, in CTL.CTL_def]
p_release' [definition, in CTL.agreement]
R
R [definition, in CTL.CTL_def]RE [lemma, in CTL.CTL_def]
ref [inductive, in CTL.relaxed_pruning]
refE1n [lemma, in CTL.hilbert_ref]
refI1n [lemma, in CTL.hilbert_ref]
RefPred [section, in CTL.hilbert_ref]
RefPred [section, in CTL.gen_ref]
refpred_ref' [lemma, in CTL.gen_ref]
RefPred.EventualityRefutations [section, in CTL.hilbert_ref]
RefPred.EventualityRefutations.coref_S [variable, in CTL.hilbert_ref]
RefPred.EventualityRefutations.S [variable, in CTL.hilbert_ref]
RefPred.EventualityRefutations.sub_S [variable, in CTL.hilbert_ref]
RefPred.F [variable, in CTL.hilbert_ref]
RefPred.F [variable, in CTL.gen_ref]
RefPred.sfc_F [variable, in CTL.hilbert_ref]
RefPred.sfc_F [variable, in CTL.gen_ref]
ref_compl [lemma, in CTL.relaxed_pruning]
ref_R3 [lemma, in CTL.gen_ref]
ref_R3_aux [lemma, in CTL.gen_ref]
ref_R4 [lemma, in CTL.gen_ref]
ref_R4_aux [lemma, in CTL.gen_ref]
ref_R2 [lemma, in CTL.gen_ref]
ref_R1 [lemma, in CTL.gen_ref]
ref_R0 [lemma, in CTL.gen_ref]
ref' [definition, in CTL.gen_ref]
relaxed_pruning [library]
relT [definition, in CTL.demo]
Req [definition, in CTL.demo]
ReqU [lemma, in CTL.relaxed_pruning]
req_cond [definition, in CTL.demo]
Req_RC [lemma, in CTL.demo]
respects [definition, in CTL.dags]
restrict [definition, in CTL.dags]
results [library]
rGen [lemma, in CTL.hilbert_Eme90]
rGraph [record, in CTL.dags]
RGraph [constructor, in CTL.dags]
RinU [lemma, in CTL.CTL_def]
root [projection, in CTL.dags]
rootP [projection, in CTL.dags]
Rpos [lemma, in CTL.CTL_def]
RU [lemma, in CTL.CTL_def]
R0 [lemma, in CTL.CTL_def]
R1 [lemma, in CTL.CTL_def]
R1 [constructor, in CTL.relaxed_pruning]
R2 [constructor, in CTL.relaxed_pruning]
R3 [constructor, in CTL.relaxed_pruning]
R3 [definition, in CTL.agreement]
R4 [constructor, in CTL.relaxed_pruning]
S
satisfies [definition, in CTL.CTL_def]sat_dec [lemma, in CTL.results]
sat_dec [lemma, in CTL.hilbert_ref]
serial [projection, in CTL.CTL_def]
serial_relT [lemma, in CTL.demo]
ser_R3 [lemma, in CTL.agreement]
sfc [definition, in CTL.CTL_def]
sfcU [lemma, in CTL.CTL_def]
sfc_bigcup [lemma, in CTL.CTL_def]
sfc_ssub [lemma, in CTL.CTL_def]
sform [definition, in CTL.CTL_def]
sf_ssub [lemma, in CTL.CTL_def]
sf_closed'_mon [lemma, in CTL.CTL_def]
sf_closed [definition, in CTL.CTL_def]
sf_closed' [definition, in CTL.CTL_def]
sf_AR [lemma, in CTL.gen_dec]
sf_AU [lemma, in CTL.gen_dec]
simple_frag [lemma, in CTL.demo]
size_ssub [lemma, in CTL.CTL_def]
small_models [lemma, in CTL.results]
small_models [lemma, in CTL.hilbert_ref]
small_models [lemma, in CTL.demo]
SN [constructor, in CTL.dags]
sn [inductive, in CTL.dags]
sn_preimage [lemma, in CTL.dags]
soundness [lemma, in CTL.results]
Soundness [section, in CTL.agreement]
Soundness.dc [variable, in CTL.agreement]
Soundness.xm [variable, in CTL.agreement]
ssub [definition, in CTL.CTL_def]
SsubU [lemma, in CTL.relaxed_pruning]
ssub_refl [lemma, in CTL.CTL_def]
ssub' [definition, in CTL.CTL_def]
ssub'_refl [lemma, in CTL.CTL_def]
stable [definition, in CTL.CTL_def]
star [inductive, in CTL.dags]
StarL [constructor, in CTL.dags]
Star0 [constructor, in CTL.dags]
state [projection, in CTL.CTL_def]
step [definition, in CTL.gen_dec]
stepP [lemma, in CTL.gen_dec]
step_jmp [definition, in CTL.gen_dec]
step_annot [definition, in CTL.gen_dec]
step_plain [definition, in CTL.gen_dec]
step_plain_cases [definition, in CTL.gen_dec]
sts [record, in CTL.CTL_def]
STS [constructor, in CTL.CTL_def]
sts_agreement [lemma, in CTL.results]
sts_of [projection, in CTL.CTL_def]
sts_path_soundness [lemma, in CTL.agreement]
sts_agreement [lemma, in CTL.agreement]
subCs [lemma, in CTL.gen_dec]
subDD [definition, in CTL.relaxed_pruning]
subU [lemma, in CTL.gen_dec]
sub_sfc [lemma, in CTL.CTL_def]
supp [definition, in CTL.CTL_def]
suppC1 [lemma, in CTL.CTL_def]
suppE [lemma, in CTL.CTL_def]
supp_lit [lemma, in CTL.CTL_def]
supp_mon [lemma, in CTL.CTL_def]
supp_cond [definition, in CTL.demo]
supp0F [lemma, in CTL.CTL_def]
sweight_lit [lemma, in CTL.CTL_def]
s_weight [definition, in CTL.CTL_def]
S0 [abbreviation, in CTL.hilbert_ref]
S0 [definition, in CTL.relaxed_pruning]
S0 [abbreviation, in CTL.gen_ref]
T
terminates [definition, in CTL.dags]terminates_measure [lemma, in CTL.dags]
terminates_gtn [lemma, in CTL.dags]
trans [projection, in CTL.CTL_def]
U
U [abbreviation, in CTL.hilbert_ref]U [definition, in CTL.relaxed_pruning]
U [abbreviation, in CTL.gen_ref]
U [definition, in CTL.gen_dec]
unfulfilledAR_refute [lemma, in CTL.hilbert_ref]
unfulfilledAU_refute [lemma, in CTL.hilbert_ref]
unit_model [definition, in CTL.demo]
V
valid_dec [lemma, in CTL.results]valid_dec [lemma, in CTL.hilbert_ref]
var [definition, in CTL.CTL_def]
vertex [projection, in CTL.dags]
X
xaf [abbreviation, in CTL.hilbert_ref]xaf [abbreviation, in CTL.gen_ref]
xchoose_rel [lemma, in CTL.agreement]
XM_required [lemma, in CTL.results]
XM_required [lemma, in CTL.agreement]
other
_ |> _ [notation, in CTL.CTL_def]_ |> _ ^- [notation, in CTL.CTL_def]
_ |> _ ^+ [notation, in CTL.CTL_def]
_ |> _ ^ _ [notation, in CTL.CTL_def]
_ ^+ [notation, in CTL.CTL_def]
_ ^- [notation, in CTL.CTL_def]
_ =p _ [notation, in CTL.CTL_def]
Notation Index
E
_ <--> _ [in CTL.hilbert_Eme90]_ :/\: _ [in CTL.hilbert_Eme90]
_ :\/: _ [in CTL.hilbert_Eme90]
_ ---> _ [in CTL.hilbert_Eme90]
~~: _ [in CTL.hilbert_Eme90]
I
_ ---> _ [in CTL.hilbert]L
_ <--> _ [in CTL.hilbert_LS]_ :/\: _ [in CTL.hilbert_LS]
_ :\/: _ [in CTL.hilbert_LS]
_ ---> _ [in CTL.hilbert_LS]
~~: _ [in CTL.hilbert_LS]
other
_ |> _ [in CTL.CTL_def]_ |> _ ^- [in CTL.CTL_def]
_ |> _ ^+ [in CTL.CTL_def]
_ |> _ ^ _ [in CTL.CTL_def]
_ ^+ [in CTL.CTL_def]
_ ^- [in CTL.CTL_def]
_ =p _ [in CTL.CTL_def]
Module Index
A
Annot [in CTL.gen_def]E
Eme90 [in CTL.hilbert_Eme90]F
formChoice [in CTL.CTL_def]I
IC [in CTL.hilbert]L
LS [in CTL.hilbert_LS]M
ModelConstruction [in CTL.demo]Variable Index
A
Agreement.e [in CTL.agreement]Agreement.p [in CTL.agreement]
Agreement.q [in CTL.agreement]
Agreement.serial_e [in CTL.agreement]
Agreement.T [in CTL.agreement]
C
Characterizations.e [in CTL.CTL_def]Characterizations.X [in CTL.CTL_def]
D
Decidability.e [in CTL.CTL_def]Decidability.p [in CTL.CTL_def]
Decidability.q [in CTL.CTL_def]
Decidability.T [in CTL.CTL_def]
DemoToFragment.demoST [in CTL.demo]
DemoToFragment.Fragments.s [in CTL.demo]
DemoToFragment.Fragments.t [in CTL.demo]
DemoToFragment.S [in CTL.demo]
DemoToFragment.T [in CTL.demo]
Disjoint.G [in CTL.dags]
Disjoint.I [in CTL.dags]
Disjoint.L [in CTL.dags]
F
FiniteModels.M [in CTL.CTL_def]FragmentDemo.S [in CTL.demo]
FragmentDemo.T [in CTL.demo]
Fulfillment.S [in CTL.demo]
Fulfillment.T [in CTL.demo]
G
gen_closure.RinU [in CTL.gen_dec]gen_closure.sfc_F [in CTL.gen_dec]
gen_closure.F [in CTL.gen_dec]
GraphTheory.L [in CTL.dags]
GraphTheory.p [in CTL.dags]
L
LPO.f [in CTL.agreement]LPO.hyp_AR [in CTL.results]
LPO.hyp_AR [in CTL.agreement]
M
ModelConstruction.ModelConstruction.D [in CTL.demo]ModelConstruction.ModelConstruction.Dl [in CTL.demo]
ModelConstruction.ModelConstruction.FD [in CTL.demo]
P
Paths.P [in CTL.agreement]Paths.Q [in CTL.agreement]
Paths.R [in CTL.agreement]
Paths.R_serial [in CTL.agreement]
Paths.X [in CTL.agreement]
Paths2.R [in CTL.agreement]
Paths2.R_serial [in CTL.agreement]
Paths2.X [in CTL.agreement]
Prune.F [in CTL.relaxed_pruning]
Prune.sfc_F [in CTL.relaxed_pruning]
R
RefPred.EventualityRefutations.coref_S [in CTL.hilbert_ref]RefPred.EventualityRefutations.S [in CTL.hilbert_ref]
RefPred.EventualityRefutations.sub_S [in CTL.hilbert_ref]
RefPred.F [in CTL.hilbert_ref]
RefPred.F [in CTL.gen_ref]
RefPred.sfc_F [in CTL.hilbert_ref]
RefPred.sfc_F [in CTL.gen_ref]
S
Soundness.dc [in CTL.agreement]Soundness.xm [in CTL.agreement]
Library Index
A
agreementC
CTL_defD
dagsdemo
G
gen_refgen_hsound
gen_dec
gen_def
H
hilberthilbert_hist
hilbert_ref
hilbert_Eme90
hilbert_LS
R
relaxed_pruningresults
Lemma Index
A
aAR_inU [in CTL.gen_dec]aAU_inU [in CTL.gen_dec]
aAXR_inU [in CTL.gen_dec]
aAXU_inU [in CTL.gen_dec]
annot_request [in CTL.gen_hsound]
Annot.pickleP [in CTL.gen_def]
ARel [in CTL.hilbert_LS]
ARH_hil [in CTL.hilbert_hist]
ARlE [in CTL.demo]
arP [in CTL.CTL_def]
arP2 [in CTL.agreement]
AR_mono [in CTL.CTL_def]
AR_strengthen [in CTL.CTL_def]
AR_shift [in CTL.gen_dec]
AR_rel_supp [in CTL.demo]
AR_ev_cond [in CTL.demo]
AR_rel_term [in CTL.demo]
AR_rel_succ [in CTL.demo]
AR1 [in CTL.agreement]
AR2 [in CTL.agreement]
AR3_0 [in CTL.agreement]
AsAR [in CTL.gen_dec]
AsAU [in CTL.gen_dec]
AsAXR [in CTL.gen_dec]
AsAXU [in CTL.gen_dec]
AsV [in CTL.gen_dec]
AsX [in CTL.gen_dec]
AsX' [in CTL.gen_dec]
AUH_hil [in CTL.hilbert_hist]
AUlE [in CTL.demo]
auP [in CTL.CTL_def]
auP2 [in CTL.agreement]
AU_mono [in CTL.CTL_def]
AU_strengthen [in CTL.CTL_def]
AU_shift [in CTL.gen_dec]
AU_rel_supp [in CTL.demo]
AU_rel_term [in CTL.demo]
AU_rel_succ [in CTL.demo]
AU1 [in CTL.agreement]
AU2 [in CTL.agreement]
axARdef [in CTL.hilbert_Eme90]
axARf [in CTL.hilbert_LS]
axAUcmp [in CTL.hilbert_LS]
axAUeq [in CTL.hilbert_Eme90]
axAUr [in CTL.hilbert_Eme90]
axAXdef [in CTL.hilbert_Eme90]
axAXT [in CTL.hilbert_Eme90]
axERf [in CTL.hilbert_LS]
axEUeq [in CTL.hilbert_Eme90]
axEUr [in CTL.hilbert_Eme90]
axEXAXI [in CTL.hilbert_Eme90]
axEXD [in CTL.hilbert_Eme90]
AXn_complete_DD [in CTL.relaxed_pruning]
axReg [in CTL.hilbert_Eme90]
AXR_shift [in CTL.gen_dec]
axSer [in CTL.hilbert_LS]
axSer [in CTL.hilbert_Eme90]
AXU_shift [in CTL.gen_dec]
ax_ReqR [in CTL.hilbert_ref]
ax_Req [in CTL.hilbert_ref]
ax_lcons [in CTL.hilbert_ref]
B
baseP [in CTL.hilbert_ref]base0P [in CTL.hilbert_ref]
bounded_step [in CTL.gen_dec]
bounded_fulfillAR_step [in CTL.demo]
bounded_fulfillAU_step [in CTL.demo]
C
cAR_cEU [in CTL.CTL_def]cAU_eq [in CTL.CTL_def]
cAU_cER [in CTL.CTL_def]
cEU_eq [in CTL.CTL_def]
closed_sfc [in CTL.CTL_def]
connect_subtype [in CTL.dags]
corefD1 [in CTL.relaxed_pruning]
coref_supp [in CTL.hilbert_ref]
coref_DD [in CTL.relaxed_pruning]
D
DC_required [in CTL.results]DC_required [in CTL.agreement]
DD_refute [in CTL.relaxed_pruning]
DD_sat [in CTL.relaxed_pruning]
DD_small_model [in CTL.relaxed_pruning]
DD_size [in CTL.relaxed_pruning]
DD_fragment_bound [in CTL.demo]
DD_demo_aux [in CTL.demo]
DD_bounded_demo [in CTL.demo]
demoDD_S0 [in CTL.relaxed_pruning]
dmAll [in CTL.agreement]
dmAR [in CTL.agreement]
dmAU [in CTL.agreement]
dmpAR [in CTL.agreement]
dn [in CTL.agreement]
E
Eme90_sound [in CTL.hilbert_Eme90]Eme90_translation [in CTL.hilbert_Eme90]
Eme90.AR_ind [in CTL.hilbert_Eme90]
Eme90.AU_ind [in CTL.hilbert_Eme90]
Eme90.AU_ind_aux [in CTL.hilbert_Eme90]
Eme90.axABBA [in CTL.hilbert_Eme90]
Eme90.axARdef [in CTL.hilbert_Eme90]
Eme90.axARE [in CTL.hilbert_Eme90]
Eme90.axARu [in CTL.hilbert_Eme90]
Eme90.axAUeq [in CTL.hilbert_Eme90]
Eme90.axAUf [in CTL.hilbert_Eme90]
Eme90.axAUI [in CTL.hilbert_Eme90]
Eme90.axAUr [in CTL.hilbert_Eme90]
Eme90.axAXdef [in CTL.hilbert_Eme90]
Eme90.axEUeq [in CTL.hilbert_Eme90]
Eme90.axEUr [in CTL.hilbert_Eme90]
Eme90.axEXD [in CTL.hilbert_Eme90]
Eme90.axN [in CTL.hilbert_Eme90]
Eme90.axReg [in CTL.hilbert_Eme90]
Eme90.axSer [in CTL.hilbert_Eme90]
Eme90.ax_serial [in CTL.hilbert_Eme90]
Eme90.rNec [in CTL.hilbert_Eme90]
Eme90.rRegAX [in CTL.hilbert_Eme90]
Eme90.rRegEX [in CTL.hilbert_Eme90]
eq_form_dec [in CTL.CTL_def]
eq_annot_dec [in CTL.gen_def]
ERel [in CTL.hilbert_LS]
ER_strengthen [in CTL.CTL_def]
ER1 [in CTL.agreement]
ER2 [in CTL.agreement]
EU_strengthen [in CTL.CTL_def]
EU1 [in CTL.agreement]
EU2 [in CTL.agreement]
evalP [in CTL.CTL_def]
evalP2 [in CTL.results]
evalP2 [in CTL.agreement]
evP [in CTL.demo]
F
fin_path_soundness [in CTL.results]fin_completeness [in CTL.results]
fin_modelP [in CTL.CTL_def]
fin_completeness [in CTL.hilbert_ref]
formChoice.pickleP [in CTL.CTL_def]
frag_AR [in CTL.demo]
frag_AU [in CTL.demo]
Fsub [in CTL.relaxed_pruning]
Fs_size [in CTL.relaxed_pruning]
fulfillsAREn [in CTL.gen_ref]
fulfillsAR_DD [in CTL.relaxed_pruning]
fulfillsAUEn [in CTL.gen_ref]
fulfillsAU_DD [in CTL.relaxed_pruning]
G
genU_aAXR [in CTL.gen_dec]genU_foc' [in CTL.gen_dec]
genU_ARhr [in CTL.gen_dec]
genU_ARhl [in CTL.gen_dec]
genU_ARnr [in CTL.gen_dec]
genU_ARnl [in CTL.gen_dec]
genU_ARpr [in CTL.gen_dec]
genU_ARpl [in CTL.gen_dec]
genU_jmp [in CTL.gen_dec]
genU_AUhr [in CTL.gen_dec]
genU_AUhl [in CTL.gen_dec]
genU_foc [in CTL.gen_dec]
genU_AUnr [in CTL.gen_dec]
genU_AUnl [in CTL.gen_dec]
genU_AUpr [in CTL.gen_dec]
genU_AUpl [in CTL.gen_dec]
genU_AXn [in CTL.gen_dec]
genU_aR [in CTL.gen_dec]
genU_in [in CTL.gen_dec]
genU_ipr [in CTL.gen_dec]
genU_ipl [in CTL.gen_dec]
gen_dec [in CTL.results]
gen_complete [in CTL.results]
gen_complete [in CTL.gen_ref]
gen_dec [in CTL.gen_dec]
gen_decF [in CTL.gen_dec]
H
hilbert_soundness [in CTL.gen_hsound]histU [in CTL.gen_hsound]
hist0 [in CTL.gen_hsound]
href_translation [in CTL.hilbert_ref]
I
IC_Eme90_equivalence [in CTL.results]IC_LS_equivalence [in CTL.results]
IC_soundness [in CTL.results]
IC.box_request [in CTL.hilbert]
IC.soundness [in CTL.hilbert]
informative_completeness [in CTL.results]
informative_completeness [in CTL.hilbert_ref]
inhab_Req [in CTL.demo]
in_Req [in CTL.demo]
isBoxP [in CTL.CTL_def]
isDiaP [in CTL.CTL_def]
L
lcons_gen [in CTL.gen_ref]liftE [in CTL.dags]
lift_connect [in CTL.dags]
lift_eqn [in CTL.dags]
lift_eq [in CTL.dags]
LPO_of_disjunctive_AR [in CTL.results]
LPO_of_disjunctive_AR [in CTL.agreement]
LS_sound [in CTL.hilbert_LS]
LS_translation [in CTL.hilbert_LS]
LS.ARel [in CTL.hilbert_LS]
LS.ARI [in CTL.hilbert_LS]
LS.AR_ind [in CTL.hilbert_LS]
LS.AU_ind [in CTL.hilbert_LS]
LS.axARE [in CTL.hilbert_LS]
LS.axARf [in CTL.hilbert_LS]
LS.axARu [in CTL.hilbert_LS]
LS.axAUcmp [in CTL.hilbert_LS]
LS.axAUf [in CTL.hilbert_LS]
LS.axAUI [in CTL.hilbert_LS]
LS.axERf [in CTL.hilbert_LS]
LS.ax_serial [in CTL.hilbert_LS]
LS.ERel [in CTL.hilbert_LS]
LS.ERI [in CTL.hilbert_LS]
M
ModelConstruction.AU_lift [in CTL.demo]ModelConstruction.AU_this [in CTL.demo]
ModelConstruction.dag_D [in CTL.demo]
ModelConstruction.dag_R [in CTL.demo]
ModelConstruction.dmat_ev_cond [in CTL.demo]
ModelConstruction.EU_lift [in CTL.demo]
ModelConstruction.EU_this [in CTL.demo]
ModelConstruction.FragP [in CTL.demo]
ModelConstruction.label_lcon [in CTL.demo]
ModelConstruction.label_Dl [in CTL.demo]
ModelConstruction.label_root [in CTL.demo]
ModelConstruction.label_DF [in CTL.demo]
ModelConstruction.leaf_root' [in CTL.demo]
ModelConstruction.leaf_root [in CTL.demo]
ModelConstruction.leaf_root_aux [in CTL.demo]
ModelConstruction.MD_size [in CTL.demo]
ModelConstruction.model_existence [in CTL.demo]
ModelConstruction.MRel_D [in CTL.demo]
ModelConstruction.MRel_R [in CTL.demo]
ModelConstruction.rlabel_Fs [in CTL.demo]
ModelConstruction.root_internal [in CTL.demo]
ModelConstruction.serial_MRel [in CTL.demo]
ModelConstruction.small_model_existence [in CTL.demo]
ModelConstruction.sn_edge [in CTL.demo]
ModelConstruction.supp_eval [in CTL.demo]
ModelConstruction.supp_edge [in CTL.demo]
monotone_fulfillAR_step [in CTL.demo]
monotone_fulfillAU_step [in CTL.demo]
mono_step [in CTL.gen_dec]
N
negE [in CTL.CTL_def]nImp [in CTL.agreement]
P
pARE1 [in CTL.agreement]pARE2 [in CTL.agreement]
pAR_strengthen [in CTL.CTL_def]
pAR_pEU [in CTL.CTL_def]
path_ptail [in CTL.CTL_def]
path_pcons [in CTL.CTL_def]
path_pi3 [in CTL.agreement]
pAU_strengthen [in CTL.CTL_def]
pAU_pER [in CTL.CTL_def]
pER_strengthen [in CTL.CTL_def]
pEU_strengthen [in CTL.CTL_def]
plainP [in CTL.gen_dec]
plain_soundness [in CTL.results]
plain_soundness [in CTL.gen_hsound]
plain_inU [in CTL.gen_dec]
posE [in CTL.CTL_def]
prv_dec [in CTL.results]
prv_dec [in CTL.hilbert_ref]
prv_ER [in CTL.agreement]
R
RE [in CTL.CTL_def]refE1n [in CTL.hilbert_ref]
refI1n [in CTL.hilbert_ref]
refpred_ref' [in CTL.gen_ref]
ref_compl [in CTL.relaxed_pruning]
ref_R3 [in CTL.gen_ref]
ref_R3_aux [in CTL.gen_ref]
ref_R4 [in CTL.gen_ref]
ref_R4_aux [in CTL.gen_ref]
ref_R2 [in CTL.gen_ref]
ref_R1 [in CTL.gen_ref]
ref_R0 [in CTL.gen_ref]
ReqU [in CTL.relaxed_pruning]
Req_RC [in CTL.demo]
rGen [in CTL.hilbert_Eme90]
RinU [in CTL.CTL_def]
Rpos [in CTL.CTL_def]
RU [in CTL.CTL_def]
R0 [in CTL.CTL_def]
R1 [in CTL.CTL_def]
S
sat_dec [in CTL.results]sat_dec [in CTL.hilbert_ref]
serial_relT [in CTL.demo]
ser_R3 [in CTL.agreement]
sfcU [in CTL.CTL_def]
sfc_bigcup [in CTL.CTL_def]
sfc_ssub [in CTL.CTL_def]
sf_ssub [in CTL.CTL_def]
sf_closed'_mon [in CTL.CTL_def]
sf_AR [in CTL.gen_dec]
sf_AU [in CTL.gen_dec]
simple_frag [in CTL.demo]
size_ssub [in CTL.CTL_def]
small_models [in CTL.results]
small_models [in CTL.hilbert_ref]
small_models [in CTL.demo]
sn_preimage [in CTL.dags]
soundness [in CTL.results]
SsubU [in CTL.relaxed_pruning]
ssub_refl [in CTL.CTL_def]
ssub'_refl [in CTL.CTL_def]
stepP [in CTL.gen_dec]
sts_agreement [in CTL.results]
sts_path_soundness [in CTL.agreement]
sts_agreement [in CTL.agreement]
subCs [in CTL.gen_dec]
subU [in CTL.gen_dec]
sub_sfc [in CTL.CTL_def]
suppC1 [in CTL.CTL_def]
suppE [in CTL.CTL_def]
supp_lit [in CTL.CTL_def]
supp_mon [in CTL.CTL_def]
supp0F [in CTL.CTL_def]
sweight_lit [in CTL.CTL_def]
T
terminates_measure [in CTL.dags]terminates_gtn [in CTL.dags]
U
unfulfilledAR_refute [in CTL.hilbert_ref]unfulfilledAU_refute [in CTL.hilbert_ref]
V
valid_dec [in CTL.results]valid_dec [in CTL.hilbert_ref]
X
xchoose_rel [in CTL.agreement]XM_required [in CTL.results]
XM_required [in CTL.agreement]
Constructor Index
A
aAR [in CTL.gen_def]aAU [in CTL.gen_def]
aAXR [in CTL.gen_def]
aAXU [in CTL.gen_def]
ARs [in CTL.CTL_def]
AR0 [in CTL.CTL_def]
AUs [in CTL.CTL_def]
AU0 [in CTL.CTL_def]
aVoid [in CTL.gen_def]
C
CModel [in CTL.CTL_def]D
Demo [in CTL.demo]E
Eme90.axARdef' [in CTL.hilbert_Eme90]Eme90.axAUeq' [in CTL.hilbert_Eme90]
Eme90.axAUr' [in CTL.hilbert_Eme90]
Eme90.axAXdef' [in CTL.hilbert_Eme90]
Eme90.axAXT [in CTL.hilbert_Eme90]
Eme90.axDN [in CTL.hilbert_Eme90]
Eme90.axEUeq' [in CTL.hilbert_Eme90]
Eme90.axEUr' [in CTL.hilbert_Eme90]
Eme90.axEXD' [in CTL.hilbert_Eme90]
Eme90.axK [in CTL.hilbert_Eme90]
Eme90.axReg' [in CTL.hilbert_Eme90]
Eme90.axS [in CTL.hilbert_Eme90]
Eme90.axSer' [in CTL.hilbert_Eme90]
Eme90.rGen [in CTL.hilbert_Eme90]
Eme90.rMP [in CTL.hilbert_Eme90]
ERs [in CTL.CTL_def]
ER0 [in CTL.CTL_def]
EUs [in CTL.CTL_def]
EU0 [in CTL.CTL_def]
ev_x [in CTL.demo]
ev_AU [in CTL.demo]
ev_AR [in CTL.demo]
F
fAR [in CTL.CTL_def]fAU [in CTL.CTL_def]
fAX [in CTL.CTL_def]
fF [in CTL.CTL_def]
fImp [in CTL.CTL_def]
FModel [in CTL.CTL_def]
FragmentDemo [in CTL.demo]
fV [in CTL.CTL_def]
G
gen_jmp [in CTL.gen_def]gen_aAXR [in CTL.gen_def]
gen_ARrep [in CTL.gen_def]
gen_ARh [in CTL.gen_def]
gen_ARfoc [in CTL.gen_def]
gen_ARn [in CTL.gen_def]
gen_ARp [in CTL.gen_def]
gen_AUrep [in CTL.gen_def]
gen_AUh [in CTL.gen_def]
gen_AUfoc [in CTL.gen_def]
gen_AUn [in CTL.gen_def]
gen_AUp [in CTL.gen_def]
gen_AXn [in CTL.gen_def]
gen_In [in CTL.gen_def]
gen_Ip [in CTL.gen_def]
gen_p [in CTL.gen_def]
gen_F [in CTL.gen_def]
Graph [in CTL.dags]
I
IC.AU_ind [in CTL.hilbert]IC.axARE [in CTL.hilbert]
IC.axARu [in CTL.hilbert]
IC.axAUf [in CTL.hilbert]
IC.axAUI [in CTL.hilbert]
IC.axDN [in CTL.hilbert]
IC.axK [in CTL.hilbert]
IC.axN [in CTL.hilbert]
IC.axS [in CTL.hilbert]
IC.ax_serial [in CTL.hilbert]
IC.rAR_ind [in CTL.hilbert]
IC.rMP [in CTL.hilbert]
IC.rNec [in CTL.hilbert]
isBox_false [in CTL.CTL_def]
isBox_true [in CTL.CTL_def]
isDia_false [in CTL.CTL_def]
isDia_true [in CTL.CTL_def]
L
LS.ARel' [in CTL.hilbert_LS]LS.axARf' [in CTL.hilbert_LS]
LS.axAUcmp' [in CTL.hilbert_LS]
LS.axDN [in CTL.hilbert_LS]
LS.axERf' [in CTL.hilbert_LS]
LS.axK [in CTL.hilbert_LS]
LS.axN [in CTL.hilbert_LS]
LS.axS [in CTL.hilbert_LS]
LS.axSer [in CTL.hilbert_LS]
LS.ERel' [in CTL.hilbert_LS]
LS.rMP [in CTL.hilbert_LS]
LS.rNec [in CTL.hilbert_LS]
R
RGraph [in CTL.dags]R1 [in CTL.relaxed_pruning]
R2 [in CTL.relaxed_pruning]
R3 [in CTL.relaxed_pruning]
R4 [in CTL.relaxed_pruning]
S
SN [in CTL.dags]StarL [in CTL.dags]
Star0 [in CTL.dags]
STS [in CTL.CTL_def]
Inductive Index
A
annot [in CTL.gen_def]C
cAR [in CTL.CTL_def]cAU [in CTL.CTL_def]
cER [in CTL.CTL_def]
cEU [in CTL.CTL_def]
E
Eme90.prv [in CTL.hilbert_Eme90]ev_case [in CTL.demo]
F
form [in CTL.CTL_def]G
gen [in CTL.gen_def]I
IC.prv [in CTL.hilbert]isBox_spec [in CTL.CTL_def]
isDia_spec [in CTL.CTL_def]
L
LS.prv [in CTL.hilbert_LS]R
ref [in CTL.relaxed_pruning]S
sn [in CTL.dags]star [in CTL.dags]
Projection Index
D
demoSsubT [in CTL.demo]demoT [in CTL.demo]
demo1 [in CTL.demo]
demo2 [in CTL.demo]
demo3 [in CTL.demo]
DG1 [in CTL.demo]
DG2 [in CTL.demo]
DG3 [in CTL.demo]
DG4 [in CTL.demo]
DG5 [in CTL.demo]
DG6 [in CTL.demo]
DG7 [in CTL.demo]
E
edge [in CTL.dags]F
fd_lcons [in CTL.demo]fd_sub [in CTL.demo]
fd_trees [in CTL.demo]
flabel [in CTL.CTL_def]
fser [in CTL.CTL_def]
fstate [in CTL.CTL_def]
ftrans [in CTL.CTL_def]
G
graph_of [in CTL.dags]L
label [in CTL.CTL_def]label [in CTL.dags]
M
modelP [in CTL.CTL_def]R
root [in CTL.dags]rootP [in CTL.dags]
S
serial [in CTL.CTL_def]state [in CTL.CTL_def]
sts_of [in CTL.CTL_def]
T
trans [in CTL.CTL_def]V
vertex [in CTL.dags]Section Index
A
Agreement [in CTL.agreement]C
Characterizations [in CTL.CTL_def]D
Decidability [in CTL.CTL_def]DemoToFragment [in CTL.demo]
DemoToFragment.Fragments [in CTL.demo]
Disjoint [in CTL.dags]
E
Eme90.Hilbert [in CTL.hilbert_Eme90]F
FiniteModels [in CTL.CTL_def]FragmentDemo [in CTL.demo]
Fulfillment [in CTL.demo]
G
gen_closure [in CTL.gen_dec]GraphTheory [in CTL.dags]
I
IC.Hilbert [in CTL.hilbert]L
LPO [in CTL.results]LPO [in CTL.agreement]
LS.Hilbert [in CTL.hilbert_LS]
M
ModelConstruction.ModelConstruction [in CTL.demo]P
Paths [in CTL.agreement]Paths2 [in CTL.agreement]
Prune [in CTL.relaxed_pruning]
R
RefPred [in CTL.hilbert_ref]RefPred [in CTL.gen_ref]
RefPred.EventualityRefutations [in CTL.hilbert_ref]
S
Soundness [in CTL.agreement]Abbreviation Index
A
ARb [in CTL.agreement]AUb [in CTL.agreement]
S
S0 [in CTL.hilbert_ref]S0 [in CTL.gen_ref]
U
U [in CTL.hilbert_ref]U [in CTL.gen_ref]
X
xaf [in CTL.hilbert_ref]xaf [in CTL.gen_ref]
Definition Index
A
annot_choiceMixin [in CTL.gen_def]annot_countMixin [in CTL.gen_def]
annot_eqMixin [in CTL.gen_def]
Annot.pickle [in CTL.gen_def]
Annot.unpickle [in CTL.gen_def]
aR [in CTL.gen_def]
ARb [in CTL.CTL_def]
ARl [in CTL.demo]
ARr [in CTL.demo]
ARs [in CTL.gen_dec]
AR_fun [in CTL.CTL_def]
AR_label [in CTL.demo]
AR_rel [in CTL.demo]
AR_T0 [in CTL.demo]
AR_level [in CTL.demo]
As [in CTL.gen_dec]
AUb [in CTL.CTL_def]
AUl [in CTL.demo]
AUr [in CTL.demo]
AUs [in CTL.gen_dec]
AU_fun [in CTL.CTL_def]
AU_ [in CTL.hilbert_hist]
AU_rel [in CTL.demo]
AU_label [in CTL.demo]
AU_T0 [in CTL.demo]
AU_level [in CTL.demo]
AXn [in CTL.demo]
AXn_complete [in CTL.demo]
B
body [in CTL.CTL_def]bounded_demo [in CTL.demo]
C
cAX [in CTL.CTL_def]cEX [in CTL.CTL_def]
clause [in CTL.CTL_def]
cmodel_of_fmodel [in CTL.CTL_def]
coref [in CTL.relaxed_pruning]
Cs [in CTL.gen_dec]
D
DC [in CTL.CTL_def]DC_ [in CTL.CTL_def]
DD [in CTL.relaxed_pruning]
DD_demo [in CTL.demo]
E
Eme90.fAG [in CTL.hilbert_Eme90]Eme90.fEU [in CTL.hilbert_Eme90]
Eme90.fEX [in CTL.hilbert_Eme90]
erel [in CTL.dags]
EU_ [in CTL.hilbert_hist]
eval [in CTL.CTL_def]
evalb [in CTL.CTL_def]
ev_cond [in CTL.demo]
F
formChoice.pickle [in CTL.CTL_def]formChoice.unpickle [in CTL.CTL_def]
form_slClass [in CTL.CTL_def]
form_choiceMixin [in CTL.CTL_def]
form_countMixin [in CTL.CTL_def]
form_eqMixin [in CTL.CTL_def]
fragment_bound [in CTL.demo]
Fs [in CTL.demo]
fulfillAR_step [in CTL.demo]
fulfillAU_step [in CTL.demo]
fulfillsAR [in CTL.demo]
fulfillsARE [in CTL.demo]
fulfillsAU [in CTL.demo]
fulfillsAUE [in CTL.demo]
f_size [in CTL.CTL_def]
f_weight [in CTL.CTL_def]
G
glabels_from [in CTL.demo]glocal [in CTL.dags]
H
hist [in CTL.gen_hsound]href [in CTL.hilbert_ref]
Hs [in CTL.gen_dec]
I
interp_a [in CTL.gen_hsound]interp' [in CTL.demo]
isBox [in CTL.CTL_def]
isDia [in CTL.CTL_def]
L
lcons [in CTL.CTL_def]ldec [in CTL.CTL_def]
leaf [in CTL.dags]
lift_edge [in CTL.dags]
literal [in CTL.CTL_def]
LS.fER [in CTL.hilbert_LS]
LS.fEX [in CTL.hilbert_LS]
L3 [in CTL.agreement]
M
ModelConstruction.AU_M [in CTL.demo]ModelConstruction.DC [in CTL.demo]
ModelConstruction.DF [in CTL.demo]
ModelConstruction.EU_M [in CTL.demo]
ModelConstruction.Frag [in CTL.demo]
ModelConstruction.MD [in CTL.demo]
ModelConstruction.MLabel [in CTL.demo]
ModelConstruction.MRel [in CTL.demo]
ModelConstruction.Mstate [in CTL.demo]
ModelConstruction.MType [in CTL.demo]
M3 [in CTL.agreement]
N
negative [in CTL.CTL_def]negatives [in CTL.CTL_def]
P
pAR [in CTL.CTL_def]pAR [in CTL.relaxed_pruning]
pAR' [in CTL.agreement]
path [in CTL.CTL_def]
pAU [in CTL.CTL_def]
pAU [in CTL.relaxed_pruning]
pAXn [in CTL.relaxed_pruning]
pcond [in CTL.relaxed_pruning]
pcons [in CTL.CTL_def]
pER [in CTL.CTL_def]
pEU [in CTL.CTL_def]
pi3 [in CTL.agreement]
positive [in CTL.CTL_def]
positives [in CTL.CTL_def]
PredC [in CTL.CTL_def]
ptail [in CTL.CTL_def]
p_release [in CTL.CTL_def]
p_until [in CTL.CTL_def]
p_release' [in CTL.agreement]
R
R [in CTL.CTL_def]ref' [in CTL.gen_ref]
relT [in CTL.demo]
Req [in CTL.demo]
req_cond [in CTL.demo]
respects [in CTL.dags]
restrict [in CTL.dags]
R3 [in CTL.agreement]
S
satisfies [in CTL.CTL_def]sfc [in CTL.CTL_def]
sform [in CTL.CTL_def]
sf_closed [in CTL.CTL_def]
sf_closed' [in CTL.CTL_def]
ssub [in CTL.CTL_def]
ssub' [in CTL.CTL_def]
stable [in CTL.CTL_def]
step [in CTL.gen_dec]
step_jmp [in CTL.gen_dec]
step_annot [in CTL.gen_dec]
step_plain [in CTL.gen_dec]
step_plain_cases [in CTL.gen_dec]
subDD [in CTL.relaxed_pruning]
supp [in CTL.CTL_def]
supp_cond [in CTL.demo]
s_weight [in CTL.CTL_def]
S0 [in CTL.relaxed_pruning]
T
terminates [in CTL.dags]U
U [in CTL.relaxed_pruning]U [in CTL.gen_dec]
unit_model [in CTL.demo]
V
var [in CTL.CTL_def]Record Index
C
cmodel [in CTL.CTL_def]D
demo [in CTL.demo]F
fmodel [in CTL.CTL_def]fragment [in CTL.demo]
fragment_demo [in CTL.demo]
G
graph [in CTL.dags]R
rGraph [in CTL.dags]S
sts [in CTL.CTL_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 | (738 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 | (18 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 | (6 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 | (54 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 | (15 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 | (317 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 | (97 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 | (16 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 | (31 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 | (24 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 | (8 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 | (144 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 | (8 entries) |