| 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 | (2004 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 | (3 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 | (167 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 | (62 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 | (1264 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 | (16 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 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 | (8 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 | (64 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 | (400 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 | (5 entries) |
Global Index
A
absorb [library]absorbs_cut [definition, in absorb]
absorbs_contraction_head [lemma, in absorb]
absorbs_contraction [definition, in absorb]
absorbs_congruence [definition, in absorb]
Absorbtion [section, in absorb]
Absorbtion.L [variable, in absorb]
Absorbtion.op_eq [variable, in absorb]
Absorbtion.V [variable, in absorb]
Absorbtion.v_eq [variable, in absorb]
add [definition, in sets]
add_minus_diag [lemma, in misc]
add_context [definition, in rules]
Admissibility [section, in admissibility]
admissibility [library]
Admissibility.hypotheses [variable, in admissibility]
Admissibility.L [variable, in admissibility]
Admissibility.rules [variable, in admissibility]
Admissibility.V [variable, in admissibility]
admissible [definition, in admissibility]
admissible_depth_preserving_admissible [lemma, in admissibility]
admissible_prop [lemma, in admissibility]
admissible_rule_set [definition, in admissibility]
admissible_bounded_cut_prop_G [lemma, in propositional_properties]
all [library]
all_true_model [definition, in propositional_completeness]
and_n_subset_G_n [lemma, in rule_sets]
and_rule_no_simple_modal_conclusion [lemma, in rule_sets]
and_oracle_some [lemma, in build_prop_proof]
and_oracle [definition, in build_prop_proof]
and_oracle_tcc [lemma, in build_prop_proof]
and_rule_no_empty_conclusion [lemma, in rules]
and_rule_context [lemma, in rules]
append_single_rev [lemma, in lists]
apply_assoc_map_flatten [lemma, in assoc]
apply_assoc_map_append [lemma, in assoc]
apply_assoc_map_support [lemma, in assoc]
apply_assoc_map [definition, in assoc]
apply_propositional_subproofs [definition, in propositional_completeness]
arity [projection, in formulas]
assoc [definition, in assoc]
Assoc [section, in assoc]
assoc [library]
assoc_map_pair [lemma, in assoc]
assoc_swap_pairs [lemma, in assoc]
Assoc_2.aeq [variable, in assoc]
Assoc_2.A [variable, in assoc]
Assoc_2 [section, in assoc]
assoc_disjoint_keys_right_tail [lemma, in assoc]
assoc_disjoint_keys [definition, in assoc]
assoc_In_rev [lemma, in assoc]
assoc_In [lemma, in assoc]
assoc_rassoc_inj_some [lemma, in assoc]
assoc_mapping_cons_first [lemma, in assoc]
assoc_mapping_tail [lemma, in assoc]
assoc_mapping_cons [constructor, in assoc]
assoc_mapping_nil [constructor, in assoc]
assoc_mapping [inductive, in assoc]
assoc_map_split [lemma, in assoc]
assoc_append_split [lemma, in assoc]
assoc_rassoc_some [lemma, in assoc]
assoc_cons_tail [lemma, in assoc]
assoc_cons_first [lemma, in assoc]
assoc_cons_split [lemma, in assoc]
assoc_mapping_join_subst_maps [lemma, in factor_two_subst]
assoc_mapping_rename_disjoint [lemma, in factor_two_subst]
assoc_mapping_rename_disjoint_ind [lemma, in factor_two_subst]
Assoc.A [variable, in assoc]
Assoc.aeq [variable, in assoc]
Assoc.B [variable, in assoc]
Assoc.beq [variable, in assoc]
assume [constructor, in formulas]
assumptions [projection, in formulas]
assumption_add_context_interpretation [lemma, in propositional_sound]
assumption_add_context_state_seq_semantics [lemma, in sound]
ax_n_subset_G_n [lemma, in rule_sets]
ax_rule_no_simple_modal_conclusion [lemma, in rule_sets]
ax_oracle_some [lemma, in build_prop_proof]
ax_oracle [definition, in build_prop_proof]
ax_oracle_tcc [lemma, in build_prop_proof]
ax_rule_subst [lemma, in rules]
ax_rule_no_empty_conclusion [lemma, in rules]
a_list_prop_first_or [lemma, in some_neg_form]
a_list_prop_tail [lemma, in some_neg]
a_list_prop_head [definition, in some_neg]
a_list_prop [definition, in some_neg]
B
backward_substitution [library]back_subst_result [definition, in backward_substitution]
Back_subst.v_eq [variable, in backward_substitution]
Back_subst.L [variable, in backward_substitution]
Back_subst.V [variable, in backward_substitution]
Back_subst [section, in backward_substitution]
bare_inverted_neg_rule [definition, in rules]
bare_inverted_and_right_rule [definition, in rules]
bare_inverted_and_left_rule [definition, in rules]
bare_neg_neg_rule [definition, in rules]
bare_neg_and_rule [definition, in rules]
bare_and_rule [definition, in rules]
bcontrapositive [lemma, in misc]
bounded_head_weakening_admissible_GRC_n [lemma, in weakening]
bounded_head_weakening_admissible_cut [lemma, in weakening]
bounded_head_weakening_admissible_R [lemma, in weakening]
bounded_head_weakening_admissible_G_n_ind [lemma, in weakening]
bounded_head_weakening_admissible_G_n_step [lemma, in weakening]
bounded_head_weakening_admissible_neg_neg [lemma, in weakening]
bounded_head_weakening_admissible_neg_and [lemma, in weakening]
bounded_head_weakening_admissible_and [lemma, in weakening]
bounded_head_weakening_admissible_ax [lemma, in weakening]
bounded_weakening_provable_subst_n_conclusions [lemma, in weakening]
bounded_full_weakening [lemma, in rules]
bounded_weakening_closed_empty [lemma, in rules]
bounded_weakening_closed [definition, in rules]
bounded_weakening_rules_multiset [lemma, in rules]
bounded_weakening_rules [definition, in rules]
bounded_cut_rules [definition, in rules]
box [definition, in k_syntax]
box_v [definition, in k_syntax]
box_op [constructor, in k_syntax]
box_v_sequent_semantics_char [lemma, in k_semantics]
box_semantics [lemma, in k_semantics]
build_neg_neg_rule [definition, in build_prop_proof]
build_neg_and_rule [definition, in build_prop_proof]
build_and_rule [definition, in build_prop_proof]
build_ax_rule [definition, in build_prop_proof]
Build_prop_proof.v_eq [variable, in build_prop_proof]
Build_prop_proof.L [variable, in build_prop_proof]
Build_prop_proof.V [variable, in build_prop_proof]
Build_prop_proof [section, in build_prop_proof]
build_proof_right_property [lemma, in build_proof]
build_proof_right_result [lemma, in build_proof]
build_proof [definition, in build_proof]
Build_proof.hypotheses [variable, in build_proof]
Build_proof.rules [variable, in build_proof]
Build_proof.L [variable, in build_proof]
Build_proof.V [variable, in build_proof]
Build_proof [section, in build_proof]
build_counter_model_correct [lemma, in propositional_completeness]
build_counter_model_const_v [lemma, in propositional_completeness]
build_counter_model_const_v_ind [lemma, in propositional_completeness]
build_counter_model [definition, in propositional_completeness]
build_prop_proof [library]
build_proof [library]
C
cast [library]change_rules_provability [lemma, in formulas]
change_rules_hyp_provability [lemma, in formulas]
change_form_provable_subst_n_conclusion [lemma, in inversion]
change_sequent_provable_subst_n_conclusion [lemma, in inversion]
CK [section, in ck]
ck [library]
ck_functor [definition, in ck]
CK.fun_ext [variable, in ck]
CK.pred_ext [variable, in ck]
classic [library]
Classical_sets.A [variable, in classic]
Classical_sets [section, in classic]
classical_logic [definition, in classic]
classic_axiom_sound_contraction [lemma, in classic]
classic_axiom_sound_cut_right [lemma, in classic]
classic_axiom_sound_cut_left [lemma, in classic]
classic_axiom_neg_disjunction_other_case [lemma, in classic]
classic_axiom_neg_and_or [lemma, in classic]
coalg [projection, in semantics]
codom_map_cast [lemma, in cast]
collect_var_chain_ends_correct [lemma, in factor_subst]
collect_var_chain_ends_correct_ind [lemma, in factor_subst]
collect_var_chain_ends [definition, in factor_subst]
complete [library]
completeness [lemma, in complete]
Completeness [section, in complete]
Completeness.L [variable, in complete]
Completeness.T [variable, in complete]
Completeness.V [variable, in complete]
Completeness.v_eq [variable, in complete]
comp_law [projection, in functor]
conclusion [projection, in formulas]
congruence_assumptions_provable_with_ax [lemma, in absorb]
congruence_assumptions_subset [lemma, in absorb]
congruence_assumptions_char [lemma, in absorb]
congruence_assumptions [definition, in absorb]
congruence_assumption_list [definition, in absorb]
conj_right_head_Gn_admissible [lemma, in inversion]
conj_left_head_Gn_admissible [lemma, in inversion]
conj_head_inversion_closed [definition, in inversion]
const_rank_G_set [lemma, in rule_sets]
const_rank_GR [lemma, in weakening]
const_rank_R [lemma, in weakening]
const_rank_cut_rule_right [lemma, in rules]
const_rank_cut_rule_left [lemma, in rules]
const_rank_neg_neg_rule_context [lemma, in rules]
const_rank_neg_neg_rule [lemma, in rules]
const_rank_neg_and_rule_context [lemma, in rules]
const_rank_neg_and_rule [lemma, in rules]
const_rank_and_rule_right_context [lemma, in rules]
const_rank_and_rule_left_context [lemma, in rules]
const_rank_and_rule [lemma, in rules]
const_rank_add_context [lemma, in rules]
cons_nth_skipn [lemma, in lists]
context_inverted_neg_rule [lemma, in rules]
context_inverted_and_right_rule [lemma, in rules]
context_inverted_and_left_rule [lemma, in rules]
context_neg_neg_rule [lemma, in rules]
context_neg_and_rule [lemma, in rules]
context_and_rule [lemma, in rules]
contraction [library]
contraction_rule_multiset [lemma, in rules]
Contraction_ind.v_eq [variable, in contraction]
Contraction_ind.op_eq [variable, in contraction]
Contraction_ind.L [variable, in contraction]
Contraction_ind.V [variable, in contraction]
Contraction_ind [section, in contraction]
contrapositive [lemma, in misc]
correct_rule_inductive_G [lemma, in propositional_completeness]
countably_infinite_non_empty [lemma, in misc]
countably_infinite [definition, in misc]
counted_prop_list_valuation_semantics [lemma, in semantics]
counted_prop_list_valuation_tcc_irr [lemma, in semantics]
counted_prop_list_valuation [definition, in semantics]
counted_list_equal [lemma, in misc]
counted_0_destruction [lemma, in misc]
counted_list_eta_1 [lemma, in misc]
counted_list_eta [lemma, in misc]
counted_map [definition, in misc]
counted_head [definition, in misc]
counted_cons [constructor, in misc]
counted_nil [constructor, in misc]
counted_list [inductive, in misc]
coval [projection, in semantics]
cutout_nth_cons_succ [lemma, in lists]
cutout_nth_cons_0 [lemma, in lists]
cutout_nth [definition, in lists]
Cut_properties.L [variable, in cut_properties]
Cut_properties.V [variable, in cut_properties]
Cut_properties [section, in cut_properties]
cut_rule_multiset [lemma, in rules]
cut_elimination_osr_context [lemma, in generic_cut]
cut_admissibile_from_head_elim [lemma, in generic_cut]
cut_free_completeness [lemma, in complete]
cut_properties [library]
C_n_subset_GC_n [lemma, in rule_sets]
D
decompose_G_n_set [lemma, in rule_sets]decompose_G_n_set_coarsly [lemma, in rule_sets]
decrease_rank_R [lemma, in weakening]
delete_depth_admissible_rule [lemma, in admissibility]
depth_admissible_prop [lemma, in admissibility]
depth_preserving_admissible_rule_set [definition, in admissibility]
depth_preserving_admissible [definition, in admissibility]
dep_conj [constructor, in misc]
dep_and [inductive, in misc]
dep_list_of_every_nth [definition, in dep_lists]
dep_list_proj_left_dep_map [lemma, in dep_lists]
dep_list_proj_left [definition, in dep_lists]
dep_map_dep_dep [definition, in dep_lists]
dep_map_dep_const [definition, in dep_lists]
dep_map_const_dep [definition, in dep_lists]
dep_nth [definition, in dep_lists]
dep_cons [constructor, in dep_lists]
dep_nil [constructor, in dep_lists]
dep_list [inductive, in dep_lists]
dep_prop [definition, in dep_lists]
Dep_lists.T [variable, in dep_lists]
Dep_lists.A [variable, in dep_lists]
Dep_lists [section, in dep_lists]
dep_append_right [lemma, in some_neg]
dep_append_left [lemma, in some_neg]
dep_lists [library]
destruct_neg_mod_sequent [lemma, in k_syntax]
destruct_neg_mod_form [lemma, in k_syntax]
destruct_mod_sequent [lemma, in k_syntax]
destruct_mod_form [lemma, in k_syntax]
destruct_neg_sequent [lemma, in k_syntax]
de_morgan_neg_and [lemma, in classic]
direct_image_left_adjoint [lemma, in image]
direct_img [definition, in image]
disj_head_inversion_closed [definition, in inversion]
divide_subst_prop [lemma, in factor_subst]
divide_subst [definition, in factor_subst]
dneg_or_elim [lemma, in misc]
dneg_or_intro [lemma, in misc]
dneg_or [definition, in misc]
dneg_form_maybe [definition, in prop_mod]
dom_map_cast [lemma, in cast]
double_neg_impl_neg_or [lemma, in misc]
double_set_inverse [lemma, in sets]
double_set_inverse_rev [lemma, in classic]
double_neg_or [lemma, in classic]
downward_correct_GRC [lemma, in sound]
downward_correct_GR [lemma, in sound]
downward_correct_contraction [lemma, in sound]
downward_correct_one_step_rule [lemma, in sound]
downward_correct_rule_strengthen [definition, in sound]
downward_correct_rule_set [definition, in sound]
downward_correct_rule [definition, in sound]
dprop_or_mod_sequent [definition, in prop_mod]
dprop_or_mod_formula [definition, in prop_mod]
dset [definition, in dsets]
dsets [library]
dunion [definition, in dsets]
E
empty_sequent_set [definition, in formulas]empty_set [definition, in sets]
enumerator [definition, in misc]
enum_infinite [definition, in misc]
enum_elem [definition, in misc]
eq_unequal [lemma, in misc]
eq_equal [lemma, in misc]
eq_type [definition, in misc]
evar_bug_list_weakening_admissible_GRC_n [lemma, in weakening]
every_nth_of_dep_list [lemma, in dep_lists]
every_nth_exists_inv [lemma, in dep_lists]
every_nth_exists_apply [lemma, in dep_lists]
every_nth_exists [lemma, in dep_lists]
every_dep_nth_dep_map_const [lemma, in dep_lists]
every_dep_nth_tail [lemma, in dep_lists]
every_dep_nth_head [lemma, in dep_lists]
every_dep_nth_cons [lemma, in dep_lists]
every_dep_nth_empty [lemma, in dep_lists]
every_dep_nth [definition, in dep_lists]
every_nth_list_reorder [lemma, in reorder]
every_nth_map [lemma, in lists]
every_nth_cutout_nth [lemma, in lists]
every_nth_In_rev [lemma, in lists]
every_nth_In [lemma, in lists]
every_nth_append_right [lemma, in lists]
every_nth_append_left [lemma, in lists]
every_nth_append [lemma, in lists]
every_nth_cons [lemma, in lists]
every_nth_tail [lemma, in lists]
every_nth_head [lemma, in lists]
every_nth_mono [lemma, in lists]
every_nth_empty [lemma, in lists]
every_nth [definition, in lists]
every_nth_list_support [lemma, in list_support]
every_nth_sequent_support [lemma, in sequent_support]
excluded_middle [lemma, in classic]
exists_not_not_implies [lemma, in misc]
F
factor_subst_property [lemma, in factor_subst]factor_subst [definition, in factor_subst]
Factor_subst.v_eq [variable, in factor_subst]
Factor_subst.op_eq [variable, in factor_subst]
Factor_subst.L [variable, in factor_subst]
Factor_subst.V [variable, in factor_subst]
Factor_subst [section, in factor_subst]
factor_two_subst_property [lemma, in factor_two_subst]
factor_two_subst_equal_2 [lemma, in factor_two_subst]
factor_two_subst [definition, in factor_two_subst]
Factor_two_subst.v_eq [variable, in factor_two_subst]
Factor_two_subst.op_eq [variable, in factor_two_subst]
Factor_two_subst.L [variable, in factor_two_subst]
Factor_two_subst.V [variable, in factor_two_subst]
Factor_two_subst [section, in factor_two_subst]
factor_subst [library]
factor_two_subst [library]
fcompose [definition, in misc]
fcompose [definition, in functions]
feq_ftimes_right [lemma, in functions]
feq_ftimes_left [lemma, in functions]
feq_ftimes_both [lemma, in functions]
feq_ftimes_compose_pair [lemma, in functions]
feq_ftimes_compose [lemma, in functions]
feq_ftimes_id [lemma, in functions]
feq_pair_right [lemma, in functions]
feq_pair_left [lemma, in functions]
feq_pair_both [lemma, in functions]
feq_pair_proj [lemma, in functions]
feq_right_compose_right [lemma, in functions]
feq_right_compose_left [lemma, in functions]
feq_left_compose_right [lemma, in functions]
feq_left_compose_left [lemma, in functions]
feq_compose_right_both [lemma, in functions]
feq_compose_left_both [lemma, in functions]
feq_compose_both [lemma, in functions]
feq_compose_associative_reverse [lemma, in functions]
feq_compose_associative [lemma, in functions]
feq_id_right [lemma, in functions]
feq_id_left [lemma, in functions]
feq_rw_r [lemma, in functions]
feq_eq [lemma, in functions]
feq_symmetric [lemma, in functions]
feq_transitive [lemma, in functions]
feq_reflexive [lemma, in functions]
feq_terminal_seq_cone [lemma, in slice]
feq_slice_final_map_coval [lemma, in slice]
feq_slice_map_T_compose [lemma, in slice]
feq_slice_map_T [lemma, in slice]
feq_direct_img [lemma, in image]
fibred_semantics [projection, in semantics]
fibred_intersection [lemma, in image]
fibred_set_inverse [lemma, in image]
final_map_prop [lemma, in functions]
final_map [definition, in functions]
find_neg_neg_none [lemma, in build_prop_proof]
find_neg_neg_some [lemma, in build_prop_proof]
find_neg_neg [definition, in build_prop_proof]
find_neg_neg_tcc_neg [lemma, in build_prop_proof]
find_neg_neg_tcc_neg_neg [lemma, in build_prop_proof]
find_neg_and_none [lemma, in build_prop_proof]
find_neg_and_some [lemma, in build_prop_proof]
find_neg_and [definition, in build_prop_proof]
find_neg_and_tcc_is_and [lemma, in build_prop_proof]
find_neg_and_tcc_is_neg [lemma, in build_prop_proof]
find_and_none [lemma, in build_prop_proof]
find_and_some [lemma, in build_prop_proof]
find_and [definition, in build_prop_proof]
find_trivial_none [lemma, in build_prop_proof]
find_trivial_none_ind [lemma, in build_prop_proof]
find_trivial_some [lemma, in build_prop_proof]
find_trivial_some_ind [lemma, in build_prop_proof]
find_trivial [definition, in build_prop_proof]
firstn_firstn_less [lemma, in lists]
firstn_append_right [lemma, in lists]
firstn_append_left [lemma, in lists]
firstn_whole [lemma, in lists]
fix_var_chain_ends_no_ends [lemma, in factor_subst]
fix_var_chain_ends [definition, in factor_subst]
flatten [definition, in lists]
flatten_map_singleton_id [lemma, in lists]
flatten_append [lemma, in lists]
fmap [projection, in functor]
fmap_feq_law [projection, in functor]
fold_left_map [lemma, in lists]
forallb_every_nth [lemma, in lists]
forallb_cons [lemma, in lists]
forall_not_iff_not_exists [lemma, in misc]
Formulas [section, in formulas]
formulas [library]
Formulas.L [variable, in formulas]
Formulas.V [variable, in formulas]
formula_measure_char [lemma, in formulas]
formula_measure [definition, in formulas]
formula_counter_model_correct [lemma, in propositional_completeness]
formula_counter_model [definition, in propositional_completeness]
form_semantics_subst_change_coval [lemma, in semantics]
form_semantics_false [lemma, in semantics]
form_semantics_char [lemma, in semantics]
form_semantics [definition, in semantics]
form_prop_or_formula_of_sequent_iter [lemma, in some_neg_form]
ftimes [definition, in functions]
ftimes_def [lemma, in functions]
full_subset_full [lemma, in sets]
full_set_full [lemma, in sets]
full_set [definition, in sets]
full_weakening_rules_nonempty_conclusion [lemma, in rules]
full_weakening_closed [definition, in rules]
full_weakening_rules_multiset [lemma, in rules]
full_weakening_rules [definition, in rules]
functions [library]
function_update_split_result [lemma, in misc]
function_update_split [lemma, in misc]
function_update_twice [lemma, in misc]
function_update_unequal [lemma, in misc]
function_update_eq [lemma, in misc]
function_update [definition, in misc]
function_equal [definition, in functions]
functor [record, in functor]
functor [library]
fun_codom_cast [definition, in cast]
fun_dom_cast [definition, in cast]
G
GC_n_subset_GRC_n [lemma, in rule_sets]GC_n_as_G_C_union [lemma, in rule_sets]
GC_n_multiset [lemma, in rule_sets]
GC_n_set [definition, in rule_sets]
GC_multiset [lemma, in rule_sets]
GC_set [definition, in rule_sets]
generic_bounded_list_weakening [lemma, in weakening]
generic_substitution_lemma [lemma, in cut_properties]
Generic_cut.L [variable, in generic_cut]
Generic_cut.V [variable, in generic_cut]
Generic_cut [section, in generic_cut]
generic_cut [library]
get_modal_args [definition, in formulas]
get_and_forms [definition, in formulas]
get_neg_form [definition, in formulas]
get_prop_var [definition, in formulas]
ge_refl [lemma, in misc]
GRC_n_as_GR_C_union [lemma, in rule_sets]
GRC_n_set_empty [lemma, in rule_sets]
GRC_n_set_struct_union [lemma, in rule_sets]
GRC_n_set_wo_ax_multiset [lemma, in rule_sets]
GRC_n_set_wo_ax [definition, in rule_sets]
GRC_n_multiset [lemma, in rule_sets]
GRC_n_set [definition, in rule_sets]
GRC_set_struct_union [lemma, in rule_sets]
GRC_set_wo_ax_multiset [lemma, in rule_sets]
GRC_set_wo_ax [definition, in rule_sets]
GRC_multiset [lemma, in rule_sets]
GRC_set [definition, in rule_sets]
GRC_n_substitution_lemma [lemma, in cut_properties]
GRC_1_is_GC_1 [lemma, in propositional_rules]
GR_n_subset_GRC_n [lemma, in rule_sets]
GR_subset_GRC [lemma, in rule_sets]
GR_n_set_struct_union [lemma, in rule_sets]
GR_n_multiset [lemma, in rule_sets]
GR_n_set [definition, in rule_sets]
GR_set_no_empty_conclusion [lemma, in rule_sets]
GR_set_struct_union [lemma, in rule_sets]
GR_set_wo_ax_multiset [lemma, in rule_sets]
GR_set_wo_ax [definition, in rule_sets]
GR_multiset [lemma, in rule_sets]
GR_set [definition, in rule_sets]
GR_n_provable_with_premises [lemma, in weakening]
GR_n_substitution_lemma_empty_hyp [lemma, in cut_properties]
GR_n_substitution_lemma [lemma, in cut_properties]
GR_n_non_atomic_axiom_head [lemma, in absorb]
GR_1_is_G_prop [lemma, in propositional_rules]
G_n_subset_GRC_n [lemma, in rule_sets]
G_n_subset_GR_n [lemma, in rule_sets]
G_subset_GR [lemma, in rule_sets]
G_n_subset_GC_n [lemma, in rule_sets]
G_n_set_no_simple_modal_conclusion [lemma, in rule_sets]
G_n_set_mono [lemma, in rule_sets]
G_n_multiset [lemma, in rule_sets]
G_n_set [definition, in rule_sets]
G_set_no_empty_conclusion [lemma, in rule_sets]
G_rules_no_simple_modal_conclusion [lemma, in rule_sets]
G_multiset [lemma, in rule_sets]
G_struct_multiset [lemma, in rule_sets]
G_set_struct_union [lemma, in rule_sets]
G_set [definition, in rule_sets]
G_struct_set [definition, in rule_sets]
G_set_prop_set [lemma, in propositional_rules]
G_n_cut_elim_head_neg_neg_outside [lemma, in propositional_properties]
G_n_cut_elim_head_neg_and_outside [lemma, in propositional_properties]
G_n_cut_elim_head_and_outside [lemma, in propositional_properties]
G_n_cut_elim_head_neg_neg_inside [lemma, in propositional_properties]
G_n_cut_elim_head_neg_and_inside [lemma, in propositional_properties]
G_n_cut_elim_head_and_inside [lemma, in propositional_properties]
G_n_cut_elim_head_ax [lemma, in propositional_properties]
G_n_hyp_list_contraction_left [lemma, in propositional_properties]
G_n_contraction_head [lemma, in propositional_properties]
G_n_contraction_neg_neg_assumptions_head [lemma, in propositional_properties]
G_n_contraction_neg_and_assumptions_head [lemma, in propositional_properties]
G_n_contraction_and_assumptions_head [lemma, in propositional_properties]
G_n_contraction_head_ax [lemma, in propositional_properties]
G_non_atomic_axiom_head [lemma, in propositional_properties]
H
head_inversion_provable_subst_n_conclusion [lemma, in inversion]head_inversion_closed_empty [lemma, in inversion]
head_inversion_closed [definition, in inversion]
head_contraction_closed_empty [lemma, in propositional_properties]
head_contraction_closed [definition, in propositional_properties]
head_contraction_closed_provable_subst_n_conclusions_ind [lemma, in contraction]
hypotheses_oracle_type [definition, in build_proof]
I
id [definition, in functions]id_law [projection, in functor]
id_subst [definition, in substitution]
iff_and [lemma, in misc]
iff_neg [lemma, in misc]
iff_left [lemma, in misc]
iff_right [lemma, in misc]
Image [section, in image]
image [library]
Image.A [variable, in image]
Image.B [variable, in image]
incl_assoc_some [lemma, in assoc]
incl_prop_var_formula_sequent [lemma, in formulas]
incl_flatten_every [lemma, in list_set]
incl_rev [lemma, in list_set]
incl_list_reorder [lemma, in list_set]
incl_lappr [lemma, in list_set]
incl_lappl [lemma, in list_set]
incl_left_tail [lemma, in list_set]
incl_empty [lemma, in list_set]
injective [definition, in misc]
injective_assoc_tail [lemma, in assoc]
injective_assoc_append [lemma, in assoc]
injective_assoc_cons_rassoc [lemma, in assoc]
injective_assoc_cons_different [lemma, in assoc]
injective_assoc_empty [lemma, in assoc]
injective_assoc [definition, in assoc]
injective_neg_box_v [lemma, in k_syntax]
injective_subst_of_fixed_map [lemma, in factor_subst]
injective_assoc_fix_var_chain_ends [lemma, in factor_subst]
injective_subst_neg_simple_modal [lemma, in modal_formulas]
injective_subst_simple_modal [lemma, in modal_formulas]
injective_subst_prop_form [lemma, in modal_formulas]
injective_assoc_join_subst_maps [lemma, in factor_two_subst]
injective_assoc_rename_disjoint [lemma, in factor_two_subst]
injective_assoc_rename_disjoint_ind [lemma, in factor_two_subst]
intersection [definition, in sets]
intersection_complement [lemma, in sets]
Inversion [section, in inversion]
inversion [library]
inversion_rules_nonempty_conclusion [lemma, in rules]
inversion_rules_multiset [lemma, in rules]
inversion_rules [definition, in rules]
inversion_admissible_GR [lemma, in inversion]
inversion_admissible_GR_n [lemma, in inversion]
inversion_admissible_Gn_H [lemma, in inversion]
inversion_depth_preserving_admissible_Gn_H [lemma, in inversion]
Inversion.L [variable, in inversion]
Inversion.V [variable, in inversion]
Inversion.v_eq [variable, in inversion]
inverted_neg_rule_context [lemma, in rules]
inverted_neg_rule [definition, in rules]
inverted_or_rule_multiset [definition, in rules]
inverted_or_left_reordered_rule [lemma, in rules]
inverted_or_rule [definition, in rules]
inverted_and_right_rule_context [lemma, in rules]
inverted_and_right_rule [definition, in rules]
inverted_and_left_rule_context [lemma, in rules]
inverted_and_left_rule [definition, in rules]
inv_proj_full [lemma, in image]
inv_img_compose [lemma, in image]
inv_img_id [lemma, in image]
inv_img [definition, in image]
In_apply_assoc_map_destruct [lemma, in assoc]
In_apply_assoc_map_non_member [lemma, in assoc]
In_apply_assoc_map_member [lemma, in assoc]
In_prop_var_sequent [lemma, in formulas]
In_remove_other [lemma, in lists]
In_nth_rev [lemma, in lists]
In_nth [lemma, in lists]
in_map_reverse [lemma, in lists]
In_flatten [lemma, in lists]
in_combine_same [lemma, in lists]
is_inr [definition, in misc]
is_inl [definition, in misc]
is_none [definition, in misc]
is_some [definition, in misc]
is_neg_neg [definition, in build_prop_proof]
is_neg_and [definition, in build_prop_proof]
is_negated_prop [definition, in build_prop_proof]
is_modal [definition, in formulas]
is_and [definition, in formulas]
is_neg [definition, in formulas]
is_prop [definition, in formulas]
is_full_set [definition, in sets]
is_contraction_rule [definition, in rules]
is_cut_rule [definition, in rules]
is_neg_neg_rule [definition, in rules]
is_neg_and_rule [definition, in rules]
is_and_rule [definition, in rules]
is_ax_rule [definition, in rules]
is_prop_model_or [lemma, in propositional_models]
is_prop_model_false [lemma, in propositional_models]
is_prop_model_tcc_irr [lemma, in propositional_models]
is_prop_model [definition, in propositional_models]
iter_fmap_T [definition, in slice]
iter_obj_T_S_n [lemma, in slice]
iter_obj_T [definition, in slice]
J
join_subst_maps_equal_second_map [lemma, in factor_two_subst]join_subst_maps_contains_second_vars [lemma, in factor_two_subst]
join_subst_maps_correct_second_map [lemma, in factor_two_subst]
join_subst_maps_equal_first_map [lemma, in factor_two_subst]
join_subst_maps_contains_first_vars [lemma, in factor_two_subst]
join_subst_maps_subst_char [lemma, in factor_two_subst]
join_subst_maps [definition, in factor_two_subst]
K
KL [definition, in k_syntax]kop_eq [definition, in k_syntax]
KV [definition, in k_syntax]
kv_eq [definition, in k_syntax]
kv_enum [definition, in k_syntax]
k_n_rule_eq_1 [lemma, in k_nd]
k_nd_subset [lemma, in k_nd]
k_nd_rules [definition, in k_nd]
k_d_rule [definition, in k_nd]
k_n_rule [definition, in k_nd]
K_nd [section, in k_nd]
k_rename_fun_less [lemma, in k_syntax]
k_rename_fun [definition, in k_syntax]
k_rules_rule [lemma, in k_syntax]
k_rules [definition, in k_syntax]
k_rule [definition, in k_syntax]
k_conclusion_nonempty [lemma, in k_syntax]
k_conclusion [definition, in k_syntax]
k_conclusion_tail [definition, in k_syntax]
k_assumption [definition, in k_syntax]
k_assumption_tail [definition, in k_syntax]
k_sequent [definition, in k_syntax]
k_formulas [definition, in k_syntax]
k_operator [inductive, in k_syntax]
K_syntax [section, in k_syntax]
k_semantic_contraction [lemma, in k_sound_complete]
k_semantic_cut [lemma, in k_sound_complete]
k_complete [lemma, in k_sound_complete]
k_rules_one_step_cut_free_complete [lemma, in k_sound_complete]
k_rules_one_step_sound [lemma, in k_sound_complete]
K_sound.pred_ext [variable, in k_sound_complete]
K_sound [section, in k_sound_complete]
k_lambda [definition, in k_semantics]
k_lifting [definition, in k_semantics]
k_functor [definition, in k_semantics]
K_sementics.pred_ext [variable, in k_semantics]
K_sementics [section, in k_semantics]
k_syntactic_contraction [lemma, in k_absorb]
k_syntactic_cut [lemma, in k_absorb]
k_absorbs_cut [lemma, in k_absorb]
k_absorbs_contraction [lemma, in k_absorb]
k_absorbs_congruence [lemma, in k_absorb]
K_absorb [section, in k_absorb]
k_sound_complete [library]
k_nd [library]
k_semantics [library]
k_syntax [library]
k_absorb [library]
L
lambda_structure [record, in semantics]lambda_structure_type [definition, in semantics]
lambda_false [definition, in formulas]
lambda_or [definition, in formulas]
lambda_formula_rec_char [lemma, in formulas]
lambda_formula_rec [definition, in formulas]
lambda_formula_ind [lemma, in formulas]
lambda_formula_rect [definition, in formulas]
lambda_formula [inductive, in formulas]
lambda_subst [definition, in substitution]
lambda_formula_eq [definition, in sequent_support]
lambda_formula_bool_char [lemma, in sequent_support]
lambda_formula_bool [definition, in sequent_support]
length_list_of_counted_list [lemma, in misc]
length_dep_map_dep_const [lemma, in dep_lists]
length_k_conclusion [lemma, in k_syntax]
length_k_conclusion_tail [lemma, in k_syntax]
length_k_assumption [lemma, in k_syntax]
length_k_assumption_tail [lemma, in k_syntax]
length_subst_sequent [lemma, in substitution]
length_remove_In [lemma, in lists]
length_remove [lemma, in lists]
length_skipn [lemma, in lists]
length_firstn_less [lemma, in lists]
less_length_counted_list [lemma, in misc]
lf_modal_inversion_args [lemma, in formulas]
lf_modal_inversion_op [lemma, in formulas]
lf_modal [constructor, in formulas]
lf_and [constructor, in formulas]
lf_neg [constructor, in formulas]
lf_prop [constructor, in formulas]
lift_p_tcc_irr [lemma, in some_neg]
lift_p [definition, in some_neg]
limit_subst [definition, in substitution]
lists [library]
ListSubset [section, in list_set]
ListSubset.A [variable, in list_set]
lists_disjoint_right_cons [lemma, in list_set]
lists_disjoint_subset_right [lemma, in list_set]
lists_disjoint_symm [lemma, in list_set]
lists_disjoint_right_empty [lemma, in list_set]
lists_disjoint [definition, in list_set]
Lists0 [section, in lists]
Lists0.A [variable, in lists]
Lists1 [section, in lists]
Lists1.A [variable, in lists]
Lists2 [section, in lists]
Lists2.A [variable, in lists]
Lists3 [section, in lists]
Lists3.A [variable, in lists]
list_of_counted_list_map [lemma, in misc]
list_of_counted_list [definition, in misc]
list_weakening_admissible_GRC_n [lemma, in weakening]
list_weakening_admissible_GR_n [lemma, in weakening]
list_weakening_admissible_G_n_hyp [lemma, in weakening]
list_of_dep_list_dep_map_dep_dep [lemma, in dep_lists]
list_of_dep_list [definition, in dep_lists]
list_reorder_right_map [lemma, in reorder]
list_reorder_left_map [lemma, in reorder]
list_reorder_map [lemma, in reorder]
list_reorder_double_append [lemma, in reorder]
list_reorder_2_char [lemma, in reorder]
list_reorder_In_split [lemma, in reorder]
list_reorder_append_left [lemma, in reorder]
list_reorder_append_right [lemma, in reorder]
list_reorder_append_both [lemma, in reorder]
list_reorder_append_swap [lemma, in reorder]
list_reorder_append_3_middle [lemma, in reorder]
list_reorder_move_append [lemma, in reorder]
list_reorder_rot_3 [lemma, in reorder]
list_reorder_swap_head [lemma, in reorder]
list_reorder_first_occurence [lemma, in reorder]
list_reorder_nonempty [lemma, in reorder]
list_reorder_singleton [lemma, in reorder]
list_reorder_nil_is_nil [lemma, in reorder]
list_reorder_In [lemma, in reorder]
list_reorder_single_append [lemma, in reorder]
list_reorder_partition [lemma, in reorder]
list_reorder_inserted_2 [lemma, in reorder]
list_reorder_tail_head [lemma, in reorder]
list_reorder_tail [lemma, in reorder]
list_reorder_insert_list [lemma, in reorder]
list_reorder_insert [lemma, in reorder]
list_reorder_trans_rev [lemma, in reorder]
list_reorder_trans [lemma, in reorder]
list_reorder_occurence [lemma, in reorder]
list_reorder_occurence_full [lemma, in reorder]
list_reorder_symm [lemma, in reorder]
list_reorder_length [lemma, in reorder]
list_reorder_refl [lemma, in reorder]
list_reorder_cons_head [lemma, in reorder]
list_reorder_cons_parts [lemma, in reorder]
list_reorder_cons [constructor, in reorder]
list_reorder_nil [constructor, in reorder]
list_reorder [inductive, in reorder]
list_reorder_subst_sequent [lemma, in substitution]
list_subproofs_head_admissible [lemma, in inversion]
list_search_some_test [lemma, in lists]
list_search_some_less [lemma, in lists]
list_search_some [lemma, in lists]
list_search_some_ind [lemma, in lists]
list_search_none [lemma, in lists]
list_search [definition, in lists]
list_split_at_n2 [lemma, in lists]
list_split_n_equal [lemma, in lists]
list_split_at_n [lemma, in lists]
list_equal_nth_char [lemma, in lists]
list_support_map [lemma, in list_support]
list_support_reorder [lemma, in list_support]
list_support_same_set [lemma, in list_support]
list_support_head_contract [lemma, in list_support]
list_support_of_no_dup [lemma, in list_support]
list_support_destruct [lemma, in list_support]
list_support_incl [lemma, in list_support]
list_support_correct_subset [lemma, in list_support]
list_support_correct_content [lemma, in list_support]
list_support_correct_no_dup [lemma, in list_support]
list_support [definition, in list_support]
List_support.aeq [variable, in list_support]
List_support.A [variable, in list_support]
List_support [section, in list_support]
list_reorder_incl_both [lemma, in list_set]
list_noprop [definition, in some_neg]
list_support [library]
list_set [library]
list_multiset [library]
long_mod_seq_valid_char [lemma, in k_semantics]
M
make_unique_form [definition, in factor_subst]map_subst_correct_fix_var_chain_ends [lemma, in factor_subst]
map_rank_incl [lemma, in factor_subst]
map_rank_append [lemma, in factor_subst]
map_rank_In [lemma, in factor_subst]
map_rank_tail [lemma, in factor_subst]
map_rank_head [lemma, in factor_subst]
map_rank_cons [lemma, in factor_subst]
map_rank_empty [lemma, in factor_subst]
map_rank [definition, in factor_subst]
map_subst_correct_cons_smap [lemma, in factor_subst]
map_subst_correct_cons_rmap [lemma, in factor_subst]
map_subst_correct_empty [lemma, in factor_subst]
map_subst_correct [definition, in factor_subst]
map_subst_sequent_limit_eq [lemma, in substitution]
map_id [lemma, in lists]
map_cutout_nth [lemma, in lists]
map_skipn [lemma, in lists]
map_firstn [lemma, in lists]
map_subst_correct_disjoint_keys [lemma, in factor_two_subst]
map_subst_correct_disjoint_keys_half [lemma, in factor_two_subst]
max_mono_both [lemma, in misc]
member [definition, in lists]
member_append_right [lemma, in lists]
member_append_left [lemma, in lists]
member_append [lemma, in lists]
member_In_false [lemma, in lists]
member_In [lemma, in lists]
minimal_proof_rank_char [lemma, in formulas]
minimal_proof_rank [definition, in formulas]
minimal_rule_rank_conclusion [lemma, in formulas]
minimal_rule_rank_assumptions [lemma, in formulas]
minimal_rule_rank_gt_0 [lemma, in formulas]
minimal_rule_rank [definition, in formulas]
minimal_sequent_rank_gt_0 [lemma, in formulas]
minimal_sequent_rank [definition, in formulas]
minimal_rank_simple_modal_sequent [lemma, in modal_formulas]
misc [library]
mixed_cut_right_osr [lemma, in mixed_cut]
mixed_cut_left_osr [lemma, in mixed_cut]
mixed_cut_ax [lemma, in mixed_cut]
Mixed_cut.L [variable, in mixed_cut]
Mixed_cut.V [variable, in mixed_cut]
Mixed_cut [section, in mixed_cut]
mixed_cut [library]
modal_subst_coval [definition, in semantics]
modal_semantics [projection, in semantics]
modal_rank_ge_1 [lemma, in formulas]
modal_rank_char [lemma, in formulas]
modal_rank [definition, in formulas]
modal_operators [record, in formulas]
modal_form [definition, in modal_formulas]
Modal_formulas.v_eq [variable, in modal_formulas]
Modal_formulas.L [variable, in modal_formulas]
Modal_formulas.V [variable, in modal_formulas]
Modal_formulas [section, in modal_formulas]
modal_formulas [library]
model [record, in semantics]
mod_seq_val_valid_reorder [lemma, in semantics]
mod_val_pred_or [lemma, in semantics]
mod_val_pred_tcc_irr [lemma, in semantics]
mod_val_pred [definition, in semantics]
mod_val_semantics_valid [lemma, in semantics]
mod_seq_val_valid_tcc_irr [lemma, in semantics]
mod_seq_val_valid [definition, in semantics]
mod_seq_val_tcc_irr [lemma, in semantics]
mod_seq_val [definition, in semantics]
mod_arg_back_subst_sequent_prop [lemma, in backward_substitution]
mod_arg_back_subst_sequent_rec_prop [lemma, in backward_substitution]
mod_arg_back_subst_neg_form_prop [lemma, in backward_substitution]
mod_arg_back_subst_modal_form_prop [lemma, in backward_substitution]
mod_arg_back_subst_mod_args_prop [lemma, in backward_substitution]
mod_arg_back_subst_mod_args_prop_ind [lemma, in backward_substitution]
mod_arg_back_subst_sequent [definition, in backward_substitution]
mod_arg_back_subst_sequent_rec [definition, in backward_substitution]
mod_arg_back_subst_neg_mod_form [definition, in backward_substitution]
mod_arg_back_subst_modal_form [definition, in backward_substitution]
mod_arg_back_subst_mod_args [definition, in backward_substitution]
mod_seq_valid_k_conclusion_Sn [lemma, in k_semantics]
mod_seq_valid_k_conclusion_0 [lemma, in k_semantics]
mod_prop_hyp_oracle [definition, in complete]
Multisets [section, in list_multiset]
Multisets.A [variable, in list_multiset]
Multisets.aeq [variable, in list_multiset]
multiset_rank_rules [lemma, in formulas]
multiset_provability [lemma, in formulas]
multiset_depth_provability [lemma, in formulas]
multiset_union [lemma, in formulas]
multiset_provable_subst_n_conclusions [lemma, in weakening]
multiset_valid_subst_n_conclusions [lemma, in one_step_conditions]
multi_subset_right_list_support [lemma, in list_support]
multi_subset_list_support [lemma, in list_support]
multi_subset_right_sequent_support [lemma, in sequent_support]
multi_subset_antisymm [lemma, in list_multiset]
multi_subset_trans [lemma, in list_multiset]
multi_subset [definition, in list_multiset]
N
nat_list_max_lub [lemma, in lists]nat_list_max_le_inv [lemma, in lists]
nat_list_max_le [lemma, in lists]
nat_list_max_pairwise_le [lemma, in lists]
nat_list_max [definition, in lists]
nat_list_sum_append [lemma, in lists]
nat_list_sum [definition, in lists]
neg_simple_modal_form_renaming [lemma, in renaming]
neg_double_neg [lemma, in misc]
neg_neg_implies [lemma, in misc]
neg_implies [lemma, in misc]
neg_is_none [lemma, in misc]
neg_neg_n_subset_G_n [lemma, in rule_sets]
neg_and_n_subset_G_n [lemma, in rule_sets]
neg_neg_rule_no_simple_modal_conclusion [lemma, in rule_sets]
neg_and_rule_no_simple_modal_conclusion [lemma, in rule_sets]
neg_neg_oracle_some [lemma, in build_prop_proof]
neg_neg_oracle [definition, in build_prop_proof]
neg_neg_oracle_tcc [lemma, in build_prop_proof]
neg_and_oracle_some [lemma, in build_prop_proof]
neg_and_oracle [definition, in build_prop_proof]
neg_and_oracle_tcc [lemma, in build_prop_proof]
neg_and_over [definition, in formulas]
neg_form_maybe [definition, in formulas]
neg_form_is_neg [lemma, in formulas]
neg_form [definition, in formulas]
neg_neg_rule_no_empty_conclusion [lemma, in rules]
neg_neg_rule_context [lemma, in rules]
neg_and_rule_no_empty_conclusion [lemma, in rules]
neg_and_rule_context [lemma, in rules]
neg_sequent_subst_k_conclusion_tail [lemma, in k_syntax]
neg_sequent_subst_k_assumption_tail [lemma, in k_syntax]
neg_box_v [definition, in k_syntax]
neg_v [definition, in k_syntax]
neg_sequent_subst_sequent [lemma, in substitution]
neg_box_v_sequent_semantics_char [lemma, in k_semantics]
neg_v_sequent_double_neg_semantics [lemma, in k_semantics]
neg_inv_head_Gn_hyp_admissible [lemma, in inversion]
neg_inv_head_Gn_depth_admissible [lemma, in inversion]
neg_inv_head_Gn_depth_admissible_ind [lemma, in inversion]
neg_and_inv_head_G_n_hyp_admissible [lemma, in inversion]
neg_and_inv_head_Gn_depth_admissible [lemma, in inversion]
neg_and_inv_head_Gn_admissible_ind [lemma, in inversion]
neg_head_inversion_closed [definition, in inversion]
neg_or_and_neg [lemma, in classic]
next_unused_var_fresh [lemma, in factor_two_subst]
next_unused_var [definition, in factor_two_subst]
NoDup_seq [lemma, in lists]
NoDup_map_injective [lemma, in lists]
NoDup_map [lemma, in lists]
NoDup_head [lemma, in lists]
NoDup_tail [lemma, in lists]
nonempty_rank_subst [lemma, in substitution]
nonempty_list_tcc [lemma, in lists]
nonempty_list [definition, in lists]
nonempty_terminal_obj_sequence [lemma, in slice]
nonempty_slice_final [lemma, in slice]
non_empty_coalg [lemma, in functor]
non_trivial_functor [definition, in functor]
non_empty_type [definition, in misc]
non_decomposable_is_prop_mod [lemma, in prop_mod]
non_trivial_k_functor [lemma, in k_semantics]
non_modal_weaken_subst_formula [lemma, in inversion]
noprop [definition, in some_neg]
noprop_or_formula_of_sequnet [lemma, in some_neg_form]
noprop_or [lemma, in some_neg_form]
nth [definition, in lists]
nth_counted_prop_list_valuation [lemma, in semantics]
nth_counted_prop_list_valuation_tcc [lemma, in semantics]
nth_unit_model [definition, in step_semantics]
nth_step_semantics_args [lemma, in step_semantics]
nth_dep_map_dep_const_inv [lemma, in dep_lists]
nth_dep_map_dep_const_inv_tcc [lemma, in dep_lists]
nth_dep_map_dep_const [lemma, in dep_lists]
nth_dep_map_dep_const_tcc [lemma, in dep_lists]
nth_dep_nth_tcc_irr [lemma, in dep_lists]
nth_subst_k_conclusion_tail [lemma, in k_syntax]
nth_k_conclusion_tail [lemma, in k_syntax]
nth_subst_k_assumption_tail [lemma, in k_syntax]
nth_k_assumption_tail [lemma, in k_syntax]
nth_subst_sequent [lemma, in substitution]
nth_seq [lemma, in lists]
nth_map_inv [lemma, in lists]
nth_map_inv_tcc [lemma, in lists]
nth_map [lemma, in lists]
nth_map_tcc [lemma, in lists]
nth_skipn [lemma, in lists]
nth_skipn_tcc [lemma, in lists]
nth_firstn [lemma, in lists]
nth_firstn_tcc [lemma, in lists]
nth_append_right [lemma, in lists]
nth_append_right_ind [lemma, in lists]
nth_append_right_tcc [lemma, in lists]
nth_append_left [lemma, in lists]
nth_head_tcc [lemma, in lists]
nth_tcc_irr [lemma, in lists]
nth_tail [lemma, in lists]
nth_succ_tcc [lemma, in lists]
nth_0_nil_tcc [lemma, in lists]
n_step_subst_coval [definition, in step_semantics]
n_cut_free_completeness [lemma, in complete]
n_completeness [lemma, in complete]
O
obj [projection, in functor]one_step_semantics_valid_propositional [lemma, in step_semantics]
one_step_semantics_propositional [lemma, in step_semantics]
one_step_rule_nonempty_conclusion [lemma, in rule_sets]
one_step_rule_incl_prop_var_sequent [lemma, in rule_sets]
one_step_rule_prop_modal_prop_conclusion [lemma, in rule_sets]
one_step_rule_subst_top_modal_conclusion [lemma, in rule_sets]
one_step_rule_simple_modal_conclusion [lemma, in rule_sets]
one_step_rule_propositional_assumption [lemma, in rule_sets]
one_step_rule_set [definition, in rule_sets]
one_step_rule_multiset [lemma, in rule_sets]
one_step_rule [definition, in rule_sets]
one_step_rule_propositional_subst_assumptions [lemma, in absorb]
one_step_rule_simple_modal_conclusion_subst_reorder [lemma, in absorb]
one_step_cut_free_complete [definition, in one_step_conditions]
one_step_complete [definition, in one_step_conditions]
one_step_generic_complete [definition, in one_step_conditions]
one_step_sound [definition, in one_step_conditions]
One_step_conditions.v_eq [variable, in one_step_conditions]
One_step_conditions.T [variable, in one_step_conditions]
One_step_conditions.L [variable, in one_step_conditions]
One_step_conditions.V [variable, in one_step_conditions]
One_step_conditions [section, in one_step_conditions]
one_step_rule_set_k_rules [lemma, in k_syntax]
one_step_conditions [library]
operator [projection, in formulas]
option_contradiction [lemma, in misc]
or_neg_neg_and [lemma, in misc]
or_formula_of_sequent_nonempty [lemma, in formulas]
or_formula_of_ne_sequent_tcc_irr [lemma, in formulas]
or_formula_of_ne_sequent [definition, in formulas]
or_formula_of_sequent [definition, in formulas]
or_formula_of_sequent_iter_rev [lemma, in formulas]
or_formula_of_sequent_iter_append [lemma, in formulas]
or_formula_of_sequent_iter [definition, in formulas]
or_formula_subst_sequent [lemma, in substitution]
or_formula_subst_sequent_tcc [lemma, in substitution]
OSR_cut.v_eq [variable, in osr_cut]
OSR_cut.op_eq [variable, in osr_cut]
OSR_cut.L [variable, in osr_cut]
OSR_cut.V [variable, in osr_cut]
OSR_cut [section, in osr_cut]
osr_cut [library]
other_context_G_n_set [lemma, in rule_sets]
other_axiom_G_n_set [lemma, in inversion]
P
pair [definition, in functions]pair_compose_right [lemma, in functions]
pair_proj_right [lemma, in functions]
pair_proj_left [lemma, in functions]
partition_result [lemma, in lists]
plain_prop_mod_subst_update [lemma, in plain_prop_mod]
plain_prop_mod_id_subst [lemma, in plain_prop_mod]
plain_prop_mod_subst [definition, in plain_prop_mod]
plain_prop_or_mod_formula [definition, in plain_prop_mod]
Plain_prop_mod.L [variable, in plain_prop_mod]
Plain_prop_mod.V [variable, in plain_prop_mod]
Plain_prop_mod [section, in plain_prop_mod]
plain_prop_mod [library]
plug_empty_hypothesis_proof [lemma, in formulas]
plug_hypothesis_proof [lemma, in formulas]
plus_minus_assoc [lemma, in misc]
proof [inductive, in formulas]
proof_set_equal_rules [lemma, in formulas]
proof_set_equal [lemma, in formulas]
proof_mono_rules [lemma, in formulas]
proof_mono_hyp [lemma, in formulas]
proof_mono [lemma, in formulas]
proof_depth_mono [lemma, in formulas]
proof_depth_sequent_ind [lemma, in formulas]
proof_sequent_ind [lemma, in formulas]
proof_ind [lemma, in formulas]
proof_depth_rule_1 [lemma, in formulas]
proof_depth_0 [lemma, in formulas]
proof_depth_rule_le_inv [lemma, in formulas]
proof_depth_rule_le [lemma, in formulas]
proof_depth_rule [lemma, in formulas]
proof_depth_assume [lemma, in formulas]
proof_depth [definition, in formulas]
proof_rect_rule [lemma, in formulas]
proof_rect [definition, in formulas]
proof_minimal_proof_rank [lemma, in cut_properties]
propositional [definition, in propositional_formulas]
propositional_sound_G [lemma, in propositional_sound]
propositional_correct_G_derivation [lemma, in propositional_sound]
propositional_correct_derivation [lemma, in propositional_sound]
Propositional_soundness.L [variable, in propositional_sound]
Propositional_soundness.V [variable, in propositional_sound]
Propositional_soundness [section, in propositional_sound]
propositional_valuation_false [lemma, in semantics]
propositional_valuation_tcc_irr [lemma, in semantics]
propositional_valuation [definition, in semantics]
propositional_renaming [lemma, in renaming]
propositional_sequent_cons_append [lemma, in propositional_formulas]
propositional_sequent_append_right [lemma, in propositional_formulas]
propositional_sequent_append_left [lemma, in propositional_formulas]
propositional_sequent_append [lemma, in propositional_formulas]
propositional_sequent_cons [lemma, in propositional_formulas]
propositional_or_formula [lemma, in propositional_formulas]
propositional_sequent_tail [lemma, in propositional_formulas]
propositional_sequent_head [lemma, in propositional_formulas]
propositional_sequent_empty [lemma, in propositional_formulas]
propositional_sequent [definition, in propositional_formulas]
propositional_lambda_or [lemma, in propositional_formulas]
propositional_tcc_modal [lemma, in propositional_formulas]
propositional_and_right [lemma, in propositional_formulas]
propositional_and_left [lemma, in propositional_formulas]
propositional_lf_and [lemma, in propositional_formulas]
propositional_neg_inv [lemma, in propositional_formulas]
propositional_neg [lemma, in propositional_formulas]
propositional_lf_prop [lemma, in propositional_formulas]
Propositional_formulas.L [variable, in propositional_formulas]
Propositional_formulas.V [variable, in propositional_formulas]
Propositional_formulas [section, in propositional_formulas]
propositional_renamed_one_step_assumptions [lemma, in one_step_conditions]
propositional_sequent_k_assumption [lemma, in k_syntax]
propositional_sequent_k_assumption_tail [lemma, in k_syntax]
propositional_neg_v [lemma, in k_syntax]
propositional_prop_G_set [lemma, in propositional_rules]
propositional_rule_set [definition, in propositional_rules]
propositional_empty_sequent_set [lemma, in propositional_rules]
propositional_sequent_set [definition, in propositional_rules]
propositional_rule_add_context_bare_rule [lemma, in propositional_rules]
propositional_rule [definition, in propositional_rules]
propositional_add_context_right [lemma, in propositional_rules]
propositional_add_context_left [lemma, in propositional_rules]
propositional_add_context_propositional [lemma, in propositional_rules]
propositional_add_context [lemma, in propositional_rules]
Propositional_rules.L [variable, in propositional_rules]
Propositional_rules.V [variable, in propositional_rules]
Propositional_rules [section, in propositional_rules]
Propositional_models.L [variable, in propositional_models]
Propositional_models.V [variable, in propositional_models]
Propositional_models [section, in propositional_models]
propositional_complete_G [lemma, in propositional_completeness]
Propositional_Completeness.v_eq [variable, in propositional_completeness]
Propositional_Completeness.L [variable, in propositional_completeness]
Propositional_Completeness.V [variable, in propositional_completeness]
Propositional_Completeness [section, in propositional_completeness]
propositional_cut_contraction_weakening [lemma, in propositional_properties]
Propositional_properties.L [variable, in propositional_properties]
Propositional_properties.V [variable, in propositional_properties]
Propositional_properties [section, in propositional_properties]
propositional_sound [library]
propositional_formulas [library]
propositional_properties [library]
propositional_models [library]
propositional_completeness [library]
propositional_rules [library]
prop_downward_correct_prop_G [lemma, in propositional_sound]
prop_downward_correct_neg_neg [lemma, in propositional_sound]
prop_downward_correct_neg_and [lemma, in propositional_sound]
prop_downward_correct_and [lemma, in propositional_sound]
prop_downward_correct_ax [lemma, in propositional_sound]
prop_downward_correct_context [lemma, in propositional_sound]
prop_downward_correct_rule_set [definition, in propositional_sound]
prop_downward_correct_rule_tcc_irr [lemma, in propositional_sound]
prop_downward_correct_rule [definition, in propositional_sound]
prop_proof_type [definition, in propositional_sound]
prop_modal_prop_semantics [lemma, in semantics]
prop_modal_prop_valuation_tcc_irr [lemma, in semantics]
prop_modal_prop_valuation [definition, in semantics]
prop_seq_val_valid_reorder [lemma, in semantics]
prop_val_pred_or [lemma, in semantics]
prop_val_pred_tcc_irr [lemma, in semantics]
prop_val_pred [definition, in semantics]
prop_val_semantics_valid [lemma, in semantics]
prop_val_semantics [lemma, in semantics]
prop_seq_val_valid_tcc_irr [lemma, in semantics]
prop_seq_val_valid [definition, in semantics]
prop_seq_val_tcc_irr [lemma, in semantics]
prop_seq_val [definition, in semantics]
prop_form_subst_neg_simple_modal_form [lemma, in renaming]
prop_form_subst_simple_modal_form [lemma, in renaming]
prop_sequent_renaming [lemma, in renaming]
prop_form_renaming [lemma, in renaming]
prop_neg_up_correct [lemma, in misc]
prop_neg_down_correct [lemma, in misc]
prop_or_up_correct [lemma, in misc]
prop_or_up_correct_context [lemma, in misc]
prop_or_down_correct [lemma, in misc]
prop_and_up_correct [lemma, in misc]
prop_and_down_correct [lemma, in misc]
prop_ax_up_correct [lemma, in misc]
prop_ax_down_correct [lemma, in misc]
prop_G_oracle_None_tautology [lemma, in build_prop_proof]
prop_G_oracle_None_simple [lemma, in build_prop_proof]
prop_G_oracle_None [lemma, in build_prop_proof]
prop_G_oracle [definition, in build_prop_proof]
prop_sequent_is_propositional [lemma, in propositional_formulas]
prop_form_is_propositional [lemma, in propositional_formulas]
prop_var_sequent_cutout_nth [lemma, in formulas]
prop_var_sequent_list_reorder [lemma, in formulas]
prop_var_sequent_append [lemma, in formulas]
prop_var_sequent_cons [lemma, in formulas]
prop_var_sequent [definition, in formulas]
prop_var_modal_args_cons [lemma, in formulas]
prop_var_formula_char [lemma, in formulas]
prop_var_modal_args [definition, in formulas]
prop_var_formula [definition, in formulas]
prop_sequent_list_reorder [lemma, in formulas]
prop_sequent_head [lemma, in formulas]
prop_sequent_tail [lemma, in formulas]
prop_sequent_cons [lemma, in formulas]
prop_sequent [definition, in formulas]
prop_form_acc_tcc_irr [lemma, in formulas]
prop_form_acc [definition, in formulas]
prop_form [definition, in formulas]
prop_back_subst_form_prop [lemma, in backward_substitution]
prop_back_subst_form_prop_ind [lemma, in backward_substitution]
prop_back_subst_form [definition, in backward_substitution]
prop_back_subst_form_rec [definition, in backward_substitution]
prop_var_list_below_append [lemma, in backward_substitution]
prop_var_list_below_empty [lemma, in backward_substitution]
prop_var_list_below_singleton [lemma, in backward_substitution]
prop_var_list_below [definition, in backward_substitution]
prop_or_mod_partition [lemma, in prop_mod]
prop_or_mod_sequent_prop [lemma, in prop_mod]
prop_or_mod_sequent_append_right [lemma, in prop_mod]
prop_or_mod_sequent_append_left [lemma, in prop_mod]
prop_or_mod_sequent_list_reorder [lemma, in prop_mod]
prop_or_mod_sequent_cons [lemma, in prop_mod]
prop_or_mod_sequent_empty [lemma, in prop_mod]
prop_or_mod_sequent [definition, in prop_mod]
prop_or_mod_formula_prop [lemma, in prop_mod]
prop_or_mod_formula [definition, in prop_mod]
Prop_mod.v_eq [variable, in prop_mod]
Prop_mod.L [variable, in prop_mod]
Prop_mod.V [variable, in prop_mod]
Prop_mod [section, in prop_mod]
prop_var_sequent_subst_k_conclusion_tail [lemma, in k_syntax]
prop_var_sequent_subst_k_conclusion_tail_ind [lemma, in k_syntax]
prop_var_sequent_k_conclusion [lemma, in k_syntax]
prop_modal_prop_sequent_k_conclusion [lemma, in k_syntax]
prop_var_sequent_k_assumption [lemma, in k_syntax]
prop_sequent_subst_k_assumption [lemma, in k_syntax]
prop_sequent_subst_k_assumption_tail [lemma, in k_syntax]
prop_sequent_k_assumption [lemma, in k_syntax]
prop_sequent_k_assumption_tail [lemma, in k_syntax]
prop_G_subset_prop_GC [lemma, in propositional_rules]
prop_GC_set [definition, in propositional_rules]
prop_G_subset_GRC [lemma, in propositional_rules]
prop_G_subset_GR [lemma, in propositional_rules]
prop_G_subset_Gn [lemma, in propositional_rules]
prop_G_set [definition, in propositional_rules]
prop_sequent_rule_concl_tcc [lemma, in propositional_rules]
prop_sequent_rule_ass_tcc [lemma, in propositional_rules]
Prop_cut.v_eq [variable, in prop_cut]
Prop_cut.op_eq [variable, in prop_cut]
Prop_cut.L [variable, in prop_cut]
Prop_cut.V [variable, in prop_cut]
Prop_cut [section, in prop_cut]
prop_seq_valid_k_assumption_Sn [lemma, in k_semantics]
prop_seq_valid_renamed_k_assumption_Sn [lemma, in k_semantics]
prop_seq_valid_renamed_k_assumption_0 [lemma, in k_semantics]
prop_seq_valid_k_assumption_0 [lemma, in k_semantics]
prop_model_sequent_interpretation [lemma, in propositional_models]
prop_sequent_interpretation_add_context_split [lemma, in propositional_models]
prop_sequent_interpretation_add_context [lemma, in propositional_models]
prop_sequent_interpretation_append_split [lemma, in propositional_models]
prop_sequent_interpretation_append [lemma, in propositional_models]
prop_sequent_interpretation_cons_cons_intro [lemma, in propositional_models]
prop_sequent_interpretation_cons_case_intro [lemma, in propositional_models]
prop_sequent_interpretation_length_case_intro [lemma, in propositional_models]
prop_sequent_interpretation_cons_cons_elim [lemma, in propositional_models]
prop_sequent_interpretation_cons_case_elim [lemma, in propositional_models]
prop_sequent_interpretation_nth_intro [lemma, in propositional_models]
prop_sequent_interpretation_singleton [lemma, in propositional_models]
prop_sequent_interpretation_empty [lemma, in propositional_models]
prop_sequent_interpretation_tcc_irr [lemma, in propositional_models]
prop_sequent_interpretation [definition, in propositional_models]
prop_valid_sequent [definition, in propositional_models]
prop_valid [definition, in propositional_models]
prop_model [definition, in propositional_models]
prop_modal_sequent_tail [lemma, in modal_formulas]
prop_modal_sequent_head [lemma, in modal_formulas]
prop_modal_sequent_cons [lemma, in modal_formulas]
prop_modal_sequent [definition, in modal_formulas]
prop_modal [definition, in modal_formulas]
prop_modal_prop_or_formula [lemma, in modal_formulas]
prop_modal_prop_or_formula_iter [lemma, in modal_formulas]
prop_modal_prop_sequent_tail [lemma, in modal_formulas]
prop_modal_prop_sequent_head [lemma, in modal_formulas]
prop_modal_prop_sequent_cons [lemma, in modal_formulas]
prop_modal_prop_sequent_append_right [lemma, in modal_formulas]
prop_modal_prop_sequent_append_left [lemma, in modal_formulas]
prop_modal_prop_sequent [definition, in modal_formulas]
prop_modal_prop_tcc_modal [lemma, in modal_formulas]
prop_modal_prop_tcc_and_2 [lemma, in modal_formulas]
prop_modal_prop_tcc_and_1 [lemma, in modal_formulas]
prop_modal_prop_tcc_neg [lemma, in modal_formulas]
prop_modal_prop_tcc_prop [lemma, in modal_formulas]
prop_modal_prop_lambda_or [lemma, in modal_formulas]
prop_modal_prop [definition, in modal_formulas]
prop_var_sequent_subst_rename_of_map [lemma, in factor_two_subst]
prop_var_formula_subst_rename_of_map [lemma, in factor_two_subst]
prop_var_sequent_support [lemma, in k_absorb]
prop_mod_build_proof [definition, in complete]
prop_mod_build_proof_left [lemma, in complete]
prop_mod_build_proof_maybe [definition, in complete]
prop_Gn_oracle [definition, in complete]
prop_3_2_1 [lemma, in propositional_completeness]
prop_correct_propositional [lemma, in propositional_completeness]
prop_correct [definition, in propositional_completeness]
prop_build_proof_prop [definition, in propositional_completeness]
prop_build_proof_prop_type [definition, in propositional_completeness]
prop_build_proof [definition, in propositional_completeness]
prop_hyp_oracle [definition, in propositional_completeness]
prop_G_cut_elim_head [lemma, in propositional_properties]
prop_G_cut_elim_head_ind [lemma, in propositional_properties]
prop_contraction_head [lemma, in propositional_properties]
prop_mod [library]
prop_cut [library]
provable [definition, in formulas]
provable_GRC_n_list_reorder [lemma, in rule_sets]
provable_GR_n_list_reorder [lemma, in rule_sets]
provable_GR_n_hyp_list_reorder [lemma, in rule_sets]
provable_with_cut [lemma, in rule_sets]
provable_with_neg_neg [lemma, in rule_sets]
provable_with_neg_and [lemma, in rule_sets]
provable_with_and [lemma, in rule_sets]
provable_G_n_list_reorder [lemma, in rule_sets]
provable_G_n_hyp_list_reorder [lemma, in rule_sets]
provable_depth_G_n_hyp_list_reorder [lemma, in rule_sets]
provable_rank_rules_has_rank_n [lemma, in formulas]
provable_rank_rules_hyp_has_rank_n [lemma, in formulas]
provable_at_depth_destruct [lemma, in formulas]
provable_at_depth_with_rule [lemma, in formulas]
provable_at_depth_0 [lemma, in formulas]
provable_at_depth_provable [lemma, in formulas]
provable_at_proof_depth [lemma, in formulas]
provable_at_depth [definition, in formulas]
provable_with_rule [lemma, in formulas]
provable_with_assumption [lemma, in formulas]
provable_subst_n_conclusions [definition, in weakening]
provable_k_nd_hyp_list_reorder [lemma, in k_nd]
provable_sequent_axiom [lemma, in generic_cut]
provable_sequent_axiom_ind [lemma, in generic_cut]
provable_or_formula_of_ne_sequent [lemma, in generic_cut]
provable_GRC_n_GR_n_from_head_elim [lemma, in generic_cut]
provable_prop_G_hyp_list_reorder [lemma, in propositional_rules]
provable_depth_prop_list_reorder [lemma, in propositional_rules]
provable_subst_n_conclusions_rank_non_modal [lemma, in inversion]
provable_GRC_1_GR_1 [lemma, in propositional_properties]
provable_GC_1_G_1 [lemma, in propositional_properties]
provable_assumptions_contraction_rule [lemma, in contraction]
p_or_formula_of_sequent_iter [lemma, in some_neg_form]
R
rank_sequent_renaming [lemma, in renaming]rank_renaming [lemma, in renaming]
rank_subst_conclusion [lemma, in rule_sets]
rank_sequent_subst_nth_assumptions [lemma, in rule_sets]
rank_subst_assumptions [lemma, in rule_sets]
rank_G_n_inductive [lemma, in build_prop_proof]
rank_rules_ge_minimal [lemma, in formulas]
rank_rules_minimal_rule_rank [lemma, in formulas]
rank_rules_distribute_union [lemma, in formulas]
rank_rules_subset_rank [lemma, in formulas]
rank_rules_set_eq [lemma, in formulas]
rank_rules_mono [lemma, in formulas]
rank_rules [definition, in formulas]
rank_sequent_set_sequent_list_set [lemma, in formulas]
rank_sequent_set_mono [lemma, in formulas]
rank_sequent_set_empty [lemma, in formulas]
rank_sequent_set [definition, in formulas]
rank_formula_modal_args_TCC [lemma, in formulas]
rank_formula_modal_1_TCC [lemma, in formulas]
rank_formula_modal_ge_2 [lemma, in formulas]
rank_sequent_ge_minimal [lemma, in formulas]
rank_sequent_le_minimal [lemma, in formulas]
rank_sequent_succ_minimal_nonempty_sequent_rank [lemma, in formulas]
rank_sequent_minimal_sequent_rank [lemma, in formulas]
rank_prop_sequent [lemma, in formulas]
rank_formula_or_formula_of_ne_sequent [lemma, in formulas]
rank_formula_succ_or_formula_of_sequent [lemma, in formulas]
rank_formula_or_formula_of_sequent [lemma, in formulas]
rank_formula_or_formula_iter_rev [lemma, in formulas]
rank_formula_or_formula_iter [lemma, in formulas]
rank_sequent_different_head [lemma, in formulas]
rank_sequent_append_right [lemma, in formulas]
rank_sequent_append_left [lemma, in formulas]
rank_sequent_append [lemma, in formulas]
rank_sequent_tail [lemma, in formulas]
rank_sequent_head [lemma, in formulas]
rank_sequent_cons [lemma, in formulas]
rank_sequent_empty [lemma, in formulas]
rank_sequent_list_reorder [lemma, in formulas]
rank_sequent_mono [lemma, in formulas]
rank_sequent [definition, in formulas]
rank_formula_modal [lemma, in formulas]
rank_formula_prop_form [lemma, in formulas]
rank_formula_lambda_or_rev [lemma, in formulas]
rank_formula_lambda_or [lemma, in formulas]
rank_formula_neg_and_over [lemma, in formulas]
rank_formula_neg_form_maybe [lemma, in formulas]
rank_formula_false [lemma, in formulas]
rank_formula_and_right [lemma, in formulas]
rank_formula_and_left [lemma, in formulas]
rank_formula_lf_and [lemma, in formulas]
rank_formula_lf_neg_TCC [lemma, in formulas]
rank_formula_lf_neg [lemma, in formulas]
rank_formula_lf_prop [lemma, in formulas]
rank_formula_ge [lemma, in formulas]
rank_formula_zero_TCC [lemma, in formulas]
rank_formula_zero [lemma, in formulas]
rank_formula [definition, in formulas]
rank_sequent_set_provable_subst_n_conclusions [lemma, in weakening]
rank_proof_GR_fixed_rank [lemma, in weakening]
rank_sequent_osr_subst_conclusion [lemma, in weakening]
rank_weaken_subst_rule [definition, in weakening]
rank_proof_GR [lemma, in cut_properties]
rank_proof_GRC [lemma, in cut_properties]
rank_assumptions_bounded_weakening_rule [lemma, in rules]
rank_conclusion_bounded_weakening_rule [lemma, in rules]
rank_sequent_subst_Ax_set [lemma, in rules]
rank_rule_add_context_rev [lemma, in rules]
rank_sequent_set_congruence_assumptions [lemma, in absorb]
rank_sequent_set_valid_subst_n_conclusions [lemma, in one_step_conditions]
rank_subst_subst_of_fixed_map [lemma, in factor_subst]
rank_unique_form [lemma, in factor_subst]
rank_subst_limit_lf_modal [lemma, in substitution]
rank_subst_id_subst [lemma, in substitution]
rank_formula_id_subst [lemma, in substitution]
rank_subst_subst_compose [lemma, in substitution]
rank_sequent_subst_prop_sequent [lemma, in substitution]
rank_sequent_subst_add [lemma, in substitution]
rank_formula_subst_formula_add [lemma, in substitution]
rank_subst_update [lemma, in substitution]
rank_subst_ge [lemma, in substitution]
rank_subst [definition, in substitution]
rank_sequent_prop_modal_prop_sequent [lemma, in modal_formulas]
rank_formula_prop_modal_prop [lemma, in modal_formulas]
rank_subst_limit_subst_rule [lemma, in modal_formulas]
rank_subst_limit_simple_modal_form [lemma, in modal_formulas]
rank_sequent_subst_simple_modal_sequent [lemma, in modal_formulas]
rank_simple_modal_sequent [lemma, in modal_formulas]
rank_formula_simple_modal_form [lemma, in modal_formulas]
rank_join_subst_maps [lemma, in factor_two_subst]
rank_sequent_sequent_support [lemma, in sequent_support]
rassoc [definition, in assoc]
rassoc_assoc_some [lemma, in assoc]
rassoc_assoc_none [lemma, in assoc]
rassoc_cons_tail [lemma, in assoc]
rassoc_cons_first [lemma, in assoc]
rassoc_cons_split [lemma, in assoc]
rename_of_id [lemma, in renaming]
rename_of_fun [definition, in renaming]
rename_of_map_prop [lemma, in factor_subst]
rename_of_map_cons_split [lemma, in factor_subst]
rename_of_map [definition, in factor_subst]
rename_disjoint_compose_identity [lemma, in factor_two_subst]
rename_disjoint_values_not_in_source [lemma, in factor_two_subst]
rename_disjoint_disjoint [lemma, in factor_two_subst]
rename_disjoint_disjoint_ind [lemma, in factor_two_subst]
rename_disjoint [definition, in factor_two_subst]
renaming [definition, in renaming]
Renaming [section, in renaming]
renaming [library]
renaming_rename_of_fun [lemma, in renaming]
renaming_limit_subst_simple_modal_sequent [lemma, in renaming]
renaming_subst_compose [lemma, in renaming]
renaming_id_subst [lemma, in renaming]
renaming_rename_of_map [lemma, in factor_subst]
Renaming.L [variable, in renaming]
Renaming.V [variable, in renaming]
Renaming.v_eq [variable, in renaming]
Reorder [section, in reorder]
reorder [library]
reordered_sequent_list_set [definition, in formulas]
reordered_rule [definition, in formulas]
reorder_rule_add_context [lemma, in rules]
Reorder.A [variable, in reorder]
restricted_map_ext [lemma, in lists]
restrict_hypothesis [definition, in build_proof]
rule [constructor, in formulas]
Rules [section, in rules]
rules [library]
Rules.L [variable, in rules]
Rules.V [variable, in rules]
Rule_sets.L [variable, in rule_sets]
Rule_sets.V [variable, in rule_sets]
Rule_sets [section, in rule_sets]
rule_oracle_G_property [definition, in build_prop_proof]
rule_has_rank [definition, in formulas]
rule_multiset [definition, in formulas]
rule_add_context [definition, in rules]
rule_multiset_k_nd [lemma, in k_nd]
rule_has_rank_subst_rule [lemma, in substitution]
rule_inductive [definition, in build_proof]
rule_oracle_type [definition, in build_proof]
rule_oracle_result [definition, in build_proof]
rule_sets [library]
R_n_subset_GRC_n [lemma, in rule_sets]
R_n_subset_GR_n [lemma, in rule_sets]
R_set_1_empty [lemma, in rule_sets]
R_set_no_empty_conclusion [lemma, in rule_sets]
S
scssv_4_13_nonempty_tcc [lemma, in step_semantics]Semantics [section, in semantics]
semantics [library]
semantics_step_semantics [lemma, in step_semantics]
Semantics.L [variable, in semantics]
Semantics.T [variable, in semantics]
Semantics.V [variable, in semantics]
semantic_admissible_contraction [lemma, in complete]
semantic_admissible_cut [lemma, in complete]
semantic_admissible_rules [lemma, in complete]
sequent [definition, in formulas]
sequent_other_context_G_n_set [lemma, in rule_sets]
sequent_multiset_reordered_sequent_list_set [lemma, in formulas]
sequent_multiset_empty [lemma, in formulas]
sequent_multiset [definition, in formulas]
sequent_measure_simple_context_lt [lemma, in formulas]
sequent_measure_context_lt [lemma, in formulas]
sequent_measure_append [lemma, in formulas]
sequent_measure_cons [lemma, in formulas]
sequent_measure [definition, in formulas]
sequent_rule [record, in formulas]
sequent_prop [definition, in some_neg_form]
sequent_other_axiom_G_n_set [lemma, in inversion]
sequent_support_subst_sequent [lemma, in sequent_support]
sequent_support_destruct [lemma, in sequent_support]
sequent_support_reorder [lemma, in sequent_support]
sequent_support_head_contract [lemma, in sequent_support]
sequent_support_incl [lemma, in sequent_support]
sequent_support_correct_subset [lemma, in sequent_support]
sequent_support_correct_content [lemma, in sequent_support]
sequent_support_correct_no_dup [lemma, in sequent_support]
sequent_support [definition, in sequent_support]
Sequent_support.v_eq [variable, in sequent_support]
Sequent_support.op_eq [variable, in sequent_support]
Sequent_support.L [variable, in sequent_support]
Sequent_support.V [variable, in sequent_support]
Sequent_support [section, in sequent_support]
sequent_support [library]
seq_semantics [definition, in semantics]
set [definition, in sets]
Sets [section, in dsets]
Sets [section, in sets]
sets [library]
sets_containing [definition, in sets]
Sets.A [variable, in dsets]
Sets.A [variable, in sets]
set_equal_form_semantics_subst_change_coval [lemma, in semantics]
set_equal_modal_semantics [projection, in semantics]
set_equal_multiset [lemma, in formulas]
set_inverse_intersection [lemma, in sets]
set_equal_rw_r [lemma, in sets]
set_equal_implies_subset [lemma, in sets]
set_equal_union_empty_right [lemma, in sets]
set_equal_union_subset_right [lemma, in sets]
set_equal_is_full [lemma, in sets]
set_equal_set_inverse [lemma, in sets]
set_equal_intersection [lemma, in sets]
set_equal_union [lemma, in sets]
set_equal_subset [lemma, in sets]
set_equal_subset_char [lemma, in sets]
set_equal_trans [lemma, in sets]
set_equal_symm [lemma, in sets]
set_equal_refl [lemma, in sets]
set_equal [definition, in sets]
set_inverse [definition, in sets]
set_equal_inv_img_feq [lemma, in image]
set_equal_inv_img_pred [lemma, in image]
set_equal_inv_img [lemma, in image]
short_mod_seq_valid_char [lemma, in k_semantics]
simple_mod_seq_val_valid_correct [lemma, in semantics]
simple_mod_seq_val_valid [definition, in semantics]
simple_mod_seq_val_length_case_intro [lemma, in semantics]
simple_mod_seq_val_append_right [lemma, in semantics]
simple_mod_seq_val_append_left [lemma, in semantics]
simple_mod_seq_val_tail [lemma, in semantics]
simple_mod_seq_val_head [lemma, in semantics]
simple_mod_seq_val_nth_intro [lemma, in semantics]
simple_mod_seq_val_tcc_irr [lemma, in semantics]
simple_mod_seq_val [definition, in semantics]
simple_prop_seq_val_valid_correct [lemma, in semantics]
simple_prop_seq_val_valid [definition, in semantics]
simple_prop_seq_val_length_case_intro [lemma, in semantics]
simple_prop_seq_val_tail [lemma, in semantics]
simple_prop_seq_val_head [lemma, in semantics]
simple_prop_seq_val_tcc_irr [lemma, in semantics]
simple_prop_seq_val [definition, in semantics]
simple_modal_sequent_renaming [lemma, in renaming]
simple_modal_form_renaming [lemma, in renaming]
simple_tautology_contract_head [lemma, in rules]
simple_tautology_cons_destruct [lemma, in rules]
simple_tautology_append_right [lemma, in rules]
simple_tautology_reorder [lemma, in rules]
simple_tautology_tail [lemma, in rules]
simple_tautology_append_left [lemma, in rules]
simple_tautology_cons [lemma, in rules]
simple_tautology [definition, in rules]
simple_tautology_witness [definition, in rules]
simple_modal_from_prop [lemma, in prop_mod]
simple_prop_from_prop [lemma, in prop_mod]
simple_one_step_cut_free_complete [lemma, in one_step_conditions]
simple_mod_weaken_rule_assumptions [lemma, in one_step_conditions]
simple_mod_weaken_rule [definition, in one_step_conditions]
simple_modal_sequent_subst_k_conclusion_tail [lemma, in k_syntax]
simple_modal_sequent_k_conclusion [lemma, in k_syntax]
simple_modal_sequent_k_conclusion_tail [lemma, in k_syntax]
simple_modal_neg_box_v [lemma, in k_syntax]
simple_modal_box_v [lemma, in k_syntax]
simple_prop_seq_val_k_assumption_head [lemma, in k_semantics]
simple_modal_sequent_is_prop_modal_prop [lemma, in modal_formulas]
simple_modal_form_is_prop_modal_prop [lemma, in modal_formulas]
simple_modal_sequent_partition [lemma, in modal_formulas]
simple_modal_sequent_cutout_nth [lemma, in modal_formulas]
simple_modal_sequent_list_reorder [lemma, in modal_formulas]
simple_modal_sequent_tail [lemma, in modal_formulas]
simple_modal_sequent_head [lemma, in modal_formulas]
simple_modal_sequent_cons [lemma, in modal_formulas]
simple_modal_sequent_append_right [lemma, in modal_formulas]
simple_modal_sequent_append_left [lemma, in modal_formulas]
simple_modal_sequent_append [lemma, in modal_formulas]
simple_modal_sequent_empty [lemma, in modal_formulas]
simple_modal_sequent [definition, in modal_formulas]
simple_modal_form [definition, in modal_formulas]
simple_4_13_sequent [definition, in complete]
simple_tautology_cons_append [lemma, in propositional_completeness]
single_prop_ax_correct [lemma, in misc]
skipn_firstn [lemma, in lists]
skipn_skipn [lemma, in lists]
skipn_append_right [lemma, in lists]
skipn_append_left [lemma, in lists]
skipn_whole [lemma, in lists]
Slice [section, in slice]
slice [library]
slice_model_nth_unit [lemma, in step_semantics]
slice_model [definition, in step_semantics]
slice_unit_coalg [definition, in slice]
slice_final_map_times_prop [lemma, in slice]
slice_final_map_pair_prop [lemma, in slice]
slice_final_map_id [lemma, in slice]
slice_final_map [definition, in slice]
slice_final [definition, in slice]
slice_obj_T_eq_lift_refl [lemma, in slice]
slice_obj_T_eq_lift [lemma, in slice]
slice_map_T_id [lemma, in slice]
slice_map_T [definition, in slice]
slice_obj_T [definition, in slice]
Slice.T [variable, in slice]
Slice.V [variable, in slice]
smaller_context_G_n_set [lemma, in rule_sets]
some_nth_singleton [lemma, in some_nth]
some_nth_some [lemma, in some_nth]
some_nth [definition, in some_nth]
Some_nth.P [variable, in some_nth]
Some_nth.A [variable, in some_nth]
Some_nth [section, in some_nth]
some_neg_correct [lemma, in some_neg_form]
Some_neg_form.P_or_formula [variable, in some_neg_form]
Some_neg_form.P_false [variable, in some_neg_form]
Some_neg_form.P [variable, in some_neg_form]
Some_neg_form.L [variable, in some_neg_form]
Some_neg_form.V [variable, in some_neg_form]
Some_neg_form [section, in some_neg_form]
some_neg_dep_correct [lemma, in some_neg_form]
Some_neg_dep_form_2.P_false [variable, in some_neg_form]
Some_neg_dep_form_2.P_or_formula [variable, in some_neg_form]
Some_neg_dep_form_2.P_tcc_irr [variable, in some_neg_form]
Some_neg_dep_form_2.form_prop_or_formula_of_sequent [variable, in some_neg_form]
Some_neg_dep_form_2.form_prop_or [variable, in some_neg_form]
Some_neg_dep_form_2.P [variable, in some_neg_form]
Some_neg_dep_form_2.form_prop [variable, in some_neg_form]
Some_neg_dep_form_2.L [variable, in some_neg_form]
Some_neg_dep_form_2.V [variable, in some_neg_form]
Some_neg_dep_form_2 [section, in some_neg_form]
some_neg_dep_cons_correct [lemma, in some_neg_form]
Some_neg_dep_form.P_or_formula [variable, in some_neg_form]
Some_neg_dep_form.P_tcc_irr [variable, in some_neg_form]
Some_neg_dep_form.form_prop_or_formula_of_sequent_iter [variable, in some_neg_form]
Some_neg_dep_form.form_prop_or [variable, in some_neg_form]
Some_neg_dep_form.P [variable, in some_neg_form]
Some_neg_dep_form.form_prop [variable, in some_neg_form]
Some_neg_dep_form.L [variable, in some_neg_form]
Some_neg_dep_form.V [variable, in some_neg_form]
Some_neg_dep_form [section, in some_neg_form]
some_neg_reorder [definition, in some_neg]
some_neg_tail [definition, in some_neg]
some_neg_append_left [definition, in some_neg]
some_neg_append_right [definition, in some_neg]
some_neg_append [definition, in some_neg]
some_neg_long_neg_intro [definition, in some_neg]
some_neg_cons_case_intro [definition, in some_neg]
some_neg_length_case_intro [definition, in some_neg]
some_neg_head [definition, in some_neg]
some_neg_cons_case_elim [definition, in some_neg]
some_neg_nth_intro [definition, in some_neg]
some_neg_singleton [lemma, in some_neg]
some_neg_singleton_back [definition, in some_neg]
some_neg_singleton_for [definition, in some_neg]
some_neg_empty [definition, in some_neg]
some_neg [definition, in some_neg]
Some_neg.P [variable, in some_neg]
Some_neg.A [variable, in some_neg]
Some_neg [section, in some_neg]
some_neg_dep_map [lemma, in some_neg]
some_neg_dep_reorder [lemma, in some_neg]
some_neg_dep_tail [lemma, in some_neg]
some_neg_dep_append_left [lemma, in some_neg]
some_neg_dep_append_right [lemma, in some_neg]
some_neg_dep_append [lemma, in some_neg]
some_neg_dep_long_neg_intro [lemma, in some_neg]
some_neg_dep_cons_case_intro [lemma, in some_neg]
some_neg_dep_length_case_intro [lemma, in some_neg]
some_neg_dep_head [lemma, in some_neg]
some_neg_dep_cons_cons_elim [lemma, in some_neg]
some_neg_dep_cons_case_elim [lemma, in some_neg]
some_neg_dep_nth_intro [lemma, in some_neg]
some_neg_dep_singleton_rev [lemma, in some_neg]
some_neg_dep_singleton [lemma, in some_neg]
some_neg_dep_empty [lemma, in some_neg]
some_neg_dep_tcc_irr [lemma, in some_neg]
some_neg_dep [definition, in some_neg]
Some_neg_dep.P_tcc_irr [variable, in some_neg]
Some_neg_dep.P [variable, in some_neg]
Some_neg_dep.aprop [variable, in some_neg]
Some_neg_dep.A [variable, in some_neg]
Some_neg_dep [section, in some_neg]
some_nth [library]
some_neg_form [library]
some_neg [library]
sound [library]
Soundness [section, in sound]
Soundness.L [variable, in sound]
Soundness.T [variable, in sound]
Soundness.V [variable, in sound]
sound_k_GR [lemma, in k_sound_complete]
sound_k_GRC [lemma, in k_sound_complete]
sound_GR [lemma, in sound]
sound_GRC [lemma, in sound]
sound_derivation [lemma, in sound]
split_nat_case_le [lemma, in misc]
split_nat_case_lt [lemma, in misc]
split_prop_mod [lemma, in complete]
state [projection, in semantics]
state_seq_semantics_valid [lemma, in semantics]
state_seq_semantics_correct [lemma, in semantics]
state_seq_semantics_reorder [lemma, in semantics]
state_seq_semantics_append_left [lemma, in semantics]
state_seq_semantics_append_right [lemma, in semantics]
state_seq_semantics_append [lemma, in semantics]
state_seq_semantics_length_case_intro [lemma, in semantics]
state_seq_semantics_cons_case_elim [lemma, in semantics]
state_seq_semantics_nth_intro [lemma, in semantics]
state_seq_semantics_singleton [lemma, in semantics]
state_seq_semantics [definition, in semantics]
state_seq_step_semantics_valid_correct [lemma, in step_semantics]
state_seq_step_semantics_valid [definition, in step_semantics]
state_seq_step_semantics_correct [lemma, in step_semantics]
state_seq_step_form_pred_lambda_or [lemma, in step_semantics]
state_seq_step_semantics_long_neg_intro [lemma, in step_semantics]
state_seq_step_semantics_append_left [lemma, in step_semantics]
state_seq_step_semantics_append_right [lemma, in step_semantics]
state_seq_step_semantics_append [lemma, in step_semantics]
state_seq_step_semantics_list_reorder_rev [lemma, in step_semantics]
state_seq_step_semantics_list_reorder [lemma, in step_semantics]
state_seq_step_semantics_tcc_irr [lemma, in step_semantics]
state_seq_step_semantics [definition, in step_semantics]
state_seq_step_form_pred [definition, in step_semantics]
step_prop_sequent_semantics [lemma, in step_semantics]
step_mod_sequent_semantics [lemma, in step_semantics]
step_semantics_valid_G_rule_inductive [lemma, in step_semantics]
step_semantics_sequent_append [lemma, in step_semantics]
step_semantics_valid_at_rank_list_reorder [lemma, in step_semantics]
step_semantics_valid_list_reorder [lemma, in step_semantics]
step_semantics_validity [lemma, in step_semantics]
step_semantics_valid_at_rank [definition, in step_semantics]
step_semantics_valid_taut [lemma, in step_semantics]
step_semantics_valid_nonempty [lemma, in step_semantics]
step_semantics_valid_tcc_irr [lemma, in step_semantics]
step_semantics_valid [definition, in step_semantics]
step_semantics_sequent_empty [lemma, in step_semantics]
step_semantics_sequent_tcc_irr [lemma, in step_semantics]
step_semantics_sequent [definition, in step_semantics]
step_semantics_false [lemma, in step_semantics]
step_semantics_lf_neg_rev [lemma, in step_semantics]
step_semantics_tcc_irr [lemma, in step_semantics]
step_semantics_tcc_irr_eq [lemma, in step_semantics]
step_semantics_modal [lemma, in step_semantics]
step_semantics_args [definition, in step_semantics]
step_semantics [definition, in step_semantics]
Step_semantics.T [variable, in step_semantics]
Step_semantics.L [variable, in step_semantics]
Step_semantics.V [variable, in step_semantics]
Step_semantics [section, in step_semantics]
step_semantics [library]
stratified_one_step_rules [lemma, in weakening]
strong_downward_correct_cut [lemma, in sound]
strong_downward_correct_neg_neg [lemma, in sound]
strong_downward_correct_neg_and [lemma, in sound]
strong_downward_correct_and [lemma, in sound]
strong_downward_correct_ax [lemma, in sound]
strong_downward_correct_context [lemma, in sound]
strong_downward_correct_rule [definition, in sound]
subproofs_head_admissible [lemma, in inversion]
subset [definition, in sets]
subset_rank_rules [lemma, in formulas]
subset_empty_set [lemma, in sets]
subset_union_lub [lemma, in sets]
subset_union_both [lemma, in sets]
subset_union_right [lemma, in sets]
subset_union_left [lemma, in sets]
subset_add [lemma, in sets]
subset_trans [lemma, in sets]
subset_refl [lemma, in sets]
subset_dep_prop [definition, in dep_lists]
substitution [library]
Substitutions [section, in substitution]
Substitutions.L [variable, in substitution]
Substitutions.V [variable, in substitution]
Substitutions.v_eq [variable, in substitution]
subst_coval [definition, in semantics]
subst_coval_prop_step_semantics_valid [lemma, in step_semantics]
subst_coval_prop_step_semantics [lemma, in step_semantics]
subst_coval_modal_step_semantics_valid_for_4_13 [lemma, in step_semantics]
subst_coval_modal_step_semantics_valid [lemma, in step_semantics]
subst_coval_modal_step_semantics [lemma, in step_semantics]
subst_closed_GRC_set_wo_ax [lemma, in rule_sets]
subst_closed_GR_set_wo_ax [lemma, in rule_sets]
subst_closed_weaken_subst [lemma, in rule_sets]
subst_closed_G_struct_set [lemma, in rule_sets]
subst_eq_on_vars_below [lemma, in backward_substitution]
subst_equal_below_mono [definition, in backward_substitution]
subst_equal_below_single_update [definition, in backward_substitution]
subst_equal_below_trans [definition, in backward_substitution]
subst_equal_below_refl [definition, in backward_substitution]
subst_equal_below [definition, in backward_substitution]
subst_cut_rule [lemma, in rules]
subst_Ax_n_set [definition, in rules]
subst_Ax_set [definition, in rules]
subst_closed_neg_neg [lemma, in rules]
subst_closed_neg_and [lemma, in rules]
subst_closed_and [lemma, in rules]
subst_form_neg_box_v [lemma, in k_syntax]
subst_form_box_v [lemma, in k_syntax]
subst_k_rename_k_conclusion [lemma, in k_syntax]
subst_k_rename_k_assumption [lemma, in k_syntax]
subst_subst_of_fixed_map [lemma, in factor_subst]
subst_of_map [definition, in factor_subst]
subst_sequent_limit_eq [lemma, in substitution]
subst_eq_on_vars_limit [lemma, in substitution]
subst_sequent_eq [lemma, in substitution]
subst_modal_args_eq [lemma, in substitution]
subst_formula_eq [lemma, in substitution]
subst_eq_on_vars_append [lemma, in substitution]
subst_eq_on_vars_compose_right_change [lemma, in substitution]
subst_eq_on_vars_seq [lemma, in substitution]
subst_eq_on_vars_trans_rev [lemma, in substitution]
subst_eq_on_vars_trans [lemma, in substitution]
subst_eq_on_vars_symm [lemma, in substitution]
subst_eq_on_vars_empty [lemma, in substitution]
subst_eq_on_vars [definition, in substitution]
subst_closed_rule_set [definition, in substitution]
subst_sequent_rule [definition, in substitution]
subst_sequent_set_empty [lemma, in substitution]
subst_sequent_set [definition, in substitution]
subst_sequent_compose [lemma, in substitution]
subst_sequent_rank_increase [lemma, in substitution]
subst_sequent_append [lemma, in substitution]
subst_sequent_id [lemma, in substitution]
subst_sequent [definition, in substitution]
subst_compose_assoc [lemma, in substitution]
subst_compose_id_right [lemma, in substitution]
subst_form_compose [lemma, in substitution]
subst_compose [definition, in substitution]
subst_form_id [lemma, in substitution]
subst_form_rank_increase [lemma, in substitution]
subst_form_or [lemma, in substitution]
subst_form_char [lemma, in substitution]
subst_form [definition, in substitution]
subst_sequent_renamed_k_assumption [lemma, in k_semantics]
subst_eq_on_vars_compose_rename_change [lemma, in factor_two_subst]
subst_osr_conclusions_with_ax [definition, in complete]
subst_eq_on_vars_support [lemma, in sequent_support]
swap_pair [definition, in misc]
swap_pairs [definition, in lists]
syntactic_admissible_contraction [lemma, in syntactic_cut]
syntactic_admissible_cut [lemma, in syntactic_cut]
syntactic_GR_n_cc [lemma, in syntactic_cut]
syntactic_GR_n_cut_elimination [lemma, in syntactic_cut]
syntactic_GR_n_cut_head_elimination_ind [lemma, in syntactic_cut]
Syntactic_cut.v_eq [variable, in syntactic_cut]
Syntactic_cut.op_eq [variable, in syntactic_cut]
Syntactic_cut.L [variable, in syntactic_cut]
Syntactic_cut.V [variable, in syntactic_cut]
Syntactic_cut [section, in syntactic_cut]
syntactic_GR_n_provable_subst_Ax [lemma, in absorb]
syntactic_GR_n_non_atomic_axioms [lemma, in absorb]
syntactic_GR_n_cut_two_prop [lemma, in prop_cut]
syntactic_GR_n_cut_eli_two_osr [lemma, in osr_cut]
syntactic_GR_n_cut_eli_two_osr_concl [lemma, in osr_cut]
syntactic_GR_n_prove_cut_absorb_conclusion [lemma, in osr_cut]
syntactic_GR_n_prove_cut_absorb_assumptions [lemma, in osr_cut]
syntactic_GR_n_get_cut_rule [lemma, in osr_cut]
syntactic_support_contraction [lemma, in contraction]
syntactic_support_contraction_ind [lemma, in contraction]
syntactic_GR_n_contraction_ind [lemma, in contraction]
syntactic_cut [library]
T
tautology_witness [definition, in rules]terminal_seq_cone_property [lemma, in slice]
terminal_seq_cone [definition, in slice]
terminal_morph_sequence_char [lemma, in slice]
terminal_morph_sequence [definition, in slice]
terminal_obj_sequence_pi_2 [definition, in slice]
terminal_obj_sequence_pi_1_char [lemma, in slice]
terminal_obj_sequence_pi_1 [definition, in slice]
terminal_obj_sequence [definition, in slice]
top_modal_sequent_head [lemma, in modal_formulas]
top_modal_sequent_tail [lemma, in modal_formulas]
top_modal_is_prop_modal_sequent [lemma, in modal_formulas]
top_modal_sequent_list_reorder [lemma, in modal_formulas]
top_modal_sequent [definition, in modal_formulas]
top_modal_not_prop [lemma, in modal_formulas]
top_modal_not_neg_prop [lemma, in modal_formulas]
top_modal_form_lf_neg [lemma, in modal_formulas]
top_modal_is_prop_modal [lemma, in modal_formulas]
top_modal_form [definition, in modal_formulas]
top_mod_n_cut_free_completeness [lemma, in complete]
top_mod_n_completeness [lemma, in complete]
U
union [definition, in sets]union_comm [lemma, in sets]
union_double_neg_intersection [lemma, in classic]
union_set_inverse [lemma, in classic]
union_complement [lemma, in classic]
unique_form_greater [lemma, in factor_subst]
unit_coalg_seq_cone_identity [lemma, in slice]
unit_coalg_seq_cone_after_c [lemma, in slice]
unit_coalg_seq_cone [definition, in slice]
unit_coalg_sequence_char [lemma, in slice]
unit_coalg_sequence [definition, in slice]
unused_next_unused_var_left [lemma, in factor_two_subst]
unused_next_unused_var [lemma, in factor_two_subst]
unused_next_unused_var_ind [lemma, in factor_two_subst]
upward_step_correct_G [lemma, in step_semantics]
upward_step_correct_neg_neg [lemma, in step_semantics]
upward_step_correct_neg_and [lemma, in step_semantics]
upward_step_correct_and [lemma, in step_semantics]
upward_step_correct_ax [lemma, in step_semantics]
upward_step_correct_context [lemma, in step_semantics]
upward_step_correct_rule [definition, in step_semantics]
upward_correct_neg_neg [lemma, in propositional_completeness]
upward_propositional_bare_neg_neg [lemma, in propositional_completeness]
upward_propositional_bare_neg_neg_sequent [lemma, in propositional_completeness]
upward_correct_neg_and [lemma, in propositional_completeness]
upward_propositional_bare_neg_and [lemma, in propositional_completeness]
upward_propositional_bare_neg_and_sequent [lemma, in propositional_completeness]
upward_correct_and [lemma, in propositional_completeness]
upward_propositional_bare_and [lemma, in propositional_completeness]
upward_propositional_bare_and_right [lemma, in propositional_completeness]
upward_propositional_bare_and_left [lemma, in propositional_completeness]
upward_correct_ax [lemma, in propositional_completeness]
upward_correct_context [lemma, in propositional_completeness]
upward_correct_rule [definition, in propositional_completeness]
V
valid_all_states_reorder [lemma, in semantics]valid_all_states_append_right [lemma, in semantics]
valid_all_models [definition, in semantics]
valid_all_states_subst_change_coval [lemma, in semantics]
valid_all_states [definition, in semantics]
valid_subst_n_conclusions [definition, in one_step_conditions]
valid_simple_4_13_sequent_list_reorder [lemma, in complete]
valid_simple_4_13_sequent [definition, in complete]
var_chain_ends [definition, in factor_subst]
W
Weakening [section, in weakening]weakening [library]
weakening_admissible_GRC_n [lemma, in weakening]
weakening_admissible_GR [lemma, in weakening]
weakening_admissible_GR_n [lemma, in weakening]
weakening_admissible_Gn [lemma, in weakening]
Weakening.L [variable, in weakening]
Weakening.V [variable, in weakening]
Weakening.v_eq [variable, in weakening]
weaken_subst_rule_multiset [lemma, in rule_sets]
weaken_subst_rule [definition, in rule_sets]
weak_map_subst_correct_fix_var_chain_ends [lemma, in factor_subst]
well_founded_G_oracle [lemma, in build_prop_proof]
well_founded_neg_neg_rule [lemma, in build_prop_proof]
well_founded_neg_and_rule [lemma, in build_prop_proof]
well_founded_and_rule [lemma, in build_prop_proof]
well_founded_ax_rule [lemma, in build_prop_proof]
well_founded_rule_oracle [definition, in build_proof]
well_founded_rule [definition, in build_proof]
well_founded_Gn_oracle [lemma, in complete]
X
x_nat_functor [definition, in functor]other
_ ≡ _ (feq_scope) [notation, in functions]_ ∘ _ (feq_scope) [notation, in functions]
_ # _ /#\ _ (type_scope) [notation, in misc]
Notation Index
other
_ ≡ _ (feq_scope) [in functions]_ ∘ _ (feq_scope) [in functions]
_ # _ /#\ _ (type_scope) [in misc]
Variable Index
A
Absorbtion.L [in absorb]Absorbtion.op_eq [in absorb]
Absorbtion.V [in absorb]
Absorbtion.v_eq [in absorb]
Admissibility.hypotheses [in admissibility]
Admissibility.L [in admissibility]
Admissibility.rules [in admissibility]
Admissibility.V [in admissibility]
Assoc_2.aeq [in assoc]
Assoc_2.A [in assoc]
Assoc.A [in assoc]
Assoc.aeq [in assoc]
Assoc.B [in assoc]
Assoc.beq [in assoc]
B
Back_subst.v_eq [in backward_substitution]Back_subst.L [in backward_substitution]
Back_subst.V [in backward_substitution]
Build_prop_proof.v_eq [in build_prop_proof]
Build_prop_proof.L [in build_prop_proof]
Build_prop_proof.V [in build_prop_proof]
Build_proof.hypotheses [in build_proof]
Build_proof.rules [in build_proof]
Build_proof.L [in build_proof]
Build_proof.V [in build_proof]
C
CK.fun_ext [in ck]CK.pred_ext [in ck]
Classical_sets.A [in classic]
Completeness.L [in complete]
Completeness.T [in complete]
Completeness.V [in complete]
Completeness.v_eq [in complete]
Contraction_ind.v_eq [in contraction]
Contraction_ind.op_eq [in contraction]
Contraction_ind.L [in contraction]
Contraction_ind.V [in contraction]
Cut_properties.L [in cut_properties]
Cut_properties.V [in cut_properties]
D
Dep_lists.T [in dep_lists]Dep_lists.A [in dep_lists]
F
Factor_subst.v_eq [in factor_subst]Factor_subst.op_eq [in factor_subst]
Factor_subst.L [in factor_subst]
Factor_subst.V [in factor_subst]
Factor_two_subst.v_eq [in factor_two_subst]
Factor_two_subst.op_eq [in factor_two_subst]
Factor_two_subst.L [in factor_two_subst]
Factor_two_subst.V [in factor_two_subst]
Formulas.L [in formulas]
Formulas.V [in formulas]
G
Generic_cut.L [in generic_cut]Generic_cut.V [in generic_cut]
I
Image.A [in image]Image.B [in image]
Inversion.L [in inversion]
Inversion.V [in inversion]
Inversion.v_eq [in inversion]
K
K_sound.pred_ext [in k_sound_complete]K_sementics.pred_ext [in k_semantics]
L
ListSubset.A [in list_set]Lists0.A [in lists]
Lists1.A [in lists]
Lists2.A [in lists]
Lists3.A [in lists]
List_support.aeq [in list_support]
List_support.A [in list_support]
M
Mixed_cut.L [in mixed_cut]Mixed_cut.V [in mixed_cut]
Modal_formulas.v_eq [in modal_formulas]
Modal_formulas.L [in modal_formulas]
Modal_formulas.V [in modal_formulas]
Multisets.A [in list_multiset]
Multisets.aeq [in list_multiset]
O
One_step_conditions.v_eq [in one_step_conditions]One_step_conditions.T [in one_step_conditions]
One_step_conditions.L [in one_step_conditions]
One_step_conditions.V [in one_step_conditions]
OSR_cut.v_eq [in osr_cut]
OSR_cut.op_eq [in osr_cut]
OSR_cut.L [in osr_cut]
OSR_cut.V [in osr_cut]
P
Plain_prop_mod.L [in plain_prop_mod]Plain_prop_mod.V [in plain_prop_mod]
Propositional_soundness.L [in propositional_sound]
Propositional_soundness.V [in propositional_sound]
Propositional_formulas.L [in propositional_formulas]
Propositional_formulas.V [in propositional_formulas]
Propositional_rules.L [in propositional_rules]
Propositional_rules.V [in propositional_rules]
Propositional_models.L [in propositional_models]
Propositional_models.V [in propositional_models]
Propositional_Completeness.v_eq [in propositional_completeness]
Propositional_Completeness.L [in propositional_completeness]
Propositional_Completeness.V [in propositional_completeness]
Propositional_properties.L [in propositional_properties]
Propositional_properties.V [in propositional_properties]
Prop_mod.v_eq [in prop_mod]
Prop_mod.L [in prop_mod]
Prop_mod.V [in prop_mod]
Prop_cut.v_eq [in prop_cut]
Prop_cut.op_eq [in prop_cut]
Prop_cut.L [in prop_cut]
Prop_cut.V [in prop_cut]
R
Renaming.L [in renaming]Renaming.V [in renaming]
Renaming.v_eq [in renaming]
Reorder.A [in reorder]
Rules.L [in rules]
Rules.V [in rules]
Rule_sets.L [in rule_sets]
Rule_sets.V [in rule_sets]
S
Semantics.L [in semantics]Semantics.T [in semantics]
Semantics.V [in semantics]
Sequent_support.v_eq [in sequent_support]
Sequent_support.op_eq [in sequent_support]
Sequent_support.L [in sequent_support]
Sequent_support.V [in sequent_support]
Sets.A [in dsets]
Sets.A [in sets]
Slice.T [in slice]
Slice.V [in slice]
Some_nth.P [in some_nth]
Some_nth.A [in some_nth]
Some_neg_form.P_or_formula [in some_neg_form]
Some_neg_form.P_false [in some_neg_form]
Some_neg_form.P [in some_neg_form]
Some_neg_form.L [in some_neg_form]
Some_neg_form.V [in some_neg_form]
Some_neg_dep_form_2.P_false [in some_neg_form]
Some_neg_dep_form_2.P_or_formula [in some_neg_form]
Some_neg_dep_form_2.P_tcc_irr [in some_neg_form]
Some_neg_dep_form_2.form_prop_or_formula_of_sequent [in some_neg_form]
Some_neg_dep_form_2.form_prop_or [in some_neg_form]
Some_neg_dep_form_2.P [in some_neg_form]
Some_neg_dep_form_2.form_prop [in some_neg_form]
Some_neg_dep_form_2.L [in some_neg_form]
Some_neg_dep_form_2.V [in some_neg_form]
Some_neg_dep_form.P_or_formula [in some_neg_form]
Some_neg_dep_form.P_tcc_irr [in some_neg_form]
Some_neg_dep_form.form_prop_or_formula_of_sequent_iter [in some_neg_form]
Some_neg_dep_form.form_prop_or [in some_neg_form]
Some_neg_dep_form.P [in some_neg_form]
Some_neg_dep_form.form_prop [in some_neg_form]
Some_neg_dep_form.L [in some_neg_form]
Some_neg_dep_form.V [in some_neg_form]
Some_neg.P [in some_neg]
Some_neg.A [in some_neg]
Some_neg_dep.P_tcc_irr [in some_neg]
Some_neg_dep.P [in some_neg]
Some_neg_dep.aprop [in some_neg]
Some_neg_dep.A [in some_neg]
Soundness.L [in sound]
Soundness.T [in sound]
Soundness.V [in sound]
Step_semantics.T [in step_semantics]
Step_semantics.L [in step_semantics]
Step_semantics.V [in step_semantics]
Substitutions.L [in substitution]
Substitutions.V [in substitution]
Substitutions.v_eq [in substitution]
Syntactic_cut.v_eq [in syntactic_cut]
Syntactic_cut.op_eq [in syntactic_cut]
Syntactic_cut.L [in syntactic_cut]
Syntactic_cut.V [in syntactic_cut]
W
Weakening.L [in weakening]Weakening.V [in weakening]
Weakening.v_eq [in weakening]
Library Index
A
absorbadmissibility
all
assoc
B
backward_substitutionbuild_prop_proof
build_proof
C
castck
classic
complete
contraction
cut_properties
D
dep_listsdsets
F
factor_substfactor_two_subst
formulas
functions
functor
G
generic_cutI
imageinversion
K
k_sound_completek_nd
k_semantics
k_syntax
k_absorb
L
listslist_support
list_set
list_multiset
M
miscmixed_cut
modal_formulas
O
one_step_conditionsosr_cut
P
plain_prop_modpropositional_sound
propositional_formulas
propositional_properties
propositional_models
propositional_completeness
propositional_rules
prop_mod
prop_cut
R
renamingreorder
rules
rule_sets
S
semanticssequent_support
sets
slice
some_nth
some_neg_form
some_neg
sound
step_semantics
substitution
syntactic_cut
W
weakeningLemma Index
A
absorbs_contraction_head [in absorb]add_minus_diag [in misc]
admissible_depth_preserving_admissible [in admissibility]
admissible_prop [in admissibility]
admissible_bounded_cut_prop_G [in propositional_properties]
and_n_subset_G_n [in rule_sets]
and_rule_no_simple_modal_conclusion [in rule_sets]
and_oracle_some [in build_prop_proof]
and_oracle_tcc [in build_prop_proof]
and_rule_no_empty_conclusion [in rules]
and_rule_context [in rules]
append_single_rev [in lists]
apply_assoc_map_flatten [in assoc]
apply_assoc_map_append [in assoc]
apply_assoc_map_support [in assoc]
assoc_map_pair [in assoc]
assoc_swap_pairs [in assoc]
assoc_disjoint_keys_right_tail [in assoc]
assoc_In_rev [in assoc]
assoc_In [in assoc]
assoc_rassoc_inj_some [in assoc]
assoc_mapping_cons_first [in assoc]
assoc_mapping_tail [in assoc]
assoc_map_split [in assoc]
assoc_append_split [in assoc]
assoc_rassoc_some [in assoc]
assoc_cons_tail [in assoc]
assoc_cons_first [in assoc]
assoc_cons_split [in assoc]
assoc_mapping_join_subst_maps [in factor_two_subst]
assoc_mapping_rename_disjoint [in factor_two_subst]
assoc_mapping_rename_disjoint_ind [in factor_two_subst]
assumption_add_context_interpretation [in propositional_sound]
assumption_add_context_state_seq_semantics [in sound]
ax_n_subset_G_n [in rule_sets]
ax_rule_no_simple_modal_conclusion [in rule_sets]
ax_oracle_some [in build_prop_proof]
ax_oracle_tcc [in build_prop_proof]
ax_rule_subst [in rules]
ax_rule_no_empty_conclusion [in rules]
a_list_prop_first_or [in some_neg_form]
a_list_prop_tail [in some_neg]
B
bcontrapositive [in misc]bounded_head_weakening_admissible_GRC_n [in weakening]
bounded_head_weakening_admissible_cut [in weakening]
bounded_head_weakening_admissible_R [in weakening]
bounded_head_weakening_admissible_G_n_ind [in weakening]
bounded_head_weakening_admissible_G_n_step [in weakening]
bounded_head_weakening_admissible_neg_neg [in weakening]
bounded_head_weakening_admissible_neg_and [in weakening]
bounded_head_weakening_admissible_and [in weakening]
bounded_head_weakening_admissible_ax [in weakening]
bounded_weakening_provable_subst_n_conclusions [in weakening]
bounded_full_weakening [in rules]
bounded_weakening_closed_empty [in rules]
bounded_weakening_rules_multiset [in rules]
box_v_sequent_semantics_char [in k_semantics]
box_semantics [in k_semantics]
build_proof_right_property [in build_proof]
build_proof_right_result [in build_proof]
build_counter_model_correct [in propositional_completeness]
build_counter_model_const_v [in propositional_completeness]
build_counter_model_const_v_ind [in propositional_completeness]
C
change_rules_provability [in formulas]change_rules_hyp_provability [in formulas]
change_form_provable_subst_n_conclusion [in inversion]
change_sequent_provable_subst_n_conclusion [in inversion]
classic_axiom_sound_contraction [in classic]
classic_axiom_sound_cut_right [in classic]
classic_axiom_sound_cut_left [in classic]
classic_axiom_neg_disjunction_other_case [in classic]
classic_axiom_neg_and_or [in classic]
codom_map_cast [in cast]
collect_var_chain_ends_correct [in factor_subst]
collect_var_chain_ends_correct_ind [in factor_subst]
completeness [in complete]
congruence_assumptions_provable_with_ax [in absorb]
congruence_assumptions_subset [in absorb]
congruence_assumptions_char [in absorb]
conj_right_head_Gn_admissible [in inversion]
conj_left_head_Gn_admissible [in inversion]
const_rank_G_set [in rule_sets]
const_rank_GR [in weakening]
const_rank_R [in weakening]
const_rank_cut_rule_right [in rules]
const_rank_cut_rule_left [in rules]
const_rank_neg_neg_rule_context [in rules]
const_rank_neg_neg_rule [in rules]
const_rank_neg_and_rule_context [in rules]
const_rank_neg_and_rule [in rules]
const_rank_and_rule_right_context [in rules]
const_rank_and_rule_left_context [in rules]
const_rank_and_rule [in rules]
const_rank_add_context [in rules]
cons_nth_skipn [in lists]
context_inverted_neg_rule [in rules]
context_inverted_and_right_rule [in rules]
context_inverted_and_left_rule [in rules]
context_neg_neg_rule [in rules]
context_neg_and_rule [in rules]
context_and_rule [in rules]
contraction_rule_multiset [in rules]
contrapositive [in misc]
correct_rule_inductive_G [in propositional_completeness]
countably_infinite_non_empty [in misc]
counted_prop_list_valuation_semantics [in semantics]
counted_prop_list_valuation_tcc_irr [in semantics]
counted_list_equal [in misc]
counted_0_destruction [in misc]
counted_list_eta_1 [in misc]
counted_list_eta [in misc]
cutout_nth_cons_succ [in lists]
cutout_nth_cons_0 [in lists]
cut_rule_multiset [in rules]
cut_elimination_osr_context [in generic_cut]
cut_admissibile_from_head_elim [in generic_cut]
cut_free_completeness [in complete]
C_n_subset_GC_n [in rule_sets]
D
decompose_G_n_set [in rule_sets]decompose_G_n_set_coarsly [in rule_sets]
decrease_rank_R [in weakening]
delete_depth_admissible_rule [in admissibility]
depth_admissible_prop [in admissibility]
dep_list_proj_left_dep_map [in dep_lists]
dep_append_right [in some_neg]
dep_append_left [in some_neg]
destruct_neg_mod_sequent [in k_syntax]
destruct_neg_mod_form [in k_syntax]
destruct_mod_sequent [in k_syntax]
destruct_mod_form [in k_syntax]
destruct_neg_sequent [in k_syntax]
de_morgan_neg_and [in classic]
direct_image_left_adjoint [in image]
divide_subst_prop [in factor_subst]
dneg_or_elim [in misc]
dneg_or_intro [in misc]
dom_map_cast [in cast]
double_neg_impl_neg_or [in misc]
double_set_inverse [in sets]
double_set_inverse_rev [in classic]
double_neg_or [in classic]
downward_correct_GRC [in sound]
downward_correct_GR [in sound]
downward_correct_contraction [in sound]
downward_correct_one_step_rule [in sound]
E
eq_unequal [in misc]eq_equal [in misc]
evar_bug_list_weakening_admissible_GRC_n [in weakening]
every_nth_of_dep_list [in dep_lists]
every_nth_exists_inv [in dep_lists]
every_nth_exists_apply [in dep_lists]
every_nth_exists [in dep_lists]
every_dep_nth_dep_map_const [in dep_lists]
every_dep_nth_tail [in dep_lists]
every_dep_nth_head [in dep_lists]
every_dep_nth_cons [in dep_lists]
every_dep_nth_empty [in dep_lists]
every_nth_list_reorder [in reorder]
every_nth_map [in lists]
every_nth_cutout_nth [in lists]
every_nth_In_rev [in lists]
every_nth_In [in lists]
every_nth_append_right [in lists]
every_nth_append_left [in lists]
every_nth_append [in lists]
every_nth_cons [in lists]
every_nth_tail [in lists]
every_nth_head [in lists]
every_nth_mono [in lists]
every_nth_empty [in lists]
every_nth_list_support [in list_support]
every_nth_sequent_support [in sequent_support]
excluded_middle [in classic]
exists_not_not_implies [in misc]
F
factor_subst_property [in factor_subst]factor_two_subst_property [in factor_two_subst]
factor_two_subst_equal_2 [in factor_two_subst]
feq_ftimes_right [in functions]
feq_ftimes_left [in functions]
feq_ftimes_both [in functions]
feq_ftimes_compose_pair [in functions]
feq_ftimes_compose [in functions]
feq_ftimes_id [in functions]
feq_pair_right [in functions]
feq_pair_left [in functions]
feq_pair_both [in functions]
feq_pair_proj [in functions]
feq_right_compose_right [in functions]
feq_right_compose_left [in functions]
feq_left_compose_right [in functions]
feq_left_compose_left [in functions]
feq_compose_right_both [in functions]
feq_compose_left_both [in functions]
feq_compose_both [in functions]
feq_compose_associative_reverse [in functions]
feq_compose_associative [in functions]
feq_id_right [in functions]
feq_id_left [in functions]
feq_rw_r [in functions]
feq_eq [in functions]
feq_symmetric [in functions]
feq_transitive [in functions]
feq_reflexive [in functions]
feq_terminal_seq_cone [in slice]
feq_slice_final_map_coval [in slice]
feq_slice_map_T_compose [in slice]
feq_slice_map_T [in slice]
feq_direct_img [in image]
fibred_intersection [in image]
fibred_set_inverse [in image]
final_map_prop [in functions]
find_neg_neg_none [in build_prop_proof]
find_neg_neg_some [in build_prop_proof]
find_neg_neg_tcc_neg [in build_prop_proof]
find_neg_neg_tcc_neg_neg [in build_prop_proof]
find_neg_and_none [in build_prop_proof]
find_neg_and_some [in build_prop_proof]
find_neg_and_tcc_is_and [in build_prop_proof]
find_neg_and_tcc_is_neg [in build_prop_proof]
find_and_none [in build_prop_proof]
find_and_some [in build_prop_proof]
find_trivial_none [in build_prop_proof]
find_trivial_none_ind [in build_prop_proof]
find_trivial_some [in build_prop_proof]
find_trivial_some_ind [in build_prop_proof]
firstn_firstn_less [in lists]
firstn_append_right [in lists]
firstn_append_left [in lists]
firstn_whole [in lists]
fix_var_chain_ends_no_ends [in factor_subst]
flatten_map_singleton_id [in lists]
flatten_append [in lists]
fold_left_map [in lists]
forallb_every_nth [in lists]
forallb_cons [in lists]
forall_not_iff_not_exists [in misc]
formula_measure_char [in formulas]
formula_counter_model_correct [in propositional_completeness]
form_semantics_subst_change_coval [in semantics]
form_semantics_false [in semantics]
form_semantics_char [in semantics]
form_prop_or_formula_of_sequent_iter [in some_neg_form]
ftimes_def [in functions]
full_subset_full [in sets]
full_set_full [in sets]
full_weakening_rules_nonempty_conclusion [in rules]
full_weakening_rules_multiset [in rules]
function_update_split_result [in misc]
function_update_split [in misc]
function_update_twice [in misc]
function_update_unequal [in misc]
function_update_eq [in misc]
G
GC_n_subset_GRC_n [in rule_sets]GC_n_as_G_C_union [in rule_sets]
GC_n_multiset [in rule_sets]
GC_multiset [in rule_sets]
generic_bounded_list_weakening [in weakening]
generic_substitution_lemma [in cut_properties]
ge_refl [in misc]
GRC_n_as_GR_C_union [in rule_sets]
GRC_n_set_empty [in rule_sets]
GRC_n_set_struct_union [in rule_sets]
GRC_n_set_wo_ax_multiset [in rule_sets]
GRC_n_multiset [in rule_sets]
GRC_set_struct_union [in rule_sets]
GRC_set_wo_ax_multiset [in rule_sets]
GRC_multiset [in rule_sets]
GRC_n_substitution_lemma [in cut_properties]
GRC_1_is_GC_1 [in propositional_rules]
GR_n_subset_GRC_n [in rule_sets]
GR_subset_GRC [in rule_sets]
GR_n_set_struct_union [in rule_sets]
GR_n_multiset [in rule_sets]
GR_set_no_empty_conclusion [in rule_sets]
GR_set_struct_union [in rule_sets]
GR_set_wo_ax_multiset [in rule_sets]
GR_multiset [in rule_sets]
GR_n_provable_with_premises [in weakening]
GR_n_substitution_lemma_empty_hyp [in cut_properties]
GR_n_substitution_lemma [in cut_properties]
GR_n_non_atomic_axiom_head [in absorb]
GR_1_is_G_prop [in propositional_rules]
G_n_subset_GRC_n [in rule_sets]
G_n_subset_GR_n [in rule_sets]
G_subset_GR [in rule_sets]
G_n_subset_GC_n [in rule_sets]
G_n_set_no_simple_modal_conclusion [in rule_sets]
G_n_set_mono [in rule_sets]
G_n_multiset [in rule_sets]
G_set_no_empty_conclusion [in rule_sets]
G_rules_no_simple_modal_conclusion [in rule_sets]
G_multiset [in rule_sets]
G_struct_multiset [in rule_sets]
G_set_struct_union [in rule_sets]
G_set_prop_set [in propositional_rules]
G_n_cut_elim_head_neg_neg_outside [in propositional_properties]
G_n_cut_elim_head_neg_and_outside [in propositional_properties]
G_n_cut_elim_head_and_outside [in propositional_properties]
G_n_cut_elim_head_neg_neg_inside [in propositional_properties]
G_n_cut_elim_head_neg_and_inside [in propositional_properties]
G_n_cut_elim_head_and_inside [in propositional_properties]
G_n_cut_elim_head_ax [in propositional_properties]
G_n_hyp_list_contraction_left [in propositional_properties]
G_n_contraction_head [in propositional_properties]
G_n_contraction_neg_neg_assumptions_head [in propositional_properties]
G_n_contraction_neg_and_assumptions_head [in propositional_properties]
G_n_contraction_and_assumptions_head [in propositional_properties]
G_n_contraction_head_ax [in propositional_properties]
G_non_atomic_axiom_head [in propositional_properties]
H
head_inversion_provable_subst_n_conclusion [in inversion]head_inversion_closed_empty [in inversion]
head_contraction_closed_empty [in propositional_properties]
head_contraction_closed_provable_subst_n_conclusions_ind [in contraction]
I
iff_and [in misc]iff_neg [in misc]
iff_left [in misc]
iff_right [in misc]
incl_assoc_some [in assoc]
incl_prop_var_formula_sequent [in formulas]
incl_flatten_every [in list_set]
incl_rev [in list_set]
incl_list_reorder [in list_set]
incl_lappr [in list_set]
incl_lappl [in list_set]
incl_left_tail [in list_set]
incl_empty [in list_set]
injective_assoc_tail [in assoc]
injective_assoc_append [in assoc]
injective_assoc_cons_rassoc [in assoc]
injective_assoc_cons_different [in assoc]
injective_assoc_empty [in assoc]
injective_neg_box_v [in k_syntax]
injective_subst_of_fixed_map [in factor_subst]
injective_assoc_fix_var_chain_ends [in factor_subst]
injective_subst_neg_simple_modal [in modal_formulas]
injective_subst_simple_modal [in modal_formulas]
injective_subst_prop_form [in modal_formulas]
injective_assoc_join_subst_maps [in factor_two_subst]
injective_assoc_rename_disjoint [in factor_two_subst]
injective_assoc_rename_disjoint_ind [in factor_two_subst]
intersection_complement [in sets]
inversion_rules_nonempty_conclusion [in rules]
inversion_rules_multiset [in rules]
inversion_admissible_GR [in inversion]
inversion_admissible_GR_n [in inversion]
inversion_admissible_Gn_H [in inversion]
inversion_depth_preserving_admissible_Gn_H [in inversion]
inverted_neg_rule_context [in rules]
inverted_or_left_reordered_rule [in rules]
inverted_and_right_rule_context [in rules]
inverted_and_left_rule_context [in rules]
inv_proj_full [in image]
inv_img_compose [in image]
inv_img_id [in image]
In_apply_assoc_map_destruct [in assoc]
In_apply_assoc_map_non_member [in assoc]
In_apply_assoc_map_member [in assoc]
In_prop_var_sequent [in formulas]
In_remove_other [in lists]
In_nth_rev [in lists]
In_nth [in lists]
in_map_reverse [in lists]
In_flatten [in lists]
in_combine_same [in lists]
is_prop_model_or [in propositional_models]
is_prop_model_false [in propositional_models]
is_prop_model_tcc_irr [in propositional_models]
iter_obj_T_S_n [in slice]
J
join_subst_maps_equal_second_map [in factor_two_subst]join_subst_maps_contains_second_vars [in factor_two_subst]
join_subst_maps_correct_second_map [in factor_two_subst]
join_subst_maps_equal_first_map [in factor_two_subst]
join_subst_maps_contains_first_vars [in factor_two_subst]
join_subst_maps_subst_char [in factor_two_subst]
K
k_n_rule_eq_1 [in k_nd]k_nd_subset [in k_nd]
k_rename_fun_less [in k_syntax]
k_rules_rule [in k_syntax]
k_conclusion_nonempty [in k_syntax]
k_semantic_contraction [in k_sound_complete]
k_semantic_cut [in k_sound_complete]
k_complete [in k_sound_complete]
k_rules_one_step_cut_free_complete [in k_sound_complete]
k_rules_one_step_sound [in k_sound_complete]
k_syntactic_contraction [in k_absorb]
k_syntactic_cut [in k_absorb]
k_absorbs_cut [in k_absorb]
k_absorbs_contraction [in k_absorb]
k_absorbs_congruence [in k_absorb]
L
lambda_formula_rec_char [in formulas]lambda_formula_ind [in formulas]
lambda_formula_bool_char [in sequent_support]
length_list_of_counted_list [in misc]
length_dep_map_dep_const [in dep_lists]
length_k_conclusion [in k_syntax]
length_k_conclusion_tail [in k_syntax]
length_k_assumption [in k_syntax]
length_k_assumption_tail [in k_syntax]
length_subst_sequent [in substitution]
length_remove_In [in lists]
length_remove [in lists]
length_skipn [in lists]
length_firstn_less [in lists]
less_length_counted_list [in misc]
lf_modal_inversion_args [in formulas]
lf_modal_inversion_op [in formulas]
lift_p_tcc_irr [in some_neg]
lists_disjoint_right_cons [in list_set]
lists_disjoint_subset_right [in list_set]
lists_disjoint_symm [in list_set]
lists_disjoint_right_empty [in list_set]
list_of_counted_list_map [in misc]
list_weakening_admissible_GRC_n [in weakening]
list_weakening_admissible_GR_n [in weakening]
list_weakening_admissible_G_n_hyp [in weakening]
list_of_dep_list_dep_map_dep_dep [in dep_lists]
list_reorder_right_map [in reorder]
list_reorder_left_map [in reorder]
list_reorder_map [in reorder]
list_reorder_double_append [in reorder]
list_reorder_2_char [in reorder]
list_reorder_In_split [in reorder]
list_reorder_append_left [in reorder]
list_reorder_append_right [in reorder]
list_reorder_append_both [in reorder]
list_reorder_append_swap [in reorder]
list_reorder_append_3_middle [in reorder]
list_reorder_move_append [in reorder]
list_reorder_rot_3 [in reorder]
list_reorder_swap_head [in reorder]
list_reorder_first_occurence [in reorder]
list_reorder_nonempty [in reorder]
list_reorder_singleton [in reorder]
list_reorder_nil_is_nil [in reorder]
list_reorder_In [in reorder]
list_reorder_single_append [in reorder]
list_reorder_partition [in reorder]
list_reorder_inserted_2 [in reorder]
list_reorder_tail_head [in reorder]
list_reorder_tail [in reorder]
list_reorder_insert_list [in reorder]
list_reorder_insert [in reorder]
list_reorder_trans_rev [in reorder]
list_reorder_trans [in reorder]
list_reorder_occurence [in reorder]
list_reorder_occurence_full [in reorder]
list_reorder_symm [in reorder]
list_reorder_length [in reorder]
list_reorder_refl [in reorder]
list_reorder_cons_head [in reorder]
list_reorder_cons_parts [in reorder]
list_reorder_subst_sequent [in substitution]
list_subproofs_head_admissible [in inversion]
list_search_some_test [in lists]
list_search_some_less [in lists]
list_search_some [in lists]
list_search_some_ind [in lists]
list_search_none [in lists]
list_split_at_n2 [in lists]
list_split_n_equal [in lists]
list_split_at_n [in lists]
list_equal_nth_char [in lists]
list_support_map [in list_support]
list_support_reorder [in list_support]
list_support_same_set [in list_support]
list_support_head_contract [in list_support]
list_support_of_no_dup [in list_support]
list_support_destruct [in list_support]
list_support_incl [in list_support]
list_support_correct_subset [in list_support]
list_support_correct_content [in list_support]
list_support_correct_no_dup [in list_support]
list_reorder_incl_both [in list_set]
long_mod_seq_valid_char [in k_semantics]
M
map_subst_correct_fix_var_chain_ends [in factor_subst]map_rank_incl [in factor_subst]
map_rank_append [in factor_subst]
map_rank_In [in factor_subst]
map_rank_tail [in factor_subst]
map_rank_head [in factor_subst]
map_rank_cons [in factor_subst]
map_rank_empty [in factor_subst]
map_subst_correct_cons_smap [in factor_subst]
map_subst_correct_cons_rmap [in factor_subst]
map_subst_correct_empty [in factor_subst]
map_subst_sequent_limit_eq [in substitution]
map_id [in lists]
map_cutout_nth [in lists]
map_skipn [in lists]
map_firstn [in lists]
map_subst_correct_disjoint_keys [in factor_two_subst]
map_subst_correct_disjoint_keys_half [in factor_two_subst]
max_mono_both [in misc]
member_append_right [in lists]
member_append_left [in lists]
member_append [in lists]
member_In_false [in lists]
member_In [in lists]
minimal_proof_rank_char [in formulas]
minimal_rule_rank_conclusion [in formulas]
minimal_rule_rank_assumptions [in formulas]
minimal_rule_rank_gt_0 [in formulas]
minimal_sequent_rank_gt_0 [in formulas]
minimal_rank_simple_modal_sequent [in modal_formulas]
mixed_cut_right_osr [in mixed_cut]
mixed_cut_left_osr [in mixed_cut]
mixed_cut_ax [in mixed_cut]
modal_rank_ge_1 [in formulas]
modal_rank_char [in formulas]
mod_seq_val_valid_reorder [in semantics]
mod_val_pred_or [in semantics]
mod_val_pred_tcc_irr [in semantics]
mod_val_semantics_valid [in semantics]
mod_seq_val_valid_tcc_irr [in semantics]
mod_seq_val_tcc_irr [in semantics]
mod_arg_back_subst_sequent_prop [in backward_substitution]
mod_arg_back_subst_sequent_rec_prop [in backward_substitution]
mod_arg_back_subst_neg_form_prop [in backward_substitution]
mod_arg_back_subst_modal_form_prop [in backward_substitution]
mod_arg_back_subst_mod_args_prop [in backward_substitution]
mod_arg_back_subst_mod_args_prop_ind [in backward_substitution]
mod_seq_valid_k_conclusion_Sn [in k_semantics]
mod_seq_valid_k_conclusion_0 [in k_semantics]
multiset_rank_rules [in formulas]
multiset_provability [in formulas]
multiset_depth_provability [in formulas]
multiset_union [in formulas]
multiset_provable_subst_n_conclusions [in weakening]
multiset_valid_subst_n_conclusions [in one_step_conditions]
multi_subset_right_list_support [in list_support]
multi_subset_list_support [in list_support]
multi_subset_right_sequent_support [in sequent_support]
multi_subset_antisymm [in list_multiset]
multi_subset_trans [in list_multiset]
N
nat_list_max_lub [in lists]nat_list_max_le_inv [in lists]
nat_list_max_le [in lists]
nat_list_max_pairwise_le [in lists]
nat_list_sum_append [in lists]
neg_simple_modal_form_renaming [in renaming]
neg_double_neg [in misc]
neg_neg_implies [in misc]
neg_implies [in misc]
neg_is_none [in misc]
neg_neg_n_subset_G_n [in rule_sets]
neg_and_n_subset_G_n [in rule_sets]
neg_neg_rule_no_simple_modal_conclusion [in rule_sets]
neg_and_rule_no_simple_modal_conclusion [in rule_sets]
neg_neg_oracle_some [in build_prop_proof]
neg_neg_oracle_tcc [in build_prop_proof]
neg_and_oracle_some [in build_prop_proof]
neg_and_oracle_tcc [in build_prop_proof]
neg_form_is_neg [in formulas]
neg_neg_rule_no_empty_conclusion [in rules]
neg_neg_rule_context [in rules]
neg_and_rule_no_empty_conclusion [in rules]
neg_and_rule_context [in rules]
neg_sequent_subst_k_conclusion_tail [in k_syntax]
neg_sequent_subst_k_assumption_tail [in k_syntax]
neg_sequent_subst_sequent [in substitution]
neg_box_v_sequent_semantics_char [in k_semantics]
neg_v_sequent_double_neg_semantics [in k_semantics]
neg_inv_head_Gn_hyp_admissible [in inversion]
neg_inv_head_Gn_depth_admissible [in inversion]
neg_inv_head_Gn_depth_admissible_ind [in inversion]
neg_and_inv_head_G_n_hyp_admissible [in inversion]
neg_and_inv_head_Gn_depth_admissible [in inversion]
neg_and_inv_head_Gn_admissible_ind [in inversion]
neg_or_and_neg [in classic]
next_unused_var_fresh [in factor_two_subst]
NoDup_seq [in lists]
NoDup_map_injective [in lists]
NoDup_map [in lists]
NoDup_head [in lists]
NoDup_tail [in lists]
nonempty_rank_subst [in substitution]
nonempty_list_tcc [in lists]
nonempty_terminal_obj_sequence [in slice]
nonempty_slice_final [in slice]
non_empty_coalg [in functor]
non_decomposable_is_prop_mod [in prop_mod]
non_trivial_k_functor [in k_semantics]
non_modal_weaken_subst_formula [in inversion]
noprop_or_formula_of_sequnet [in some_neg_form]
noprop_or [in some_neg_form]
nth_counted_prop_list_valuation [in semantics]
nth_counted_prop_list_valuation_tcc [in semantics]
nth_step_semantics_args [in step_semantics]
nth_dep_map_dep_const_inv [in dep_lists]
nth_dep_map_dep_const_inv_tcc [in dep_lists]
nth_dep_map_dep_const [in dep_lists]
nth_dep_map_dep_const_tcc [in dep_lists]
nth_dep_nth_tcc_irr [in dep_lists]
nth_subst_k_conclusion_tail [in k_syntax]
nth_k_conclusion_tail [in k_syntax]
nth_subst_k_assumption_tail [in k_syntax]
nth_k_assumption_tail [in k_syntax]
nth_subst_sequent [in substitution]
nth_seq [in lists]
nth_map_inv [in lists]
nth_map_inv_tcc [in lists]
nth_map [in lists]
nth_map_tcc [in lists]
nth_skipn [in lists]
nth_skipn_tcc [in lists]
nth_firstn [in lists]
nth_firstn_tcc [in lists]
nth_append_right [in lists]
nth_append_right_ind [in lists]
nth_append_right_tcc [in lists]
nth_append_left [in lists]
nth_head_tcc [in lists]
nth_tcc_irr [in lists]
nth_tail [in lists]
nth_succ_tcc [in lists]
nth_0_nil_tcc [in lists]
n_cut_free_completeness [in complete]
n_completeness [in complete]
O
one_step_semantics_valid_propositional [in step_semantics]one_step_semantics_propositional [in step_semantics]
one_step_rule_nonempty_conclusion [in rule_sets]
one_step_rule_incl_prop_var_sequent [in rule_sets]
one_step_rule_prop_modal_prop_conclusion [in rule_sets]
one_step_rule_subst_top_modal_conclusion [in rule_sets]
one_step_rule_simple_modal_conclusion [in rule_sets]
one_step_rule_propositional_assumption [in rule_sets]
one_step_rule_multiset [in rule_sets]
one_step_rule_propositional_subst_assumptions [in absorb]
one_step_rule_simple_modal_conclusion_subst_reorder [in absorb]
one_step_rule_set_k_rules [in k_syntax]
option_contradiction [in misc]
or_neg_neg_and [in misc]
or_formula_of_sequent_nonempty [in formulas]
or_formula_of_ne_sequent_tcc_irr [in formulas]
or_formula_of_sequent_iter_rev [in formulas]
or_formula_of_sequent_iter_append [in formulas]
or_formula_subst_sequent [in substitution]
or_formula_subst_sequent_tcc [in substitution]
other_context_G_n_set [in rule_sets]
other_axiom_G_n_set [in inversion]
P
pair_compose_right [in functions]pair_proj_right [in functions]
pair_proj_left [in functions]
partition_result [in lists]
plain_prop_mod_subst_update [in plain_prop_mod]
plain_prop_mod_id_subst [in plain_prop_mod]
plug_empty_hypothesis_proof [in formulas]
plug_hypothesis_proof [in formulas]
plus_minus_assoc [in misc]
proof_set_equal_rules [in formulas]
proof_set_equal [in formulas]
proof_mono_rules [in formulas]
proof_mono_hyp [in formulas]
proof_mono [in formulas]
proof_depth_mono [in formulas]
proof_depth_sequent_ind [in formulas]
proof_sequent_ind [in formulas]
proof_ind [in formulas]
proof_depth_rule_1 [in formulas]
proof_depth_0 [in formulas]
proof_depth_rule_le_inv [in formulas]
proof_depth_rule_le [in formulas]
proof_depth_rule [in formulas]
proof_depth_assume [in formulas]
proof_rect_rule [in formulas]
proof_minimal_proof_rank [in cut_properties]
propositional_sound_G [in propositional_sound]
propositional_correct_G_derivation [in propositional_sound]
propositional_correct_derivation [in propositional_sound]
propositional_valuation_false [in semantics]
propositional_valuation_tcc_irr [in semantics]
propositional_renaming [in renaming]
propositional_sequent_cons_append [in propositional_formulas]
propositional_sequent_append_right [in propositional_formulas]
propositional_sequent_append_left [in propositional_formulas]
propositional_sequent_append [in propositional_formulas]
propositional_sequent_cons [in propositional_formulas]
propositional_or_formula [in propositional_formulas]
propositional_sequent_tail [in propositional_formulas]
propositional_sequent_head [in propositional_formulas]
propositional_sequent_empty [in propositional_formulas]
propositional_lambda_or [in propositional_formulas]
propositional_tcc_modal [in propositional_formulas]
propositional_and_right [in propositional_formulas]
propositional_and_left [in propositional_formulas]
propositional_lf_and [in propositional_formulas]
propositional_neg_inv [in propositional_formulas]
propositional_neg [in propositional_formulas]
propositional_lf_prop [in propositional_formulas]
propositional_renamed_one_step_assumptions [in one_step_conditions]
propositional_sequent_k_assumption [in k_syntax]
propositional_sequent_k_assumption_tail [in k_syntax]
propositional_neg_v [in k_syntax]
propositional_prop_G_set [in propositional_rules]
propositional_empty_sequent_set [in propositional_rules]
propositional_rule_add_context_bare_rule [in propositional_rules]
propositional_add_context_right [in propositional_rules]
propositional_add_context_left [in propositional_rules]
propositional_add_context_propositional [in propositional_rules]
propositional_add_context [in propositional_rules]
propositional_complete_G [in propositional_completeness]
propositional_cut_contraction_weakening [in propositional_properties]
prop_downward_correct_prop_G [in propositional_sound]
prop_downward_correct_neg_neg [in propositional_sound]
prop_downward_correct_neg_and [in propositional_sound]
prop_downward_correct_and [in propositional_sound]
prop_downward_correct_ax [in propositional_sound]
prop_downward_correct_context [in propositional_sound]
prop_downward_correct_rule_tcc_irr [in propositional_sound]
prop_modal_prop_semantics [in semantics]
prop_modal_prop_valuation_tcc_irr [in semantics]
prop_seq_val_valid_reorder [in semantics]
prop_val_pred_or [in semantics]
prop_val_pred_tcc_irr [in semantics]
prop_val_semantics_valid [in semantics]
prop_val_semantics [in semantics]
prop_seq_val_valid_tcc_irr [in semantics]
prop_seq_val_tcc_irr [in semantics]
prop_form_subst_neg_simple_modal_form [in renaming]
prop_form_subst_simple_modal_form [in renaming]
prop_sequent_renaming [in renaming]
prop_form_renaming [in renaming]
prop_neg_up_correct [in misc]
prop_neg_down_correct [in misc]
prop_or_up_correct [in misc]
prop_or_up_correct_context [in misc]
prop_or_down_correct [in misc]
prop_and_up_correct [in misc]
prop_and_down_correct [in misc]
prop_ax_up_correct [in misc]
prop_ax_down_correct [in misc]
prop_G_oracle_None_tautology [in build_prop_proof]
prop_G_oracle_None_simple [in build_prop_proof]
prop_G_oracle_None [in build_prop_proof]
prop_sequent_is_propositional [in propositional_formulas]
prop_form_is_propositional [in propositional_formulas]
prop_var_sequent_cutout_nth [in formulas]
prop_var_sequent_list_reorder [in formulas]
prop_var_sequent_append [in formulas]
prop_var_sequent_cons [in formulas]
prop_var_modal_args_cons [in formulas]
prop_var_formula_char [in formulas]
prop_sequent_list_reorder [in formulas]
prop_sequent_head [in formulas]
prop_sequent_tail [in formulas]
prop_sequent_cons [in formulas]
prop_form_acc_tcc_irr [in formulas]
prop_back_subst_form_prop [in backward_substitution]
prop_back_subst_form_prop_ind [in backward_substitution]
prop_var_list_below_append [in backward_substitution]
prop_var_list_below_empty [in backward_substitution]
prop_var_list_below_singleton [in backward_substitution]
prop_or_mod_partition [in prop_mod]
prop_or_mod_sequent_prop [in prop_mod]
prop_or_mod_sequent_append_right [in prop_mod]
prop_or_mod_sequent_append_left [in prop_mod]
prop_or_mod_sequent_list_reorder [in prop_mod]
prop_or_mod_sequent_cons [in prop_mod]
prop_or_mod_sequent_empty [in prop_mod]
prop_or_mod_formula_prop [in prop_mod]
prop_var_sequent_subst_k_conclusion_tail [in k_syntax]
prop_var_sequent_subst_k_conclusion_tail_ind [in k_syntax]
prop_var_sequent_k_conclusion [in k_syntax]
prop_modal_prop_sequent_k_conclusion [in k_syntax]
prop_var_sequent_k_assumption [in k_syntax]
prop_sequent_subst_k_assumption [in k_syntax]
prop_sequent_subst_k_assumption_tail [in k_syntax]
prop_sequent_k_assumption [in k_syntax]
prop_sequent_k_assumption_tail [in k_syntax]
prop_G_subset_prop_GC [in propositional_rules]
prop_G_subset_GRC [in propositional_rules]
prop_G_subset_GR [in propositional_rules]
prop_G_subset_Gn [in propositional_rules]
prop_sequent_rule_concl_tcc [in propositional_rules]
prop_sequent_rule_ass_tcc [in propositional_rules]
prop_seq_valid_k_assumption_Sn [in k_semantics]
prop_seq_valid_renamed_k_assumption_Sn [in k_semantics]
prop_seq_valid_renamed_k_assumption_0 [in k_semantics]
prop_seq_valid_k_assumption_0 [in k_semantics]
prop_model_sequent_interpretation [in propositional_models]
prop_sequent_interpretation_add_context_split [in propositional_models]
prop_sequent_interpretation_add_context [in propositional_models]
prop_sequent_interpretation_append_split [in propositional_models]
prop_sequent_interpretation_append [in propositional_models]
prop_sequent_interpretation_cons_cons_intro [in propositional_models]
prop_sequent_interpretation_cons_case_intro [in propositional_models]
prop_sequent_interpretation_length_case_intro [in propositional_models]
prop_sequent_interpretation_cons_cons_elim [in propositional_models]
prop_sequent_interpretation_cons_case_elim [in propositional_models]
prop_sequent_interpretation_nth_intro [in propositional_models]
prop_sequent_interpretation_singleton [in propositional_models]
prop_sequent_interpretation_empty [in propositional_models]
prop_sequent_interpretation_tcc_irr [in propositional_models]
prop_modal_sequent_tail [in modal_formulas]
prop_modal_sequent_head [in modal_formulas]
prop_modal_sequent_cons [in modal_formulas]
prop_modal_prop_or_formula [in modal_formulas]
prop_modal_prop_or_formula_iter [in modal_formulas]
prop_modal_prop_sequent_tail [in modal_formulas]
prop_modal_prop_sequent_head [in modal_formulas]
prop_modal_prop_sequent_cons [in modal_formulas]
prop_modal_prop_sequent_append_right [in modal_formulas]
prop_modal_prop_sequent_append_left [in modal_formulas]
prop_modal_prop_tcc_modal [in modal_formulas]
prop_modal_prop_tcc_and_2 [in modal_formulas]
prop_modal_prop_tcc_and_1 [in modal_formulas]
prop_modal_prop_tcc_neg [in modal_formulas]
prop_modal_prop_tcc_prop [in modal_formulas]
prop_modal_prop_lambda_or [in modal_formulas]
prop_var_sequent_subst_rename_of_map [in factor_two_subst]
prop_var_formula_subst_rename_of_map [in factor_two_subst]
prop_var_sequent_support [in k_absorb]
prop_mod_build_proof_left [in complete]
prop_3_2_1 [in propositional_completeness]
prop_correct_propositional [in propositional_completeness]
prop_G_cut_elim_head [in propositional_properties]
prop_G_cut_elim_head_ind [in propositional_properties]
prop_contraction_head [in propositional_properties]
provable_GRC_n_list_reorder [in rule_sets]
provable_GR_n_list_reorder [in rule_sets]
provable_GR_n_hyp_list_reorder [in rule_sets]
provable_with_cut [in rule_sets]
provable_with_neg_neg [in rule_sets]
provable_with_neg_and [in rule_sets]
provable_with_and [in rule_sets]
provable_G_n_list_reorder [in rule_sets]
provable_G_n_hyp_list_reorder [in rule_sets]
provable_depth_G_n_hyp_list_reorder [in rule_sets]
provable_rank_rules_has_rank_n [in formulas]
provable_rank_rules_hyp_has_rank_n [in formulas]
provable_at_depth_destruct [in formulas]
provable_at_depth_with_rule [in formulas]
provable_at_depth_0 [in formulas]
provable_at_depth_provable [in formulas]
provable_at_proof_depth [in formulas]
provable_with_rule [in formulas]
provable_with_assumption [in formulas]
provable_k_nd_hyp_list_reorder [in k_nd]
provable_sequent_axiom [in generic_cut]
provable_sequent_axiom_ind [in generic_cut]
provable_or_formula_of_ne_sequent [in generic_cut]
provable_GRC_n_GR_n_from_head_elim [in generic_cut]
provable_prop_G_hyp_list_reorder [in propositional_rules]
provable_depth_prop_list_reorder [in propositional_rules]
provable_subst_n_conclusions_rank_non_modal [in inversion]
provable_GRC_1_GR_1 [in propositional_properties]
provable_GC_1_G_1 [in propositional_properties]
provable_assumptions_contraction_rule [in contraction]
p_or_formula_of_sequent_iter [in some_neg_form]
R
rank_sequent_renaming [in renaming]rank_renaming [in renaming]
rank_subst_conclusion [in rule_sets]
rank_sequent_subst_nth_assumptions [in rule_sets]
rank_subst_assumptions [in rule_sets]
rank_G_n_inductive [in build_prop_proof]
rank_rules_ge_minimal [in formulas]
rank_rules_minimal_rule_rank [in formulas]
rank_rules_distribute_union [in formulas]
rank_rules_subset_rank [in formulas]
rank_rules_set_eq [in formulas]
rank_rules_mono [in formulas]
rank_sequent_set_sequent_list_set [in formulas]
rank_sequent_set_mono [in formulas]
rank_sequent_set_empty [in formulas]
rank_formula_modal_args_TCC [in formulas]
rank_formula_modal_1_TCC [in formulas]
rank_formula_modal_ge_2 [in formulas]
rank_sequent_ge_minimal [in formulas]
rank_sequent_le_minimal [in formulas]
rank_sequent_succ_minimal_nonempty_sequent_rank [in formulas]
rank_sequent_minimal_sequent_rank [in formulas]
rank_prop_sequent [in formulas]
rank_formula_or_formula_of_ne_sequent [in formulas]
rank_formula_succ_or_formula_of_sequent [in formulas]
rank_formula_or_formula_of_sequent [in formulas]
rank_formula_or_formula_iter_rev [in formulas]
rank_formula_or_formula_iter [in formulas]
rank_sequent_different_head [in formulas]
rank_sequent_append_right [in formulas]
rank_sequent_append_left [in formulas]
rank_sequent_append [in formulas]
rank_sequent_tail [in formulas]
rank_sequent_head [in formulas]
rank_sequent_cons [in formulas]
rank_sequent_empty [in formulas]
rank_sequent_list_reorder [in formulas]
rank_sequent_mono [in formulas]
rank_formula_modal [in formulas]
rank_formula_prop_form [in formulas]
rank_formula_lambda_or_rev [in formulas]
rank_formula_lambda_or [in formulas]
rank_formula_neg_and_over [in formulas]
rank_formula_neg_form_maybe [in formulas]
rank_formula_false [in formulas]
rank_formula_and_right [in formulas]
rank_formula_and_left [in formulas]
rank_formula_lf_and [in formulas]
rank_formula_lf_neg_TCC [in formulas]
rank_formula_lf_neg [in formulas]
rank_formula_lf_prop [in formulas]
rank_formula_ge [in formulas]
rank_formula_zero_TCC [in formulas]
rank_formula_zero [in formulas]
rank_sequent_set_provable_subst_n_conclusions [in weakening]
rank_proof_GR_fixed_rank [in weakening]
rank_sequent_osr_subst_conclusion [in weakening]
rank_proof_GR [in cut_properties]
rank_proof_GRC [in cut_properties]
rank_assumptions_bounded_weakening_rule [in rules]
rank_conclusion_bounded_weakening_rule [in rules]
rank_sequent_subst_Ax_set [in rules]
rank_rule_add_context_rev [in rules]
rank_sequent_set_congruence_assumptions [in absorb]
rank_sequent_set_valid_subst_n_conclusions [in one_step_conditions]
rank_subst_subst_of_fixed_map [in factor_subst]
rank_unique_form [in factor_subst]
rank_subst_limit_lf_modal [in substitution]
rank_subst_id_subst [in substitution]
rank_formula_id_subst [in substitution]
rank_subst_subst_compose [in substitution]
rank_sequent_subst_prop_sequent [in substitution]
rank_sequent_subst_add [in substitution]
rank_formula_subst_formula_add [in substitution]
rank_subst_update [in substitution]
rank_subst_ge [in substitution]
rank_sequent_prop_modal_prop_sequent [in modal_formulas]
rank_formula_prop_modal_prop [in modal_formulas]
rank_subst_limit_subst_rule [in modal_formulas]
rank_subst_limit_simple_modal_form [in modal_formulas]
rank_sequent_subst_simple_modal_sequent [in modal_formulas]
rank_simple_modal_sequent [in modal_formulas]
rank_formula_simple_modal_form [in modal_formulas]
rank_join_subst_maps [in factor_two_subst]
rank_sequent_sequent_support [in sequent_support]
rassoc_assoc_some [in assoc]
rassoc_assoc_none [in assoc]
rassoc_cons_tail [in assoc]
rassoc_cons_first [in assoc]
rassoc_cons_split [in assoc]
rename_of_id [in renaming]
rename_of_map_prop [in factor_subst]
rename_of_map_cons_split [in factor_subst]
rename_disjoint_compose_identity [in factor_two_subst]
rename_disjoint_values_not_in_source [in factor_two_subst]
rename_disjoint_disjoint [in factor_two_subst]
rename_disjoint_disjoint_ind [in factor_two_subst]
renaming_rename_of_fun [in renaming]
renaming_limit_subst_simple_modal_sequent [in renaming]
renaming_subst_compose [in renaming]
renaming_id_subst [in renaming]
renaming_rename_of_map [in factor_subst]
reorder_rule_add_context [in rules]
restricted_map_ext [in lists]
rule_multiset_k_nd [in k_nd]
rule_has_rank_subst_rule [in substitution]
R_n_subset_GRC_n [in rule_sets]
R_n_subset_GR_n [in rule_sets]
R_set_1_empty [in rule_sets]
R_set_no_empty_conclusion [in rule_sets]
S
scssv_4_13_nonempty_tcc [in step_semantics]semantics_step_semantics [in step_semantics]
semantic_admissible_contraction [in complete]
semantic_admissible_cut [in complete]
semantic_admissible_rules [in complete]
sequent_other_context_G_n_set [in rule_sets]
sequent_multiset_reordered_sequent_list_set [in formulas]
sequent_multiset_empty [in formulas]
sequent_measure_simple_context_lt [in formulas]
sequent_measure_context_lt [in formulas]
sequent_measure_append [in formulas]
sequent_measure_cons [in formulas]
sequent_other_axiom_G_n_set [in inversion]
sequent_support_subst_sequent [in sequent_support]
sequent_support_destruct [in sequent_support]
sequent_support_reorder [in sequent_support]
sequent_support_head_contract [in sequent_support]
sequent_support_incl [in sequent_support]
sequent_support_correct_subset [in sequent_support]
sequent_support_correct_content [in sequent_support]
sequent_support_correct_no_dup [in sequent_support]
set_equal_form_semantics_subst_change_coval [in semantics]
set_equal_multiset [in formulas]
set_inverse_intersection [in sets]
set_equal_rw_r [in sets]
set_equal_implies_subset [in sets]
set_equal_union_empty_right [in sets]
set_equal_union_subset_right [in sets]
set_equal_is_full [in sets]
set_equal_set_inverse [in sets]
set_equal_intersection [in sets]
set_equal_union [in sets]
set_equal_subset [in sets]
set_equal_subset_char [in sets]
set_equal_trans [in sets]
set_equal_symm [in sets]
set_equal_refl [in sets]
set_equal_inv_img_feq [in image]
set_equal_inv_img_pred [in image]
set_equal_inv_img [in image]
short_mod_seq_valid_char [in k_semantics]
simple_mod_seq_val_valid_correct [in semantics]
simple_mod_seq_val_length_case_intro [in semantics]
simple_mod_seq_val_append_right [in semantics]
simple_mod_seq_val_append_left [in semantics]
simple_mod_seq_val_tail [in semantics]
simple_mod_seq_val_head [in semantics]
simple_mod_seq_val_nth_intro [in semantics]
simple_mod_seq_val_tcc_irr [in semantics]
simple_prop_seq_val_valid_correct [in semantics]
simple_prop_seq_val_length_case_intro [in semantics]
simple_prop_seq_val_tail [in semantics]
simple_prop_seq_val_head [in semantics]
simple_prop_seq_val_tcc_irr [in semantics]
simple_modal_sequent_renaming [in renaming]
simple_modal_form_renaming [in renaming]
simple_tautology_contract_head [in rules]
simple_tautology_cons_destruct [in rules]
simple_tautology_append_right [in rules]
simple_tautology_reorder [in rules]
simple_tautology_tail [in rules]
simple_tautology_append_left [in rules]
simple_tautology_cons [in rules]
simple_modal_from_prop [in prop_mod]
simple_prop_from_prop [in prop_mod]
simple_one_step_cut_free_complete [in one_step_conditions]
simple_mod_weaken_rule_assumptions [in one_step_conditions]
simple_modal_sequent_subst_k_conclusion_tail [in k_syntax]
simple_modal_sequent_k_conclusion [in k_syntax]
simple_modal_sequent_k_conclusion_tail [in k_syntax]
simple_modal_neg_box_v [in k_syntax]
simple_modal_box_v [in k_syntax]
simple_prop_seq_val_k_assumption_head [in k_semantics]
simple_modal_sequent_is_prop_modal_prop [in modal_formulas]
simple_modal_form_is_prop_modal_prop [in modal_formulas]
simple_modal_sequent_partition [in modal_formulas]
simple_modal_sequent_cutout_nth [in modal_formulas]
simple_modal_sequent_list_reorder [in modal_formulas]
simple_modal_sequent_tail [in modal_formulas]
simple_modal_sequent_head [in modal_formulas]
simple_modal_sequent_cons [in modal_formulas]
simple_modal_sequent_append_right [in modal_formulas]
simple_modal_sequent_append_left [in modal_formulas]
simple_modal_sequent_append [in modal_formulas]
simple_modal_sequent_empty [in modal_formulas]
simple_tautology_cons_append [in propositional_completeness]
single_prop_ax_correct [in misc]
skipn_firstn [in lists]
skipn_skipn [in lists]
skipn_append_right [in lists]
skipn_append_left [in lists]
skipn_whole [in lists]
slice_model_nth_unit [in step_semantics]
slice_final_map_times_prop [in slice]
slice_final_map_pair_prop [in slice]
slice_final_map_id [in slice]
slice_obj_T_eq_lift_refl [in slice]
slice_obj_T_eq_lift [in slice]
slice_map_T_id [in slice]
smaller_context_G_n_set [in rule_sets]
some_nth_singleton [in some_nth]
some_nth_some [in some_nth]
some_neg_correct [in some_neg_form]
some_neg_dep_correct [in some_neg_form]
some_neg_dep_cons_correct [in some_neg_form]
some_neg_singleton [in some_neg]
some_neg_dep_map [in some_neg]
some_neg_dep_reorder [in some_neg]
some_neg_dep_tail [in some_neg]
some_neg_dep_append_left [in some_neg]
some_neg_dep_append_right [in some_neg]
some_neg_dep_append [in some_neg]
some_neg_dep_long_neg_intro [in some_neg]
some_neg_dep_cons_case_intro [in some_neg]
some_neg_dep_length_case_intro [in some_neg]
some_neg_dep_head [in some_neg]
some_neg_dep_cons_cons_elim [in some_neg]
some_neg_dep_cons_case_elim [in some_neg]
some_neg_dep_nth_intro [in some_neg]
some_neg_dep_singleton_rev [in some_neg]
some_neg_dep_singleton [in some_neg]
some_neg_dep_empty [in some_neg]
some_neg_dep_tcc_irr [in some_neg]
sound_k_GR [in k_sound_complete]
sound_k_GRC [in k_sound_complete]
sound_GR [in sound]
sound_GRC [in sound]
sound_derivation [in sound]
split_nat_case_le [in misc]
split_nat_case_lt [in misc]
split_prop_mod [in complete]
state_seq_semantics_valid [in semantics]
state_seq_semantics_correct [in semantics]
state_seq_semantics_reorder [in semantics]
state_seq_semantics_append_left [in semantics]
state_seq_semantics_append_right [in semantics]
state_seq_semantics_append [in semantics]
state_seq_semantics_length_case_intro [in semantics]
state_seq_semantics_cons_case_elim [in semantics]
state_seq_semantics_nth_intro [in semantics]
state_seq_semantics_singleton [in semantics]
state_seq_step_semantics_valid_correct [in step_semantics]
state_seq_step_semantics_correct [in step_semantics]
state_seq_step_form_pred_lambda_or [in step_semantics]
state_seq_step_semantics_long_neg_intro [in step_semantics]
state_seq_step_semantics_append_left [in step_semantics]
state_seq_step_semantics_append_right [in step_semantics]
state_seq_step_semantics_append [in step_semantics]
state_seq_step_semantics_list_reorder_rev [in step_semantics]
state_seq_step_semantics_list_reorder [in step_semantics]
state_seq_step_semantics_tcc_irr [in step_semantics]
step_prop_sequent_semantics [in step_semantics]
step_mod_sequent_semantics [in step_semantics]
step_semantics_valid_G_rule_inductive [in step_semantics]
step_semantics_sequent_append [in step_semantics]
step_semantics_valid_at_rank_list_reorder [in step_semantics]
step_semantics_valid_list_reorder [in step_semantics]
step_semantics_validity [in step_semantics]
step_semantics_valid_taut [in step_semantics]
step_semantics_valid_nonempty [in step_semantics]
step_semantics_valid_tcc_irr [in step_semantics]
step_semantics_sequent_empty [in step_semantics]
step_semantics_sequent_tcc_irr [in step_semantics]
step_semantics_false [in step_semantics]
step_semantics_lf_neg_rev [in step_semantics]
step_semantics_tcc_irr [in step_semantics]
step_semantics_tcc_irr_eq [in step_semantics]
step_semantics_modal [in step_semantics]
stratified_one_step_rules [in weakening]
strong_downward_correct_cut [in sound]
strong_downward_correct_neg_neg [in sound]
strong_downward_correct_neg_and [in sound]
strong_downward_correct_and [in sound]
strong_downward_correct_ax [in sound]
strong_downward_correct_context [in sound]
subproofs_head_admissible [in inversion]
subset_rank_rules [in formulas]
subset_empty_set [in sets]
subset_union_lub [in sets]
subset_union_both [in sets]
subset_union_right [in sets]
subset_union_left [in sets]
subset_add [in sets]
subset_trans [in sets]
subset_refl [in sets]
subst_coval_prop_step_semantics_valid [in step_semantics]
subst_coval_prop_step_semantics [in step_semantics]
subst_coval_modal_step_semantics_valid_for_4_13 [in step_semantics]
subst_coval_modal_step_semantics_valid [in step_semantics]
subst_coval_modal_step_semantics [in step_semantics]
subst_closed_GRC_set_wo_ax [in rule_sets]
subst_closed_GR_set_wo_ax [in rule_sets]
subst_closed_weaken_subst [in rule_sets]
subst_closed_G_struct_set [in rule_sets]
subst_eq_on_vars_below [in backward_substitution]
subst_cut_rule [in rules]
subst_closed_neg_neg [in rules]
subst_closed_neg_and [in rules]
subst_closed_and [in rules]
subst_form_neg_box_v [in k_syntax]
subst_form_box_v [in k_syntax]
subst_k_rename_k_conclusion [in k_syntax]
subst_k_rename_k_assumption [in k_syntax]
subst_subst_of_fixed_map [in factor_subst]
subst_sequent_limit_eq [in substitution]
subst_eq_on_vars_limit [in substitution]
subst_sequent_eq [in substitution]
subst_modal_args_eq [in substitution]
subst_formula_eq [in substitution]
subst_eq_on_vars_append [in substitution]
subst_eq_on_vars_compose_right_change [in substitution]
subst_eq_on_vars_seq [in substitution]
subst_eq_on_vars_trans_rev [in substitution]
subst_eq_on_vars_trans [in substitution]
subst_eq_on_vars_symm [in substitution]
subst_eq_on_vars_empty [in substitution]
subst_sequent_set_empty [in substitution]
subst_sequent_compose [in substitution]
subst_sequent_rank_increase [in substitution]
subst_sequent_append [in substitution]
subst_sequent_id [in substitution]
subst_compose_assoc [in substitution]
subst_compose_id_right [in substitution]
subst_form_compose [in substitution]
subst_form_id [in substitution]
subst_form_rank_increase [in substitution]
subst_form_or [in substitution]
subst_form_char [in substitution]
subst_sequent_renamed_k_assumption [in k_semantics]
subst_eq_on_vars_compose_rename_change [in factor_two_subst]
subst_eq_on_vars_support [in sequent_support]
syntactic_admissible_contraction [in syntactic_cut]
syntactic_admissible_cut [in syntactic_cut]
syntactic_GR_n_cc [in syntactic_cut]
syntactic_GR_n_cut_elimination [in syntactic_cut]
syntactic_GR_n_cut_head_elimination_ind [in syntactic_cut]
syntactic_GR_n_provable_subst_Ax [in absorb]
syntactic_GR_n_non_atomic_axioms [in absorb]
syntactic_GR_n_cut_two_prop [in prop_cut]
syntactic_GR_n_cut_eli_two_osr [in osr_cut]
syntactic_GR_n_cut_eli_two_osr_concl [in osr_cut]
syntactic_GR_n_prove_cut_absorb_conclusion [in osr_cut]
syntactic_GR_n_prove_cut_absorb_assumptions [in osr_cut]
syntactic_GR_n_get_cut_rule [in osr_cut]
syntactic_support_contraction [in contraction]
syntactic_support_contraction_ind [in contraction]
syntactic_GR_n_contraction_ind [in contraction]
T
terminal_seq_cone_property [in slice]terminal_morph_sequence_char [in slice]
terminal_obj_sequence_pi_1_char [in slice]
top_modal_sequent_head [in modal_formulas]
top_modal_sequent_tail [in modal_formulas]
top_modal_is_prop_modal_sequent [in modal_formulas]
top_modal_sequent_list_reorder [in modal_formulas]
top_modal_not_prop [in modal_formulas]
top_modal_not_neg_prop [in modal_formulas]
top_modal_form_lf_neg [in modal_formulas]
top_modal_is_prop_modal [in modal_formulas]
top_mod_n_cut_free_completeness [in complete]
top_mod_n_completeness [in complete]
U
union_comm [in sets]union_double_neg_intersection [in classic]
union_set_inverse [in classic]
union_complement [in classic]
unique_form_greater [in factor_subst]
unit_coalg_seq_cone_identity [in slice]
unit_coalg_seq_cone_after_c [in slice]
unit_coalg_sequence_char [in slice]
unused_next_unused_var_left [in factor_two_subst]
unused_next_unused_var [in factor_two_subst]
unused_next_unused_var_ind [in factor_two_subst]
upward_step_correct_G [in step_semantics]
upward_step_correct_neg_neg [in step_semantics]
upward_step_correct_neg_and [in step_semantics]
upward_step_correct_and [in step_semantics]
upward_step_correct_ax [in step_semantics]
upward_step_correct_context [in step_semantics]
upward_correct_neg_neg [in propositional_completeness]
upward_propositional_bare_neg_neg [in propositional_completeness]
upward_propositional_bare_neg_neg_sequent [in propositional_completeness]
upward_correct_neg_and [in propositional_completeness]
upward_propositional_bare_neg_and [in propositional_completeness]
upward_propositional_bare_neg_and_sequent [in propositional_completeness]
upward_correct_and [in propositional_completeness]
upward_propositional_bare_and [in propositional_completeness]
upward_propositional_bare_and_right [in propositional_completeness]
upward_propositional_bare_and_left [in propositional_completeness]
upward_correct_ax [in propositional_completeness]
upward_correct_context [in propositional_completeness]
V
valid_all_states_reorder [in semantics]valid_all_states_append_right [in semantics]
valid_all_states_subst_change_coval [in semantics]
valid_simple_4_13_sequent_list_reorder [in complete]
W
weakening_admissible_GRC_n [in weakening]weakening_admissible_GR [in weakening]
weakening_admissible_GR_n [in weakening]
weakening_admissible_Gn [in weakening]
weaken_subst_rule_multiset [in rule_sets]
weak_map_subst_correct_fix_var_chain_ends [in factor_subst]
well_founded_G_oracle [in build_prop_proof]
well_founded_neg_neg_rule [in build_prop_proof]
well_founded_neg_and_rule [in build_prop_proof]
well_founded_and_rule [in build_prop_proof]
well_founded_ax_rule [in build_prop_proof]
well_founded_Gn_oracle [in complete]
Constructor Index
A
assoc_mapping_cons [in assoc]assoc_mapping_nil [in assoc]
assume [in formulas]
B
box_op [in k_syntax]C
counted_cons [in misc]counted_nil [in misc]
D
dep_conj [in misc]dep_cons [in dep_lists]
dep_nil [in dep_lists]
L
lf_modal [in formulas]lf_and [in formulas]
lf_neg [in formulas]
lf_prop [in formulas]
list_reorder_cons [in reorder]
list_reorder_nil [in reorder]
R
rule [in formulas]Projection Index
A
arity [in formulas]assumptions [in formulas]
C
coalg [in semantics]comp_law [in functor]
conclusion [in formulas]
coval [in semantics]
F
fibred_semantics [in semantics]fmap [in functor]
fmap_feq_law [in functor]
I
id_law [in functor]M
modal_semantics [in semantics]O
obj [in functor]operator [in formulas]
S
set_equal_modal_semantics [in semantics]state [in semantics]
Inductive Index
A
assoc_mapping [in assoc]C
counted_list [in misc]D
dep_and [in misc]dep_list [in dep_lists]
K
k_operator [in k_syntax]L
lambda_formula [in formulas]list_reorder [in reorder]
P
proof [in formulas]Section Index
A
Absorbtion [in absorb]Admissibility [in admissibility]
Assoc [in assoc]
Assoc_2 [in assoc]
B
Back_subst [in backward_substitution]Build_prop_proof [in build_prop_proof]
Build_proof [in build_proof]
C
CK [in ck]Classical_sets [in classic]
Completeness [in complete]
Contraction_ind [in contraction]
Cut_properties [in cut_properties]
D
Dep_lists [in dep_lists]F
Factor_subst [in factor_subst]Factor_two_subst [in factor_two_subst]
Formulas [in formulas]
G
Generic_cut [in generic_cut]I
Image [in image]Inversion [in inversion]
K
K_nd [in k_nd]K_syntax [in k_syntax]
K_sound [in k_sound_complete]
K_sementics [in k_semantics]
K_absorb [in k_absorb]
L
ListSubset [in list_set]Lists0 [in lists]
Lists1 [in lists]
Lists2 [in lists]
Lists3 [in lists]
List_support [in list_support]
M
Mixed_cut [in mixed_cut]Modal_formulas [in modal_formulas]
Multisets [in list_multiset]
O
One_step_conditions [in one_step_conditions]OSR_cut [in osr_cut]
P
Plain_prop_mod [in plain_prop_mod]Propositional_soundness [in propositional_sound]
Propositional_formulas [in propositional_formulas]
Propositional_rules [in propositional_rules]
Propositional_models [in propositional_models]
Propositional_Completeness [in propositional_completeness]
Propositional_properties [in propositional_properties]
Prop_mod [in prop_mod]
Prop_cut [in prop_cut]
R
Renaming [in renaming]Reorder [in reorder]
Rules [in rules]
Rule_sets [in rule_sets]
S
Semantics [in semantics]Sequent_support [in sequent_support]
Sets [in dsets]
Sets [in sets]
Slice [in slice]
Some_nth [in some_nth]
Some_neg_form [in some_neg_form]
Some_neg_dep_form_2 [in some_neg_form]
Some_neg_dep_form [in some_neg_form]
Some_neg [in some_neg]
Some_neg_dep [in some_neg]
Soundness [in sound]
Step_semantics [in step_semantics]
Substitutions [in substitution]
Syntactic_cut [in syntactic_cut]
W
Weakening [in weakening]Definition Index
A
absorbs_cut [in absorb]absorbs_contraction [in absorb]
absorbs_congruence [in absorb]
add [in sets]
add_context [in rules]
admissible [in admissibility]
admissible_rule_set [in admissibility]
all_true_model [in propositional_completeness]
and_oracle [in build_prop_proof]
apply_assoc_map [in assoc]
apply_propositional_subproofs [in propositional_completeness]
assoc [in assoc]
assoc_disjoint_keys [in assoc]
ax_oracle [in build_prop_proof]
a_list_prop_head [in some_neg]
a_list_prop [in some_neg]
B
back_subst_result [in backward_substitution]bare_inverted_neg_rule [in rules]
bare_inverted_and_right_rule [in rules]
bare_inverted_and_left_rule [in rules]
bare_neg_neg_rule [in rules]
bare_neg_and_rule [in rules]
bare_and_rule [in rules]
bounded_weakening_closed [in rules]
bounded_weakening_rules [in rules]
bounded_cut_rules [in rules]
box [in k_syntax]
box_v [in k_syntax]
build_neg_neg_rule [in build_prop_proof]
build_neg_and_rule [in build_prop_proof]
build_and_rule [in build_prop_proof]
build_ax_rule [in build_prop_proof]
build_proof [in build_proof]
build_counter_model [in propositional_completeness]
C
ck_functor [in ck]classical_logic [in classic]
collect_var_chain_ends [in factor_subst]
congruence_assumptions [in absorb]
congruence_assumption_list [in absorb]
conj_head_inversion_closed [in inversion]
countably_infinite [in misc]
counted_prop_list_valuation [in semantics]
counted_map [in misc]
counted_head [in misc]
cutout_nth [in lists]
D
depth_preserving_admissible_rule_set [in admissibility]depth_preserving_admissible [in admissibility]
dep_list_of_every_nth [in dep_lists]
dep_list_proj_left [in dep_lists]
dep_map_dep_dep [in dep_lists]
dep_map_dep_const [in dep_lists]
dep_map_const_dep [in dep_lists]
dep_nth [in dep_lists]
dep_prop [in dep_lists]
direct_img [in image]
disj_head_inversion_closed [in inversion]
divide_subst [in factor_subst]
dneg_or [in misc]
dneg_form_maybe [in prop_mod]
downward_correct_rule_strengthen [in sound]
downward_correct_rule_set [in sound]
downward_correct_rule [in sound]
dprop_or_mod_sequent [in prop_mod]
dprop_or_mod_formula [in prop_mod]
dset [in dsets]
dunion [in dsets]
E
empty_sequent_set [in formulas]empty_set [in sets]
enumerator [in misc]
enum_infinite [in misc]
enum_elem [in misc]
eq_type [in misc]
every_dep_nth [in dep_lists]
every_nth [in lists]
F
factor_subst [in factor_subst]factor_two_subst [in factor_two_subst]
fcompose [in misc]
fcompose [in functions]
final_map [in functions]
find_neg_neg [in build_prop_proof]
find_neg_and [in build_prop_proof]
find_and [in build_prop_proof]
find_trivial [in build_prop_proof]
fix_var_chain_ends [in factor_subst]
flatten [in lists]
formula_measure [in formulas]
formula_counter_model [in propositional_completeness]
form_semantics [in semantics]
ftimes [in functions]
full_set [in sets]
full_weakening_closed [in rules]
full_weakening_rules [in rules]
function_update [in misc]
function_equal [in functions]
fun_codom_cast [in cast]
fun_dom_cast [in cast]
G
GC_n_set [in rule_sets]GC_set [in rule_sets]
get_modal_args [in formulas]
get_and_forms [in formulas]
get_neg_form [in formulas]
get_prop_var [in formulas]
GRC_n_set_wo_ax [in rule_sets]
GRC_n_set [in rule_sets]
GRC_set_wo_ax [in rule_sets]
GRC_set [in rule_sets]
GR_n_set [in rule_sets]
GR_set_wo_ax [in rule_sets]
GR_set [in rule_sets]
G_n_set [in rule_sets]
G_set [in rule_sets]
G_struct_set [in rule_sets]
H
head_inversion_closed [in inversion]head_contraction_closed [in propositional_properties]
hypotheses_oracle_type [in build_proof]
I
id [in functions]id_subst [in substitution]
injective [in misc]
injective_assoc [in assoc]
intersection [in sets]
inversion_rules [in rules]
inverted_neg_rule [in rules]
inverted_or_rule_multiset [in rules]
inverted_or_rule [in rules]
inverted_and_right_rule [in rules]
inverted_and_left_rule [in rules]
inv_img [in image]
is_inr [in misc]
is_inl [in misc]
is_none [in misc]
is_some [in misc]
is_neg_neg [in build_prop_proof]
is_neg_and [in build_prop_proof]
is_negated_prop [in build_prop_proof]
is_modal [in formulas]
is_and [in formulas]
is_neg [in formulas]
is_prop [in formulas]
is_full_set [in sets]
is_contraction_rule [in rules]
is_cut_rule [in rules]
is_neg_neg_rule [in rules]
is_neg_and_rule [in rules]
is_and_rule [in rules]
is_ax_rule [in rules]
is_prop_model [in propositional_models]
iter_fmap_T [in slice]
iter_obj_T [in slice]
J
join_subst_maps [in factor_two_subst]K
KL [in k_syntax]kop_eq [in k_syntax]
KV [in k_syntax]
kv_eq [in k_syntax]
kv_enum [in k_syntax]
k_nd_rules [in k_nd]
k_d_rule [in k_nd]
k_n_rule [in k_nd]
k_rename_fun [in k_syntax]
k_rules [in k_syntax]
k_rule [in k_syntax]
k_conclusion [in k_syntax]
k_conclusion_tail [in k_syntax]
k_assumption [in k_syntax]
k_assumption_tail [in k_syntax]
k_sequent [in k_syntax]
k_formulas [in k_syntax]
k_lambda [in k_semantics]
k_lifting [in k_semantics]
k_functor [in k_semantics]
L
lambda_structure_type [in semantics]lambda_false [in formulas]
lambda_or [in formulas]
lambda_formula_rec [in formulas]
lambda_formula_rect [in formulas]
lambda_subst [in substitution]
lambda_formula_eq [in sequent_support]
lambda_formula_bool [in sequent_support]
lift_p [in some_neg]
limit_subst [in substitution]
lists_disjoint [in list_set]
list_of_counted_list [in misc]
list_of_dep_list [in dep_lists]
list_search [in lists]
list_support [in list_support]
list_noprop [in some_neg]
M
make_unique_form [in factor_subst]map_rank [in factor_subst]
map_subst_correct [in factor_subst]
member [in lists]
minimal_proof_rank [in formulas]
minimal_rule_rank [in formulas]
minimal_sequent_rank [in formulas]
modal_subst_coval [in semantics]
modal_rank [in formulas]
modal_form [in modal_formulas]
mod_val_pred [in semantics]
mod_seq_val_valid [in semantics]
mod_seq_val [in semantics]
mod_arg_back_subst_sequent [in backward_substitution]
mod_arg_back_subst_sequent_rec [in backward_substitution]
mod_arg_back_subst_neg_mod_form [in backward_substitution]
mod_arg_back_subst_modal_form [in backward_substitution]
mod_arg_back_subst_mod_args [in backward_substitution]
mod_prop_hyp_oracle [in complete]
multi_subset [in list_multiset]
N
nat_list_max [in lists]nat_list_sum [in lists]
neg_neg_oracle [in build_prop_proof]
neg_and_oracle [in build_prop_proof]
neg_and_over [in formulas]
neg_form_maybe [in formulas]
neg_form [in formulas]
neg_box_v [in k_syntax]
neg_v [in k_syntax]
neg_head_inversion_closed [in inversion]
next_unused_var [in factor_two_subst]
nonempty_list [in lists]
non_trivial_functor [in functor]
non_empty_type [in misc]
noprop [in some_neg]
nth [in lists]
nth_unit_model [in step_semantics]
n_step_subst_coval [in step_semantics]
O
one_step_rule_set [in rule_sets]one_step_rule [in rule_sets]
one_step_cut_free_complete [in one_step_conditions]
one_step_complete [in one_step_conditions]
one_step_generic_complete [in one_step_conditions]
one_step_sound [in one_step_conditions]
or_formula_of_ne_sequent [in formulas]
or_formula_of_sequent [in formulas]
or_formula_of_sequent_iter [in formulas]
P
pair [in functions]plain_prop_mod_subst [in plain_prop_mod]
plain_prop_or_mod_formula [in plain_prop_mod]
proof_depth [in formulas]
proof_rect [in formulas]
propositional [in propositional_formulas]
propositional_valuation [in semantics]
propositional_sequent [in propositional_formulas]
propositional_rule_set [in propositional_rules]
propositional_sequent_set [in propositional_rules]
propositional_rule [in propositional_rules]
prop_downward_correct_rule_set [in propositional_sound]
prop_downward_correct_rule [in propositional_sound]
prop_proof_type [in propositional_sound]
prop_modal_prop_valuation [in semantics]
prop_val_pred [in semantics]
prop_seq_val_valid [in semantics]
prop_seq_val [in semantics]
prop_G_oracle [in build_prop_proof]
prop_var_sequent [in formulas]
prop_var_modal_args [in formulas]
prop_var_formula [in formulas]
prop_sequent [in formulas]
prop_form_acc [in formulas]
prop_form [in formulas]
prop_back_subst_form [in backward_substitution]
prop_back_subst_form_rec [in backward_substitution]
prop_var_list_below [in backward_substitution]
prop_or_mod_sequent [in prop_mod]
prop_or_mod_formula [in prop_mod]
prop_GC_set [in propositional_rules]
prop_G_set [in propositional_rules]
prop_sequent_interpretation [in propositional_models]
prop_valid_sequent [in propositional_models]
prop_valid [in propositional_models]
prop_model [in propositional_models]
prop_modal_sequent [in modal_formulas]
prop_modal [in modal_formulas]
prop_modal_prop_sequent [in modal_formulas]
prop_modal_prop [in modal_formulas]
prop_mod_build_proof [in complete]
prop_mod_build_proof_maybe [in complete]
prop_Gn_oracle [in complete]
prop_correct [in propositional_completeness]
prop_build_proof_prop [in propositional_completeness]
prop_build_proof_prop_type [in propositional_completeness]
prop_build_proof [in propositional_completeness]
prop_hyp_oracle [in propositional_completeness]
provable [in formulas]
provable_at_depth [in formulas]
provable_subst_n_conclusions [in weakening]
R
rank_rules [in formulas]rank_sequent_set [in formulas]
rank_sequent [in formulas]
rank_formula [in formulas]
rank_weaken_subst_rule [in weakening]
rank_subst [in substitution]
rassoc [in assoc]
rename_of_fun [in renaming]
rename_of_map [in factor_subst]
rename_disjoint [in factor_two_subst]
renaming [in renaming]
reordered_sequent_list_set [in formulas]
reordered_rule [in formulas]
restrict_hypothesis [in build_proof]
rule_oracle_G_property [in build_prop_proof]
rule_has_rank [in formulas]
rule_multiset [in formulas]
rule_add_context [in rules]
rule_inductive [in build_proof]
rule_oracle_type [in build_proof]
rule_oracle_result [in build_proof]
S
sequent [in formulas]sequent_multiset [in formulas]
sequent_measure [in formulas]
sequent_prop [in some_neg_form]
sequent_support [in sequent_support]
seq_semantics [in semantics]
set [in sets]
sets_containing [in sets]
set_equal [in sets]
set_inverse [in sets]
simple_mod_seq_val_valid [in semantics]
simple_mod_seq_val [in semantics]
simple_prop_seq_val_valid [in semantics]
simple_prop_seq_val [in semantics]
simple_tautology [in rules]
simple_tautology_witness [in rules]
simple_mod_weaken_rule [in one_step_conditions]
simple_modal_sequent [in modal_formulas]
simple_modal_form [in modal_formulas]
simple_4_13_sequent [in complete]
slice_model [in step_semantics]
slice_unit_coalg [in slice]
slice_final_map [in slice]
slice_final [in slice]
slice_map_T [in slice]
slice_obj_T [in slice]
some_nth [in some_nth]
some_neg_reorder [in some_neg]
some_neg_tail [in some_neg]
some_neg_append_left [in some_neg]
some_neg_append_right [in some_neg]
some_neg_append [in some_neg]
some_neg_long_neg_intro [in some_neg]
some_neg_cons_case_intro [in some_neg]
some_neg_length_case_intro [in some_neg]
some_neg_head [in some_neg]
some_neg_cons_case_elim [in some_neg]
some_neg_nth_intro [in some_neg]
some_neg_singleton_back [in some_neg]
some_neg_singleton_for [in some_neg]
some_neg_empty [in some_neg]
some_neg [in some_neg]
some_neg_dep [in some_neg]
state_seq_semantics [in semantics]
state_seq_step_semantics_valid [in step_semantics]
state_seq_step_semantics [in step_semantics]
state_seq_step_form_pred [in step_semantics]
step_semantics_valid_at_rank [in step_semantics]
step_semantics_valid [in step_semantics]
step_semantics_sequent [in step_semantics]
step_semantics_args [in step_semantics]
step_semantics [in step_semantics]
strong_downward_correct_rule [in sound]
subset [in sets]
subset_dep_prop [in dep_lists]
subst_coval [in semantics]
subst_equal_below_mono [in backward_substitution]
subst_equal_below_single_update [in backward_substitution]
subst_equal_below_trans [in backward_substitution]
subst_equal_below_refl [in backward_substitution]
subst_equal_below [in backward_substitution]
subst_Ax_n_set [in rules]
subst_Ax_set [in rules]
subst_of_map [in factor_subst]
subst_eq_on_vars [in substitution]
subst_closed_rule_set [in substitution]
subst_sequent_rule [in substitution]
subst_sequent_set [in substitution]
subst_sequent [in substitution]
subst_compose [in substitution]
subst_form [in substitution]
subst_osr_conclusions_with_ax [in complete]
swap_pair [in misc]
swap_pairs [in lists]
T
tautology_witness [in rules]terminal_seq_cone [in slice]
terminal_morph_sequence [in slice]
terminal_obj_sequence_pi_2 [in slice]
terminal_obj_sequence_pi_1 [in slice]
terminal_obj_sequence [in slice]
top_modal_sequent [in modal_formulas]
top_modal_form [in modal_formulas]
U
union [in sets]unit_coalg_seq_cone [in slice]
unit_coalg_sequence [in slice]
upward_step_correct_rule [in step_semantics]
upward_correct_rule [in propositional_completeness]
V
valid_all_models [in semantics]valid_all_states [in semantics]
valid_subst_n_conclusions [in one_step_conditions]
valid_simple_4_13_sequent [in complete]
var_chain_ends [in factor_subst]
W
weaken_subst_rule [in rule_sets]well_founded_rule_oracle [in build_proof]
well_founded_rule [in build_proof]
X
x_nat_functor [in functor]Record Index
F
functor [in functor]L
lambda_structure [in semantics]M
modal_operators [in formulas]model [in semantics]
S
sequent_rule [in formulas]| 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 | (2004 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 | (3 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 | (167 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 | (62 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 | (1264 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 | (16 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 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 | (8 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 | (64 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 | (400 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 | (5 entries) |
This page has been generated by coqdoc