| 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 | (573 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) |
| 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 | (11 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 | (10 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 | (211 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 | (153 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 | (34 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 | (26 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| 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 | (17 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 | (68 entries) |
Global Index
A
Algorithmic [section, in Step]avar [inductive, in VarDef]
avar_f [constructor, in VarDef]
avar_b [constructor, in VarDef]
avar_search_equiv [lemma, in Step]
B
BiSubtyProperties [section, in Stareat]BisubtyStronger [section, in Step]
bnd_layer [definition, in Kernel]
bsubtyp [definition, in Stareat]
bsubtyp_sound [lemma, in Stareat]
bs'_bnd [constructor, in StrongKernel]
bs'_all [constructor, in StrongKernel]
bs'_sel_right [constructor, in StrongKernel]
bs'_sel_left [constructor, in StrongKernel]
bs'_sel_refl [constructor, in StrongKernel]
bs'_top [constructor, in StrongKernel]
bs'_bot [constructor, in StrongKernel]
bt_bnd [constructor, in Stareat]
bt_all [constructor, in Stareat]
bt_sel_right [constructor, in Stareat]
bt_sel_left [constructor, in Stareat]
bt_sel_refl [constructor, in Stareat]
bt_top [constructor, in Stareat]
bt_bot [constructor, in Stareat]
bv_search_idx [lemma, in Step]
bv_search_equiv [lemma, in Step]
C
CloseAvar [instance, in Definitions]CloseTrm [instance, in Definitions]
CloseTyp [instance, in Definitions]
CloseVal [instance, in Definitions]
close_lc_val [lemma, in OperationProperties]
close_lc_trm [lemma, in OperationProperties]
close_lc_typ [lemma, in OperationProperties]
close_lc_avar [lemma, in OperationProperties]
close_lc [abbreviation, in OperationProperties]
close_rec_val [definition, in Definitions]
close_rec_trm [definition, in Definitions]
close_rec_typ [definition, in Definitions]
close_rec_avar [definition, in Definitions]
ClosingDefinitions [section, in Definitions]
D
dce_bnd [constructor, in Step]dce_top [constructor, in Step]
dce_bot [constructor, in Step]
dc_bnd [constructor, in Stareat]
dc_top [constructor, in Stareat]
dc_bot [constructor, in Stareat]
Definitions [library]
denv [abbreviation, in Step]
denv_measure [definition, in Step]
denv_fv [definition, in Step]
de_bnd [constructor, in Kernel]
de_top [constructor, in Kernel]
de_bot [constructor, in Kernel]
downcast [inductive, in Stareat]
DowncastProperties [section, in Stareat]
downcast_f_dep_eq_downcast_f [lemma, in Stareat]
downcast_f_dep [definition, in Stareat]
downcast_f_u_eq [lemma, in Stareat]
downcast_f_u [definition, in Stareat]
downcast_func_decreases_measure [lemma, in Stareat]
downcast_func_sound_wrt_spec [lemma, in Stareat]
downcast_func [definition, in Stareat]
downcast_preserves_wf [lemma, in Stareat]
downcast_sound [lemma, in Stareat]
downcast_decreases_measure [lemma, in Stareat]
downcast_e'_to_downcast_e [lemma, in Kernel]
downcast_e' [inductive, in Kernel]
downcast_e_measure_decrease [lemma, in Step]
downcast_gives_prefix [lemma, in Step]
downcast_strengthening [lemma, in Step]
downcast_e_to_downcast [lemma, in Step]
downcast_e_preserves_lc [lemma, in Step]
downcast_e_preserves_wf [lemma, in Step]
downcast_e [inductive, in Step]
E
env [abbreviation, in Definitions]env_measure_app [lemma, in Misc]
env_measure_cons [lemma, in Misc]
env_measure [definition, in Misc]
EqAvar [instance, in VarDef]
EqDecTyp [instance, in Definitions]
EquivalentRepr [section, in Step]
eq_typ_sel [definition, in Stareat]
exposure [inductive, in Step]
exposure_measure_decrease [lemma, in Step]
exposure_sound [lemma, in Step]
exposure_to_exposure' [lemma, in Step]
exposure_weakening [lemma, in Step]
exposure_preserves_lc [lemma, in Step]
exposure_preserves_wf [lemma, in Step]
exposure_strengthening [lemma, in Step]
exposure_to_revealing [lemma, in Step]
exposure_to_revealing_gen [lemma, in Step]
exposure' [inductive, in Step]
exposure'_to_subtysk [lemma, in StrongKernel]
exposure'_to_subtykn [lemma, in Kernel]
exposure'_equiv_exposure [lemma, in Step]
exposure'_to_exposure [lemma, in Step]
exposure'_weakening_gen [lemma, in Step]
exposure'_weakening [lemma, in Step]
exp_bnd [constructor, in Step]
exp_bot [constructor, in Step]
exp_top [constructor, in Step]
exp_stop [constructor, in Step]
ex_bnd [constructor, in Step]
ex_bot [constructor, in Step]
ex_top [constructor, in Step]
ex_stop [constructor, in Step]
F
FreeVariables [section, in Definitions]free_all [lemma, in StructuralProperties]
fresh_inj [abbreviation, in OperationProperties]
FvAvar [instance, in Definitions]
FvClose [section, in OperationProperties]
FvDenv [instance, in Step]
FvEnv [instance, in Definitions]
FvOpen [section, in OperationProperties]
FvTrm [instance, in Definitions]
FvTyp [instance, in Definitions]
FvVal [instance, in Definitions]
fv_add_close_val [lemma, in OperationProperties]
fv_add_close_trm [lemma, in OperationProperties]
fv_add_close_typ [lemma, in OperationProperties]
fv_add_close_avar [lemma, in OperationProperties]
fv_add_close [abbreviation, in OperationProperties]
fv_close_val [lemma, in OperationProperties]
fv_close_trm [lemma, in OperationProperties]
fv_close_typ [lemma, in OperationProperties]
fv_close_avar [lemma, in OperationProperties]
fv_close [abbreviation, in OperationProperties]
fv_close_self_val [lemma, in OperationProperties]
fv_close_self_trm [lemma, in OperationProperties]
fv_close_self_typ [lemma, in OperationProperties]
fv_close_self_avar [lemma, in OperationProperties]
fv_close_self [abbreviation, in OperationProperties]
fv_open_val [lemma, in OperationProperties]
fv_open_trm [lemma, in OperationProperties]
fv_open_typ [lemma, in OperationProperties]
fv_open_avar [lemma, in OperationProperties]
fv_open [abbreviation, in OperationProperties]
fv_union [lemma, in Definitions]
fv_val [definition, in Definitions]
fv_trm [definition, in Definitions]
fv_typ [definition, in Definitions]
fv_avar [definition, in Definitions]
fv_unpack [lemma, in VarDef]
fv_values [definition, in VarDef]
fv_deapp [lemma, in Stareat]
fv_ignores_D [lemma, in Step]
fv_search_equiv [lemma, in Step]
I
incr_lc [inductive, in Step]is_bnd_dec [definition, in Misc]
is_bnd [definition, in Misc]
is_all_dec [definition, in Misc]
is_all [definition, in Misc]
is_sel_dec [definition, in Misc]
is_sel [definition, in Misc]
is_bot_dec [definition, in Misc]
is_bot [definition, in Misc]
is_top_dec [definition, in Misc]
is_top [definition, in Misc]
K
Kernel [library]L
layered_bot_trans [lemma, in StrongKernel]layered_top_trans [lemma, in StrongKernel]
layered_bot_trans [lemma, in Kernel]
layered_top_trans [lemma, in Kernel]
LcAvar [instance, in Definitions]
LcOpenClosingProperties [section, in OperationProperties]
LcTrm [instance, in Definitions]
LcTyp [instance, in Definitions]
LcVal [instance, in Definitions]
lc_relax_val [lemma, in OperationProperties]
lc_relax_trm [lemma, in OperationProperties]
lc_relax_typ [lemma, in OperationProperties]
lc_relax_avar [lemma, in OperationProperties]
lc_relax [abbreviation, in OperationProperties]
lc_val_lam [constructor, in Definitions]
lc_val_bnd [constructor, in Definitions]
lc_val_at [inductive, in Definitions]
lc_trm_let [constructor, in Definitions]
lc_trm_app [constructor, in Definitions]
lc_trm_val [constructor, in Definitions]
lc_trm_var [constructor, in Definitions]
lc_trm_at [inductive, in Definitions]
lc_typ_bnd [constructor, in Definitions]
lc_typ_all [constructor, in Definitions]
lc_typ_sel [constructor, in Definitions]
lc_typ_bot [constructor, in Definitions]
lc_typ_top [constructor, in Definitions]
lc_typ_at [inductive, in Definitions]
lc_af [constructor, in Definitions]
lc_ab [constructor, in Definitions]
lc_avar_at [inductive, in Definitions]
lc_cons [constructor, in Step]
lc_nil [constructor, in Step]
LocalClosure [section, in Definitions]
M
MeasuresAndFacts [section, in Step]Misc [library]
N
narrowing [abbreviation, in StructuralProperties]narrow_subty [lemma, in StructuralProperties]
narrow_typing [lemma, in StructuralProperties]
narrow_subty_gen [lemma, in StructuralProperties]
narrow_typing_gen [lemma, in StructuralProperties]
narrow_var [lemma, in StructuralProperties]
O
OpenAvar [instance, in Definitions]OpenFreshInj [section, in OperationProperties]
OpenFreshInj.z [variable, in OperationProperties]
OpeningDefinitions [section, in Definitions]
OpenTrm [instance, in Definitions]
OpenTyp [instance, in Definitions]
OpenVal [instance, in Definitions]
open_substi_rewrite2 [lemma, in OperationProperties]
open_substi_rewrite [lemma, in OperationProperties]
open_fresh_inj_val [lemma, in OperationProperties]
open_fresh_inj_trm [lemma, in OperationProperties]
open_fresh_inj_typ [lemma, in OperationProperties]
open_fresh_inj_avar [lemma, in OperationProperties]
open_left_inv_val [lemma, in OperationProperties]
open_left_inv_trm [lemma, in OperationProperties]
open_left_inv_typ [lemma, in OperationProperties]
open_left_inv_avar [lemma, in OperationProperties]
open_left_inv [abbreviation, in OperationProperties]
open_lc_inv_val [lemma, in OperationProperties]
open_lc_inv_trm [lemma, in OperationProperties]
open_lc_inv_typ [lemma, in OperationProperties]
open_lc_inv_avar [lemma, in OperationProperties]
open_lc_inv [abbreviation, in OperationProperties]
open_lc_le_val [lemma, in OperationProperties]
open_lc_le_trm [lemma, in OperationProperties]
open_lc_le_typ [lemma, in OperationProperties]
open_lc_le_avar [lemma, in OperationProperties]
open_lc_le [abbreviation, in OperationProperties]
open_lc_val [lemma, in OperationProperties]
open_lc_trm [lemma, in OperationProperties]
open_lc_typ [lemma, in OperationProperties]
open_lc_avar [lemma, in OperationProperties]
open_lc [abbreviation, in OperationProperties]
open_rec_val [definition, in Definitions]
open_rec_trm [definition, in Definitions]
open_rec_typ [definition, in Definitions]
open_rec_avar [definition, in Definitions]
open_subst_subty [lemma, in StructuralProperties]
open_subst_typing [lemma, in StructuralProperties]
open_val_same_measure [lemma, in Misc]
open_trm_same_measure [lemma, in Misc]
open_typ_same_measure [lemma, in Misc]
open_rec_D [definition, in Step]
OpeProperties [section, in OpeSub]
OperationProperties [library]
OpeSub [library]
ope_sub_stareat_sound [lemma, in Stareat]
ope_sub_app [lemma, in OpeSub]
ope_sub_nil [lemma, in OpeSub]
ope_sub_refl [lemma, in OpeSub]
ope_sub_trans [lemma, in OpeSub]
ope_narrow_subty [lemma, in OpeSub]
ope_narrow_trm [lemma, in OpeSub]
ope_narrow_var [lemma, in OpeSub]
ope_sub_length [lemma, in OpeSub]
ope_sub [inductive, in OpeSub]
ope_list_fv_env_subset [lemma, in Step]
os_keep [constructor, in OpeSub]
os_drop [constructor, in OpeSub]
os_nil [constructor, in OpeSub]
P
Predicates [section, in Misc]prefix_wf_env [lemma, in Step]
R
renaming_fresh [lemma, in StructuralProperties]renaming_subty [lemma, in StructuralProperties]
renaming_trm [lemma, in StructuralProperties]
revealing [inductive, in Stareat]
RevealingProperties [section, in Stareat]
RevealingSubsumesExposure [section, in Step]
revealing_to_subtysk [lemma, in StrongKernel]
revealing_fv_bound [lemma, in StrongKernel]
revealing_terminates [definition, in Stareat]
revealing_measure [lemma, in Stareat]
revealing_preserves_wf [lemma, in Stareat]
revealing_sound [lemma, in Stareat]
revealing_termination [inductive, in Stareat]
revealing_to_exposure [lemma, in Step]
revealing_strengthening [lemma, in Step]
revealing_sel_weakening_prefix [lemma, in Step]
revealing_sel_weakening [lemma, in Step]
revealing_gives_prefix [lemma, in Step]
reveal_func_sound_wrt_spec [lemma, in Stareat]
reveal_func [definition, in Stareat]
rt_bnd [constructor, in Stareat]
rt_bot [constructor, in Stareat]
rt_top [constructor, in Stareat]
rt_stop [constructor, in Stareat]
rv_bnd [constructor, in Stareat]
rv_bot [constructor, in Stareat]
rv_top [constructor, in Stareat]
rv_stop [constructor, in Stareat]
S
sa_bnd [constructor, in Stareat]sa_all [constructor, in Stareat]
sa_sel_right [constructor, in Stareat]
sa_sel_left [constructor, in Stareat]
sa_sel_refl [constructor, in Stareat]
sa_top [constructor, in Stareat]
sa_bot [constructor, in Stareat]
sk_trans_on_bot [lemma, in StrongKernel]
sk_trans_on_top [lemma, in StrongKernel]
snf_sel2 [constructor, in Kernel]
snf_sel1 [constructor, in Kernel]
snf_all [constructor, in Kernel]
snf_bnd [constructor, in Kernel]
snf_bot [constructor, in Kernel]
snf_top [constructor, in Kernel]
snf_vrefl [constructor, in Kernel]
snf'_sel2 [constructor, in Kernel]
snf'_sel1 [constructor, in Kernel]
snf'_all [constructor, in Kernel]
snf'_bnd [constructor, in Kernel]
snf'_bot [constructor, in Kernel]
snf'_top [constructor, in Kernel]
snf'_refl [constructor, in Kernel]
ssk_sel2 [constructor, in StrongKernel]
ssk_sel1 [constructor, in StrongKernel]
ssk_all [constructor, in StrongKernel]
ssk_bnd [constructor, in StrongKernel]
ssk_bot [constructor, in StrongKernel]
ssk_top [constructor, in StrongKernel]
ssk_refl [constructor, in StrongKernel]
ssk'_sel2 [constructor, in StrongKernel]
ssk'_sel1 [constructor, in StrongKernel]
ssk'_all [constructor, in StrongKernel]
ssk'_bnd [constructor, in StrongKernel]
ssk'_bot [constructor, in StrongKernel]
ssk'_top [constructor, in StrongKernel]
ssk'_refl [constructor, in StrongKernel]
sst_all [constructor, in Step]
sst_bnd [constructor, in Step]
sst_sel_right [constructor, in Step]
sst_sel_left [constructor, in Step]
sst_sel_refl [constructor, in Step]
sst_bot [constructor, in Step]
sst_top [constructor, in Step]
ss_all [constructor, in Step]
ss_bnd [constructor, in Step]
ss_sel_right [constructor, in Step]
ss_sel_left [constructor, in Step]
ss_sel_refl [constructor, in Step]
ss_bot [constructor, in Step]
ss_top [constructor, in Step]
ss'_all [constructor, in Kernel]
ss'_bnd [constructor, in Kernel]
ss'_sel_right [constructor, in Kernel]
ss'_sel_left [constructor, in Kernel]
ss'_sel_refl [constructor, in Kernel]
ss'_bot [constructor, in Kernel]
ss'_top [constructor, in Kernel]
stareat [inductive, in Stareat]
Stareat [library]
stareat_cong_names [lemma, in StrongKernel]
stareat_to_subtysk [lemma, in StrongKernel]
stareat_to_stareat' [lemma, in StrongKernel]
stareat_terminates [definition, in Stareat]
stareat_termination [inductive, in Stareat]
stareat_refl [definition, in Stareat]
stareat_strengthening [lemma, in Step]
stareat' [inductive, in StrongKernel]
stareat'_to_subtysk [lemma, in StrongKernel]
stareat'_weakening_r [lemma, in StrongKernel]
stareat'_weakening_l [lemma, in StrongKernel]
stareat'_weakening_gen [lemma, in StrongKernel]
stareat'_to_stareat [lemma, in StrongKernel]
Step [library]
stp_subty'_to_stp_subty [lemma, in Kernel]
stp_subty'_refl [definition, in Kernel]
stp_subty' [inductive, in Kernel]
stp_subty_to_subtykn [lemma, in Kernel]
stp_subty_terminates [definition, in Step]
stp_subty_termination [inductive, in Step]
stp_subty_sound [lemma, in Step]
stp_subty_to_stareat [lemma, in Step]
stp_subty [inductive, in Step]
StrongKernel [library]
StructuralProperties [section, in StructuralProperties]
StructuralProperties [library]
_ ⪯ _ [notation, in StructuralProperties]
st_sel2 [constructor, in Definitions]
st_sel1 [constructor, in Definitions]
st_all [constructor, in Definitions]
st_bnd [constructor, in Definitions]
st_trans [constructor, in Definitions]
st_bot [constructor, in Definitions]
st_top [constructor, in Definitions]
st_refl [constructor, in Definitions]
subenv [inductive, in StructuralProperties]
subenv_implies_uniq [lemma, in StructuralProperties]
subenv_last [lemma, in StructuralProperties]
subenv_push [lemma, in StructuralProperties]
subenv_refl [lemma, in StructuralProperties]
subenv_grow [constructor, in StructuralProperties]
subenv_empty [constructor, in StructuralProperties]
SubstAvar [instance, in Definitions]
SubstFresh [section, in OperationProperties]
SubstFresh.x [variable, in OperationProperties]
SubstFresh.y [variable, in OperationProperties]
SubstFvarProps [section, in OperationProperties]
SubstFvarProps.subst_open_comm [variable, in OperationProperties]
SubstFvarProps.t [variable, in OperationProperties]
SubstFvarProps.T [variable, in OperationProperties]
SubstFvarProps.x [variable, in OperationProperties]
SubstFvarProps.y [variable, in OperationProperties]
SubstFvarProps.z [variable, in OperationProperties]
SubstiEnv [instance, in StructuralProperties]
SubstIntro [section, in OperationProperties]
Substitutions [section, in Definitions]
SubstOpenComm [section, in OperationProperties]
SubstOpenComm.x [variable, in OperationProperties]
SubstOpenComm.y [variable, in OperationProperties]
SubstTrm [instance, in Definitions]
SubstTyp [instance, in Definitions]
SubstVal [instance, in Definitions]
subst_intro_typ [lemma, in OperationProperties]
subst_intro_val [lemma, in OperationProperties]
subst_intro_trm [lemma, in OperationProperties]
subst_intro [abbreviation, in OperationProperties]
subst_open_comm_val [lemma, in OperationProperties]
subst_open_comm_trm [lemma, in OperationProperties]
subst_open_comm_typ [lemma, in OperationProperties]
subst_open_comm_avar [lemma, in OperationProperties]
subst_open_comm [abbreviation, in OperationProperties]
subst_fvar [definition, in OperationProperties]
subst_fresh_val [lemma, in OperationProperties]
subst_fresh_trm [lemma, in OperationProperties]
subst_fresh_typ [lemma, in OperationProperties]
subst_fresh_avar [lemma, in OperationProperties]
subst_fresh [abbreviation, in OperationProperties]
subst_val [definition, in Definitions]
subst_trm [definition, in Definitions]
subst_typ [definition, in Definitions]
subst_avar [definition, in Definitions]
subst_trm_var [lemma, in StructuralProperties]
subst_env [definition, in StructuralProperties]
subty [inductive, in Definitions]
subtykn [inductive, in Kernel]
subtykn_to_subtysk [lemma, in StrongKernel]
subtykn_equiv_stp_subty [lemma, in Kernel]
subtykn_to_stp_subty [lemma, in Kernel]
subtykn_to_stp_subty' [lemma, in Kernel]
subtykn_equiv_subtykn' [lemma, in Kernel]
subtykn_to_subtykn' [lemma, in Kernel]
subtykn_sound [lemma, in Kernel]
subtykn_refl [definition, in Kernel]
subtykn' [inductive, in Kernel]
subtykn'_conversions [definition, in Kernel]
subtykn'_to_subtykn [lemma, in Kernel]
subtysk [inductive, in StrongKernel]
subtysk_equiv_stareat [lemma, in StrongKernel]
subtysk_to_stareat [lemma, in StrongKernel]
subtysk_to_stareat' [lemma, in StrongKernel]
subtysk_equiv_subtysk' [lemma, in StrongKernel]
subtysk_to_subtysk' [lemma, in StrongKernel]
subtysk_sound [lemma, in StrongKernel]
subtysk_sound_gen [lemma, in StrongKernel]
subtysk_refl [definition, in StrongKernel]
subtysk' [inductive, in StrongKernel]
subtysk'_conversions [definition, in StrongKernel]
subtysk'_to_subtysk [lemma, in StrongKernel]
subty_subst [lemma, in StructuralProperties]
subty_subst_gen [lemma, in StructuralProperties]
subty_measure [definition, in Stareat]
T
Termination [section, in Stareat]total [definition, in Misc]
total_app [lemma, in Misc]
trans_on_bot [lemma, in Kernel]
trans_on_top [lemma, in Kernel]
trm [inductive, in Definitions]
trm_let [constructor, in Definitions]
trm_app [constructor, in Definitions]
trm_val [constructor, in Definitions]
trm_var [constructor, in Definitions]
trm_struct_measure [definition, in Misc]
typ [inductive, in Definitions]
typing [inductive, in Definitions]
typing_subst [lemma, in StructuralProperties]
typing_subst_gen [lemma, in StructuralProperties]
typ_bnd [constructor, in Definitions]
typ_all [constructor, in Definitions]
typ_sel [constructor, in Definitions]
typ_bot [constructor, in Definitions]
typ_top [constructor, in Definitions]
typ_struct_measure_ge_1 [lemma, in Misc]
typ_struct_measure [definition, in Misc]
ty_sub [constructor, in Definitions]
ty_let [constructor, in Definitions]
ty_app [constructor, in Definitions]
ty_lam [constructor, in Definitions]
ty_bnd [constructor, in Definitions]
ty_var [constructor, in Definitions]
U
uce_bnd [constructor, in Step]uce_bot [constructor, in Step]
uce_top [constructor, in Step]
uc_bnd [constructor, in Stareat]
uc_bot [constructor, in Stareat]
uc_top [constructor, in Stareat]
ue_bnd [constructor, in Kernel]
ue_bot [constructor, in Kernel]
ue_top [constructor, in Kernel]
upcast [inductive, in Stareat]
UpcastProperties [section, in Stareat]
upcast_f_dep_eq_upcast_f [lemma, in Stareat]
upcast_f_dep [definition, in Stareat]
upcast_f_u_eq [lemma, in Stareat]
upcast_f_u [definition, in Stareat]
upcast_func_decreases_measure [lemma, in Stareat]
upcast_func_sound_wrt_spec [lemma, in Stareat]
upcast_func [definition, in Stareat]
upcast_preserves_wf [lemma, in Stareat]
upcast_sound [lemma, in Stareat]
upcast_decreases_measure [lemma, in Stareat]
upcast_e'_to_upcast_e [lemma, in Kernel]
upcast_e' [inductive, in Kernel]
upcast_e_measure_decrease [lemma, in Step]
upcast_gives_prefix [lemma, in Step]
upcast_strengthening [lemma, in Step]
upcast_e_to_upcast [lemma, in Step]
upcast_e_preserves_lc [lemma, in Step]
upcast_e_preserves_wf [lemma, in Step]
upcast_e [inductive, in Step]
V
val [inductive, in Definitions]val_lam [constructor, in Definitions]
val_bnd [constructor, in Definitions]
val_struct_measure [definition, in Misc]
VarDef [library]
W
weaken_subty [definition, in StructuralProperties]weaken_typing [definition, in StructuralProperties]
weaken_subty_gen [lemma, in StructuralProperties]
weaken_typing_gen [lemma, in StructuralProperties]
weaken_subtykn [lemma, in Kernel]
weaken_subtykn_gen [lemma, in Kernel]
wf_fv_is_dom [lemma, in Misc]
wf_var_in [lemma, in Misc]
wf_uniq [lemma, in Misc]
wf_deapp [lemma, in Misc]
wf_decons [lemma, in Misc]
wf_cons [constructor, in Misc]
wf_nil [constructor, in Misc]
wf_env [inductive, in Misc]
wf_search_lookup [lemma, in Step]
wf_search_wf_ge_1 [lemma, in Step]
wf_open_shift [lemma, in Step]
wf_open_shift_gen [definition, in Step]
wf_search_impl_avar_f_eq [lemma, in Step]
wf_lookup_lt [lemma, in Step]
wf_search_weaken [lemma, in Step]
wf_search_weaken_gen [definition, in Step]
wf_weaken_measure [definition, in Step]
wf_search_fv_weaken [lemma, in Step]
wf_search_avar [definition, in Step]
wf_search_bv [definition, in Step]
wf_search_fv [definition, in Step]
wf_search [definition, in Step]
wf_search_impl [definition, in Step]
wf_measure [definition, in Step]
other
_ ⊢ _ <⦂ _ [notation, in Definitions]_ ⊢ _ ⦂ _ [notation, in Definitions]
_ ⊢S _ <⦂ _ [notation, in Stareat]
_ ⊢ _ ↘ _ ⊢! _ [notation, in Stareat]
_ ⊢ _ ↗ _ ⊢! _ [notation, in Stareat]
_ ⊢ _ ⤊ _ ⊢! _ [notation, in Stareat]
_ ⊆<⦂ _ [notation, in OpeSub]
_ ⊢ _ ↘! _ [notation, in Step]
_ ⊢ _ ↗! _ [notation, in Step]
_ ⊢ _ ⇑ _ [notation, in Step]
[ _ , _ ] _ ⊢k _ <⦂ _ k⊣ _ [notation, in StrongKernel]
[ _ ] _ >> _ <⦂p _ << _ [notation, in StrongKernel]
[ _ ] _ ⊢k _ <⦂ _ k⊣ _ [notation, in StrongKernel]
[ _ ] _ >> _ <⦂ _ << _ [notation, in Stareat]
[ _ , _ ] _ ⊢k _ <⦂ _ [notation, in Kernel]
[ _ ] _ ⊢k _ <⦂ _ [notation, in Kernel]
[ _ ] _ ⊢s _ <⦂ _ [notation, in Step]
Notation Index
S
_ ⪯ _ [in StructuralProperties]other
_ ⊢ _ <⦂ _ [in Definitions]_ ⊢ _ ⦂ _ [in Definitions]
_ ⊢S _ <⦂ _ [in Stareat]
_ ⊢ _ ↘ _ ⊢! _ [in Stareat]
_ ⊢ _ ↗ _ ⊢! _ [in Stareat]
_ ⊢ _ ⤊ _ ⊢! _ [in Stareat]
_ ⊆<⦂ _ [in OpeSub]
_ ⊢ _ ↘! _ [in Step]
_ ⊢ _ ↗! _ [in Step]
_ ⊢ _ ⇑ _ [in Step]
[ _ , _ ] _ ⊢k _ <⦂ _ k⊣ _ [in StrongKernel]
[ _ ] _ >> _ <⦂p _ << _ [in StrongKernel]
[ _ ] _ ⊢k _ <⦂ _ k⊣ _ [in StrongKernel]
[ _ ] _ >> _ <⦂ _ << _ [in Stareat]
[ _ , _ ] _ ⊢k _ <⦂ _ [in Kernel]
[ _ ] _ ⊢k _ <⦂ _ [in Kernel]
[ _ ] _ ⊢s _ <⦂ _ [in Step]
Variable Index
O
OpenFreshInj.z [in OperationProperties]S
SubstFresh.x [in OperationProperties]SubstFresh.y [in OperationProperties]
SubstFvarProps.subst_open_comm [in OperationProperties]
SubstFvarProps.t [in OperationProperties]
SubstFvarProps.T [in OperationProperties]
SubstFvarProps.x [in OperationProperties]
SubstFvarProps.y [in OperationProperties]
SubstFvarProps.z [in OperationProperties]
SubstOpenComm.x [in OperationProperties]
SubstOpenComm.y [in OperationProperties]
Library Index
D
DefinitionsK
KernelM
MiscO
OperationPropertiesOpeSub
S
StareatStep
StrongKernel
StructuralProperties
V
VarDefLemma Index
A
avar_search_equiv [in Step]B
bsubtyp_sound [in Stareat]bv_search_idx [in Step]
bv_search_equiv [in Step]
C
close_lc_val [in OperationProperties]close_lc_trm [in OperationProperties]
close_lc_typ [in OperationProperties]
close_lc_avar [in OperationProperties]
D
downcast_f_dep_eq_downcast_f [in Stareat]downcast_f_u_eq [in Stareat]
downcast_func_decreases_measure [in Stareat]
downcast_func_sound_wrt_spec [in Stareat]
downcast_preserves_wf [in Stareat]
downcast_sound [in Stareat]
downcast_decreases_measure [in Stareat]
downcast_e'_to_downcast_e [in Kernel]
downcast_e_measure_decrease [in Step]
downcast_gives_prefix [in Step]
downcast_strengthening [in Step]
downcast_e_to_downcast [in Step]
downcast_e_preserves_lc [in Step]
downcast_e_preserves_wf [in Step]
E
env_measure_app [in Misc]env_measure_cons [in Misc]
exposure_measure_decrease [in Step]
exposure_sound [in Step]
exposure_to_exposure' [in Step]
exposure_weakening [in Step]
exposure_preserves_lc [in Step]
exposure_preserves_wf [in Step]
exposure_strengthening [in Step]
exposure_to_revealing [in Step]
exposure_to_revealing_gen [in Step]
exposure'_to_subtysk [in StrongKernel]
exposure'_to_subtykn [in Kernel]
exposure'_equiv_exposure [in Step]
exposure'_to_exposure [in Step]
exposure'_weakening_gen [in Step]
exposure'_weakening [in Step]
F
free_all [in StructuralProperties]fv_add_close_val [in OperationProperties]
fv_add_close_trm [in OperationProperties]
fv_add_close_typ [in OperationProperties]
fv_add_close_avar [in OperationProperties]
fv_close_val [in OperationProperties]
fv_close_trm [in OperationProperties]
fv_close_typ [in OperationProperties]
fv_close_avar [in OperationProperties]
fv_close_self_val [in OperationProperties]
fv_close_self_trm [in OperationProperties]
fv_close_self_typ [in OperationProperties]
fv_close_self_avar [in OperationProperties]
fv_open_val [in OperationProperties]
fv_open_trm [in OperationProperties]
fv_open_typ [in OperationProperties]
fv_open_avar [in OperationProperties]
fv_union [in Definitions]
fv_unpack [in VarDef]
fv_deapp [in Stareat]
fv_ignores_D [in Step]
fv_search_equiv [in Step]
L
layered_bot_trans [in StrongKernel]layered_top_trans [in StrongKernel]
layered_bot_trans [in Kernel]
layered_top_trans [in Kernel]
lc_relax_val [in OperationProperties]
lc_relax_trm [in OperationProperties]
lc_relax_typ [in OperationProperties]
lc_relax_avar [in OperationProperties]
N
narrow_subty [in StructuralProperties]narrow_typing [in StructuralProperties]
narrow_subty_gen [in StructuralProperties]
narrow_typing_gen [in StructuralProperties]
narrow_var [in StructuralProperties]
O
open_substi_rewrite2 [in OperationProperties]open_substi_rewrite [in OperationProperties]
open_fresh_inj_val [in OperationProperties]
open_fresh_inj_trm [in OperationProperties]
open_fresh_inj_typ [in OperationProperties]
open_fresh_inj_avar [in OperationProperties]
open_left_inv_val [in OperationProperties]
open_left_inv_trm [in OperationProperties]
open_left_inv_typ [in OperationProperties]
open_left_inv_avar [in OperationProperties]
open_lc_inv_val [in OperationProperties]
open_lc_inv_trm [in OperationProperties]
open_lc_inv_typ [in OperationProperties]
open_lc_inv_avar [in OperationProperties]
open_lc_le_val [in OperationProperties]
open_lc_le_trm [in OperationProperties]
open_lc_le_typ [in OperationProperties]
open_lc_le_avar [in OperationProperties]
open_lc_val [in OperationProperties]
open_lc_trm [in OperationProperties]
open_lc_typ [in OperationProperties]
open_lc_avar [in OperationProperties]
open_subst_subty [in StructuralProperties]
open_subst_typing [in StructuralProperties]
open_val_same_measure [in Misc]
open_trm_same_measure [in Misc]
open_typ_same_measure [in Misc]
ope_sub_stareat_sound [in Stareat]
ope_sub_app [in OpeSub]
ope_sub_nil [in OpeSub]
ope_sub_refl [in OpeSub]
ope_sub_trans [in OpeSub]
ope_narrow_subty [in OpeSub]
ope_narrow_trm [in OpeSub]
ope_narrow_var [in OpeSub]
ope_sub_length [in OpeSub]
ope_list_fv_env_subset [in Step]
P
prefix_wf_env [in Step]R
renaming_fresh [in StructuralProperties]renaming_subty [in StructuralProperties]
renaming_trm [in StructuralProperties]
revealing_to_subtysk [in StrongKernel]
revealing_fv_bound [in StrongKernel]
revealing_measure [in Stareat]
revealing_preserves_wf [in Stareat]
revealing_sound [in Stareat]
revealing_to_exposure [in Step]
revealing_strengthening [in Step]
revealing_sel_weakening_prefix [in Step]
revealing_sel_weakening [in Step]
revealing_gives_prefix [in Step]
reveal_func_sound_wrt_spec [in Stareat]
S
sk_trans_on_bot [in StrongKernel]sk_trans_on_top [in StrongKernel]
stareat_cong_names [in StrongKernel]
stareat_to_subtysk [in StrongKernel]
stareat_to_stareat' [in StrongKernel]
stareat_strengthening [in Step]
stareat'_to_subtysk [in StrongKernel]
stareat'_weakening_r [in StrongKernel]
stareat'_weakening_l [in StrongKernel]
stareat'_weakening_gen [in StrongKernel]
stareat'_to_stareat [in StrongKernel]
stp_subty'_to_stp_subty [in Kernel]
stp_subty_to_subtykn [in Kernel]
stp_subty_sound [in Step]
stp_subty_to_stareat [in Step]
subenv_implies_uniq [in StructuralProperties]
subenv_last [in StructuralProperties]
subenv_push [in StructuralProperties]
subenv_refl [in StructuralProperties]
subst_intro_typ [in OperationProperties]
subst_intro_val [in OperationProperties]
subst_intro_trm [in OperationProperties]
subst_open_comm_val [in OperationProperties]
subst_open_comm_trm [in OperationProperties]
subst_open_comm_typ [in OperationProperties]
subst_open_comm_avar [in OperationProperties]
subst_fresh_val [in OperationProperties]
subst_fresh_trm [in OperationProperties]
subst_fresh_typ [in OperationProperties]
subst_fresh_avar [in OperationProperties]
subst_trm_var [in StructuralProperties]
subtykn_to_subtysk [in StrongKernel]
subtykn_equiv_stp_subty [in Kernel]
subtykn_to_stp_subty [in Kernel]
subtykn_to_stp_subty' [in Kernel]
subtykn_equiv_subtykn' [in Kernel]
subtykn_to_subtykn' [in Kernel]
subtykn_sound [in Kernel]
subtykn'_to_subtykn [in Kernel]
subtysk_equiv_stareat [in StrongKernel]
subtysk_to_stareat [in StrongKernel]
subtysk_to_stareat' [in StrongKernel]
subtysk_equiv_subtysk' [in StrongKernel]
subtysk_to_subtysk' [in StrongKernel]
subtysk_sound [in StrongKernel]
subtysk_sound_gen [in StrongKernel]
subtysk'_to_subtysk [in StrongKernel]
subty_subst [in StructuralProperties]
subty_subst_gen [in StructuralProperties]
T
total_app [in Misc]trans_on_bot [in Kernel]
trans_on_top [in Kernel]
typing_subst [in StructuralProperties]
typing_subst_gen [in StructuralProperties]
typ_struct_measure_ge_1 [in Misc]
U
upcast_f_dep_eq_upcast_f [in Stareat]upcast_f_u_eq [in Stareat]
upcast_func_decreases_measure [in Stareat]
upcast_func_sound_wrt_spec [in Stareat]
upcast_preserves_wf [in Stareat]
upcast_sound [in Stareat]
upcast_decreases_measure [in Stareat]
upcast_e'_to_upcast_e [in Kernel]
upcast_e_measure_decrease [in Step]
upcast_gives_prefix [in Step]
upcast_strengthening [in Step]
upcast_e_to_upcast [in Step]
upcast_e_preserves_lc [in Step]
upcast_e_preserves_wf [in Step]
W
weaken_subty_gen [in StructuralProperties]weaken_typing_gen [in StructuralProperties]
weaken_subtykn [in Kernel]
weaken_subtykn_gen [in Kernel]
wf_fv_is_dom [in Misc]
wf_var_in [in Misc]
wf_uniq [in Misc]
wf_deapp [in Misc]
wf_decons [in Misc]
wf_search_lookup [in Step]
wf_search_wf_ge_1 [in Step]
wf_open_shift [in Step]
wf_search_impl_avar_f_eq [in Step]
wf_lookup_lt [in Step]
wf_search_weaken [in Step]
wf_search_fv_weaken [in Step]
Constructor Index
A
avar_f [in VarDef]avar_b [in VarDef]
B
bs'_bnd [in StrongKernel]bs'_all [in StrongKernel]
bs'_sel_right [in StrongKernel]
bs'_sel_left [in StrongKernel]
bs'_sel_refl [in StrongKernel]
bs'_top [in StrongKernel]
bs'_bot [in StrongKernel]
bt_bnd [in Stareat]
bt_all [in Stareat]
bt_sel_right [in Stareat]
bt_sel_left [in Stareat]
bt_sel_refl [in Stareat]
bt_top [in Stareat]
bt_bot [in Stareat]
D
dce_bnd [in Step]dce_top [in Step]
dce_bot [in Step]
dc_bnd [in Stareat]
dc_top [in Stareat]
dc_bot [in Stareat]
de_bnd [in Kernel]
de_top [in Kernel]
de_bot [in Kernel]
E
exp_bnd [in Step]exp_bot [in Step]
exp_top [in Step]
exp_stop [in Step]
ex_bnd [in Step]
ex_bot [in Step]
ex_top [in Step]
ex_stop [in Step]
L
lc_val_lam [in Definitions]lc_val_bnd [in Definitions]
lc_trm_let [in Definitions]
lc_trm_app [in Definitions]
lc_trm_val [in Definitions]
lc_trm_var [in Definitions]
lc_typ_bnd [in Definitions]
lc_typ_all [in Definitions]
lc_typ_sel [in Definitions]
lc_typ_bot [in Definitions]
lc_typ_top [in Definitions]
lc_af [in Definitions]
lc_ab [in Definitions]
lc_cons [in Step]
lc_nil [in Step]
O
os_keep [in OpeSub]os_drop [in OpeSub]
os_nil [in OpeSub]
R
rt_bnd [in Stareat]rt_bot [in Stareat]
rt_top [in Stareat]
rt_stop [in Stareat]
rv_bnd [in Stareat]
rv_bot [in Stareat]
rv_top [in Stareat]
rv_stop [in Stareat]
S
sa_bnd [in Stareat]sa_all [in Stareat]
sa_sel_right [in Stareat]
sa_sel_left [in Stareat]
sa_sel_refl [in Stareat]
sa_top [in Stareat]
sa_bot [in Stareat]
snf_sel2 [in Kernel]
snf_sel1 [in Kernel]
snf_all [in Kernel]
snf_bnd [in Kernel]
snf_bot [in Kernel]
snf_top [in Kernel]
snf_vrefl [in Kernel]
snf'_sel2 [in Kernel]
snf'_sel1 [in Kernel]
snf'_all [in Kernel]
snf'_bnd [in Kernel]
snf'_bot [in Kernel]
snf'_top [in Kernel]
snf'_refl [in Kernel]
ssk_sel2 [in StrongKernel]
ssk_sel1 [in StrongKernel]
ssk_all [in StrongKernel]
ssk_bnd [in StrongKernel]
ssk_bot [in StrongKernel]
ssk_top [in StrongKernel]
ssk_refl [in StrongKernel]
ssk'_sel2 [in StrongKernel]
ssk'_sel1 [in StrongKernel]
ssk'_all [in StrongKernel]
ssk'_bnd [in StrongKernel]
ssk'_bot [in StrongKernel]
ssk'_top [in StrongKernel]
ssk'_refl [in StrongKernel]
sst_all [in Step]
sst_bnd [in Step]
sst_sel_right [in Step]
sst_sel_left [in Step]
sst_sel_refl [in Step]
sst_bot [in Step]
sst_top [in Step]
ss_all [in Step]
ss_bnd [in Step]
ss_sel_right [in Step]
ss_sel_left [in Step]
ss_sel_refl [in Step]
ss_bot [in Step]
ss_top [in Step]
ss'_all [in Kernel]
ss'_bnd [in Kernel]
ss'_sel_right [in Kernel]
ss'_sel_left [in Kernel]
ss'_sel_refl [in Kernel]
ss'_bot [in Kernel]
ss'_top [in Kernel]
st_sel2 [in Definitions]
st_sel1 [in Definitions]
st_all [in Definitions]
st_bnd [in Definitions]
st_trans [in Definitions]
st_bot [in Definitions]
st_top [in Definitions]
st_refl [in Definitions]
subenv_grow [in StructuralProperties]
subenv_empty [in StructuralProperties]
T
trm_let [in Definitions]trm_app [in Definitions]
trm_val [in Definitions]
trm_var [in Definitions]
typ_bnd [in Definitions]
typ_all [in Definitions]
typ_sel [in Definitions]
typ_bot [in Definitions]
typ_top [in Definitions]
ty_sub [in Definitions]
ty_let [in Definitions]
ty_app [in Definitions]
ty_lam [in Definitions]
ty_bnd [in Definitions]
ty_var [in Definitions]
U
uce_bnd [in Step]uce_bot [in Step]
uce_top [in Step]
uc_bnd [in Stareat]
uc_bot [in Stareat]
uc_top [in Stareat]
ue_bnd [in Kernel]
ue_bot [in Kernel]
ue_top [in Kernel]
V
val_lam [in Definitions]val_bnd [in Definitions]
W
wf_cons [in Misc]wf_nil [in Misc]
Inductive Index
A
avar [in VarDef]D
downcast [in Stareat]downcast_e' [in Kernel]
downcast_e [in Step]
E
exposure [in Step]exposure' [in Step]
I
incr_lc [in Step]L
lc_val_at [in Definitions]lc_trm_at [in Definitions]
lc_typ_at [in Definitions]
lc_avar_at [in Definitions]
O
ope_sub [in OpeSub]R
revealing [in Stareat]revealing_termination [in Stareat]
S
stareat [in Stareat]stareat_termination [in Stareat]
stareat' [in StrongKernel]
stp_subty' [in Kernel]
stp_subty_termination [in Step]
stp_subty [in Step]
subenv [in StructuralProperties]
subty [in Definitions]
subtykn [in Kernel]
subtykn' [in Kernel]
subtysk [in StrongKernel]
subtysk' [in StrongKernel]
T
trm [in Definitions]typ [in Definitions]
typing [in Definitions]
U
upcast [in Stareat]upcast_e' [in Kernel]
upcast_e [in Step]
V
val [in Definitions]W
wf_env [in Misc]Section Index
A
Algorithmic [in Step]B
BiSubtyProperties [in Stareat]BisubtyStronger [in Step]
C
ClosingDefinitions [in Definitions]D
DowncastProperties [in Stareat]E
EquivalentRepr [in Step]F
FreeVariables [in Definitions]FvClose [in OperationProperties]
FvOpen [in OperationProperties]
L
LcOpenClosingProperties [in OperationProperties]LocalClosure [in Definitions]
M
MeasuresAndFacts [in Step]O
OpenFreshInj [in OperationProperties]OpeningDefinitions [in Definitions]
OpeProperties [in OpeSub]
P
Predicates [in Misc]R
RevealingProperties [in Stareat]RevealingSubsumesExposure [in Step]
S
StructuralProperties [in StructuralProperties]SubstFresh [in OperationProperties]
SubstFvarProps [in OperationProperties]
SubstIntro [in OperationProperties]
Substitutions [in Definitions]
SubstOpenComm [in OperationProperties]
T
Termination [in Stareat]U
UpcastProperties [in Stareat]Instance Index
C
CloseAvar [in Definitions]CloseTrm [in Definitions]
CloseTyp [in Definitions]
CloseVal [in Definitions]
E
EqAvar [in VarDef]EqDecTyp [in Definitions]
F
FvAvar [in Definitions]FvDenv [in Step]
FvEnv [in Definitions]
FvTrm [in Definitions]
FvTyp [in Definitions]
FvVal [in Definitions]
L
LcAvar [in Definitions]LcTrm [in Definitions]
LcTyp [in Definitions]
LcVal [in Definitions]
O
OpenAvar [in Definitions]OpenTrm [in Definitions]
OpenTyp [in Definitions]
OpenVal [in Definitions]
S
SubstAvar [in Definitions]SubstiEnv [in StructuralProperties]
SubstTrm [in Definitions]
SubstTyp [in Definitions]
SubstVal [in Definitions]
Abbreviation Index
C
close_lc [in OperationProperties]D
denv [in Step]E
env [in Definitions]F
fresh_inj [in OperationProperties]fv_add_close [in OperationProperties]
fv_close [in OperationProperties]
fv_close_self [in OperationProperties]
fv_open [in OperationProperties]
L
lc_relax [in OperationProperties]N
narrowing [in StructuralProperties]O
open_left_inv [in OperationProperties]open_lc_inv [in OperationProperties]
open_lc_le [in OperationProperties]
open_lc [in OperationProperties]
S
subst_intro [in OperationProperties]subst_open_comm [in OperationProperties]
subst_fresh [in OperationProperties]
Definition Index
B
bnd_layer [in Kernel]bsubtyp [in Stareat]
C
close_rec_val [in Definitions]close_rec_trm [in Definitions]
close_rec_typ [in Definitions]
close_rec_avar [in Definitions]
D
denv_measure [in Step]denv_fv [in Step]
downcast_f_dep [in Stareat]
downcast_f_u [in Stareat]
downcast_func [in Stareat]
E
env_measure [in Misc]eq_typ_sel [in Stareat]
F
fv_val [in Definitions]fv_trm [in Definitions]
fv_typ [in Definitions]
fv_avar [in Definitions]
fv_values [in VarDef]
I
is_bnd_dec [in Misc]is_bnd [in Misc]
is_all_dec [in Misc]
is_all [in Misc]
is_sel_dec [in Misc]
is_sel [in Misc]
is_bot_dec [in Misc]
is_bot [in Misc]
is_top_dec [in Misc]
is_top [in Misc]
O
open_rec_val [in Definitions]open_rec_trm [in Definitions]
open_rec_typ [in Definitions]
open_rec_avar [in Definitions]
open_rec_D [in Step]
R
revealing_terminates [in Stareat]reveal_func [in Stareat]
S
stareat_terminates [in Stareat]stareat_refl [in Stareat]
stp_subty'_refl [in Kernel]
stp_subty_terminates [in Step]
subst_fvar [in OperationProperties]
subst_val [in Definitions]
subst_trm [in Definitions]
subst_typ [in Definitions]
subst_avar [in Definitions]
subst_env [in StructuralProperties]
subtykn_refl [in Kernel]
subtykn'_conversions [in Kernel]
subtysk_refl [in StrongKernel]
subtysk'_conversions [in StrongKernel]
subty_measure [in Stareat]
T
total [in Misc]trm_struct_measure [in Misc]
typ_struct_measure [in Misc]
U
upcast_f_dep [in Stareat]upcast_f_u [in Stareat]
upcast_func [in Stareat]
V
val_struct_measure [in Misc]W
weaken_subty [in StructuralProperties]weaken_typing [in StructuralProperties]
wf_open_shift_gen [in Step]
wf_search_weaken_gen [in Step]
wf_weaken_measure [in Step]
wf_search_avar [in Step]
wf_search_bv [in Step]
wf_search_fv [in Step]
wf_search [in Step]
wf_search_impl [in Step]
wf_measure [in Step]
| 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 | (573 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) |
| 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 | (11 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 | (10 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 | (211 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 | (153 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 | (34 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 | (26 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 entries) |
| 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 | (17 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 | (68 entries) |


LANG_BRUTE_FORCE_MONITOR=Brute Force Monitor
LANG_FAILED_LOGINS=Failed Logins
LANG_CLICK_IP_TO_FILTER=Click IP address or User to filter results
LANG_CLEAR_SEARCH_FILTER=Clear Search Filter
LANG_SKIP_LIST=Skip List
LANG_LOG_SCANNING_OFF=Log Scanning is not currently turned on. Enable it from your Admin Settings
LANG_IP_ZERO=IP limit is set to 0. Admins will not be notified for failed login attempts from an IP.
LANG_IP_VALUE=Admins will be notified when an IP makes |IP_LIMIT| failed attempts.
LANG_USER_ZERO=User limit is set to 0. Admins will not be notified for failed attempts on a specific account.
LANG_USER_VALUE=Admins will be notified when |USER_LIMIT| failed attempts are made on a specific account.
LANG_ADD_TO_SKIP=Add to Skip List
LANG_COMMENTS=Comments
LANG_BLOCK_IPS=Block IPs
LANG_ARE_YOU_SURE_BLOCK=Are you sure you want to block these IPs?
LANG_BLOCKED_IPS=Blocked IPs
LANG_UNBLOCK=UnBlock
LANG_OPTIONAL_IP=Optional IP/Range/Domain


Project Timeline
-
Project norm submission
As the initial step of the individual research project student should require submitting their one-page project norms including problem, solution, technology and the area of the research project. Appendix 1 shows the sample project norm submission form. This should be done in the first week of the first semester. At this point, a student should able to present their project ideas including Suitable title of the project, problem solution and area of the research.
-
Project proposal submission
After allocating a supervisor, the student should require submitting their project proposal including Introduction to project, the area of the research with some motivation, problem, solution, the significance of the project, aim and objectives, requirements, action plan and ethical clearance. At the end of the research student should able to present innovative and/or a creative product as a solution to a real-world problem. The proposal is also the first document that should require describing proposed activities clearly.
-
Project proposal presentation
The student should able to present their project proposal with incorporating the supervisor’s comments. The scope of the project and the suitability (Ethical concern etc.) will consider in the proposal evaluation. Project proposal should evaluate by two examiners with supervisor observation. Total marks allocate to the project proposal is 10 marks. Evaluation sheet of the Project proposal is attached in Appendix 02. If the proposed project is not in the proper stranded, student should able to re-submit another proposal and evaluation panel can be decided whether student able to re-present or not.
-
Apply for final year research project
After accepting the project proposal student and supervisor should require submitting dually completed project proposal application to the project coordinator for further approval. After getting this approval student not allow to do any modifications. Sample application for the final year research project attached in the appendix 3.
-
Supervisor meetings
-
Interim report 1 submission
Student required to submit first interim report including introduction, Lecturer Review, approach, Design and discussion chapters. The supervisor should correct the report and handover to the student at the progress review. Use the final thesis format as the interim report format and which is given in the appendix 7.
-
Progress Review 1
Student required to present his progress for the panel with the supervisor. Up to this point, the student needs to complete and present their review, approach and system design. In addition to the above, student should require demonstrating prototype system. Evaluation form of the 1st progress review is attached in Appendix 5. Total marks allocated for the first progress review is 10. Time allocate for the progress review 10 min presentation+ 5 min demonstration + 10 min discussion.
-
Interim report 2 submission
Student required to submit their second interim report including introduction, Lecturer Review, approach and Design, Technology, Implementation, Evaluation (in complete) and discussion chapters. The supervisor should correct the report and handover to the student at the second progress review. Use the thesis format as the interim report format. (Note that, the student required to write only technology, implementation, and evaluation chapters. The other chapters already submitted in the first progress review).
-
Progress Review 2
Student required to present his progress for the panel with supervisor Up to this point student need to complete implementation and some part of the system evaluation. Evaluation form of the 2nd progress review is attached in Appendix 6. In the second progress review student should able to demonstrate their complete system demonstration. Total marks allocated for the second progress review is 10. Time allocate for the progress review 5 min presentation + 10 min demonstration + 10 min discussion.
-
Publish your research work
The student can publish their research work according to the supervisor comments. According to the content of the research paper and the index value of the publication marks are given for the publications. Total 10 marks allocated for research publication(s). Note that, a student can publish a review paper, conference paper or journal paper. If it is unpublished work some marks are deducted.
-
Draft thesis submission
The student should able to submit 2 copies of their draft thesis with a Soft copy (MS-Word or Latex) and the complete source code of the project with project demonstration video (10 minutes). Thesis guideline and sample temple for MSWord and Latex is also given to the student. The general guideline for the thesis preparation is attached in Appendix 7. Note that word limit of the thesis is 15000 ± 10% words.
-
Final presentation + VIVA
The student should able to present their completed project work on the final viva. Evaluation sheet of the Final presentation is attached in Appendix 9. The final presentation should have held before the second-semester examination. Total marks allocated for the final VIVA is 30. Time allocate for the progress review 10 min presentation + 10 min demonstration + 30 min. VIVA.
-
Final Thesis submission
Student able to submit their 3 copies of hard bind final thesis with CDs including soft copy and the complete source code with project demonstration video (Maximum 5 min). The guideline is also given to the student.


If your castle is destroyed, you lose! Destroy the opponent's castle to win!
Left click to select a unit, or drag to select multiple.
Right click to order selected units to move, attack, or mine gold (peasants only).
Each mining peasant increases your gold per 5 seconds by 2.
Each building periodically creates units, up to 8 units for that building type.
Additional buildings of the same type will increase the maximum possible units of that type by an additional 8.
AVAILABLE BUILDINGS:
(Select a peasant and press key)
T - Tavern - Recruits - 100g
B - Barracks - Knights - 150g
R - Range - Archers - 200g
H - Horse Stables - Cavalry - 250g
NOTE: Your progress will be saved (via cookies) every 10 seconds; close or reload the page to resume later. However, if your
last game already ended in a victory or defeat, the 'Load Saved Game' button will instead start a new game.


McDonald's employee charged in tampering of police officer's food
by Michael HollanManagement at a McDonald’s reportedly caught an employee tampering with food being prepared for a police officer.
The employee was taken into custody after the local sheriff’s office was made aware of the incident. The suspect had previously accused the local police department of excessive force for a 2017 encounter with law enforcement officers.
The incident occurred at a McDonald’s in Bakersfield, Calif., ABC 23 reports. According to the report, the employee allegedly tampered with a police officer’s food on Tuesday. She was taken into custody on Saturday morning. She was booked on one felony count of tampering with food.
The restaurant's management became aware of the incident while reviewing footage, which they turned over to authorities.
COOK OUT MANAGER WHO WAS FIRED AFTER COP WAS REFUSED SERVICE SAYS EMPLOYEES FOLLOWED STORE POLICY
In a press release obtained by ABC 23, the Kern County Sheriff’s Office said that they obtained video footage of Tatyana Hargrove tampering with the food. Based on the footage, her actions appeared to be intentional.
It has not been revealed what exactly Hargrove did to the food, but the Bakersfield Police Department confirmed to Bakersfield.com that a BPD officer was involved in the incident.
CLICK HERE TO SIGN UP FOR OUR LIFESTYLE NEWSLETTER
In 2017, Hargrove sued the city of Bakersfield, alleging excessive force and civil rights violations after she was reportedly mistaken for a male suspect. ABC 23 reports that officers looking for a male suspect who was 5 feet 10 inches tall and weighed 160 pounds approached Hargrove, who is 5 feet 2 inches tall and 120 pounds.
CLICK HERE TO GET THE FOX NEWS APP
The officers denied Hargrove’s claims that officers used excessive force, instead claiming that she resisted arrested. In October, a district court ruled in favor of the arresting officers, ABC 23 reports.
In a statement obtained by Fox News, the McDonald's owner, Jim Abbate, said, "I want to ensure our customers and law enforcement that the behavior exhibited by the individual involved in this incident does not represent my values nor those of my McDonald’s business. When we found out about this disturbing incident, we quickly notified the police. We are cooperating with their investigation and want law enforcement to know they are always welcome at McDonald’s."


Hello again, neighbors.
I have simple and sad news: Things are bad. The spread of Covid-19 is worse than ever - here and across the whole country. The slope of the line means it's going to get much worse over at least the next few weeks. Many many hospital systems are going to be overwhelmed. Ours in Seattle still has better-than-average capacity, but I can't predict whether it will be enough.
Protect yourselves. Wear a mask. Use grocery pickup. As much as you possibly can, avoid all indoor gatherings of any kind and stay away from crowds outside. (This is my advice, not the current legal requirements.) Remember, anyone you see likely sees other people. Don't breathe "used" indoor air (pretend everyone is breathing out toxic smoke). Keep washing your hands after contacting public surfaces. Use video calls in lieu of holiday gatherings, to protect yourself and your dearest loved ones.
Our neighborhood has been relatively sheltered and privileged so far, compared to most. That comparative fortune will likely continue, but we won't be unscathed. If you've had a Covid-19 case in your household or the houses next to yours at any time, would you please just hit 'reply' and let me know?
In our two census tracts (14 and 16), at least 30% of residents have taken a test for the virus at some point, with positive results being about 2% of those (compared to 3.4% cumulatively for Seattle). The two dozen deaths in our zip code have been in other nearby neighborhoods. I presume that everyone has had their support systems in place for months, but if yours breaks down and you don't know what else to do, let me know - you can respond to this email or call the phone number down below.
My best wishes go out to all of you during this hard and strange winter. Stay (virtually) connected to your favorite humans and love each other well.
Peace and good fortune to you,
James
|
|
|
|


Notice to Centre, AIIMS over plea on quota for disabled
Plea claims institute not providing adequate quota for differently abled for PG programmes
by Staff ReporterThe Delhi High Court on Tuesday issued notice to the Centre and the All India Institute of Medical Sciences (AIIMS) on a petition claiming that the premier institution was not providing adequate reservation to persons with disabilities (PWD) in its post graduate programme.
A Bench of Chief Justice D.N. Patel and Justice C. Hari Shankar sought the response on the plea by NGO Prhari Sahyog Association, which has alleged that there is “non-inclusiveness of PWD” in the institute.
The NGO, in its petition filed through advocate Gaurav Kumar Bansal, has contended that AIIMS has failed to adopt the principle of inclusive education as it provided only one PG seat out of a total of 435 advertised in 2018-19, to PWD when it was legally bound to reserve 5% of seats for PWD.
The petition has also claimed that the United Nation Convention on the Rights of Persons with Disabilities makes it mandatory for their member States to adopt the principle of inclusive education. It has urged the court to call for a status report from AIIMS indicating the efforts made by it to provide inclusive education to PWD.


When to Ship It, When to Kill It
A few weeks ago at lunch I had the opportunity to catch up with a company in the current YC batch, building something very similar to dataclips. While we talked about a lot of things from what we’ve learned from dataclips, marketing, and other areas. One area we talked about was product and when to ship vs. when to kill things and I realized I hadn’t talked on my fairly simple but clear view on this publicly, so here it is.
A large credit to Adam Wiggins for giving this model early on in Heroku and his approach to shipping product.
A precursor to shipping
First a little background on shipping, in shipping something I’m going to assume you have some process of alpha/beta testing with users. This is actually fairly key, if you’re not testing it with users then well the rest of this is all moot. Alpha and beta testing is pretty simple, you need some early users. These can be friends, people within a network, or random users you select from. There’s different value to how you select these but that’s a topic for another time and place.
On to shipping
So how do you know it’s ready. The basic idea is super simple. Give it to some users in alpha/beta testing. Or start to roll it out following a one –> some –> many all principle (maybe to 5% or 10% of your userbase). Then take that brand new feature away.
There’s a couple of ways to do this as far as mechanics. If you’re in contact with users such as alpha/beta users that you were higher touch with just email them. Tell them you’re removing the feature, or if you want to approach it more softly ask them how much they’d miss it if it were gone tomorrow. If you’re rolling it out more broadly perhaps behind a feature flag, flip it off and watch for feedback.
Once you take the feature away or threaten to if you don’t have users with pitchforks almost immediately then it’s not ready to ship.
Go back to the drawing board and work more on it or simply kill it. As @james_heroku would say: “So you’re saying the reason to ship the shitty thing now is becase you’ve spent a lot of time on it?”. Stepping back it’s all logical, but all too often it’s not put in practice when shipping it.
Your metrics can lie
Relying on just seeing a user spend some time on the new feature can often be misleading vs. the above approach. There’s a great talk by Des Traynor over at intercom.io that hits on this in part, the basic premise in there is that users shifting time from feature X to Y doesn’t mean it was a success it just means they’re spending time on something different. In launching new things you want to increase the overall value of your product, not simply shift users focus to the new flavor of the week.


INTRODUCTION ¶
Time and again, researchers are presented with problems for which they postulate and test hypotheses in order to provide us with robust explanations for research questions successfully investigated. Often enough, solid explanations for complex problems require exploring a multitude of datasources. This is the case, for example, in domains such as e-science (multiple scientific datasets), e-commerce (multiple product vendors), tourism (multiple data providers), e-social science, digital humanities, etc.
1. Context¶
DATA INTEGRATION. The use of various datasources come at the expense of heterogeneity which obfuscates the path to data integration and thereby hinders accurately addressing complex problems.
Dealing with multiple datasources or data providers highlights the freedom at which providers document facets of the same entity. Indeed, this feature of oriented freedom for entity descriptions can explain, to a certain extent, the inherent difficulty to integrate heterogeneous datasources.
In the Semantic Web, this problem is partially circumvented as any pair of resources can be linked regardless to the uniformity of data representation or vocabulary used, i.e. uniformizing data/schema is not a prerequisite for data integration provided that links between co-referent entities across heterogeneous datasets exist.
RESULT QUALITY. The quality of supporting evidence for accepting or rejecting the hypothesis under investigation for a complex problem greatly depends on the correctness of the links integrating the underlying datasources.
This begs for questions regarding the aboutness and correctness of the links, such as:
-
How to create correct links? More specifically, are there reliable tools or macthing algorithms for linking co-referent descriptions of entity scattered across various heterogeneous datasets? Can different tools or algorithms be combined?
-
How to judge the applicability of links? Can their quality be estimated? Can they be improved, manipulated, visualised for validation purposes, reproduced? More specifically, is there a platform that supports all of the aforementioned concerns?
LINK CONSTRUCTION. Through the years, a number of entity matching tools have been developed and tested.
However, some of theses tools have been developed for specific datasets, while others have limited applicability as they have mainly been tested in domain specific areas using synthetic or simplistic data, generally from at most two datasets. For example, as research in social sciences is increasingly based on multiple heterogeneous datasources, it becomes problematic to be limited to the integration of two datasets.
Furthermore, in practice, the heterogeneity, messiness, incompleteness of data raise the bar higher in terms of entity matching complexity.
In other words, most matching algorithms have been successfully applied in limited and controlled environments. This motivates the need for having the means to (re)use and combine generic matching approaches in order to solve specific problems.
2. Disambiguation Proposal¶
In this document, we present a tool that supports disambiguation over multiple datasets: the Lenticular Lens. As a domain agnostic approach, the Lenticular Lens tool reuses existing matching approaches to allow for the user to reach their goals in ways that alleviates some of the main aforementioned issues:
-
User-dependent and context-specific link discovery.
-
User-based explicit concept mapping.
-
Integration of more than two datasets.
-
Combining entity matching algorithms and results.
-
Structure-based evaluation of identity link networks.
-
Enabling visualisation to support link/cluster validation.
-
Metadata for documenting the link aboutness and enabling reproducibility.
The context dependent link discovery idea developed and implemented in the Lenticular Lens [Idrissou 2017, 2018, 2019] is an extension of the Linkset and Lens concepts introduced by the [OpenPhacts] project in the quests for building an infrastructure for integrating pharmacological data. Our extension and broadening of these concepts enabled us to design and build a flexible tool for undertaking entity disambiguation in a broader perspective.
2.1 Workflow¶
The Lenticular Lens tool offers the users a number of matching-related mandatory and optional tasks to achieve their integration-goals. A workflow depicting possible sequences of executions for those tasks is presented in Figure 1. The process starts with (1) Data Selection and is followed by (2) Link Creation (Linkset). The next optional steps include: (3) Link Manipulation (Lens) for combining previously obtained links; (4) Link Validation for the curation of the obtained links; (5) Link Visualisation to support the verification of the quality of the obtained links; (6) Export Linksets/Lenses to extract the obtained links from the tool and finally (7) Export Integrated Data of Interest to support the user on the extraction of specific descriptions (property values) of integrated entities.
2.1 Dataflow¶
The data used as input to the Lenticular Lens originates from a Timbuctoo Endpoint. The pulled data is then stored and manipulated in PostgreSQL for efficiency purposes. The resultant links generated by the Lenticular Lens tool can be injected back into the Timbuctoo Enpoint, which in turn also enables communication with a SPARQL Enpoint.
3. GUI Menus¶
As a preview of what can be done with the Lenticular Lens tool, we list here the main menus composing the tool and provide a brief description of what can be done in each of the menu.
CONTEXT
This menu aims to specify the scope of the research by giving the researcher the opportunity to remind herself and other users the why of the research. This is done by providing a title, describing the goal and possibly linking the work done in this tool to a published result.
DATA
This menu provides means to:
- Select a GraphQL endpoint so that remote datasources can be located and made available to the user. The default selection is the Golden Agent’s endpoint ;
- Select Datasources and Entity-types from the available list at the remote location so that information can be extracted and integrated in order to conduct an experiment;
- Define restrictions over selected Entity-types.
- Explore data based on pre-defined specifications (Datasource, Entity-type and Property-value Restrictions).
LINKSET
This menu provides means to:
-
Specify the conditions in which to use a matching method or combined matching methods for the creation of a LINKSET, which is a set of links sharing the same specifications.
-
Run the specification i.e create set of links and clusters.
-
Get statistics on the result such as the total number of links found, how they cluster…
-
Validate the resulting links by annotating them with flags such as accept or reject.
-
Export the result in various format.
LENS
This menu provides means to:
-
Specify the conditions in which to combine LINKSET(S) and/or LENS(ES) for the creation of a new LENS, specifically, the use of set like operations (Union, Intersection, Difference, Composition and In-Set) over linksets and lenses.
-
Run the specification i.e combine Linkset(s) and/or Lens(es) and cluster the links.
-
Get statistics on the result such as the total number of links found, how they cluster…
-
Visualise and Validate the resulting links by annotating them with flags such as accept or reject.
-
Export the result in various format.
DATA INTEGRATION
The menu here enables the user to materialise an entity-based integration of her selected datasources for the extraction of information vital to her analysis.
The rest of the manual will discuss
- Terminology
- Link Annotation Ontology
- Algorithms
- Link Construction (it includes the
RESEARCH
,DATA
andCREATE
options) - Link Manipulation (it includes the
MANIPULATE
, andVALIDATION
options) - Link Export (it is about the
EXPORT
option) and - Data Integration (it is about the
EXTRACT
option)


{% load static from staticfiles %}
{% verbatim nabu %}
AKWriters Chat
Notifications
{{ status_msg }}
{{ m.from }} has joined the room
{{ m.from }} has left the room
{{ m.from }}
Reconnecting in {{ retry_time }}
{{ o }}
×
{{ chatbox }}
Send
{% endverbatim nabu %}


val paymentMethodBillingDetails: BillingDetails?
Return a valid PaymentMethod.BillingDetails object based on user input, or null if any field is invalid
null


SUBROUTINE SLARRV( N, VL, VU, D, L, PIVMIN, $ ISPLIT, M, DOL, DOU, MINRGP, $ RTOL1, RTOL2, W, WERR, WGAP, $ IBLOCK, INDEXW, GERS, Z, LDZ, ISUPPZ, $ WORK, IWORK, INFO ) * * -- LAPACK auxiliary routine (version 3.1.1) -- * Univ. of Tennessee, Univ. of California Berkeley and NAG Ltd.. * November 2006 * * .. Scalar Arguments .. INTEGER DOL, DOU, INFO, LDZ, M, N REAL MINRGP, PIVMIN, RTOL1, RTOL2, VL, VU * .. * .. Array Arguments .. INTEGER IBLOCK( * ), INDEXW( * ), ISPLIT( * ), $ ISUPPZ( * ), IWORK( * ) REAL D( * ), GERS( * ), L( * ), W( * ), WERR( * ), $ WGAP( * ), WORK( * ) REAL Z( LDZ, * ) * .. * * Purpose * ======= * * SLARRV computes the eigenvectors of the tridiagonal matrix * T = L D L^T given L, D and APPROXIMATIONS to the eigenvalues of L D L^T. * The input eigenvalues should have been computed by SLARRE. * * Arguments * ========= * * N (input) INTEGER * The order of the matrix. N >= 0. * * VL (input) REAL * VU (input) REAL * Lower and upper bounds of the interval that contains the desired * eigenvalues. VL < VU. Needed to compute gaps on the left or right * end of the extremal eigenvalues in the desired RANGE. * * D (input/output) REAL array, dimension (N) * On entry, the N diagonal elements of the diagonal matrix D. * On exit, D may be overwritten. * * L (input/output) REAL array, dimension (N) * On entry, the (N-1) subdiagonal elements of the unit * bidiagonal matrix L are in elements 1 to N-1 of L * (if the matrix is not splitted.) At the end of each block * is stored the corresponding shift as given by SLARRE. * On exit, L is overwritten. * * PIVMIN (in) DOUBLE PRECISION * The minimum pivot allowed in the Sturm sequence. * * ISPLIT (input) INTEGER array, dimension (N) * The splitting points, at which T breaks up into blocks. * The first block consists of rows/columns 1 to * ISPLIT( 1 ), the second of rows/columns ISPLIT( 1 )+1 * through ISPLIT( 2 ), etc. * * M (input) INTEGER * The total number of input eigenvalues. 0 <= M <= N. * * DOL (input) INTEGER * DOU (input) INTEGER * If the user wants to compute only selected eigenvectors from all * the eigenvalues supplied, he can specify an index range DOL:DOU. * Or else the setting DOL=1, DOU=M should be applied. * Note that DOL and DOU refer to the order in which the eigenvalues * are stored in W. * If the user wants to compute only selected eigenpairs, then * the columns DOL-1 to DOU+1 of the eigenvector space Z contain the * computed eigenvectors. All other columns of Z are set to zero. * * MINRGP (input) REAL * * RTOL1 (input) REAL * RTOL2 (input) REAL * Parameters for bisection. * An interval [LEFT,RIGHT] has converged if * RIGHT-LEFT.LT.MAX( RTOL1*GAP, RTOL2*MAX(|LEFT|,|RIGHT|) ) * * W (input/output) REAL array, dimension (N) * The first M elements of W contain the APPROXIMATE eigenvalues for * which eigenvectors are to be computed. The eigenvalues * should be grouped by split-off block and ordered from * smallest to largest within the block ( The output array * W from SLARRE is expected here ). Furthermore, they are with * respect to the shift of the corresponding root representation * for their block. On exit, W holds the eigenvalues of the * UNshifted matrix. * * WERR (input/output) REAL array, dimension (N) * The first M elements contain the semiwidth of the uncertainty * interval of the corresponding eigenvalue in W * * WGAP (input/output) REAL array, dimension (N) * The separation from the right neighbor eigenvalue in W. * * IBLOCK (input) INTEGER array, dimension (N) * The indices of the blocks (submatrices) associated with the * corresponding eigenvalues in W; IBLOCK(i)=1 if eigenvalue * W(i) belongs to the first block from the top, =2 if W(i) * belongs to the second block, etc. * * INDEXW (input) INTEGER array, dimension (N) * The indices of the eigenvalues within each block (submatrix); * for example, INDEXW(i)= 10 and IBLOCK(i)=2 imply that the * i-th eigenvalue W(i) is the 10-th eigenvalue in the second block. * * GERS (input) REAL array, dimension (2*N) * The N Gerschgorin intervals (the i-th Gerschgorin interval * is (GERS(2*i-1), GERS(2*i)). The Gerschgorin intervals should * be computed from the original UNshifted matrix. * * Z (output) REAL array, dimension (LDZ, max(1,M) ) * If INFO = 0, the first M columns of Z contain the * orthonormal eigenvectors of the matrix T * corresponding to the input eigenvalues, with the i-th * column of Z holding the eigenvector associated with W(i). * Note: the user must ensure that at least max(1,M) columns are * supplied in the array Z. * * LDZ (input) INTEGER * The leading dimension of the array Z. LDZ >= 1, and if * JOBZ = 'V', LDZ >= max(1,N). * * ISUPPZ (output) INTEGER array, dimension ( 2*max(1,M) ) * The support of the eigenvectors in Z, i.e., the indices * indicating the nonzero elements in Z. The I-th eigenvector * is nonzero only in elements ISUPPZ( 2*I-1 ) through * ISUPPZ( 2*I ). * * WORK (workspace) REAL array, dimension (12*N) * * IWORK (workspace) INTEGER array, dimension (7*N) * * INFO (output) INTEGER * = 0: successful exit * * > 0: A problem occured in SLARRV. * < 0: One of the called subroutines signaled an internal problem. * Needs inspection of the corresponding parameter IINFO * for further information. * * =-1: Problem in SLARRB when refining a child's eigenvalues. * =-2: Problem in SLARRF when computing the RRR of a child. * When a child is inside a tight cluster, it can be difficult * to find an RRR. A partial remedy from the user's point of * view is to make the parameter MINRGP smaller and recompile. * However, as the orthogonality of the computed vectors is * proportional to 1/MINRGP, the user should be aware that * he might be trading in precision when he decreases MINRGP. * =-3: Problem in SLARRB when refining a single eigenvalue * after the Rayleigh correction was rejected. * = 5: The Rayleigh Quotient Iteration failed to converge to * full accuracy in MAXITR steps. * * Further Details * =============== * * Based on contributions by * Beresford Parlett, University of California, Berkeley, USA * Jim Demmel, University of California, Berkeley, USA * Inderjit Dhillon, University of Texas, Austin, USA * Osni Marques, LBNL/NERSC, USA * Christof Voemel, University of California, Berkeley, USA * * ===================================================================== * * .. Parameters .. INTEGER MAXITR PARAMETER ( MAXITR = 10 ) REAL ZERO, ONE, TWO, THREE, FOUR, HALF PARAMETER ( ZERO = 0.0E0, ONE = 1.0E0, $ TWO = 2.0E0, THREE = 3.0E0, $ FOUR = 4.0E0, HALF = 0.5E0) * .. * .. Local Scalars ..  * .. External Functions .. REAL SLAMCH EXTERNAL SLAMCH * .. * .. External Subroutines .. EXTERNAL SCOPY, SLAR1V, SLARRB, SLARRF, SLASET, $ SSCAL * .. * .. Intrinsic Functions .. INTRINSIC ABS, REAL, MAX, MIN * .. * .. Executable Statements .. * .. * The first N entries of WORK are reserved for the eigenvalues INDLD = N+1 INDLLD= 2*N+1 INDWRK= 3*N+1 MINWSIZE = 12 * N DO 5 I= 1,MINWSIZE WORK( I ) = ZERO 5 CONTINUE * IWORK(IINDR+1:IINDR+N) hold the twist indices R for the * factorization used to compute the FP vector IINDR = 0 * IWORK(IINDC1+1:IINC2+N) are used to store the clusters of the current * layer and the one above. IINDC1 = N IINDC2 = 2*N IINDWK = 3*N + 1 MINIWSIZE = 7 * N DO 10 I= 1,MINIWSIZE IWORK( I ) = 0 10 CONTINUE ZUSEDL = 1 IF(DOL.GT.1) THEN * Set lower bound for use of Z ZUSEDL = DOL-1 ENDIF ZUSEDU = M IF(DOU.LT.M) THEN * Set lower bound for use of Z ZUSEDU = DOU+1 ENDIF * The width of the part of Z that is used ZUSEDW = ZUSEDU - ZUSEDL + 1 CALL SLASET( 'Full', N, ZUSEDW, ZERO, ZERO, $ Z(1,ZUSEDL), LDZ ) EPS = SLAMCH( 'Precision' ) RQTOL = TWO * EPS * * Set expert flags for standard code. TRYRQC = .TRUE. IF((DOL.EQ.1).AND.(DOU.EQ.M)) THEN ELSE * Only selected eigenpairs are computed. Since the other evalues * are not refined by RQ iteration, bisection has to compute to full * accuracy. RTOL1 = FOUR * EPS RTOL2 = FOUR * EPS ENDIF * The entries WBEGIN:WEND in W, WERR, WGAP correspond to the * desired eigenvalues. The support of the nonzero eigenvector * entries is contained in the interval IBEGIN:IEND. * Remark that if k eigenpairs are desired, then the eigenvectors * are stored in k contiguous columns of Z. * DONE is the number of eigenvectors already computed DONE = 0 IBEGIN = 1 WBEGIN = 1 DO 170 JBLK = 1, IBLOCK( M ) IEND = ISPLIT( JBLK ) SIGMA = L( IEND ) * Find the eigenvectors of the submatrix indexed IBEGIN * through IEND. WEND = WBEGIN - 1 15 CONTINUE IF( WEND.LT.M ) THEN IF( IBLOCK( WEND+1 ).EQ.JBLK ) THEN WEND = WEND + 1 GO TO 15 END IF END IF IF( WEND.LT.WBEGIN ) THEN IBEGIN = IEND + 1 GO TO 170 ELSEIF( (WEND.LT.DOL).OR.(WBEGIN.GT.DOU) ) THEN IBEGIN = IEND + 1 WBEGIN = WEND + 1 GO TO 170 END IF * Find local spectral diameter of the block GL = GERS( 2*IBEGIN-1 ) GU = GERS( 2*IBEGIN ) DO 20 I = IBEGIN+1 , IEND GL = MIN( GERS( 2*I-1 ), GL ) GU = MAX( GERS( 2*I ), GU ) 20 CONTINUE SPDIAM = GU - GL * OLDIEN is the last index of the previous block OLDIEN = IBEGIN - 1 * Calculate the size of the current block IN = IEND - IBEGIN + 1 * The number of eigenvalues in the current block IM = WEND - WBEGIN + 1 * This is for a 1x1 block IF( IBEGIN.EQ.IEND ) THEN DONE = DONE+1 Z( IBEGIN, WBEGIN ) = ONE ISUPPZ( 2*WBEGIN-1 ) = IBEGIN ISUPPZ( 2*WBEGIN ) = IBEGIN W( WBEGIN ) = W( WBEGIN ) + SIGMA WORK( WBEGIN ) = W( WBEGIN ) IBEGIN = IEND + 1 WBEGIN = WBEGIN + 1 GO TO 170 END IF * The desired (shifted) eigenvalues are stored in W(WBEGIN:WEND) * Note that these can be approximations, in this case, the corresp. * entries of WERR give the size of the uncertainty interval. * The eigenvalue approximations will be refined when necessary as * high relative accuracy is required for the computation of the * corresponding eigenvectors. CALL SCOPY( IM, W( WBEGIN ), 1, & WORK( WBEGIN ), 1 ) * We store in W the eigenvalue approximations w.r.t. the original * matrix T. DO 30 I=1,IM W(WBEGIN+I-1) = W(WBEGIN+I-1)+SIGMA 30 CONTINUE * NDEPTH is the current depth of the representation tree NDEPTH = 0 * PARITY is either 1 or 0 PARITY = 1 * NCLUS is the number of clusters for the next level of the * representation tree, we start with NCLUS = 1 for the root NCLUS = 1 IWORK( IINDC1+1 ) = 1 IWORK( IINDC1+2 ) = IM * IDONE is the number of eigenvectors already computed in the current * block IDONE = 0 * loop while( IDONE.LT.IM ) * generate the representation tree for the current block and * compute the eigenvectors 40 CONTINUE IF( IDONE.LT.IM ) THEN * This is a crude protection against infinitely deep trees IF( NDEPTH.GT.M ) THEN INFO = -2 RETURN ENDIF * breadth first processing of the current level of the representation * tree: OLDNCL = number of clusters on current level OLDNCL = NCLUS * reset NCLUS to count the number of child clusters NCLUS = 0 * PARITY = 1 - PARITY IF( PARITY.EQ.0 ) THEN OLDCLS = IINDC1 NEWCLS = IINDC2 ELSE OLDCLS = IINDC2 NEWCLS = IINDC1 END IF * Process the clusters on the current level DO 150 I = 1, OLDNCL J = OLDCLS + 2*I * OLDFST, OLDLST = first, last index of current cluster. * cluster indices start with 1 and are relative * to WBEGIN when accessing W, WGAP, WERR, Z OLDFST = IWORK( J-1 ) OLDLST = IWORK( J ) IF( NDEPTH.GT.0 ) THEN * Retrieve relatively robust representation (RRR) of cluster * that has been computed at the previous level * The RRR is stored in Z and overwritten once the eigenvectors * have been computed or when the cluster is refined IF((DOL.EQ.1).AND.(DOU.EQ.M)) THEN * Get representation from location of the leftmost evalue * of the cluster J = WBEGIN + OLDFST - 1 ELSE IF(WBEGIN+OLDFST-1.LT.DOL) THEN * Get representation from the left end of Z array J = DOL - 1 ELSEIF(WBEGIN+OLDFST-1.GT.DOU) THEN * Get representation from the right end of Z array J = DOU ELSE J = WBEGIN + OLDFST - 1 ENDIF ENDIF CALL SCOPY( IN, Z( IBEGIN, J ), 1, D( IBEGIN ), 1 ) CALL SCOPY( IN-1, Z( IBEGIN, J+1 ), 1, L( IBEGIN ), $ 1 ) SIGMA = Z( IEND, J+1 ) * Set the corresponding entries in Z to zero CALL SLASET( 'Full', IN, 2, ZERO, ZERO, $ Z( IBEGIN, J), LDZ ) END IF * Compute DL and DLL of current RRR DO 50 J = IBEGIN, IEND-1 TMP = D( J )*L( J ) WORK( INDLD-1+J ) = TMP WORK( INDLLD-1+J ) = TMP*L( J ) 50 CONTINUE IF( NDEPTH.GT.0 ) THEN * P and Q are index of the first and last eigenvalue to compute * within the current block P = INDEXW( WBEGIN-1+OLDFST ) Q = INDEXW( WBEGIN-1+OLDLST ) * Offset for the arrays WORK, WGAP and WERR, i.e., th P-OFFSET * thru' Q-OFFSET elements of these arrays are to be used. C OFFSET = P-OLDFST OFFSET = INDEXW( WBEGIN ) - 1 * perform limited bisection (if necessary) to get approximate * eigenvalues to the precision needed. CALL SLARRB( IN, D( IBEGIN ), $ WORK(INDLLD+IBEGIN-1), $ P, Q, RTOL1, RTOL2, OFFSET, $ WORK(WBEGIN),WGAP(WBEGIN),WERR(WBEGIN), $ WORK( INDWRK ), IWORK( IINDWK ), $ PIVMIN, SPDIAM, IN, IINFO ) IF( IINFO.NE.0 ) THEN INFO = -1 RETURN ENDIF * We also recompute the extremal gaps. W holds all eigenvalues * of the unshifted matrix and must be used for computation * of WGAP, the entries of WORK might stem from RRRs with * different shifts. The gaps from WBEGIN-1+OLDFST to * WBEGIN-1+OLDLST are correctly computed in SLARRB. * However, we only allow the gaps to become greater since * this is what should happen when we decrease WERR IF( OLDFST.GT.1) THEN WGAP( WBEGIN+OLDFST-2 ) = $ MAX(WGAP(WBEGIN+OLDFST-2), $ W(WBEGIN+OLDFST-1)-WERR(WBEGIN+OLDFST-1) $ - W(WBEGIN+OLDFST-2)-WERR(WBEGIN+OLDFST-2) ) ENDIF IF( WBEGIN + OLDLST -1 .LT. WEND ) THEN WGAP( WBEGIN+OLDLST-1 ) = $ MAX(WGAP(WBEGIN+OLDLST-1), $ W(WBEGIN+OLDLST)-WERR(WBEGIN+OLDLST) $ - W(WBEGIN+OLDLST-1)-WERR(WBEGIN+OLDLST-1) ) ENDIF * Each time the eigenvalues in WORK get refined, we store * the newly found approximation with all shifts applied in W DO 53 J=OLDFST,OLDLST W(WBEGIN+J-1) = WORK(WBEGIN+J-1)+SIGMA 53 CONTINUE END IF * Process the current node. NEWFST = OLDFST DO 140 J = OLDFST, OLDLST IF( J.EQ.OLDLST ) THEN * we are at the right end of the cluster, this is also the * boundary of the child cluster NEWLST = J ELSE IF ( WGAP( WBEGIN + J -1).GE. $ MINRGP* ABS( WORK(WBEGIN + J -1) ) ) THEN * the right relative gap is big enough, the child cluster * (NEWFST,..,NEWLST) is well separated from the following NEWLST = J ELSE * inside a child cluster, the relative gap is not * big enough. GOTO 140 END IF * Compute size of child cluster found NEWSIZ = NEWLST - NEWFST + 1 * NEWFTT is the place in Z where the new RRR or the computed * eigenvector is to be stored IF((DOL.EQ.1).AND.(DOU.EQ.M)) THEN * Store representation at location of the leftmost evalue * of the cluster NEWFTT = WBEGIN + NEWFST - 1 ELSE IF(WBEGIN+NEWFST-1.LT.DOL) THEN * Store representation at the left end of Z array NEWFTT = DOL - 1 ELSEIF(WBEGIN+NEWFST-1.GT.DOU) THEN * Store representation at the right end of Z array NEWFTT = DOU ELSE NEWFTT = WBEGIN + NEWFST - 1 ENDIF ENDIF IF( NEWSIZ.GT.1) THEN * * Current child is not a singleton but a cluster. * Compute and store new representation of child. * * * Compute left and right cluster gap. * * LGAP and RGAP are not computed from WORK because * the eigenvalue approximations may stem from RRRs * different shifts. However, W hold all eigenvalues * of the unshifted matrix. Still, the entries in WGAP * have to be computed from WORK since the entries * in W might be of the same order so that gaps are not * exhibited correctly for very close eigenvalues. IF( NEWFST.EQ.1 ) THEN LGAP = MAX( ZERO, $ W(WBEGIN)-WERR(WBEGIN) - VL ) ELSE LGAP = WGAP( WBEGIN+NEWFST-2 ) ENDIF RGAP = WGAP( WBEGIN+NEWLST-1 ) * * Compute left- and rightmost eigenvalue of child * to high precision in order to shift as close * as possible and obtain as large relative gaps * as possible * DO 55 K =1,2 IF(K.EQ.1) THEN P = INDEXW( WBEGIN-1+NEWFST ) ELSE P = INDEXW( WBEGIN-1+NEWLST ) ENDIF OFFSET = INDEXW( WBEGIN ) - 1 CALL SLARRB( IN, D(IBEGIN), $ WORK( INDLLD+IBEGIN-1 ),P,P, $ RQTOL, RQTOL, OFFSET, $ WORK(WBEGIN),WGAP(WBEGIN), $ WERR(WBEGIN),WORK( INDWRK ), $ IWORK( IINDWK ), PIVMIN, SPDIAM, $ IN, IINFO ) 55 CONTINUE * IF((WBEGIN+NEWLST-1.LT.DOL).OR. $ (WBEGIN+NEWFST-1.GT.DOU)) THEN * if the cluster contains no desired eigenvalues * skip the computation of that branch of the rep. tree * * We could skip before the refinement of the extremal * eigenvalues of the child, but then the representation * tree could be different from the one when nothing is * skipped. For this reason we skip at this place. IDONE = IDONE + NEWLST - NEWFST + 1 GOTO 139 ENDIF * * Compute RRR of child cluster. * Note that the new RRR is stored in Z * C SLARRF needs LWORK = 2*N CALL SLARRF( IN, D( IBEGIN ), L( IBEGIN ), $ WORK(INDLD+IBEGIN-1), $ NEWFST, NEWLST, WORK(WBEGIN), $ WGAP(WBEGIN), WERR(WBEGIN), $ SPDIAM, LGAP, RGAP, PIVMIN, TAU, $ Z(IBEGIN, NEWFTT),Z(IBEGIN, NEWFTT+1), $ WORK( INDWRK ), IINFO ) IF( IINFO.EQ.0 ) THEN * a new RRR for the cluster was found by SLARRF * update shift and store it SSIGMA = SIGMA + TAU Z( IEND, NEWFTT+1 ) = SSIGMA * WORK() are the midpoints and WERR() the semi-width * Note that the entries in W are unchanged. DO 116 K = NEWFST, NEWLST FUDGE = $ THREE*EPS*ABS(WORK(WBEGIN+K-1)) WORK( WBEGIN + K - 1 ) = $ WORK( WBEGIN + K - 1) - TAU FUDGE = FUDGE + $ FOUR*EPS*ABS(WORK(WBEGIN+K-1)) * Fudge errors WERR( WBEGIN + K - 1 ) = $ WERR( WBEGIN + K - 1 ) + FUDGE * Gaps are not fudged. Provided that WERR is small * when eigenvalues are close, a zero gap indicates * that a new representation is needed for resolving * the cluster. A fudge could lead to a wrong decision * of judging eigenvalues 'separated' which in * reality are not. This could have a negative impact * on the orthogonality of the computed eigenvectors. 116 CONTINUE NCLUS = NCLUS + 1 K = NEWCLS + 2*NCLUS IWORK( K-1 ) = NEWFST IWORK( K ) = NEWLST ELSE INFO = -2 RETURN ENDIF ELSE * * Compute eigenvector of singleton * ITER = 0 * TOL = FOUR * LOG(REAL(IN)) * EPS * K = NEWFST WINDEX = WBEGIN + K - 1 WINDMN = MAX(WINDEX - 1,1) WINDPL = MIN(WINDEX + 1,M) LAMBDA = WORK( WINDEX ) DONE = DONE + 1 * Check if eigenvector computation is to be skipped IF((WINDEX.LT.DOL).OR. $ (WINDEX.GT.DOU)) THEN ESKIP = .TRUE. GOTO 125 ELSE ESKIP = .FALSE. ENDIF LEFT = WORK( WINDEX ) - WERR( WINDEX ) RIGHT = WORK( WINDEX ) + WERR( WINDEX ) INDEIG = INDEXW( WINDEX ) * Note that since we compute the eigenpairs for a child, * all eigenvalue approximations are w.r.t the same shift. * In this case, the entries in WORK should be used for * computing the gaps since they exhibit even very small * differences in the eigenvalues, as opposed to the * entries in W which might "look" the same. IF( K .EQ. 1) THEN * In the case RANGE='I' and with not much initial * accuracy in LAMBDA and VL, the formula * LGAP = MAX( ZERO, (SIGMA - VL) + LAMBDA ) * can lead to an overestimation of the left gap and * thus to inadequately early RQI 'convergence'. * Prevent this by forcing a small left gap. LGAP = EPS*MAX(ABS(LEFT),ABS(RIGHT)) ELSE LGAP = WGAP(WINDMN) ENDIF IF( K .EQ. IM) THEN * In the case RANGE='I' and with not much initial * accuracy in LAMBDA and VU, the formula * can lead to an overestimation of the right gap and * thus to inadequately early RQI 'convergence'. * Prevent this by forcing a small right gap. RGAP = EPS*MAX(ABS(LEFT),ABS(RIGHT)) ELSE RGAP = WGAP(WINDEX) ENDIF GAP = MIN( LGAP, RGAP ) IF(( K .EQ. 1).OR.(K .EQ. IM)) THEN * The eigenvector support can become wrong * because significant entries could be cut off due to a * large GAPTOL parameter in LAR1V. Prevent this. GAPTOL = ZERO ELSE GAPTOL = GAP * EPS ENDIF ISUPMN = IN ISUPMX = 1 * Update WGAP so that it holds the minimum gap * to the left or the right. This is crucial in the * case where bisection is used to ensure that the * eigenvalue is refined up to the required precision. * The correct value is restored afterwards. SAVGAP = WGAP(WINDEX) WGAP(WINDEX) = GAP * We want to use the Rayleigh Quotient Correction * as often as possible since it converges quadratically * when we are close enough to the desired eigenvalue. * However, the Rayleigh Quotient can have the wrong sign * and lead us away from the desired eigenvalue. In this * case, the best we can do is to use bisection. USEDBS = .FALSE. USEDRQ = .FALSE. * Bisection is initially turned off unless it is forced NEEDBS = .NOT.TRYRQC 120 CONTINUE * Check if bisection should be used to refine eigenvalue IF(NEEDBS) THEN * Take the bisection as new iterate USEDBS = .TRUE. ITMP1 = IWORK( IINDR+WINDEX ) OFFSET = INDEXW( WBEGIN ) - 1 CALL SLARRB( IN, D(IBEGIN), $ WORK(INDLLD+IBEGIN-1),INDEIG,INDEIG, $ ZERO, TWO*EPS, OFFSET, $ WORK(WBEGIN),WGAP(WBEGIN), $ WERR(WBEGIN),WORK( INDWRK ), $ IWORK( IINDWK ), PIVMIN, SPDIAM, $ ITMP1, IINFO ) IF( IINFO.NE.0 ) THEN INFO = -3 RETURN ENDIF LAMBDA = WORK( WINDEX ) * Reset twist index from inaccurate LAMBDA to * force computation of true MINGMA IWORK( IINDR+WINDEX ) = 0 ENDIF * Given LAMBDA, compute the eigenvector. CALL SLAR1V( IN, 1, IN, LAMBDA, D( IBEGIN ), $ L( IBEGIN ), WORK(INDLD+IBEGIN-1), $ WORK(INDLLD+IBEGIN-1), $ PIVMIN, GAPTOL, Z( IBEGIN, WINDEX ), $ .NOT.USEDBS, NEGCNT, ZTZ, MINGMA, $ IWORK( IINDR+WINDEX ), ISUPPZ( 2*WINDEX-1 ), $ NRMINV, RESID, RQCORR, WORK( INDWRK ) ) IF(ITER .EQ. 0) THEN BSTRES = RESID BSTW = LAMBDA ELSEIF(RESID.LT.BSTRES) THEN BSTRES = RESID BSTW = LAMBDA ENDIF ISUPMN = MIN(ISUPMN,ISUPPZ( 2*WINDEX-1 )) ISUPMX = MAX(ISUPMX,ISUPPZ( 2*WINDEX )) ITER = ITER + 1 * sin alpha <= |resid|/gap * Note that both the residual and the gap are * proportional to the matrix, so ||T|| doesn't play * a role in the quotient * * Convergence test for Rayleigh-Quotient iteration * (omitted when Bisection has been used) * IF( RESID.GT.TOL*GAP .AND. ABS( RQCORR ).GT. $ RQTOL*ABS( LAMBDA ) .AND. .NOT. USEDBS) $ THEN * We need to check that the RQCORR update doesn't * move the eigenvalue away from the desired one and * towards a neighbor. -> protection with bisection IF(INDEIG.LE.NEGCNT) THEN * The wanted eigenvalue lies to the left SGNDEF = -ONE ELSE * The wanted eigenvalue lies to the right SGNDEF = ONE ENDIF * We only use the RQCORR if it improves the * the iterate reasonably. IF( ( RQCORR*SGNDEF.GE.ZERO ) $ .AND.( LAMBDA + RQCORR.LE. RIGHT) $ .AND.( LAMBDA + RQCORR.GE. LEFT) $ ) THEN USEDRQ = .TRUE. * Store new midpoint of bisection interval in WORK IF(SGNDEF.EQ.ONE) THEN * The current LAMBDA is on the left of the true * eigenvalue LEFT = LAMBDA * We prefer to assume that the error estimate * is correct. We could make the interval not * as a bracket but to be modified if the RQCORR * chooses to. In this case, the RIGHT side should * be modified as follows: * RIGHT = MAX(RIGHT, LAMBDA + RQCORR) ELSE * The current LAMBDA is on the right of the true * eigenvalue RIGHT = LAMBDA * See comment about assuming the error estimate is * correct above. * LEFT = MIN(LEFT, LAMBDA + RQCORR) ENDIF WORK( WINDEX ) = $ HALF * (RIGHT + LEFT) * Take RQCORR since it has the correct sign and * improves the iterate reasonably LAMBDA = LAMBDA + RQCORR * Update width of error interval WERR( WINDEX ) = $ HALF * (RIGHT-LEFT) ELSE NEEDBS = .TRUE. ENDIF IF(RIGHT-LEFT.LT.RQTOL*ABS(LAMBDA)) THEN * The eigenvalue is computed to bisection accuracy * compute eigenvector and stop USEDBS = .TRUE. GOTO 120 ELSEIF( ITER.LT.MAXITR ) THEN GOTO 120 ELSEIF( ITER.EQ.MAXITR ) THEN NEEDBS = .TRUE. GOTO 120 ELSE INFO = 5 RETURN END IF ELSE STP2II = .FALSE. IF(USEDRQ .AND. USEDBS .AND. $ BSTRES.LE.RESID) THEN LAMBDA = BSTW STP2II = .TRUE. ENDIF IF (STP2II) THEN * improve error angle by second step CALL SLAR1V( IN, 1, IN, LAMBDA, $ D( IBEGIN ), L( IBEGIN ), $ WORK(INDLD+IBEGIN-1), $ WORK(INDLLD+IBEGIN-1), $ PIVMIN, GAPTOL, Z( IBEGIN, WINDEX ), $ .NOT.USEDBS, NEGCNT, ZTZ, MINGMA, $ IWORK( IINDR+WINDEX ), $ ISUPPZ( 2*WINDEX-1 ), $ NRMINV, RESID, RQCORR, WORK( INDWRK ) ) ENDIF WORK( WINDEX ) = LAMBDA END IF * * Compute FP-vector support w.r.t. whole matrix * ISUPPZ( 2*WINDEX-1 ) = ISUPPZ( 2*WINDEX-1 )+OLDIEN ISUPPZ( 2*WINDEX ) = ISUPPZ( 2*WINDEX )+OLDIEN ZFROM = ISUPPZ( 2*WINDEX-1 ) ZTO = ISUPPZ( 2*WINDEX ) ISUPMN = ISUPMN + OLDIEN ISUPMX = ISUPMX + OLDIEN * Ensure vector is ok if support in the RQI has changed IF(ISUPMN.LT.ZFROM) THEN DO 122 II = ISUPMN,ZFROM-1 Z( II, WINDEX ) = ZERO 122 CONTINUE ENDIF IF(ISUPMX.GT.ZTO) THEN DO 123 II = ZTO+1,ISUPMX Z( II, WINDEX ) = ZERO 123 CONTINUE ENDIF CALL SSCAL( ZTO-ZFROM+1, NRMINV, $ Z( ZFROM, WINDEX ), 1 ) 125 CONTINUE * Update W W( WINDEX ) = LAMBDA+SIGMA * Recompute the gaps on the left and right * But only allow them to become larger and not * smaller (which can only happen through "bad" * cancellation and doesn't reflect the theory * where the initial gaps are underestimated due * to WERR being too crude.) IF(.NOT.ESKIP) THEN IF( K.GT.1) THEN WGAP( WINDMN ) = MAX( WGAP(WINDMN), $ W(WINDEX)-WERR(WINDEX) $ - W(WINDMN)-WERR(WINDMN) ) ENDIF IF( WINDEX.LT.WEND ) THEN WGAP( WINDEX ) = MAX( SAVGAP, $ W( WINDPL )-WERR( WINDPL ) $ - W( WINDEX )-WERR( WINDEX) ) ENDIF ENDIF IDONE = IDONE + 1 ENDIF * here ends the code for the current child * 139 CONTINUE * Proceed to any remaining child nodes NEWFST = J + 1 140 CONTINUE 150 CONTINUE NDEPTH = NDEPTH + 1 GO TO 40 END IF IBEGIN = IEND + 1 WBEGIN = WEND + 1 170 CONTINUE * RETURN * * End of SLARRV * END


In this lab module, you will complete the configuration of the dispenser firmware, download the compiled files to your laptop, and then use the tools to flash the microcontroller. At that point, the main components of the dispenser with the exception of the motor, will be fully operational.
By the end of the module you will have:
Follow each step in order and use the Click to open for detailed step-by-step instructions if required.
The X.509 client certificate and private key you downloaded earlier to your laptop’s cdd
directory uniquely identify your dispenser from all others. In order to communicate to AWS IoT core, the firmware must be configured with this information. To do so, you need to modify two of the source files in in device_firmware/demos/include
with the following:
| Firmware Source File | #define Statement in File |
Content |
|---|---|---|
aws_clientcredential.h |
clientcredentialMQTT_BROKER_ENDPOINT | AWS IoT Endpoint value from MY DETAILS section of dispenser app |
aws_clientcredential.h |
clientcredentialIOT_THING_NAME | Your assigned dispenser name (3-digit number) to use when connecting to the MQTT broker |
aws_clientcredential.h |
clientcredentialWIFI_SSID | WiFi network name provided by workshop presenter |
aws_clientcredential.h |
clientcredentialWIFI_PASSWORD | Provided password for the WiFi network |
aws_clientcredential_keys.h |
keyCLIENT_CERTIFICATE_PEM | Converted X.509 certificate (nnn-certificate.pem.crt ) content from Credential Formatter |
aws_clientcredential_keys.h |
keyCLIENT_PRIVATE_KEY_PEM | Converted certificate private key nnn-private.pem.key content from Credential Formatter |
In Cloud9, navigate to the device_firmware/demos/include
folder, then double-click on the two files above and modify the contents. To modify the X.509 certificate and private key, use the Credential Formatter and copy the converted PEM content into the file.
The content of the aws_clientcredential_keys.h
file should look similar to the following before and after copying the converted content of the two PEM files:
BEFORE:
#define keyCLIENT_CERTIFICATE_PEM "REPLACE_WITH_CONVERTED_CERTIFICATE_STRING"
AFTER:
#define keyCLIENT_CERTIFICATE_PEM "-----BEGIN CERTIFICATE-----\n"\
"MIICxjCCAa6gAwIBAgIVAJhkG3c6wT05SEZKJ3OsVHrQov6nMA0GCSqGSIb3DQEB\n"\
"IdbvOv7LLT9BD2Z8Mx9H/BhCd9ylpZEyQcl948GjEXgBDGdxUKFhrEfx\n"\
"-----END CERTIFICATE-----"
Ensure that you update both the Certificate and Private Key sections. Leave the rest as-is.
Once both files are modified, save them from the Cloud9 IDE. You can leave the tabs open to quickly go back to the files if needed.
After saving the updated files, click on the terminal window where you did the compile steps in the previous lab. Run the make
command again which will pick up the file changes and recompile the firmware.
cd ~/environment/connected-drink-dispenser-workshop/device_firmware/build
make all -j4
In the Cloud9 file browser navigate to the connected-drink-dispenser-workshop/device_firmware/build
folder and expand it. Scroll down and right-click on aws_demos.bin
and select Download and save to your cdd
directory. Do the same for the build/bootloader/bootloader.bin
and build/partition_table/partition_table.bin
files.
In your laptop’s cdd
directory you should now have these three files.
The final step in the modify->build->download->flash sequence is to flash the microcontroller. Connect the microcontroller to your laptop. Next, from the command prompt or terminal opened earlier, ensure you are in the cdd
directory and then use esptool to flash.
The command esptool ...
will be used. Use the syntax that works for your laptop installation (e.g., ./esptool.py
, esptool
, etc.).
Run the flashing program replacing the --port
with your value (default for macOS used below).
esptool.py --chip esp32 --port /dev/tty.SLAB_USBtoUART --baud 921600 --before default_reset --after hard_reset write_flash -z --flash_mode dio --flash_freq 40m --flash_size detect 0x1000 bootloader.bin 0x20000 aws_demos.bin 0x8000 partition-table.bin
You should see output similar indicated the firmware was flashed.
esptool.py v2.8
Serial port /dev/tty.SLAB_USBtoUART
Connecting........__
Chip is ESP32D0WDQ5 (revision 1)
Features: WiFi, BT, Dual Core, Coding Scheme None
Crystal is 40MHz
MAC: 24:0a:c4:23:d6:5c
Uploading stub...
Running stub...
Stub running...
Changing baud rate to 921600
Changed.
Configuring flash size...
Auto-detected Flash size: 4MB
Compressed 24272 bytes to 14397...
Wrote 24272 bytes (14397 compressed) at 0x00001000 in 0.2 seconds (effective 1140.8 kbit/s)...
Hash of data verified.
Compressed 860384 bytes to 529993...
Wrote 860384 bytes (529993 compressed) at 0x00020000 in 8.0 seconds (effective 859.5 kbit/s)...
Hash of data verified.
Compressed 3072 bytes to 118...
Wrote 3072 bytes (118 compressed) at 0x00008000 in 0.0 seconds (effective 3733.3 kbit/s)...
Hash of data verified.
Leaving...
Hard resetting via RTS pin...
At this point the microcontroller will reset and your code will be running on it! To verify that the process was performed correctly, start your serial monitoring program (PuTTY or screen). Reset the microcontroller via the button right to the Micro USB connector, and view the output. A properly configured microcontroller will have an I (nnn) WIFI: SYSTEM_EVENT_STA_CONNECTED message indicating it connected to the WiFi network, and then [ShadowTask] operations with SUCCESS, indicating that it is communicating with AWS IoT.
If you need to correct any errors in the firmware, ensure to exit your screen session (Ctrl-a
+Ctrl-\
) or close the console window in PuTTY before re-flashing it since the serial port can only be used by one process at the time.
Please ensure the following checkpoints are validated before moving on to the next module.
In this lab we went through all the normal steps of firmware development–albeit as all manual steps. The process is similar to normal software development where you write code, compile, debug, and then repeat. In the case of firmware development, especially when working with hardware peripherals, the added step is flashing the firmware to development board.
While Cloud9 is a fully integrated development environment, we only used it to edit and build the firmware, and have not taken full advantage of its capabilities.
While we used manual processes to illustrate the various steps, we would normally automate and use specific tools to make the development process more streamlined, consistent, and to reduce errors. All of the steps completed manually can be automated. In a more automated environment, the development process could operate in this manner:
.bin
files to an Amazon S3 bucket.By understanding what the development process looks like in this lab module, you can automate any series of steps slowly to add consistency and repeatability to your development processes.