| 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 | (1366 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 | (63 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (97 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 | (25 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 | (699 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 | (98 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (40 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 | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 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 | (217 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 | (12 entries) |
Global Index
A
absorp_Or2 [lemma, in FObiint.FOBIH_properties]absorp_Or1 [lemma, in FObiint.FOBIH_properties]
absorp_Or2 [lemma, in FOcdint.FOCDIH_properties]
absorp_Or1 [lemma, in FOcdint.FOCDIH_properties]
AccT [inductive, in General.genT]
AccT_sind [definition, in General.genT]
AccT_rec [definition, in General.genT]
AccT_ind [definition, in General.genT]
AccT_rect [definition, in General.genT]
AccT_intro [constructor, in General.genT]
add_remove_list_preserve_NoDup [lemma, in FOcdint.FO_CDInt_remove_list]
add_remove_list_preserve_NoDup [lemma, in FObiint.FO_BiInt_remove_list]
adj [abbreviation, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
adj [abbreviation, in FObiint.FOBIH_properties]
adj [abbreviation, in FOcdint.FO_CDInt_completeness]
adj [abbreviation, in FObiint.FO_BiInt_completeness]
adj [abbreviation, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
adj [abbreviation, in FOcdint.FOCDIH_properties]
adj [abbreviation, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
all_henk' [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
all_henk [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
all_henk' [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
all_henk [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
And_Imp [lemma, in FObiint.FOBIH_properties]
And_Imp [lemma, in FOcdint.FOCDIH_properties]
and_true [lemma, in General.gen]
anon [definition, in General.genT]
anonD [lemma, in General.genT]
anonI [lemma, in General.genT]
anon_forall [lemma, in General.genT]
anon_sigT [lemma, in General.genT]
anon_iffT [lemma, in General.genT]
anon_imp [lemma, in General.genT]
anon_sum [lemma, in General.genT]
anon_prod [lemma, in General.genT]
anon_eq [lemma, in General.genT]
appl [lemma, in General.gen]
app_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
app_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
arg_cong_imp' [lemma, in General.gen]
arg_cong_imp [lemma, in General.gen]
arg_cong [lemma, in General.gen]
arg1_cong_imp' [lemma, in General.gen]
arg1_cong_imp [lemma, in General.gen]
ar_preds [projection, in FOcdint.FO_CDInt_Syntax]
ar_syms [projection, in FOcdint.FO_CDInt_Syntax]
ar_preds [projection, in FObiint.FO_BiInt_Syntax]
ar_syms [projection, in FObiint.FO_BiInt_Syntax]
AThm_irrel [lemma, in FObiint.FOBIH_properties]
atom [constructor, in FOcdint.FO_CDInt_Syntax]
atom [constructor, in FObiint.FO_BiInt_Syntax]
atom_subst_Ax [lemma, in FOcdint.FO_CDInt_logic]
atom_subst_comp_strong [lemma, in FOcdint.FO_CDInt_Syntax]
atom_subst_comp [lemma, in FOcdint.FO_CDInt_Syntax]
atom_subst_id [lemma, in FOcdint.FO_CDInt_Syntax]
atom_subst_strong_to_normal [lemma, in FOcdint.FO_CDInt_Syntax]
atom_subst_respects_strong [definition, in FOcdint.FO_CDInt_Syntax]
atom_subst_respects [definition, in FOcdint.FO_CDInt_Syntax]
atom_subst [definition, in FOcdint.FO_CDInt_Syntax]
atom_inv [lemma, in FOcdint.FO_CDInt_Syntax]
atom_subst_Ax [lemma, in FObiint.FO_BiInt_logic]
atom_subst_comp_strong [lemma, in FObiint.FO_BiInt_Syntax]
atom_subst_comp [lemma, in FObiint.FO_BiInt_Syntax]
atom_subst_id [lemma, in FObiint.FO_BiInt_Syntax]
atom_subst_strong_to_normal [lemma, in FObiint.FO_BiInt_Syntax]
atom_subst_respects_strong [definition, in FObiint.FO_BiInt_Syntax]
atom_subst_respects [definition, in FObiint.FO_BiInt_Syntax]
atom_subst [definition, in FObiint.FO_BiInt_Syntax]
atom_inv [lemma, in FObiint.FO_BiInt_Syntax]
Ax [constructor, in FOcdint.FO_CDInt_GHC]
Ax [constructor, in FObiint.FO_BiInt_GHC]
Axioms [inductive, in FOcdint.FO_CDInt_GHC]
Axioms [inductive, in FObiint.FO_BiInt_GHC]
Axioms_sind [definition, in FOcdint.FO_CDInt_GHC]
Axioms_ind [definition, in FOcdint.FO_CDInt_GHC]
Axioms_sind [definition, in FObiint.FO_BiInt_GHC]
Axioms_ind [definition, in FObiint.FO_BiInt_GHC]
Ax_valid [lemma, in FOcdint.FO_CDInt_soundness]
Ax_valid [lemma, in FObiint.FO_BiInt_soundness]
A1 [constructor, in FOcdint.FO_CDInt_GHC]
A1 [constructor, in FObiint.FO_BiInt_GHC]
A2 [constructor, in FOcdint.FO_CDInt_GHC]
A2 [constructor, in FObiint.FO_BiInt_GHC]
A3 [constructor, in FOcdint.FO_CDInt_GHC]
A3 [constructor, in FObiint.FO_BiInt_GHC]
A4 [constructor, in FOcdint.FO_CDInt_GHC]
A4 [constructor, in FObiint.FO_BiInt_GHC]
A5 [constructor, in FOcdint.FO_CDInt_GHC]
A5 [constructor, in FObiint.FO_BiInt_GHC]
A6 [constructor, in FOcdint.FO_CDInt_GHC]
A6 [constructor, in FObiint.FO_BiInt_GHC]
A7 [constructor, in FOcdint.FO_CDInt_GHC]
A7 [constructor, in FObiint.FO_BiInt_GHC]
A8 [constructor, in FOcdint.FO_CDInt_GHC]
A8 [constructor, in FObiint.FO_BiInt_GHC]
A9 [constructor, in FOcdint.FO_CDInt_GHC]
A9 [constructor, in FObiint.FO_BiInt_GHC]
B
BA1 [constructor, in FObiint.FO_BiInt_GHC]BA2 [constructor, in FObiint.FO_BiInt_GHC]
BA3 [constructor, in FObiint.FO_BiInt_GHC]
BA4 [constructor, in FObiint.FO_BiInt_GHC]
biinterp [instance, in FOcdint.FO_CDInt_Conservativity]
bikmodel [instance, in FOcdint.FO_CDInt_Conservativity]
BiLEM [lemma, in FObiint.FOBIH_properties]
bin [constructor, in FOcdint.FO_CDInt_Syntax]
bin [constructor, in FObiint.FO_BiInt_Syntax]
binop [projection, in FOcdint.FO_CDInt_Syntax]
binop [projection, in FObiint.FO_BiInt_Syntax]
biΣ_preds [instance, in FOcdint.FO_CDInt_Conservativity]
biΣ_funcs [instance, in FOcdint.FO_CDInt_Conservativity]
bot [constructor, in FOcdint.FO_CDInt_Syntax]
bot [constructor, in FObiint.FO_BiInt_Syntax]
C
call_henk [projection, in FOcdint.FO_CDInt_completeness]call_henk [projection, in FObiint.FO_BiInt_completeness]
Canon_model [instance, in FOcdint.FO_CDInt_completeness]
Canon_model [instance, in FObiint.FO_BiInt_completeness]
cconsist [projection, in FOcdint.FO_CDInt_completeness]
cconsist [projection, in FObiint.FO_BiInt_completeness]
CD [constructor, in FOcdint.FO_CDInt_GHC]
cded_clos [projection, in FOcdint.FO_CDInt_completeness]
cded_clos [projection, in FObiint.FO_BiInt_completeness]
cex_henk [projection, in FOcdint.FO_CDInt_completeness]
cex_henk [projection, in FObiint.FO_BiInt_completeness]
closed [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
closed [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
closeder_fst_Lind_pair [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
closeder_fst_Lind_pair [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
closed_S [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
closed_L [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
closed_S [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
closed_L [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
comm_Or [lemma, in FObiint.FOBIH_properties]
comm_Or_obj [lemma, in FObiint.FOBIH_properties]
comm_And_obj [lemma, in FObiint.FOBIH_properties]
comm_Or [lemma, in FOcdint.FOCDIH_properties]
comm_Or_obj [lemma, in FOcdint.FOCDIH_properties]
comm_And_obj [lemma, in FOcdint.FOCDIH_properties]
Completeness [lemma, in FOcdint.FO_CDInt_completeness]
completeness [section, in FOcdint.FO_CDInt_completeness]
Completeness [lemma, in FObiint.FO_BiInt_completeness]
completeness [section, in FObiint.FO_BiInt_completeness]
completeness.eq_dec_funcs [variable, in FOcdint.FO_CDInt_completeness]
completeness.eq_dec_preds [variable, in FOcdint.FO_CDInt_completeness]
completeness.eq_dec_funcs [variable, in FObiint.FO_BiInt_completeness]
completeness.eq_dec_preds [variable, in FObiint.FO_BiInt_completeness]
completeness.form_index_inj [variable, in FOcdint.FO_CDInt_completeness]
completeness.form_enum_index [variable, in FOcdint.FO_CDInt_completeness]
completeness.form_index [variable, in FOcdint.FO_CDInt_completeness]
completeness.form_enum_unused [variable, in FOcdint.FO_CDInt_completeness]
completeness.form_enum_sur [variable, in FOcdint.FO_CDInt_completeness]
completeness.form_enum [variable, in FOcdint.FO_CDInt_completeness]
completeness.form_index_inj [variable, in FObiint.FO_BiInt_completeness]
completeness.form_enum_index [variable, in FObiint.FO_BiInt_completeness]
completeness.form_index [variable, in FObiint.FO_BiInt_completeness]
completeness.form_enum_unused [variable, in FObiint.FO_BiInt_completeness]
completeness.form_enum_sur [variable, in FObiint.FO_BiInt_completeness]
completeness.form_enum [variable, in FObiint.FO_BiInt_completeness]
completeness.SLEM [variable, in FOcdint.FO_CDInt_completeness]
completeness.SLEM [variable, in FObiint.FO_BiInt_completeness]
_ |- _ [notation, in FOcdint.FO_CDInt_completeness]
_ el _ [notation, in FOcdint.FO_CDInt_completeness]
_ |- _ [notation, in FObiint.FO_BiInt_completeness]
_ el _ [notation, in FObiint.FO_BiInt_completeness]
Conservativity [lemma, in FOcdint.FO_CDInt_Conservativity]
conservativity [section, in FOcdint.FO_CDInt_Conservativity]
conservativity.eq_dec_funcs [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.eq_dec_preds [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.form_index_inj [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum_unused [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum_index [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.form_index [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum_sur [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum [variable, in FOcdint.FO_CDInt_Conservativity]
conservativity.SLEM [variable, in FOcdint.FO_CDInt_Conservativity]
consist [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
consist [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Consist_extension_theory [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Consist_extension_theory_pair [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Consist_nextension_theory [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Consist_extension_theory [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Consist_extension_theory_pair [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Consist_nextension_theory [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Constant_Domain_Ax [lemma, in FObiint.FOBIH_properties]
Contr_Bot [lemma, in FObiint.FOBIH_properties]
Contr_Bot [lemma, in FOcdint.FOCDIH_properties]
cprime [projection, in FOcdint.FO_CDInt_completeness]
cprime [projection, in FObiint.FO_BiInt_completeness]
Cut [lemma, in FObiint.FOBIH_properties]
Cut [lemma, in FOcdint.FOCDIH_properties]
cwDownLind [lemma, in FObiint.FO_BiInt_completeness]
cworlds [record, in FOcdint.FO_CDInt_completeness]
cworlds [record, in FObiint.FO_BiInt_completeness]
cwTradLind [lemma, in FOcdint.FO_CDInt_completeness]
cwTradLind [lemma, in FObiint.FO_BiInt_completeness]
cwUpLind [lemma, in FOcdint.FO_CDInt_completeness]
cwUpLind [lemma, in FObiint.FO_BiInt_completeness]
cX [projection, in FOcdint.FO_CDInt_completeness]
cX [projection, in FObiint.FO_BiInt_completeness]
cycle_shift_shift [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
cycle_shift_subject [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
cycle_shift [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
cycle_shift_shift [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
cycle_shift_subject [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
cycle_shift [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
D
ded_clos [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]ded_clos [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
der_list_conj_finite_context [lemma, in FObiint.FOBIH_properties]
der_list_disj_bot [lemma, in FObiint.FOBIH_properties]
der_list_disj_remove2 [lemma, in FObiint.FOBIH_properties]
der_list_disj_remove1 [lemma, in FObiint.FOBIH_properties]
der_list_conj_finite_context [lemma, in FOcdint.FOCDIH_properties]
der_list_disj_bot [lemma, in FOcdint.FOCDIH_properties]
der_list_disj_remove2 [lemma, in FOcdint.FOCDIH_properties]
der_list_disj_remove1 [lemma, in FOcdint.FOCDIH_properties]
der_nextension_theory_mextension_theory_le [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
der_nextension_theory_mextension_theory_le [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
dext [definition, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_prime [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_consist [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_B0 [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_A0 [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_ded_clos [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_all_henk [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_ex_henk [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_el [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_nder [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_prv [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_der [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DN [constructor, in FObiint.FO_BiInt_GHC]
DN_to_form [lemma, in FObiint.FOBIH_properties]
DN_clos_set_sind [definition, in FObiint.FO_BiInt_Syntax]
DN_clos_set_ind [definition, in FObiint.FO_BiInt_Syntax]
DN_clos_set [inductive, in FObiint.FO_BiInt_Syntax]
DN_form [definition, in FObiint.FO_BiInt_Syntax]
double_remove [lemma, in FOcdint.FO_CDInt_remove_list]
double_remove [lemma, in FObiint.FO_BiInt_remove_list]
DownLind [section, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.w_nder [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.B0 [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.A0 [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wded_clos [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wprime [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wconsist [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wall_henk [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wex_henk [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.w [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr [section, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.eq_dec_funcs [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.eq_dec_preds [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_index_inj [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum_index [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_index [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum_unused [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum_sur [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.SLEM [variable, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
_ |- _ [notation, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
_ el _ [notation, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Down_Lindenbaum_lemma [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Dual_Constant_Domain [lemma, in FObiint.FOBIH_properties]
dual_MP [lemma, in FObiint.FOBIH_properties]
dual_residuation_gen [lemma, in FObiint.FOBIH_properties]
dual_residuation [lemma, in FObiint.FOBIH_properties]
dual_residuation_obj [lemma, in FObiint.FOBIH_properties]
E
EC [constructor, in FOcdint.FO_CDInt_GHC]EC [constructor, in FObiint.FO_BiInt_GHC]
EC_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
EC_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
EFQ [lemma, in FObiint.FOBIH_properties]
EFQ [lemma, in FOcdint.FOCDIH_properties]
embed [definition, in FOcdint.FO_CDInt_Conservativity]
embed_ksat [lemma, in FOcdint.FO_CDInt_Conservativity]
embed_eval [lemma, in FOcdint.FO_CDInt_Conservativity]
embed_S [definition, in FOcdint.FO_CDInt_Conservativity]
embed_quant [definition, in FOcdint.FO_CDInt_Conservativity]
embed_bin [definition, in FOcdint.FO_CDInt_Conservativity]
embed_term [definition, in FOcdint.FO_CDInt_Conservativity]
empty [inductive, in General.genT]
emptyT [inductive, in General.genT]
emptyT_any [lemma, in General.genT]
emptyT_any' [lemma, in General.genT]
emptyT_sind [definition, in General.genT]
emptyT_rec [definition, in General.genT]
emptyT_ind [definition, in General.genT]
emptyT_rect [definition, in General.genT]
empty_False [lemma, in General.genT]
empty_explosion [lemma, in General.genT]
empty_sind [definition, in General.genT]
empty_rec [definition, in General.genT]
empty_ind [definition, in General.genT]
empty_rect [definition, in General.genT]
empty_relT_sind [definition, in General.genT]
empty_relT_rec [definition, in General.genT]
empty_relT_ind [definition, in General.genT]
empty_relT_rect [definition, in General.genT]
empty_relT [inductive, in General.genT]
env [definition, in FObiint.FO_BiInt_Kripke_sem]
env [definition, in FOcdint.FO_CDInt_Kripke_sem]
EqDec [section, in FOcdint.FO_CDInt_Syntax]
EqDec [section, in FObiint.FO_BiInt_Syntax]
eq_dec_form [lemma, in FOcdint.FO_CDInt_Syntax]
eq_dec_term [lemma, in FOcdint.FO_CDInt_Syntax]
eq_dec_preserved_vector0 [lemma, in FOcdint.FO_CDInt_Syntax]
eq_dec_preserved_vector [lemma, in FOcdint.FO_CDInt_Syntax]
eq_dec_nat [lemma, in FOcdint.FO_CDInt_Syntax]
eq_S_F [lemma, in General.genT]
eq_dec_form [lemma, in FObiint.FO_BiInt_Syntax]
eq_dec_term [lemma, in FObiint.FO_BiInt_Syntax]
eq_dec_preserved_vector0 [lemma, in FObiint.FO_BiInt_Syntax]
eq_dec_preserved_vector [lemma, in FObiint.FO_BiInt_Syntax]
eq_dec_nat [lemma, in FObiint.FO_BiInt_Syntax]
eq_TrueI [lemma, in General.gen]
eval [definition, in FObiint.FO_BiInt_Kripke_sem]
eval [definition, in FOcdint.FO_CDInt_Kripke_sem]
eval_comp [lemma, in FObiint.FO_BiInt_Kripke_sem]
eval_ext [lemma, in FObiint.FO_BiInt_Kripke_sem]
eval_comp [lemma, in FOcdint.FO_CDInt_Kripke_sem]
eval_ext [lemma, in FOcdint.FO_CDInt_Kripke_sem]
existsT [library]
exist_unused_term_exists_First_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
exist_unused_term_exists_First_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
ext [definition, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext [definition, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
extension_theory_extens [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
extension_theory_extens_nextension [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
extension_theory [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
extension_theory_extens [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
extension_theory_extens_nextension [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
extension_theory [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
ext_prime [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_nel [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_nel' [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_consist [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_B0 [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_A0 [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_ded_clos [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_all_henk [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_ex_henk [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_el [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_nder [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_prv [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_der [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_prime [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_nel [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_nel' [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_consist [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_B0 [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_A0 [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_ded_clos [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_all_henk [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_ex_henk [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_el [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_nder [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_prv [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_der [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ex_henk [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
ex_henk [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
F
False_empty [lemma, in General.genT]false_or [lemma, in General.gen]
finite_context_list_conj [lemma, in FObiint.FOBIH_properties]
finite_context_list_conj [lemma, in FOcdint.FOCDIH_properties]
First_unused [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
First_unused [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
fix_signature [section, in FOcdint.FO_CDInt_Syntax]
fix_signature [section, in FOcdint.FO_CDInt_Syntax]
fix_signature [section, in FObiint.FO_BiInt_Syntax]
fix_signature [section, in FObiint.FO_BiInt_Syntax]
FOBIH [section, in FObiint.FO_BiInt_GHC]
FOBIH_Dual_Deduction_Theorem [lemma, in FObiint.FOBIH_properties]
FOBIH_Dual_Detachment_Theorem [lemma, in FObiint.FOBIH_properties]
FOBIH_Deduction_Theorem [lemma, in FObiint.FOBIH_properties]
FOBIH_Detachment_Theorem [lemma, in FObiint.FOBIH_properties]
FOBIH_prv_sind [definition, in FObiint.FO_BiInt_GHC]
FOBIH_prv_ind [definition, in FObiint.FO_BiInt_GHC]
FOBIH_prv [inductive, in FObiint.FO_BiInt_GHC]
FOBIH_finite [lemma, in FObiint.FO_BiInt_logic]
FOBIH_struct [lemma, in FObiint.FO_BiInt_logic]
FOBIH_comp [lemma, in FObiint.FO_BiInt_logic]
FOBIH_subst [lemma, in FObiint.FO_BiInt_logic]
FOBIH_monot [lemma, in FObiint.FO_BiInt_logic]
FOBIH_properties [library]
FOCDIH [section, in FOcdint.FO_CDInt_GHC]
FOCDIH_finite [lemma, in FOcdint.FO_CDInt_logic]
FOCDIH_struct [lemma, in FOcdint.FO_CDInt_logic]
FOCDIH_comp [lemma, in FOcdint.FO_CDInt_logic]
FOCDIH_subst [lemma, in FOcdint.FO_CDInt_logic]
FOCDIH_monot [lemma, in FOcdint.FO_CDInt_logic]
FOCDIH_prv_sind [definition, in FOcdint.FO_CDInt_GHC]
FOCDIH_prv_ind [definition, in FOcdint.FO_CDInt_GHC]
FOCDIH_prv [inductive, in FOcdint.FO_CDInt_GHC]
FOCDIH_Deduction_Theorem [lemma, in FOcdint.FOCDIH_properties]
FOCDIH_Detachment_Theorem [lemma, in FOcdint.FOCDIH_properties]
FOCDIH_properties [library]
Forall [inductive, in FOcdint.FO_CDInt_Syntax]
Forall [inductive, in FObiint.FO_BiInt_Syntax]
ForallT [inductive, in General.genT]
ForallTD_forall [definition, in General.genT]
ForallTI_forall [definition, in General.genT]
ForallT_Forall [lemma, in General.genT]
ForallT_Forall' [lemma, in General.genT]
ForallT_forall [lemma, in General.genT]
ForallT_impl [lemma, in General.genT]
ForallT_2I [definition, in General.genT]
ForallT_2I' [definition, in General.genT]
ForallT_D2 [definition, in General.genT]
ForallT_D1 [definition, in General.genT]
ForallT_2D [definition, in General.genT]
ForallT_map_rev [lemma, in General.genT]
ForallT_map [lemma, in General.genT]
ForallT_map_2 [lemma, in General.genT]
ForallT_2 [lemma, in General.genT]
ForallT_appendI [definition, in General.genT]
ForallT_appendI' [definition, in General.genT]
ForallT_appendD2 [definition, in General.genT]
ForallT_appendD1 [definition, in General.genT]
ForallT_appendD [definition, in General.genT]
ForallT_append [lemma, in General.genT]
ForallT_cons_iff [lemma, in General.genT]
ForallT_singleI [definition, in General.genT]
ForallT_singleD [definition, in General.genT]
ForallT_single [lemma, in General.genT]
ForallT_cons_inv [lemma, in General.genT]
ForallT_inv [lemma, in General.genT]
ForallT_sind [definition, in General.genT]
ForallT_rec [definition, in General.genT]
ForallT_ind [definition, in General.genT]
ForallT_rect [definition, in General.genT]
ForallT_cons [constructor, in General.genT]
ForallT_nil [constructor, in General.genT]
Forall_sind [definition, in FOcdint.FO_CDInt_Syntax]
Forall_rec [definition, in FOcdint.FO_CDInt_Syntax]
Forall_ind [definition, in FOcdint.FO_CDInt_Syntax]
Forall_rect [definition, in FOcdint.FO_CDInt_Syntax]
Forall_cons [constructor, in FOcdint.FO_CDInt_Syntax]
Forall_nil [constructor, in FOcdint.FO_CDInt_Syntax]
forall_list_disj [lemma, in FObiint.FOBIH_properties]
Forall_ForallT' [lemma, in General.genT]
Forall_ForallT [lemma, in General.genT]
Forall_sind [definition, in FObiint.FO_BiInt_Syntax]
Forall_rec [definition, in FObiint.FO_BiInt_Syntax]
Forall_ind [definition, in FObiint.FO_BiInt_Syntax]
Forall_rect [definition, in FObiint.FO_BiInt_Syntax]
Forall_cons [constructor, in FObiint.FO_BiInt_Syntax]
Forall_nil [constructor, in FObiint.FO_BiInt_Syntax]
forall_list_disj [lemma, in FOcdint.FOCDIH_properties]
Forall_map_2 [lemma, in General.gen]
Forall_map_single [lemma, in General.gen]
Forall_single [lemma, in General.gen]
Forall_append [lemma, in General.gen]
Forall_cons_iff [lemma, in General.gen]
Forall_cons_inv [lemma, in General.gen]
Forall2T [inductive, in General.genT]
Forall2T_ex_r [lemma, in General.genT]
Forall2T_ex_l [lemma, in General.genT]
Forall2T_app [lemma, in General.genT]
Forall2T_app_inv_r [lemma, in General.genT]
Forall2T_app_inv_l [lemma, in General.genT]
Forall2T_sind [definition, in General.genT]
Forall2T_rec [definition, in General.genT]
Forall2T_ind [definition, in General.genT]
Forall2T_rect [definition, in General.genT]
Forall2T_cons [constructor, in General.genT]
Forall2T_nil [constructor, in General.genT]
form [inductive, in FOcdint.FO_CDInt_Syntax]
form [inductive, in FObiint.FO_BiInt_Syntax]
form_ex [lemma, in FOcdint.FO_CDInt_Syntax]
form_all [lemma, in FOcdint.FO_CDInt_Syntax]
form_subst_help [lemma, in FOcdint.FO_CDInt_Syntax]
form_ind_subst [lemma, in FOcdint.FO_CDInt_Syntax]
form_sind [definition, in FOcdint.FO_CDInt_Syntax]
form_rec [definition, in FOcdint.FO_CDInt_Syntax]
form_ind [definition, in FOcdint.FO_CDInt_Syntax]
form_rect [definition, in FOcdint.FO_CDInt_Syntax]
form_ex [lemma, in FObiint.FO_BiInt_Syntax]
form_all [lemma, in FObiint.FO_BiInt_Syntax]
form_subst_help [lemma, in FObiint.FO_BiInt_Syntax]
form_ind_subst [lemma, in FObiint.FO_BiInt_Syntax]
form_sind [definition, in FObiint.FO_BiInt_Syntax]
form_rec [definition, in FObiint.FO_BiInt_Syntax]
form_ind [definition, in FObiint.FO_BiInt_Syntax]
form_rect [definition, in FObiint.FO_BiInt_Syntax]
form_index_In_L_or_R [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_index_inj [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_exists_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_index_In_L_or_R [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
form_index_inj [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
form_exists_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
form_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
form' [definition, in FOcdint.FO_CDInt_Conservativity]
FO_BiInt_Syntax [library]
FO_BiInt_Kripke_sem [library]
FO_CDInt_GHC [library]
FO_BiInt_remove_list [library]
FO_BiInt_GHC [library]
FO_CDInt_logic [library]
FO_CDInt_Stand_Lindenbaum_lem [library]
FO_CDInt_Conservativity [library]
FO_BiInt_Stand_Lindenbaum_lem [library]
FO_BiInt_completeness [library]
FO_CDInt_soundness [library]
FO_CDInt_Up_Lindenbaum_lem [library]
FO_BiInt_Down_Lindenbaum_lem [library]
FO_CDInt_completeness [library]
FO_BiInt_Up_Lindenbaum_lem [library]
FO_BiInt_logic [library]
FO_CDInt_Syntax [library]
FO_CDInt_remove_list [library]
FO_CDInt_Kripke_sem [library]
FO_BiInt_soundness [library]
FullSyntax [module, in FOcdint.FO_CDInt_Syntax]
FullSyntax [module, in FObiint.FO_BiInt_Syntax]
FullSyntax.All [constructor, in FOcdint.FO_CDInt_Syntax]
FullSyntax.All [constructor, in FObiint.FO_BiInt_Syntax]
FullSyntax.Conj [constructor, in FOcdint.FO_CDInt_Syntax]
FullSyntax.Conj [constructor, in FObiint.FO_BiInt_Syntax]
FullSyntax.Disj [constructor, in FOcdint.FO_CDInt_Syntax]
FullSyntax.Disj [constructor, in FObiint.FO_BiInt_Syntax]
FullSyntax.Ex [constructor, in FOcdint.FO_CDInt_Syntax]
FullSyntax.Ex [constructor, in FObiint.FO_BiInt_Syntax]
FullSyntax.Excl [constructor, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_operators [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_sind [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_rec [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_ind [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_rect [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant [inductive, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_sind [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_rec [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_ind [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_rect [definition, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym [inductive, in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_operators [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_sind [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_rec [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_ind [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_rect [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant [inductive, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_sind [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_rec [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_ind [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_rect [definition, in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym [inductive, in FObiint.FO_BiInt_Syntax]
FullSyntax.Impl [constructor, in FOcdint.FO_CDInt_Syntax]
FullSyntax.Impl [constructor, in FObiint.FO_BiInt_Syntax]
_ <--> _ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
_ --> _ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
_ ∨ _ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
_ ∧ _ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
_ <--> _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
_ --< _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
_ --> _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
_ ∨ _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
_ ∧ _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
¬ _ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
¬ _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
∀ _ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
∀ _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
∃ _ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
∃ _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
∞ _ (syn) [notation, in FObiint.FO_BiInt_Syntax]
⊤ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
⊤ (syn) [notation, in FObiint.FO_BiInt_Syntax]
⊥ (syn) [notation, in FOcdint.FO_CDInt_Syntax]
⊥ (syn) [notation, in FObiint.FO_BiInt_Syntax]
func [constructor, in FOcdint.FO_CDInt_Syntax]
func [constructor, in FObiint.FO_BiInt_Syntax]
funcomp [definition, in FOcdint.FO_CDInt_Syntax]
funcomp [definition, in FObiint.FO_BiInt_Syntax]
funcs_signature [record, in FOcdint.FO_CDInt_Syntax]
funcs_signature [record, in FObiint.FO_BiInt_Syntax]
func_inv [lemma, in FOcdint.FO_CDInt_Syntax]
func_inv [lemma, in FObiint.FO_BiInt_Syntax]
fun_cong [lemma, in General.gen]
G
Gen [constructor, in FOcdint.FO_CDInt_GHC]Gen [constructor, in FObiint.FO_BiInt_GHC]
gen [library]
genT [library]
gen_FOBIH_Dual_Deduction_Theorem [lemma, in FObiint.FOBIH_properties]
gen_FOBIH_Dual_Detachment_Theorem [lemma, in FObiint.FOBIH_properties]
gen_FOBIH_Deduction_Theorem [lemma, in FObiint.FOBIH_properties]
gen_FOBIH_Detachment_Theorem [lemma, in FObiint.FOBIH_properties]
gen_FOCDIH_Deduction_Theorem [lemma, in FOcdint.FOCDIH_properties]
gen_FOCDIH_Detachment_Theorem [lemma, in FOcdint.FOCDIH_properties]
gen_choice_code [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Gen_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
gen_choice_code [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Gen_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
gen_cong [lemma, in General.gen]
I
Id [constructor, in FOcdint.FO_CDInt_GHC]Id [constructor, in FObiint.FO_BiInt_GHC]
Id_list_disj_remove [lemma, in FObiint.FOBIH_properties]
Id_list_disj [lemma, in FObiint.FOBIH_properties]
Id_list_disj_remove [lemma, in FOcdint.FOCDIH_properties]
Id_list_disj [lemma, in FOcdint.FOCDIH_properties]
iffD1 [lemma, in General.gen]
iffD2 [lemma, in General.gen]
iffT_prod [lemma, in General.genT]
iffT_D2 [definition, in General.genT]
iffT_D1 [definition, in General.genT]
iffT_sym [definition, in General.genT]
iffT_D2' [lemma, in General.genT]
iffT_D1' [lemma, in General.genT]
iffT_refl [lemma, in General.genT]
iffT_sym' [lemma, in General.genT]
iffT_trans [lemma, in General.genT]
Imp_And [lemma, in FObiint.FOBIH_properties]
Imp_trans [lemma, in FObiint.FOBIH_properties]
Imp_trans_help427 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help410 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help170 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help54 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help37 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help35 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help14 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help9 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help8 [lemma, in FObiint.FOBIH_properties]
Imp_trans_help7 [lemma, in FObiint.FOBIH_properties]
imp_Id_gen [lemma, in FObiint.FOBIH_properties]
Imp_And [lemma, in FOcdint.FOCDIH_properties]
Imp_trans [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help427 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help410 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help170 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help54 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help37 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help35 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help14 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help9 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help8 [lemma, in FOcdint.FOCDIH_properties]
Imp_trans_help7 [lemma, in FOcdint.FOCDIH_properties]
imp_Id_gen [lemma, in FOcdint.FOCDIH_properties]
IndClo [constructor, in FObiint.FO_BiInt_Syntax]
inhabited_anon [lemma, in General.genT]
InitClo [constructor, in FObiint.FO_BiInt_Syntax]
InT [inductive, in General.genT]
interp [record, in FObiint.FO_BiInt_Kripke_sem]
interp [record, in FOcdint.FO_CDInt_Kripke_sem]
InTv [inductive, in FOcdint.FO_CDInt_Syntax]
InTv [inductive, in FObiint.FO_BiInt_Syntax]
InTv_sind [definition, in FOcdint.FO_CDInt_Syntax]
InTv_rec [definition, in FOcdint.FO_CDInt_Syntax]
InTv_ind [definition, in FOcdint.FO_CDInt_Syntax]
InTv_rect [definition, in FOcdint.FO_CDInt_Syntax]
InTv_cons_tl [constructor, in FOcdint.FO_CDInt_Syntax]
InTv_cons_hd [constructor, in FOcdint.FO_CDInt_Syntax]
InTv_sind [definition, in FObiint.FO_BiInt_Syntax]
InTv_rec [definition, in FObiint.FO_BiInt_Syntax]
InTv_ind [definition, in FObiint.FO_BiInt_Syntax]
InTv_rect [definition, in FObiint.FO_BiInt_Syntax]
InTv_cons_tl [constructor, in FObiint.FO_BiInt_Syntax]
InTv_cons_hd [constructor, in FObiint.FO_BiInt_Syntax]
InT_remove [lemma, in FObiint.FOBIH_properties]
InT_In_eq' [lemma, in General.genT]
InT_In_eq [lemma, in General.genT]
InT_In' [lemma, in General.genT]
InT_In [lemma, in General.genT]
InT_concat [lemma, in General.genT]
InT_mapI [definition, in General.genT]
InT_map_iffT [lemma, in General.genT]
InT_mapE [lemma, in General.genT]
InT_map [lemma, in General.genT]
InT_inv [lemma, in General.genT]
InT_split [lemma, in General.genT]
InT_nilE [lemma, in General.genT]
InT_nilE' [lemma, in General.genT]
InT_appE [lemma, in General.genT]
InT_appE' [lemma, in General.genT]
InT_appR [lemma, in General.genT]
InT_appL [lemma, in General.genT]
InT_2nd [definition, in General.genT]
InT_eq [lemma, in General.genT]
InT_sind [definition, in General.genT]
InT_rec [definition, in General.genT]
InT_ind [definition, in General.genT]
InT_rect [definition, in General.genT]
InT_cons [constructor, in General.genT]
InT_eq' [constructor, in General.genT]
InT_remove [lemma, in FOcdint.FOCDIH_properties]
In_matters_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove_list_remove_redund [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove_list_In_list_not_In_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove_list_In_list [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove_In_list [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove_length_same [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove_same [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove_diff [lemma, in FOcdint.FO_CDInt_remove_list]
in_remove_in_init [lemma, in FOcdint.FO_CDInt_remove_list]
in_not_touched_remove [lemma, in FOcdint.FO_CDInt_remove_list]
In_dec [lemma, in FOcdint.FO_CDInt_remove_list]
In_remove [lemma, in FObiint.FOBIH_properties]
In_matters_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
In_remove_list_remove_redund [lemma, in FObiint.FO_BiInt_remove_list]
In_remove_list_In_list_not_In_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
In_remove_list_In_list [lemma, in FObiint.FO_BiInt_remove_list]
In_remove_In_list [lemma, in FObiint.FO_BiInt_remove_list]
In_remove_length_same [lemma, in FObiint.FO_BiInt_remove_list]
In_remove_same [lemma, in FObiint.FO_BiInt_remove_list]
In_remove_diff [lemma, in FObiint.FO_BiInt_remove_list]
in_remove_in_init [lemma, in FObiint.FO_BiInt_remove_list]
in_not_touched_remove [lemma, in FObiint.FO_BiInt_remove_list]
In_dec [lemma, in FObiint.FO_BiInt_remove_list]
In_InT [lemma, in General.genT]
In_remove [lemma, in FOcdint.FOCDIH_properties]
In_extension_In_form_index_R [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
In_extension_In_form_index_L [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
In_extension_In_form_index_R [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
In_extension_In_form_index_L [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
in_single [lemma, in General.gen]
i_func [projection, in FObiint.FO_BiInt_Kripke_sem]
i_func [projection, in FOcdint.FO_CDInt_Kripke_sem]
K
keep_list_delete_head_not_In [lemma, in FOcdint.FO_CDInt_remove_list]keep_list_delete_head_not_origin [lemma, in FOcdint.FO_CDInt_remove_list]
keep_list_delete_head_not_In [lemma, in FObiint.FO_BiInt_remove_list]
keep_list_delete_head_not_origin [lemma, in FObiint.FO_BiInt_remove_list]
kmodel [record, in FObiint.FO_BiInt_Kripke_sem]
kmodel [record, in FOcdint.FO_CDInt_Kripke_sem]
Kripke [section, in FObiint.FO_BiInt_Kripke_sem]
Kripke [section, in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Conseq_Rel [section, in FObiint.FO_BiInt_Kripke_sem]
Kripke.Conseq_Rel [section, in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Model [section, in FObiint.FO_BiInt_Kripke_sem]
Kripke.Model [section, in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Model.domain [variable, in FObiint.FO_BiInt_Kripke_sem]
Kripke.Model.domain [variable, in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Model.M [variable, in FObiint.FO_BiInt_Kripke_sem]
Kripke.Model.M [variable, in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Substs [section, in FObiint.FO_BiInt_Kripke_sem]
Kripke.Substs [section, in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Substs.D [variable, in FObiint.FO_BiInt_Kripke_sem]
Kripke.Substs.D [variable, in FOcdint.FO_CDInt_Kripke_sem]
_ ⊩( _ , _ ) _ [notation, in FObiint.FO_BiInt_Kripke_sem]
_ ⊩( _ ) _ [notation, in FObiint.FO_BiInt_Kripke_sem]
_ ⊩( _ , _ ) _ [notation, in FOcdint.FO_CDInt_Kripke_sem]
_ ⊩( _ ) _ [notation, in FOcdint.FO_CDInt_Kripke_sem]
ksat [definition, in FObiint.FO_BiInt_Kripke_sem]
ksat [definition, in FOcdint.FO_CDInt_Kripke_sem]
ksatis [definition, in FObiint.FO_BiInt_Kripke_sem]
ksatis [definition, in FOcdint.FO_CDInt_Kripke_sem]
ksat_comp [lemma, in FObiint.FO_BiInt_Kripke_sem]
ksat_ext [lemma, in FObiint.FO_BiInt_Kripke_sem]
ksat_dec [lemma, in FObiint.FO_BiInt_Kripke_sem]
ksat_iff [lemma, in FObiint.FO_BiInt_Kripke_sem]
ksat_mon [lemma, in FObiint.FO_BiInt_Kripke_sem]
ksat_comp [lemma, in FOcdint.FO_CDInt_Kripke_sem]
ksat_ext [lemma, in FOcdint.FO_CDInt_Kripke_sem]
ksat_dec [lemma, in FOcdint.FO_CDInt_Kripke_sem]
ksat_iff [lemma, in FOcdint.FO_CDInt_Kripke_sem]
ksat_mon [lemma, in FOcdint.FO_CDInt_Kripke_sem]
ksat_dec [lemma, in FOcdint.FO_CDInt_soundness]
ksat_dec [lemma, in FObiint.FO_BiInt_soundness]
kvalid [definition, in FObiint.FO_BiInt_Kripke_sem]
kvalid [definition, in FOcdint.FO_CDInt_Kripke_sem]
kvalid_ctx [definition, in FObiint.FO_BiInt_Kripke_sem]
kvalid_ctx [definition, in FOcdint.FO_CDInt_Kripke_sem]
k_P [projection, in FObiint.FO_BiInt_Kripke_sem]
k_interp [projection, in FObiint.FO_BiInt_Kripke_sem]
k_P [projection, in FOcdint.FO_CDInt_Kripke_sem]
k_interp [projection, in FOcdint.FO_CDInt_Kripke_sem]
L
Ldext [definition, in FObiint.FO_BiInt_Down_Lindenbaum_lem]Ldext_mono [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_B0 [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_A0 [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_nder [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_cum2 [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_cum1 [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_all [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_ex [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
LEM [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
LEM [lemma, in FOcdint.FO_CDInt_completeness]
LEM [lemma, in FObiint.FO_BiInt_completeness]
LEM [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
LEM [axiom, in FOcdint.FO_CDInt_soundness]
LEM [axiom, in FObiint.FO_BiInt_soundness]
LEM [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
length_le_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
length_le_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
leT [inductive, in General.genT]
leT_ex_plus [lemma, in General.genT]
leT_or_gt [lemma, in General.genT]
leT_S_or_eq [lemma, in General.genT]
leT_S_F [lemma, in General.genT]
leT_plus_l [lemma, in General.genT]
leT_plus_r [lemma, in General.genT]
leT_0_n [lemma, in General.genT]
leT_trans [definition, in General.genT]
leT_trans' [lemma, in General.genT]
leT_S_n [definition, in General.genT]
leT_S_n' [lemma, in General.genT]
leT_n_S [lemma, in General.genT]
leT_sind [definition, in General.genT]
leT_rec [definition, in General.genT]
leT_ind [definition, in General.genT]
leT_rect [definition, in General.genT]
leT_S [constructor, in General.genT]
leT_n [constructor, in General.genT]
Lext [definition, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext [definition, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_all_der [lemma, in FObiint.FOBIH_properties]
Lext_ex_der [lemma, in FObiint.FOBIH_properties]
Lext_all_in [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_mono [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_B0 [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_A0 [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_nder [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_cum2 [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_cum1 [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_ex [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_all [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_all_der [lemma, in FOcdint.FOCDIH_properties]
Lext_ex_der [lemma, in FOcdint.FOCDIH_properties]
Lext_all_in [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_mono [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_B0 [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_A0 [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_nder [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_cum2 [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_cum1 [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_ex [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_all [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lindenbaum [section, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum [section, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum_index [variable, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.form_index [variable, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum_unused [variable, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum [variable, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum_index [variable, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.form_index [variable, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum_unused [variable, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum [variable, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.LEM [variable, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.LEM [variable, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.Lindenbaum_construction [section, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.Lindenbaum_construction [section, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties [section, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties [section, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties_Lind [section, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties_Lind [section, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.unused [section, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.unused [section, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lind_pair_all_henk [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lind_pair_ex_henk [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lind_pair_all_henk [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lind_pair_ex_henk [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
list_disj_weak [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
list_disj_subst_form [lemma, in FObiint.FO_BiInt_Down_Lindenbaum_lem]
List_Reverse_arrow [lemma, in FOcdint.FO_CDInt_logic]
list_disj_mono [lemma, in FObiint.FOBIH_properties]
list_conj_finite_context [lemma, in FObiint.FOBIH_properties]
list_conj_in_list [lemma, in FObiint.FOBIH_properties]
list_disj_nodup [lemma, in FObiint.FOBIH_properties]
list_disj_In_prv [lemma, in FObiint.FOBIH_properties]
list_disj_app_distr [lemma, in FObiint.FOBIH_properties]
list_disj_In [lemma, in FObiint.FOBIH_properties]
list_disj_In0 [lemma, in FObiint.FOBIH_properties]
list_disj_remove_form [lemma, in FObiint.FOBIH_properties]
list_disj_remove_app [lemma, in FObiint.FOBIH_properties]
list_disj_app0 [lemma, in FObiint.FOBIH_properties]
list_disj_app [lemma, in FObiint.FOBIH_properties]
list_conj [definition, in FOcdint.FO_CDInt_GHC]
list_disj [definition, in FOcdint.FO_CDInt_GHC]
list_conj [definition, in FObiint.FO_BiInt_GHC]
list_disj [definition, in FObiint.FO_BiInt_GHC]
List_Reverse_arrow [lemma, in FObiint.FO_BiInt_logic]
list_disj_mono [lemma, in FOcdint.FOCDIH_properties]
list_conj_finite_context [lemma, in FOcdint.FOCDIH_properties]
list_conj_in_list [lemma, in FOcdint.FOCDIH_properties]
list_disj_nodup [lemma, in FOcdint.FOCDIH_properties]
list_disj_In_prv [lemma, in FOcdint.FOCDIH_properties]
list_disj_app_distr [lemma, in FOcdint.FOCDIH_properties]
list_disj_In [lemma, in FOcdint.FOCDIH_properties]
list_disj_In0 [lemma, in FOcdint.FOCDIH_properties]
list_disj_remove_form [lemma, in FOcdint.FOCDIH_properties]
list_disj_remove_app [lemma, in FOcdint.FOCDIH_properties]
list_disj_app0 [lemma, in FOcdint.FOCDIH_properties]
list_disj_app [lemma, in FOcdint.FOCDIH_properties]
list_primeness_fst_Lind_pair [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
list_form_infinite_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
list_disj_prime [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
list_primeness_fst_Lind_pair [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
list_form_infinite_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
list_disj_prime [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
loc_conseq [definition, in FObiint.FO_BiInt_Kripke_sem]
loc_conseq [definition, in FOcdint.FO_CDInt_Kripke_sem]
Logic [section, in FOcdint.FO_CDInt_logic]
Logic [section, in FObiint.FO_BiInt_logic]
Lwitness_Ex_help [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lwitness_Ex_help [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
M
map_eq_nil [lemma, in General.gen]map_app_ex [lemma, in General.gen]
map_cons_ex' [lemma, in General.gen]
map_cons_ex [lemma, in General.gen]
max_list_form_index [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
max_list_infinite_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
max_list_form_index [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
max_list_infinite_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
monoL_Excl [lemma, in FObiint.FOBIH_properties]
monoR_Excl [lemma, in FObiint.FOBIH_properties]
monotL_Or [lemma, in FObiint.FOBIH_properties]
monotL_Or [lemma, in FOcdint.FOCDIH_properties]
monotR_Or [lemma, in FObiint.FOBIH_properties]
monotR_Or [lemma, in FOcdint.FOCDIH_properties]
monot_Or2 [lemma, in FObiint.FOBIH_properties]
monot_Or2 [lemma, in FOcdint.FOCDIH_properties]
mon_P [projection, in FObiint.FO_BiInt_Kripke_sem]
mon_P [projection, in FOcdint.FO_CDInt_Kripke_sem]
MP [constructor, in FOcdint.FO_CDInt_GHC]
MP [constructor, in FObiint.FO_BiInt_GHC]
N
nextension_infinite_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]nextension_theory_extens_le [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
nextension_theory_extens [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
nextension_theory [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
nextension_infinite_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
nextension_theory_extens_le [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
nextension_theory_extens [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
nextension_theory [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
nodes [projection, in FObiint.FO_BiInt_Kripke_sem]
nodes [projection, in FOcdint.FO_CDInt_Kripke_sem]
NoDup_destr_split [lemma, in FOcdint.FO_CDInt_remove_list]
NoDup_remove [lemma, in FObiint.FOBIH_properties]
NoDup_destr_split [lemma, in FObiint.FO_BiInt_remove_list]
NoDup_remove [lemma, in FOcdint.FOCDIH_properties]
not_removed_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
not_removed_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
O
operators [record, in FOcdint.FO_CDInt_Syntax]operators [record, in FObiint.FO_BiInt_Syntax]
Or_imp_assoc [lemma, in FObiint.FOBIH_properties]
Or_imp_assoc [lemma, in FOcdint.FOCDIH_properties]
or_false [lemma, in General.gen]
P
pair_der [definition, in FOcdint.FO_CDInt_GHC]pair_der [definition, in FObiint.FO_BiInt_GHC]
pair_der_nextension_theory_mextension_theory_le [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
pair_der_nextension_theory_mextension_theory_le [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
pair_eqI [lemma, in General.gen]
permut_remove_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
permut_remove [lemma, in FOcdint.FO_CDInt_remove_list]
permut_remove_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
permut_remove [lemma, in FObiint.FO_BiInt_remove_list]
PiffD1 [lemma, in General.gen]
PiffD2 [lemma, in General.gen]
PredicateSubstitution [section, in FOcdint.FO_CDInt_Syntax]
PredicateSubstitution [section, in FObiint.FO_BiInt_Syntax]
_ [ _ /atom ] (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
_ [ _ /atom ] (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
preds [projection, in FOcdint.FO_CDInt_Syntax]
preds [projection, in FObiint.FO_BiInt_Syntax]
preds_signature [record, in FOcdint.FO_CDInt_Syntax]
preds_signature [record, in FObiint.FO_BiInt_Syntax]
prime [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
prime [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
primeness_fst_Lind_pair [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
primeness_fst_Lind_pair [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
prod_nat_split [lemma, in General.genT]
prod_mono [lemma, in General.genT]
Properties [section, in FObiint.FOBIH_properties]
Properties [section, in FOcdint.FOCDIH_properties]
Properties.Bi_Int [section, in FObiint.FOBIH_properties]
Properties.list_conj_stuff [section, in FObiint.FOBIH_properties]
Properties.list_disj_stuff [section, in FObiint.FOBIH_properties]
Properties.list_conj_stuff [section, in FOcdint.FOCDIH_properties]
Properties.list_disj_stuff [section, in FOcdint.FOCDIH_properties]
Properties.Prv [section, in FObiint.FOBIH_properties]
Properties.Prv [section, in FOcdint.FOCDIH_properties]
Properties.remove_stuff [section, in FObiint.FOBIH_properties]
Properties.remove_stuff [section, in FOcdint.FOCDIH_properties]
_ |- _ [notation, in FObiint.FOBIH_properties]
_ el _ [notation, in FObiint.FOBIH_properties]
_ |- _ [notation, in FOcdint.FOCDIH_properties]
_ el _ [notation, in FOcdint.FOCDIH_properties]
prv_list_disj [lemma, in FObiint.FOBIH_properties]
prv_list_conj' [lemma, in FObiint.FOBIH_properties]
prv_list_conj [lemma, in FObiint.FOBIH_properties]
prv_cas_car [lemma, in FObiint.FOBIH_properties]
prv_exp [lemma, in FObiint.FOBIH_properties]
prv_CE2 [lemma, in FObiint.FOBIH_properties]
prv_CE1 [lemma, in FObiint.FOBIH_properties]
prv_CI [lemma, in FObiint.FOBIH_properties]
prv_DE [lemma, in FObiint.FOBIH_properties]
prv_DI2 [lemma, in FObiint.FOBIH_properties]
prv_DI1 [lemma, in FObiint.FOBIH_properties]
prv_AE [lemma, in FObiint.FOBIH_properties]
prv_AI [lemma, in FObiint.FOBIH_properties]
prv_EE [lemma, in FObiint.FOBIH_properties]
prv_EI [lemma, in FObiint.FOBIH_properties]
prv_cut [lemma, in FObiint.FOBIH_properties]
prv_compact [lemma, in FObiint.FOBIH_properties]
prv_DT [lemma, in FObiint.FOBIH_properties]
prv_MP [lemma, in FObiint.FOBIH_properties]
prv_weak [lemma, in FObiint.FOBIH_properties]
prv_ctx [lemma, in FObiint.FOBIH_properties]
prv_Top [lemma, in FObiint.FOBIH_properties]
prv_list_disj [lemma, in FOcdint.FOCDIH_properties]
prv_list_conj' [lemma, in FOcdint.FOCDIH_properties]
prv_list_conj [lemma, in FOcdint.FOCDIH_properties]
prv_cas_car [lemma, in FOcdint.FOCDIH_properties]
prv_exp [lemma, in FOcdint.FOCDIH_properties]
prv_CE2 [lemma, in FOcdint.FOCDIH_properties]
prv_CE1 [lemma, in FOcdint.FOCDIH_properties]
prv_CI [lemma, in FOcdint.FOCDIH_properties]
prv_DE [lemma, in FOcdint.FOCDIH_properties]
prv_DI2 [lemma, in FOcdint.FOCDIH_properties]
prv_DI1 [lemma, in FOcdint.FOCDIH_properties]
prv_AE [lemma, in FOcdint.FOCDIH_properties]
prv_AI [lemma, in FOcdint.FOCDIH_properties]
prv_EE [lemma, in FOcdint.FOCDIH_properties]
prv_EI [lemma, in FOcdint.FOCDIH_properties]
prv_cut [lemma, in FOcdint.FOCDIH_properties]
prv_compact [lemma, in FOcdint.FOCDIH_properties]
prv_DT [lemma, in FOcdint.FOCDIH_properties]
prv_MP [lemma, in FOcdint.FOCDIH_properties]
prv_weak [lemma, in FOcdint.FOCDIH_properties]
prv_ctx [lemma, in FOcdint.FOCDIH_properties]
prv_Top [lemma, in FOcdint.FOCDIH_properties]
Q
QA1 [constructor, in FOcdint.FO_CDInt_GHC]QA1 [constructor, in FObiint.FO_BiInt_GHC]
QA2 [constructor, in FOcdint.FO_CDInt_GHC]
QA2 [constructor, in FObiint.FO_BiInt_GHC]
QA3 [constructor, in FOcdint.FO_CDInt_GHC]
QA3 [constructor, in FObiint.FO_BiInt_GHC]
quant [constructor, in FOcdint.FO_CDInt_Syntax]
quant [constructor, in FObiint.FO_BiInt_Syntax]
quantop [projection, in FOcdint.FO_CDInt_Syntax]
quantop [projection, in FObiint.FO_BiInt_Syntax]
quasi_completeness [lemma, in FOcdint.FO_CDInt_completeness]
quasi_completeness [lemma, in FObiint.FO_BiInt_completeness]
R
rappl [lemma, in General.gen]reachable [projection, in FObiint.FO_BiInt_Kripke_sem]
reachable [projection, in FOcdint.FO_CDInt_Kripke_sem]
reach_tran [projection, in FObiint.FO_BiInt_Kripke_sem]
reach_refl [projection, in FObiint.FO_BiInt_Kripke_sem]
reach_tran [projection, in FOcdint.FO_CDInt_Kripke_sem]
reach_refl [projection, in FOcdint.FO_CDInt_Kripke_sem]
redund_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
redund_remove [lemma, in FOcdint.FO_CDInt_remove_list]
redund_remove_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
redund_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
redund_remove [lemma, in FObiint.FO_BiInt_remove_list]
redund_remove_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
relationT [definition, in General.genT]
Remove [section, in FOcdint.FO_CDInt_remove_list]
Remove [section, in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr4 [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr2 [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr1 [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr3 [lemma, in FOcdint.FO_CDInt_remove_list]
remove_delete_origin [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_is_nil [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_in_nil [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_delete_head_In [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_delete_head [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_non_empty_inter_smaller_length [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_singl_id_or_nil [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_is_in [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_in_single [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_dist_app [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_cont [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_preserv_NoDup [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list_of_nil [lemma, in FOcdint.FO_CDInt_remove_list]
remove_list [definition, in FOcdint.FO_CDInt_remove_list]
remove_In_smaller_length [lemma, in FOcdint.FO_CDInt_remove_list]
remove_le_length [lemma, in FOcdint.FO_CDInt_remove_list]
remove_preserv_NoDup [lemma, in FOcdint.FO_CDInt_remove_list]
remove_not_in_anymore [lemma, in FOcdint.FO_CDInt_remove_list]
remove_dist_app [lemma, in FOcdint.FO_CDInt_remove_list]
remove_disj [lemma, in FObiint.FOBIH_properties]
remove_list_incr_decr [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr4 [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr2 [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr1 [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr3 [lemma, in FObiint.FO_BiInt_remove_list]
remove_delete_origin [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_is_nil [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_in_nil [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_delete_head_In [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_delete_head [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_non_empty_inter_smaller_length [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_singl_id_or_nil [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_is_in [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_in_single [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_dist_app [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_cont [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_preserv_NoDup [lemma, in FObiint.FO_BiInt_remove_list]
remove_list_of_nil [lemma, in FObiint.FO_BiInt_remove_list]
remove_list [definition, in FObiint.FO_BiInt_remove_list]
remove_In_smaller_length [lemma, in FObiint.FO_BiInt_remove_list]
remove_le_length [lemma, in FObiint.FO_BiInt_remove_list]
remove_preserv_NoDup [lemma, in FObiint.FO_BiInt_remove_list]
remove_not_in_anymore [lemma, in FObiint.FO_BiInt_remove_list]
remove_dist_app [lemma, in FObiint.FO_BiInt_remove_list]
remove_disj [lemma, in FOcdint.FOCDIH_properties]
req [definition, in General.gen]
req_trans [lemma, in General.gen]
req_sym [lemma, in General.gen]
req_refl [lemma, in General.gen]
rls [definition, in General.gen]
rlsT [definition, in General.genT]
rsub [definition, in General.gen]
rsubD [definition, in General.gen]
rsubI [definition, in General.gen]
rsub_emptyT [lemma, in General.genT]
rsub_imp [definition, in General.gen]
rsub_id [lemma, in General.gen]
rsub_trans [lemma, in General.gen]
rsub_def [lemma, in General.gen]
Rwitness_All_help [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Rwitness_All_help [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
S
scons [definition, in FOcdint.FO_CDInt_Syntax]scons [definition, in FObiint.FO_BiInt_Syntax]
Semantics [section, in FObiint.FO_BiInt_Kripke_sem]
Semantics [section, in FOcdint.FO_CDInt_Kripke_sem]
Semantics.domain [variable, in FObiint.FO_BiInt_Kripke_sem]
Semantics.domain [variable, in FOcdint.FO_CDInt_Kripke_sem]
shift_P [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
shift_P [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
size [definition, in FOcdint.FO_CDInt_Syntax]
size [definition, in FObiint.FO_BiInt_Syntax]
size_ind [lemma, in FOcdint.FO_CDInt_Syntax]
size_ind [lemma, in FObiint.FO_BiInt_Syntax]
Soundness [lemma, in FOcdint.FO_CDInt_soundness]
Soundness [lemma, in FObiint.FO_BiInt_soundness]
Soundness_LEM [section, in FOcdint.FO_CDInt_soundness]
Soundness_LEM [section, in FObiint.FO_BiInt_soundness]
Stand_Lindenbaum_lemma [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Stand_Lindenbaum_lemma_pair [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Stand_Lindenbaum_lemma [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Stand_Lindenbaum_lemma_pair [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
strong_term_ind [lemma, in FOcdint.FO_CDInt_Syntax]
strong_term_ind' [lemma, in FOcdint.FO_CDInt_Syntax]
strong_term_ind [lemma, in FObiint.FO_BiInt_Syntax]
strong_term_ind' [lemma, in FObiint.FO_BiInt_Syntax]
Subst [section, in FOcdint.FO_CDInt_Syntax]
Subst [section, in FObiint.FO_BiInt_Syntax]
subst_Ax [lemma, in FOcdint.FO_CDInt_logic]
subst_shift [lemma, in FOcdint.FO_CDInt_Syntax]
subst_comp [lemma, in FOcdint.FO_CDInt_Syntax]
subst_var [lemma, in FOcdint.FO_CDInt_Syntax]
subst_id [lemma, in FOcdint.FO_CDInt_Syntax]
subst_ext [lemma, in FOcdint.FO_CDInt_Syntax]
subst_term_shift [lemma, in FOcdint.FO_CDInt_Syntax]
subst_term_comp [lemma, in FOcdint.FO_CDInt_Syntax]
subst_term_var [lemma, in FOcdint.FO_CDInt_Syntax]
subst_term_id [lemma, in FOcdint.FO_CDInt_Syntax]
subst_term_ext [lemma, in FOcdint.FO_CDInt_Syntax]
subst_size [lemma, in FOcdint.FO_CDInt_Syntax]
subst_form [definition, in FOcdint.FO_CDInt_Syntax]
subst_term [definition, in FOcdint.FO_CDInt_Syntax]
subst_Ax [lemma, in FObiint.FO_BiInt_logic]
subst_shift [lemma, in FObiint.FO_BiInt_Syntax]
subst_comp [lemma, in FObiint.FO_BiInt_Syntax]
subst_var [lemma, in FObiint.FO_BiInt_Syntax]
subst_id [lemma, in FObiint.FO_BiInt_Syntax]
subst_ext [lemma, in FObiint.FO_BiInt_Syntax]
subst_term_shift [lemma, in FObiint.FO_BiInt_Syntax]
subst_term_comp [lemma, in FObiint.FO_BiInt_Syntax]
subst_term_var [lemma, in FObiint.FO_BiInt_Syntax]
subst_term_id [lemma, in FObiint.FO_BiInt_Syntax]
subst_term_ext [lemma, in FObiint.FO_BiInt_Syntax]
subst_size [lemma, in FObiint.FO_BiInt_Syntax]
subst_form [definition, in FObiint.FO_BiInt_Syntax]
subst_term [definition, in FObiint.FO_BiInt_Syntax]
subst_unused_single [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
subst_unused_form [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
subst_unused_term [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
subst_unused_single [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
subst_unused_form [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
subst_unused_term [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
swap_remove_list [lemma, in FOcdint.FO_CDInt_remove_list]
swap_remove_list [lemma, in FObiint.FO_BiInt_remove_list]
syms [projection, in FOcdint.FO_CDInt_Syntax]
syms [projection, in FObiint.FO_BiInt_Syntax]
T
term [inductive, in FOcdint.FO_CDInt_Syntax]term [inductive, in FObiint.FO_BiInt_Syntax]
term_indT [lemma, in FOcdint.FO_CDInt_Syntax]
term_ind [lemma, in FOcdint.FO_CDInt_Syntax]
term_rect [lemma, in FOcdint.FO_CDInt_Syntax]
term_rect' [lemma, in FOcdint.FO_CDInt_Syntax]
term_indT [lemma, in FObiint.FO_BiInt_Syntax]
term_ind [lemma, in FObiint.FO_BiInt_Syntax]
term_rect [lemma, in FObiint.FO_BiInt_Syntax]
term_rect' [lemma, in FObiint.FO_BiInt_Syntax]
term_exists_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
term_infinite_unused [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
term_exists_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
term_infinite_unused [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Thm_irrel [lemma, in FObiint.FOBIH_properties]
Thm_irrel [lemma, in FOcdint.FOCDIH_properties]
transitiveT [definition, in General.genT]
true_and [lemma, in General.gen]
truth_lemma [lemma, in FOcdint.FO_CDInt_completeness]
truth_lemma [lemma, in FObiint.FO_BiInt_completeness]
U
uf_quant [constructor, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]uf_bin [constructor, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
uf_atom [constructor, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
uf_bot [constructor, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
uf_quant [constructor, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
uf_bin [constructor, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
uf_atom [constructor, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
uf_bot [constructor, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Under_extension_theory [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Under_nextension_theory [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Under_pair_add_left_or_right [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Under_extension_theory [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Under_nextension_theory [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Under_pair_add_left_or_right [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
universal_interp_eval0 [lemma, in FOcdint.FO_CDInt_completeness]
universal_interp_eval [lemma, in FOcdint.FO_CDInt_completeness]
universal_interp [instance, in FOcdint.FO_CDInt_completeness]
universal_interp_eval0 [lemma, in FObiint.FO_BiInt_completeness]
universal_interp_eval [lemma, in FObiint.FO_BiInt_completeness]
universal_interp [instance, in FObiint.FO_BiInt_completeness]
unused [inductive, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused [inductive, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_after_subst [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term_after_subst [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_list_conj [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_list_disj [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_subst_term [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_S [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_L [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_sind [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_ind [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term_sind [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term_ind [definition, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term [inductive, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_after_subst [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term_after_subst [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_list_conj [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_list_disj [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_subst_term [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_S [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_L [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_sind [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_ind [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term_sind [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term_ind [definition, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term [inductive, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
up [definition, in FOcdint.FO_CDInt_Syntax]
up [definition, in FObiint.FO_BiInt_Syntax]
UpLind [section, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind [section, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.eq_dec_funcs [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.eq_dec_preds [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.eq_dec_funcs [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.eq_dec_preds [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_index_inj [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum_index [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_index [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum_unused [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum_sur [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_index_inj [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum_index [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_index [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum_unused [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum_sur [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.SLEM [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.SLEM [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w_nder [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.B0 [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.A0 [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wex_henk [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wded_clos [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wconsist [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wall_henk [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w [variable, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr [section, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w_nder [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.B0 [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.A0 [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wex_henk [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wded_clos [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wconsist [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wall_henk [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w [variable, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr [section, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
_ |- _ [notation, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
_ el _ [notation, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
_ |- _ [notation, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
_ el _ [notation, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
up_var_comp [lemma, in FOcdint.FO_CDInt_Syntax]
up_decompose [lemma, in FOcdint.FO_CDInt_Syntax]
up_form [lemma, in FOcdint.FO_CDInt_Syntax]
up_funcomp [lemma, in FOcdint.FO_CDInt_Syntax]
up_var [lemma, in FOcdint.FO_CDInt_Syntax]
up_ext [lemma, in FOcdint.FO_CDInt_Syntax]
up_term [lemma, in FOcdint.FO_CDInt_Syntax]
up_var_comp [lemma, in FObiint.FO_BiInt_Syntax]
up_decompose [lemma, in FObiint.FO_BiInt_Syntax]
up_form [lemma, in FObiint.FO_BiInt_Syntax]
up_funcomp [lemma, in FObiint.FO_BiInt_Syntax]
up_var [lemma, in FObiint.FO_BiInt_Syntax]
up_ext [lemma, in FObiint.FO_BiInt_Syntax]
up_term [lemma, in FObiint.FO_BiInt_Syntax]
Up_Lindenbaum_lemma [lemma, in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Up_Lindenbaum_lemma [lemma, in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ut_func [constructor, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
ut_var [constructor, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
ut_func [constructor, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
ut_var [constructor, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
V
var [constructor, in FOcdint.FO_CDInt_Syntax]var [constructor, in FObiint.FO_BiInt_Syntax]
vec [abbreviation, in FObiint.FO_BiInt_Kripke_sem]
vec [abbreviation, in FOcdint.FO_CDInt_Syntax]
vec [abbreviation, in FOcdint.FO_CDInt_Kripke_sem]
vec [abbreviation, in FOcdint.FO_CDInt_Conservativity]
vec [abbreviation, in FObiint.FO_BiInt_Syntax]
vec [abbreviation, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec [abbreviation, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
VectorIn_vec_in_term [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
VectorIn_vec_in_term [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_0_nil [lemma, in FOcdint.FO_CDInt_Syntax]
vec_in_sind [definition, in FOcdint.FO_CDInt_Syntax]
vec_in_rec [definition, in FOcdint.FO_CDInt_Syntax]
vec_in_ind [definition, in FOcdint.FO_CDInt_Syntax]
vec_in_rect [definition, in FOcdint.FO_CDInt_Syntax]
vec_inS [constructor, in FOcdint.FO_CDInt_Syntax]
vec_inB [constructor, in FOcdint.FO_CDInt_Syntax]
vec_in [inductive, in FOcdint.FO_CDInt_Syntax]
vec_0_nil [lemma, in FObiint.FO_BiInt_Syntax]
vec_in_sind [definition, in FObiint.FO_BiInt_Syntax]
vec_in_rec [definition, in FObiint.FO_BiInt_Syntax]
vec_in_ind [definition, in FObiint.FO_BiInt_Syntax]
vec_in_rect [definition, in FObiint.FO_BiInt_Syntax]
vec_inS [constructor, in FObiint.FO_BiInt_Syntax]
vec_inB [constructor, in FObiint.FO_BiInt_Syntax]
vec_in [inductive, in FObiint.FO_BiInt_Syntax]
vec_map_ext [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_map [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_dec [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_VectorIn_term [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_map_if [lemma, in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_map_ext [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_map [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_dec [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_VectorIn_term [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_map_if [lemma, in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
W
want_prod_under_universal4 [lemma, in General.genT]want_right_prod_under_universal' [lemma, in General.genT]
want_right_prod_under_universal [lemma, in General.genT]
want_left_prod_under_universal [lemma, in General.genT]
well_foundedT [definition, in General.genT]
other
_ [ _ /atom ] (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]↑ (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
_ .. (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
_ >> _ (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
_ .: _ (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
_ [ _ ] (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
_ `[ _ ] (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
$ _ (subst_scope) [notation, in FOcdint.FO_CDInt_Syntax]
_ [ _ /atom ] (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
↑ (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
_ .. (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
_ >> _ (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
_ .: _ (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
_ [ _ ] (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
_ `[ _ ] (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
$ _ (subst_scope) [notation, in FObiint.FO_BiInt_Syntax]
existsT2 _ .. _ , _ (type_scope) [notation, in General.existsT]
existsT _ .. _ , _ (type_scope) [notation, in General.existsT]
_ ⊩( _ , _ ) _ [notation, in FObiint.FO_BiInt_Kripke_sem]
_ ⊩( _ ) _ [notation, in FObiint.FO_BiInt_Kripke_sem]
_ ⊩( _ , _ ) _ [notation, in FOcdint.FO_CDInt_Kripke_sem]
_ ⊩( _ ) _ [notation, in FOcdint.FO_CDInt_Kripke_sem]
T~ _ [notation, in General.genT]
Notation Index
C
_ |- _ [in FOcdint.FO_CDInt_completeness]_ el _ [in FOcdint.FO_CDInt_completeness]
_ |- _ [in FObiint.FO_BiInt_completeness]
_ el _ [in FObiint.FO_BiInt_completeness]
D
_ |- _ [in FObiint.FO_BiInt_Down_Lindenbaum_lem]_ el _ [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
F
_ <--> _ (syn) [in FOcdint.FO_CDInt_Syntax]_ --> _ (syn) [in FOcdint.FO_CDInt_Syntax]
_ ∨ _ (syn) [in FOcdint.FO_CDInt_Syntax]
_ ∧ _ (syn) [in FOcdint.FO_CDInt_Syntax]
_ <--> _ (syn) [in FObiint.FO_BiInt_Syntax]
_ --< _ (syn) [in FObiint.FO_BiInt_Syntax]
_ --> _ (syn) [in FObiint.FO_BiInt_Syntax]
_ ∨ _ (syn) [in FObiint.FO_BiInt_Syntax]
_ ∧ _ (syn) [in FObiint.FO_BiInt_Syntax]
¬ _ (syn) [in FOcdint.FO_CDInt_Syntax]
¬ _ (syn) [in FObiint.FO_BiInt_Syntax]
∀ _ (syn) [in FOcdint.FO_CDInt_Syntax]
∀ _ (syn) [in FObiint.FO_BiInt_Syntax]
∃ _ (syn) [in FOcdint.FO_CDInt_Syntax]
∃ _ (syn) [in FObiint.FO_BiInt_Syntax]
∞ _ (syn) [in FObiint.FO_BiInt_Syntax]
⊤ (syn) [in FOcdint.FO_CDInt_Syntax]
⊤ (syn) [in FObiint.FO_BiInt_Syntax]
⊥ (syn) [in FOcdint.FO_CDInt_Syntax]
⊥ (syn) [in FObiint.FO_BiInt_Syntax]
K
_ ⊩( _ , _ ) _ [in FObiint.FO_BiInt_Kripke_sem]_ ⊩( _ ) _ [in FObiint.FO_BiInt_Kripke_sem]
_ ⊩( _ , _ ) _ [in FOcdint.FO_CDInt_Kripke_sem]
_ ⊩( _ ) _ [in FOcdint.FO_CDInt_Kripke_sem]
P
_ [ _ /atom ] (subst_scope) [in FOcdint.FO_CDInt_Syntax]_ [ _ /atom ] (subst_scope) [in FObiint.FO_BiInt_Syntax]
_ |- _ [in FObiint.FOBIH_properties]
_ el _ [in FObiint.FOBIH_properties]
_ |- _ [in FOcdint.FOCDIH_properties]
_ el _ [in FOcdint.FOCDIH_properties]
U
_ |- _ [in FObiint.FO_BiInt_Up_Lindenbaum_lem]_ el _ [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
_ |- _ [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
_ el _ [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
other
_ [ _ /atom ] (subst_scope) [in FOcdint.FO_CDInt_Syntax]↑ (subst_scope) [in FOcdint.FO_CDInt_Syntax]
_ .. (subst_scope) [in FOcdint.FO_CDInt_Syntax]
_ >> _ (subst_scope) [in FOcdint.FO_CDInt_Syntax]
_ .: _ (subst_scope) [in FOcdint.FO_CDInt_Syntax]
_ [ _ ] (subst_scope) [in FOcdint.FO_CDInt_Syntax]
_ `[ _ ] (subst_scope) [in FOcdint.FO_CDInt_Syntax]
$ _ (subst_scope) [in FOcdint.FO_CDInt_Syntax]
_ [ _ /atom ] (subst_scope) [in FObiint.FO_BiInt_Syntax]
↑ (subst_scope) [in FObiint.FO_BiInt_Syntax]
_ .. (subst_scope) [in FObiint.FO_BiInt_Syntax]
_ >> _ (subst_scope) [in FObiint.FO_BiInt_Syntax]
_ .: _ (subst_scope) [in FObiint.FO_BiInt_Syntax]
_ [ _ ] (subst_scope) [in FObiint.FO_BiInt_Syntax]
_ `[ _ ] (subst_scope) [in FObiint.FO_BiInt_Syntax]
$ _ (subst_scope) [in FObiint.FO_BiInt_Syntax]
existsT2 _ .. _ , _ (type_scope) [in General.existsT]
existsT _ .. _ , _ (type_scope) [in General.existsT]
_ ⊩( _ , _ ) _ [in FObiint.FO_BiInt_Kripke_sem]
_ ⊩( _ ) _ [in FObiint.FO_BiInt_Kripke_sem]
_ ⊩( _ , _ ) _ [in FOcdint.FO_CDInt_Kripke_sem]
_ ⊩( _ ) _ [in FOcdint.FO_CDInt_Kripke_sem]
T~ _ [in General.genT]
Module Index
F
FullSyntax [in FOcdint.FO_CDInt_Syntax]FullSyntax [in FObiint.FO_BiInt_Syntax]
Variable Index
C
completeness.eq_dec_funcs [in FOcdint.FO_CDInt_completeness]completeness.eq_dec_preds [in FOcdint.FO_CDInt_completeness]
completeness.eq_dec_funcs [in FObiint.FO_BiInt_completeness]
completeness.eq_dec_preds [in FObiint.FO_BiInt_completeness]
completeness.form_index_inj [in FOcdint.FO_CDInt_completeness]
completeness.form_enum_index [in FOcdint.FO_CDInt_completeness]
completeness.form_index [in FOcdint.FO_CDInt_completeness]
completeness.form_enum_unused [in FOcdint.FO_CDInt_completeness]
completeness.form_enum_sur [in FOcdint.FO_CDInt_completeness]
completeness.form_enum [in FOcdint.FO_CDInt_completeness]
completeness.form_index_inj [in FObiint.FO_BiInt_completeness]
completeness.form_enum_index [in FObiint.FO_BiInt_completeness]
completeness.form_index [in FObiint.FO_BiInt_completeness]
completeness.form_enum_unused [in FObiint.FO_BiInt_completeness]
completeness.form_enum_sur [in FObiint.FO_BiInt_completeness]
completeness.form_enum [in FObiint.FO_BiInt_completeness]
completeness.SLEM [in FOcdint.FO_CDInt_completeness]
completeness.SLEM [in FObiint.FO_BiInt_completeness]
conservativity.eq_dec_funcs [in FOcdint.FO_CDInt_Conservativity]
conservativity.eq_dec_preds [in FOcdint.FO_CDInt_Conservativity]
conservativity.form_index_inj [in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum_unused [in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum_index [in FOcdint.FO_CDInt_Conservativity]
conservativity.form_index [in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum_sur [in FOcdint.FO_CDInt_Conservativity]
conservativity.form_enum [in FOcdint.FO_CDInt_Conservativity]
conservativity.SLEM [in FOcdint.FO_CDInt_Conservativity]
D
DownLind.DownLind_constr.w_nder [in FObiint.FO_BiInt_Down_Lindenbaum_lem]DownLind.DownLind_constr.B0 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.A0 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wded_clos [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wprime [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wconsist [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wall_henk [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.wex_henk [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.DownLind_constr.w [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.eq_dec_funcs [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.eq_dec_preds [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_index_inj [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum_index [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_index [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum_unused [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum_sur [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.form_enum [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DownLind.SLEM [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
K
Kripke.Model.domain [in FObiint.FO_BiInt_Kripke_sem]Kripke.Model.domain [in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Model.M [in FObiint.FO_BiInt_Kripke_sem]
Kripke.Model.M [in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Substs.D [in FObiint.FO_BiInt_Kripke_sem]
Kripke.Substs.D [in FOcdint.FO_CDInt_Kripke_sem]
L
Lindenbaum.form_enum_index [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]Lindenbaum.form_index [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum_index [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.form_index [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.form_enum [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.LEM [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.LEM [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
S
Semantics.domain [in FObiint.FO_BiInt_Kripke_sem]Semantics.domain [in FOcdint.FO_CDInt_Kripke_sem]
U
UpLind.eq_dec_funcs [in FObiint.FO_BiInt_Up_Lindenbaum_lem]UpLind.eq_dec_preds [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.eq_dec_funcs [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.eq_dec_preds [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_index_inj [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum_index [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_index [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum_unused [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum_sur [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_enum [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.form_index_inj [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum_index [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_index [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum_unused [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum_sur [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.form_enum [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.SLEM [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.SLEM [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w_nder [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.B0 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.A0 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wex_henk [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wded_clos [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wconsist [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wall_henk [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w_nder [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.B0 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.A0 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wex_henk [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wded_clos [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wconsist [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.wall_henk [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr.w [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Library Index
E
existsTF
FOBIH_propertiesFOCDIH_properties
FO_BiInt_Syntax
FO_BiInt_Kripke_sem
FO_CDInt_GHC
FO_BiInt_remove_list
FO_BiInt_GHC
FO_CDInt_logic
FO_CDInt_Stand_Lindenbaum_lem
FO_CDInt_Conservativity
FO_BiInt_Stand_Lindenbaum_lem
FO_BiInt_completeness
FO_CDInt_soundness
FO_CDInt_Up_Lindenbaum_lem
FO_BiInt_Down_Lindenbaum_lem
FO_CDInt_completeness
FO_BiInt_Up_Lindenbaum_lem
FO_BiInt_logic
FO_CDInt_Syntax
FO_CDInt_remove_list
FO_CDInt_Kripke_sem
FO_BiInt_soundness
G
gengenT
Lemma Index
A
absorp_Or2 [in FObiint.FOBIH_properties]absorp_Or1 [in FObiint.FOBIH_properties]
absorp_Or2 [in FOcdint.FOCDIH_properties]
absorp_Or1 [in FOcdint.FOCDIH_properties]
add_remove_list_preserve_NoDup [in FOcdint.FO_CDInt_remove_list]
add_remove_list_preserve_NoDup [in FObiint.FO_BiInt_remove_list]
all_henk' [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
all_henk' [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
And_Imp [in FObiint.FOBIH_properties]
And_Imp [in FOcdint.FOCDIH_properties]
and_true [in General.gen]
anonD [in General.genT]
anonI [in General.genT]
anon_forall [in General.genT]
anon_sigT [in General.genT]
anon_iffT [in General.genT]
anon_imp [in General.genT]
anon_sum [in General.genT]
anon_prod [in General.genT]
anon_eq [in General.genT]
appl [in General.gen]
app_remove_list [in FOcdint.FO_CDInt_remove_list]
app_remove_list [in FObiint.FO_BiInt_remove_list]
arg_cong_imp' [in General.gen]
arg_cong_imp [in General.gen]
arg_cong [in General.gen]
arg1_cong_imp' [in General.gen]
arg1_cong_imp [in General.gen]
AThm_irrel [in FObiint.FOBIH_properties]
atom_subst_Ax [in FOcdint.FO_CDInt_logic]
atom_subst_comp_strong [in FOcdint.FO_CDInt_Syntax]
atom_subst_comp [in FOcdint.FO_CDInt_Syntax]
atom_subst_id [in FOcdint.FO_CDInt_Syntax]
atom_subst_strong_to_normal [in FOcdint.FO_CDInt_Syntax]
atom_inv [in FOcdint.FO_CDInt_Syntax]
atom_subst_Ax [in FObiint.FO_BiInt_logic]
atom_subst_comp_strong [in FObiint.FO_BiInt_Syntax]
atom_subst_comp [in FObiint.FO_BiInt_Syntax]
atom_subst_id [in FObiint.FO_BiInt_Syntax]
atom_subst_strong_to_normal [in FObiint.FO_BiInt_Syntax]
atom_inv [in FObiint.FO_BiInt_Syntax]
Ax_valid [in FOcdint.FO_CDInt_soundness]
Ax_valid [in FObiint.FO_BiInt_soundness]
B
BiLEM [in FObiint.FOBIH_properties]C
closeder_fst_Lind_pair [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]closeder_fst_Lind_pair [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
comm_Or [in FObiint.FOBIH_properties]
comm_Or_obj [in FObiint.FOBIH_properties]
comm_And_obj [in FObiint.FOBIH_properties]
comm_Or [in FOcdint.FOCDIH_properties]
comm_Or_obj [in FOcdint.FOCDIH_properties]
comm_And_obj [in FOcdint.FOCDIH_properties]
Completeness [in FOcdint.FO_CDInt_completeness]
Completeness [in FObiint.FO_BiInt_completeness]
Conservativity [in FOcdint.FO_CDInt_Conservativity]
Consist_extension_theory [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Consist_extension_theory_pair [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Consist_nextension_theory [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Consist_extension_theory [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Consist_extension_theory_pair [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Consist_nextension_theory [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Constant_Domain_Ax [in FObiint.FOBIH_properties]
Contr_Bot [in FObiint.FOBIH_properties]
Contr_Bot [in FOcdint.FOCDIH_properties]
Cut [in FObiint.FOBIH_properties]
Cut [in FOcdint.FOCDIH_properties]
cwDownLind [in FObiint.FO_BiInt_completeness]
cwTradLind [in FOcdint.FO_CDInt_completeness]
cwTradLind [in FObiint.FO_BiInt_completeness]
cwUpLind [in FOcdint.FO_CDInt_completeness]
cwUpLind [in FObiint.FO_BiInt_completeness]
cycle_shift_shift [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
cycle_shift_subject [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
cycle_shift_shift [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
cycle_shift_subject [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
D
der_list_conj_finite_context [in FObiint.FOBIH_properties]der_list_disj_bot [in FObiint.FOBIH_properties]
der_list_disj_remove2 [in FObiint.FOBIH_properties]
der_list_disj_remove1 [in FObiint.FOBIH_properties]
der_list_conj_finite_context [in FOcdint.FOCDIH_properties]
der_list_disj_bot [in FOcdint.FOCDIH_properties]
der_list_disj_remove2 [in FOcdint.FOCDIH_properties]
der_list_disj_remove1 [in FOcdint.FOCDIH_properties]
der_nextension_theory_mextension_theory_le [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
der_nextension_theory_mextension_theory_le [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
dext_prime [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_consist [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_B0 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_A0 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_ded_clos [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_all_henk [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_ex_henk [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_el [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_nder [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_prv [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
dext_der [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DN_to_form [in FObiint.FOBIH_properties]
double_remove [in FOcdint.FO_CDInt_remove_list]
double_remove [in FObiint.FO_BiInt_remove_list]
Down_Lindenbaum_lemma [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Dual_Constant_Domain [in FObiint.FOBIH_properties]
dual_MP [in FObiint.FOBIH_properties]
dual_residuation_gen [in FObiint.FOBIH_properties]
dual_residuation [in FObiint.FOBIH_properties]
dual_residuation_obj [in FObiint.FOBIH_properties]
E
EC_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]EC_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
EFQ [in FObiint.FOBIH_properties]
EFQ [in FOcdint.FOCDIH_properties]
embed_ksat [in FOcdint.FO_CDInt_Conservativity]
embed_eval [in FOcdint.FO_CDInt_Conservativity]
emptyT_any [in General.genT]
emptyT_any' [in General.genT]
empty_False [in General.genT]
empty_explosion [in General.genT]
eq_dec_form [in FOcdint.FO_CDInt_Syntax]
eq_dec_term [in FOcdint.FO_CDInt_Syntax]
eq_dec_preserved_vector0 [in FOcdint.FO_CDInt_Syntax]
eq_dec_preserved_vector [in FOcdint.FO_CDInt_Syntax]
eq_dec_nat [in FOcdint.FO_CDInt_Syntax]
eq_S_F [in General.genT]
eq_dec_form [in FObiint.FO_BiInt_Syntax]
eq_dec_term [in FObiint.FO_BiInt_Syntax]
eq_dec_preserved_vector0 [in FObiint.FO_BiInt_Syntax]
eq_dec_preserved_vector [in FObiint.FO_BiInt_Syntax]
eq_dec_nat [in FObiint.FO_BiInt_Syntax]
eq_TrueI [in General.gen]
eval_comp [in FObiint.FO_BiInt_Kripke_sem]
eval_ext [in FObiint.FO_BiInt_Kripke_sem]
eval_comp [in FOcdint.FO_CDInt_Kripke_sem]
eval_ext [in FOcdint.FO_CDInt_Kripke_sem]
exist_unused_term_exists_First_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
exist_unused_term_exists_First_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
extension_theory_extens [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
extension_theory_extens_nextension [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
extension_theory_extens [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
extension_theory_extens_nextension [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
ext_prime [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_nel [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_nel' [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_consist [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_B0 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_A0 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_ded_clos [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_all_henk [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_ex_henk [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_el [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_nder [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_prv [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_der [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext_prime [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_nel [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_nel' [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_consist [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_B0 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_A0 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_ded_clos [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_all_henk [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_ex_henk [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_el [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_nder [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_prv [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
ext_der [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
F
False_empty [in General.genT]false_or [in General.gen]
finite_context_list_conj [in FObiint.FOBIH_properties]
finite_context_list_conj [in FOcdint.FOCDIH_properties]
FOBIH_Dual_Deduction_Theorem [in FObiint.FOBIH_properties]
FOBIH_Dual_Detachment_Theorem [in FObiint.FOBIH_properties]
FOBIH_Deduction_Theorem [in FObiint.FOBIH_properties]
FOBIH_Detachment_Theorem [in FObiint.FOBIH_properties]
FOBIH_finite [in FObiint.FO_BiInt_logic]
FOBIH_struct [in FObiint.FO_BiInt_logic]
FOBIH_comp [in FObiint.FO_BiInt_logic]
FOBIH_subst [in FObiint.FO_BiInt_logic]
FOBIH_monot [in FObiint.FO_BiInt_logic]
FOCDIH_finite [in FOcdint.FO_CDInt_logic]
FOCDIH_struct [in FOcdint.FO_CDInt_logic]
FOCDIH_comp [in FOcdint.FO_CDInt_logic]
FOCDIH_subst [in FOcdint.FO_CDInt_logic]
FOCDIH_monot [in FOcdint.FO_CDInt_logic]
FOCDIH_Deduction_Theorem [in FOcdint.FOCDIH_properties]
FOCDIH_Detachment_Theorem [in FOcdint.FOCDIH_properties]
ForallT_Forall [in General.genT]
ForallT_Forall' [in General.genT]
ForallT_forall [in General.genT]
ForallT_impl [in General.genT]
ForallT_map_rev [in General.genT]
ForallT_map [in General.genT]
ForallT_map_2 [in General.genT]
ForallT_2 [in General.genT]
ForallT_append [in General.genT]
ForallT_cons_iff [in General.genT]
ForallT_single [in General.genT]
ForallT_cons_inv [in General.genT]
ForallT_inv [in General.genT]
forall_list_disj [in FObiint.FOBIH_properties]
Forall_ForallT' [in General.genT]
Forall_ForallT [in General.genT]
forall_list_disj [in FOcdint.FOCDIH_properties]
Forall_map_2 [in General.gen]
Forall_map_single [in General.gen]
Forall_single [in General.gen]
Forall_append [in General.gen]
Forall_cons_iff [in General.gen]
Forall_cons_inv [in General.gen]
Forall2T_ex_r [in General.genT]
Forall2T_ex_l [in General.genT]
Forall2T_app [in General.genT]
Forall2T_app_inv_r [in General.genT]
Forall2T_app_inv_l [in General.genT]
form_ex [in FOcdint.FO_CDInt_Syntax]
form_all [in FOcdint.FO_CDInt_Syntax]
form_subst_help [in FOcdint.FO_CDInt_Syntax]
form_ind_subst [in FOcdint.FO_CDInt_Syntax]
form_ex [in FObiint.FO_BiInt_Syntax]
form_all [in FObiint.FO_BiInt_Syntax]
form_subst_help [in FObiint.FO_BiInt_Syntax]
form_ind_subst [in FObiint.FO_BiInt_Syntax]
form_index_In_L_or_R [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_index_inj [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_exists_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
form_index_In_L_or_R [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
form_index_inj [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
form_exists_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
form_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
func_inv [in FOcdint.FO_CDInt_Syntax]
func_inv [in FObiint.FO_BiInt_Syntax]
fun_cong [in General.gen]
G
gen_FOBIH_Dual_Deduction_Theorem [in FObiint.FOBIH_properties]gen_FOBIH_Dual_Detachment_Theorem [in FObiint.FOBIH_properties]
gen_FOBIH_Deduction_Theorem [in FObiint.FOBIH_properties]
gen_FOBIH_Detachment_Theorem [in FObiint.FOBIH_properties]
gen_FOCDIH_Deduction_Theorem [in FOcdint.FOCDIH_properties]
gen_FOCDIH_Detachment_Theorem [in FOcdint.FOCDIH_properties]
Gen_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Gen_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
gen_cong [in General.gen]
I
Id_list_disj_remove [in FObiint.FOBIH_properties]Id_list_disj [in FObiint.FOBIH_properties]
Id_list_disj_remove [in FOcdint.FOCDIH_properties]
Id_list_disj [in FOcdint.FOCDIH_properties]
iffD1 [in General.gen]
iffD2 [in General.gen]
iffT_prod [in General.genT]
iffT_D2' [in General.genT]
iffT_D1' [in General.genT]
iffT_refl [in General.genT]
iffT_sym' [in General.genT]
iffT_trans [in General.genT]
Imp_And [in FObiint.FOBIH_properties]
Imp_trans [in FObiint.FOBIH_properties]
Imp_trans_help427 [in FObiint.FOBIH_properties]
Imp_trans_help410 [in FObiint.FOBIH_properties]
Imp_trans_help170 [in FObiint.FOBIH_properties]
Imp_trans_help54 [in FObiint.FOBIH_properties]
Imp_trans_help37 [in FObiint.FOBIH_properties]
Imp_trans_help35 [in FObiint.FOBIH_properties]
Imp_trans_help14 [in FObiint.FOBIH_properties]
Imp_trans_help9 [in FObiint.FOBIH_properties]
Imp_trans_help8 [in FObiint.FOBIH_properties]
Imp_trans_help7 [in FObiint.FOBIH_properties]
imp_Id_gen [in FObiint.FOBIH_properties]
Imp_And [in FOcdint.FOCDIH_properties]
Imp_trans [in FOcdint.FOCDIH_properties]
Imp_trans_help427 [in FOcdint.FOCDIH_properties]
Imp_trans_help410 [in FOcdint.FOCDIH_properties]
Imp_trans_help170 [in FOcdint.FOCDIH_properties]
Imp_trans_help54 [in FOcdint.FOCDIH_properties]
Imp_trans_help37 [in FOcdint.FOCDIH_properties]
Imp_trans_help35 [in FOcdint.FOCDIH_properties]
Imp_trans_help14 [in FOcdint.FOCDIH_properties]
Imp_trans_help9 [in FOcdint.FOCDIH_properties]
Imp_trans_help8 [in FOcdint.FOCDIH_properties]
Imp_trans_help7 [in FOcdint.FOCDIH_properties]
imp_Id_gen [in FOcdint.FOCDIH_properties]
inhabited_anon [in General.genT]
InT_remove [in FObiint.FOBIH_properties]
InT_In_eq' [in General.genT]
InT_In_eq [in General.genT]
InT_In' [in General.genT]
InT_In [in General.genT]
InT_concat [in General.genT]
InT_map_iffT [in General.genT]
InT_mapE [in General.genT]
InT_map [in General.genT]
InT_inv [in General.genT]
InT_split [in General.genT]
InT_nilE [in General.genT]
InT_nilE' [in General.genT]
InT_appE [in General.genT]
InT_appE' [in General.genT]
InT_appR [in General.genT]
InT_appL [in General.genT]
InT_eq [in General.genT]
InT_remove [in FOcdint.FOCDIH_properties]
In_matters_remove_list [in FOcdint.FO_CDInt_remove_list]
In_remove_list_remove_redund [in FOcdint.FO_CDInt_remove_list]
In_remove_list_In_list_not_In_remove_list [in FOcdint.FO_CDInt_remove_list]
In_remove_list_In_list [in FOcdint.FO_CDInt_remove_list]
In_remove_In_list [in FOcdint.FO_CDInt_remove_list]
In_remove_length_same [in FOcdint.FO_CDInt_remove_list]
In_remove_same [in FOcdint.FO_CDInt_remove_list]
In_remove_diff [in FOcdint.FO_CDInt_remove_list]
in_remove_in_init [in FOcdint.FO_CDInt_remove_list]
in_not_touched_remove [in FOcdint.FO_CDInt_remove_list]
In_dec [in FOcdint.FO_CDInt_remove_list]
In_remove [in FObiint.FOBIH_properties]
In_matters_remove_list [in FObiint.FO_BiInt_remove_list]
In_remove_list_remove_redund [in FObiint.FO_BiInt_remove_list]
In_remove_list_In_list_not_In_remove_list [in FObiint.FO_BiInt_remove_list]
In_remove_list_In_list [in FObiint.FO_BiInt_remove_list]
In_remove_In_list [in FObiint.FO_BiInt_remove_list]
In_remove_length_same [in FObiint.FO_BiInt_remove_list]
In_remove_same [in FObiint.FO_BiInt_remove_list]
In_remove_diff [in FObiint.FO_BiInt_remove_list]
in_remove_in_init [in FObiint.FO_BiInt_remove_list]
in_not_touched_remove [in FObiint.FO_BiInt_remove_list]
In_dec [in FObiint.FO_BiInt_remove_list]
In_InT [in General.genT]
In_remove [in FOcdint.FOCDIH_properties]
In_extension_In_form_index_R [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
In_extension_In_form_index_L [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
In_extension_In_form_index_R [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
In_extension_In_form_index_L [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
in_single [in General.gen]
K
keep_list_delete_head_not_In [in FOcdint.FO_CDInt_remove_list]keep_list_delete_head_not_origin [in FOcdint.FO_CDInt_remove_list]
keep_list_delete_head_not_In [in FObiint.FO_BiInt_remove_list]
keep_list_delete_head_not_origin [in FObiint.FO_BiInt_remove_list]
ksat_comp [in FObiint.FO_BiInt_Kripke_sem]
ksat_ext [in FObiint.FO_BiInt_Kripke_sem]
ksat_dec [in FObiint.FO_BiInt_Kripke_sem]
ksat_iff [in FObiint.FO_BiInt_Kripke_sem]
ksat_mon [in FObiint.FO_BiInt_Kripke_sem]
ksat_comp [in FOcdint.FO_CDInt_Kripke_sem]
ksat_ext [in FOcdint.FO_CDInt_Kripke_sem]
ksat_dec [in FOcdint.FO_CDInt_Kripke_sem]
ksat_iff [in FOcdint.FO_CDInt_Kripke_sem]
ksat_mon [in FOcdint.FO_CDInt_Kripke_sem]
ksat_dec [in FOcdint.FO_CDInt_soundness]
ksat_dec [in FObiint.FO_BiInt_soundness]
L
Ldext_mono [in FObiint.FO_BiInt_Down_Lindenbaum_lem]Ldext_B0 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_A0 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_nder [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_cum2 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_cum1 [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_all [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
Ldext_ex [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
LEM [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
LEM [in FOcdint.FO_CDInt_completeness]
LEM [in FObiint.FO_BiInt_completeness]
LEM [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
LEM [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
length_le_remove_list [in FOcdint.FO_CDInt_remove_list]
length_le_remove_list [in FObiint.FO_BiInt_remove_list]
leT_ex_plus [in General.genT]
leT_or_gt [in General.genT]
leT_S_or_eq [in General.genT]
leT_S_F [in General.genT]
leT_plus_l [in General.genT]
leT_plus_r [in General.genT]
leT_0_n [in General.genT]
leT_trans' [in General.genT]
leT_S_n' [in General.genT]
leT_n_S [in General.genT]
Lext_all_der [in FObiint.FOBIH_properties]
Lext_ex_der [in FObiint.FOBIH_properties]
Lext_all_in [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_mono [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_B0 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_A0 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_nder [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_cum2 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_cum1 [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_ex [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_all [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext_all_der [in FOcdint.FOCDIH_properties]
Lext_ex_der [in FOcdint.FOCDIH_properties]
Lext_all_in [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_mono [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_B0 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_A0 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_nder [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_cum2 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_cum1 [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_ex [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lext_all [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Lind_pair_all_henk [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lind_pair_ex_henk [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lind_pair_all_henk [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lind_pair_ex_henk [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
list_disj_weak [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
list_disj_subst_form [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
List_Reverse_arrow [in FOcdint.FO_CDInt_logic]
list_disj_mono [in FObiint.FOBIH_properties]
list_conj_finite_context [in FObiint.FOBIH_properties]
list_conj_in_list [in FObiint.FOBIH_properties]
list_disj_nodup [in FObiint.FOBIH_properties]
list_disj_In_prv [in FObiint.FOBIH_properties]
list_disj_app_distr [in FObiint.FOBIH_properties]
list_disj_In [in FObiint.FOBIH_properties]
list_disj_In0 [in FObiint.FOBIH_properties]
list_disj_remove_form [in FObiint.FOBIH_properties]
list_disj_remove_app [in FObiint.FOBIH_properties]
list_disj_app0 [in FObiint.FOBIH_properties]
list_disj_app [in FObiint.FOBIH_properties]
List_Reverse_arrow [in FObiint.FO_BiInt_logic]
list_disj_mono [in FOcdint.FOCDIH_properties]
list_conj_finite_context [in FOcdint.FOCDIH_properties]
list_conj_in_list [in FOcdint.FOCDIH_properties]
list_disj_nodup [in FOcdint.FOCDIH_properties]
list_disj_In_prv [in FOcdint.FOCDIH_properties]
list_disj_app_distr [in FOcdint.FOCDIH_properties]
list_disj_In [in FOcdint.FOCDIH_properties]
list_disj_In0 [in FOcdint.FOCDIH_properties]
list_disj_remove_form [in FOcdint.FOCDIH_properties]
list_disj_remove_app [in FOcdint.FOCDIH_properties]
list_disj_app0 [in FOcdint.FOCDIH_properties]
list_disj_app [in FOcdint.FOCDIH_properties]
list_primeness_fst_Lind_pair [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
list_form_infinite_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
list_disj_prime [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
list_primeness_fst_Lind_pair [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
list_form_infinite_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
list_disj_prime [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lwitness_Ex_help [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lwitness_Ex_help [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
M
map_eq_nil [in General.gen]map_app_ex [in General.gen]
map_cons_ex' [in General.gen]
map_cons_ex [in General.gen]
max_list_form_index [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
max_list_infinite_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
max_list_form_index [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
max_list_infinite_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
monoL_Excl [in FObiint.FOBIH_properties]
monoR_Excl [in FObiint.FOBIH_properties]
monotL_Or [in FObiint.FOBIH_properties]
monotL_Or [in FOcdint.FOCDIH_properties]
monotR_Or [in FObiint.FOBIH_properties]
monotR_Or [in FOcdint.FOCDIH_properties]
monot_Or2 [in FObiint.FOBIH_properties]
monot_Or2 [in FOcdint.FOCDIH_properties]
N
nextension_infinite_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]nextension_theory_extens_le [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
nextension_theory_extens [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
nextension_infinite_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
nextension_theory_extens_le [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
nextension_theory_extens [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
NoDup_destr_split [in FOcdint.FO_CDInt_remove_list]
NoDup_remove [in FObiint.FOBIH_properties]
NoDup_destr_split [in FObiint.FO_BiInt_remove_list]
NoDup_remove [in FOcdint.FOCDIH_properties]
not_removed_remove_list [in FOcdint.FO_CDInt_remove_list]
not_removed_remove_list [in FObiint.FO_BiInt_remove_list]
O
Or_imp_assoc [in FObiint.FOBIH_properties]Or_imp_assoc [in FOcdint.FOCDIH_properties]
or_false [in General.gen]
P
pair_der_nextension_theory_mextension_theory_le [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]pair_der_nextension_theory_mextension_theory_le [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
pair_eqI [in General.gen]
permut_remove_remove_list [in FOcdint.FO_CDInt_remove_list]
permut_remove [in FOcdint.FO_CDInt_remove_list]
permut_remove_remove_list [in FObiint.FO_BiInt_remove_list]
permut_remove [in FObiint.FO_BiInt_remove_list]
PiffD1 [in General.gen]
PiffD2 [in General.gen]
primeness_fst_Lind_pair [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
primeness_fst_Lind_pair [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
prod_nat_split [in General.genT]
prod_mono [in General.genT]
prv_list_disj [in FObiint.FOBIH_properties]
prv_list_conj' [in FObiint.FOBIH_properties]
prv_list_conj [in FObiint.FOBIH_properties]
prv_cas_car [in FObiint.FOBIH_properties]
prv_exp [in FObiint.FOBIH_properties]
prv_CE2 [in FObiint.FOBIH_properties]
prv_CE1 [in FObiint.FOBIH_properties]
prv_CI [in FObiint.FOBIH_properties]
prv_DE [in FObiint.FOBIH_properties]
prv_DI2 [in FObiint.FOBIH_properties]
prv_DI1 [in FObiint.FOBIH_properties]
prv_AE [in FObiint.FOBIH_properties]
prv_AI [in FObiint.FOBIH_properties]
prv_EE [in FObiint.FOBIH_properties]
prv_EI [in FObiint.FOBIH_properties]
prv_cut [in FObiint.FOBIH_properties]
prv_compact [in FObiint.FOBIH_properties]
prv_DT [in FObiint.FOBIH_properties]
prv_MP [in FObiint.FOBIH_properties]
prv_weak [in FObiint.FOBIH_properties]
prv_ctx [in FObiint.FOBIH_properties]
prv_Top [in FObiint.FOBIH_properties]
prv_list_disj [in FOcdint.FOCDIH_properties]
prv_list_conj' [in FOcdint.FOCDIH_properties]
prv_list_conj [in FOcdint.FOCDIH_properties]
prv_cas_car [in FOcdint.FOCDIH_properties]
prv_exp [in FOcdint.FOCDIH_properties]
prv_CE2 [in FOcdint.FOCDIH_properties]
prv_CE1 [in FOcdint.FOCDIH_properties]
prv_CI [in FOcdint.FOCDIH_properties]
prv_DE [in FOcdint.FOCDIH_properties]
prv_DI2 [in FOcdint.FOCDIH_properties]
prv_DI1 [in FOcdint.FOCDIH_properties]
prv_AE [in FOcdint.FOCDIH_properties]
prv_AI [in FOcdint.FOCDIH_properties]
prv_EE [in FOcdint.FOCDIH_properties]
prv_EI [in FOcdint.FOCDIH_properties]
prv_cut [in FOcdint.FOCDIH_properties]
prv_compact [in FOcdint.FOCDIH_properties]
prv_DT [in FOcdint.FOCDIH_properties]
prv_MP [in FOcdint.FOCDIH_properties]
prv_weak [in FOcdint.FOCDIH_properties]
prv_ctx [in FOcdint.FOCDIH_properties]
prv_Top [in FOcdint.FOCDIH_properties]
Q
quasi_completeness [in FOcdint.FO_CDInt_completeness]quasi_completeness [in FObiint.FO_BiInt_completeness]
R
rappl [in General.gen]redund_remove_list [in FOcdint.FO_CDInt_remove_list]
redund_remove [in FOcdint.FO_CDInt_remove_list]
redund_remove_remove_list [in FOcdint.FO_CDInt_remove_list]
redund_remove_list [in FObiint.FO_BiInt_remove_list]
redund_remove [in FObiint.FO_BiInt_remove_list]
redund_remove_remove_list [in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr [in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr4 [in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr2 [in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr1 [in FOcdint.FO_CDInt_remove_list]
remove_list_incr_decr3 [in FOcdint.FO_CDInt_remove_list]
remove_delete_origin [in FOcdint.FO_CDInt_remove_list]
remove_list_is_nil [in FOcdint.FO_CDInt_remove_list]
remove_list_in_nil [in FOcdint.FO_CDInt_remove_list]
remove_list_delete_head_In [in FOcdint.FO_CDInt_remove_list]
remove_list_delete_head [in FOcdint.FO_CDInt_remove_list]
remove_list_non_empty_inter_smaller_length [in FOcdint.FO_CDInt_remove_list]
remove_list_singl_id_or_nil [in FOcdint.FO_CDInt_remove_list]
remove_list_is_in [in FOcdint.FO_CDInt_remove_list]
remove_list_in_single [in FOcdint.FO_CDInt_remove_list]
remove_list_dist_app [in FOcdint.FO_CDInt_remove_list]
remove_list_cont [in FOcdint.FO_CDInt_remove_list]
remove_list_preserv_NoDup [in FOcdint.FO_CDInt_remove_list]
remove_list_of_nil [in FOcdint.FO_CDInt_remove_list]
remove_In_smaller_length [in FOcdint.FO_CDInt_remove_list]
remove_le_length [in FOcdint.FO_CDInt_remove_list]
remove_preserv_NoDup [in FOcdint.FO_CDInt_remove_list]
remove_not_in_anymore [in FOcdint.FO_CDInt_remove_list]
remove_dist_app [in FOcdint.FO_CDInt_remove_list]
remove_disj [in FObiint.FOBIH_properties]
remove_list_incr_decr [in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr4 [in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr2 [in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr1 [in FObiint.FO_BiInt_remove_list]
remove_list_incr_decr3 [in FObiint.FO_BiInt_remove_list]
remove_delete_origin [in FObiint.FO_BiInt_remove_list]
remove_list_is_nil [in FObiint.FO_BiInt_remove_list]
remove_list_in_nil [in FObiint.FO_BiInt_remove_list]
remove_list_delete_head_In [in FObiint.FO_BiInt_remove_list]
remove_list_delete_head [in FObiint.FO_BiInt_remove_list]
remove_list_non_empty_inter_smaller_length [in FObiint.FO_BiInt_remove_list]
remove_list_singl_id_or_nil [in FObiint.FO_BiInt_remove_list]
remove_list_is_in [in FObiint.FO_BiInt_remove_list]
remove_list_in_single [in FObiint.FO_BiInt_remove_list]
remove_list_dist_app [in FObiint.FO_BiInt_remove_list]
remove_list_cont [in FObiint.FO_BiInt_remove_list]
remove_list_preserv_NoDup [in FObiint.FO_BiInt_remove_list]
remove_list_of_nil [in FObiint.FO_BiInt_remove_list]
remove_In_smaller_length [in FObiint.FO_BiInt_remove_list]
remove_le_length [in FObiint.FO_BiInt_remove_list]
remove_preserv_NoDup [in FObiint.FO_BiInt_remove_list]
remove_not_in_anymore [in FObiint.FO_BiInt_remove_list]
remove_dist_app [in FObiint.FO_BiInt_remove_list]
remove_disj [in FOcdint.FOCDIH_properties]
req_trans [in General.gen]
req_sym [in General.gen]
req_refl [in General.gen]
rsub_emptyT [in General.genT]
rsub_id [in General.gen]
rsub_trans [in General.gen]
rsub_def [in General.gen]
Rwitness_All_help [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Rwitness_All_help [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
S
size_ind [in FOcdint.FO_CDInt_Syntax]size_ind [in FObiint.FO_BiInt_Syntax]
Soundness [in FOcdint.FO_CDInt_soundness]
Soundness [in FObiint.FO_BiInt_soundness]
Stand_Lindenbaum_lemma [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Stand_Lindenbaum_lemma_pair [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Stand_Lindenbaum_lemma [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Stand_Lindenbaum_lemma_pair [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
strong_term_ind [in FOcdint.FO_CDInt_Syntax]
strong_term_ind' [in FOcdint.FO_CDInt_Syntax]
strong_term_ind [in FObiint.FO_BiInt_Syntax]
strong_term_ind' [in FObiint.FO_BiInt_Syntax]
subst_Ax [in FOcdint.FO_CDInt_logic]
subst_shift [in FOcdint.FO_CDInt_Syntax]
subst_comp [in FOcdint.FO_CDInt_Syntax]
subst_var [in FOcdint.FO_CDInt_Syntax]
subst_id [in FOcdint.FO_CDInt_Syntax]
subst_ext [in FOcdint.FO_CDInt_Syntax]
subst_term_shift [in FOcdint.FO_CDInt_Syntax]
subst_term_comp [in FOcdint.FO_CDInt_Syntax]
subst_term_var [in FOcdint.FO_CDInt_Syntax]
subst_term_id [in FOcdint.FO_CDInt_Syntax]
subst_term_ext [in FOcdint.FO_CDInt_Syntax]
subst_size [in FOcdint.FO_CDInt_Syntax]
subst_Ax [in FObiint.FO_BiInt_logic]
subst_shift [in FObiint.FO_BiInt_Syntax]
subst_comp [in FObiint.FO_BiInt_Syntax]
subst_var [in FObiint.FO_BiInt_Syntax]
subst_id [in FObiint.FO_BiInt_Syntax]
subst_ext [in FObiint.FO_BiInt_Syntax]
subst_term_shift [in FObiint.FO_BiInt_Syntax]
subst_term_comp [in FObiint.FO_BiInt_Syntax]
subst_term_var [in FObiint.FO_BiInt_Syntax]
subst_term_id [in FObiint.FO_BiInt_Syntax]
subst_term_ext [in FObiint.FO_BiInt_Syntax]
subst_size [in FObiint.FO_BiInt_Syntax]
subst_unused_single [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
subst_unused_form [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
subst_unused_term [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
subst_unused_single [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
subst_unused_form [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
subst_unused_term [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
swap_remove_list [in FOcdint.FO_CDInt_remove_list]
swap_remove_list [in FObiint.FO_BiInt_remove_list]
T
term_indT [in FOcdint.FO_CDInt_Syntax]term_ind [in FOcdint.FO_CDInt_Syntax]
term_rect [in FOcdint.FO_CDInt_Syntax]
term_rect' [in FOcdint.FO_CDInt_Syntax]
term_indT [in FObiint.FO_BiInt_Syntax]
term_ind [in FObiint.FO_BiInt_Syntax]
term_rect [in FObiint.FO_BiInt_Syntax]
term_rect' [in FObiint.FO_BiInt_Syntax]
term_exists_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
term_infinite_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
term_exists_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
term_infinite_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Thm_irrel [in FObiint.FOBIH_properties]
Thm_irrel [in FOcdint.FOCDIH_properties]
true_and [in General.gen]
truth_lemma [in FOcdint.FO_CDInt_completeness]
truth_lemma [in FObiint.FO_BiInt_completeness]
U
Under_extension_theory [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]Under_nextension_theory [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Under_pair_add_left_or_right [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Under_extension_theory [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Under_nextension_theory [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Under_pair_add_left_or_right [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
universal_interp_eval0 [in FOcdint.FO_CDInt_completeness]
universal_interp_eval [in FOcdint.FO_CDInt_completeness]
universal_interp_eval0 [in FObiint.FO_BiInt_completeness]
universal_interp_eval [in FObiint.FO_BiInt_completeness]
unused_after_subst [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term_after_subst [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_list_conj [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_list_disj [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_subst_term [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_after_subst [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term_after_subst [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_list_conj [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_list_disj [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_subst_term [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
up_var_comp [in FOcdint.FO_CDInt_Syntax]
up_decompose [in FOcdint.FO_CDInt_Syntax]
up_form [in FOcdint.FO_CDInt_Syntax]
up_funcomp [in FOcdint.FO_CDInt_Syntax]
up_var [in FOcdint.FO_CDInt_Syntax]
up_ext [in FOcdint.FO_CDInt_Syntax]
up_term [in FOcdint.FO_CDInt_Syntax]
up_var_comp [in FObiint.FO_BiInt_Syntax]
up_decompose [in FObiint.FO_BiInt_Syntax]
up_form [in FObiint.FO_BiInt_Syntax]
up_funcomp [in FObiint.FO_BiInt_Syntax]
up_var [in FObiint.FO_BiInt_Syntax]
up_ext [in FObiint.FO_BiInt_Syntax]
up_term [in FObiint.FO_BiInt_Syntax]
Up_Lindenbaum_lemma [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Up_Lindenbaum_lemma [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
V
VectorIn_vec_in_term [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]VectorIn_vec_in_term [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_0_nil [in FOcdint.FO_CDInt_Syntax]
vec_0_nil [in FObiint.FO_BiInt_Syntax]
vec_map_ext [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_map [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_dec [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_VectorIn_term [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_in_map_if [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec_map_ext [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_map [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_dec [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_VectorIn_term [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
vec_in_map_if [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
W
want_prod_under_universal4 [in General.genT]want_right_prod_under_universal' [in General.genT]
want_right_prod_under_universal [in General.genT]
want_left_prod_under_universal [in General.genT]
Constructor Index
A
AccT_intro [in General.genT]atom [in FOcdint.FO_CDInt_Syntax]
atom [in FObiint.FO_BiInt_Syntax]
Ax [in FOcdint.FO_CDInt_GHC]
Ax [in FObiint.FO_BiInt_GHC]
A1 [in FOcdint.FO_CDInt_GHC]
A1 [in FObiint.FO_BiInt_GHC]
A2 [in FOcdint.FO_CDInt_GHC]
A2 [in FObiint.FO_BiInt_GHC]
A3 [in FOcdint.FO_CDInt_GHC]
A3 [in FObiint.FO_BiInt_GHC]
A4 [in FOcdint.FO_CDInt_GHC]
A4 [in FObiint.FO_BiInt_GHC]
A5 [in FOcdint.FO_CDInt_GHC]
A5 [in FObiint.FO_BiInt_GHC]
A6 [in FOcdint.FO_CDInt_GHC]
A6 [in FObiint.FO_BiInt_GHC]
A7 [in FOcdint.FO_CDInt_GHC]
A7 [in FObiint.FO_BiInt_GHC]
A8 [in FOcdint.FO_CDInt_GHC]
A8 [in FObiint.FO_BiInt_GHC]
A9 [in FOcdint.FO_CDInt_GHC]
A9 [in FObiint.FO_BiInt_GHC]
B
BA1 [in FObiint.FO_BiInt_GHC]BA2 [in FObiint.FO_BiInt_GHC]
BA3 [in FObiint.FO_BiInt_GHC]
BA4 [in FObiint.FO_BiInt_GHC]
bin [in FOcdint.FO_CDInt_Syntax]
bin [in FObiint.FO_BiInt_Syntax]
bot [in FOcdint.FO_CDInt_Syntax]
bot [in FObiint.FO_BiInt_Syntax]
C
CD [in FOcdint.FO_CDInt_GHC]D
DN [in FObiint.FO_BiInt_GHC]E
EC [in FOcdint.FO_CDInt_GHC]EC [in FObiint.FO_BiInt_GHC]
F
ForallT_cons [in General.genT]ForallT_nil [in General.genT]
Forall_cons [in FOcdint.FO_CDInt_Syntax]
Forall_nil [in FOcdint.FO_CDInt_Syntax]
Forall_cons [in FObiint.FO_BiInt_Syntax]
Forall_nil [in FObiint.FO_BiInt_Syntax]
Forall2T_cons [in General.genT]
Forall2T_nil [in General.genT]
FullSyntax.All [in FOcdint.FO_CDInt_Syntax]
FullSyntax.All [in FObiint.FO_BiInt_Syntax]
FullSyntax.Conj [in FOcdint.FO_CDInt_Syntax]
FullSyntax.Conj [in FObiint.FO_BiInt_Syntax]
FullSyntax.Disj [in FOcdint.FO_CDInt_Syntax]
FullSyntax.Disj [in FObiint.FO_BiInt_Syntax]
FullSyntax.Ex [in FOcdint.FO_CDInt_Syntax]
FullSyntax.Ex [in FObiint.FO_BiInt_Syntax]
FullSyntax.Excl [in FObiint.FO_BiInt_Syntax]
FullSyntax.Impl [in FOcdint.FO_CDInt_Syntax]
FullSyntax.Impl [in FObiint.FO_BiInt_Syntax]
func [in FOcdint.FO_CDInt_Syntax]
func [in FObiint.FO_BiInt_Syntax]
G
Gen [in FOcdint.FO_CDInt_GHC]Gen [in FObiint.FO_BiInt_GHC]
I
Id [in FOcdint.FO_CDInt_GHC]Id [in FObiint.FO_BiInt_GHC]
IndClo [in FObiint.FO_BiInt_Syntax]
InitClo [in FObiint.FO_BiInt_Syntax]
InTv_cons_tl [in FOcdint.FO_CDInt_Syntax]
InTv_cons_hd [in FOcdint.FO_CDInt_Syntax]
InTv_cons_tl [in FObiint.FO_BiInt_Syntax]
InTv_cons_hd [in FObiint.FO_BiInt_Syntax]
InT_cons [in General.genT]
InT_eq' [in General.genT]
L
leT_S [in General.genT]leT_n [in General.genT]
M
MP [in FOcdint.FO_CDInt_GHC]MP [in FObiint.FO_BiInt_GHC]
Q
QA1 [in FOcdint.FO_CDInt_GHC]QA1 [in FObiint.FO_BiInt_GHC]
QA2 [in FOcdint.FO_CDInt_GHC]
QA2 [in FObiint.FO_BiInt_GHC]
QA3 [in FOcdint.FO_CDInt_GHC]
QA3 [in FObiint.FO_BiInt_GHC]
quant [in FOcdint.FO_CDInt_Syntax]
quant [in FObiint.FO_BiInt_Syntax]
U
uf_quant [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]uf_bin [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
uf_atom [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
uf_bot [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
uf_quant [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
uf_bin [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
uf_atom [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
uf_bot [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
ut_func [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
ut_var [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
ut_func [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
ut_var [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
V
var [in FOcdint.FO_CDInt_Syntax]var [in FObiint.FO_BiInt_Syntax]
vec_inS [in FOcdint.FO_CDInt_Syntax]
vec_inB [in FOcdint.FO_CDInt_Syntax]
vec_inS [in FObiint.FO_BiInt_Syntax]
vec_inB [in FObiint.FO_BiInt_Syntax]
Axiom Index
L
LEM [in FOcdint.FO_CDInt_soundness]LEM [in FObiint.FO_BiInt_soundness]
Projection Index
A
ar_preds [in FOcdint.FO_CDInt_Syntax]ar_syms [in FOcdint.FO_CDInt_Syntax]
ar_preds [in FObiint.FO_BiInt_Syntax]
ar_syms [in FObiint.FO_BiInt_Syntax]
B
binop [in FOcdint.FO_CDInt_Syntax]binop [in FObiint.FO_BiInt_Syntax]
C
call_henk [in FOcdint.FO_CDInt_completeness]call_henk [in FObiint.FO_BiInt_completeness]
cconsist [in FOcdint.FO_CDInt_completeness]
cconsist [in FObiint.FO_BiInt_completeness]
cded_clos [in FOcdint.FO_CDInt_completeness]
cded_clos [in FObiint.FO_BiInt_completeness]
cex_henk [in FOcdint.FO_CDInt_completeness]
cex_henk [in FObiint.FO_BiInt_completeness]
cprime [in FOcdint.FO_CDInt_completeness]
cprime [in FObiint.FO_BiInt_completeness]
cX [in FOcdint.FO_CDInt_completeness]
cX [in FObiint.FO_BiInt_completeness]
I
i_func [in FObiint.FO_BiInt_Kripke_sem]i_func [in FOcdint.FO_CDInt_Kripke_sem]
K
k_P [in FObiint.FO_BiInt_Kripke_sem]k_interp [in FObiint.FO_BiInt_Kripke_sem]
k_P [in FOcdint.FO_CDInt_Kripke_sem]
k_interp [in FOcdint.FO_CDInt_Kripke_sem]
M
mon_P [in FObiint.FO_BiInt_Kripke_sem]mon_P [in FOcdint.FO_CDInt_Kripke_sem]
N
nodes [in FObiint.FO_BiInt_Kripke_sem]nodes [in FOcdint.FO_CDInt_Kripke_sem]
P
preds [in FOcdint.FO_CDInt_Syntax]preds [in FObiint.FO_BiInt_Syntax]
Q
quantop [in FOcdint.FO_CDInt_Syntax]quantop [in FObiint.FO_BiInt_Syntax]
R
reachable [in FObiint.FO_BiInt_Kripke_sem]reachable [in FOcdint.FO_CDInt_Kripke_sem]
reach_tran [in FObiint.FO_BiInt_Kripke_sem]
reach_refl [in FObiint.FO_BiInt_Kripke_sem]
reach_tran [in FOcdint.FO_CDInt_Kripke_sem]
reach_refl [in FOcdint.FO_CDInt_Kripke_sem]
S
syms [in FOcdint.FO_CDInt_Syntax]syms [in FObiint.FO_BiInt_Syntax]
Inductive Index
A
AccT [in General.genT]Axioms [in FOcdint.FO_CDInt_GHC]
Axioms [in FObiint.FO_BiInt_GHC]
D
DN_clos_set [in FObiint.FO_BiInt_Syntax]E
empty [in General.genT]emptyT [in General.genT]
empty_relT [in General.genT]
F
FOBIH_prv [in FObiint.FO_BiInt_GHC]FOCDIH_prv [in FOcdint.FO_CDInt_GHC]
Forall [in FOcdint.FO_CDInt_Syntax]
Forall [in FObiint.FO_BiInt_Syntax]
ForallT [in General.genT]
Forall2T [in General.genT]
form [in FOcdint.FO_CDInt_Syntax]
form [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym [in FObiint.FO_BiInt_Syntax]
I
InT [in General.genT]InTv [in FOcdint.FO_CDInt_Syntax]
InTv [in FObiint.FO_BiInt_Syntax]
L
leT [in General.genT]T
term [in FOcdint.FO_CDInt_Syntax]term [in FObiint.FO_BiInt_Syntax]
U
unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
V
vec_in [in FOcdint.FO_CDInt_Syntax]vec_in [in FObiint.FO_BiInt_Syntax]
Section Index
C
completeness [in FOcdint.FO_CDInt_completeness]completeness [in FObiint.FO_BiInt_completeness]
conservativity [in FOcdint.FO_CDInt_Conservativity]
D
DownLind [in FObiint.FO_BiInt_Down_Lindenbaum_lem]DownLind.DownLind_constr [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
E
EqDec [in FOcdint.FO_CDInt_Syntax]EqDec [in FObiint.FO_BiInt_Syntax]
F
fix_signature [in FOcdint.FO_CDInt_Syntax]fix_signature [in FOcdint.FO_CDInt_Syntax]
fix_signature [in FObiint.FO_BiInt_Syntax]
fix_signature [in FObiint.FO_BiInt_Syntax]
FOBIH [in FObiint.FO_BiInt_GHC]
FOCDIH [in FOcdint.FO_CDInt_GHC]
K
Kripke [in FObiint.FO_BiInt_Kripke_sem]Kripke [in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Conseq_Rel [in FObiint.FO_BiInt_Kripke_sem]
Kripke.Conseq_Rel [in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Model [in FObiint.FO_BiInt_Kripke_sem]
Kripke.Model [in FOcdint.FO_CDInt_Kripke_sem]
Kripke.Substs [in FObiint.FO_BiInt_Kripke_sem]
Kripke.Substs [in FOcdint.FO_CDInt_Kripke_sem]
L
Lindenbaum [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]Lindenbaum [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.Lindenbaum_construction [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.Lindenbaum_construction [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties_Lind [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.Properties_Lind [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Lindenbaum.unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
Lindenbaum.unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Logic [in FOcdint.FO_CDInt_logic]
Logic [in FObiint.FO_BiInt_logic]
P
PredicateSubstitution [in FOcdint.FO_CDInt_Syntax]PredicateSubstitution [in FObiint.FO_BiInt_Syntax]
Properties [in FObiint.FOBIH_properties]
Properties [in FOcdint.FOCDIH_properties]
Properties.Bi_Int [in FObiint.FOBIH_properties]
Properties.list_conj_stuff [in FObiint.FOBIH_properties]
Properties.list_disj_stuff [in FObiint.FOBIH_properties]
Properties.list_conj_stuff [in FOcdint.FOCDIH_properties]
Properties.list_disj_stuff [in FOcdint.FOCDIH_properties]
Properties.Prv [in FObiint.FOBIH_properties]
Properties.Prv [in FOcdint.FOCDIH_properties]
Properties.remove_stuff [in FObiint.FOBIH_properties]
Properties.remove_stuff [in FOcdint.FOCDIH_properties]
R
Remove [in FOcdint.FO_CDInt_remove_list]Remove [in FObiint.FO_BiInt_remove_list]
S
Semantics [in FObiint.FO_BiInt_Kripke_sem]Semantics [in FOcdint.FO_CDInt_Kripke_sem]
Soundness_LEM [in FOcdint.FO_CDInt_soundness]
Soundness_LEM [in FObiint.FO_BiInt_soundness]
Subst [in FOcdint.FO_CDInt_Syntax]
Subst [in FObiint.FO_BiInt_Syntax]
U
UpLind [in FObiint.FO_BiInt_Up_Lindenbaum_lem]UpLind [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
UpLind.UpLind_constr [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
Instance Index
B
biinterp [in FOcdint.FO_CDInt_Conservativity]bikmodel [in FOcdint.FO_CDInt_Conservativity]
biΣ_preds [in FOcdint.FO_CDInt_Conservativity]
biΣ_funcs [in FOcdint.FO_CDInt_Conservativity]
C
Canon_model [in FOcdint.FO_CDInt_completeness]Canon_model [in FObiint.FO_BiInt_completeness]
U
universal_interp [in FOcdint.FO_CDInt_completeness]universal_interp [in FObiint.FO_BiInt_completeness]
Abbreviation Index
A
adj [in FObiint.FO_BiInt_Down_Lindenbaum_lem]adj [in FObiint.FOBIH_properties]
adj [in FOcdint.FO_CDInt_completeness]
adj [in FObiint.FO_BiInt_completeness]
adj [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
adj [in FOcdint.FOCDIH_properties]
adj [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
V
vec [in FObiint.FO_BiInt_Kripke_sem]vec [in FOcdint.FO_CDInt_Syntax]
vec [in FOcdint.FO_CDInt_Kripke_sem]
vec [in FOcdint.FO_CDInt_Conservativity]
vec [in FObiint.FO_BiInt_Syntax]
vec [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
vec [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
Definition Index
A
AccT_sind [in General.genT]AccT_rec [in General.genT]
AccT_ind [in General.genT]
AccT_rect [in General.genT]
all_henk [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
all_henk [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
anon [in General.genT]
atom_subst_respects_strong [in FOcdint.FO_CDInt_Syntax]
atom_subst_respects [in FOcdint.FO_CDInt_Syntax]
atom_subst [in FOcdint.FO_CDInt_Syntax]
atom_subst_respects_strong [in FObiint.FO_BiInt_Syntax]
atom_subst_respects [in FObiint.FO_BiInt_Syntax]
atom_subst [in FObiint.FO_BiInt_Syntax]
Axioms_sind [in FOcdint.FO_CDInt_GHC]
Axioms_ind [in FOcdint.FO_CDInt_GHC]
Axioms_sind [in FObiint.FO_BiInt_GHC]
Axioms_ind [in FObiint.FO_BiInt_GHC]
C
closed [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]closed [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
closed_S [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
closed_L [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
closed_S [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
closed_L [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
consist [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
consist [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
cycle_shift [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
cycle_shift [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
D
ded_clos [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]ded_clos [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
dext [in FObiint.FO_BiInt_Down_Lindenbaum_lem]
DN_clos_set_sind [in FObiint.FO_BiInt_Syntax]
DN_clos_set_ind [in FObiint.FO_BiInt_Syntax]
DN_form [in FObiint.FO_BiInt_Syntax]
E
embed [in FOcdint.FO_CDInt_Conservativity]embed_S [in FOcdint.FO_CDInt_Conservativity]
embed_quant [in FOcdint.FO_CDInt_Conservativity]
embed_bin [in FOcdint.FO_CDInt_Conservativity]
embed_term [in FOcdint.FO_CDInt_Conservativity]
emptyT_sind [in General.genT]
emptyT_rec [in General.genT]
emptyT_ind [in General.genT]
emptyT_rect [in General.genT]
empty_sind [in General.genT]
empty_rec [in General.genT]
empty_ind [in General.genT]
empty_rect [in General.genT]
empty_relT_sind [in General.genT]
empty_relT_rec [in General.genT]
empty_relT_ind [in General.genT]
empty_relT_rect [in General.genT]
env [in FObiint.FO_BiInt_Kripke_sem]
env [in FOcdint.FO_CDInt_Kripke_sem]
eval [in FObiint.FO_BiInt_Kripke_sem]
eval [in FOcdint.FO_CDInt_Kripke_sem]
ext [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
ext [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
extension_theory [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
extension_theory [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
ex_henk [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
ex_henk [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
F
First_unused [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]First_unused [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
FOBIH_prv_sind [in FObiint.FO_BiInt_GHC]
FOBIH_prv_ind [in FObiint.FO_BiInt_GHC]
FOCDIH_prv_sind [in FOcdint.FO_CDInt_GHC]
FOCDIH_prv_ind [in FOcdint.FO_CDInt_GHC]
ForallTD_forall [in General.genT]
ForallTI_forall [in General.genT]
ForallT_2I [in General.genT]
ForallT_2I' [in General.genT]
ForallT_D2 [in General.genT]
ForallT_D1 [in General.genT]
ForallT_2D [in General.genT]
ForallT_appendI [in General.genT]
ForallT_appendI' [in General.genT]
ForallT_appendD2 [in General.genT]
ForallT_appendD1 [in General.genT]
ForallT_appendD [in General.genT]
ForallT_singleI [in General.genT]
ForallT_singleD [in General.genT]
ForallT_sind [in General.genT]
ForallT_rec [in General.genT]
ForallT_ind [in General.genT]
ForallT_rect [in General.genT]
Forall_sind [in FOcdint.FO_CDInt_Syntax]
Forall_rec [in FOcdint.FO_CDInt_Syntax]
Forall_ind [in FOcdint.FO_CDInt_Syntax]
Forall_rect [in FOcdint.FO_CDInt_Syntax]
Forall_sind [in FObiint.FO_BiInt_Syntax]
Forall_rec [in FObiint.FO_BiInt_Syntax]
Forall_ind [in FObiint.FO_BiInt_Syntax]
Forall_rect [in FObiint.FO_BiInt_Syntax]
Forall2T_sind [in General.genT]
Forall2T_rec [in General.genT]
Forall2T_ind [in General.genT]
Forall2T_rect [in General.genT]
form_sind [in FOcdint.FO_CDInt_Syntax]
form_rec [in FOcdint.FO_CDInt_Syntax]
form_ind [in FOcdint.FO_CDInt_Syntax]
form_rect [in FOcdint.FO_CDInt_Syntax]
form_sind [in FObiint.FO_BiInt_Syntax]
form_rec [in FObiint.FO_BiInt_Syntax]
form_ind [in FObiint.FO_BiInt_Syntax]
form_rect [in FObiint.FO_BiInt_Syntax]
form' [in FOcdint.FO_CDInt_Conservativity]
FullSyntax.full_operators [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_sind [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_rec [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_ind [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_quant_rect [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_sind [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_rec [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_ind [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_logic_sym_rect [in FOcdint.FO_CDInt_Syntax]
FullSyntax.full_operators [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_sind [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_rec [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_ind [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_quant_rect [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_sind [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_rec [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_ind [in FObiint.FO_BiInt_Syntax]
FullSyntax.full_logic_sym_rect [in FObiint.FO_BiInt_Syntax]
funcomp [in FOcdint.FO_CDInt_Syntax]
funcomp [in FObiint.FO_BiInt_Syntax]
G
gen_choice_code [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]gen_choice_code [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
I
iffT_D2 [in General.genT]iffT_D1 [in General.genT]
iffT_sym [in General.genT]
InTv_sind [in FOcdint.FO_CDInt_Syntax]
InTv_rec [in FOcdint.FO_CDInt_Syntax]
InTv_ind [in FOcdint.FO_CDInt_Syntax]
InTv_rect [in FOcdint.FO_CDInt_Syntax]
InTv_sind [in FObiint.FO_BiInt_Syntax]
InTv_rec [in FObiint.FO_BiInt_Syntax]
InTv_ind [in FObiint.FO_BiInt_Syntax]
InTv_rect [in FObiint.FO_BiInt_Syntax]
InT_mapI [in General.genT]
InT_2nd [in General.genT]
InT_sind [in General.genT]
InT_rec [in General.genT]
InT_ind [in General.genT]
InT_rect [in General.genT]
K
ksat [in FObiint.FO_BiInt_Kripke_sem]ksat [in FOcdint.FO_CDInt_Kripke_sem]
ksatis [in FObiint.FO_BiInt_Kripke_sem]
ksatis [in FOcdint.FO_CDInt_Kripke_sem]
kvalid [in FObiint.FO_BiInt_Kripke_sem]
kvalid [in FOcdint.FO_CDInt_Kripke_sem]
kvalid_ctx [in FObiint.FO_BiInt_Kripke_sem]
kvalid_ctx [in FOcdint.FO_CDInt_Kripke_sem]
L
Ldext [in FObiint.FO_BiInt_Down_Lindenbaum_lem]leT_trans [in General.genT]
leT_S_n [in General.genT]
leT_sind [in General.genT]
leT_rec [in General.genT]
leT_ind [in General.genT]
leT_rect [in General.genT]
Lext [in FObiint.FO_BiInt_Up_Lindenbaum_lem]
Lext [in FOcdint.FO_CDInt_Up_Lindenbaum_lem]
list_conj [in FOcdint.FO_CDInt_GHC]
list_disj [in FOcdint.FO_CDInt_GHC]
list_conj [in FObiint.FO_BiInt_GHC]
list_disj [in FObiint.FO_BiInt_GHC]
loc_conseq [in FObiint.FO_BiInt_Kripke_sem]
loc_conseq [in FOcdint.FO_CDInt_Kripke_sem]
N
nextension_theory [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]nextension_theory [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
P
pair_der [in FOcdint.FO_CDInt_GHC]pair_der [in FObiint.FO_BiInt_GHC]
prime [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
prime [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
R
relationT [in General.genT]remove_list [in FOcdint.FO_CDInt_remove_list]
remove_list [in FObiint.FO_BiInt_remove_list]
req [in General.gen]
rls [in General.gen]
rlsT [in General.genT]
rsub [in General.gen]
rsubD [in General.gen]
rsubI [in General.gen]
rsub_imp [in General.gen]
S
scons [in FOcdint.FO_CDInt_Syntax]scons [in FObiint.FO_BiInt_Syntax]
shift_P [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
shift_P [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
size [in FOcdint.FO_CDInt_Syntax]
size [in FObiint.FO_BiInt_Syntax]
subst_form [in FOcdint.FO_CDInt_Syntax]
subst_term [in FOcdint.FO_CDInt_Syntax]
subst_form [in FObiint.FO_BiInt_Syntax]
subst_term [in FObiint.FO_BiInt_Syntax]
T
transitiveT [in General.genT]U
unused_S [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]unused_L [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_sind [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_ind [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term_sind [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_term_ind [in FObiint.FO_BiInt_Stand_Lindenbaum_lem]
unused_S [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_L [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_sind [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_ind [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term_sind [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
unused_term_ind [in FOcdint.FO_CDInt_Stand_Lindenbaum_lem]
up [in FOcdint.FO_CDInt_Syntax]
up [in FObiint.FO_BiInt_Syntax]
V
vec_in_sind [in FOcdint.FO_CDInt_Syntax]vec_in_rec [in FOcdint.FO_CDInt_Syntax]
vec_in_ind [in FOcdint.FO_CDInt_Syntax]
vec_in_rect [in FOcdint.FO_CDInt_Syntax]
vec_in_sind [in FObiint.FO_BiInt_Syntax]
vec_in_rec [in FObiint.FO_BiInt_Syntax]
vec_in_ind [in FObiint.FO_BiInt_Syntax]
vec_in_rect [in FObiint.FO_BiInt_Syntax]
W
well_foundedT [in General.genT]Record Index
C
cworlds [in FOcdint.FO_CDInt_completeness]cworlds [in FObiint.FO_BiInt_completeness]
F
funcs_signature [in FOcdint.FO_CDInt_Syntax]funcs_signature [in FObiint.FO_BiInt_Syntax]
I
interp [in FObiint.FO_BiInt_Kripke_sem]interp [in FOcdint.FO_CDInt_Kripke_sem]
K
kmodel [in FObiint.FO_BiInt_Kripke_sem]kmodel [in FOcdint.FO_CDInt_Kripke_sem]
O
operators [in FOcdint.FO_CDInt_Syntax]operators [in FObiint.FO_BiInt_Syntax]
P
preds_signature [in FOcdint.FO_CDInt_Syntax]preds_signature [in FObiint.FO_BiInt_Syntax]
| 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 | (1366 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 | (63 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (97 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 | (25 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 | (699 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 | (98 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (40 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 | (31 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 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 | (217 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 | (12 entries) |