| 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 | (904 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 | (40 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 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 | (7 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 | (30 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 | (467 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 | (22 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 | (44 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 | (39 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 | (7 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 | (40 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 | (40 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 | (4 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 | (149 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 | (3 entries) |
Global Index
A
absorp_Or1 [lemma, in KM.GHC.properties]additive_cut [lemma, in KM.Sequent.Cut]
aleq [definition, in KM.Algebra.KM_Algebras]
aleq_K [lemma, in KM.Algebra.KM_Algebras]
aleq_antisym [lemma, in KM.Algebra.KM_Algebras]
aleq_refl [lemma, in KM.Algebra.KM_Algebras]
aleq_trans [lemma, in KM.Algebra.KM_Algebras]
algebraic_semantic [library]
algebraizable [section, in KM.Algebra.KMH_algebraizable]
alg_completeness_KMH [lemma, in KM.Algebra.KMH_alg_completeness]
alg_soundness_KMH [lemma, in KM.Algebra.alg_soundness]
alg_sem_properties [section, in KM.Algebra.algebraic_semantic]
alg_eqconseq [definition, in KM.Algebra.algebraic_semantic]
alg_eqconseq_eq [definition, in KM.Algebra.algebraic_semantic]
alg_semantics [section, in KM.Algebra.algebraic_semantic]
alg_MA3 [lemma, in KM.Algebra.KM_Algebras]
alg_MA2 [lemma, in KM.Algebra.KM_Algebras]
alg_MA1 [lemma, in KM.Algebra.KM_Algebras]
alg_A9 [lemma, in KM.Algebra.KM_Algebras]
alg_A8 [lemma, in KM.Algebra.KM_Algebras]
alg_A7 [lemma, in KM.Algebra.KM_Algebras]
alg_A6 [lemma, in KM.Algebra.KM_Algebras]
alg_A5 [lemma, in KM.Algebra.KM_Algebras]
alg_A4 [lemma, in KM.Algebra.KM_Algebras]
alg_A3 [lemma, in KM.Algebra.KM_Algebras]
alg_A2 [lemma, in KM.Algebra.KM_Algebras]
alg_A1 [lemma, in KM.Algebra.KM_Algebras]
alg_soundness [library]
AllForm [definition, in KM.GHC.Lindenbaum_lem]
And [constructor, in KM.Syntax.syntax]
AndL [constructor, in KM.Sequent.Sequents]
AndL_rev [lemma, in KM.Sequent.SequentProps]
AndR [constructor, in KM.Sequent.Sequents]
AndR_rev [lemma, in KM.Sequent.SequentProps]
and_congruence [lemma, in KM.Sequent.Optimizations]
And_Imp [lemma, in KM.GHC.properties]
assoc_And_obj [lemma, in KM.GHC.properties]
Atom [constructor, in KM.Sequent.Sequents]
Ax [constructor, in KM.GHC.KMH]
Axcoreflection [lemma, in KM.GHC.properties]
Axioms [definition, in KM.GHC.KMH]
Axioms_one [lemma, in KM.Algebra.alg_soundness]
Ax_valid [lemma, in KM.Kripke.soundness]
B
Bot [constructor, in KM.Syntax.syntax]bot_not_tautology [lemma, in KM.Sequent.SequentProps]
Box [constructor, in KM.Syntax.syntax]
box [projection, in KM.Algebra.KM_Algebras]
boxone [projection, in KM.Algebra.KM_Algebras]
BoxR [constructor, in KM.Sequent.Sequents]
Box_list [definition, in KM.Syntax.syntax]
Box_distrib_list_Imp [lemma, in KM.GHC.properties]
box_bot_not_tautology [lemma, in KM.Sequent.SequentProps]
box_var_not_tautology [lemma, in KM.Sequent.SequentProps]
box_monot [lemma, in KM.Algebra.KM_Algebras]
C
choice_code [definition, in KM.GHC.Lindenbaum_lem]choice_form [definition, in KM.GHC.Lindenbaum_lem]
choose_impl_top_weight [lemma, in KM.Sequent.Optimizations]
choose_impl_weight [lemma, in KM.Sequent.Optimizations]
choose_impl_sound_R [lemma, in KM.Sequent.Optimizations]
choose_impl_sound_L [lemma, in KM.Sequent.Optimizations]
choose_disj_equiv_R [lemma, in KM.Sequent.Optimizations]
choose_disj_equiv_L [lemma, in KM.Sequent.Optimizations]
choose_disj_sound_L2 [lemma, in KM.Sequent.Optimizations]
choose_disj_sound_L1 [lemma, in KM.Sequent.Optimizations]
choose_conj_equiv_R [lemma, in KM.Sequent.Optimizations]
choose_conj_equiv_L [lemma, in KM.Sequent.Optimizations]
choose_conj_sound_L [lemma, in KM.Sequent.Optimizations]
choose_conj_topL [lemma, in KM.Sequent.Optimizations]
choose_impl [definition, in KM.Sequent.Optimizations]
choose_disj [definition, in KM.Sequent.Optimizations]
choose_conj [definition, in KM.Sequent.Optimizations]
closed [definition, in KM.GHC.Lindenbaum_lem]
comm_Or [lemma, in KM.GHC.properties]
comm_Or_obj [lemma, in KM.GHC.properties]
comm_And_obj [lemma, in KM.GHC.properties]
Completeness [section, in KM.Sequent.Equiv_KMH]
Completeness [section, in KM.Algebra.KMH_alg_completeness]
Completeness.Γ [variable, in KM.Algebra.KMH_alg_completeness]
conjunction [definition, in KM.Sequent.Optimizations]
conjunction_L'' [lemma, in KM.Sequent.Optimizations]
conjunction_R [lemma, in KM.Sequent.Optimizations]
conjunction_L' [lemma, in KM.Sequent.Optimizations]
conjunction_L [lemma, in KM.Sequent.Optimizations]
conjunction_R2 [lemma, in KM.Sequent.Optimizations]
conjunction_R1 [lemma, in KM.Sequent.Optimizations]
Consist_Lind_theory [lemma, in KM.GHC.Lindenbaum_lem]
Consist_nLind_theory [lemma, in KM.GHC.Lindenbaum_lem]
contractionl [lemma, in KM.Sequent.SequentProps]
contractionr [lemma, in KM.Sequent.SequentProps]
Contr_Bot [lemma, in KM.GHC.properties]
coreflec [projection, in KM.Algebra.KM_Algebras]
CountablyManyFormulas [section, in KM.Sequent.syntax_facts]
cut [lemma, in KM.Sequent.Cut]
Cut [library]
D
decidable_is_negation [instance, in KM.Sequent.Environments]decidable_is_implication [instance, in KM.Sequent.Environments]
decidable_is_double_negation [instance, in KM.Sequent.Environments]
decide_in [lemma, in KM.Sequent.Environments]
DecisionProcedure [library]
der_Lind_theory_nLind_theory [lemma, in KM.GHC.Lindenbaum_lem]
der_nLind_theory_mLind_theory_le [lemma, in KM.GHC.Lindenbaum_lem]
difference_include [lemma, in KM.Sequent.Environments]
difference_singleton [lemma, in KM.Sequent.Environments]
diff_not_in [lemma, in KM.Sequent.Environments]
diff_mult [lemma, in KM.Sequent.Environments]
disjunction [definition, in KM.Sequent.Optimizations]
disjunction_R'' [lemma, in KM.Sequent.Optimizations]
disjunction_L'' [lemma, in KM.Sequent.Optimizations]
disjunction_L' [lemma, in KM.Sequent.Optimizations]
disjunction_R [lemma, in KM.Sequent.Optimizations]
disjunction_L [lemma, in KM.Sequent.Optimizations]
distr_join_meet [lemma, in KM.Algebra.KM_Algebras]
distr_meet_join [lemma, in KM.Algebra.KM_Algebras]
double_negation_obviously_smaller [lemma, in KM.Sequent.Optimizations]
double_neg [lemma, in KM.Algebra.KM_Algebras]
E
EFQ [lemma, in KM.GHC.properties]elements_elem_of [lemma, in KM.Sequent.Order]
elements_list_to_set_disj [lemma, in KM.Sequent.Environments]
elements_open_boxes [lemma, in KM.Sequent.Environments]
elements_env_add [lemma, in KM.Sequent.Environments]
elem_of_list_In_1 [lemma, in KM.Sequent.Order]
elem_of_open_boxes [lemma, in KM.Sequent.Environments]
empty [definition, in KM.Sequent.Environments]
empty_not_tautology [lemma, in KM.Sequent.SequentProps]
enum [library]
env [definition, in KM.Sequent.Environments]
Environments [library]
env_pair_order_nil_l [lemma, in KM.Sequent.Order]
env_pair_order_l [lemma, in KM.Sequent.Order]
env_pair_order_refl [definition, in KM.Sequent.Order]
env_pair_order_botf_L [lemma, in KM.Sequent.Order]
env_pair_order_bot_L [lemma, in KM.Sequent.Order]
env_pair_order_bot_R [lemma, in KM.Sequent.Order]
env_order_empty [lemma, in KM.Sequent.Order]
env_order_open_box [lemma, in KM.Sequent.Order]
env_pair_order_cancel_left [lemma, in KM.Sequent.Order]
env_pair_order_cancel_right [lemma, in KM.Sequent.Order]
env_order_le_lt_trans [lemma, in KM.Sequent.Order]
env_order_lt_le_trans [lemma, in KM.Sequent.Order]
env_order_refl_add' [lemma, in KM.Sequent.Order]
env_order_refl_add [lemma, in KM.Sequent.Order]
env_order_refl_cancel_right [lemma, in KM.Sequent.Order]
env_order_cancel_right [lemma, in KM.Sequent.Order]
env_order_cancel_left [lemma, in KM.Sequent.Order]
env_order_cancel_singleton_right [lemma, in KM.Sequent.Order]
env_order_8 [lemma, in KM.Sequent.Order]
env_order_7 [lemma, in KM.Sequent.Order]
env_order_6 [lemma, in KM.Sequent.Order]
env_order_5 [lemma, in KM.Sequent.Order]
env_order_4 [lemma, in KM.Sequent.Order]
env_order_3 [lemma, in KM.Sequent.Order]
env_order_2 [lemma, in KM.Sequent.Order]
env_order_1 [lemma, in KM.Sequent.Order]
env_order_0 [lemma, in KM.Sequent.Order]
env_order_disj_union_compat_strong_left [lemma, in KM.Sequent.Order]
env_order_disj_union_compat_strong_right [lemma, in KM.Sequent.Order]
env_order_refl_disj_union_compat [lemma, in KM.Sequent.Order]
env_order_disj_union_compat [lemma, in KM.Sequent.Order]
env_order_disj_union_compat_right [lemma, in KM.Sequent.Order]
env_order_disj_union_compat_left [lemma, in KM.Sequent.Order]
env_order_add_compat [lemma, in KM.Sequent.Order]
env_order_compat' [lemma, in KM.Sequent.Order]
env_order_compat [lemma, in KM.Sequent.Order]
env_order_equiv_left_compat [lemma, in KM.Sequent.Order]
env_order_equiv_right_compat [lemma, in KM.Sequent.Order]
env_pair_ms_order [definition, in KM.Sequent.Order]
env_pair_order [definition, in KM.Sequent.Order]
env_pair [definition, in KM.Sequent.Order]
env_order_trans [instance, in KM.Sequent.Order]
env_order_self [lemma, in KM.Sequent.Order]
env_order_env_order_refl [lemma, in KM.Sequent.Order]
env_order_refl [definition, in KM.Sequent.Order]
env_order_singleton [lemma, in KM.Sequent.Order]
env_weight_singleton [lemma, in KM.Sequent.Order]
env_order [definition, in KM.Sequent.Order]
env_weight_add [lemma, in KM.Sequent.Order]
env_weight_nil [lemma, in KM.Sequent.Order]
env_weight_app [lemma, in KM.Sequent.Order]
env_weight_disj_union [lemma, in KM.Sequent.Order]
env_weight [definition, in KM.Sequent.Order]
env_equiv_eq [lemma, in KM.Sequent.Environments]
env_add_inv' [lemma, in KM.Sequent.Environments]
env_add_inv [lemma, in KM.Sequent.Environments]
env_add_comm [lemma, in KM.Sequent.Environments]
env_in_add [lemma, in KM.Sequent.Environments]
env_add_remove [lemma, in KM.Sequent.Environments]
env_replace [lemma, in KM.Sequent.Environments]
env_singleton [lemma, in KM.Sequent.Environments]
env_refl [lemma, in KM.Sequent.Environments]
env_weight_0_empty [lemma, in KM.Sequent.Cut]
env_add_non_empty [lemma, in KM.Sequent.SequentProps]
epbox [instance, in KM.Algebra.KMH_alg_completeness]
epboxcoreflec [lemma, in KM.Algebra.KMH_alg_completeness]
epboxlbx [lemma, in KM.Algebra.KMH_alg_completeness]
epboxnextalw [lemma, in KM.Algebra.KMH_alg_completeness]
epboxnormal [lemma, in KM.Algebra.KMH_alg_completeness]
epboxone [lemma, in KM.Algebra.KMH_alg_completeness]
epequiv [definition, in KM.Algebra.KMH_alg_completeness]
epform_eqprv [instance, in KM.Algebra.KMH_alg_completeness]
epgreatest [lemma, in KM.Algebra.KMH_alg_completeness]
epjabsorp [lemma, in KM.Algebra.KMH_alg_completeness]
epjassoc [lemma, in KM.Algebra.KMH_alg_completeness]
epjcomm [lemma, in KM.Algebra.KMH_alg_completeness]
epjoin [instance, in KM.Algebra.KMH_alg_completeness]
eplowest [lemma, in KM.Algebra.KMH_alg_completeness]
epmabsorp [lemma, in KM.Algebra.KMH_alg_completeness]
epmassoc [lemma, in KM.Algebra.KMH_alg_completeness]
epmcomm [lemma, in KM.Algebra.KMH_alg_completeness]
epmeet [instance, in KM.Algebra.KMH_alg_completeness]
epone [instance, in KM.Algebra.KMH_alg_completeness]
epresiduation [lemma, in KM.Algebra.KMH_alg_completeness]
eprpc [instance, in KM.Algebra.KMH_alg_completeness]
eprvbox [lemma, in KM.Algebra.KMH_alg_completeness]
eprvform_eqprv [lemma, in KM.Algebra.KMH_alg_completeness]
eprvjoin [lemma, in KM.Algebra.KMH_alg_completeness]
eprvmeet [lemma, in KM.Algebra.KMH_alg_completeness]
eprvone [lemma, in KM.Algebra.KMH_alg_completeness]
eprvrpc [lemma, in KM.Algebra.KMH_alg_completeness]
eprvzero [lemma, in KM.Algebra.KMH_alg_completeness]
epzero [instance, in KM.Algebra.KMH_alg_completeness]
EqImp2 [definition, in KM.Algebra.KMH_implicative]
EqImp4 [definition, in KM.Algebra.KMH_implicative]
eqprv [record, in KM.Algebra.KMH_alg_completeness]
equiprov [projection, in KM.Algebra.KMH_alg_completeness]
Equiprovable_classes.Γ [variable, in KM.Algebra.KMH_alg_completeness]
Equiprovable_classes [section, in KM.Algebra.KMH_alg_completeness]
equiv [projection, in KM.Algebra.KM_Algebras]
Equivalence [section, in KM.Sequent.Simplifications]
equiv_epequiv [instance, in KM.Algebra.KMH_alg_completeness]
equiv_assoc [instance, in KM.Sequent.Environments]
equiv_disj_union_compat_r [lemma, in KM.Sequent.Environments]
equiv_form_equiv_envF [lemma, in KM.Sequent.Simplifications]
equiv_form_equiv_env [lemma, in KM.Sequent.Simplifications]
equiv_envR_equiv_form [lemma, in KM.Sequent.Simplifications]
equiv_envL_equiv_form [lemma, in KM.Sequent.Simplifications]
equiv_envR_spec [lemma, in KM.Sequent.Simplifications]
equiv_envL_spec [lemma, in KM.Sequent.Simplifications]
equiv_envR_trans [lemma, in KM.Sequent.Simplifications]
equiv_envR_refl [lemma, in KM.Sequent.Simplifications]
equiv_envR [definition, in KM.Sequent.Simplifications]
equiv_envL_trans [lemma, in KM.Sequent.Simplifications]
equiv_envL_refl [lemma, in KM.Sequent.Simplifications]
equiv_envL [definition, in KM.Sequent.Simplifications]
equiv_form [definition, in KM.Sequent.Simplifications]
equiv_equiv [projection, in KM.Algebra.KM_Algebras]
Equiv_KMH [library]
eq_repres_aleq [lemma, in KM.Algebra.KM_Algebras]
ExFalso [constructor, in KM.Sequent.Sequents]
exfalso [lemma, in KM.Sequent.SequentProps]
exists_dec [definition, in KM.Sequent.DecisionProcedure]
Explosion [lemma, in KM.GHC.properties]
Extraction [library]
F
first_subst_idem [lemma, in KM.Syntax.syntax]first_subst [definition, in KM.Syntax.syntax]
first_subst_interp [lemma, in KM.Algebra.algebraic_semantic]
fomula_bottom [instance, in KM.Sequent.syntax_facts]
forall_list_conj [lemma, in KM.GHC.properties]
forall_list_disj [lemma, in KM.GHC.properties]
forces [definition, in KM.Kripke.kripke_sem]
form [inductive, in KM.Syntax.syntax]
form_eq_dec [instance, in KM.Syntax.syntax]
form_sind [definition, in KM.Syntax.syntax]
form_rec [definition, in KM.Syntax.syntax]
form_ind [definition, in KM.Syntax.syntax]
form_rect [definition, in KM.Syntax.syntax]
form_order [definition, in KM.Sequent.syntax_facts]
form_count [instance, in KM.Sequent.syntax_facts]
form_to_gen_tree [definition, in KM.Sequent.syntax_facts]
form_index_inj [lemma, in KM.GHC.enum]
form_enum_index [lemma, in KM.GHC.enum]
form_index [definition, in KM.GHC.enum]
form_index' [definition, in KM.GHC.enum]
form_enum_sur [lemma, in KM.GHC.enum]
form_enum [definition, in KM.GHC.enum]
G
gAx [constructor, in KM.GHC.KMH]GeneralEnvironments [section, in KM.Sequent.Environments]
generalised_contractionr [lemma, in KM.Sequent.SequentProps]
generalised_contractionl [lemma, in KM.Sequent.SequentProps]
generalised_axiom [lemma, in KM.Sequent.SequentProps]
generalised_weakeningrR [lemma, in KM.Sequent.SequentProps]
generalised_weakeningrL_form [lemma, in KM.Sequent.SequentProps]
generalised_weakeningrL [lemma, in KM.Sequent.SequentProps]
generalised_weakeninglR [lemma, in KM.Sequent.SequentProps]
generalised_weakeninglL [lemma, in KM.Sequent.SequentProps]
General_Lind.Lindenbaum_lemma [section, in KM.GHC.Lindenbaum_lem]
General_Lind.PrimeProps [section, in KM.GHC.Lindenbaum_lem]
General_Lind.Prime [section, in KM.GHC.Lindenbaum_lem]
General_Lind.prelims [section, in KM.GHC.Lindenbaum_lem]
General_Lind.Sets_of_forms [section, in KM.GHC.Lindenbaum_lem]
General_Lind [section, in KM.GHC.Lindenbaum_lem]
gen_tree_to_form [definition, in KM.Sequent.syntax_facts]
gId [constructor, in KM.GHC.KMH]
gKMH_id_KMH [lemma, in KM.GHC.same_calcs]
gKMH_prv_sind [definition, in KM.GHC.KMH]
gKMH_prv_ind [definition, in KM.GHC.KMH]
gKMH_prv [inductive, in KM.GHC.KMH]
gKMH_finite [lemma, in KM.GHC.logics]
gKMH_struct [lemma, in KM.GHC.logics]
gKMH_comp [lemma, in KM.GHC.logics]
gKMH_monot [lemma, in KM.GHC.logics]
gKM_Soundness [lemma, in KM.Kripke.soundness]
glb [lemma, in KM.Algebra.KM_Algebras]
glob_conseq [definition, in KM.Kripke.kripke_sem]
gMP [constructor, in KM.GHC.KMH]
gmultiset_elements_list_to_set_disj [lemma, in KM.Sequent.Environments]
gmultiset_rec [lemma, in KM.Sequent.Environments]
gmultiset_choose_or_empty [lemma, in KM.Sequent.Environments]
gNec [constructor, in KM.GHC.KMH]
greatest [projection, in KM.Algebra.KM_Algebras]
G4KM_compl_KMH [lemma, in KM.Sequent.Equiv_KMH]
G4KM_sound_KMH [lemma, in KM.Sequent.Equiv_KMH]
H
height [definition, in KM.Sequent.SequentProps]height_0 [lemma, in KM.Sequent.SequentProps]
high_one [lemma, in KM.Algebra.KM_Algebras]
I
IAxioms [inductive, in KM.GHC.KMH]IAxioms_sind [definition, in KM.GHC.KMH]
IAxioms_ind [definition, in KM.GHC.KMH]
IA1 [constructor, in KM.GHC.KMH]
IA2 [constructor, in KM.GHC.KMH]
IA3 [constructor, in KM.GHC.KMH]
IA4 [constructor, in KM.GHC.KMH]
IA5 [constructor, in KM.GHC.KMH]
IA6 [constructor, in KM.GHC.KMH]
IA7 [constructor, in KM.GHC.KMH]
IA8 [constructor, in KM.GHC.KMH]
IA9 [constructor, in KM.GHC.KMH]
Id [constructor, in KM.GHC.KMH]
IdL_list_disj [lemma, in KM.GHC.properties]
IdL_list_disj_obj [lemma, in KM.GHC.properties]
IdR_list_disj [lemma, in KM.GHC.properties]
IdR_list_disj_obj [lemma, in KM.GHC.properties]
Imp [constructor, in KM.Syntax.syntax]
ImpL [lemma, in KM.Sequent.SequentProps]
ImpLAnd [constructor, in KM.Sequent.Sequents]
ImpLAnd_rev [lemma, in KM.Sequent.SequentProps]
ImpLBox [constructor, in KM.Sequent.Sequents]
ImpLBox_dup [lemma, in KM.Sequent.SequentProps]
ImpLBox_prev [lemma, in KM.Sequent.SequentProps]
implicative [section, in KM.Algebra.KMH_implicative]
ImpLImp [constructor, in KM.Sequent.Sequents]
ImpLImp_prev' [lemma, in KM.Sequent.SequentProps]
ImpLImp_prev [lemma, in KM.Sequent.SequentProps]
ImpLOr [constructor, in KM.Sequent.Sequents]
ImpLOr_rev [lemma, in KM.Sequent.SequentProps]
ImpLVar [constructor, in KM.Sequent.Sequents]
ImpLVar_rev [lemma, in KM.Sequent.SequentProps]
ImpL_dup_contr [lemma, in KM.Sequent.SequentProps]
ImpR [constructor, in KM.Sequent.Sequents]
ImpR_singleton [lemma, in KM.Sequent.SequentProps]
ImpR_revl [lemma, in KM.Sequent.SequentProps]
Imp_list_Imp [lemma, in KM.GHC.properties]
Imp_And [lemma, in KM.GHC.properties]
Imp_trans [lemma, in KM.GHC.properties]
Imp_trans_help427 [lemma, in KM.GHC.properties]
Imp_trans_help410 [lemma, in KM.GHC.properties]
Imp_trans_help170 [lemma, in KM.GHC.properties]
Imp_trans_help54 [lemma, in KM.GHC.properties]
Imp_trans_help37 [lemma, in KM.GHC.properties]
Imp_trans_help35 [lemma, in KM.GHC.properties]
Imp_trans_help14 [lemma, in KM.GHC.properties]
Imp_trans_help9 [lemma, in KM.GHC.properties]
Imp_trans_help8 [lemma, in KM.GHC.properties]
Imp_trans_help7 [lemma, in KM.GHC.properties]
imp_Id_gen [lemma, in KM.GHC.properties]
imp_cut [lemma, in KM.Sequent.SequentProps]
inhab [projection, in KM.Algebra.KMH_alg_completeness]
inhabbox [lemma, in KM.Algebra.KMH_alg_completeness]
inhabform_eqprv [lemma, in KM.Algebra.KMH_alg_completeness]
inhabjoin [lemma, in KM.Algebra.KMH_alg_completeness]
inhabmeet [lemma, in KM.Algebra.KMH_alg_completeness]
inhabone [lemma, in KM.Algebra.KMH_alg_completeness]
inhabrpc [lemma, in KM.Algebra.KMH_alg_completeness]
inhabzero [lemma, in KM.Algebra.KMH_alg_completeness]
interactions [section, in KM.GHC.same_calcs]
interp [definition, in KM.Algebra.algebraic_semantic]
Int_ImpR [lemma, in KM.Sequent.SequentProps]
inverse [definition, in KM.Kripke.kripke_sem]
inv_mreach_wf [projection, in KM.Kripke.kripke_sem]
in_sfform_eqprv [lemma, in KM.Algebra.KMH_alg_completeness]
In_form_dec [instance, in KM.Syntax.syntax]
In_open_boxes' [lemma, in KM.Sequent.Environments]
In_open_boxes [lemma, in KM.Sequent.Environments]
in_rm [lemma, in KM.Sequent.Environments]
in_difference [lemma, in KM.Sequent.Environments]
in_map_ext [lemma, in KM.Sequent.Environments]
in_map_empty [lemma, in KM.Sequent.Environments]
in_map_in [lemma, in KM.Sequent.Environments]
in_subset [definition, in KM.Sequent.Environments]
in_in_map [lemma, in KM.Sequent.Environments]
in_map [definition, in KM.Sequent.Environments]
in_map_aux [definition, in KM.Sequent.Environments]
In_Box_list_In_list [lemma, in KM.GHC.properties]
In_list_In_Box_list [lemma, in KM.GHC.properties]
ireachable [projection, in KM.Kripke.kripke_sem]
ireach_tran [projection, in KM.Kripke.kripke_sem]
ireach_refl [projection, in KM.Kripke.kripke_sem]
irreducible [definition, in KM.Sequent.Environments]
irreflexive_form_order [instance, in KM.Sequent.syntax_facts]
is_box [definition, in KM.Sequent.DecisionProcedure]
is_disj [definition, in KM.Sequent.DecisionProcedure]
is_conj [definition, in KM.Sequent.DecisionProcedure]
is_imp [definition, in KM.Sequent.DecisionProcedure]
is_var [definition, in KM.Sequent.DecisionProcedure]
is_implication_obviously_smaller [lemma, in KM.Sequent.Optimizations]
is_box_weight_open_box [lemma, in KM.Sequent.Environments]
is_not_box_open_box [lemma, in KM.Sequent.Environments]
is_box [definition, in KM.Sequent.Environments]
is_negation [definition, in KM.Sequent.Environments]
is_implication [definition, in KM.Sequent.Environments]
is_double_negation [definition, in KM.Sequent.Environments]
J
jabsorp [projection, in KM.Algebra.KM_Algebras]jassoc [projection, in KM.Algebra.KM_Algebras]
jcomm [projection, in KM.Algebra.KM_Algebras]
join [projection, in KM.Algebra.KM_Algebras]
join_deep [lemma, in KM.Algebra.KM_Algebras]
join_inj2 [lemma, in KM.Algebra.KM_Algebras]
join_inj1 [lemma, in KM.Algebra.KM_Algebras]
join_id [lemma, in KM.Algebra.KM_Algebras]
K
K [constructor, in KM.GHC.KMH]KMalg [record, in KM.Algebra.KM_Algebras]
_ << _ [notation, in KM.Algebra.KM_Algebras]
KMalg_props.KMH [variable, in KM.Algebra.KM_Algebras]
KMalg_props [section, in KM.Algebra.KM_Algebras]
KMH [library]
KMH_Alg4 [lemma, in KM.Algebra.KMH_algebraizable]
KMH_Alg3 [lemma, in KM.Algebra.KMH_algebraizable]
KMH_Alg2 [lemma, in KM.Algebra.KMH_algebraizable]
KMH_Alg1 [lemma, in KM.Algebra.KMH_algebraizable]
KMH_prv_sind [definition, in KM.GHC.KMH]
KMH_prv_ind [definition, in KM.GHC.KMH]
KMH_prv [inductive, in KM.GHC.KMH]
KMH_IL3_Box [lemma, in KM.Algebra.KMH_implicative]
KMH_IL3_Imp [lemma, in KM.Algebra.KMH_implicative]
KMH_IL3_Or [lemma, in KM.Algebra.KMH_implicative]
KMH_IL3_And [lemma, in KM.Algebra.KMH_implicative]
KMH_IL3_Bot [lemma, in KM.Algebra.KMH_implicative]
KMH_IL3_Top [lemma, in KM.Algebra.KMH_implicative]
KMH_IL5 [lemma, in KM.Algebra.KMH_implicative]
KMH_IL4 [lemma, in KM.Algebra.KMH_implicative]
KMH_IL2 [lemma, in KM.Algebra.KMH_implicative]
KMH_IL1 [lemma, in KM.Algebra.KMH_implicative]
KMH_Imp_list_Detachment_Deduction_Theorem [lemma, in KM.GHC.properties]
KMH_Deduction_Theorem [lemma, in KM.GHC.properties]
KMH_Detachment_Theorem [lemma, in KM.GHC.properties]
KMH_finite [lemma, in KM.GHC.logics]
KMH_struct [lemma, in KM.GHC.logics]
KMH_comp [lemma, in KM.GHC.logics]
KMH_monot [lemma, in KM.GHC.logics]
KMH_export [library]
KMH_alg_completeness [library]
KMH_algebraizable [library]
KMH_implicative [library]
KM_simp [definition, in KM.extraction.Extraction]
KM_A [definition, in KM.extraction.Extraction]
KM_E [definition, in KM.extraction.Extraction]
KM_Algebras [library]
kripke_sem [section, in KM.Kripke.kripke_sem]
kripke_sem [library]
kripke_export [library]
K_rule [lemma, in KM.GHC.properties]
K_list_Imp [lemma, in KM.GHC.properties]
L
L [constructor, in KM.GHC.KMH]lbx [projection, in KM.Algebra.KM_Algebras]
LEM [axiom, in KM.Kripke.soundness]
LindAlg [instance, in KM.Algebra.KMH_alg_completeness]
LindAlgamap [definition, in KM.Algebra.KMH_alg_completeness]
LindAlgrepres [lemma, in KM.Algebra.KMH_alg_completeness]
Lindenbaum [lemma, in KM.GHC.Lindenbaum_lem]
Lindenbaum_algebra.Γ [variable, in KM.Algebra.KMH_alg_completeness]
Lindenbaum_algebra [section, in KM.Algebra.KMH_alg_completeness]
Lindenbaum_Tarski_preorder_Bot [lemma, in KM.Sequent.Optimizations]
Lindenbaum_Tarski_preorder [definition, in KM.Sequent.Optimizations]
Lindenbaum_lem [library]
Lind_theory_extens [lemma, in KM.GHC.Lindenbaum_lem]
Lind_theory [definition, in KM.GHC.Lindenbaum_lem]
list_disj_perm [lemma, in KM.Sequent.Equiv_KMH]
list_Imp [definition, in KM.Syntax.syntax]
list_to_set_disj_open_boxes [lemma, in KM.Sequent.Environments]
list_to_set_disj_rm_rev [definition, in KM.Sequent.Environments]
list_to_set_disj_rm [lemma, in KM.Sequent.Environments]
list_to_set_disj_env_add' [lemma, in KM.Sequent.Environments]
list_to_set_disj_env_add [lemma, in KM.Sequent.Environments]
list_disj_in_prv [lemma, in KM.GHC.properties]
list_conj [definition, in KM.GHC.properties]
list_disj_Box [lemma, in KM.GHC.properties]
list_disj_Box_obj [lemma, in KM.GHC.properties]
list_disj_map_Box [lemma, in KM.GHC.properties]
list_disj [definition, in KM.GHC.properties]
lKM_Soundness [lemma, in KM.Kripke.soundness]
loc_conseq [definition, in KM.Kripke.kripke_sem]
logics [library]
logic_props [section, in KM.GHC.logics]
lowest [projection, in KM.Algebra.KM_Algebras]
low_zero [lemma, in KM.Algebra.KM_Algebras]
lub [lemma, in KM.Algebra.KM_Algebras]
L_enum_exhaustive [lemma, in KM.GHC.enum]
L_enum_cumulative [lemma, in KM.GHC.enum]
L_enum [definition, in KM.GHC.enum]
M
mabsorp [projection, in KM.Algebra.KM_Algebras]MakeSimpProps [module, in KM.Sequent.Simplifications]
MakeSimpProps.simp_envR_nil [definition, in KM.Sequent.Simplifications]
MakeSimpProps.simp_envL_nil [definition, in KM.Sequent.Simplifications]
MakeSimpProps.simp_env_pointed_env_order [definition, in KM.Sequent.Simplifications]
MakeSimpProps.simp_envR_pointed_env_order [definition, in KM.Sequent.Simplifications]
MakeSimpProps.simp_envR_env_order [definition, in KM.Sequent.Simplifications]
MakeSimpProps.simp_envL_env_order [definition, in KM.Sequent.Simplifications]
MakeSimpProps.simp_envL_pointed_env_order [definition, in KM.Sequent.Simplifications]
make_impl_complete_R [lemma, in KM.Sequent.Optimizations]
make_impl_complete_L2 [lemma, in KM.Sequent.Optimizations]
make_impl_complete_L [lemma, in KM.Sequent.Optimizations]
make_impl_sound_L2' [lemma, in KM.Sequent.Optimizations]
make_impl_sound_L2 [lemma, in KM.Sequent.Optimizations]
make_impl_sound_R [lemma, in KM.Sequent.Optimizations]
make_impl_sound_L [lemma, in KM.Sequent.Optimizations]
make_disj_complete_R [lemma, in KM.Sequent.Optimizations]
make_disj_sound_R [lemma, in KM.Sequent.Optimizations]
make_disj_complete_L [lemma, in KM.Sequent.Optimizations]
make_disj_sound_L [lemma, in KM.Sequent.Optimizations]
make_disj_equiv_R [lemma, in KM.Sequent.Optimizations]
make_disj_equiv_L [lemma, in KM.Sequent.Optimizations]
make_conj_complete_R [lemma, in KM.Sequent.Optimizations]
make_conj_sound_R [lemma, in KM.Sequent.Optimizations]
make_conj_complete_L [lemma, in KM.Sequent.Optimizations]
make_conj_sound_L [lemma, in KM.Sequent.Optimizations]
make_conj_equiv_R [lemma, in KM.Sequent.Optimizations]
make_conj_equiv_L [lemma, in KM.Sequent.Optimizations]
make_impl [definition, in KM.Sequent.Optimizations]
make_disj [definition, in KM.Sequent.Optimizations]
make_conj [definition, in KM.Sequent.Optimizations]
massoc [projection, in KM.Algebra.KM_Algebras]
MAxioms [inductive, in KM.GHC.KMH]
MAxioms_sind [definition, in KM.GHC.KMH]
MAxioms_ind [definition, in KM.GHC.KMH]
mcomm [projection, in KM.Algebra.KM_Algebras]
meet [projection, in KM.Algebra.KM_Algebras]
meet_deep [lemma, in KM.Algebra.KM_Algebras]
meet_elim2 [lemma, in KM.Algebra.KM_Algebras]
meet_elim1 [lemma, in KM.Algebra.KM_Algebras]
meet_absorp3 [lemma, in KM.Algebra.KM_Algebras]
meet_absorp2 [lemma, in KM.Algebra.KM_Algebras]
meet_absorp1 [lemma, in KM.Algebra.KM_Algebras]
meet_absorp0 [lemma, in KM.Algebra.KM_Algebras]
meet_id [lemma, in KM.Algebra.KM_Algebras]
meta_Imp_trans [lemma, in KM.GHC.properties]
Modal [section, in KM.Sequent.Environments]
model [record, in KM.Kripke.kripke_sem]
monotL_Or [lemma, in KM.GHC.properties]
monotR_Or [lemma, in KM.GHC.properties]
monot_Or2 [lemma, in KM.GHC.properties]
more_for_eq_seq [section, in KM.GHC.properties]
MP [constructor, in KM.GHC.KMH]
MP [lemma, in KM.Sequent.SequentProps]
mp [lemma, in KM.Algebra.KM_Algebras]
mreachable [projection, in KM.Kripke.kripke_sem]
mreach_irrefl [lemma, in KM.Kripke.kripke_sem]
mreach_tran [lemma, in KM.Kripke.kripke_sem]
mreach_irrefl_ireach [projection, in KM.Kripke.kripke_sem]
multeq_meq [lemma, in KM.Sequent.Environments]
N
NA [constructor, in KM.GHC.KMH]Natural_Deduction [section, in KM.GHC.properties]
ND_OrE [lemma, in KM.GHC.properties]
ND_OrI2 [lemma, in KM.GHC.properties]
ND_OrI1 [lemma, in KM.GHC.properties]
ND_AndE2 [lemma, in KM.GHC.properties]
ND_AndE1 [lemma, in KM.GHC.properties]
ND_AndI [lemma, in KM.GHC.properties]
ND_BotE [lemma, in KM.GHC.properties]
Nec [constructor, in KM.GHC.KMH]
Neg [definition, in KM.Syntax.syntax]
next [definition, in KM.Kripke.kripke_sem]
nextalw [projection, in KM.Algebra.KM_Algebras]
nLind_theory_extens_le [lemma, in KM.GHC.Lindenbaum_lem]
nLind_theory_extens [lemma, in KM.GHC.Lindenbaum_lem]
nLind_theory [definition, in KM.GHC.Lindenbaum_lem]
nodes [projection, in KM.Kripke.kripke_sem]
nodes [projection, in KM.Algebra.KM_Algebras]
normal [projection, in KM.Algebra.KM_Algebras]
not_In_Lind_theory_deriv [lemma, in KM.GHC.Lindenbaum_lem]
O
obviously_smaller_top_not_Eq [lemma, in KM.Sequent.Optimizations]obviously_smaller_compatible_GT [lemma, in KM.Sequent.Optimizations]
obviously_smaller_compatible_LT [lemma, in KM.Sequent.Optimizations]
obviously_smaller [definition, in KM.Sequent.Optimizations]
occurs_in [definition, in KM.Sequent.syntax_facts]
occurs_in_make_impl2 [lemma, in KM.Sequent.Optimizations]
occurs_in_make_impl [lemma, in KM.Sequent.Optimizations]
occurs_in_choose_impl [lemma, in KM.Sequent.Optimizations]
occurs_in_make_disj [lemma, in KM.Sequent.Optimizations]
occurs_in_choose_disj [lemma, in KM.Sequent.Optimizations]
occurs_in_make_conj [lemma, in KM.Sequent.Optimizations]
occurs_in_choose_conj [lemma, in KM.Sequent.Optimizations]
occurs_in_map_open_box [lemma, in KM.Sequent.Environments]
occurs_in_open_boxes [lemma, in KM.Sequent.Environments]
one [projection, in KM.Algebra.KM_Algebras]
openboxes_env_order [lemma, in KM.Sequent.Order]
open_boxes_GL_rule [lemma, in KM.Sequent.Equiv_KMH]
open_boxes_env_order [lemma, in KM.Sequent.Order]
open_boxes_remove [lemma, in KM.Sequent.Environments]
open_boxes_add [lemma, in KM.Sequent.Environments]
open_boxes_singleton [lemma, in KM.Sequent.Environments]
open_boxes_disj_union [lemma, in KM.Sequent.Environments]
open_boxes_empty [lemma, in KM.Sequent.Environments]
open_boxes [definition, in KM.Sequent.Environments]
open_box [definition, in KM.Sequent.Environments]
open_boxes_case [lemma, in KM.Sequent.SequentProps]
open_boxes_weakening_L [lemma, in KM.Sequent.SequentProps]
open_boxes_R3 [lemma, in KM.Sequent.SequentProps]
open_boxes_R2 [lemma, in KM.Sequent.SequentProps]
open_boxes_R [lemma, in KM.Sequent.SequentProps]
open_box_L [lemma, in KM.Sequent.SequentProps]
Optimizations [library]
op_disjunction_R [lemma, in KM.Sequent.Optimizations]
Or [constructor, in KM.Syntax.syntax]
Order [library]
ord_resid [lemma, in KM.Algebra.KM_Algebras]
OrL [constructor, in KM.Sequent.Sequents]
OrL_rev [lemma, in KM.Sequent.SequentProps]
OrR [constructor, in KM.Sequent.Sequents]
OrR_idemp [lemma, in KM.Sequent.SequentProps]
OrR_Bot_rev [lemma, in KM.Sequent.SequentProps]
OrR_rev [lemma, in KM.Sequent.SequentProps]
or_congruence [lemma, in KM.Sequent.Optimizations]
Or_imp_assoc [lemma, in KM.GHC.properties]
P
pair_env_equiv [definition, in KM.Sequent.SequentProps]Permutation_rm [lemma, in KM.Sequent.Order]
persist [projection, in KM.Kripke.kripke_sem]
Persistence [lemma, in KM.Kripke.kripke_sem]
pow9_gt_0 [lemma, in KM.Sequent.Order]
prime [definition, in KM.GHC.Lindenbaum_lem]
prime_list_disj [lemma, in KM.GHC.Lindenbaum_lem]
Proof_tree_dec [lemma, in KM.Sequent.DecisionProcedure]
properties [library]
_ ≖ _ [notation, in KM.Algebra.KMH_alg_completeness]
Properties_eqprv.Γ [variable, in KM.Algebra.KMH_alg_completeness]
Properties_eqprv [section, in KM.Algebra.KMH_alg_completeness]
proper_epbox [instance, in KM.Algebra.KMH_alg_completeness]
proper_eprpc [instance, in KM.Algebra.KMH_alg_completeness]
proper_epjoin [instance, in KM.Algebra.KMH_alg_completeness]
proper_epmeet [instance, in KM.Algebra.KMH_alg_completeness]
proper_rm [instance, in KM.Sequent.DecisionProcedure]
Proper_env_order_refl [instance, in KM.Sequent.Order]
Proper_env_order [instance, in KM.Sequent.Order]
Proper_env_order_refl_env_weight [instance, in KM.Sequent.Order]
Proper_env_weight [instance, in KM.Sequent.Order]
proper_Provable [instance, in KM.Sequent.Sequents]
Proper_elements [instance, in KM.Sequent.Environments]
proper_open_boxes [instance, in KM.Sequent.Environments]
proper_difference [instance, in KM.Sequent.Environments]
proper_disj_union [instance, in KM.Sequent.Environments]
proper_elem_of [instance, in KM.Sequent.Environments]
Proper_pair_env [instance, in KM.Sequent.SequentProps]
proper_box [projection, in KM.Algebra.KM_Algebras]
proper_rpc [projection, in KM.Algebra.KM_Algebras]
proper_join [projection, in KM.Algebra.KM_Algebras]
proper_meet [projection, in KM.Algebra.KM_Algebras]
PropQuant [module, in KM.Sequent.PropQuantifiers]
PropQuantifiers [library]
PropQuantProp [module, in KM.Sequent.PropQuantifiers]
PropQuantProp.A_left [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.A_right [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_r [abbreviation, in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_l [abbreviation, in KM.Sequent.PropQuantifiers]
PropQuantProp.A_simp_env [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_l_spec [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_r_vars [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_l_vars [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness [section, in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness.EntailmentCorrect [section, in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness.p [variable, in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness.PropQuantCorrect [section, in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness.VariablesCorrect [section, in KM.Sequent.PropQuantifiers]
PropQuantProp.EA_vars [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.entail_correct [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.E_of_empty [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.E_left [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.e_rule [abbreviation, in KM.Sequent.PropQuantifiers]
PropQuantProp.E_simp_env [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.e_rule_vars [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.KM_uniform_interpolation [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.pq_correct [lemma, in KM.Sequent.PropQuantifiers]
PropQuantProp.PropQuandDef [module, in KM.Sequent.PropQuantifiers]
PropQuantProp.SP [module, in KM.Sequent.PropQuantifiers]
PropQuantProp.vars_incl [definition, in KM.Sequent.PropQuantifiers]
PropQuant.A [definition, in KM.Sequent.PropQuantifiers]
PropQuant.Af [definition, in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_r_cong_strong [lemma, in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_l_cong_strong [lemma, in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_r [definition, in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_l [definition, in KM.Sequent.PropQuantifiers]
PropQuant.E [definition, in KM.Sequent.PropQuantifiers]
PropQuant.EA [definition, in KM.Sequent.PropQuantifiers]
PropQuant.Ef [definition, in KM.Sequent.PropQuantifiers]
PropQuant.e_rule_cong_strong [lemma, in KM.Sequent.PropQuantifiers]
PropQuant.e_rule [definition, in KM.Sequent.PropQuantifiers]
PropQuant.PropQuantDefinition [section, in KM.Sequent.PropQuantifiers]
PropQuant.PropQuantDefinition.p [variable, in KM.Sequent.PropQuantifiers]
PropQuant.WF_pointed_env_order [instance, in KM.Sequent.PropQuantifiers]
Provable [inductive, in KM.Sequent.Sequents]
Provable_dec_of_Prop [lemma, in KM.Sequent.DecisionProcedure]
Provable_dec [lemma, in KM.Sequent.DecisionProcedure]
Provable_sind [definition, in KM.Sequent.Sequents]
Provable_rec [definition, in KM.Sequent.Sequents]
Provable_ind [definition, in KM.Sequent.Sequents]
Provable_rect [definition, in KM.Sequent.Sequents]
prv_list_left_conj [lemma, in KM.GHC.properties]
prv_Top [lemma, in KM.GHC.properties]
Q
quasi_prime_Lind_theory [lemma, in KM.GHC.Lindenbaum_lem]quasi_prime [definition, in KM.GHC.Lindenbaum_lem]
R
remove_In_env_order [lemma, in KM.Sequent.Order]remove_In_env_order_refl [lemma, in KM.Sequent.Order]
remove_env_order [lemma, in KM.Sequent.Order]
remove_include [lemma, in KM.Sequent.Environments]
residuation [projection, in KM.Algebra.KM_Algebras]
restr_closeder_Lind_theory [lemma, in KM.GHC.Lindenbaum_lem]
rm [definition, in KM.Sequent.Environments]
rpc [projection, in KM.Algebra.KM_Algebras]
S
S [module, in KM.Sequent.Simp_env]S [module, in KM.extraction.Extraction]
same_calcs [library]
sEq [definition, in KM.Algebra.KMH_alg_completeness]
sEq [definition, in KM.Algebra.alg_soundness]
SequentProps [library]
Sequents [library]
setform [projection, in KM.Algebra.KMH_alg_completeness]
sfbox [definition, in KM.Algebra.KMH_alg_completeness]
sfform_eqprv [definition, in KM.Algebra.KMH_alg_completeness]
sfjoin [definition, in KM.Algebra.KMH_alg_completeness]
sfmeet [definition, in KM.Algebra.KMH_alg_completeness]
sfone [definition, in KM.Algebra.KMH_alg_completeness]
sfrpc [definition, in KM.Algebra.KMH_alg_completeness]
sfzero [definition, in KM.Algebra.KMH_alg_completeness]
Simplifications [library]
SimpProps [module, in KM.Sequent.Simplifications]
SimpProps.simp_envR_nil [axiom, in KM.Sequent.Simplifications]
SimpProps.simp_envL_nil [axiom, in KM.Sequent.Simplifications]
SimpProps.simp_envR_env_order [axiom, in KM.Sequent.Simplifications]
SimpProps.simp_envL_env_order [axiom, in KM.Sequent.Simplifications]
SimpProps.simp_env_pointed_env_order [axiom, in KM.Sequent.Simplifications]
SimpProps.simp_envR_pointed_env_order [axiom, in KM.Sequent.Simplifications]
SimpProps.simp_envL_pointed_env_order [axiom, in KM.Sequent.Simplifications]
SimpT [module, in KM.Sequent.Simplifications]
SimpT.simp_form_weight [axiom, in KM.Sequent.Simplifications]
SimpT.simp_envR_order [axiom, in KM.Sequent.Simplifications]
SimpT.simp_envL_order [axiom, in KM.Sequent.Simplifications]
SimpT.simp_form [axiom, in KM.Sequent.Simplifications]
SimpT.simp_envR [axiom, in KM.Sequent.Simplifications]
SimpT.simp_envL [axiom, in KM.Sequent.Simplifications]
Simp_env [library]
singleton [instance, in KM.Sequent.Environments]
singletonMS [instance, in KM.Sequent.Environments]
singleton_eq_inv [lemma, in KM.Sequent.Environments]
singleton_mult_notin [lemma, in KM.Sequent.Environments]
singleton_mult_in [lemma, in KM.Sequent.Environments]
Soundness [section, in KM.Sequent.Equiv_KMH]
Soundness [section, in KM.Algebra.alg_soundness]
soundness [section, in KM.Kripke.soundness]
soundness [library]
SoundS [module, in KM.Sequent.Simp_env]
SoundSimpT [module, in KM.Sequent.Simplifications]
SoundSimpT.equiv_envR_vars [axiom, in KM.Sequent.Simplifications]
SoundSimpT.equiv_envL_vars [axiom, in KM.Sequent.Simplifications]
SoundSimpT.equiv_form_simp_form [axiom, in KM.Sequent.Simplifications]
SoundSimpT.equiv_envR_simp_env [axiom, in KM.Sequent.Simplifications]
SoundSimpT.equiv_envL_simp_env [axiom, in KM.Sequent.Simplifications]
SoundSimpT.occurs_in_simp_form [axiom, in KM.Sequent.Simplifications]
SoundSimpT.simp_envR_idempotent [axiom, in KM.Sequent.Simplifications]
SoundSimpT.simp_envL_idempotent [axiom, in KM.Sequent.Simplifications]
SoundS.contextual_simp_form_spec [lemma, in KM.Sequent.Simp_env]
SoundS.Equivalence [section, in KM.Sequent.Simp_env]
SoundS.equiv_envL_vars [lemma, in KM.Sequent.Simp_env]
SoundS.equiv_form_simp_form [lemma, in KM.Sequent.Simp_env]
SoundS.equiv_env_simp_envL [lemma, in KM.Sequent.Simp_env]
SoundS.occurs_in_simp_form [lemma, in KM.Sequent.Simp_env]
SoundS.occurs_in_contextual_simp_form [lemma, in KM.Sequent.Simp_env]
SoundS.simp_envL_idempotent [lemma, in KM.Sequent.Simp_env]
SoundS.Variables [section, in KM.Sequent.Simp_env]
specialised_weakening [lemma, in KM.Sequent.Optimizations]
SPQr [module, in KM.extraction.Extraction]
strongness [lemma, in KM.Sequent.SequentProps]
SubAnd [constructor, in KM.Sequent.syntax_facts]
SubBox [constructor, in KM.Sequent.syntax_facts]
SubEq [constructor, in KM.Sequent.syntax_facts]
subform [definition, in KM.Syntax.syntax]
subformlist [definition, in KM.Syntax.syntax]
subformP [inductive, in KM.Sequent.syntax_facts]
subformP_sind [definition, in KM.Sequent.syntax_facts]
subformP_ind [definition, in KM.Sequent.syntax_facts]
subform_trans [lemma, in KM.Syntax.syntax]
subform_id [lemma, in KM.Syntax.syntax]
SubImpl [constructor, in KM.Sequent.syntax_facts]
SubOr [constructor, in KM.Sequent.syntax_facts]
subst [definition, in KM.Syntax.syntax]
subst_Ax [lemma, in KM.GHC.logics]
SubTheory [definition, in KM.GHC.Lindenbaum_lem]
symmetric_cut [lemma, in KM.Sequent.Cut]
symmetric_equiv_envR [lemma, in KM.Sequent.Simplifications]
symmetric_equiv_envL [lemma, in KM.Sequent.Simplifications]
symmetric_equiv_form [lemma, in KM.Sequent.Simplifications]
syntax [library]
syntax_facts [library]
S.applicable_contextual_simp_form [definition, in KM.Sequent.Simp_env]
S.applicable_strong_weakening [definition, in KM.Sequent.Simp_env]
S.applicable_ImpLOr [definition, in KM.Sequent.Simp_env]
S.applicable_ImpLAnd [definition, in KM.Sequent.Simp_env]
S.applicable_ImpLVar [definition, in KM.Sequent.Simp_env]
S.applicable_OrR [definition, in KM.Sequent.Simp_env]
S.applicable_AndL [definition, in KM.Sequent.Simp_env]
S.contextual_simp_form_weight [lemma, in KM.Sequent.Simp_env]
S.contextual_simp_form [definition, in KM.Sequent.Simp_env]
S.env_weight_provableR [lemma, in KM.Sequent.Simp_env]
S.SimpEnvL [section, in KM.Sequent.Simp_env]
S.SimpEnvR [section, in KM.Sequent.Simp_env]
S.simp_envL_nil [lemma, in KM.Sequent.Simp_env]
S.simp_envL_order [lemma, in KM.Sequent.Simp_env]
S.simp_form_weight [lemma, in KM.Sequent.Simp_env]
S.simp_form [definition, in KM.Sequent.Simp_env]
S.simp_envR_order [lemma, in KM.Sequent.Simp_env]
S.simp_envR_eq [lemma, in KM.Sequent.Simp_env]
S.simp_envR [definition, in KM.Sequent.Simp_env]
S.simp_envL_eq [lemma, in KM.Sequent.Simp_env]
S.simp_envL [definition, in KM.Sequent.Simp_env]
S.sumor_bind3 [definition, in KM.Sequent.Simp_env]
S.sumor_bind2 [definition, in KM.Sequent.Simp_env]
S.sumor_bind1 [definition, in KM.Sequent.Simp_env]
S.sumor_bind0 [definition, in KM.Sequent.Simp_env]
_ • _ (list_scope) [notation, in KM.Sequent.Simp_env]
_ ? _ ⋮₃ _ [notation, in KM.Sequent.Simp_env]
_ ? _ ⋮₂ _ [notation, in KM.Sequent.Simp_env]
_ ? _ ⋮₁ _ [notation, in KM.Sequent.Simp_env]
_ ? _ ⋮₀ _ [notation, in KM.Sequent.Simp_env]
T
tautology_cut [lemma, in KM.Sequent.Optimizations]theorems_and_meta.list_of_conjunctions [section, in KM.GHC.properties]
theorems_and_meta.list_of_disjunctions [section, in KM.GHC.properties]
theorems_and_meta [section, in KM.GHC.properties]
Theory [definition, in KM.GHC.Lindenbaum_lem]
Theory_AllForm [lemma, in KM.GHC.Lindenbaum_lem]
Thm_irrel [lemma, in KM.GHC.properties]
Top [definition, in KM.Syntax.syntax]
Top [instance, in KM.Sequent.Sequents]
TopL_rev [lemma, in KM.Sequent.SequentProps]
top_Provable [lemma, in KM.Sequent.SequentProps]
Top_rpczz [lemma, in KM.Algebra.KM_Algebras]
transitive [lemma, in KM.Algebra.KM_Algebras]
transitive_form_order [instance, in KM.Sequent.syntax_facts]
U
Under_Lind_theory [lemma, in KM.GHC.Lindenbaum_lem]Under_nLind_theory [lemma, in KM.GHC.Lindenbaum_lem]
union_difference_R [lemma, in KM.Sequent.Environments]
union_difference_L [lemma, in KM.Sequent.Environments]
union_mult [lemma, in KM.Sequent.Environments]
V
val [projection, in KM.Kripke.kripke_sem]Var [constructor, in KM.Syntax.syntax]
variable [abbreviation, in KM.Syntax.syntax]
variables_disjunction [lemma, in KM.Sequent.Optimizations]
variables_conjunction [lemma, in KM.Sequent.Optimizations]
var_not_in_env [definition, in KM.Sequent.Environments]
var_not_tautology [lemma, in KM.Sequent.SequentProps]
W
weakeningl [lemma, in KM.Sequent.SequentProps]weakeningr [lemma, in KM.Sequent.SequentProps]
weak_cut [lemma, in KM.Sequent.Optimizations]
weight [definition, in KM.Sequent.syntax_facts]
weight_ind [definition, in KM.Sequent.syntax_facts]
weight_pos [lemma, in KM.Sequent.syntax_facts]
weight_or_bot [lemma, in KM.Sequent.Order]
weight_Box_1 [lemma, in KM.Sequent.Order]
weight_Arrow_1 [lemma, in KM.Sequent.Order]
weight_open_box [lemma, in KM.Sequent.Order]
weight_open_box [lemma, in KM.Sequent.Environments]
weight_tautology [lemma, in KM.Sequent.SequentProps]
wf_env_pair_ms_order [lemma, in KM.Sequent.Order]
wf_pointed_order [lemma, in KM.Sequent.Order]
wf_env_order [definition, in KM.Sequent.Order]
Z
zero [projection, in KM.Algebra.KM_Algebras]other
_ • _ (list_scope) [notation, in KM.Sequent.Order]_ ≼ _ (provability) [notation, in KM.Sequent.Optimizations]
_ ↔ _ [notation, in KM.Syntax.syntax]
_ → _ [notation, in KM.Syntax.syntax]
_ ∨ _ [notation, in KM.Syntax.syntax]
_ ∧ _ [notation, in KM.Syntax.syntax]
_ ⊢? _ [notation, in KM.Sequent.DecisionProcedure]
_ ≺f _ [notation, in KM.Sequent.syntax_facts]
_ ⇢ _ [notation, in KM.Sequent.Optimizations]
_ ⊻ _ [notation, in KM.Sequent.Optimizations]
_ ⊼ _ [notation, in KM.Sequent.Optimizations]
_ ≺· _ [notation, in KM.Sequent.Order]
_ ≼ _ [notation, in KM.Sequent.Order]
_ ≺ _ [notation, in KM.Sequent.Order]
_ ⊢KM _ [notation, in KM.Sequent.Sequents]
_ ⊢ _ [notation, in KM.Sequent.Sequents]
_ • _ [notation, in KM.Sequent.Environments]
_ ≡er _ [notation, in KM.Sequent.Simplifications]
_ ≡el _ [notation, in KM.Sequent.Simplifications]
_ ≡f _ [notation, in KM.Sequent.Simplifications]
_ ≡ _ [notation, in KM.Algebra.KM_Algebras]
# _ [notation, in KM.Syntax.syntax]
¬ _ [notation, in KM.Syntax.syntax]
⊗ _ [notation, in KM.Sequent.Environments]
⊙ _ [notation, in KM.Sequent.Environments]
⊤ [notation, in KM.Syntax.syntax]
⊥ [notation, in KM.Syntax.syntax]
⊥ [notation, in KM.Syntax.syntax]
⋀ [notation, in KM.Sequent.Optimizations]
⋁ [notation, in KM.Sequent.Optimizations]
□ _ [notation, in KM.Syntax.syntax]
□⁻¹ _ [notation, in KM.Sequent.DecisionProcedure]
□⁻¹ _ [notation, in KM.Sequent.Environments]
Notation Index
K
_ << _ [in KM.Algebra.KM_Algebras]P
_ ≖ _ [in KM.Algebra.KMH_alg_completeness]S
_ • _ (list_scope) [in KM.Sequent.Simp_env]_ ? _ ⋮₃ _ [in KM.Sequent.Simp_env]
_ ? _ ⋮₂ _ [in KM.Sequent.Simp_env]
_ ? _ ⋮₁ _ [in KM.Sequent.Simp_env]
_ ? _ ⋮₀ _ [in KM.Sequent.Simp_env]
other
_ • _ (list_scope) [in KM.Sequent.Order]_ ≼ _ (provability) [in KM.Sequent.Optimizations]
_ ↔ _ [in KM.Syntax.syntax]
_ → _ [in KM.Syntax.syntax]
_ ∨ _ [in KM.Syntax.syntax]
_ ∧ _ [in KM.Syntax.syntax]
_ ⊢? _ [in KM.Sequent.DecisionProcedure]
_ ≺f _ [in KM.Sequent.syntax_facts]
_ ⇢ _ [in KM.Sequent.Optimizations]
_ ⊻ _ [in KM.Sequent.Optimizations]
_ ⊼ _ [in KM.Sequent.Optimizations]
_ ≺· _ [in KM.Sequent.Order]
_ ≼ _ [in KM.Sequent.Order]
_ ≺ _ [in KM.Sequent.Order]
_ ⊢KM _ [in KM.Sequent.Sequents]
_ ⊢ _ [in KM.Sequent.Sequents]
_ • _ [in KM.Sequent.Environments]
_ ≡er _ [in KM.Sequent.Simplifications]
_ ≡el _ [in KM.Sequent.Simplifications]
_ ≡f _ [in KM.Sequent.Simplifications]
_ ≡ _ [in KM.Algebra.KM_Algebras]
# _ [in KM.Syntax.syntax]
¬ _ [in KM.Syntax.syntax]
⊗ _ [in KM.Sequent.Environments]
⊙ _ [in KM.Sequent.Environments]
⊤ [in KM.Syntax.syntax]
⊥ [in KM.Syntax.syntax]
⊥ [in KM.Syntax.syntax]
⋀ [in KM.Sequent.Optimizations]
⋁ [in KM.Sequent.Optimizations]
□ _ [in KM.Syntax.syntax]
□⁻¹ _ [in KM.Sequent.DecisionProcedure]
□⁻¹ _ [in KM.Sequent.Environments]
Module Index
M
MakeSimpProps [in KM.Sequent.Simplifications]P
PropQuant [in KM.Sequent.PropQuantifiers]PropQuantProp [in KM.Sequent.PropQuantifiers]
PropQuantProp.PropQuandDef [in KM.Sequent.PropQuantifiers]
PropQuantProp.SP [in KM.Sequent.PropQuantifiers]
S
S [in KM.Sequent.Simp_env]S [in KM.extraction.Extraction]
SimpProps [in KM.Sequent.Simplifications]
SimpT [in KM.Sequent.Simplifications]
SoundS [in KM.Sequent.Simp_env]
SoundSimpT [in KM.Sequent.Simplifications]
SPQr [in KM.extraction.Extraction]
Variable Index
C
Completeness.Γ [in KM.Algebra.KMH_alg_completeness]E
Equiprovable_classes.Γ [in KM.Algebra.KMH_alg_completeness]K
KMalg_props.KMH [in KM.Algebra.KM_Algebras]L
Lindenbaum_algebra.Γ [in KM.Algebra.KMH_alg_completeness]P
Properties_eqprv.Γ [in KM.Algebra.KMH_alg_completeness]PropQuantProp.Correctness.p [in KM.Sequent.PropQuantifiers]
PropQuant.PropQuantDefinition.p [in KM.Sequent.PropQuantifiers]
Library Index
A
algebraic_semanticalg_soundness
C
CutD
DecisionProcedureE
enumEnvironments
Equiv_KMH
Extraction
K
KMHKMH_export
KMH_alg_completeness
KMH_algebraizable
KMH_implicative
KM_Algebras
kripke_sem
kripke_export
L
Lindenbaum_lemlogics
O
OptimizationsOrder
P
propertiesPropQuantifiers
S
same_calcsSequentProps
Sequents
Simplifications
Simp_env
soundness
syntax
syntax_facts
Lemma Index
A
absorp_Or1 [in KM.GHC.properties]additive_cut [in KM.Sequent.Cut]
aleq_K [in KM.Algebra.KM_Algebras]
aleq_antisym [in KM.Algebra.KM_Algebras]
aleq_refl [in KM.Algebra.KM_Algebras]
aleq_trans [in KM.Algebra.KM_Algebras]
alg_completeness_KMH [in KM.Algebra.KMH_alg_completeness]
alg_soundness_KMH [in KM.Algebra.alg_soundness]
alg_MA3 [in KM.Algebra.KM_Algebras]
alg_MA2 [in KM.Algebra.KM_Algebras]
alg_MA1 [in KM.Algebra.KM_Algebras]
alg_A9 [in KM.Algebra.KM_Algebras]
alg_A8 [in KM.Algebra.KM_Algebras]
alg_A7 [in KM.Algebra.KM_Algebras]
alg_A6 [in KM.Algebra.KM_Algebras]
alg_A5 [in KM.Algebra.KM_Algebras]
alg_A4 [in KM.Algebra.KM_Algebras]
alg_A3 [in KM.Algebra.KM_Algebras]
alg_A2 [in KM.Algebra.KM_Algebras]
alg_A1 [in KM.Algebra.KM_Algebras]
AndL_rev [in KM.Sequent.SequentProps]
AndR_rev [in KM.Sequent.SequentProps]
and_congruence [in KM.Sequent.Optimizations]
And_Imp [in KM.GHC.properties]
assoc_And_obj [in KM.GHC.properties]
Axcoreflection [in KM.GHC.properties]
Axioms_one [in KM.Algebra.alg_soundness]
Ax_valid [in KM.Kripke.soundness]
B
bot_not_tautology [in KM.Sequent.SequentProps]Box_distrib_list_Imp [in KM.GHC.properties]
box_bot_not_tautology [in KM.Sequent.SequentProps]
box_var_not_tautology [in KM.Sequent.SequentProps]
box_monot [in KM.Algebra.KM_Algebras]
C
choose_impl_top_weight [in KM.Sequent.Optimizations]choose_impl_weight [in KM.Sequent.Optimizations]
choose_impl_sound_R [in KM.Sequent.Optimizations]
choose_impl_sound_L [in KM.Sequent.Optimizations]
choose_disj_equiv_R [in KM.Sequent.Optimizations]
choose_disj_equiv_L [in KM.Sequent.Optimizations]
choose_disj_sound_L2 [in KM.Sequent.Optimizations]
choose_disj_sound_L1 [in KM.Sequent.Optimizations]
choose_conj_equiv_R [in KM.Sequent.Optimizations]
choose_conj_equiv_L [in KM.Sequent.Optimizations]
choose_conj_sound_L [in KM.Sequent.Optimizations]
choose_conj_topL [in KM.Sequent.Optimizations]
comm_Or [in KM.GHC.properties]
comm_Or_obj [in KM.GHC.properties]
comm_And_obj [in KM.GHC.properties]
conjunction_L'' [in KM.Sequent.Optimizations]
conjunction_R [in KM.Sequent.Optimizations]
conjunction_L' [in KM.Sequent.Optimizations]
conjunction_L [in KM.Sequent.Optimizations]
conjunction_R2 [in KM.Sequent.Optimizations]
conjunction_R1 [in KM.Sequent.Optimizations]
Consist_Lind_theory [in KM.GHC.Lindenbaum_lem]
Consist_nLind_theory [in KM.GHC.Lindenbaum_lem]
contractionl [in KM.Sequent.SequentProps]
contractionr [in KM.Sequent.SequentProps]
Contr_Bot [in KM.GHC.properties]
cut [in KM.Sequent.Cut]
D
decide_in [in KM.Sequent.Environments]der_Lind_theory_nLind_theory [in KM.GHC.Lindenbaum_lem]
der_nLind_theory_mLind_theory_le [in KM.GHC.Lindenbaum_lem]
difference_include [in KM.Sequent.Environments]
difference_singleton [in KM.Sequent.Environments]
diff_not_in [in KM.Sequent.Environments]
diff_mult [in KM.Sequent.Environments]
disjunction_R'' [in KM.Sequent.Optimizations]
disjunction_L'' [in KM.Sequent.Optimizations]
disjunction_L' [in KM.Sequent.Optimizations]
disjunction_R [in KM.Sequent.Optimizations]
disjunction_L [in KM.Sequent.Optimizations]
distr_join_meet [in KM.Algebra.KM_Algebras]
distr_meet_join [in KM.Algebra.KM_Algebras]
double_negation_obviously_smaller [in KM.Sequent.Optimizations]
double_neg [in KM.Algebra.KM_Algebras]
E
EFQ [in KM.GHC.properties]elements_elem_of [in KM.Sequent.Order]
elements_list_to_set_disj [in KM.Sequent.Environments]
elements_open_boxes [in KM.Sequent.Environments]
elements_env_add [in KM.Sequent.Environments]
elem_of_list_In_1 [in KM.Sequent.Order]
elem_of_open_boxes [in KM.Sequent.Environments]
empty_not_tautology [in KM.Sequent.SequentProps]
env_pair_order_nil_l [in KM.Sequent.Order]
env_pair_order_l [in KM.Sequent.Order]
env_pair_order_botf_L [in KM.Sequent.Order]
env_pair_order_bot_L [in KM.Sequent.Order]
env_pair_order_bot_R [in KM.Sequent.Order]
env_order_empty [in KM.Sequent.Order]
env_order_open_box [in KM.Sequent.Order]
env_pair_order_cancel_left [in KM.Sequent.Order]
env_pair_order_cancel_right [in KM.Sequent.Order]
env_order_le_lt_trans [in KM.Sequent.Order]
env_order_lt_le_trans [in KM.Sequent.Order]
env_order_refl_add' [in KM.Sequent.Order]
env_order_refl_add [in KM.Sequent.Order]
env_order_refl_cancel_right [in KM.Sequent.Order]
env_order_cancel_right [in KM.Sequent.Order]
env_order_cancel_left [in KM.Sequent.Order]
env_order_cancel_singleton_right [in KM.Sequent.Order]
env_order_8 [in KM.Sequent.Order]
env_order_7 [in KM.Sequent.Order]
env_order_6 [in KM.Sequent.Order]
env_order_5 [in KM.Sequent.Order]
env_order_4 [in KM.Sequent.Order]
env_order_3 [in KM.Sequent.Order]
env_order_2 [in KM.Sequent.Order]
env_order_1 [in KM.Sequent.Order]
env_order_0 [in KM.Sequent.Order]
env_order_disj_union_compat_strong_left [in KM.Sequent.Order]
env_order_disj_union_compat_strong_right [in KM.Sequent.Order]
env_order_refl_disj_union_compat [in KM.Sequent.Order]
env_order_disj_union_compat [in KM.Sequent.Order]
env_order_disj_union_compat_right [in KM.Sequent.Order]
env_order_disj_union_compat_left [in KM.Sequent.Order]
env_order_add_compat [in KM.Sequent.Order]
env_order_compat' [in KM.Sequent.Order]
env_order_compat [in KM.Sequent.Order]
env_order_equiv_left_compat [in KM.Sequent.Order]
env_order_equiv_right_compat [in KM.Sequent.Order]
env_order_self [in KM.Sequent.Order]
env_order_env_order_refl [in KM.Sequent.Order]
env_order_singleton [in KM.Sequent.Order]
env_weight_singleton [in KM.Sequent.Order]
env_weight_add [in KM.Sequent.Order]
env_weight_nil [in KM.Sequent.Order]
env_weight_app [in KM.Sequent.Order]
env_weight_disj_union [in KM.Sequent.Order]
env_equiv_eq [in KM.Sequent.Environments]
env_add_inv' [in KM.Sequent.Environments]
env_add_inv [in KM.Sequent.Environments]
env_add_comm [in KM.Sequent.Environments]
env_in_add [in KM.Sequent.Environments]
env_add_remove [in KM.Sequent.Environments]
env_replace [in KM.Sequent.Environments]
env_singleton [in KM.Sequent.Environments]
env_refl [in KM.Sequent.Environments]
env_weight_0_empty [in KM.Sequent.Cut]
env_add_non_empty [in KM.Sequent.SequentProps]
epboxcoreflec [in KM.Algebra.KMH_alg_completeness]
epboxlbx [in KM.Algebra.KMH_alg_completeness]
epboxnextalw [in KM.Algebra.KMH_alg_completeness]
epboxnormal [in KM.Algebra.KMH_alg_completeness]
epboxone [in KM.Algebra.KMH_alg_completeness]
epgreatest [in KM.Algebra.KMH_alg_completeness]
epjabsorp [in KM.Algebra.KMH_alg_completeness]
epjassoc [in KM.Algebra.KMH_alg_completeness]
epjcomm [in KM.Algebra.KMH_alg_completeness]
eplowest [in KM.Algebra.KMH_alg_completeness]
epmabsorp [in KM.Algebra.KMH_alg_completeness]
epmassoc [in KM.Algebra.KMH_alg_completeness]
epmcomm [in KM.Algebra.KMH_alg_completeness]
epresiduation [in KM.Algebra.KMH_alg_completeness]
eprvbox [in KM.Algebra.KMH_alg_completeness]
eprvform_eqprv [in KM.Algebra.KMH_alg_completeness]
eprvjoin [in KM.Algebra.KMH_alg_completeness]
eprvmeet [in KM.Algebra.KMH_alg_completeness]
eprvone [in KM.Algebra.KMH_alg_completeness]
eprvrpc [in KM.Algebra.KMH_alg_completeness]
eprvzero [in KM.Algebra.KMH_alg_completeness]
equiv_disj_union_compat_r [in KM.Sequent.Environments]
equiv_form_equiv_envF [in KM.Sequent.Simplifications]
equiv_form_equiv_env [in KM.Sequent.Simplifications]
equiv_envR_equiv_form [in KM.Sequent.Simplifications]
equiv_envL_equiv_form [in KM.Sequent.Simplifications]
equiv_envR_spec [in KM.Sequent.Simplifications]
equiv_envL_spec [in KM.Sequent.Simplifications]
equiv_envR_trans [in KM.Sequent.Simplifications]
equiv_envR_refl [in KM.Sequent.Simplifications]
equiv_envL_trans [in KM.Sequent.Simplifications]
equiv_envL_refl [in KM.Sequent.Simplifications]
eq_repres_aleq [in KM.Algebra.KM_Algebras]
exfalso [in KM.Sequent.SequentProps]
Explosion [in KM.GHC.properties]
F
first_subst_idem [in KM.Syntax.syntax]first_subst_interp [in KM.Algebra.algebraic_semantic]
forall_list_conj [in KM.GHC.properties]
forall_list_disj [in KM.GHC.properties]
form_index_inj [in KM.GHC.enum]
form_enum_index [in KM.GHC.enum]
form_enum_sur [in KM.GHC.enum]
G
generalised_contractionr [in KM.Sequent.SequentProps]generalised_contractionl [in KM.Sequent.SequentProps]
generalised_axiom [in KM.Sequent.SequentProps]
generalised_weakeningrR [in KM.Sequent.SequentProps]
generalised_weakeningrL_form [in KM.Sequent.SequentProps]
generalised_weakeningrL [in KM.Sequent.SequentProps]
generalised_weakeninglR [in KM.Sequent.SequentProps]
generalised_weakeninglL [in KM.Sequent.SequentProps]
gKMH_id_KMH [in KM.GHC.same_calcs]
gKMH_finite [in KM.GHC.logics]
gKMH_struct [in KM.GHC.logics]
gKMH_comp [in KM.GHC.logics]
gKMH_monot [in KM.GHC.logics]
gKM_Soundness [in KM.Kripke.soundness]
glb [in KM.Algebra.KM_Algebras]
gmultiset_elements_list_to_set_disj [in KM.Sequent.Environments]
gmultiset_rec [in KM.Sequent.Environments]
gmultiset_choose_or_empty [in KM.Sequent.Environments]
G4KM_compl_KMH [in KM.Sequent.Equiv_KMH]
G4KM_sound_KMH [in KM.Sequent.Equiv_KMH]
H
height_0 [in KM.Sequent.SequentProps]high_one [in KM.Algebra.KM_Algebras]
I
IdL_list_disj [in KM.GHC.properties]IdL_list_disj_obj [in KM.GHC.properties]
IdR_list_disj [in KM.GHC.properties]
IdR_list_disj_obj [in KM.GHC.properties]
ImpL [in KM.Sequent.SequentProps]
ImpLAnd_rev [in KM.Sequent.SequentProps]
ImpLBox_dup [in KM.Sequent.SequentProps]
ImpLBox_prev [in KM.Sequent.SequentProps]
ImpLImp_prev' [in KM.Sequent.SequentProps]
ImpLImp_prev [in KM.Sequent.SequentProps]
ImpLOr_rev [in KM.Sequent.SequentProps]
ImpLVar_rev [in KM.Sequent.SequentProps]
ImpL_dup_contr [in KM.Sequent.SequentProps]
ImpR_singleton [in KM.Sequent.SequentProps]
ImpR_revl [in KM.Sequent.SequentProps]
Imp_list_Imp [in KM.GHC.properties]
Imp_And [in KM.GHC.properties]
Imp_trans [in KM.GHC.properties]
Imp_trans_help427 [in KM.GHC.properties]
Imp_trans_help410 [in KM.GHC.properties]
Imp_trans_help170 [in KM.GHC.properties]
Imp_trans_help54 [in KM.GHC.properties]
Imp_trans_help37 [in KM.GHC.properties]
Imp_trans_help35 [in KM.GHC.properties]
Imp_trans_help14 [in KM.GHC.properties]
Imp_trans_help9 [in KM.GHC.properties]
Imp_trans_help8 [in KM.GHC.properties]
Imp_trans_help7 [in KM.GHC.properties]
imp_Id_gen [in KM.GHC.properties]
imp_cut [in KM.Sequent.SequentProps]
inhabbox [in KM.Algebra.KMH_alg_completeness]
inhabform_eqprv [in KM.Algebra.KMH_alg_completeness]
inhabjoin [in KM.Algebra.KMH_alg_completeness]
inhabmeet [in KM.Algebra.KMH_alg_completeness]
inhabone [in KM.Algebra.KMH_alg_completeness]
inhabrpc [in KM.Algebra.KMH_alg_completeness]
inhabzero [in KM.Algebra.KMH_alg_completeness]
Int_ImpR [in KM.Sequent.SequentProps]
in_sfform_eqprv [in KM.Algebra.KMH_alg_completeness]
In_open_boxes' [in KM.Sequent.Environments]
In_open_boxes [in KM.Sequent.Environments]
in_rm [in KM.Sequent.Environments]
in_difference [in KM.Sequent.Environments]
in_map_ext [in KM.Sequent.Environments]
in_map_empty [in KM.Sequent.Environments]
in_map_in [in KM.Sequent.Environments]
in_in_map [in KM.Sequent.Environments]
In_Box_list_In_list [in KM.GHC.properties]
In_list_In_Box_list [in KM.GHC.properties]
is_implication_obviously_smaller [in KM.Sequent.Optimizations]
is_box_weight_open_box [in KM.Sequent.Environments]
is_not_box_open_box [in KM.Sequent.Environments]
J
join_deep [in KM.Algebra.KM_Algebras]join_inj2 [in KM.Algebra.KM_Algebras]
join_inj1 [in KM.Algebra.KM_Algebras]
join_id [in KM.Algebra.KM_Algebras]
K
KMH_Alg4 [in KM.Algebra.KMH_algebraizable]KMH_Alg3 [in KM.Algebra.KMH_algebraizable]
KMH_Alg2 [in KM.Algebra.KMH_algebraizable]
KMH_Alg1 [in KM.Algebra.KMH_algebraizable]
KMH_IL3_Box [in KM.Algebra.KMH_implicative]
KMH_IL3_Imp [in KM.Algebra.KMH_implicative]
KMH_IL3_Or [in KM.Algebra.KMH_implicative]
KMH_IL3_And [in KM.Algebra.KMH_implicative]
KMH_IL3_Bot [in KM.Algebra.KMH_implicative]
KMH_IL3_Top [in KM.Algebra.KMH_implicative]
KMH_IL5 [in KM.Algebra.KMH_implicative]
KMH_IL4 [in KM.Algebra.KMH_implicative]
KMH_IL2 [in KM.Algebra.KMH_implicative]
KMH_IL1 [in KM.Algebra.KMH_implicative]
KMH_Imp_list_Detachment_Deduction_Theorem [in KM.GHC.properties]
KMH_Deduction_Theorem [in KM.GHC.properties]
KMH_Detachment_Theorem [in KM.GHC.properties]
KMH_finite [in KM.GHC.logics]
KMH_struct [in KM.GHC.logics]
KMH_comp [in KM.GHC.logics]
KMH_monot [in KM.GHC.logics]
K_rule [in KM.GHC.properties]
K_list_Imp [in KM.GHC.properties]
L
LindAlgrepres [in KM.Algebra.KMH_alg_completeness]Lindenbaum [in KM.GHC.Lindenbaum_lem]
Lindenbaum_Tarski_preorder_Bot [in KM.Sequent.Optimizations]
Lind_theory_extens [in KM.GHC.Lindenbaum_lem]
list_disj_perm [in KM.Sequent.Equiv_KMH]
list_to_set_disj_open_boxes [in KM.Sequent.Environments]
list_to_set_disj_rm [in KM.Sequent.Environments]
list_to_set_disj_env_add' [in KM.Sequent.Environments]
list_to_set_disj_env_add [in KM.Sequent.Environments]
list_disj_in_prv [in KM.GHC.properties]
list_disj_Box [in KM.GHC.properties]
list_disj_Box_obj [in KM.GHC.properties]
list_disj_map_Box [in KM.GHC.properties]
lKM_Soundness [in KM.Kripke.soundness]
low_zero [in KM.Algebra.KM_Algebras]
lub [in KM.Algebra.KM_Algebras]
L_enum_exhaustive [in KM.GHC.enum]
L_enum_cumulative [in KM.GHC.enum]
M
make_impl_complete_R [in KM.Sequent.Optimizations]make_impl_complete_L2 [in KM.Sequent.Optimizations]
make_impl_complete_L [in KM.Sequent.Optimizations]
make_impl_sound_L2' [in KM.Sequent.Optimizations]
make_impl_sound_L2 [in KM.Sequent.Optimizations]
make_impl_sound_R [in KM.Sequent.Optimizations]
make_impl_sound_L [in KM.Sequent.Optimizations]
make_disj_complete_R [in KM.Sequent.Optimizations]
make_disj_sound_R [in KM.Sequent.Optimizations]
make_disj_complete_L [in KM.Sequent.Optimizations]
make_disj_sound_L [in KM.Sequent.Optimizations]
make_disj_equiv_R [in KM.Sequent.Optimizations]
make_disj_equiv_L [in KM.Sequent.Optimizations]
make_conj_complete_R [in KM.Sequent.Optimizations]
make_conj_sound_R [in KM.Sequent.Optimizations]
make_conj_complete_L [in KM.Sequent.Optimizations]
make_conj_sound_L [in KM.Sequent.Optimizations]
make_conj_equiv_R [in KM.Sequent.Optimizations]
make_conj_equiv_L [in KM.Sequent.Optimizations]
meet_deep [in KM.Algebra.KM_Algebras]
meet_elim2 [in KM.Algebra.KM_Algebras]
meet_elim1 [in KM.Algebra.KM_Algebras]
meet_absorp3 [in KM.Algebra.KM_Algebras]
meet_absorp2 [in KM.Algebra.KM_Algebras]
meet_absorp1 [in KM.Algebra.KM_Algebras]
meet_absorp0 [in KM.Algebra.KM_Algebras]
meet_id [in KM.Algebra.KM_Algebras]
meta_Imp_trans [in KM.GHC.properties]
monotL_Or [in KM.GHC.properties]
monotR_Or [in KM.GHC.properties]
monot_Or2 [in KM.GHC.properties]
MP [in KM.Sequent.SequentProps]
mp [in KM.Algebra.KM_Algebras]
mreach_irrefl [in KM.Kripke.kripke_sem]
mreach_tran [in KM.Kripke.kripke_sem]
multeq_meq [in KM.Sequent.Environments]
N
ND_OrE [in KM.GHC.properties]ND_OrI2 [in KM.GHC.properties]
ND_OrI1 [in KM.GHC.properties]
ND_AndE2 [in KM.GHC.properties]
ND_AndE1 [in KM.GHC.properties]
ND_AndI [in KM.GHC.properties]
ND_BotE [in KM.GHC.properties]
nLind_theory_extens_le [in KM.GHC.Lindenbaum_lem]
nLind_theory_extens [in KM.GHC.Lindenbaum_lem]
not_In_Lind_theory_deriv [in KM.GHC.Lindenbaum_lem]
O
obviously_smaller_top_not_Eq [in KM.Sequent.Optimizations]obviously_smaller_compatible_GT [in KM.Sequent.Optimizations]
obviously_smaller_compatible_LT [in KM.Sequent.Optimizations]
occurs_in_make_impl2 [in KM.Sequent.Optimizations]
occurs_in_make_impl [in KM.Sequent.Optimizations]
occurs_in_choose_impl [in KM.Sequent.Optimizations]
occurs_in_make_disj [in KM.Sequent.Optimizations]
occurs_in_choose_disj [in KM.Sequent.Optimizations]
occurs_in_make_conj [in KM.Sequent.Optimizations]
occurs_in_choose_conj [in KM.Sequent.Optimizations]
occurs_in_map_open_box [in KM.Sequent.Environments]
occurs_in_open_boxes [in KM.Sequent.Environments]
openboxes_env_order [in KM.Sequent.Order]
open_boxes_GL_rule [in KM.Sequent.Equiv_KMH]
open_boxes_env_order [in KM.Sequent.Order]
open_boxes_remove [in KM.Sequent.Environments]
open_boxes_add [in KM.Sequent.Environments]
open_boxes_singleton [in KM.Sequent.Environments]
open_boxes_disj_union [in KM.Sequent.Environments]
open_boxes_empty [in KM.Sequent.Environments]
open_boxes_case [in KM.Sequent.SequentProps]
open_boxes_weakening_L [in KM.Sequent.SequentProps]
open_boxes_R3 [in KM.Sequent.SequentProps]
open_boxes_R2 [in KM.Sequent.SequentProps]
open_boxes_R [in KM.Sequent.SequentProps]
open_box_L [in KM.Sequent.SequentProps]
op_disjunction_R [in KM.Sequent.Optimizations]
ord_resid [in KM.Algebra.KM_Algebras]
OrL_rev [in KM.Sequent.SequentProps]
OrR_idemp [in KM.Sequent.SequentProps]
OrR_Bot_rev [in KM.Sequent.SequentProps]
OrR_rev [in KM.Sequent.SequentProps]
or_congruence [in KM.Sequent.Optimizations]
Or_imp_assoc [in KM.GHC.properties]
P
Permutation_rm [in KM.Sequent.Order]Persistence [in KM.Kripke.kripke_sem]
pow9_gt_0 [in KM.Sequent.Order]
prime_list_disj [in KM.GHC.Lindenbaum_lem]
Proof_tree_dec [in KM.Sequent.DecisionProcedure]
PropQuantProp.A_left [in KM.Sequent.PropQuantifiers]
PropQuantProp.A_right [in KM.Sequent.PropQuantifiers]
PropQuantProp.A_simp_env [in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_l_spec [in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_r_vars [in KM.Sequent.PropQuantifiers]
PropQuantProp.a_rule_l_vars [in KM.Sequent.PropQuantifiers]
PropQuantProp.EA_vars [in KM.Sequent.PropQuantifiers]
PropQuantProp.entail_correct [in KM.Sequent.PropQuantifiers]
PropQuantProp.E_of_empty [in KM.Sequent.PropQuantifiers]
PropQuantProp.E_left [in KM.Sequent.PropQuantifiers]
PropQuantProp.E_simp_env [in KM.Sequent.PropQuantifiers]
PropQuantProp.e_rule_vars [in KM.Sequent.PropQuantifiers]
PropQuantProp.KM_uniform_interpolation [in KM.Sequent.PropQuantifiers]
PropQuantProp.pq_correct [in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_r_cong_strong [in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_l_cong_strong [in KM.Sequent.PropQuantifiers]
PropQuant.e_rule_cong_strong [in KM.Sequent.PropQuantifiers]
Provable_dec_of_Prop [in KM.Sequent.DecisionProcedure]
Provable_dec [in KM.Sequent.DecisionProcedure]
prv_list_left_conj [in KM.GHC.properties]
prv_Top [in KM.GHC.properties]
Q
quasi_prime_Lind_theory [in KM.GHC.Lindenbaum_lem]R
remove_In_env_order [in KM.Sequent.Order]remove_In_env_order_refl [in KM.Sequent.Order]
remove_env_order [in KM.Sequent.Order]
remove_include [in KM.Sequent.Environments]
restr_closeder_Lind_theory [in KM.GHC.Lindenbaum_lem]
S
singleton_eq_inv [in KM.Sequent.Environments]singleton_mult_notin [in KM.Sequent.Environments]
singleton_mult_in [in KM.Sequent.Environments]
SoundS.contextual_simp_form_spec [in KM.Sequent.Simp_env]
SoundS.equiv_envL_vars [in KM.Sequent.Simp_env]
SoundS.equiv_form_simp_form [in KM.Sequent.Simp_env]
SoundS.equiv_env_simp_envL [in KM.Sequent.Simp_env]
SoundS.occurs_in_simp_form [in KM.Sequent.Simp_env]
SoundS.occurs_in_contextual_simp_form [in KM.Sequent.Simp_env]
SoundS.simp_envL_idempotent [in KM.Sequent.Simp_env]
specialised_weakening [in KM.Sequent.Optimizations]
strongness [in KM.Sequent.SequentProps]
subform_trans [in KM.Syntax.syntax]
subform_id [in KM.Syntax.syntax]
subst_Ax [in KM.GHC.logics]
symmetric_cut [in KM.Sequent.Cut]
symmetric_equiv_envR [in KM.Sequent.Simplifications]
symmetric_equiv_envL [in KM.Sequent.Simplifications]
symmetric_equiv_form [in KM.Sequent.Simplifications]
S.contextual_simp_form_weight [in KM.Sequent.Simp_env]
S.env_weight_provableR [in KM.Sequent.Simp_env]
S.simp_envL_nil [in KM.Sequent.Simp_env]
S.simp_envL_order [in KM.Sequent.Simp_env]
S.simp_form_weight [in KM.Sequent.Simp_env]
S.simp_envR_order [in KM.Sequent.Simp_env]
S.simp_envR_eq [in KM.Sequent.Simp_env]
S.simp_envL_eq [in KM.Sequent.Simp_env]
T
tautology_cut [in KM.Sequent.Optimizations]Theory_AllForm [in KM.GHC.Lindenbaum_lem]
Thm_irrel [in KM.GHC.properties]
TopL_rev [in KM.Sequent.SequentProps]
top_Provable [in KM.Sequent.SequentProps]
Top_rpczz [in KM.Algebra.KM_Algebras]
transitive [in KM.Algebra.KM_Algebras]
U
Under_Lind_theory [in KM.GHC.Lindenbaum_lem]Under_nLind_theory [in KM.GHC.Lindenbaum_lem]
union_difference_R [in KM.Sequent.Environments]
union_difference_L [in KM.Sequent.Environments]
union_mult [in KM.Sequent.Environments]
V
variables_disjunction [in KM.Sequent.Optimizations]variables_conjunction [in KM.Sequent.Optimizations]
var_not_tautology [in KM.Sequent.SequentProps]
W
weakeningl [in KM.Sequent.SequentProps]weakeningr [in KM.Sequent.SequentProps]
weak_cut [in KM.Sequent.Optimizations]
weight_pos [in KM.Sequent.syntax_facts]
weight_or_bot [in KM.Sequent.Order]
weight_Box_1 [in KM.Sequent.Order]
weight_Arrow_1 [in KM.Sequent.Order]
weight_open_box [in KM.Sequent.Order]
weight_open_box [in KM.Sequent.Environments]
weight_tautology [in KM.Sequent.SequentProps]
wf_env_pair_ms_order [in KM.Sequent.Order]
wf_pointed_order [in KM.Sequent.Order]
Axiom Index
L
LEM [in KM.Kripke.soundness]S
SimpProps.simp_envR_nil [in KM.Sequent.Simplifications]SimpProps.simp_envL_nil [in KM.Sequent.Simplifications]
SimpProps.simp_envR_env_order [in KM.Sequent.Simplifications]
SimpProps.simp_envL_env_order [in KM.Sequent.Simplifications]
SimpProps.simp_env_pointed_env_order [in KM.Sequent.Simplifications]
SimpProps.simp_envR_pointed_env_order [in KM.Sequent.Simplifications]
SimpProps.simp_envL_pointed_env_order [in KM.Sequent.Simplifications]
SimpT.simp_form_weight [in KM.Sequent.Simplifications]
SimpT.simp_envR_order [in KM.Sequent.Simplifications]
SimpT.simp_envL_order [in KM.Sequent.Simplifications]
SimpT.simp_form [in KM.Sequent.Simplifications]
SimpT.simp_envR [in KM.Sequent.Simplifications]
SimpT.simp_envL [in KM.Sequent.Simplifications]
SoundSimpT.equiv_envR_vars [in KM.Sequent.Simplifications]
SoundSimpT.equiv_envL_vars [in KM.Sequent.Simplifications]
SoundSimpT.equiv_form_simp_form [in KM.Sequent.Simplifications]
SoundSimpT.equiv_envR_simp_env [in KM.Sequent.Simplifications]
SoundSimpT.equiv_envL_simp_env [in KM.Sequent.Simplifications]
SoundSimpT.occurs_in_simp_form [in KM.Sequent.Simplifications]
SoundSimpT.simp_envR_idempotent [in KM.Sequent.Simplifications]
SoundSimpT.simp_envL_idempotent [in KM.Sequent.Simplifications]
Constructor Index
A
And [in KM.Syntax.syntax]AndL [in KM.Sequent.Sequents]
AndR [in KM.Sequent.Sequents]
Atom [in KM.Sequent.Sequents]
Ax [in KM.GHC.KMH]
B
Bot [in KM.Syntax.syntax]Box [in KM.Syntax.syntax]
BoxR [in KM.Sequent.Sequents]
E
ExFalso [in KM.Sequent.Sequents]G
gAx [in KM.GHC.KMH]gId [in KM.GHC.KMH]
gMP [in KM.GHC.KMH]
gNec [in KM.GHC.KMH]
I
IA1 [in KM.GHC.KMH]IA2 [in KM.GHC.KMH]
IA3 [in KM.GHC.KMH]
IA4 [in KM.GHC.KMH]
IA5 [in KM.GHC.KMH]
IA6 [in KM.GHC.KMH]
IA7 [in KM.GHC.KMH]
IA8 [in KM.GHC.KMH]
IA9 [in KM.GHC.KMH]
Id [in KM.GHC.KMH]
Imp [in KM.Syntax.syntax]
ImpLAnd [in KM.Sequent.Sequents]
ImpLBox [in KM.Sequent.Sequents]
ImpLImp [in KM.Sequent.Sequents]
ImpLOr [in KM.Sequent.Sequents]
ImpLVar [in KM.Sequent.Sequents]
ImpR [in KM.Sequent.Sequents]
K
K [in KM.GHC.KMH]L
L [in KM.GHC.KMH]M
MP [in KM.GHC.KMH]N
NA [in KM.GHC.KMH]Nec [in KM.GHC.KMH]
O
Or [in KM.Syntax.syntax]OrL [in KM.Sequent.Sequents]
OrR [in KM.Sequent.Sequents]
S
SubAnd [in KM.Sequent.syntax_facts]SubBox [in KM.Sequent.syntax_facts]
SubEq [in KM.Sequent.syntax_facts]
SubImpl [in KM.Sequent.syntax_facts]
SubOr [in KM.Sequent.syntax_facts]
V
Var [in KM.Syntax.syntax]Projection Index
B
box [in KM.Algebra.KM_Algebras]boxone [in KM.Algebra.KM_Algebras]
C
coreflec [in KM.Algebra.KM_Algebras]E
equiprov [in KM.Algebra.KMH_alg_completeness]equiv [in KM.Algebra.KM_Algebras]
equiv_equiv [in KM.Algebra.KM_Algebras]
G
greatest [in KM.Algebra.KM_Algebras]I
inhab [in KM.Algebra.KMH_alg_completeness]inv_mreach_wf [in KM.Kripke.kripke_sem]
ireachable [in KM.Kripke.kripke_sem]
ireach_tran [in KM.Kripke.kripke_sem]
ireach_refl [in KM.Kripke.kripke_sem]
J
jabsorp [in KM.Algebra.KM_Algebras]jassoc [in KM.Algebra.KM_Algebras]
jcomm [in KM.Algebra.KM_Algebras]
join [in KM.Algebra.KM_Algebras]
L
lbx [in KM.Algebra.KM_Algebras]lowest [in KM.Algebra.KM_Algebras]
M
mabsorp [in KM.Algebra.KM_Algebras]massoc [in KM.Algebra.KM_Algebras]
mcomm [in KM.Algebra.KM_Algebras]
meet [in KM.Algebra.KM_Algebras]
mreachable [in KM.Kripke.kripke_sem]
mreach_irrefl_ireach [in KM.Kripke.kripke_sem]
N
nextalw [in KM.Algebra.KM_Algebras]nodes [in KM.Kripke.kripke_sem]
nodes [in KM.Algebra.KM_Algebras]
normal [in KM.Algebra.KM_Algebras]
O
one [in KM.Algebra.KM_Algebras]P
persist [in KM.Kripke.kripke_sem]proper_box [in KM.Algebra.KM_Algebras]
proper_rpc [in KM.Algebra.KM_Algebras]
proper_join [in KM.Algebra.KM_Algebras]
proper_meet [in KM.Algebra.KM_Algebras]
R
residuation [in KM.Algebra.KM_Algebras]rpc [in KM.Algebra.KM_Algebras]
S
setform [in KM.Algebra.KMH_alg_completeness]V
val [in KM.Kripke.kripke_sem]Z
zero [in KM.Algebra.KM_Algebras]Inductive Index
F
form [in KM.Syntax.syntax]G
gKMH_prv [in KM.GHC.KMH]I
IAxioms [in KM.GHC.KMH]K
KMH_prv [in KM.GHC.KMH]M
MAxioms [in KM.GHC.KMH]P
Provable [in KM.Sequent.Sequents]S
subformP [in KM.Sequent.syntax_facts]Section Index
A
algebraizable [in KM.Algebra.KMH_algebraizable]alg_sem_properties [in KM.Algebra.algebraic_semantic]
alg_semantics [in KM.Algebra.algebraic_semantic]
C
Completeness [in KM.Sequent.Equiv_KMH]Completeness [in KM.Algebra.KMH_alg_completeness]
CountablyManyFormulas [in KM.Sequent.syntax_facts]
E
Equiprovable_classes [in KM.Algebra.KMH_alg_completeness]Equivalence [in KM.Sequent.Simplifications]
G
GeneralEnvironments [in KM.Sequent.Environments]General_Lind.Lindenbaum_lemma [in KM.GHC.Lindenbaum_lem]
General_Lind.PrimeProps [in KM.GHC.Lindenbaum_lem]
General_Lind.Prime [in KM.GHC.Lindenbaum_lem]
General_Lind.prelims [in KM.GHC.Lindenbaum_lem]
General_Lind.Sets_of_forms [in KM.GHC.Lindenbaum_lem]
General_Lind [in KM.GHC.Lindenbaum_lem]
I
implicative [in KM.Algebra.KMH_implicative]interactions [in KM.GHC.same_calcs]
K
KMalg_props [in KM.Algebra.KM_Algebras]kripke_sem [in KM.Kripke.kripke_sem]
L
Lindenbaum_algebra [in KM.Algebra.KMH_alg_completeness]logic_props [in KM.GHC.logics]
M
Modal [in KM.Sequent.Environments]more_for_eq_seq [in KM.GHC.properties]
N
Natural_Deduction [in KM.GHC.properties]P
Properties_eqprv [in KM.Algebra.KMH_alg_completeness]PropQuantProp.Correctness [in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness.EntailmentCorrect [in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness.PropQuantCorrect [in KM.Sequent.PropQuantifiers]
PropQuantProp.Correctness.VariablesCorrect [in KM.Sequent.PropQuantifiers]
PropQuant.PropQuantDefinition [in KM.Sequent.PropQuantifiers]
S
Soundness [in KM.Sequent.Equiv_KMH]Soundness [in KM.Algebra.alg_soundness]
soundness [in KM.Kripke.soundness]
SoundS.Equivalence [in KM.Sequent.Simp_env]
SoundS.Variables [in KM.Sequent.Simp_env]
S.SimpEnvL [in KM.Sequent.Simp_env]
S.SimpEnvR [in KM.Sequent.Simp_env]
T
theorems_and_meta.list_of_conjunctions [in KM.GHC.properties]theorems_and_meta.list_of_disjunctions [in KM.GHC.properties]
theorems_and_meta [in KM.GHC.properties]
Instance Index
D
decidable_is_negation [in KM.Sequent.Environments]decidable_is_implication [in KM.Sequent.Environments]
decidable_is_double_negation [in KM.Sequent.Environments]
E
env_order_trans [in KM.Sequent.Order]epbox [in KM.Algebra.KMH_alg_completeness]
epform_eqprv [in KM.Algebra.KMH_alg_completeness]
epjoin [in KM.Algebra.KMH_alg_completeness]
epmeet [in KM.Algebra.KMH_alg_completeness]
epone [in KM.Algebra.KMH_alg_completeness]
eprpc [in KM.Algebra.KMH_alg_completeness]
epzero [in KM.Algebra.KMH_alg_completeness]
equiv_epequiv [in KM.Algebra.KMH_alg_completeness]
equiv_assoc [in KM.Sequent.Environments]
F
fomula_bottom [in KM.Sequent.syntax_facts]form_eq_dec [in KM.Syntax.syntax]
form_count [in KM.Sequent.syntax_facts]
I
In_form_dec [in KM.Syntax.syntax]irreflexive_form_order [in KM.Sequent.syntax_facts]
L
LindAlg [in KM.Algebra.KMH_alg_completeness]P
proper_epbox [in KM.Algebra.KMH_alg_completeness]proper_eprpc [in KM.Algebra.KMH_alg_completeness]
proper_epjoin [in KM.Algebra.KMH_alg_completeness]
proper_epmeet [in KM.Algebra.KMH_alg_completeness]
proper_rm [in KM.Sequent.DecisionProcedure]
Proper_env_order_refl [in KM.Sequent.Order]
Proper_env_order [in KM.Sequent.Order]
Proper_env_order_refl_env_weight [in KM.Sequent.Order]
Proper_env_weight [in KM.Sequent.Order]
proper_Provable [in KM.Sequent.Sequents]
Proper_elements [in KM.Sequent.Environments]
proper_open_boxes [in KM.Sequent.Environments]
proper_difference [in KM.Sequent.Environments]
proper_disj_union [in KM.Sequent.Environments]
proper_elem_of [in KM.Sequent.Environments]
Proper_pair_env [in KM.Sequent.SequentProps]
PropQuant.WF_pointed_env_order [in KM.Sequent.PropQuantifiers]
S
singleton [in KM.Sequent.Environments]singletonMS [in KM.Sequent.Environments]
T
Top [in KM.Sequent.Sequents]transitive_form_order [in KM.Sequent.syntax_facts]
Abbreviation Index
P
PropQuantProp.a_rule_r [in KM.Sequent.PropQuantifiers]PropQuantProp.a_rule_l [in KM.Sequent.PropQuantifiers]
PropQuantProp.e_rule [in KM.Sequent.PropQuantifiers]
V
variable [in KM.Syntax.syntax]Definition Index
A
aleq [in KM.Algebra.KM_Algebras]alg_eqconseq [in KM.Algebra.algebraic_semantic]
alg_eqconseq_eq [in KM.Algebra.algebraic_semantic]
AllForm [in KM.GHC.Lindenbaum_lem]
Axioms [in KM.GHC.KMH]
B
Box_list [in KM.Syntax.syntax]C
choice_code [in KM.GHC.Lindenbaum_lem]choice_form [in KM.GHC.Lindenbaum_lem]
choose_impl [in KM.Sequent.Optimizations]
choose_disj [in KM.Sequent.Optimizations]
choose_conj [in KM.Sequent.Optimizations]
closed [in KM.GHC.Lindenbaum_lem]
conjunction [in KM.Sequent.Optimizations]
D
disjunction [in KM.Sequent.Optimizations]E
empty [in KM.Sequent.Environments]env [in KM.Sequent.Environments]
env_pair_order_refl [in KM.Sequent.Order]
env_pair_ms_order [in KM.Sequent.Order]
env_pair_order [in KM.Sequent.Order]
env_pair [in KM.Sequent.Order]
env_order_refl [in KM.Sequent.Order]
env_order [in KM.Sequent.Order]
env_weight [in KM.Sequent.Order]
epequiv [in KM.Algebra.KMH_alg_completeness]
EqImp2 [in KM.Algebra.KMH_implicative]
EqImp4 [in KM.Algebra.KMH_implicative]
equiv_envR [in KM.Sequent.Simplifications]
equiv_envL [in KM.Sequent.Simplifications]
equiv_form [in KM.Sequent.Simplifications]
exists_dec [in KM.Sequent.DecisionProcedure]
F
first_subst [in KM.Syntax.syntax]forces [in KM.Kripke.kripke_sem]
form_sind [in KM.Syntax.syntax]
form_rec [in KM.Syntax.syntax]
form_ind [in KM.Syntax.syntax]
form_rect [in KM.Syntax.syntax]
form_order [in KM.Sequent.syntax_facts]
form_to_gen_tree [in KM.Sequent.syntax_facts]
form_index [in KM.GHC.enum]
form_index' [in KM.GHC.enum]
form_enum [in KM.GHC.enum]
G
gen_tree_to_form [in KM.Sequent.syntax_facts]gKMH_prv_sind [in KM.GHC.KMH]
gKMH_prv_ind [in KM.GHC.KMH]
glob_conseq [in KM.Kripke.kripke_sem]
H
height [in KM.Sequent.SequentProps]I
IAxioms_sind [in KM.GHC.KMH]IAxioms_ind [in KM.GHC.KMH]
interp [in KM.Algebra.algebraic_semantic]
inverse [in KM.Kripke.kripke_sem]
in_subset [in KM.Sequent.Environments]
in_map [in KM.Sequent.Environments]
in_map_aux [in KM.Sequent.Environments]
irreducible [in KM.Sequent.Environments]
is_box [in KM.Sequent.DecisionProcedure]
is_disj [in KM.Sequent.DecisionProcedure]
is_conj [in KM.Sequent.DecisionProcedure]
is_imp [in KM.Sequent.DecisionProcedure]
is_var [in KM.Sequent.DecisionProcedure]
is_box [in KM.Sequent.Environments]
is_negation [in KM.Sequent.Environments]
is_implication [in KM.Sequent.Environments]
is_double_negation [in KM.Sequent.Environments]
K
KMH_prv_sind [in KM.GHC.KMH]KMH_prv_ind [in KM.GHC.KMH]
KM_simp [in KM.extraction.Extraction]
KM_A [in KM.extraction.Extraction]
KM_E [in KM.extraction.Extraction]
L
LindAlgamap [in KM.Algebra.KMH_alg_completeness]Lindenbaum_Tarski_preorder [in KM.Sequent.Optimizations]
Lind_theory [in KM.GHC.Lindenbaum_lem]
list_Imp [in KM.Syntax.syntax]
list_to_set_disj_rm_rev [in KM.Sequent.Environments]
list_conj [in KM.GHC.properties]
list_disj [in KM.GHC.properties]
loc_conseq [in KM.Kripke.kripke_sem]
L_enum [in KM.GHC.enum]
M
MakeSimpProps.simp_envR_nil [in KM.Sequent.Simplifications]MakeSimpProps.simp_envL_nil [in KM.Sequent.Simplifications]
MakeSimpProps.simp_env_pointed_env_order [in KM.Sequent.Simplifications]
MakeSimpProps.simp_envR_pointed_env_order [in KM.Sequent.Simplifications]
MakeSimpProps.simp_envR_env_order [in KM.Sequent.Simplifications]
MakeSimpProps.simp_envL_env_order [in KM.Sequent.Simplifications]
MakeSimpProps.simp_envL_pointed_env_order [in KM.Sequent.Simplifications]
make_impl [in KM.Sequent.Optimizations]
make_disj [in KM.Sequent.Optimizations]
make_conj [in KM.Sequent.Optimizations]
MAxioms_sind [in KM.GHC.KMH]
MAxioms_ind [in KM.GHC.KMH]
N
Neg [in KM.Syntax.syntax]next [in KM.Kripke.kripke_sem]
nLind_theory [in KM.GHC.Lindenbaum_lem]
O
obviously_smaller [in KM.Sequent.Optimizations]occurs_in [in KM.Sequent.syntax_facts]
open_boxes [in KM.Sequent.Environments]
open_box [in KM.Sequent.Environments]
P
pair_env_equiv [in KM.Sequent.SequentProps]prime [in KM.GHC.Lindenbaum_lem]
PropQuantProp.vars_incl [in KM.Sequent.PropQuantifiers]
PropQuant.A [in KM.Sequent.PropQuantifiers]
PropQuant.Af [in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_r [in KM.Sequent.PropQuantifiers]
PropQuant.a_rule_l [in KM.Sequent.PropQuantifiers]
PropQuant.E [in KM.Sequent.PropQuantifiers]
PropQuant.EA [in KM.Sequent.PropQuantifiers]
PropQuant.Ef [in KM.Sequent.PropQuantifiers]
PropQuant.e_rule [in KM.Sequent.PropQuantifiers]
Provable_sind [in KM.Sequent.Sequents]
Provable_rec [in KM.Sequent.Sequents]
Provable_ind [in KM.Sequent.Sequents]
Provable_rect [in KM.Sequent.Sequents]
Q
quasi_prime [in KM.GHC.Lindenbaum_lem]R
rm [in KM.Sequent.Environments]S
sEq [in KM.Algebra.KMH_alg_completeness]sEq [in KM.Algebra.alg_soundness]
sfbox [in KM.Algebra.KMH_alg_completeness]
sfform_eqprv [in KM.Algebra.KMH_alg_completeness]
sfjoin [in KM.Algebra.KMH_alg_completeness]
sfmeet [in KM.Algebra.KMH_alg_completeness]
sfone [in KM.Algebra.KMH_alg_completeness]
sfrpc [in KM.Algebra.KMH_alg_completeness]
sfzero [in KM.Algebra.KMH_alg_completeness]
subform [in KM.Syntax.syntax]
subformlist [in KM.Syntax.syntax]
subformP_sind [in KM.Sequent.syntax_facts]
subformP_ind [in KM.Sequent.syntax_facts]
subst [in KM.Syntax.syntax]
SubTheory [in KM.GHC.Lindenbaum_lem]
S.applicable_contextual_simp_form [in KM.Sequent.Simp_env]
S.applicable_strong_weakening [in KM.Sequent.Simp_env]
S.applicable_ImpLOr [in KM.Sequent.Simp_env]
S.applicable_ImpLAnd [in KM.Sequent.Simp_env]
S.applicable_ImpLVar [in KM.Sequent.Simp_env]
S.applicable_OrR [in KM.Sequent.Simp_env]
S.applicable_AndL [in KM.Sequent.Simp_env]
S.contextual_simp_form [in KM.Sequent.Simp_env]
S.simp_form [in KM.Sequent.Simp_env]
S.simp_envR [in KM.Sequent.Simp_env]
S.simp_envL [in KM.Sequent.Simp_env]
S.sumor_bind3 [in KM.Sequent.Simp_env]
S.sumor_bind2 [in KM.Sequent.Simp_env]
S.sumor_bind1 [in KM.Sequent.Simp_env]
S.sumor_bind0 [in KM.Sequent.Simp_env]
T
Theory [in KM.GHC.Lindenbaum_lem]Top [in KM.Syntax.syntax]
V
var_not_in_env [in KM.Sequent.Environments]W
weight [in KM.Sequent.syntax_facts]weight_ind [in KM.Sequent.syntax_facts]
wf_env_order [in KM.Sequent.Order]
Record Index
E
eqprv [in KM.Algebra.KMH_alg_completeness]K
KMalg [in KM.Algebra.KM_Algebras]M
model [in KM.Kripke.kripke_sem]| 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 | (904 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 | (40 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 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 | (7 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 | (30 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 | (467 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 | (22 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 | (44 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 | (39 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 | (7 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 | (40 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 | (40 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 | (4 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 | (149 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 | (3 entries) |