| 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 | (939 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 | (13 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 | (25 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 | (31 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 | (516 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| 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 | (51 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (46 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 | (21 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 | (37 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 | (173 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
Global Index
A
absorp_Or2 [lemma, in GenHil.wBIH_meta_interactions]absorp_Or1 [lemma, in GenHil.wBIH_meta_interactions]
AccT [inductive, in General.genT]
AccT_sind [definition, in General.genT]
AccT_rec [definition, in General.genT]
AccT_ind [definition, in General.genT]
AccT_rect [definition, in General.genT]
AccT_intro [constructor, in General.genT]
add_remove_list_preserve_NoDup [lemma, in Synt.lems_remove_list]
aleq [definition, in Alg.Bi_Heyting_Algebras]
aleq_closed [projection, in Alg.wBIH_not_algebraizable]
aleq_antisym [lemma, in Alg.Bi_Heyting_Algebras]
aleq_refl [lemma, in Alg.Bi_Heyting_Algebras]
aleq_trans [lemma, in Alg.Bi_Heyting_Algebras]
algebraic_semantic [library]
algebraizable [section, in Alg.sBIH_algebraizable]
algebraizable.Hypirrel [variable, in Alg.sBIH_algebraizable]
algord_soundness_wBIH [lemma, in Alg.alg_soundness]
algtd_soundness_wBIH [lemma, in Alg.alg_soundness]
algtd_completeness_wBIH [lemma, in Alg.wBIH_alg_completeness]
alg_sem_properties [section, in Alg.algebraic_semantic]
alg_ordconseq [definition, in Alg.algebraic_semantic]
alg_tdconseq [definition, in Alg.algebraic_semantic]
alg_eqconseq [definition, in Alg.algebraic_semantic]
alg_eqconseq_eq [definition, in Alg.algebraic_semantic]
alg_semantics [section, in Alg.algebraic_semantic]
alg_completeness_sBIH [lemma, in Alg.sBIH_alg_completeness]
alg_soundness_wBIH_eq [lemma, in Alg.alg_soundness]
alg_soundness_sBIH [lemma, in Alg.alg_soundness]
alg_eq_iff_wBIH_eqprv [lemma, in Alg.wBIH_no_biHA_alg_sem]
alg_BA4 [lemma, in Alg.Bi_Heyting_Algebras]
alg_BA3 [lemma, in Alg.Bi_Heyting_Algebras]
alg_BA2 [lemma, in Alg.Bi_Heyting_Algebras]
alg_BA1 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A10 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A9 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A8 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A7 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A6 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A5 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A4 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A3 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A2 [lemma, in Alg.Bi_Heyting_Algebras]
alg_A1 [lemma, in Alg.Bi_Heyting_Algebras]
alg_soundness [library]
always_add_a_nat [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
And [constructor, in Synt.Syntax]
And_Imp [lemma, in GenHil.wBIH_meta_interactions]
and_true [lemma, in General.gen]
anon [definition, in General.genT]
anonD [lemma, in General.genT]
anonI [lemma, in General.genT]
anon_forall [lemma, in General.genT]
anon_sigT [lemma, in General.genT]
anon_iffT [lemma, in General.genT]
anon_imp [lemma, in General.genT]
anon_sum [lemma, in General.genT]
anon_prod [lemma, in General.genT]
anon_eq [lemma, in General.genT]
appl [lemma, in General.gen]
app_remove_list [lemma, in Synt.lems_remove_list]
arg_cong_imp' [lemma, in General.gen]
arg_cong_imp [lemma, in General.gen]
arg_cong [lemma, in General.gen]
arg1_cong_imp' [lemma, in General.gen]
arg1_cong_imp [lemma, in General.gen]
assoc_And_obj [lemma, in GenHil.wBIH_meta_interactions]
AThm_irrel [lemma, in GenHil.wBIH_meta_interactions]
Axioms [inductive, in GenHil.BiInt_GHC]
Axioms_one [lemma, in Alg.alg_soundness]
Axioms_sind [definition, in GenHil.BiInt_GHC]
Axioms_ind [definition, in GenHil.BiInt_GHC]
Ax_valid [lemma, in Krip.BiInt_soundness]
A1 [constructor, in GenHil.BiInt_GHC]
A10 [constructor, in GenHil.BiInt_GHC]
A2 [constructor, in GenHil.BiInt_GHC]
A3 [constructor, in GenHil.BiInt_GHC]
A4 [constructor, in GenHil.BiInt_GHC]
A5 [constructor, in GenHil.BiInt_GHC]
A6 [constructor, in GenHil.BiInt_GHC]
A7 [constructor, in GenHil.BiInt_GHC]
A8 [constructor, in GenHil.BiInt_GHC]
A9 [constructor, in GenHil.BiInt_GHC]
B
BA1 [constructor, in GenHil.BiInt_GHC]BA2 [constructor, in GenHil.BiInt_GHC]
BA3 [constructor, in GenHil.BiInt_GHC]
BA4 [constructor, in GenHil.BiInt_GHC]
biHalg [record, in Alg.Bi_Heyting_Algebras]
_ << _ [notation, in Alg.Bi_Heyting_Algebras]
biHalg_props.BH [variable, in Alg.Bi_Heyting_Algebras]
biHalg_props [section, in Alg.Bi_Heyting_Algebras]
BIH_export [library]
BiInt [section, in GenHil.sBIH_meta_interactions]
BiInt_soundness [library]
BiInt_sem_look_back [library]
BiInt_Kripke_sem [library]
BiInt_Lindenbaum_lem_prelim [library]
BiInt_enum [library]
BiInt_bisimulation [library]
BiInt_extens_interactions [library]
BiInt_logics [library]
BiInt_Lindenbaum_lem [library]
BiInt_GHC [library]
BiLEM [lemma, in GenHil.wBIH_meta_interactions]
bisimulation [definition, in Krip.BiInt_bisimulation]
Bisimulation [section, in Krip.BiInt_bisimulation]
bisimulation_imp_bi_int_equiv [lemma, in Krip.BiInt_bisimulation]
bi_LEM [lemma, in Alg.Bi_Heyting_Algebras]
Bi_Heyting_Algebras [library]
Bot [constructor, in Synt.Syntax]
C
Canon_val [definition, in Krip.wBIH_completeness]Canon_rel [definition, in Krip.wBIH_completeness]
Canon_worlds [record, in Krip.wBIH_completeness]
choice_code [definition, in GenHil.BiInt_Lindenbaum_lem]
choice_form [definition, in GenHil.BiInt_Lindenbaum_lem]
closed [definition, in GenHil.BiInt_Lindenbaum_lem]
Closed [projection, in Krip.wBIH_completeness]
closeder_fst_Lind_pair [lemma, in GenHil.BiInt_Lindenbaum_lem]
Closure_DN_strong [lemma, in GenHil.sBIH_meta_interactions]
clos_DN_eq [definition, in Alg.wBIH_equivalential]
CM [instance, in Krip.wBIH_completeness]
comm_Or [lemma, in GenHil.wBIH_meta_interactions]
comm_Or_obj [lemma, in GenHil.wBIH_meta_interactions]
comm_And_obj [lemma, in GenHil.wBIH_meta_interactions]
complete [definition, in GenHil.BiInt_GHC]
Completeness [section, in Alg.sBIH_alg_completeness]
Completeness [section, in Alg.wBIH_alg_completeness]
Completeness.Hypirrel [variable, in Alg.sBIH_alg_completeness]
Completeness.Hypirrel [variable, in Alg.wBIH_alg_completeness]
Completeness.Γ [variable, in Alg.sBIH_alg_completeness]
Compl_prime_theory_extens [lemma, in GenHil.BiInt_Lindenbaum_lem]
cong [projection, in Alg.wBIH_not_algebraizable]
congruence [record, in Alg.wBIH_not_algebraizable]
congruences [section, in Alg.wBIH_not_algebraizable]
cong_subtr [projection, in Alg.wBIH_not_algebraizable]
cong_rpc [projection, in Alg.wBIH_not_algebraizable]
cong_join [projection, in Alg.wBIH_not_algebraizable]
cong_meet [projection, in Alg.wBIH_not_algebraizable]
cong_trans [projection, in Alg.wBIH_not_algebraizable]
cong_sym [projection, in Alg.wBIH_not_algebraizable]
cong_refl [projection, in Alg.wBIH_not_algebraizable]
connect_to_s [section, in GenHil.wBIH_meta_interactions]
ConseqSoundness [section, in Krip.BiInt_sem_look_back]
ConseqSoundness.Counterexamples [section, in Krip.BiInt_sem_look_back]
ConseqSoundness.DefModels [section, in Krip.BiInt_sem_look_back]
Consequences_Soundness4 [lemma, in Krip.BiInt_sem_look_back]
Consequences_Soundness3 [lemma, in Krip.BiInt_sem_look_back]
Consequences_Soundness2 [lemma, in Krip.BiInt_sem_look_back]
Consequences_Soundness1 [lemma, in Krip.BiInt_sem_look_back]
Consist_prime_theory [lemma, in GenHil.BiInt_Lindenbaum_lem]
Consist_nprime_theory [lemma, in GenHil.BiInt_Lindenbaum_lem]
contains_one [projection, in Alg.wBIH_not_algebraizable]
Contrapositive [lemma, in GenHil.wBIH_meta_interactions]
Contr_Bot [lemma, in GenHil.wBIH_meta_interactions]
ctx_dual_residuation_obj [lemma, in GenHil.wBIH_meta_interactions]
Cut [lemma, in GenHil.wBIH_meta_interactions]
C_val_persist [lemma, in Krip.wBIH_completeness]
C_R_trans [lemma, in Krip.wBIH_completeness]
C_R_refl [lemma, in Krip.wBIH_completeness]
D
dec_zho_leq_qel [lemma, in Alg.wBIH_not_algebraizable]dec_zho_leq [lemma, in Alg.wBIH_not_algebraizable]
depth [definition, in Synt.Syntax]
depth_zero [lemma, in Synt.Syntax]
der_prime_theory_nprime_theory [lemma, in GenHil.BiInt_Lindenbaum_lem]
der_nprime_theory_mprime_theory_le [lemma, in GenHil.BiInt_Lindenbaum_lem]
der_list_conj_finite_context [lemma, in GenHil.wBIH_meta_interactions]
der_list_disj_bot [lemma, in GenHil.wBIH_meta_interactions]
der_list_disj_remove2 [lemma, in GenHil.wBIH_meta_interactions]
der_list_disj_remove1 [lemma, in GenHil.wBIH_meta_interactions]
der_mult_disj_Bot [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
Deux [constructor, in Krip.BiInt_sem_look_back]
distr_join_meet [lemma, in Alg.Bi_Heyting_Algebras]
distr_meet_join [lemma, in Alg.Bi_Heyting_Algebras]
DN_clos_DN_form [lemma, in Krip.sBIH_completeness]
DN_form_DN [lemma, in Krip.sBIH_completeness]
DN_form_interp [lemma, in Alg.algebraic_semantic]
DN_form_rule [lemma, in GenHil.wBIH_meta_interactions]
DN_form_dist_imp [lemma, in GenHil.wBIH_meta_interactions]
DN_dist_imp [lemma, in GenHil.wBIH_meta_interactions]
DN_to_form [lemma, in GenHil.wBIH_meta_interactions]
DN_form_n_reachable [lemma, in Alg.wBIH_equivalential]
DN_form_S [lemma, in Synt.Syntax]
DN_clos_set_sind [definition, in Synt.Syntax]
DN_clos_set_ind [definition, in Synt.Syntax]
DN_clos_set [inductive, in Synt.Syntax]
DN_form [definition, in Synt.Syntax]
DN_alg [definition, in Alg.Bi_Heyting_Algebras]
double_remove [lemma, in Synt.lems_remove_list]
double_coneg [lemma, in Alg.Bi_Heyting_Algebras]
double_neg [lemma, in Alg.Bi_Heyting_Algebras]
dresiduation [projection, in Alg.Bi_Heyting_Algebras]
dual_MP [lemma, in GenHil.wBIH_meta_interactions]
dual_residuation_gen [lemma, in GenHil.wBIH_meta_interactions]
dual_residuation [lemma, in GenHil.wBIH_meta_interactions]
dual_residuation_obj [lemma, in GenHil.wBIH_meta_interactions]
d_to_l_filter [lemma, in Alg.wBIH_not_algebraizable]
d_filter [projection, in Alg.wBIH_not_algebraizable]
E
EFQ [lemma, in GenHil.wBIH_meta_interactions]epdresiduation [lemma, in Alg.sBIH_alg_completeness]
epdresiduation [lemma, in Alg.wBIH_alg_completeness]
epform_eqprv [instance, in Alg.sBIH_alg_completeness]
epform_eqprv [instance, in Alg.wBIH_alg_completeness]
epgreatest [lemma, in Alg.sBIH_alg_completeness]
epgreatest [lemma, in Alg.wBIH_alg_completeness]
epjabsorp [lemma, in Alg.sBIH_alg_completeness]
epjabsorp [lemma, in Alg.wBIH_alg_completeness]
epjassoc [lemma, in Alg.sBIH_alg_completeness]
epjassoc [lemma, in Alg.wBIH_alg_completeness]
epjcomm [lemma, in Alg.sBIH_alg_completeness]
epjcomm [lemma, in Alg.wBIH_alg_completeness]
epjoin [instance, in Alg.sBIH_alg_completeness]
epjoin [instance, in Alg.wBIH_alg_completeness]
eplowest [lemma, in Alg.sBIH_alg_completeness]
eplowest [lemma, in Alg.wBIH_alg_completeness]
epmabsorp [lemma, in Alg.sBIH_alg_completeness]
epmabsorp [lemma, in Alg.wBIH_alg_completeness]
epmassoc [lemma, in Alg.sBIH_alg_completeness]
epmassoc [lemma, in Alg.wBIH_alg_completeness]
epmcomm [lemma, in Alg.sBIH_alg_completeness]
epmcomm [lemma, in Alg.wBIH_alg_completeness]
epmeet [instance, in Alg.sBIH_alg_completeness]
epmeet [instance, in Alg.wBIH_alg_completeness]
epone [instance, in Alg.sBIH_alg_completeness]
epone [instance, in Alg.wBIH_alg_completeness]
epresiduation [lemma, in Alg.sBIH_alg_completeness]
epresiduation [lemma, in Alg.wBIH_alg_completeness]
eprpc [instance, in Alg.sBIH_alg_completeness]
eprpc [instance, in Alg.wBIH_alg_completeness]
eprvform_eqprv [lemma, in Alg.sBIH_alg_completeness]
eprvform_eqprv [lemma, in Alg.wBIH_alg_completeness]
eprvjoin [lemma, in Alg.sBIH_alg_completeness]
eprvjoin [lemma, in Alg.wBIH_alg_completeness]
eprvmeet [lemma, in Alg.sBIH_alg_completeness]
eprvmeet [lemma, in Alg.wBIH_alg_completeness]
eprvone [lemma, in Alg.sBIH_alg_completeness]
eprvone [lemma, in Alg.wBIH_alg_completeness]
eprvrpc [lemma, in Alg.sBIH_alg_completeness]
eprvrpc [lemma, in Alg.wBIH_alg_completeness]
eprvsubtr [lemma, in Alg.sBIH_alg_completeness]
eprvsubtr [lemma, in Alg.wBIH_alg_completeness]
eprvzero [lemma, in Alg.sBIH_alg_completeness]
eprvzero [lemma, in Alg.wBIH_alg_completeness]
epsubtr [instance, in Alg.sBIH_alg_completeness]
epsubtr [instance, in Alg.wBIH_alg_completeness]
epzero [instance, in Alg.sBIH_alg_completeness]
epzero [instance, in Alg.wBIH_alg_completeness]
EqImp [definition, in Alg.sBIH_implicative]
eqprv [record, in Alg.sBIH_alg_completeness]
eqprv [record, in Alg.wBIH_alg_completeness]
equiprov [projection, in Alg.sBIH_alg_completeness]
equiprov [projection, in Alg.wBIH_alg_completeness]
Equiprovable_classes.Γ [variable, in Alg.sBIH_alg_completeness]
Equiprovable_classes [section, in Alg.sBIH_alg_completeness]
Equiprovable_classes [section, in Alg.wBIH_alg_completeness]
equivalential [section, in Alg.wBIH_equivalential]
equivalential.LEM [variable, in Alg.wBIH_equivalential]
eq_S_F [lemma, in General.genT]
eq_dec_form [lemma, in Synt.Syntax]
eq_TrueI [lemma, in General.gen]
Eq_elem_invalid [lemma, in Alg.wBIH_no_biHA_alg_sem]
eq_repres_aleq [lemma, in Alg.Bi_Heyting_Algebras]
Even [definition, in Alg.wBIH_equivalential]
Even_Odd_dec [lemma, in Alg.wBIH_equivalential]
Excl [constructor, in Synt.Syntax]
existsT [library]
extens_diff_sBIH [lemma, in GenHil.BiInt_extens_interactions]
F
failure_gen_sBIH_Dual_Detachment_Theorem [lemma, in Krip.BiInt_sem_look_back]failure_gen_sBIH_Deduction_Theorem [lemma, in Krip.BiInt_sem_look_back]
failure_Xmas_lights [lemma, in Alg.wBIH_equivalential]
false_or [lemma, in General.gen]
filters [section, in Alg.wBIH_not_algebraizable]
finclos_DN_eq [definition, in Alg.wBIH_equivalential]
finite_context_list_conj [lemma, in GenHil.wBIH_meta_interactions]
first_zho_lattice_filters [definition, in Alg.wBIH_not_algebraizable]
first_subst_interp [lemma, in Alg.algebraic_semantic]
first_subst_idem [lemma, in Synt.Syntax]
first_subst [definition, in Synt.Syntax]
ForallT [inductive, in General.genT]
ForallTD_forall [definition, in General.genT]
ForallTI_forall [definition, in General.genT]
ForallT_Forall [lemma, in General.genT]
ForallT_Forall' [lemma, in General.genT]
ForallT_forall [lemma, in General.genT]
ForallT_impl [lemma, in General.genT]
ForallT_2I [definition, in General.genT]
ForallT_2I' [definition, in General.genT]
ForallT_D2 [definition, in General.genT]
ForallT_D1 [definition, in General.genT]
ForallT_2D [definition, in General.genT]
ForallT_map_rev [lemma, in General.genT]
ForallT_map [lemma, in General.genT]
ForallT_map_2 [lemma, in General.genT]
ForallT_2 [lemma, in General.genT]
ForallT_appendI [definition, in General.genT]
ForallT_appendI' [definition, in General.genT]
ForallT_appendD2 [definition, in General.genT]
ForallT_appendD1 [definition, in General.genT]
ForallT_appendD [definition, in General.genT]
ForallT_append [lemma, in General.genT]
ForallT_cons_iff [lemma, in General.genT]
ForallT_singleI [definition, in General.genT]
ForallT_singleD [definition, in General.genT]
ForallT_single [lemma, in General.genT]
ForallT_cons_inv [lemma, in General.genT]
ForallT_inv [lemma, in General.genT]
ForallT_sind [definition, in General.genT]
ForallT_rec [definition, in General.genT]
ForallT_ind [definition, in General.genT]
ForallT_rect [definition, in General.genT]
ForallT_cons [constructor, in General.genT]
ForallT_nil [constructor, in General.genT]
Forall_ForallT' [lemma, in General.genT]
Forall_ForallT [lemma, in General.genT]
forall_list_disj [lemma, in GenHil.wBIH_meta_interactions]
Forall_map_2 [lemma, in General.gen]
Forall_map_single [lemma, in General.gen]
Forall_single [lemma, in General.gen]
Forall_append [lemma, in General.gen]
Forall_cons_iff [lemma, in General.gen]
Forall_cons_inv [lemma, in General.gen]
Forall2T [inductive, in General.genT]
Forall2T_ex_r [lemma, in General.genT]
Forall2T_ex_l [lemma, in General.genT]
Forall2T_app [lemma, in General.genT]
Forall2T_app_inv_r [lemma, in General.genT]
Forall2T_app_inv_l [lemma, in General.genT]
Forall2T_sind [definition, in General.genT]
Forall2T_rec [definition, in General.genT]
Forall2T_ind [definition, in General.genT]
Forall2T_rect [definition, in General.genT]
Forall2T_cons [constructor, in General.genT]
Forall2T_nil [constructor, in General.genT]
form [inductive, in Synt.Syntax]
form_index_inj [lemma, in GenHil.BiInt_enum]
form_enum_index [lemma, in GenHil.BiInt_enum]
form_index [definition, in GenHil.BiInt_enum]
form_index' [definition, in GenHil.BiInt_enum]
form_enum_sur [lemma, in GenHil.BiInt_enum]
form_enum [definition, in GenHil.BiInt_enum]
form_sind [definition, in Synt.Syntax]
form_rec [definition, in Synt.Syntax]
form_ind [definition, in Synt.Syntax]
form_rect [definition, in Synt.Syntax]
Fq [constructor, in Krip.BiInt_sem_look_back]
fun_cong [lemma, in General.gen]
G
gen [library]genT [library]
gen_wBIH_Dual_Deduction_Theorem [lemma, in GenHil.wBIH_meta_interactions]
gen_wBIH_Dual_Detachment_Theorem [lemma, in GenHil.wBIH_meta_interactions]
gen_wBIH_Deduction_Theorem [lemma, in GenHil.wBIH_meta_interactions]
gen_wBIH_Detachment_Theorem [lemma, in GenHil.wBIH_meta_interactions]
gen_sBIH_Double_Negated_Detachment_Theorem [lemma, in GenHil.sBIH_meta_interactions]
gen_sBIH_Deduction_Theorem [lemma, in GenHil.sBIH_meta_interactions]
gen_sBIH_Detachment_Theorem [lemma, in GenHil.sBIH_meta_interactions]
gen_cong [lemma, in General.gen]
glb [lemma, in Alg.Bi_Heyting_Algebras]
glob_conseq [definition, in Krip.BiInt_Kripke_sem]
greatest [projection, in Alg.Bi_Heyting_Algebras]
H
Half [constructor, in Alg.wBIH_not_algebraizable]head_n_zz [lemma, in Alg.wBIH_equivalential]
head_n_reachable [lemma, in Alg.wBIH_equivalential]
higher [definition, in Alg.wBIH_not_algebraizable]
high_one [lemma, in Alg.Bi_Heyting_Algebras]
I
Id_list_disj_remove [lemma, in GenHil.wBIH_meta_interactions]Id_list_disj [lemma, in GenHil.wBIH_meta_interactions]
iffD1 [lemma, in General.gen]
iffD2 [lemma, in General.gen]
iffT_prod [lemma, in General.genT]
iffT_D2 [definition, in General.genT]
iffT_D1 [definition, in General.genT]
iffT_sym [definition, in General.genT]
iffT_D2' [lemma, in General.genT]
iffT_D1' [lemma, in General.genT]
iffT_refl [lemma, in General.genT]
iffT_sym' [lemma, in General.genT]
iffT_trans [lemma, in General.genT]
Imp [constructor, in Synt.Syntax]
implicative [section, in Alg.sBIH_implicative]
Imp_And [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help427 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help410 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help170 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help54 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help37 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help35 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help14 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help9 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help8 [lemma, in GenHil.wBIH_meta_interactions]
Imp_trans_help7 [lemma, in GenHil.wBIH_meta_interactions]
imp_Id_gen [lemma, in GenHil.wBIH_meta_interactions]
IndClo [constructor, in Synt.Syntax]
inhabited_anon [lemma, in General.genT]
inhab_eqprv [lemma, in Alg.sBIH_alg_completeness]
inhab_eqprv [lemma, in Alg.wBIH_alg_completeness]
InitClo [constructor, in Synt.Syntax]
InT [inductive, in General.genT]
interp [definition, in Alg.algebraic_semantic]
InT_In_eq' [lemma, in General.genT]
InT_In_eq [lemma, in General.genT]
InT_In' [lemma, in General.genT]
InT_In [lemma, in General.genT]
InT_concat [lemma, in General.genT]
InT_mapI [definition, in General.genT]
InT_map_iffT [lemma, in General.genT]
InT_mapE [lemma, in General.genT]
InT_map [lemma, in General.genT]
InT_inv [lemma, in General.genT]
InT_split [lemma, in General.genT]
InT_nilE [lemma, in General.genT]
InT_nilE' [lemma, in General.genT]
InT_appE [lemma, in General.genT]
InT_appE' [lemma, in General.genT]
InT_appR [lemma, in General.genT]
InT_appL [lemma, in General.genT]
InT_2nd [definition, in General.genT]
InT_eq [lemma, in General.genT]
InT_sind [definition, in General.genT]
InT_rec [definition, in General.genT]
InT_ind [definition, in General.genT]
InT_rect [definition, in General.genT]
InT_cons [constructor, in General.genT]
InT_eq' [constructor, in General.genT]
InT_remove [lemma, in GenHil.wBIH_meta_interactions]
In_InT [lemma, in General.genT]
in_sfform_eqprv [lemma, in Alg.sBIH_alg_completeness]
In_remove [lemma, in GenHil.wBIH_meta_interactions]
in_sfform_eqprv [lemma, in Alg.wBIH_alg_completeness]
In_matters_remove_list [lemma, in Synt.lems_remove_list]
In_remove_list_remove_redund [lemma, in Synt.lems_remove_list]
In_remove_list_In_list_not_In_remove_list [lemma, in Synt.lems_remove_list]
In_remove_list_In_list [lemma, in Synt.lems_remove_list]
In_remove_In_list [lemma, in Synt.lems_remove_list]
In_remove_length_same [lemma, in Synt.lems_remove_list]
In_remove_same [lemma, in Synt.lems_remove_list]
In_remove_diff [lemma, in Synt.lems_remove_list]
in_remove_in_init [lemma, in Synt.lems_remove_list]
in_not_touched_remove [lemma, in Synt.lems_remove_list]
In_dec [lemma, in Synt.lems_remove_list]
In_form_dec [lemma, in Synt.Syntax]
in_single [lemma, in General.gen]
J
jabsorp [projection, in Alg.Bi_Heyting_Algebras]jassoc [projection, in Alg.Bi_Heyting_Algebras]
jcomm [projection, in Alg.Bi_Heyting_Algebras]
join [projection, in Alg.Bi_Heyting_Algebras]
join_deep [lemma, in Alg.Bi_Heyting_Algebras]
join_inj2 [lemma, in Alg.Bi_Heyting_Algebras]
join_inj1 [lemma, in Alg.Bi_Heyting_Algebras]
join_id [lemma, in Alg.Bi_Heyting_Algebras]
K
keep_list_delete_head_not_In [lemma, in Synt.lems_remove_list]keep_list_delete_head_not_origin [lemma, in Synt.lems_remove_list]
Kripke_semantics [section, in Krip.BiInt_Kripke_sem]
Kripke_export [library]
L
lattice_filter [record, in Alg.wBIH_not_algebraizable]LEM [axiom, in Krip.sBIH_completeness]
LEM [axiom, in Alg.sBIH_alg_completeness]
LEM [axiom, in Alg.wBIH_alg_completeness]
lems_remove_list [library]
LEM_sSoundness [lemma, in Krip.BiInt_soundness]
LEM_wSoundness [lemma, in Krip.BiInt_soundness]
LEM_world [lemma, in Krip.wBIH_completeness]
LEM_Lindenbaum [lemma, in Krip.wBIH_completeness]
LEM_prime [lemma, in Krip.wBIH_completeness]
LEM_completeness.LEM [variable, in Krip.wBIH_completeness]
LEM_completeness [section, in Krip.wBIH_completeness]
length_le_remove_list [lemma, in Synt.lems_remove_list]
len_nodes [definition, in Alg.wBIH_no_biHA_alg_sem]
leT [inductive, in General.genT]
leT_ex_plus [lemma, in General.genT]
leT_or_gt [lemma, in General.genT]
leT_S_or_eq [lemma, in General.genT]
leT_S_F [lemma, in General.genT]
leT_plus_l [lemma, in General.genT]
leT_plus_r [lemma, in General.genT]
leT_0_n [lemma, in General.genT]
leT_trans [definition, in General.genT]
leT_trans' [lemma, in General.genT]
leT_S_n [definition, in General.genT]
leT_S_n' [lemma, in General.genT]
leT_n_S [lemma, in General.genT]
leT_sind [definition, in General.genT]
leT_rec [definition, in General.genT]
leT_ind [definition, in General.genT]
leT_rect [definition, in General.genT]
leT_S [constructor, in General.genT]
leT_n [constructor, in General.genT]
LindAlg [instance, in Alg.sBIH_alg_completeness]
LindAlg [instance, in Alg.wBIH_alg_completeness]
LindAlgamap [definition, in Alg.sBIH_alg_completeness]
LindAlgamap [definition, in Alg.wBIH_alg_completeness]
LindAlgrepres [lemma, in Alg.sBIH_alg_completeness]
LindAlgrepres [lemma, in Alg.wBIH_alg_completeness]
Lindenbaum [lemma, in GenHil.BiInt_Lindenbaum_lem]
Lindenbaum_algebra.Hypirrel [variable, in Alg.sBIH_alg_completeness]
Lindenbaum_algebra.Γ [variable, in Alg.sBIH_alg_completeness]
Lindenbaum_algebra [section, in Alg.sBIH_alg_completeness]
Lindenbaum_algebra.Hypirrel [variable, in Alg.wBIH_alg_completeness]
Lindenbaum_algebra [section, in Alg.wBIH_alg_completeness]
list_disj_witn [lemma, in Krip.BiInt_soundness]
list_disj_prime [lemma, in GenHil.BiInt_Lindenbaum_lem]
list_conj_interp [lemma, in Alg.algebraic_semantic]
list_conj_finite_context [lemma, in GenHil.wBIH_meta_interactions]
list_conj_in_list [lemma, in GenHil.wBIH_meta_interactions]
list_disj_nodup [lemma, in GenHil.wBIH_meta_interactions]
list_disj_In_prv [lemma, in GenHil.wBIH_meta_interactions]
list_disj_app_distr [lemma, in GenHil.wBIH_meta_interactions]
list_disj_In [lemma, in GenHil.wBIH_meta_interactions]
list_disj_In0 [lemma, in GenHil.wBIH_meta_interactions]
list_disj_remove_form [lemma, in GenHil.wBIH_meta_interactions]
list_disj_remove_app [lemma, in GenHil.wBIH_meta_interactions]
list_disj_app0 [lemma, in GenHil.wBIH_meta_interactions]
list_disj_app [lemma, in GenHil.wBIH_meta_interactions]
list_all_pred_nat [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
list_conj [definition, in Synt.Syntax]
list_disj [definition, in Synt.Syntax]
list_meet_all [lemma, in Alg.Bi_Heyting_Algebras]
list_meet [definition, in Alg.Bi_Heyting_Algebras]
lnc [definition, in Alg.wBIH_no_biHA_alg_sem]
loc_conseq [definition, in Krip.BiInt_Kripke_sem]
lower [definition, in Alg.wBIH_not_algebraizable]
lowest [projection, in Alg.Bi_Heyting_Algebras]
low_zero [lemma, in Alg.Bi_Heyting_Algebras]
lub [lemma, in Alg.Bi_Heyting_Algebras]
L_enum_exhaustive [lemma, in GenHil.BiInt_enum]
L_enum_cumulative [lemma, in GenHil.BiInt_enum]
L_enum [definition, in GenHil.BiInt_enum]
l_to_d_filter [lemma, in Alg.wBIH_not_algebraizable]
l_filter [projection, in Alg.wBIH_not_algebraizable]
M
mabsorp [projection, in Alg.Bi_Heyting_Algebras]map_eq_nil [lemma, in General.gen]
map_app_ex [lemma, in General.gen]
map_cons_ex' [lemma, in General.gen]
map_cons_ex [lemma, in General.gen]
massoc [projection, in Alg.Bi_Heyting_Algebras]
max_of_list [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
mcomm [projection, in Alg.Bi_Heyting_Algebras]
meet [projection, in Alg.Bi_Heyting_Algebras]
meet_closed [projection, in Alg.wBIH_not_algebraizable]
meet_deep [lemma, in Alg.Bi_Heyting_Algebras]
meet_elim2 [lemma, in Alg.Bi_Heyting_Algebras]
meet_elim1 [lemma, in Alg.Bi_Heyting_Algebras]
meet_absorp3 [lemma, in Alg.Bi_Heyting_Algebras]
meet_absorp2 [lemma, in Alg.Bi_Heyting_Algebras]
meet_absorp1 [lemma, in Alg.Bi_Heyting_Algebras]
meet_absorp0 [lemma, in Alg.Bi_Heyting_Algebras]
meet_id [lemma, in Alg.Bi_Heyting_Algebras]
meta_Imp_trans [lemma, in GenHil.wBIH_meta_interactions]
meta_sImp_trans [lemma, in GenHil.sBIH_meta_interactions]
mforces [definition, in Krip.BiInt_Kripke_sem]
model [record, in Krip.BiInt_Kripke_sem]
model_construction.w [variable, in Alg.wBIH_no_biHA_alg_sem]
model_construction.M [variable, in Alg.wBIH_no_biHA_alg_sem]
model_construction [section, in Alg.wBIH_no_biHA_alg_sem]
monoL_Excl [lemma, in GenHil.wBIH_meta_interactions]
monoR_Excl [lemma, in GenHil.wBIH_meta_interactions]
monotL_Or [lemma, in GenHil.wBIH_meta_interactions]
monotR_Or [lemma, in GenHil.wBIH_meta_interactions]
monot_Or2 [lemma, in GenHil.wBIH_meta_interactions]
monot_Or2 [lemma, in GenHil.sBIH_meta_interactions]
mp [lemma, in Alg.Bi_Heyting_Algebras]
mult_disj_dec [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
mult_disj_dec1 [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
mult_disj_dec0 [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
mult_disj_Id [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
mult_disj [definition, in GenHil.BiInt_Lindenbaum_lem_prelim]
M0 [instance, in Krip.BiInt_sem_look_back]
M1 [instance, in Krip.BiInt_sem_look_back]
M2 [instance, in Krip.BiInt_sem_look_back]
N
nat_remove_In_smaller_length [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]nat_remove_le_length [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
nodes [projection, in Krip.BiInt_Kripke_sem]
nodes [projection, in Alg.Bi_Heyting_Algebras]
NoDup_remove [lemma, in GenHil.wBIH_meta_interactions]
NoDup_destr_split [lemma, in Synt.lems_remove_list]
NotDer [projection, in Krip.wBIH_completeness]
not_In_prime_theory_deriv [lemma, in GenHil.BiInt_Lindenbaum_lem]
not_removed_remove_list [lemma, in Synt.lems_remove_list]
not_finitely_equivalential.n [variable, in Alg.wBIH_equivalential]
not_finitely_equivalential [section, in Alg.wBIH_equivalential]
no_isomorphism.LEM [variable, in Alg.wBIH_not_algebraizable]
no_isomorphism [section, in Alg.wBIH_not_algebraizable]
no_list_all_nat [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
No_wBIH_alg_sem [lemma, in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics.wBIH_alg_sem [variable, in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics.Eq [variable, in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics.LEM [variable, in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics.Hypirrel [variable, in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics [section, in Alg.wBIH_no_biHA_alg_sem]
nprime_theory_extens_le [lemma, in GenHil.BiInt_Lindenbaum_lem]
nprime_theory_extens [lemma, in GenHil.BiInt_Lindenbaum_lem]
nprime_theory [definition, in GenHil.BiInt_Lindenbaum_lem]
n_reachable_DN_clos [lemma, in Krip.sBIH_completeness]
n_reachable_zz [lemma, in Krip.sBIH_completeness]
n_reachable_head [lemma, in Krip.sBIH_completeness]
n_reachable_tail [lemma, in Krip.sBIH_completeness]
n_zz_reachable_subset [lemma, in Krip.sBIH_completeness]
n_zz [definition, in Krip.sBIH_completeness]
n_reachable [definition, in Krip.sBIH_completeness]
n_bisimulation_imp_n_depth_equiv [lemma, in Krip.BiInt_bisimulation]
n_bisimulation_cum [lemma, in Krip.BiInt_bisimulation]
n_bisimulation_S [lemma, in Krip.BiInt_bisimulation]
n_bisimulation [definition, in Krip.BiInt_bisimulation]
n_Bisimulation [section, in Krip.BiInt_bisimulation]
n_reachable_finclos_DN_24 [lemma, in Alg.wBIH_equivalential]
n_reachable_finclos_DN_13 [lemma, in Alg.wBIH_equivalential]
n_reachable_Xmas_Id [lemma, in Alg.wBIH_equivalential]
n_reachable_False [lemma, in Alg.wBIH_equivalential]
n_zz_DN_clos_equiv [lemma, in Alg.wBIH_equivalential]
n_reachable_DN_clos_equiv [lemma, in Alg.wBIH_equivalential]
n_reachable_DN_clos [lemma, in Alg.wBIH_equivalential]
n_reachable_sym [lemma, in Alg.wBIH_no_biHA_alg_sem]
n_reachable_head [lemma, in Alg.wBIH_no_biHA_alg_sem]
n_reachable_Xmas [lemma, in Alg.wBIH_no_biHA_alg_sem]
O
Odd [definition, in Alg.wBIH_equivalential]One [constructor, in Alg.wBIH_not_algebraizable]
one [projection, in Alg.Bi_Heyting_Algebras]
One_high [constructor, in Alg.wBIH_not_algebraizable]
only_two_zho_congruences [lemma, in Alg.wBIH_not_algebraizable]
Or [constructor, in Synt.Syntax]
ord_dresid [lemma, in Alg.Bi_Heyting_Algebras]
ord_resid [lemma, in Alg.Bi_Heyting_Algebras]
Or_Neg [lemma, in GenHil.wBIH_meta_interactions]
Or_imp_assoc [lemma, in GenHil.wBIH_meta_interactions]
or_false [lemma, in General.gen]
P
pair_sBIH_extens_wBIH [lemma, in GenHil.BiInt_extens_interactions]pair_eqI [lemma, in General.gen]
permut_remove_remove_list [lemma, in Synt.lems_remove_list]
permut_remove [lemma, in Synt.lems_remove_list]
persist [projection, in Krip.BiInt_Kripke_sem]
Persistence [lemma, in Krip.BiInt_Kripke_sem]
persist_val3 [lemma, in Krip.BiInt_sem_look_back]
persist_val2 [lemma, in Krip.BiInt_sem_look_back]
persist_val1 [lemma, in Krip.BiInt_sem_look_back]
PiffD1 [lemma, in General.gen]
PiffD2 [lemma, in General.gen]
prim [projection, in Krip.wBIH_completeness]
prime [definition, in GenHil.BiInt_Lindenbaum_lem]
Prime [projection, in Krip.wBIH_completeness]
prime_theory_extens [lemma, in GenHil.BiInt_Lindenbaum_lem]
prime_theory [definition, in GenHil.BiInt_Lindenbaum_lem]
prod_nat_split [lemma, in General.genT]
prod_mono [lemma, in General.genT]
properties [section, in GenHil.wBIH_meta_interactions]
Properties_eqprv.eqprv_prf_irrel [variable, in Alg.sBIH_alg_completeness]
Properties_eqprv.Γ [variable, in Alg.sBIH_alg_completeness]
Properties_eqprv [section, in Alg.sBIH_alg_completeness]
Properties_eqprv.eqprv_prf_irrel [variable, in Alg.wBIH_alg_completeness]
Properties_eqprv [section, in Alg.wBIH_alg_completeness]
properties.Bi_Int [section, in GenHil.wBIH_meta_interactions]
properties.list_conj_stuff [section, in GenHil.wBIH_meta_interactions]
properties.list_disj_stuff [section, in GenHil.wBIH_meta_interactions]
properties.remove_stuff [section, in GenHil.wBIH_meta_interactions]
pruned_wforces [lemma, in Krip.sBIH_completeness]
pruned_bisim [lemma, in Krip.sBIH_completeness]
pruned_M [instance, in Krip.sBIH_completeness]
pruning [section, in Krip.sBIH_completeness]
pruning.M [variable, in Krip.sBIH_completeness]
pruning.s [variable, in Krip.sBIH_completeness]
prv_Top [lemma, in GenHil.wBIH_meta_interactions]
Q
quasi_prime_Lind_pair [lemma, in GenHil.BiInt_Lindenbaum_lem]quasi_prime [definition, in GenHil.BiInt_Lindenbaum_lem]
R
rappl [lemma, in General.gen]reachable [projection, in Krip.BiInt_Kripke_sem]
reach_tran [projection, in Krip.BiInt_Kripke_sem]
reach_refl [projection, in Krip.BiInt_Kripke_sem]
redund_remove_list [lemma, in Synt.lems_remove_list]
redund_remove [lemma, in Synt.lems_remove_list]
redund_remove_remove_list [lemma, in Synt.lems_remove_list]
relationT [definition, in General.genT]
remove_disj [lemma, in GenHil.wBIH_meta_interactions]
remove_list_incr_decr [lemma, in Synt.lems_remove_list]
remove_list_incr_decr4 [lemma, in Synt.lems_remove_list]
remove_list_incr_decr2 [lemma, in Synt.lems_remove_list]
remove_list_incr_decr1 [lemma, in Synt.lems_remove_list]
remove_list_incr_decr3 [lemma, in Synt.lems_remove_list]
remove_delete_origin [lemma, in Synt.lems_remove_list]
remove_list_is_nil [lemma, in Synt.lems_remove_list]
remove_list_in_nil [lemma, in Synt.lems_remove_list]
remove_list_delete_head_In [lemma, in Synt.lems_remove_list]
remove_list_delete_head [lemma, in Synt.lems_remove_list]
remove_list_non_empty_inter_smaller_length [lemma, in Synt.lems_remove_list]
remove_list_singl_id_or_nil [lemma, in Synt.lems_remove_list]
remove_list_is_in [lemma, in Synt.lems_remove_list]
remove_list_in_single [lemma, in Synt.lems_remove_list]
remove_list_dist_app [lemma, in Synt.lems_remove_list]
remove_list_cont [lemma, in Synt.lems_remove_list]
remove_list_preserv_NoDup [lemma, in Synt.lems_remove_list]
remove_list_of_nil [lemma, in Synt.lems_remove_list]
remove_list [definition, in Synt.lems_remove_list]
remove_In_smaller_length [lemma, in Synt.lems_remove_list]
remove_le_length [lemma, in Synt.lems_remove_list]
remove_preserv_NoDup [lemma, in Synt.lems_remove_list]
remove_not_in_anymore [lemma, in Synt.lems_remove_list]
remove_dist_app [lemma, in Synt.lems_remove_list]
req [definition, in General.gen]
req_trans [lemma, in General.gen]
req_sym [lemma, in General.gen]
req_refl [lemma, in General.gen]
residuation [projection, in Alg.Bi_Heyting_Algebras]
right_stable_Lind_pair [lemma, in GenHil.BiInt_Lindenbaum_lem]
rls [definition, in General.gen]
rlsT [definition, in General.genT]
Rooted_models_validity [lemma, in Krip.BiInt_sem_look_back]
rpc [projection, in Alg.Bi_Heyting_Algebras]
rsub [definition, in General.gen]
rsubD [definition, in General.gen]
rsubI [definition, in General.gen]
rsub_imp [definition, in General.gen]
rsub_id [lemma, in General.gen]
rsub_trans [lemma, in General.gen]
rsub_def [lemma, in General.gen]
S
sabsorp_Or1 [lemma, in GenHil.sBIH_meta_interactions]sAnd_Imp [lemma, in GenHil.sBIH_meta_interactions]
sassoc_And_obj [lemma, in GenHil.sBIH_meta_interactions]
sAx [constructor, in GenHil.BiInt_GHC]
sBIH_finite [lemma, in GenHil.BiInt_logics]
sBIH_struct [lemma, in GenHil.BiInt_logics]
sBIH_comp [lemma, in GenHil.BiInt_logics]
sBIH_monot [lemma, in GenHil.BiInt_logics]
sBIH_not_incl_wBIH [lemma, in Krip.BiInt_sem_look_back]
sBIH_IL3_Excl [lemma, in Alg.sBIH_implicative]
sBIH_IL3_Imp [lemma, in Alg.sBIH_implicative]
sBIH_IL3_Or [lemma, in Alg.sBIH_implicative]
sBIH_IL3_And [lemma, in Alg.sBIH_implicative]
sBIH_IL3_Bot [lemma, in Alg.sBIH_implicative]
sBIH_IL3_Top [lemma, in Alg.sBIH_implicative]
sBIH_IL5 [lemma, in Alg.sBIH_implicative]
sBIH_IL4 [lemma, in Alg.sBIH_implicative]
sBIH_IL2 [lemma, in Alg.sBIH_implicative]
sBIH_IL1 [lemma, in Alg.sBIH_implicative]
sBIH_prv_sind [definition, in GenHil.BiInt_GHC]
sBIH_prv_ind [definition, in GenHil.BiInt_GHC]
sBIH_prv [inductive, in GenHil.BiInt_GHC]
sBIH_wBIH_same_thms [lemma, in GenHil.BiInt_extens_interactions]
sBIH_extens_wBIH [lemma, in GenHil.BiInt_extens_interactions]
sBIH_Alg4 [lemma, in Alg.sBIH_algebraizable]
sBIH_Alg3 [lemma, in Alg.sBIH_algebraizable]
sBIH_Alg2 [lemma, in Alg.sBIH_algebraizable]
sBIH_Alg1 [lemma, in Alg.sBIH_algebraizable]
sBIH_Deduction_Theorem [lemma, in GenHil.sBIH_meta_interactions]
sBIH_Detachment_Theorem [lemma, in GenHil.sBIH_meta_interactions]
sBIH_alg_completeness [library]
sBIH_completeness [library]
sBIH_algebraizable [library]
sBIH_implicative [library]
sBIH_meta_interactions [library]
sClaim1 [lemma, in GenHil.sBIH_meta_interactions]
scomm_Or [lemma, in GenHil.sBIH_meta_interactions]
scomm_Or_obj [lemma, in GenHil.sBIH_meta_interactions]
scomm_And_obj [lemma, in GenHil.sBIH_meta_interactions]
sCompleteness [lemma, in Krip.sBIH_completeness]
sContr_Bot [lemma, in GenHil.sBIH_meta_interactions]
sDN [constructor, in GenHil.BiInt_GHC]
sDN_form_dist_imp [lemma, in GenHil.sBIH_meta_interactions]
sDN_dist_imp [lemma, in GenHil.sBIH_meta_interactions]
sDN_to_form [lemma, in GenHil.sBIH_meta_interactions]
sdual_residuation [lemma, in GenHil.sBIH_meta_interactions]
second_zho_lattice_filters [definition, in Alg.wBIH_not_algebraizable]
sEFQ [lemma, in GenHil.sBIH_meta_interactions]
sEq [definition, in Alg.sBIH_alg_completeness]
sEq [definition, in Alg.alg_soundness]
setform [projection, in Alg.sBIH_alg_completeness]
setform [projection, in Alg.wBIH_alg_completeness]
sfform_eqprv [definition, in Alg.sBIH_alg_completeness]
sfform_eqprv [definition, in Alg.wBIH_alg_completeness]
sfjoin [definition, in Alg.sBIH_alg_completeness]
sfjoin [definition, in Alg.wBIH_alg_completeness]
sfmeet [definition, in Alg.sBIH_alg_completeness]
sfmeet [definition, in Alg.wBIH_alg_completeness]
sfone [definition, in Alg.sBIH_alg_completeness]
sfone [definition, in Alg.wBIH_alg_completeness]
sfrpc [definition, in Alg.sBIH_alg_completeness]
sfrpc [definition, in Alg.wBIH_alg_completeness]
sfsubtr [definition, in Alg.sBIH_alg_completeness]
sfsubtr [definition, in Alg.wBIH_alg_completeness]
sfzero [definition, in Alg.sBIH_alg_completeness]
sfzero [definition, in Alg.wBIH_alg_completeness]
sId [constructor, in GenHil.BiInt_GHC]
sImp_And [lemma, in GenHil.sBIH_meta_interactions]
sImp_trans [lemma, in GenHil.sBIH_meta_interactions]
simp_Id_gen [lemma, in GenHil.sBIH_meta_interactions]
smonoL_Excl [lemma, in GenHil.sBIH_meta_interactions]
smonoR_Excl [lemma, in GenHil.sBIH_meta_interactions]
smonotL_Or [lemma, in GenHil.sBIH_meta_interactions]
smonotR_Or [lemma, in GenHil.sBIH_meta_interactions]
sMP [constructor, in GenHil.BiInt_GHC]
sOr_imp_assoc [lemma, in GenHil.sBIH_meta_interactions]
sOr_Neg [lemma, in GenHil.sBIH_meta_interactions]
Soundness [section, in Alg.alg_soundness]
Soundness_LEM.LEM [variable, in Krip.BiInt_soundness]
Soundness_LEM [section, in Krip.BiInt_soundness]
spair_der [definition, in GenHil.BiInt_GHC]
spair_dual_residuation_gen [lemma, in GenHil.sBIH_meta_interactions]
sprv_Top [lemma, in GenHil.sBIH_meta_interactions]
sQuasiCompleteness [lemma, in Krip.sBIH_completeness]
sSoundCompl [lemma, in Krip.sBIH_completeness]
sSoundness [definition, in Krip.BiInt_soundness]
stable [definition, in GenHil.BiInt_Lindenbaum_lem]
Stable [projection, in Krip.wBIH_completeness]
stable_Lind_pair [lemma, in GenHil.BiInt_Lindenbaum_lem]
sThm_irrel [lemma, in GenHil.sBIH_meta_interactions]
sT_for_DN [lemma, in GenHil.sBIH_meta_interactions]
subform [definition, in Synt.Syntax]
subformlist [definition, in Synt.Syntax]
subst [definition, in Synt.Syntax]
subst_Ax [lemma, in GenHil.BiInt_logics]
subtr [projection, in Alg.Bi_Heyting_Algebras]
subtr_meet [lemma, in Alg.Bi_Heyting_Algebras]
swap_remove_list [lemma, in Synt.lems_remove_list]
Syntax [library]
s_val_persist [lemma, in Krip.sBIH_completeness]
s_R_trans [lemma, in Krip.sBIH_completeness]
s_R_refl [lemma, in Krip.sBIH_completeness]
s_pruned_val [definition, in Krip.sBIH_completeness]
s_pruned_rel [definition, in Krip.sBIH_completeness]
s_pruned_worlds [definition, in Krip.sBIH_completeness]
s_is_n_reachable [definition, in Krip.sBIH_completeness]
T
Thm_irrel [lemma, in GenHil.wBIH_meta_interactions]three_zho_lattice_filters [definition, in Alg.wBIH_not_algebraizable]
too_many_disj1 [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
too_many_disj10 [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
too_many_disj0 [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
too_many_disj00 [lemma, in GenHil.BiInt_Lindenbaum_lem_prelim]
Top [constructor, in Synt.Syntax]
TpFq [inductive, in Krip.BiInt_sem_look_back]
TpFq_sind [definition, in Krip.BiInt_sem_look_back]
TpFq_rec [definition, in Krip.BiInt_sem_look_back]
TpFq_ind [definition, in Krip.BiInt_sem_look_back]
TpFq_rect [definition, in Krip.BiInt_sem_look_back]
transitiveT [definition, in General.genT]
Trois [constructor, in Krip.BiInt_sem_look_back]
true_and [lemma, in General.gen]
truth_lemma [lemma, in Krip.wBIH_completeness]
T_for_DN [lemma, in GenHil.wBIH_meta_interactions]
U
UDle [definition, in Krip.BiInt_sem_look_back]UDle_trans [lemma, in Krip.BiInt_sem_look_back]
UDle_refl [lemma, in Krip.BiInt_sem_look_back]
UDTle [definition, in Krip.BiInt_sem_look_back]
UDTle_trans [lemma, in Krip.BiInt_sem_look_back]
UDTle_refl [lemma, in Krip.BiInt_sem_look_back]
Un [constructor, in Krip.BiInt_sem_look_back]
Under_Lind_pair [lemma, in GenHil.BiInt_Lindenbaum_lem]
Under_Lind_pair_init [lemma, in GenHil.BiInt_Lindenbaum_lem]
Under_nprime_theory [lemma, in GenHil.BiInt_Lindenbaum_lem]
UnDeux [inductive, in Krip.BiInt_sem_look_back]
UnDeuxTrois [inductive, in Krip.BiInt_sem_look_back]
UnDeuxTrois_sind [definition, in Krip.BiInt_sem_look_back]
UnDeuxTrois_rec [definition, in Krip.BiInt_sem_look_back]
UnDeuxTrois_ind [definition, in Krip.BiInt_sem_look_back]
UnDeuxTrois_rect [definition, in Krip.BiInt_sem_look_back]
UnDeux_I [constructor, in Krip.BiInt_sem_look_back]
UnDeux_sind [definition, in Krip.BiInt_sem_look_back]
UnDeux_rec [definition, in Krip.BiInt_sem_look_back]
UnDeux_ind [definition, in Krip.BiInt_sem_look_back]
UnDeux_rect [definition, in Krip.BiInt_sem_look_back]
V
val [projection, in Krip.BiInt_Kripke_sem]valid_form [definition, in Krip.BiInt_Kripke_sem]
val1 [definition, in Krip.BiInt_sem_look_back]
val2 [definition, in Krip.BiInt_sem_look_back]
val3 [definition, in Krip.BiInt_sem_look_back]
Var [constructor, in Synt.Syntax]
vm [definition, in Alg.wBIH_no_biHA_alg_sem]
W
want_prod_under_universal4 [lemma, in General.genT]want_right_prod_under_universal' [lemma, in General.genT]
want_right_prod_under_universal [lemma, in General.genT]
want_left_prod_under_universal [lemma, in General.genT]
wAx [constructor, in GenHil.BiInt_GHC]
wBIH_closed [projection, in Alg.wBIH_not_algebraizable]
wBIH_filter [record, in Alg.wBIH_not_algebraizable]
wBIH_finite [lemma, in GenHil.BiInt_logics]
wBIH_struct [lemma, in GenHil.BiInt_logics]
wBIH_comp [lemma, in GenHil.BiInt_logics]
wBIH_monot [lemma, in GenHil.BiInt_logics]
wBIH_Dual_Deduction_Theorem [lemma, in GenHil.wBIH_meta_interactions]
wBIH_Dual_Detachment_Theorem [lemma, in GenHil.wBIH_meta_interactions]
wBIH_Deduction_Theorem [lemma, in GenHil.wBIH_meta_interactions]
wBIH_Detachment_Theorem [lemma, in GenHil.wBIH_meta_interactions]
wBIH_Re_Excl_fail [lemma, in Alg.wBIH_equivalential]
wBIH_Re_Excl [lemma, in Alg.wBIH_equivalential]
wBIH_Re_Imp [lemma, in Alg.wBIH_equivalential]
wBIH_Re_Or [lemma, in Alg.wBIH_equivalential]
wBIH_Re_And [lemma, in Alg.wBIH_equivalential]
wBIH_Re_Bot [lemma, in Alg.wBIH_equivalential]
wBIH_Re_Top [lemma, in Alg.wBIH_equivalential]
wBIH_MP [lemma, in Alg.wBIH_equivalential]
wBIH_R [lemma, in Alg.wBIH_equivalential]
wBIH_prv_sind [definition, in GenHil.BiInt_GHC]
wBIH_prv_ind [definition, in GenHil.BiInt_GHC]
wBIH_prv [inductive, in GenHil.BiInt_GHC]
wBIH_no_biHA_alg_sem [library]
wBIH_equivalential [library]
wBIH_completeness [library]
wBIH_not_algebraizable [library]
wBIH_meta_interactions [library]
wBIH_alg_completeness [library]
wClaim1 [lemma, in GenHil.wBIH_meta_interactions]
wCompleteness [lemma, in Krip.wBIH_completeness]
wDN [constructor, in GenHil.BiInt_GHC]
well_foundedT [definition, in General.genT]
wforces [definition, in Krip.BiInt_Kripke_sem]
wforces_dec [lemma, in Krip.BiInt_soundness]
wforces_DN_form_le [lemma, in Alg.wBIH_equivalential]
wId [constructor, in GenHil.BiInt_GHC]
wMP [constructor, in GenHil.BiInt_GHC]
wpair_der [definition, in GenHil.BiInt_GHC]
wQuasiCompleteness [lemma, in Krip.wBIH_completeness]
wSoundCompl [lemma, in Krip.wBIH_completeness]
wSoundness [definition, in Krip.BiInt_soundness]
w_Xmas_lightsM_nbisim_M [lemma, in Alg.wBIH_no_biHA_alg_sem]
X
Xmas_lights [definition, in Alg.wBIH_equivalential]Xmas_lightsM_nbisim_M [lemma, in Alg.wBIH_no_biHA_alg_sem]
Xmas_lightsM [definition, in Alg.wBIH_no_biHA_alg_sem]
Z
Zero [constructor, in Alg.wBIH_not_algebraizable]zero [projection, in Alg.Bi_Heyting_Algebras]
Zero_low [constructor, in Alg.wBIH_not_algebraizable]
zho_alg [definition, in Alg.wBIH_not_algebraizable]
zho_leq_sind [definition, in Alg.wBIH_not_algebraizable]
zho_leq_ind [definition, in Alg.wBIH_not_algebraizable]
zho_leq_refl [constructor, in Alg.wBIH_not_algebraizable]
zho_leq [inductive, in Alg.wBIH_not_algebraizable]
zho_type_sind [definition, in Alg.wBIH_not_algebraizable]
zho_type_rec [definition, in Alg.wBIH_not_algebraizable]
zho_type_ind [definition, in Alg.wBIH_not_algebraizable]
zho_type_rect [definition, in Alg.wBIH_not_algebraizable]
zho_type [inductive, in Alg.wBIH_not_algebraizable]
zw [definition, in Alg.wBIH_no_biHA_alg_sem]
zz [definition, in Krip.sBIH_completeness]
other
∞ _ (My_scope) [notation, in Synt.Syntax]¬ _ (My_scope) [notation, in Synt.Syntax]
⊤ (My_scope) [notation, in Synt.Syntax]
⊥ (My_scope) [notation, in Synt.Syntax]
_ <--> _ (My_scope) [notation, in Synt.Syntax]
_ ∧ _ (My_scope) [notation, in Synt.Syntax]
_ ∨ _ (My_scope) [notation, in Synt.Syntax]
_ --< _ (My_scope) [notation, in Synt.Syntax]
_ --> _ (My_scope) [notation, in Synt.Syntax]
# _ (My_scope) [notation, in Synt.Syntax]
existsT2 _ .. _ , _ (type_scope) [notation, in General.existsT]
existsT _ .. _ , _ (type_scope) [notation, in General.existsT]
Notation Index
B
_ << _ [in Alg.Bi_Heyting_Algebras]other
∞ _ (My_scope) [in Synt.Syntax]¬ _ (My_scope) [in Synt.Syntax]
⊤ (My_scope) [in Synt.Syntax]
⊥ (My_scope) [in Synt.Syntax]
_ <--> _ (My_scope) [in Synt.Syntax]
_ ∧ _ (My_scope) [in Synt.Syntax]
_ ∨ _ (My_scope) [in Synt.Syntax]
_ --< _ (My_scope) [in Synt.Syntax]
_ --> _ (My_scope) [in Synt.Syntax]
# _ (My_scope) [in Synt.Syntax]
existsT2 _ .. _ , _ (type_scope) [in General.existsT]
existsT _ .. _ , _ (type_scope) [in General.existsT]
Variable Index
A
algebraizable.Hypirrel [in Alg.sBIH_algebraizable]B
biHalg_props.BH [in Alg.Bi_Heyting_Algebras]C
Completeness.Hypirrel [in Alg.sBIH_alg_completeness]Completeness.Hypirrel [in Alg.wBIH_alg_completeness]
Completeness.Γ [in Alg.sBIH_alg_completeness]
E
Equiprovable_classes.Γ [in Alg.sBIH_alg_completeness]equivalential.LEM [in Alg.wBIH_equivalential]
L
LEM_completeness.LEM [in Krip.wBIH_completeness]Lindenbaum_algebra.Hypirrel [in Alg.sBIH_alg_completeness]
Lindenbaum_algebra.Γ [in Alg.sBIH_alg_completeness]
Lindenbaum_algebra.Hypirrel [in Alg.wBIH_alg_completeness]
M
model_construction.w [in Alg.wBIH_no_biHA_alg_sem]model_construction.M [in Alg.wBIH_no_biHA_alg_sem]
N
not_finitely_equivalential.n [in Alg.wBIH_equivalential]no_isomorphism.LEM [in Alg.wBIH_not_algebraizable]
No_biHA_semantics.wBIH_alg_sem [in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics.Eq [in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics.LEM [in Alg.wBIH_no_biHA_alg_sem]
No_biHA_semantics.Hypirrel [in Alg.wBIH_no_biHA_alg_sem]
P
Properties_eqprv.eqprv_prf_irrel [in Alg.sBIH_alg_completeness]Properties_eqprv.Γ [in Alg.sBIH_alg_completeness]
Properties_eqprv.eqprv_prf_irrel [in Alg.wBIH_alg_completeness]
pruning.M [in Krip.sBIH_completeness]
pruning.s [in Krip.sBIH_completeness]
S
Soundness_LEM.LEM [in Krip.BiInt_soundness]Library Index
A
algebraic_semanticalg_soundness
B
BIH_exportBiInt_soundness
BiInt_sem_look_back
BiInt_Kripke_sem
BiInt_Lindenbaum_lem_prelim
BiInt_enum
BiInt_bisimulation
BiInt_extens_interactions
BiInt_logics
BiInt_Lindenbaum_lem
BiInt_GHC
Bi_Heyting_Algebras
E
existsTG
gengenT
K
Kripke_exportL
lems_remove_listS
sBIH_alg_completenesssBIH_completeness
sBIH_algebraizable
sBIH_implicative
sBIH_meta_interactions
Syntax
W
wBIH_no_biHA_alg_semwBIH_equivalential
wBIH_completeness
wBIH_not_algebraizable
wBIH_meta_interactions
wBIH_alg_completeness
Lemma Index
A
absorp_Or2 [in GenHil.wBIH_meta_interactions]absorp_Or1 [in GenHil.wBIH_meta_interactions]
add_remove_list_preserve_NoDup [in Synt.lems_remove_list]
aleq_antisym [in Alg.Bi_Heyting_Algebras]
aleq_refl [in Alg.Bi_Heyting_Algebras]
aleq_trans [in Alg.Bi_Heyting_Algebras]
algord_soundness_wBIH [in Alg.alg_soundness]
algtd_soundness_wBIH [in Alg.alg_soundness]
algtd_completeness_wBIH [in Alg.wBIH_alg_completeness]
alg_completeness_sBIH [in Alg.sBIH_alg_completeness]
alg_soundness_wBIH_eq [in Alg.alg_soundness]
alg_soundness_sBIH [in Alg.alg_soundness]
alg_eq_iff_wBIH_eqprv [in Alg.wBIH_no_biHA_alg_sem]
alg_BA4 [in Alg.Bi_Heyting_Algebras]
alg_BA3 [in Alg.Bi_Heyting_Algebras]
alg_BA2 [in Alg.Bi_Heyting_Algebras]
alg_BA1 [in Alg.Bi_Heyting_Algebras]
alg_A10 [in Alg.Bi_Heyting_Algebras]
alg_A9 [in Alg.Bi_Heyting_Algebras]
alg_A8 [in Alg.Bi_Heyting_Algebras]
alg_A7 [in Alg.Bi_Heyting_Algebras]
alg_A6 [in Alg.Bi_Heyting_Algebras]
alg_A5 [in Alg.Bi_Heyting_Algebras]
alg_A4 [in Alg.Bi_Heyting_Algebras]
alg_A3 [in Alg.Bi_Heyting_Algebras]
alg_A2 [in Alg.Bi_Heyting_Algebras]
alg_A1 [in Alg.Bi_Heyting_Algebras]
always_add_a_nat [in GenHil.BiInt_Lindenbaum_lem_prelim]
And_Imp [in GenHil.wBIH_meta_interactions]
and_true [in General.gen]
anonD [in General.genT]
anonI [in General.genT]
anon_forall [in General.genT]
anon_sigT [in General.genT]
anon_iffT [in General.genT]
anon_imp [in General.genT]
anon_sum [in General.genT]
anon_prod [in General.genT]
anon_eq [in General.genT]
appl [in General.gen]
app_remove_list [in Synt.lems_remove_list]
arg_cong_imp' [in General.gen]
arg_cong_imp [in General.gen]
arg_cong [in General.gen]
arg1_cong_imp' [in General.gen]
arg1_cong_imp [in General.gen]
assoc_And_obj [in GenHil.wBIH_meta_interactions]
AThm_irrel [in GenHil.wBIH_meta_interactions]
Axioms_one [in Alg.alg_soundness]
Ax_valid [in Krip.BiInt_soundness]
B
BiLEM [in GenHil.wBIH_meta_interactions]bisimulation_imp_bi_int_equiv [in Krip.BiInt_bisimulation]
bi_LEM [in Alg.Bi_Heyting_Algebras]
C
closeder_fst_Lind_pair [in GenHil.BiInt_Lindenbaum_lem]Closure_DN_strong [in GenHil.sBIH_meta_interactions]
comm_Or [in GenHil.wBIH_meta_interactions]
comm_Or_obj [in GenHil.wBIH_meta_interactions]
comm_And_obj [in GenHil.wBIH_meta_interactions]
Compl_prime_theory_extens [in GenHil.BiInt_Lindenbaum_lem]
Consequences_Soundness4 [in Krip.BiInt_sem_look_back]
Consequences_Soundness3 [in Krip.BiInt_sem_look_back]
Consequences_Soundness2 [in Krip.BiInt_sem_look_back]
Consequences_Soundness1 [in Krip.BiInt_sem_look_back]
Consist_prime_theory [in GenHil.BiInt_Lindenbaum_lem]
Consist_nprime_theory [in GenHil.BiInt_Lindenbaum_lem]
Contrapositive [in GenHil.wBIH_meta_interactions]
Contr_Bot [in GenHil.wBIH_meta_interactions]
ctx_dual_residuation_obj [in GenHil.wBIH_meta_interactions]
Cut [in GenHil.wBIH_meta_interactions]
C_val_persist [in Krip.wBIH_completeness]
C_R_trans [in Krip.wBIH_completeness]
C_R_refl [in Krip.wBIH_completeness]
D
dec_zho_leq_qel [in Alg.wBIH_not_algebraizable]dec_zho_leq [in Alg.wBIH_not_algebraizable]
depth_zero [in Synt.Syntax]
der_prime_theory_nprime_theory [in GenHil.BiInt_Lindenbaum_lem]
der_nprime_theory_mprime_theory_le [in GenHil.BiInt_Lindenbaum_lem]
der_list_conj_finite_context [in GenHil.wBIH_meta_interactions]
der_list_disj_bot [in GenHil.wBIH_meta_interactions]
der_list_disj_remove2 [in GenHil.wBIH_meta_interactions]
der_list_disj_remove1 [in GenHil.wBIH_meta_interactions]
der_mult_disj_Bot [in GenHil.BiInt_Lindenbaum_lem_prelim]
distr_join_meet [in Alg.Bi_Heyting_Algebras]
distr_meet_join [in Alg.Bi_Heyting_Algebras]
DN_clos_DN_form [in Krip.sBIH_completeness]
DN_form_DN [in Krip.sBIH_completeness]
DN_form_interp [in Alg.algebraic_semantic]
DN_form_rule [in GenHil.wBIH_meta_interactions]
DN_form_dist_imp [in GenHil.wBIH_meta_interactions]
DN_dist_imp [in GenHil.wBIH_meta_interactions]
DN_to_form [in GenHil.wBIH_meta_interactions]
DN_form_n_reachable [in Alg.wBIH_equivalential]
DN_form_S [in Synt.Syntax]
double_remove [in Synt.lems_remove_list]
double_coneg [in Alg.Bi_Heyting_Algebras]
double_neg [in Alg.Bi_Heyting_Algebras]
dual_MP [in GenHil.wBIH_meta_interactions]
dual_residuation_gen [in GenHil.wBIH_meta_interactions]
dual_residuation [in GenHil.wBIH_meta_interactions]
dual_residuation_obj [in GenHil.wBIH_meta_interactions]
d_to_l_filter [in Alg.wBIH_not_algebraizable]
E
EFQ [in GenHil.wBIH_meta_interactions]epdresiduation [in Alg.sBIH_alg_completeness]
epdresiduation [in Alg.wBIH_alg_completeness]
epgreatest [in Alg.sBIH_alg_completeness]
epgreatest [in Alg.wBIH_alg_completeness]
epjabsorp [in Alg.sBIH_alg_completeness]
epjabsorp [in Alg.wBIH_alg_completeness]
epjassoc [in Alg.sBIH_alg_completeness]
epjassoc [in Alg.wBIH_alg_completeness]
epjcomm [in Alg.sBIH_alg_completeness]
epjcomm [in Alg.wBIH_alg_completeness]
eplowest [in Alg.sBIH_alg_completeness]
eplowest [in Alg.wBIH_alg_completeness]
epmabsorp [in Alg.sBIH_alg_completeness]
epmabsorp [in Alg.wBIH_alg_completeness]
epmassoc [in Alg.sBIH_alg_completeness]
epmassoc [in Alg.wBIH_alg_completeness]
epmcomm [in Alg.sBIH_alg_completeness]
epmcomm [in Alg.wBIH_alg_completeness]
epresiduation [in Alg.sBIH_alg_completeness]
epresiduation [in Alg.wBIH_alg_completeness]
eprvform_eqprv [in Alg.sBIH_alg_completeness]
eprvform_eqprv [in Alg.wBIH_alg_completeness]
eprvjoin [in Alg.sBIH_alg_completeness]
eprvjoin [in Alg.wBIH_alg_completeness]
eprvmeet [in Alg.sBIH_alg_completeness]
eprvmeet [in Alg.wBIH_alg_completeness]
eprvone [in Alg.sBIH_alg_completeness]
eprvone [in Alg.wBIH_alg_completeness]
eprvrpc [in Alg.sBIH_alg_completeness]
eprvrpc [in Alg.wBIH_alg_completeness]
eprvsubtr [in Alg.sBIH_alg_completeness]
eprvsubtr [in Alg.wBIH_alg_completeness]
eprvzero [in Alg.sBIH_alg_completeness]
eprvzero [in Alg.wBIH_alg_completeness]
eq_S_F [in General.genT]
eq_dec_form [in Synt.Syntax]
eq_TrueI [in General.gen]
Eq_elem_invalid [in Alg.wBIH_no_biHA_alg_sem]
eq_repres_aleq [in Alg.Bi_Heyting_Algebras]
Even_Odd_dec [in Alg.wBIH_equivalential]
extens_diff_sBIH [in GenHil.BiInt_extens_interactions]
F
failure_gen_sBIH_Dual_Detachment_Theorem [in Krip.BiInt_sem_look_back]failure_gen_sBIH_Deduction_Theorem [in Krip.BiInt_sem_look_back]
failure_Xmas_lights [in Alg.wBIH_equivalential]
false_or [in General.gen]
finite_context_list_conj [in GenHil.wBIH_meta_interactions]
first_subst_interp [in Alg.algebraic_semantic]
first_subst_idem [in Synt.Syntax]
ForallT_Forall [in General.genT]
ForallT_Forall' [in General.genT]
ForallT_forall [in General.genT]
ForallT_impl [in General.genT]
ForallT_map_rev [in General.genT]
ForallT_map [in General.genT]
ForallT_map_2 [in General.genT]
ForallT_2 [in General.genT]
ForallT_append [in General.genT]
ForallT_cons_iff [in General.genT]
ForallT_single [in General.genT]
ForallT_cons_inv [in General.genT]
ForallT_inv [in General.genT]
Forall_ForallT' [in General.genT]
Forall_ForallT [in General.genT]
forall_list_disj [in GenHil.wBIH_meta_interactions]
Forall_map_2 [in General.gen]
Forall_map_single [in General.gen]
Forall_single [in General.gen]
Forall_append [in General.gen]
Forall_cons_iff [in General.gen]
Forall_cons_inv [in General.gen]
Forall2T_ex_r [in General.genT]
Forall2T_ex_l [in General.genT]
Forall2T_app [in General.genT]
Forall2T_app_inv_r [in General.genT]
Forall2T_app_inv_l [in General.genT]
form_index_inj [in GenHil.BiInt_enum]
form_enum_index [in GenHil.BiInt_enum]
form_enum_sur [in GenHil.BiInt_enum]
fun_cong [in General.gen]
G
gen_wBIH_Dual_Deduction_Theorem [in GenHil.wBIH_meta_interactions]gen_wBIH_Dual_Detachment_Theorem [in GenHil.wBIH_meta_interactions]
gen_wBIH_Deduction_Theorem [in GenHil.wBIH_meta_interactions]
gen_wBIH_Detachment_Theorem [in GenHil.wBIH_meta_interactions]
gen_sBIH_Double_Negated_Detachment_Theorem [in GenHil.sBIH_meta_interactions]
gen_sBIH_Deduction_Theorem [in GenHil.sBIH_meta_interactions]
gen_sBIH_Detachment_Theorem [in GenHil.sBIH_meta_interactions]
gen_cong [in General.gen]
glb [in Alg.Bi_Heyting_Algebras]
H
head_n_zz [in Alg.wBIH_equivalential]head_n_reachable [in Alg.wBIH_equivalential]
high_one [in Alg.Bi_Heyting_Algebras]
I
Id_list_disj_remove [in GenHil.wBIH_meta_interactions]Id_list_disj [in GenHil.wBIH_meta_interactions]
iffD1 [in General.gen]
iffD2 [in General.gen]
iffT_prod [in General.genT]
iffT_D2' [in General.genT]
iffT_D1' [in General.genT]
iffT_refl [in General.genT]
iffT_sym' [in General.genT]
iffT_trans [in General.genT]
Imp_And [in GenHil.wBIH_meta_interactions]
Imp_trans [in GenHil.wBIH_meta_interactions]
Imp_trans_help427 [in GenHil.wBIH_meta_interactions]
Imp_trans_help410 [in GenHil.wBIH_meta_interactions]
Imp_trans_help170 [in GenHil.wBIH_meta_interactions]
Imp_trans_help54 [in GenHil.wBIH_meta_interactions]
Imp_trans_help37 [in GenHil.wBIH_meta_interactions]
Imp_trans_help35 [in GenHil.wBIH_meta_interactions]
Imp_trans_help14 [in GenHil.wBIH_meta_interactions]
Imp_trans_help9 [in GenHil.wBIH_meta_interactions]
Imp_trans_help8 [in GenHil.wBIH_meta_interactions]
Imp_trans_help7 [in GenHil.wBIH_meta_interactions]
imp_Id_gen [in GenHil.wBIH_meta_interactions]
inhabited_anon [in General.genT]
inhab_eqprv [in Alg.sBIH_alg_completeness]
inhab_eqprv [in Alg.wBIH_alg_completeness]
InT_In_eq' [in General.genT]
InT_In_eq [in General.genT]
InT_In' [in General.genT]
InT_In [in General.genT]
InT_concat [in General.genT]
InT_map_iffT [in General.genT]
InT_mapE [in General.genT]
InT_map [in General.genT]
InT_inv [in General.genT]
InT_split [in General.genT]
InT_nilE [in General.genT]
InT_nilE' [in General.genT]
InT_appE [in General.genT]
InT_appE' [in General.genT]
InT_appR [in General.genT]
InT_appL [in General.genT]
InT_eq [in General.genT]
InT_remove [in GenHil.wBIH_meta_interactions]
In_InT [in General.genT]
in_sfform_eqprv [in Alg.sBIH_alg_completeness]
In_remove [in GenHil.wBIH_meta_interactions]
in_sfform_eqprv [in Alg.wBIH_alg_completeness]
In_matters_remove_list [in Synt.lems_remove_list]
In_remove_list_remove_redund [in Synt.lems_remove_list]
In_remove_list_In_list_not_In_remove_list [in Synt.lems_remove_list]
In_remove_list_In_list [in Synt.lems_remove_list]
In_remove_In_list [in Synt.lems_remove_list]
In_remove_length_same [in Synt.lems_remove_list]
In_remove_same [in Synt.lems_remove_list]
In_remove_diff [in Synt.lems_remove_list]
in_remove_in_init [in Synt.lems_remove_list]
in_not_touched_remove [in Synt.lems_remove_list]
In_dec [in Synt.lems_remove_list]
In_form_dec [in Synt.Syntax]
in_single [in General.gen]
J
join_deep [in Alg.Bi_Heyting_Algebras]join_inj2 [in Alg.Bi_Heyting_Algebras]
join_inj1 [in Alg.Bi_Heyting_Algebras]
join_id [in Alg.Bi_Heyting_Algebras]
K
keep_list_delete_head_not_In [in Synt.lems_remove_list]keep_list_delete_head_not_origin [in Synt.lems_remove_list]
L
LEM_sSoundness [in Krip.BiInt_soundness]LEM_wSoundness [in Krip.BiInt_soundness]
LEM_world [in Krip.wBIH_completeness]
LEM_Lindenbaum [in Krip.wBIH_completeness]
LEM_prime [in Krip.wBIH_completeness]
length_le_remove_list [in Synt.lems_remove_list]
leT_ex_plus [in General.genT]
leT_or_gt [in General.genT]
leT_S_or_eq [in General.genT]
leT_S_F [in General.genT]
leT_plus_l [in General.genT]
leT_plus_r [in General.genT]
leT_0_n [in General.genT]
leT_trans' [in General.genT]
leT_S_n' [in General.genT]
leT_n_S [in General.genT]
LindAlgrepres [in Alg.sBIH_alg_completeness]
LindAlgrepres [in Alg.wBIH_alg_completeness]
Lindenbaum [in GenHil.BiInt_Lindenbaum_lem]
list_disj_witn [in Krip.BiInt_soundness]
list_disj_prime [in GenHil.BiInt_Lindenbaum_lem]
list_conj_interp [in Alg.algebraic_semantic]
list_conj_finite_context [in GenHil.wBIH_meta_interactions]
list_conj_in_list [in GenHil.wBIH_meta_interactions]
list_disj_nodup [in GenHil.wBIH_meta_interactions]
list_disj_In_prv [in GenHil.wBIH_meta_interactions]
list_disj_app_distr [in GenHil.wBIH_meta_interactions]
list_disj_In [in GenHil.wBIH_meta_interactions]
list_disj_In0 [in GenHil.wBIH_meta_interactions]
list_disj_remove_form [in GenHil.wBIH_meta_interactions]
list_disj_remove_app [in GenHil.wBIH_meta_interactions]
list_disj_app0 [in GenHil.wBIH_meta_interactions]
list_disj_app [in GenHil.wBIH_meta_interactions]
list_all_pred_nat [in GenHil.BiInt_Lindenbaum_lem_prelim]
list_meet_all [in Alg.Bi_Heyting_Algebras]
low_zero [in Alg.Bi_Heyting_Algebras]
lub [in Alg.Bi_Heyting_Algebras]
L_enum_exhaustive [in GenHil.BiInt_enum]
L_enum_cumulative [in GenHil.BiInt_enum]
l_to_d_filter [in Alg.wBIH_not_algebraizable]
M
map_eq_nil [in General.gen]map_app_ex [in General.gen]
map_cons_ex' [in General.gen]
map_cons_ex [in General.gen]
max_of_list [in GenHil.BiInt_Lindenbaum_lem_prelim]
meet_deep [in Alg.Bi_Heyting_Algebras]
meet_elim2 [in Alg.Bi_Heyting_Algebras]
meet_elim1 [in Alg.Bi_Heyting_Algebras]
meet_absorp3 [in Alg.Bi_Heyting_Algebras]
meet_absorp2 [in Alg.Bi_Heyting_Algebras]
meet_absorp1 [in Alg.Bi_Heyting_Algebras]
meet_absorp0 [in Alg.Bi_Heyting_Algebras]
meet_id [in Alg.Bi_Heyting_Algebras]
meta_Imp_trans [in GenHil.wBIH_meta_interactions]
meta_sImp_trans [in GenHil.sBIH_meta_interactions]
monoL_Excl [in GenHil.wBIH_meta_interactions]
monoR_Excl [in GenHil.wBIH_meta_interactions]
monotL_Or [in GenHil.wBIH_meta_interactions]
monotR_Or [in GenHil.wBIH_meta_interactions]
monot_Or2 [in GenHil.wBIH_meta_interactions]
monot_Or2 [in GenHil.sBIH_meta_interactions]
mp [in Alg.Bi_Heyting_Algebras]
mult_disj_dec [in GenHil.BiInt_Lindenbaum_lem_prelim]
mult_disj_dec1 [in GenHil.BiInt_Lindenbaum_lem_prelim]
mult_disj_dec0 [in GenHil.BiInt_Lindenbaum_lem_prelim]
mult_disj_Id [in GenHil.BiInt_Lindenbaum_lem_prelim]
N
nat_remove_In_smaller_length [in GenHil.BiInt_Lindenbaum_lem_prelim]nat_remove_le_length [in GenHil.BiInt_Lindenbaum_lem_prelim]
NoDup_remove [in GenHil.wBIH_meta_interactions]
NoDup_destr_split [in Synt.lems_remove_list]
not_In_prime_theory_deriv [in GenHil.BiInt_Lindenbaum_lem]
not_removed_remove_list [in Synt.lems_remove_list]
no_list_all_nat [in GenHil.BiInt_Lindenbaum_lem_prelim]
No_wBIH_alg_sem [in Alg.wBIH_no_biHA_alg_sem]
nprime_theory_extens_le [in GenHil.BiInt_Lindenbaum_lem]
nprime_theory_extens [in GenHil.BiInt_Lindenbaum_lem]
n_reachable_DN_clos [in Krip.sBIH_completeness]
n_reachable_zz [in Krip.sBIH_completeness]
n_reachable_head [in Krip.sBIH_completeness]
n_reachable_tail [in Krip.sBIH_completeness]
n_zz_reachable_subset [in Krip.sBIH_completeness]
n_bisimulation_imp_n_depth_equiv [in Krip.BiInt_bisimulation]
n_bisimulation_cum [in Krip.BiInt_bisimulation]
n_bisimulation_S [in Krip.BiInt_bisimulation]
n_reachable_finclos_DN_24 [in Alg.wBIH_equivalential]
n_reachable_finclos_DN_13 [in Alg.wBIH_equivalential]
n_reachable_Xmas_Id [in Alg.wBIH_equivalential]
n_reachable_False [in Alg.wBIH_equivalential]
n_zz_DN_clos_equiv [in Alg.wBIH_equivalential]
n_reachable_DN_clos_equiv [in Alg.wBIH_equivalential]
n_reachable_DN_clos [in Alg.wBIH_equivalential]
n_reachable_sym [in Alg.wBIH_no_biHA_alg_sem]
n_reachable_head [in Alg.wBIH_no_biHA_alg_sem]
n_reachable_Xmas [in Alg.wBIH_no_biHA_alg_sem]
O
only_two_zho_congruences [in Alg.wBIH_not_algebraizable]ord_dresid [in Alg.Bi_Heyting_Algebras]
ord_resid [in Alg.Bi_Heyting_Algebras]
Or_Neg [in GenHil.wBIH_meta_interactions]
Or_imp_assoc [in GenHil.wBIH_meta_interactions]
or_false [in General.gen]
P
pair_sBIH_extens_wBIH [in GenHil.BiInt_extens_interactions]pair_eqI [in General.gen]
permut_remove_remove_list [in Synt.lems_remove_list]
permut_remove [in Synt.lems_remove_list]
Persistence [in Krip.BiInt_Kripke_sem]
persist_val3 [in Krip.BiInt_sem_look_back]
persist_val2 [in Krip.BiInt_sem_look_back]
persist_val1 [in Krip.BiInt_sem_look_back]
PiffD1 [in General.gen]
PiffD2 [in General.gen]
prime_theory_extens [in GenHil.BiInt_Lindenbaum_lem]
prod_nat_split [in General.genT]
prod_mono [in General.genT]
pruned_wforces [in Krip.sBIH_completeness]
pruned_bisim [in Krip.sBIH_completeness]
prv_Top [in GenHil.wBIH_meta_interactions]
Q
quasi_prime_Lind_pair [in GenHil.BiInt_Lindenbaum_lem]R
rappl [in General.gen]redund_remove_list [in Synt.lems_remove_list]
redund_remove [in Synt.lems_remove_list]
redund_remove_remove_list [in Synt.lems_remove_list]
remove_disj [in GenHil.wBIH_meta_interactions]
remove_list_incr_decr [in Synt.lems_remove_list]
remove_list_incr_decr4 [in Synt.lems_remove_list]
remove_list_incr_decr2 [in Synt.lems_remove_list]
remove_list_incr_decr1 [in Synt.lems_remove_list]
remove_list_incr_decr3 [in Synt.lems_remove_list]
remove_delete_origin [in Synt.lems_remove_list]
remove_list_is_nil [in Synt.lems_remove_list]
remove_list_in_nil [in Synt.lems_remove_list]
remove_list_delete_head_In [in Synt.lems_remove_list]
remove_list_delete_head [in Synt.lems_remove_list]
remove_list_non_empty_inter_smaller_length [in Synt.lems_remove_list]
remove_list_singl_id_or_nil [in Synt.lems_remove_list]
remove_list_is_in [in Synt.lems_remove_list]
remove_list_in_single [in Synt.lems_remove_list]
remove_list_dist_app [in Synt.lems_remove_list]
remove_list_cont [in Synt.lems_remove_list]
remove_list_preserv_NoDup [in Synt.lems_remove_list]
remove_list_of_nil [in Synt.lems_remove_list]
remove_In_smaller_length [in Synt.lems_remove_list]
remove_le_length [in Synt.lems_remove_list]
remove_preserv_NoDup [in Synt.lems_remove_list]
remove_not_in_anymore [in Synt.lems_remove_list]
remove_dist_app [in Synt.lems_remove_list]
req_trans [in General.gen]
req_sym [in General.gen]
req_refl [in General.gen]
right_stable_Lind_pair [in GenHil.BiInt_Lindenbaum_lem]
Rooted_models_validity [in Krip.BiInt_sem_look_back]
rsub_id [in General.gen]
rsub_trans [in General.gen]
rsub_def [in General.gen]
S
sabsorp_Or1 [in GenHil.sBIH_meta_interactions]sAnd_Imp [in GenHil.sBIH_meta_interactions]
sassoc_And_obj [in GenHil.sBIH_meta_interactions]
sBIH_finite [in GenHil.BiInt_logics]
sBIH_struct [in GenHil.BiInt_logics]
sBIH_comp [in GenHil.BiInt_logics]
sBIH_monot [in GenHil.BiInt_logics]
sBIH_not_incl_wBIH [in Krip.BiInt_sem_look_back]
sBIH_IL3_Excl [in Alg.sBIH_implicative]
sBIH_IL3_Imp [in Alg.sBIH_implicative]
sBIH_IL3_Or [in Alg.sBIH_implicative]
sBIH_IL3_And [in Alg.sBIH_implicative]
sBIH_IL3_Bot [in Alg.sBIH_implicative]
sBIH_IL3_Top [in Alg.sBIH_implicative]
sBIH_IL5 [in Alg.sBIH_implicative]
sBIH_IL4 [in Alg.sBIH_implicative]
sBIH_IL2 [in Alg.sBIH_implicative]
sBIH_IL1 [in Alg.sBIH_implicative]
sBIH_wBIH_same_thms [in GenHil.BiInt_extens_interactions]
sBIH_extens_wBIH [in GenHil.BiInt_extens_interactions]
sBIH_Alg4 [in Alg.sBIH_algebraizable]
sBIH_Alg3 [in Alg.sBIH_algebraizable]
sBIH_Alg2 [in Alg.sBIH_algebraizable]
sBIH_Alg1 [in Alg.sBIH_algebraizable]
sBIH_Deduction_Theorem [in GenHil.sBIH_meta_interactions]
sBIH_Detachment_Theorem [in GenHil.sBIH_meta_interactions]
sClaim1 [in GenHil.sBIH_meta_interactions]
scomm_Or [in GenHil.sBIH_meta_interactions]
scomm_Or_obj [in GenHil.sBIH_meta_interactions]
scomm_And_obj [in GenHil.sBIH_meta_interactions]
sCompleteness [in Krip.sBIH_completeness]
sContr_Bot [in GenHil.sBIH_meta_interactions]
sDN_form_dist_imp [in GenHil.sBIH_meta_interactions]
sDN_dist_imp [in GenHil.sBIH_meta_interactions]
sDN_to_form [in GenHil.sBIH_meta_interactions]
sdual_residuation [in GenHil.sBIH_meta_interactions]
sEFQ [in GenHil.sBIH_meta_interactions]
sImp_And [in GenHil.sBIH_meta_interactions]
sImp_trans [in GenHil.sBIH_meta_interactions]
simp_Id_gen [in GenHil.sBIH_meta_interactions]
smonoL_Excl [in GenHil.sBIH_meta_interactions]
smonoR_Excl [in GenHil.sBIH_meta_interactions]
smonotL_Or [in GenHil.sBIH_meta_interactions]
smonotR_Or [in GenHil.sBIH_meta_interactions]
sOr_imp_assoc [in GenHil.sBIH_meta_interactions]
sOr_Neg [in GenHil.sBIH_meta_interactions]
spair_dual_residuation_gen [in GenHil.sBIH_meta_interactions]
sprv_Top [in GenHil.sBIH_meta_interactions]
sQuasiCompleteness [in Krip.sBIH_completeness]
sSoundCompl [in Krip.sBIH_completeness]
stable_Lind_pair [in GenHil.BiInt_Lindenbaum_lem]
sThm_irrel [in GenHil.sBIH_meta_interactions]
sT_for_DN [in GenHil.sBIH_meta_interactions]
subst_Ax [in GenHil.BiInt_logics]
subtr_meet [in Alg.Bi_Heyting_Algebras]
swap_remove_list [in Synt.lems_remove_list]
s_val_persist [in Krip.sBIH_completeness]
s_R_trans [in Krip.sBIH_completeness]
s_R_refl [in Krip.sBIH_completeness]
T
Thm_irrel [in GenHil.wBIH_meta_interactions]too_many_disj1 [in GenHil.BiInt_Lindenbaum_lem_prelim]
too_many_disj10 [in GenHil.BiInt_Lindenbaum_lem_prelim]
too_many_disj0 [in GenHil.BiInt_Lindenbaum_lem_prelim]
too_many_disj00 [in GenHil.BiInt_Lindenbaum_lem_prelim]
true_and [in General.gen]
truth_lemma [in Krip.wBIH_completeness]
T_for_DN [in GenHil.wBIH_meta_interactions]
U
UDle_trans [in Krip.BiInt_sem_look_back]UDle_refl [in Krip.BiInt_sem_look_back]
UDTle_trans [in Krip.BiInt_sem_look_back]
UDTle_refl [in Krip.BiInt_sem_look_back]
Under_Lind_pair [in GenHil.BiInt_Lindenbaum_lem]
Under_Lind_pair_init [in GenHil.BiInt_Lindenbaum_lem]
Under_nprime_theory [in GenHil.BiInt_Lindenbaum_lem]
W
want_prod_under_universal4 [in General.genT]want_right_prod_under_universal' [in General.genT]
want_right_prod_under_universal [in General.genT]
want_left_prod_under_universal [in General.genT]
wBIH_finite [in GenHil.BiInt_logics]
wBIH_struct [in GenHil.BiInt_logics]
wBIH_comp [in GenHil.BiInt_logics]
wBIH_monot [in GenHil.BiInt_logics]
wBIH_Dual_Deduction_Theorem [in GenHil.wBIH_meta_interactions]
wBIH_Dual_Detachment_Theorem [in GenHil.wBIH_meta_interactions]
wBIH_Deduction_Theorem [in GenHil.wBIH_meta_interactions]
wBIH_Detachment_Theorem [in GenHil.wBIH_meta_interactions]
wBIH_Re_Excl_fail [in Alg.wBIH_equivalential]
wBIH_Re_Excl [in Alg.wBIH_equivalential]
wBIH_Re_Imp [in Alg.wBIH_equivalential]
wBIH_Re_Or [in Alg.wBIH_equivalential]
wBIH_Re_And [in Alg.wBIH_equivalential]
wBIH_Re_Bot [in Alg.wBIH_equivalential]
wBIH_Re_Top [in Alg.wBIH_equivalential]
wBIH_MP [in Alg.wBIH_equivalential]
wBIH_R [in Alg.wBIH_equivalential]
wClaim1 [in GenHil.wBIH_meta_interactions]
wCompleteness [in Krip.wBIH_completeness]
wforces_dec [in Krip.BiInt_soundness]
wforces_DN_form_le [in Alg.wBIH_equivalential]
wQuasiCompleteness [in Krip.wBIH_completeness]
wSoundCompl [in Krip.wBIH_completeness]
w_Xmas_lightsM_nbisim_M [in Alg.wBIH_no_biHA_alg_sem]
X
Xmas_lightsM_nbisim_M [in Alg.wBIH_no_biHA_alg_sem]Axiom Index
L
LEM [in Krip.sBIH_completeness]LEM [in Alg.sBIH_alg_completeness]
LEM [in Alg.wBIH_alg_completeness]
Constructor Index
A
AccT_intro [in General.genT]And [in Synt.Syntax]
A1 [in GenHil.BiInt_GHC]
A10 [in GenHil.BiInt_GHC]
A2 [in GenHil.BiInt_GHC]
A3 [in GenHil.BiInt_GHC]
A4 [in GenHil.BiInt_GHC]
A5 [in GenHil.BiInt_GHC]
A6 [in GenHil.BiInt_GHC]
A7 [in GenHil.BiInt_GHC]
A8 [in GenHil.BiInt_GHC]
A9 [in GenHil.BiInt_GHC]
B
BA1 [in GenHil.BiInt_GHC]BA2 [in GenHil.BiInt_GHC]
BA3 [in GenHil.BiInt_GHC]
BA4 [in GenHil.BiInt_GHC]
Bot [in Synt.Syntax]
D
Deux [in Krip.BiInt_sem_look_back]E
Excl [in Synt.Syntax]F
ForallT_cons [in General.genT]ForallT_nil [in General.genT]
Forall2T_cons [in General.genT]
Forall2T_nil [in General.genT]
Fq [in Krip.BiInt_sem_look_back]
H
Half [in Alg.wBIH_not_algebraizable]I
Imp [in Synt.Syntax]IndClo [in Synt.Syntax]
InitClo [in Synt.Syntax]
InT_cons [in General.genT]
InT_eq' [in General.genT]
L
leT_S [in General.genT]leT_n [in General.genT]
O
One [in Alg.wBIH_not_algebraizable]One_high [in Alg.wBIH_not_algebraizable]
Or [in Synt.Syntax]
S
sAx [in GenHil.BiInt_GHC]sDN [in GenHil.BiInt_GHC]
sId [in GenHil.BiInt_GHC]
sMP [in GenHil.BiInt_GHC]
T
Top [in Synt.Syntax]Trois [in Krip.BiInt_sem_look_back]
U
Un [in Krip.BiInt_sem_look_back]UnDeux_I [in Krip.BiInt_sem_look_back]
V
Var [in Synt.Syntax]W
wAx [in GenHil.BiInt_GHC]wDN [in GenHil.BiInt_GHC]
wId [in GenHil.BiInt_GHC]
wMP [in GenHil.BiInt_GHC]
Z
Zero [in Alg.wBIH_not_algebraizable]Zero_low [in Alg.wBIH_not_algebraizable]
zho_leq_refl [in Alg.wBIH_not_algebraizable]
Inductive Index
A
AccT [in General.genT]Axioms [in GenHil.BiInt_GHC]
D
DN_clos_set [in Synt.Syntax]F
ForallT [in General.genT]Forall2T [in General.genT]
form [in Synt.Syntax]
I
InT [in General.genT]L
leT [in General.genT]S
sBIH_prv [in GenHil.BiInt_GHC]T
TpFq [in Krip.BiInt_sem_look_back]U
UnDeux [in Krip.BiInt_sem_look_back]UnDeuxTrois [in Krip.BiInt_sem_look_back]
W
wBIH_prv [in GenHil.BiInt_GHC]Z
zho_leq [in Alg.wBIH_not_algebraizable]zho_type [in Alg.wBIH_not_algebraizable]
Projection Index
A
aleq_closed [in Alg.wBIH_not_algebraizable]C
Closed [in Krip.wBIH_completeness]cong [in Alg.wBIH_not_algebraizable]
cong_subtr [in Alg.wBIH_not_algebraizable]
cong_rpc [in Alg.wBIH_not_algebraizable]
cong_join [in Alg.wBIH_not_algebraizable]
cong_meet [in Alg.wBIH_not_algebraizable]
cong_trans [in Alg.wBIH_not_algebraizable]
cong_sym [in Alg.wBIH_not_algebraizable]
cong_refl [in Alg.wBIH_not_algebraizable]
contains_one [in Alg.wBIH_not_algebraizable]
D
dresiduation [in Alg.Bi_Heyting_Algebras]d_filter [in Alg.wBIH_not_algebraizable]
E
equiprov [in Alg.sBIH_alg_completeness]equiprov [in Alg.wBIH_alg_completeness]
G
greatest [in Alg.Bi_Heyting_Algebras]J
jabsorp [in Alg.Bi_Heyting_Algebras]jassoc [in Alg.Bi_Heyting_Algebras]
jcomm [in Alg.Bi_Heyting_Algebras]
join [in Alg.Bi_Heyting_Algebras]
L
lowest [in Alg.Bi_Heyting_Algebras]l_filter [in Alg.wBIH_not_algebraizable]
M
mabsorp [in Alg.Bi_Heyting_Algebras]massoc [in Alg.Bi_Heyting_Algebras]
mcomm [in Alg.Bi_Heyting_Algebras]
meet [in Alg.Bi_Heyting_Algebras]
meet_closed [in Alg.wBIH_not_algebraizable]
N
nodes [in Krip.BiInt_Kripke_sem]nodes [in Alg.Bi_Heyting_Algebras]
NotDer [in Krip.wBIH_completeness]
O
one [in Alg.Bi_Heyting_Algebras]P
persist [in Krip.BiInt_Kripke_sem]prim [in Krip.wBIH_completeness]
Prime [in Krip.wBIH_completeness]
R
reachable [in Krip.BiInt_Kripke_sem]reach_tran [in Krip.BiInt_Kripke_sem]
reach_refl [in Krip.BiInt_Kripke_sem]
residuation [in Alg.Bi_Heyting_Algebras]
rpc [in Alg.Bi_Heyting_Algebras]
S
setform [in Alg.sBIH_alg_completeness]setform [in Alg.wBIH_alg_completeness]
Stable [in Krip.wBIH_completeness]
subtr [in Alg.Bi_Heyting_Algebras]
V
val [in Krip.BiInt_Kripke_sem]W
wBIH_closed [in Alg.wBIH_not_algebraizable]Z
zero [in Alg.Bi_Heyting_Algebras]Instance Index
C
CM [in Krip.wBIH_completeness]E
epform_eqprv [in Alg.sBIH_alg_completeness]epform_eqprv [in Alg.wBIH_alg_completeness]
epjoin [in Alg.sBIH_alg_completeness]
epjoin [in Alg.wBIH_alg_completeness]
epmeet [in Alg.sBIH_alg_completeness]
epmeet [in Alg.wBIH_alg_completeness]
epone [in Alg.sBIH_alg_completeness]
epone [in Alg.wBIH_alg_completeness]
eprpc [in Alg.sBIH_alg_completeness]
eprpc [in Alg.wBIH_alg_completeness]
epsubtr [in Alg.sBIH_alg_completeness]
epsubtr [in Alg.wBIH_alg_completeness]
epzero [in Alg.sBIH_alg_completeness]
epzero [in Alg.wBIH_alg_completeness]
L
LindAlg [in Alg.sBIH_alg_completeness]LindAlg [in Alg.wBIH_alg_completeness]
M
M0 [in Krip.BiInt_sem_look_back]M1 [in Krip.BiInt_sem_look_back]
M2 [in Krip.BiInt_sem_look_back]
P
pruned_M [in Krip.sBIH_completeness]Section Index
A
algebraizable [in Alg.sBIH_algebraizable]alg_sem_properties [in Alg.algebraic_semantic]
alg_semantics [in Alg.algebraic_semantic]
B
biHalg_props [in Alg.Bi_Heyting_Algebras]BiInt [in GenHil.sBIH_meta_interactions]
Bisimulation [in Krip.BiInt_bisimulation]
C
Completeness [in Alg.sBIH_alg_completeness]Completeness [in Alg.wBIH_alg_completeness]
congruences [in Alg.wBIH_not_algebraizable]
connect_to_s [in GenHil.wBIH_meta_interactions]
ConseqSoundness [in Krip.BiInt_sem_look_back]
ConseqSoundness.Counterexamples [in Krip.BiInt_sem_look_back]
ConseqSoundness.DefModels [in Krip.BiInt_sem_look_back]
E
Equiprovable_classes [in Alg.sBIH_alg_completeness]Equiprovable_classes [in Alg.wBIH_alg_completeness]
equivalential [in Alg.wBIH_equivalential]
F
filters [in Alg.wBIH_not_algebraizable]I
implicative [in Alg.sBIH_implicative]K
Kripke_semantics [in Krip.BiInt_Kripke_sem]L
LEM_completeness [in Krip.wBIH_completeness]Lindenbaum_algebra [in Alg.sBIH_alg_completeness]
Lindenbaum_algebra [in Alg.wBIH_alg_completeness]
M
model_construction [in Alg.wBIH_no_biHA_alg_sem]N
not_finitely_equivalential [in Alg.wBIH_equivalential]no_isomorphism [in Alg.wBIH_not_algebraizable]
No_biHA_semantics [in Alg.wBIH_no_biHA_alg_sem]
n_Bisimulation [in Krip.BiInt_bisimulation]
P
properties [in GenHil.wBIH_meta_interactions]Properties_eqprv [in Alg.sBIH_alg_completeness]
Properties_eqprv [in Alg.wBIH_alg_completeness]
properties.Bi_Int [in GenHil.wBIH_meta_interactions]
properties.list_conj_stuff [in GenHil.wBIH_meta_interactions]
properties.list_disj_stuff [in GenHil.wBIH_meta_interactions]
properties.remove_stuff [in GenHil.wBIH_meta_interactions]
pruning [in Krip.sBIH_completeness]
S
Soundness [in Alg.alg_soundness]Soundness_LEM [in Krip.BiInt_soundness]
Definition Index
A
AccT_sind [in General.genT]AccT_rec [in General.genT]
AccT_ind [in General.genT]
AccT_rect [in General.genT]
aleq [in Alg.Bi_Heyting_Algebras]
alg_ordconseq [in Alg.algebraic_semantic]
alg_tdconseq [in Alg.algebraic_semantic]
alg_eqconseq [in Alg.algebraic_semantic]
alg_eqconseq_eq [in Alg.algebraic_semantic]
anon [in General.genT]
Axioms_sind [in GenHil.BiInt_GHC]
Axioms_ind [in GenHil.BiInt_GHC]
B
bisimulation [in Krip.BiInt_bisimulation]C
Canon_val [in Krip.wBIH_completeness]Canon_rel [in Krip.wBIH_completeness]
choice_code [in GenHil.BiInt_Lindenbaum_lem]
choice_form [in GenHil.BiInt_Lindenbaum_lem]
closed [in GenHil.BiInt_Lindenbaum_lem]
clos_DN_eq [in Alg.wBIH_equivalential]
complete [in GenHil.BiInt_GHC]
D
depth [in Synt.Syntax]DN_clos_set_sind [in Synt.Syntax]
DN_clos_set_ind [in Synt.Syntax]
DN_form [in Synt.Syntax]
DN_alg [in Alg.Bi_Heyting_Algebras]
E
EqImp [in Alg.sBIH_implicative]Even [in Alg.wBIH_equivalential]
F
finclos_DN_eq [in Alg.wBIH_equivalential]first_zho_lattice_filters [in Alg.wBIH_not_algebraizable]
first_subst [in Synt.Syntax]
ForallTD_forall [in General.genT]
ForallTI_forall [in General.genT]
ForallT_2I [in General.genT]
ForallT_2I' [in General.genT]
ForallT_D2 [in General.genT]
ForallT_D1 [in General.genT]
ForallT_2D [in General.genT]
ForallT_appendI [in General.genT]
ForallT_appendI' [in General.genT]
ForallT_appendD2 [in General.genT]
ForallT_appendD1 [in General.genT]
ForallT_appendD [in General.genT]
ForallT_singleI [in General.genT]
ForallT_singleD [in General.genT]
ForallT_sind [in General.genT]
ForallT_rec [in General.genT]
ForallT_ind [in General.genT]
ForallT_rect [in General.genT]
Forall2T_sind [in General.genT]
Forall2T_rec [in General.genT]
Forall2T_ind [in General.genT]
Forall2T_rect [in General.genT]
form_index [in GenHil.BiInt_enum]
form_index' [in GenHil.BiInt_enum]
form_enum [in GenHil.BiInt_enum]
form_sind [in Synt.Syntax]
form_rec [in Synt.Syntax]
form_ind [in Synt.Syntax]
form_rect [in Synt.Syntax]
G
glob_conseq [in Krip.BiInt_Kripke_sem]H
higher [in Alg.wBIH_not_algebraizable]I
iffT_D2 [in General.genT]iffT_D1 [in General.genT]
iffT_sym [in General.genT]
interp [in Alg.algebraic_semantic]
InT_mapI [in General.genT]
InT_2nd [in General.genT]
InT_sind [in General.genT]
InT_rec [in General.genT]
InT_ind [in General.genT]
InT_rect [in General.genT]
L
len_nodes [in Alg.wBIH_no_biHA_alg_sem]leT_trans [in General.genT]
leT_S_n [in General.genT]
leT_sind [in General.genT]
leT_rec [in General.genT]
leT_ind [in General.genT]
leT_rect [in General.genT]
LindAlgamap [in Alg.sBIH_alg_completeness]
LindAlgamap [in Alg.wBIH_alg_completeness]
list_conj [in Synt.Syntax]
list_disj [in Synt.Syntax]
list_meet [in Alg.Bi_Heyting_Algebras]
lnc [in Alg.wBIH_no_biHA_alg_sem]
loc_conseq [in Krip.BiInt_Kripke_sem]
lower [in Alg.wBIH_not_algebraizable]
L_enum [in GenHil.BiInt_enum]
M
mforces [in Krip.BiInt_Kripke_sem]mult_disj [in GenHil.BiInt_Lindenbaum_lem_prelim]
N
nprime_theory [in GenHil.BiInt_Lindenbaum_lem]n_zz [in Krip.sBIH_completeness]
n_reachable [in Krip.sBIH_completeness]
n_bisimulation [in Krip.BiInt_bisimulation]
O
Odd [in Alg.wBIH_equivalential]P
prime [in GenHil.BiInt_Lindenbaum_lem]prime_theory [in GenHil.BiInt_Lindenbaum_lem]
Q
quasi_prime [in GenHil.BiInt_Lindenbaum_lem]R
relationT [in General.genT]remove_list [in Synt.lems_remove_list]
req [in General.gen]
rls [in General.gen]
rlsT [in General.genT]
rsub [in General.gen]
rsubD [in General.gen]
rsubI [in General.gen]
rsub_imp [in General.gen]
S
sBIH_prv_sind [in GenHil.BiInt_GHC]sBIH_prv_ind [in GenHil.BiInt_GHC]
second_zho_lattice_filters [in Alg.wBIH_not_algebraizable]
sEq [in Alg.sBIH_alg_completeness]
sEq [in Alg.alg_soundness]
sfform_eqprv [in Alg.sBIH_alg_completeness]
sfform_eqprv [in Alg.wBIH_alg_completeness]
sfjoin [in Alg.sBIH_alg_completeness]
sfjoin [in Alg.wBIH_alg_completeness]
sfmeet [in Alg.sBIH_alg_completeness]
sfmeet [in Alg.wBIH_alg_completeness]
sfone [in Alg.sBIH_alg_completeness]
sfone [in Alg.wBIH_alg_completeness]
sfrpc [in Alg.sBIH_alg_completeness]
sfrpc [in Alg.wBIH_alg_completeness]
sfsubtr [in Alg.sBIH_alg_completeness]
sfsubtr [in Alg.wBIH_alg_completeness]
sfzero [in Alg.sBIH_alg_completeness]
sfzero [in Alg.wBIH_alg_completeness]
spair_der [in GenHil.BiInt_GHC]
sSoundness [in Krip.BiInt_soundness]
stable [in GenHil.BiInt_Lindenbaum_lem]
subform [in Synt.Syntax]
subformlist [in Synt.Syntax]
subst [in Synt.Syntax]
s_pruned_val [in Krip.sBIH_completeness]
s_pruned_rel [in Krip.sBIH_completeness]
s_pruned_worlds [in Krip.sBIH_completeness]
s_is_n_reachable [in Krip.sBIH_completeness]
T
three_zho_lattice_filters [in Alg.wBIH_not_algebraizable]TpFq_sind [in Krip.BiInt_sem_look_back]
TpFq_rec [in Krip.BiInt_sem_look_back]
TpFq_ind [in Krip.BiInt_sem_look_back]
TpFq_rect [in Krip.BiInt_sem_look_back]
transitiveT [in General.genT]
U
UDle [in Krip.BiInt_sem_look_back]UDTle [in Krip.BiInt_sem_look_back]
UnDeuxTrois_sind [in Krip.BiInt_sem_look_back]
UnDeuxTrois_rec [in Krip.BiInt_sem_look_back]
UnDeuxTrois_ind [in Krip.BiInt_sem_look_back]
UnDeuxTrois_rect [in Krip.BiInt_sem_look_back]
UnDeux_sind [in Krip.BiInt_sem_look_back]
UnDeux_rec [in Krip.BiInt_sem_look_back]
UnDeux_ind [in Krip.BiInt_sem_look_back]
UnDeux_rect [in Krip.BiInt_sem_look_back]
V
valid_form [in Krip.BiInt_Kripke_sem]val1 [in Krip.BiInt_sem_look_back]
val2 [in Krip.BiInt_sem_look_back]
val3 [in Krip.BiInt_sem_look_back]
vm [in Alg.wBIH_no_biHA_alg_sem]
W
wBIH_prv_sind [in GenHil.BiInt_GHC]wBIH_prv_ind [in GenHil.BiInt_GHC]
well_foundedT [in General.genT]
wforces [in Krip.BiInt_Kripke_sem]
wpair_der [in GenHil.BiInt_GHC]
wSoundness [in Krip.BiInt_soundness]
X
Xmas_lights [in Alg.wBIH_equivalential]Xmas_lightsM [in Alg.wBIH_no_biHA_alg_sem]
Z
zho_alg [in Alg.wBIH_not_algebraizable]zho_leq_sind [in Alg.wBIH_not_algebraizable]
zho_leq_ind [in Alg.wBIH_not_algebraizable]
zho_type_sind [in Alg.wBIH_not_algebraizable]
zho_type_rec [in Alg.wBIH_not_algebraizable]
zho_type_ind [in Alg.wBIH_not_algebraizable]
zho_type_rect [in Alg.wBIH_not_algebraizable]
zw [in Alg.wBIH_no_biHA_alg_sem]
zz [in Krip.sBIH_completeness]
Record Index
B
biHalg [in Alg.Bi_Heyting_Algebras]C
Canon_worlds [in Krip.wBIH_completeness]congruence [in Alg.wBIH_not_algebraizable]
E
eqprv [in Alg.sBIH_alg_completeness]eqprv [in Alg.wBIH_alg_completeness]
L
lattice_filter [in Alg.wBIH_not_algebraizable]M
model [in Krip.BiInt_Kripke_sem]W
wBIH_filter [in Alg.wBIH_not_algebraizable]| 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 | (939 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 | (13 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 | (25 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 | (31 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 | (516 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| 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 | (51 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (46 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 | (21 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 | (37 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 | (173 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |