| 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 | (611 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 | (8 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 | (12 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 | (17 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 | (315 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 | (42 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 | (5 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 | (16 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 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) |
| 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 | (12 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 | (151 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 | (4 entries) |
Global Index
A
absorp_Or1 [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]AccT [inductive, in CPPsiteProjPackage.CPP_genT]
AccT_sind [definition, in CPPsiteProjPackage.CPP_genT]
AccT_rec [definition, in CPPsiteProjPackage.CPP_genT]
AccT_ind [definition, in CPPsiteProjPackage.CPP_genT]
AccT_rect [definition, in CPPsiteProjPackage.CPP_genT]
AccT_intro [constructor, in CPPsiteProjPackage.CPP_genT]
add_remove_list_preserve_NoDup [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
always_add_a_nat [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
And [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
and_true [lemma, in CPPsiteProjPackage.CPP_gen]
anon [definition, in CPPsiteProjPackage.CPP_genT]
anonD [lemma, in CPPsiteProjPackage.CPP_genT]
anonI [lemma, in CPPsiteProjPackage.CPP_genT]
anon_forall [lemma, in CPPsiteProjPackage.CPP_genT]
anon_sigT [lemma, in CPPsiteProjPackage.CPP_genT]
anon_iffT [lemma, in CPPsiteProjPackage.CPP_genT]
anon_imp [lemma, in CPPsiteProjPackage.CPP_genT]
anon_sum [lemma, in CPPsiteProjPackage.CPP_genT]
anon_prod [lemma, in CPPsiteProjPackage.CPP_genT]
anon_eq [lemma, in CPPsiteProjPackage.CPP_genT]
appl [lemma, in CPPsiteProjPackage.CPP_gen]
app_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
arg_cong_imp' [lemma, in CPPsiteProjPackage.CPP_gen]
arg_cong_imp [lemma, in CPPsiteProjPackage.CPP_gen]
arg_cong [lemma, in CPPsiteProjPackage.CPP_gen]
arg1_cong_imp' [lemma, in CPPsiteProjPackage.CPP_gen]
arg1_cong_imp [lemma, in CPPsiteProjPackage.CPP_gen]
Ax [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
AxRule [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]
AxRule_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
AxRule_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
AxRule_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
Ax_valid_BIH_model [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Ax_valid_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Ax_valid_stable [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Ax_valid [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
B
BIAxioms [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]BIAxioms_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
BIAxioms_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
BIH_rules_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
BIH_rules_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
BIH_rules [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]
BIH_Dual_Deduction_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
BIH_Dual_Detachment_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
BIH_Deduction_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
BIH_Detachment_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
BIH_finite' [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
BIH_finite' [lemma, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
BIH_finite [lemma, in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_struct [lemma, in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_comp [lemma, in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_monot [lemma, in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_finite' [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
BIH_model_Sound [section, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Bot [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
bounded_model_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
bounded_model_dec' [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
bounded_model [instance, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
BPropF [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_rec [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_rect [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
C
Canon_val [definition, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]Canon_rel [definition, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Canon_worlds [record, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Canon_val [definition, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Canon_rel [definition, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Canon_worlds [record, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Canon_val [definition, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
Canon_rel [definition, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
Canon_worlds [record, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
choice_code [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
choice_form [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
closed [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Closed [projection, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Closed [projection, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Closed [projection, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
closeder_fst_Lind_pair [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
CM [instance, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
CM [instance, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
CM [instance, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
comm_Or [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
comm_Or_obj [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
comm_And_obj [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
complete [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
Completeness [definition, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Completeness_LEM [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Completeness_LEM.TLEM [variable, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Completeness_LEM.P [variable, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Completeness_LEM [section, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Compl_prime_theory_extens [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
consistency [lemma, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
consistency [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Consist_prime_theory [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Consist_nprime_theory [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Constr_Sound [section, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
CPP_BiInt_meta_interactions1 [library]
CPP_BiInt_ModEx_constr [library]
CPP_BiInt_SemDec_completeness_constr [library]
CPP_existsT [library]
CPP_BiInt_remove_list [library]
CPP_genT [library]
CPP_BiInt_GHC [library]
CPP_BiInt_Lindenbaum_lem_prelim [library]
CPP_BiInt_completeness_constr [library]
CPP_BiInt_logic [library]
CPP_BiInt_enum [library]
CPP_gen [library]
CPP_BiInt_soundness_constr [library]
CPP_BiInt_Kripke_sem_constr [library]
CPP_BiInt_quasi_completeness_constr [library]
CPP_BiInt_meta_interactions2 [library]
CPP_BiInt_Lindenbaum_lem [library]
C_val_persist [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
C_R_trans [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
C_R_refl [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
C_val_persist [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
C_R_trans [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
C_R_refl [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
C_val_persist [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
C_R_trans [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
C_R_refl [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
D
der_prime_theory_nprime_theory [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]der_nprime_theory_mprime_theory_le [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
der_list_disj_remove2 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
der_list_disj_remove1 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
der_mult_disj_Bot [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
DNw [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
DNwRule [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]
DNwRule_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
DNwRule_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
DNwRule_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
DN_clos_set_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
DN_clos_set_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
DN_clos_set [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]
DN_form [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
double_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
E
empty [inductive, in CPPsiteProjPackage.CPP_genT]emptyT [inductive, in CPPsiteProjPackage.CPP_genT]
emptyT_any [lemma, in CPPsiteProjPackage.CPP_genT]
emptyT_any' [lemma, in CPPsiteProjPackage.CPP_genT]
emptyT_sind [definition, in CPPsiteProjPackage.CPP_genT]
emptyT_rec [definition, in CPPsiteProjPackage.CPP_genT]
emptyT_ind [definition, in CPPsiteProjPackage.CPP_genT]
emptyT_rect [definition, in CPPsiteProjPackage.CPP_genT]
empty_False [lemma, in CPPsiteProjPackage.CPP_genT]
empty_explosion [lemma, in CPPsiteProjPackage.CPP_genT]
empty_sind [definition, in CPPsiteProjPackage.CPP_genT]
empty_rec [definition, in CPPsiteProjPackage.CPP_genT]
empty_ind [definition, in CPPsiteProjPackage.CPP_genT]
empty_rect [definition, in CPPsiteProjPackage.CPP_genT]
empty_relT_sind [definition, in CPPsiteProjPackage.CPP_genT]
empty_relT_rec [definition, in CPPsiteProjPackage.CPP_genT]
empty_relT_ind [definition, in CPPsiteProjPackage.CPP_genT]
empty_relT_rect [definition, in CPPsiteProjPackage.CPP_genT]
empty_relT [inductive, in CPPsiteProjPackage.CPP_genT]
enum [definition, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
eq_TrueI [lemma, in CPPsiteProjPackage.CPP_gen]
eq_dec_form [lemma, in CPPsiteProjPackage.CPP_BiInt_GHC]
eq_dec_nat [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
eq_S_F [lemma, in CPPsiteProjPackage.CPP_genT]
Excl [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
F
false_or [lemma, in CPPsiteProjPackage.CPP_gen]False_empty [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT [inductive, in CPPsiteProjPackage.CPP_genT]
ForallTD_forall [definition, in CPPsiteProjPackage.CPP_genT]
ForallTI_forall [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_Forall [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_Forall' [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_forall [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_impl [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_2I [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_2I' [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_D2 [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_D1 [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_2D [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_map_rev [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_map [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_map_2 [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_2 [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_appendI [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_appendI' [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_appendD2 [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_appendD1 [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_appendD [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_append [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_cons_iff [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_singleI [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_singleD [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_single [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_cons_inv [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_inv [lemma, in CPPsiteProjPackage.CPP_genT]
ForallT_sind [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_rec [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_ind [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_rect [definition, in CPPsiteProjPackage.CPP_genT]
ForallT_cons [constructor, in CPPsiteProjPackage.CPP_genT]
ForallT_nil [constructor, in CPPsiteProjPackage.CPP_genT]
Forall_map_2 [lemma, in CPPsiteProjPackage.CPP_gen]
Forall_map_single [lemma, in CPPsiteProjPackage.CPP_gen]
Forall_single [lemma, in CPPsiteProjPackage.CPP_gen]
Forall_append [lemma, in CPPsiteProjPackage.CPP_gen]
Forall_cons_iff [lemma, in CPPsiteProjPackage.CPP_gen]
Forall_cons_inv [lemma, in CPPsiteProjPackage.CPP_gen]
Forall_ForallT' [lemma, in CPPsiteProjPackage.CPP_genT]
Forall_ForallT [lemma, in CPPsiteProjPackage.CPP_genT]
Forall2T [inductive, in CPPsiteProjPackage.CPP_genT]
Forall2T_ex_r [lemma, in CPPsiteProjPackage.CPP_genT]
Forall2T_ex_l [lemma, in CPPsiteProjPackage.CPP_genT]
Forall2T_app [lemma, in CPPsiteProjPackage.CPP_genT]
Forall2T_app_inv_r [lemma, in CPPsiteProjPackage.CPP_genT]
Forall2T_app_inv_l [lemma, in CPPsiteProjPackage.CPP_genT]
Forall2T_sind [definition, in CPPsiteProjPackage.CPP_genT]
Forall2T_rec [definition, in CPPsiteProjPackage.CPP_genT]
Forall2T_ind [definition, in CPPsiteProjPackage.CPP_genT]
Forall2T_rect [definition, in CPPsiteProjPackage.CPP_genT]
Forall2T_cons [constructor, in CPPsiteProjPackage.CPP_genT]
Forall2T_nil [constructor, in CPPsiteProjPackage.CPP_genT]
form_enum_ded_spec [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
form_enum_ded [definition, in CPPsiteProjPackage.CPP_BiInt_enum]
form_index_inj [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
form_enum_index [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
form_index [definition, in CPPsiteProjPackage.CPP_BiInt_enum]
form_index' [definition, in CPPsiteProjPackage.CPP_BiInt_enum]
form_enum_sur [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
form_enum [definition, in CPPsiteProjPackage.CPP_BiInt_enum]
fromlist [definition, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
fromlist [definition, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
fromlist [definition, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
fun_cong [lemma, in CPPsiteProjPackage.CPP_gen]
G
gen_cong [lemma, in CPPsiteProjPackage.CPP_gen]gen_BIH_Dual_Deduction_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
gen_BIH_Dual_Detachment_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
gen_BIH_Deduction_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
gen_BIH_Detachment_Theorem [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
I
i [axiom, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]Id [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
IdRule [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]
IdRule_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
IdRule_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
IdRule_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
Id_list_disj_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
Id_list_disj [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
iffD1 [lemma, in CPPsiteProjPackage.CPP_gen]
iffD2 [lemma, in CPPsiteProjPackage.CPP_gen]
iffT_prod [lemma, in CPPsiteProjPackage.CPP_genT]
iffT_D2 [definition, in CPPsiteProjPackage.CPP_genT]
iffT_D1 [definition, in CPPsiteProjPackage.CPP_genT]
iffT_sym [definition, in CPPsiteProjPackage.CPP_genT]
iffT_D2' [lemma, in CPPsiteProjPackage.CPP_genT]
iffT_D1' [lemma, in CPPsiteProjPackage.CPP_genT]
iffT_refl [lemma, in CPPsiteProjPackage.CPP_genT]
iffT_sym' [lemma, in CPPsiteProjPackage.CPP_genT]
iffT_trans [lemma, in CPPsiteProjPackage.CPP_genT]
Imp [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
IndClo [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
inhabited_anon [lemma, in CPPsiteProjPackage.CPP_genT]
InitClo [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
InT [inductive, in CPPsiteProjPackage.CPP_genT]
InT_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
InT_In_eq' [lemma, in CPPsiteProjPackage.CPP_genT]
InT_In_eq [lemma, in CPPsiteProjPackage.CPP_genT]
InT_In' [lemma, in CPPsiteProjPackage.CPP_genT]
InT_In [lemma, in CPPsiteProjPackage.CPP_genT]
InT_concat [lemma, in CPPsiteProjPackage.CPP_genT]
InT_mapI [definition, in CPPsiteProjPackage.CPP_genT]
InT_map_iffT [lemma, in CPPsiteProjPackage.CPP_genT]
InT_mapE [lemma, in CPPsiteProjPackage.CPP_genT]
InT_map [lemma, in CPPsiteProjPackage.CPP_genT]
InT_inv [lemma, in CPPsiteProjPackage.CPP_genT]
InT_split [lemma, in CPPsiteProjPackage.CPP_genT]
InT_nilE [lemma, in CPPsiteProjPackage.CPP_genT]
InT_nilE' [lemma, in CPPsiteProjPackage.CPP_genT]
InT_appE [lemma, in CPPsiteProjPackage.CPP_genT]
InT_appE' [lemma, in CPPsiteProjPackage.CPP_genT]
InT_appR [lemma, in CPPsiteProjPackage.CPP_genT]
InT_appL [lemma, in CPPsiteProjPackage.CPP_genT]
InT_2nd [definition, in CPPsiteProjPackage.CPP_genT]
InT_eq [lemma, in CPPsiteProjPackage.CPP_genT]
InT_sind [definition, in CPPsiteProjPackage.CPP_genT]
InT_rec [definition, in CPPsiteProjPackage.CPP_genT]
InT_ind [definition, in CPPsiteProjPackage.CPP_genT]
InT_rect [definition, in CPPsiteProjPackage.CPP_genT]
InT_cons [constructor, in CPPsiteProjPackage.CPP_genT]
InT_eq' [constructor, in CPPsiteProjPackage.CPP_genT]
in_single [lemma, in CPPsiteProjPackage.CPP_gen]
In_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
In_matters_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_list_remove_redund [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_list_In_list_not_In_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_list_In_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_In_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_length_same [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_same [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_diff [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
in_remove_in_init [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
in_not_touched_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_InT [lemma, in CPPsiteProjPackage.CPP_genT]
is_Atomic [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
is_atomicT [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
K
keep_list_delete_head_not_In [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]keep_list_delete_head_not_origin [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
L
LEM [axiom, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]LEM [section, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
LEM [axiom, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
LEM_world [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
LEM_Lindenbaum [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
LEM_prime [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
LEM_completeness [section, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
LEM_wSoundness [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
LEM.P [variable, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
length_le_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
leT [inductive, in CPPsiteProjPackage.CPP_genT]
leT_ex_plus [lemma, in CPPsiteProjPackage.CPP_genT]
leT_or_gt [lemma, in CPPsiteProjPackage.CPP_genT]
leT_S_or_eq [lemma, in CPPsiteProjPackage.CPP_genT]
leT_S_F [lemma, in CPPsiteProjPackage.CPP_genT]
leT_plus_l [lemma, in CPPsiteProjPackage.CPP_genT]
leT_plus_r [lemma, in CPPsiteProjPackage.CPP_genT]
leT_0_n [lemma, in CPPsiteProjPackage.CPP_genT]
leT_trans [definition, in CPPsiteProjPackage.CPP_genT]
leT_trans' [lemma, in CPPsiteProjPackage.CPP_genT]
leT_S_n [definition, in CPPsiteProjPackage.CPP_genT]
leT_S_n' [lemma, in CPPsiteProjPackage.CPP_genT]
leT_n_S [lemma, in CPPsiteProjPackage.CPP_genT]
leT_sind [definition, in CPPsiteProjPackage.CPP_genT]
leT_rec [definition, in CPPsiteProjPackage.CPP_genT]
leT_ind [definition, in CPPsiteProjPackage.CPP_genT]
leT_rect [definition, in CPPsiteProjPackage.CPP_genT]
leT_S [constructor, in CPPsiteProjPackage.CPP_genT]
leT_n [constructor, in CPPsiteProjPackage.CPP_genT]
Lindenbaum [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
list_disj_prime [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
list_disj [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
list_disj_remove_app [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_disj_app0 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_disj_app [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_all_pred_nat [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_consistent [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
list_consistent' [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
list_bounded [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
loc_conseq [definition, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
loc_conseq_BIH_model [definition, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
loc_conseq_dec [definition, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
L_ded2 [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
L_ded1 [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
L_ded_cumulative [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
L_ded [definition, in CPPsiteProjPackage.CPP_BiInt_enum]
L_enum_exhaustive [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
L_enum_cumulative [lemma, in CPPsiteProjPackage.CPP_BiInt_enum]
L_enum [definition, in CPPsiteProjPackage.CPP_BiInt_enum]
M
map_eq_nil [lemma, in CPPsiteProjPackage.CPP_gen]map_app_ex [lemma, in CPPsiteProjPackage.CPP_gen]
map_cons_ex' [lemma, in CPPsiteProjPackage.CPP_gen]
map_cons_ex [lemma, in CPPsiteProjPackage.CPP_gen]
max_of_list [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mforces [definition, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
model [record, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
model_dec [definition, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
ModEx [section, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
ModEx [definition, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
ModEx_WLEM [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
MP [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
MP [section, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
MP [definition, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
MPRule [inductive, in CPPsiteProjPackage.CPP_BiInt_GHC]
MPRule_sind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
MPRule_ind [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
MPRule_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
MP_stable [lemma, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
mult_disj_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mult_disj_dec1 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mult_disj_dec0 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mult_disj_Id [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mult_disj [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
N
nat_remove_In_smaller_length [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]nat_remove_le_length [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
Neg [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
nodes [projection, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
NoDup_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
NoDup_destr_split [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
NotDer [projection, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
NotDer [projection, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
NotDer [projection, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
not_In_prime_theory_deriv [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
not_removed_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
no_list_all_nat [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
nprime_theory_extens_le [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
nprime_theory_extens [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
nprime_theory [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
O
Or [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]or_false [lemma, in CPPsiteProjPackage.CPP_gen]
Or_imp_assoc [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
P
pair_eqI [lemma, in CPPsiteProjPackage.CPP_gen]pair_derrec [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
permut_remove_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
permut_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
persist [projection, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
Persistence [lemma, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
PiffD1 [lemma, in CPPsiteProjPackage.CPP_gen]
PiffD2 [lemma, in CPPsiteProjPackage.CPP_gen]
point_model_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
point_model [instance, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
point_model_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
point_model [instance, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
prim [projection, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
prim [projection, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
prim [projection, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
prime [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Prime [projection, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Prime [projection, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Prime [projection, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
prime_theory_extens [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
prime_theory [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
prod_nat_split [lemma, in CPPsiteProjPackage.CPP_genT]
prod_mono [lemma, in CPPsiteProjPackage.CPP_genT]
pseudo_complete [definition, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Q
QuasiComp [definition, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]QuasiComp_WLEMS [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
quasi_prime_Lind_pair [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
quasi_prime [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Quasi_completeness_WLEMS.Tp_bounded [variable, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.Tp [variable, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.p [variable, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.Hij [variable, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.j [variable, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.i [variable, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS [section, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
R
rappl [lemma, in CPPsiteProjPackage.CPP_gen]RA1 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA1_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA10 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA10_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA11 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA11_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA12 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA12_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA13 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA13_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA14 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA14_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA15 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA15_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA16 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA16_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA2 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA2_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA3 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA3_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA4 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA4_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA5 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA5_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA6 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA6_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA7 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA7_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA8 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA8_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA9 [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
RA9_I [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
reachable [projection, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
reach_tran [projection, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
reach_refl [projection, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
redund_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
redund_remove [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
redund_remove_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
relationT [definition, in CPPsiteProjPackage.CPP_genT]
remove_disj [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
remove_list_incr_decr [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr4 [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr2 [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr1 [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr3 [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_delete_origin [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_is_nil [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_in_nil [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_delete_head_In [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_delete_head [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_non_empty_inter_smaller_length [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_singl_id_or_nil [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_is_in [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_in_single [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_dist_app [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_cont [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_preserv_NoDup [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_of_nil [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list [definition, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_In_smaller_length [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_le_length [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_preserv_NoDup [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_not_in_anymore [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_dist_app [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
req [definition, in CPPsiteProjPackage.CPP_gen]
req_trans [lemma, in CPPsiteProjPackage.CPP_gen]
req_sym [lemma, in CPPsiteProjPackage.CPP_gen]
req_refl [lemma, in CPPsiteProjPackage.CPP_gen]
right_stable_Lind_pair [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
rls [definition, in CPPsiteProjPackage.CPP_gen]
rlsT [definition, in CPPsiteProjPackage.CPP_genT]
rsub [definition, in CPPsiteProjPackage.CPP_gen]
rsubD [definition, in CPPsiteProjPackage.CPP_gen]
rsubI [definition, in CPPsiteProjPackage.CPP_gen]
rsub_imp [definition, in CPPsiteProjPackage.CPP_gen]
rsub_id [lemma, in CPPsiteProjPackage.CPP_gen]
rsub_trans [lemma, in CPPsiteProjPackage.CPP_gen]
rsub_def [lemma, in CPPsiteProjPackage.CPP_gen]
rsub_emptyT [lemma, in CPPsiteProjPackage.CPP_genT]
S
SemDec_Completeness.MPax [variable, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]SemDec_Completeness [section, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
semidec [definition, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
SemidecCompleteness [definition, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
SemidecCompleteness_MP [lemma, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
SemidecCompleteness_MP_WDNS [lemma, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
semidec_enum [lemma, in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
size_form [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
Soundness_BIH_model [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Soundness_LEM [section, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
stable [definition, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Stable [projection, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Stable [projection, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Stable [projection, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
stable_Lind_pair [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
subst [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
subst_Ax [lemma, in CPPsiteProjPackage.CPP_BiInt_logic]
swap_remove_list [lemma, in CPPsiteProjPackage.CPP_BiInt_remove_list]
T
too_many_disj1 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]too_many_disj10 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
too_many_disj0 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
too_many_disj00 [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
Top [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
Top_wNeg_cons [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
Top_wNeg [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
Tp_consistent [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
TP_consistent [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
transitiveT [definition, in CPPsiteProjPackage.CPP_genT]
trivial_model_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
trivial_model [instance, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
trivial_model_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
trivial_model [instance, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
true_and [lemma, in CPPsiteProjPackage.CPP_gen]
truth_lemma [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
truth_lemma [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
truth_lemma [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
U
Under_Lind_pair [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]Under_Lind_pair_init [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Under_nprime_theory [lemma, in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
V
val [projection, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]valid_form [definition, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
Var [constructor, in CPPsiteProjPackage.CPP_BiInt_GHC]
Var' [definition, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Var' [definition, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
W
want_prod_under_universal4 [lemma, in CPPsiteProjPackage.CPP_genT]want_right_prod_under_universal' [lemma, in CPPsiteProjPackage.CPP_genT]
want_right_prod_under_universal [lemma, in CPPsiteProjPackage.CPP_genT]
want_left_prod_under_universal [lemma, in CPPsiteProjPackage.CPP_genT]
wAThm_irrel [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wBiLEM [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wClaim1 [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wCompleteness [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
wContr_Bot [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wDN_to_form [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wDN_dist_imp [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wdual_residuation_gen [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wdual_residuation [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wdual_residuation0 [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wEFQ [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
well_foundedT [definition, in CPPsiteProjPackage.CPP_genT]
wExcl_mon [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wforces [definition, in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
wforces_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
wimp_Id_gen [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
WLEM [axiom, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM [section, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEMS [axiom, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEMS_world [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEMS_Lindenbaum [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEMS_prime [lemma, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEMS_Quasi_completeness [section, in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEM_ModEx [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM_world [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM_Lindenbaum [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM_prime [lemma, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM.P [variable, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM.TP [variable, in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
wmonotL_Or [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wmonotR_Or [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wmonot_Or2 [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wmon_Excl [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wNeg [definition, in CPPsiteProjPackage.CPP_BiInt_GHC]
wNeg_Top [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wOr_Neg [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wQuasiCompleteness [lemma, in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
wSoundness [definition, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
wSoundness_LEM [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
wSoundness_dec [lemma, in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
wThm_irrel [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wTop [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wT_for_DN [lemma, in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
other
_ --> _ (My_scope) [notation, in CPPsiteProjPackage.CPP_BiInt_GHC]# _ (My_scope) [notation, in CPPsiteProjPackage.CPP_BiInt_GHC]
existsT2 _ .. _ , _ (type_scope) [notation, in CPPsiteProjPackage.CPP_existsT]
existsT _ .. _ , _ (type_scope) [notation, in CPPsiteProjPackage.CPP_existsT]
_ :: _ [notation, in CPPsiteProjPackage.CPP_BiInt_GHC]
T~ _ [notation, in CPPsiteProjPackage.CPP_genT]
[ _ ; .. ; _ ] [notation, in CPPsiteProjPackage.CPP_BiInt_GHC]
[ ] [notation, in CPPsiteProjPackage.CPP_BiInt_GHC]
Notation Index
other
_ --> _ (My_scope) [in CPPsiteProjPackage.CPP_BiInt_GHC]# _ (My_scope) [in CPPsiteProjPackage.CPP_BiInt_GHC]
existsT2 _ .. _ , _ (type_scope) [in CPPsiteProjPackage.CPP_existsT]
existsT _ .. _ , _ (type_scope) [in CPPsiteProjPackage.CPP_existsT]
_ :: _ [in CPPsiteProjPackage.CPP_BiInt_GHC]
T~ _ [in CPPsiteProjPackage.CPP_genT]
[ _ ; .. ; _ ] [in CPPsiteProjPackage.CPP_BiInt_GHC]
[ ] [in CPPsiteProjPackage.CPP_BiInt_GHC]
Variable Index
C
Completeness_LEM.TLEM [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]Completeness_LEM.P [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
L
LEM.P [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]Q
Quasi_completeness_WLEMS.Tp_bounded [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]Quasi_completeness_WLEMS.Tp [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.p [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.Hij [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.j [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Quasi_completeness_WLEMS.i [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
S
SemDec_Completeness.MPax [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]W
WLEM.P [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]WLEM.TP [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
Library Index
C
CPP_BiInt_meta_interactions1CPP_BiInt_ModEx_constr
CPP_BiInt_SemDec_completeness_constr
CPP_existsT
CPP_BiInt_remove_list
CPP_genT
CPP_BiInt_GHC
CPP_BiInt_Lindenbaum_lem_prelim
CPP_BiInt_completeness_constr
CPP_BiInt_logic
CPP_BiInt_enum
CPP_gen
CPP_BiInt_soundness_constr
CPP_BiInt_Kripke_sem_constr
CPP_BiInt_quasi_completeness_constr
CPP_BiInt_meta_interactions2
CPP_BiInt_Lindenbaum_lem
Lemma Index
A
absorp_Or1 [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]add_remove_list_preserve_NoDup [in CPPsiteProjPackage.CPP_BiInt_remove_list]
always_add_a_nat [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
and_true [in CPPsiteProjPackage.CPP_gen]
anonD [in CPPsiteProjPackage.CPP_genT]
anonI [in CPPsiteProjPackage.CPP_genT]
anon_forall [in CPPsiteProjPackage.CPP_genT]
anon_sigT [in CPPsiteProjPackage.CPP_genT]
anon_iffT [in CPPsiteProjPackage.CPP_genT]
anon_imp [in CPPsiteProjPackage.CPP_genT]
anon_sum [in CPPsiteProjPackage.CPP_genT]
anon_prod [in CPPsiteProjPackage.CPP_genT]
anon_eq [in CPPsiteProjPackage.CPP_genT]
appl [in CPPsiteProjPackage.CPP_gen]
app_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
arg_cong_imp' [in CPPsiteProjPackage.CPP_gen]
arg_cong_imp [in CPPsiteProjPackage.CPP_gen]
arg_cong [in CPPsiteProjPackage.CPP_gen]
arg1_cong_imp' [in CPPsiteProjPackage.CPP_gen]
arg1_cong_imp [in CPPsiteProjPackage.CPP_gen]
Ax_valid_BIH_model [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Ax_valid_dec [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Ax_valid_stable [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Ax_valid [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
B
BIH_Dual_Deduction_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]BIH_Dual_Detachment_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
BIH_Deduction_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
BIH_Detachment_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
BIH_finite' [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
BIH_finite' [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
BIH_finite [in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_struct [in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_comp [in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_monot [in CPPsiteProjPackage.CPP_BiInt_logic]
BIH_finite' [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
bounded_model_dec [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
bounded_model_dec' [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
C
closeder_fst_Lind_pair [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]comm_Or [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
comm_Or_obj [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
comm_And_obj [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
Completeness_LEM [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Compl_prime_theory_extens [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
consistency [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
consistency [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Consist_prime_theory [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Consist_nprime_theory [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
C_val_persist [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
C_R_trans [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
C_R_refl [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
C_val_persist [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
C_R_trans [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
C_R_refl [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
C_val_persist [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
C_R_trans [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
C_R_refl [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
D
der_prime_theory_nprime_theory [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]der_nprime_theory_mprime_theory_le [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
der_list_disj_remove2 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
der_list_disj_remove1 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
der_mult_disj_Bot [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
double_remove [in CPPsiteProjPackage.CPP_BiInt_remove_list]
E
emptyT_any [in CPPsiteProjPackage.CPP_genT]emptyT_any' [in CPPsiteProjPackage.CPP_genT]
empty_False [in CPPsiteProjPackage.CPP_genT]
empty_explosion [in CPPsiteProjPackage.CPP_genT]
eq_TrueI [in CPPsiteProjPackage.CPP_gen]
eq_dec_form [in CPPsiteProjPackage.CPP_BiInt_GHC]
eq_dec_nat [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
eq_S_F [in CPPsiteProjPackage.CPP_genT]
F
false_or [in CPPsiteProjPackage.CPP_gen]False_empty [in CPPsiteProjPackage.CPP_genT]
ForallT_Forall [in CPPsiteProjPackage.CPP_genT]
ForallT_Forall' [in CPPsiteProjPackage.CPP_genT]
ForallT_forall [in CPPsiteProjPackage.CPP_genT]
ForallT_impl [in CPPsiteProjPackage.CPP_genT]
ForallT_map_rev [in CPPsiteProjPackage.CPP_genT]
ForallT_map [in CPPsiteProjPackage.CPP_genT]
ForallT_map_2 [in CPPsiteProjPackage.CPP_genT]
ForallT_2 [in CPPsiteProjPackage.CPP_genT]
ForallT_append [in CPPsiteProjPackage.CPP_genT]
ForallT_cons_iff [in CPPsiteProjPackage.CPP_genT]
ForallT_single [in CPPsiteProjPackage.CPP_genT]
ForallT_cons_inv [in CPPsiteProjPackage.CPP_genT]
ForallT_inv [in CPPsiteProjPackage.CPP_genT]
Forall_map_2 [in CPPsiteProjPackage.CPP_gen]
Forall_map_single [in CPPsiteProjPackage.CPP_gen]
Forall_single [in CPPsiteProjPackage.CPP_gen]
Forall_append [in CPPsiteProjPackage.CPP_gen]
Forall_cons_iff [in CPPsiteProjPackage.CPP_gen]
Forall_cons_inv [in CPPsiteProjPackage.CPP_gen]
Forall_ForallT' [in CPPsiteProjPackage.CPP_genT]
Forall_ForallT [in CPPsiteProjPackage.CPP_genT]
Forall2T_ex_r [in CPPsiteProjPackage.CPP_genT]
Forall2T_ex_l [in CPPsiteProjPackage.CPP_genT]
Forall2T_app [in CPPsiteProjPackage.CPP_genT]
Forall2T_app_inv_r [in CPPsiteProjPackage.CPP_genT]
Forall2T_app_inv_l [in CPPsiteProjPackage.CPP_genT]
form_enum_ded_spec [in CPPsiteProjPackage.CPP_BiInt_enum]
form_index_inj [in CPPsiteProjPackage.CPP_BiInt_enum]
form_enum_index [in CPPsiteProjPackage.CPP_BiInt_enum]
form_enum_sur [in CPPsiteProjPackage.CPP_BiInt_enum]
fun_cong [in CPPsiteProjPackage.CPP_gen]
G
gen_cong [in CPPsiteProjPackage.CPP_gen]gen_BIH_Dual_Deduction_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
gen_BIH_Dual_Detachment_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
gen_BIH_Deduction_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
gen_BIH_Detachment_Theorem [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
I
Id_list_disj_remove [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]Id_list_disj [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
iffD1 [in CPPsiteProjPackage.CPP_gen]
iffD2 [in CPPsiteProjPackage.CPP_gen]
iffT_prod [in CPPsiteProjPackage.CPP_genT]
iffT_D2' [in CPPsiteProjPackage.CPP_genT]
iffT_D1' [in CPPsiteProjPackage.CPP_genT]
iffT_refl [in CPPsiteProjPackage.CPP_genT]
iffT_sym' [in CPPsiteProjPackage.CPP_genT]
iffT_trans [in CPPsiteProjPackage.CPP_genT]
inhabited_anon [in CPPsiteProjPackage.CPP_genT]
InT_remove [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
InT_In_eq' [in CPPsiteProjPackage.CPP_genT]
InT_In_eq [in CPPsiteProjPackage.CPP_genT]
InT_In' [in CPPsiteProjPackage.CPP_genT]
InT_In [in CPPsiteProjPackage.CPP_genT]
InT_concat [in CPPsiteProjPackage.CPP_genT]
InT_map_iffT [in CPPsiteProjPackage.CPP_genT]
InT_mapE [in CPPsiteProjPackage.CPP_genT]
InT_map [in CPPsiteProjPackage.CPP_genT]
InT_inv [in CPPsiteProjPackage.CPP_genT]
InT_split [in CPPsiteProjPackage.CPP_genT]
InT_nilE [in CPPsiteProjPackage.CPP_genT]
InT_nilE' [in CPPsiteProjPackage.CPP_genT]
InT_appE [in CPPsiteProjPackage.CPP_genT]
InT_appE' [in CPPsiteProjPackage.CPP_genT]
InT_appR [in CPPsiteProjPackage.CPP_genT]
InT_appL [in CPPsiteProjPackage.CPP_genT]
InT_eq [in CPPsiteProjPackage.CPP_genT]
in_single [in CPPsiteProjPackage.CPP_gen]
In_remove [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
In_matters_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_list_remove_redund [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_list_In_list_not_In_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_list_In_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_In_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_length_same [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_same [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_remove_diff [in CPPsiteProjPackage.CPP_BiInt_remove_list]
in_remove_in_init [in CPPsiteProjPackage.CPP_BiInt_remove_list]
in_not_touched_remove [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_dec [in CPPsiteProjPackage.CPP_BiInt_remove_list]
In_InT [in CPPsiteProjPackage.CPP_genT]
K
keep_list_delete_head_not_In [in CPPsiteProjPackage.CPP_BiInt_remove_list]keep_list_delete_head_not_origin [in CPPsiteProjPackage.CPP_BiInt_remove_list]
L
LEM_world [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]LEM_Lindenbaum [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
LEM_prime [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
LEM_wSoundness [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
length_le_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
leT_ex_plus [in CPPsiteProjPackage.CPP_genT]
leT_or_gt [in CPPsiteProjPackage.CPP_genT]
leT_S_or_eq [in CPPsiteProjPackage.CPP_genT]
leT_S_F [in CPPsiteProjPackage.CPP_genT]
leT_plus_l [in CPPsiteProjPackage.CPP_genT]
leT_plus_r [in CPPsiteProjPackage.CPP_genT]
leT_0_n [in CPPsiteProjPackage.CPP_genT]
leT_trans' [in CPPsiteProjPackage.CPP_genT]
leT_S_n' [in CPPsiteProjPackage.CPP_genT]
leT_n_S [in CPPsiteProjPackage.CPP_genT]
Lindenbaum [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
list_disj_prime [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
list_disj_remove_app [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_disj_app0 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_disj_app [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_all_pred_nat [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
list_consistent [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
list_consistent' [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
list_bounded [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
L_ded2 [in CPPsiteProjPackage.CPP_BiInt_enum]
L_ded1 [in CPPsiteProjPackage.CPP_BiInt_enum]
L_ded_cumulative [in CPPsiteProjPackage.CPP_BiInt_enum]
L_enum_exhaustive [in CPPsiteProjPackage.CPP_BiInt_enum]
L_enum_cumulative [in CPPsiteProjPackage.CPP_BiInt_enum]
M
map_eq_nil [in CPPsiteProjPackage.CPP_gen]map_app_ex [in CPPsiteProjPackage.CPP_gen]
map_cons_ex' [in CPPsiteProjPackage.CPP_gen]
map_cons_ex [in CPPsiteProjPackage.CPP_gen]
max_of_list [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
ModEx_WLEM [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
MP_stable [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
mult_disj_dec [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mult_disj_dec1 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mult_disj_dec0 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
mult_disj_Id [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
N
nat_remove_In_smaller_length [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]nat_remove_le_length [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
NoDup_remove [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
NoDup_destr_split [in CPPsiteProjPackage.CPP_BiInt_remove_list]
not_In_prime_theory_deriv [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
not_removed_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
no_list_all_nat [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
nprime_theory_extens_le [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
nprime_theory_extens [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
O
or_false [in CPPsiteProjPackage.CPP_gen]Or_imp_assoc [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
P
pair_eqI [in CPPsiteProjPackage.CPP_gen]permut_remove_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
permut_remove [in CPPsiteProjPackage.CPP_BiInt_remove_list]
Persistence [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
PiffD1 [in CPPsiteProjPackage.CPP_gen]
PiffD2 [in CPPsiteProjPackage.CPP_gen]
point_model_dec [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
point_model_dec [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
prime_theory_extens [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
prod_nat_split [in CPPsiteProjPackage.CPP_genT]
prod_mono [in CPPsiteProjPackage.CPP_genT]
Q
QuasiComp_WLEMS [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]quasi_prime_Lind_pair [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Quasi_completeness [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
R
rappl [in CPPsiteProjPackage.CPP_gen]redund_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
redund_remove [in CPPsiteProjPackage.CPP_BiInt_remove_list]
redund_remove_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_disj [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
remove_list_incr_decr [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr4 [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr2 [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr1 [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_incr_decr3 [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_delete_origin [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_is_nil [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_in_nil [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_delete_head_In [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_delete_head [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_non_empty_inter_smaller_length [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_singl_id_or_nil [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_is_in [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_in_single [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_dist_app [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_cont [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_preserv_NoDup [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_list_of_nil [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_In_smaller_length [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_le_length [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_preserv_NoDup [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_not_in_anymore [in CPPsiteProjPackage.CPP_BiInt_remove_list]
remove_dist_app [in CPPsiteProjPackage.CPP_BiInt_remove_list]
req_trans [in CPPsiteProjPackage.CPP_gen]
req_sym [in CPPsiteProjPackage.CPP_gen]
req_refl [in CPPsiteProjPackage.CPP_gen]
right_stable_Lind_pair [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
rsub_id [in CPPsiteProjPackage.CPP_gen]
rsub_trans [in CPPsiteProjPackage.CPP_gen]
rsub_def [in CPPsiteProjPackage.CPP_gen]
rsub_emptyT [in CPPsiteProjPackage.CPP_genT]
S
SemidecCompleteness_MP [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]SemidecCompleteness_MP_WDNS [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
semidec_enum [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
Soundness_BIH_model [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
stable_Lind_pair [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
subst_Ax [in CPPsiteProjPackage.CPP_BiInt_logic]
swap_remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
T
too_many_disj1 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]too_many_disj10 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
too_many_disj0 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
too_many_disj00 [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
Top_wNeg_cons [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
Top_wNeg [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
Tp_consistent [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
TP_consistent [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
trivial_model_dec [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
trivial_model_dec [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
true_and [in CPPsiteProjPackage.CPP_gen]
truth_lemma [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
truth_lemma [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
truth_lemma [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
U
Under_Lind_pair [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]Under_Lind_pair_init [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
Under_nprime_theory [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
W
want_prod_under_universal4 [in CPPsiteProjPackage.CPP_genT]want_right_prod_under_universal' [in CPPsiteProjPackage.CPP_genT]
want_right_prod_under_universal [in CPPsiteProjPackage.CPP_genT]
want_left_prod_under_universal [in CPPsiteProjPackage.CPP_genT]
wAThm_irrel [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wBiLEM [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wClaim1 [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wCompleteness [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
wContr_Bot [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wDN_to_form [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wDN_dist_imp [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wdual_residuation_gen [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wdual_residuation [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wdual_residuation0 [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wEFQ [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wExcl_mon [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wforces_dec [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
wimp_Id_gen [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
WLEMS_world [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEMS_Lindenbaum [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEMS_prime [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
WLEM_ModEx [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM_world [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM_Lindenbaum [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
WLEM_prime [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
wmonotL_Or [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wmonotR_Or [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wmonot_Or2 [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wmon_Excl [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wNeg_Top [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wOr_Neg [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
wQuasiCompleteness [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
wSoundness_LEM [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
wSoundness_dec [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
wThm_irrel [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wTop [in CPPsiteProjPackage.CPP_BiInt_meta_interactions1]
wT_for_DN [in CPPsiteProjPackage.CPP_BiInt_meta_interactions2]
Constructor Index
A
AccT_intro [in CPPsiteProjPackage.CPP_genT]And [in CPPsiteProjPackage.CPP_BiInt_GHC]
Ax [in CPPsiteProjPackage.CPP_BiInt_GHC]
AxRule_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
B
Bot [in CPPsiteProjPackage.CPP_BiInt_GHC]D
DNw [in CPPsiteProjPackage.CPP_BiInt_GHC]DNwRule_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
E
Excl [in CPPsiteProjPackage.CPP_BiInt_GHC]F
ForallT_cons [in CPPsiteProjPackage.CPP_genT]ForallT_nil [in CPPsiteProjPackage.CPP_genT]
Forall2T_cons [in CPPsiteProjPackage.CPP_genT]
Forall2T_nil [in CPPsiteProjPackage.CPP_genT]
I
Id [in CPPsiteProjPackage.CPP_BiInt_GHC]IdRule_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
Imp [in CPPsiteProjPackage.CPP_BiInt_GHC]
IndClo [in CPPsiteProjPackage.CPP_BiInt_GHC]
InitClo [in CPPsiteProjPackage.CPP_BiInt_GHC]
InT_cons [in CPPsiteProjPackage.CPP_genT]
InT_eq' [in CPPsiteProjPackage.CPP_genT]
L
leT_S [in CPPsiteProjPackage.CPP_genT]leT_n [in CPPsiteProjPackage.CPP_genT]
M
MP [in CPPsiteProjPackage.CPP_BiInt_GHC]MPRule_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
O
Or [in CPPsiteProjPackage.CPP_BiInt_GHC]R
RA1_I [in CPPsiteProjPackage.CPP_BiInt_GHC]RA10_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA11_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA12_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA13_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA14_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA15_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA16_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA2_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA3_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA4_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA5_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA6_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA7_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA8_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA9_I [in CPPsiteProjPackage.CPP_BiInt_GHC]
T
Top [in CPPsiteProjPackage.CPP_BiInt_GHC]V
Var [in CPPsiteProjPackage.CPP_BiInt_GHC]Axiom Index
I
i [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]L
LEM [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]LEM [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
W
WLEM [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]WLEMS [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Inductive Index
A
AccT [in CPPsiteProjPackage.CPP_genT]AxRule [in CPPsiteProjPackage.CPP_BiInt_GHC]
B
BIAxioms [in CPPsiteProjPackage.CPP_BiInt_GHC]BIH_rules [in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF [in CPPsiteProjPackage.CPP_BiInt_GHC]
D
DNwRule [in CPPsiteProjPackage.CPP_BiInt_GHC]DN_clos_set [in CPPsiteProjPackage.CPP_BiInt_GHC]
E
empty [in CPPsiteProjPackage.CPP_genT]emptyT [in CPPsiteProjPackage.CPP_genT]
empty_relT [in CPPsiteProjPackage.CPP_genT]
F
ForallT [in CPPsiteProjPackage.CPP_genT]Forall2T [in CPPsiteProjPackage.CPP_genT]
I
IdRule [in CPPsiteProjPackage.CPP_BiInt_GHC]InT [in CPPsiteProjPackage.CPP_genT]
L
leT [in CPPsiteProjPackage.CPP_genT]M
MPRule [in CPPsiteProjPackage.CPP_BiInt_GHC]Projection Index
C
Closed [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]Closed [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Closed [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
N
nodes [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]NotDer [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
NotDer [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
NotDer [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
P
persist [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]prim [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
prim [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
prim [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
Prime [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Prime [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Prime [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
R
reachable [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]reach_tran [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
reach_refl [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
S
Stable [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]Stable [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Stable [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
V
val [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]Instance Index
B
bounded_model [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]C
CM [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]CM [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
CM [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
P
point_model [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]point_model [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
T
trivial_model [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]trivial_model [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
Section Index
B
BIH_model_Sound [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]C
Completeness_LEM [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]Constr_Sound [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
L
LEM [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]LEM_completeness [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
M
ModEx [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]MP [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
Q
Quasi_completeness_WLEMS [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]S
SemDec_Completeness [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]Soundness_LEM [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
W
WLEM [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]WLEMS_Quasi_completeness [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Definition Index
A
AccT_sind [in CPPsiteProjPackage.CPP_genT]AccT_rec [in CPPsiteProjPackage.CPP_genT]
AccT_ind [in CPPsiteProjPackage.CPP_genT]
AccT_rect [in CPPsiteProjPackage.CPP_genT]
anon [in CPPsiteProjPackage.CPP_genT]
AxRule_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]
AxRule_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
B
BIAxioms_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]BIAxioms_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
BIH_rules_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]
BIH_rules_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_rec [in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
BPropF_rect [in CPPsiteProjPackage.CPP_BiInt_GHC]
C
Canon_val [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]Canon_rel [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Canon_val [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Canon_rel [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Canon_val [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
Canon_rel [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
choice_code [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
choice_form [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
closed [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
complete [in CPPsiteProjPackage.CPP_BiInt_GHC]
Completeness [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
D
DNwRule_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]DNwRule_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
DN_clos_set_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]
DN_clos_set_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
DN_form [in CPPsiteProjPackage.CPP_BiInt_GHC]
E
emptyT_sind [in CPPsiteProjPackage.CPP_genT]emptyT_rec [in CPPsiteProjPackage.CPP_genT]
emptyT_ind [in CPPsiteProjPackage.CPP_genT]
emptyT_rect [in CPPsiteProjPackage.CPP_genT]
empty_sind [in CPPsiteProjPackage.CPP_genT]
empty_rec [in CPPsiteProjPackage.CPP_genT]
empty_ind [in CPPsiteProjPackage.CPP_genT]
empty_rect [in CPPsiteProjPackage.CPP_genT]
empty_relT_sind [in CPPsiteProjPackage.CPP_genT]
empty_relT_rec [in CPPsiteProjPackage.CPP_genT]
empty_relT_ind [in CPPsiteProjPackage.CPP_genT]
empty_relT_rect [in CPPsiteProjPackage.CPP_genT]
enum [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
F
ForallTD_forall [in CPPsiteProjPackage.CPP_genT]ForallTI_forall [in CPPsiteProjPackage.CPP_genT]
ForallT_2I [in CPPsiteProjPackage.CPP_genT]
ForallT_2I' [in CPPsiteProjPackage.CPP_genT]
ForallT_D2 [in CPPsiteProjPackage.CPP_genT]
ForallT_D1 [in CPPsiteProjPackage.CPP_genT]
ForallT_2D [in CPPsiteProjPackage.CPP_genT]
ForallT_appendI [in CPPsiteProjPackage.CPP_genT]
ForallT_appendI' [in CPPsiteProjPackage.CPP_genT]
ForallT_appendD2 [in CPPsiteProjPackage.CPP_genT]
ForallT_appendD1 [in CPPsiteProjPackage.CPP_genT]
ForallT_appendD [in CPPsiteProjPackage.CPP_genT]
ForallT_singleI [in CPPsiteProjPackage.CPP_genT]
ForallT_singleD [in CPPsiteProjPackage.CPP_genT]
ForallT_sind [in CPPsiteProjPackage.CPP_genT]
ForallT_rec [in CPPsiteProjPackage.CPP_genT]
ForallT_ind [in CPPsiteProjPackage.CPP_genT]
ForallT_rect [in CPPsiteProjPackage.CPP_genT]
Forall2T_sind [in CPPsiteProjPackage.CPP_genT]
Forall2T_rec [in CPPsiteProjPackage.CPP_genT]
Forall2T_ind [in CPPsiteProjPackage.CPP_genT]
Forall2T_rect [in CPPsiteProjPackage.CPP_genT]
form_enum_ded [in CPPsiteProjPackage.CPP_BiInt_enum]
form_index [in CPPsiteProjPackage.CPP_BiInt_enum]
form_index' [in CPPsiteProjPackage.CPP_BiInt_enum]
form_enum [in CPPsiteProjPackage.CPP_BiInt_enum]
fromlist [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
fromlist [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
fromlist [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
I
IdRule_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]IdRule_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
iffT_D2 [in CPPsiteProjPackage.CPP_genT]
iffT_D1 [in CPPsiteProjPackage.CPP_genT]
iffT_sym [in CPPsiteProjPackage.CPP_genT]
InT_mapI [in CPPsiteProjPackage.CPP_genT]
InT_2nd [in CPPsiteProjPackage.CPP_genT]
InT_sind [in CPPsiteProjPackage.CPP_genT]
InT_rec [in CPPsiteProjPackage.CPP_genT]
InT_ind [in CPPsiteProjPackage.CPP_genT]
InT_rect [in CPPsiteProjPackage.CPP_genT]
is_Atomic [in CPPsiteProjPackage.CPP_BiInt_GHC]
is_atomicT [in CPPsiteProjPackage.CPP_BiInt_GHC]
L
leT_trans [in CPPsiteProjPackage.CPP_genT]leT_S_n [in CPPsiteProjPackage.CPP_genT]
leT_sind [in CPPsiteProjPackage.CPP_genT]
leT_rec [in CPPsiteProjPackage.CPP_genT]
leT_ind [in CPPsiteProjPackage.CPP_genT]
leT_rect [in CPPsiteProjPackage.CPP_genT]
list_disj [in CPPsiteProjPackage.CPP_BiInt_GHC]
loc_conseq [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
loc_conseq_BIH_model [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
loc_conseq_dec [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
L_ded [in CPPsiteProjPackage.CPP_BiInt_enum]
L_enum [in CPPsiteProjPackage.CPP_BiInt_enum]
M
mforces [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]model_dec [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
ModEx [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
MP [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
MPRule_sind [in CPPsiteProjPackage.CPP_BiInt_GHC]
MPRule_ind [in CPPsiteProjPackage.CPP_BiInt_GHC]
mult_disj [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem_prelim]
N
Neg [in CPPsiteProjPackage.CPP_BiInt_GHC]nprime_theory [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
P
pair_derrec [in CPPsiteProjPackage.CPP_BiInt_GHC]prime [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
prime_theory [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
pseudo_complete [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Q
QuasiComp [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]quasi_prime [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
R
RA1 [in CPPsiteProjPackage.CPP_BiInt_GHC]RA10 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA11 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA12 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA13 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA14 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA15 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA16 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA2 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA3 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA4 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA5 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA6 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA7 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA8 [in CPPsiteProjPackage.CPP_BiInt_GHC]
RA9 [in CPPsiteProjPackage.CPP_BiInt_GHC]
relationT [in CPPsiteProjPackage.CPP_genT]
remove_list [in CPPsiteProjPackage.CPP_BiInt_remove_list]
req [in CPPsiteProjPackage.CPP_gen]
rls [in CPPsiteProjPackage.CPP_gen]
rlsT [in CPPsiteProjPackage.CPP_genT]
rsub [in CPPsiteProjPackage.CPP_gen]
rsubD [in CPPsiteProjPackage.CPP_gen]
rsubI [in CPPsiteProjPackage.CPP_gen]
rsub_imp [in CPPsiteProjPackage.CPP_gen]
S
semidec [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]SemidecCompleteness [in CPPsiteProjPackage.CPP_BiInt_SemDec_completeness_constr]
size_form [in CPPsiteProjPackage.CPP_BiInt_GHC]
stable [in CPPsiteProjPackage.CPP_BiInt_Lindenbaum_lem]
subst [in CPPsiteProjPackage.CPP_BiInt_GHC]
T
transitiveT [in CPPsiteProjPackage.CPP_genT]V
valid_form [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]Var' [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]
Var' [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
W
well_foundedT [in CPPsiteProjPackage.CPP_genT]wforces [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]
wNeg [in CPPsiteProjPackage.CPP_BiInt_GHC]
wSoundness [in CPPsiteProjPackage.CPP_BiInt_soundness_constr]
Record Index
C
Canon_worlds [in CPPsiteProjPackage.CPP_BiInt_quasi_completeness_constr]Canon_worlds [in CPPsiteProjPackage.CPP_BiInt_completeness_constr]
Canon_worlds [in CPPsiteProjPackage.CPP_BiInt_ModEx_constr]
M
model [in CPPsiteProjPackage.CPP_BiInt_Kripke_sem_constr]| 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 | (611 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 | (8 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 | (12 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 | (17 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 | (315 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 | (42 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 | (5 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 | (16 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 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) |
| 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 | (12 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 | (151 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 | (4 entries) |