| 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 | (604 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 | (9 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 | (310 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) |
| 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 | (43 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 | (18 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 | (19 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 | (15 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 | (7 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 | (160 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
A [constructor, in iS4_GG_translation]ABC [inductive, in iS4_GG_translation]
ABCreach [definition, in iS4_GG_translation]
ABCreach_trans [lemma, in iS4_GG_translation]
ABCreach_refl [lemma, in iS4_GG_translation]
ABC_upset [instance, in iS4_GG_translation]
ABC_is_upset [lemma, in iS4_GG_translation]
ABC_sind [definition, in iS4_GG_translation]
ABC_rec [definition, in iS4_GG_translation]
ABC_ind [definition, in iS4_GG_translation]
ABC_rect [definition, in iS4_GG_translation]
absorp_Or1 [lemma, in GHC.iS4H_properties]
AB_upset [instance, in iS4_GG_translation]
AB_is_upset [lemma, in iS4_GG_translation]
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]
And [constructor, in Syntax.iS4_Syntax]
and_true [lemma, in General.gen]
And_Imp [lemma, in GHC.iS4H_properties]
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_split_at_sind [definition, in General.List_lemmasT]
app_split_at_rec [definition, in General.List_lemmasT]
app_split_at_ind [definition, in General.List_lemmasT]
app_split_at_rect [definition, in General.List_lemmasT]
app_split_at [inductive, in General.List_lemmasT]
app_eq_appT2_single_tlR [lemma, in General.List_lemmasT]
app_eq_appT2_single_tlL [lemma, in General.List_lemmasT]
app_eq_appT2_single_hdR [lemma, in General.List_lemmasT]
app_eq_appT2_single_hdL [lemma, in General.List_lemmasT]
app_eq_appT2_nn [lemma, in General.List_lemmasT]
app_tl_inversion [lemma, in General.List_lemmasT]
app_hd_inversion [lemma, in General.List_lemmasT]
app_singleton_tl_inversion [lemma, in General.List_lemmasT]
app_singleton_inversion [lemma, in General.List_lemmasT]
app_eq_unitT2 [lemma, in General.List_lemmasT]
app_eq_consT [definition, in General.List_lemmasT]
app_eq_appT2 [lemma, in General.List_lemmasT]
app_eq_appT [lemma, in General.List_lemmasT]
app_eq_app [lemma, in General.List_lemmasT]
app_eq_nilT [lemma, in General.List_lemmasT]
app_eq_consT2 [definition, in General.List_lemmasT]
app_eq_cons [definition, in General.List_lemmasT]
app_cons_single [lemma, in General.List_lemmasT]
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]
asa_eq [lemma, in General.List_lemmasT]
asa_appR [constructor, in General.List_lemmasT]
asa_appL [constructor, in General.List_lemmasT]
asa_single [constructor, in General.List_lemmasT]
Ax [constructor, in GHC.iS4H]
Axioms [definition, in GHC.iS4H]
AxRule [inductive, in GHC.iS4H]
AxRule_sind [definition, in GHC.iS4H]
AxRule_ind [definition, in GHC.iS4H]
AxRule_I [constructor, in GHC.iS4H]
Ax_valid [lemma, in Topology.iS4_soundness]
B
B [constructor, in iS4_GG_translation]BC_upset [instance, in iS4_GG_translation]
BC_is_upset [lemma, in iS4_GG_translation]
Bot [constructor, in Syntax.iS4_Syntax]
Box [constructor, in Syntax.iS4_Syntax]
BoxOne [definition, in Syntax.iS4_Syntax]
BoxOne_UnBox_fixpoint [lemma, in Syntax.iS4_Syntax]
Box_UnBox_BoxOne_id [lemma, in Syntax.iS4_Syntax]
Box_list [definition, in Syntax.iS4_Syntax]
Box_distrib_list_Imp [lemma, in GHC.iS4H_properties]
B_upset [instance, in iS4_GG_translation]
B_is_upset [lemma, in iS4_GG_translation]
C
C [constructor, in iS4_GG_translation]canonical_form_upset_P [lemma, in iS4_GG_translation]
Canon_val [definition, in Topology.iS4_completeness]
Canon_rel [definition, in Topology.iS4_completeness]
Canon_worlds [record, in Topology.iS4_completeness]
choice_code [definition, in GHC.iS4_Lindenbaum_lem]
choice_form [definition, in GHC.iS4_Lindenbaum_lem]
Ci [instance, in Topology.iS4_completeness]
Ci_4 [lemma, in Topology.iS4_completeness]
Ci_T [lemma, in Topology.iS4_completeness]
Ci_inter [lemma, in Topology.iS4_completeness]
Ci_unit [lemma, in Topology.iS4_completeness]
Ci_upset [lemma, in Topology.iS4_completeness]
Ci_uset [definition, in Topology.iS4_completeness]
Clos [definition, in Syntax.iS4_Syntax]
ClosOneBox [definition, in Syntax.iS4_Syntax]
ClosSubform [definition, in Syntax.iS4_Syntax]
CM [instance, in Topology.iS4_completeness]
comm_Or [lemma, in GHC.iS4H_properties]
comm_Or_obj [lemma, in GHC.iS4H_properties]
comm_And_obj [lemma, in GHC.iS4H_properties]
Completeness [section, in Topology.iS4_completeness]
Consist_Lind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
Consist_nLind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
cons_singleton [lemma, in General.List_lemmasT]
cons_eq_appT2 [lemma, in General.List_lemmasT]
cons_eq_appT [lemma, in General.List_lemmasT]
cons_eq_app [lemma, in General.List_lemmasT]
cons_single [lemma, in General.List_lemmasT]
Contr_Bot [lemma, in GHC.iS4H_properties]
CPre [instance, in Topology.iS4_completeness]
C_val_persist [lemma, in Topology.iS4_completeness]
C_R_trans [lemma, in Topology.iS4_completeness]
C_R_refl [lemma, in Topology.iS4_completeness]
C_upset [instance, in iS4_GG_translation]
C_is_upset [lemma, in iS4_GG_translation]
D
der_Lind_theory_nLind_theory [lemma, in GHC.iS4_Lindenbaum_lem]der_nLind_theory_mLind_theory_le [lemma, in GHC.iS4_Lindenbaum_lem]
DNE_Box_Bot [lemma, in iS4_GG_translation]
double_BoxOne [lemma, in Syntax.iS4_Syntax]
E
EFQ [lemma, in GHC.iS4H_properties]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]
Empty_upset [instance, in iS4_GG_translation]
Empty_is_upset [lemma, in iS4_GG_translation]
eq_S_F [lemma, in General.genT]
eq_dec_form [lemma, in Syntax.iS4_Syntax]
eq_nnn_app [definition, in General.List_lemmasT]
eq_app_canc2 [lemma, in General.List_lemmasT]
eq_app_canc1 [lemma, in General.List_lemmasT]
eq_TrueI [lemma, in General.gen]
existsT [library]
Explosion [lemma, in GHC.iS4H_properties]
F
Failure [lemma, in iS4_GG_translation]Failure_of_GG [section, in iS4_GG_translation]
False_empty [lemma, in General.genT]
false_or [lemma, in General.gen]
Finite_Intersection [definition, in Topology.iS4_completeness]
ForallT [inductive, in General.genT]
ForallTD_forall [definition, in General.genT]
ForallTI_forall [definition, in General.genT]
ForallT_Forall [lemma, in General.genT]
ForallT_Forall' [lemma, in General.genT]
ForallT_forall [lemma, in General.genT]
ForallT_impl [lemma, in General.genT]
ForallT_2I [definition, in General.genT]
ForallT_2I' [definition, in General.genT]
ForallT_D2 [definition, in General.genT]
ForallT_D1 [definition, in General.genT]
ForallT_2D [definition, in General.genT]
ForallT_map_rev [lemma, in General.genT]
ForallT_map [lemma, in General.genT]
ForallT_map_2 [lemma, in General.genT]
ForallT_2 [lemma, in General.genT]
ForallT_appendI [definition, in General.genT]
ForallT_appendI' [definition, in General.genT]
ForallT_appendD2 [definition, in General.genT]
ForallT_appendD1 [definition, in General.genT]
ForallT_appendD [definition, in General.genT]
ForallT_append [lemma, in General.genT]
ForallT_cons_iff [lemma, in General.genT]
ForallT_singleI [definition, in General.genT]
ForallT_singleD [definition, in General.genT]
ForallT_single [lemma, in General.genT]
ForallT_cons_inv [lemma, in General.genT]
ForallT_inv [lemma, in General.genT]
ForallT_sind [definition, in General.genT]
ForallT_rec [definition, in General.genT]
ForallT_ind [definition, in General.genT]
ForallT_rect [definition, in General.genT]
ForallT_cons [constructor, in General.genT]
ForallT_nil [constructor, in General.genT]
Forall_ForallT' [lemma, in General.genT]
Forall_ForallT [lemma, in General.genT]
Forall_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]
forces [definition, in Topology.iS4_topol_sem]
force_truthset [lemma, in Topology.iS4_topol_sem]
force_Box_interior_truthset [lemma, in Topology.iS4_topol_sem]
form [inductive, in Syntax.iS4_Syntax]
form_enum_ded_spec [lemma, in GHC.iS4_enum]
form_enum_ded [definition, in GHC.iS4_enum]
form_index_inj [lemma, in GHC.iS4_enum]
form_enum_index [lemma, in GHC.iS4_enum]
form_index [definition, in GHC.iS4_enum]
form_index' [definition, in GHC.iS4_enum]
form_enum_sur [lemma, in GHC.iS4_enum]
form_enum [definition, in GHC.iS4_enum]
form_sind [definition, in Syntax.iS4_Syntax]
form_rec [definition, in Syntax.iS4_Syntax]
form_ind [definition, in Syntax.iS4_Syntax]
form_rect [definition, in Syntax.iS4_Syntax]
fun_cong [lemma, in General.gen]
G
gen [library]general_export [library]
genT [library]
gen_cong [lemma, in General.gen]
I
i [projection, in Topology.iS4_topol_sem]IAxioms [inductive, in GHC.iS4H]
IAxioms_sind [definition, in GHC.iS4H]
IAxioms_ind [definition, in GHC.iS4H]
IA1 [definition, in GHC.iS4H]
IA1_I [constructor, in GHC.iS4H]
IA2 [definition, in GHC.iS4H]
IA2_I [constructor, in GHC.iS4H]
IA3 [definition, in GHC.iS4H]
IA3_I [constructor, in GHC.iS4H]
IA4 [definition, in GHC.iS4H]
IA4_I [constructor, in GHC.iS4H]
IA5 [definition, in GHC.iS4H]
IA5_I [constructor, in GHC.iS4H]
IA6 [definition, in GHC.iS4H]
IA6_I [constructor, in GHC.iS4H]
IA7 [definition, in GHC.iS4H]
IA7_I [constructor, in GHC.iS4H]
IA8 [definition, in GHC.iS4H]
IA8_I [constructor, in GHC.iS4H]
IA9 [definition, in GHC.iS4H]
IA9_I [constructor, in GHC.iS4H]
Id [constructor, in GHC.iS4H]
IdRule [inductive, in GHC.iS4H]
IdRule_sind [definition, in GHC.iS4H]
IdRule_ind [definition, in GHC.iS4H]
IdRule_I [constructor, in GHC.iS4H]
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]
if_rev_eq [lemma, in General.List_lemmasT]
if_eq_rev_eq [lemma, in General.List_lemmasT]
Imp [constructor, in Syntax.iS4_Syntax]
Imp_list_Imp [lemma, in GHC.iS4H_properties]
Imp_And [lemma, in GHC.iS4H_properties]
Imp_trans [lemma, in GHC.iS4H_properties]
Imp_trans_help427 [lemma, in GHC.iS4H_properties]
Imp_trans_help410 [lemma, in GHC.iS4H_properties]
Imp_trans_help170 [lemma, in GHC.iS4H_properties]
Imp_trans_help54 [lemma, in GHC.iS4H_properties]
Imp_trans_help37 [lemma, in GHC.iS4H_properties]
Imp_trans_help35 [lemma, in GHC.iS4H_properties]
Imp_trans_help14 [lemma, in GHC.iS4H_properties]
Imp_trans_help9 [lemma, in GHC.iS4H_properties]
Imp_trans_help8 [lemma, in GHC.iS4H_properties]
Imp_trans_help7 [lemma, in GHC.iS4H_properties]
imp_Id_gen [lemma, in GHC.iS4H_properties]
incl_Lind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
incl_nLind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
Incl_ClosSubform_Clos [lemma, in Syntax.iS4_Syntax]
Incl_Set_ClosSubform [lemma, in Syntax.iS4_Syntax]
Inf_Union [definition, in Topology.iS4_completeness]
inhabited_anon [lemma, in General.genT]
InT [inductive, in General.genT]
inter_conj [lemma, in Topology.iS4_topol_sem]
inter_upset [instance, in Topology.iS4_topol_sem]
inter_is_upset [lemma, in Topology.iS4_topol_sem]
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_or_app [lemma, in General.List_lemmasT]
InT_app_or [lemma, in General.List_lemmasT]
InT_singleton_mid [lemma, in General.List_lemmasT]
InT_mid [lemma, in General.List_lemmasT]
InT_pt_I [lemma, in General.List_lemmasT]
InT_pair_triple_sind [definition, in General.List_lemmasT]
InT_pair_triple_rec [definition, in General.List_lemmasT]
InT_pair_triple_ind [definition, in General.List_lemmasT]
InT_pair_triple_rect [definition, in General.List_lemmasT]
InT_pt_tl [constructor, in General.List_lemmasT]
InT_pt_hd [constructor, in General.List_lemmasT]
InT_pair_triple [inductive, in General.List_lemmasT]
InT_remove [lemma, in GHC.iS4H_properties]
In_InT [lemma, in General.genT]
In_Clos_BoxOne [lemma, in Syntax.iS4_Syntax]
In_Clos_not_box [lemma, in Syntax.iS4_Syntax]
In_form_dec [lemma, in Syntax.iS4_Syntax]
in_single [lemma, in General.gen]
In_Box_list_In_list [lemma, in GHC.iS4H_properties]
In_list_In_Box_list [lemma, in GHC.iS4H_properties]
In_remove [lemma, in GHC.iS4H_properties]
is_upset [projection, in Topology.iS4_topol_sem]
iS4H [library]
iS4H_prv [definition, in GHC.iS4H]
iS4H_rules_sind [definition, in GHC.iS4H]
iS4H_rules_ind [definition, in GHC.iS4H]
iS4H_rules [inductive, in GHC.iS4H]
iS4H_finite [lemma, in GHC.iS4H_logic]
iS4H_struct [lemma, in GHC.iS4H_logic]
iS4H_comp [lemma, in GHC.iS4H_logic]
iS4H_monot [lemma, in GHC.iS4H_logic]
iS4H_Imp_list_Detachment_Deduction_Theorem [lemma, in GHC.iS4H_properties]
iS4H_Deduction_Theorem [lemma, in GHC.iS4H_properties]
iS4H_Detachment_Theorem [lemma, in GHC.iS4H_properties]
iS4H_export [library]
iS4H_logic [library]
iS4H_properties [library]
iS4_topol_export [library]
iS4_GG_translation [library]
iS4_topol_sem [library]
iS4_completeness [library]
iS4_Lindenbaum_lem [library]
iS4_enum [library]
iS4_soundness [library]
iS4_Syntax [library]
i_P_4 [lemma, in iS4_GG_translation]
i_P_T [lemma, in iS4_GG_translation]
i_P_inter [lemma, in iS4_GG_translation]
i_P_unit [lemma, in iS4_GG_translation]
i_Empty [lemma, in iS4_GG_translation]
i_C [lemma, in iS4_GG_translation]
i_B [lemma, in iS4_GG_translation]
i_BC [lemma, in iS4_GG_translation]
i_AB [lemma, in iS4_GG_translation]
i_ABC [lemma, in iS4_GG_translation]
i_P [definition, in iS4_GG_translation]
i_subset_uset_mon [lemma, in Topology.iS4_topol_sem]
i_id_uset_preserv [lemma, in Topology.iS4_topol_sem]
i_4 [projection, in Topology.iS4_topol_sem]
i_T [projection, in Topology.iS4_topol_sem]
i_inter [projection, in Topology.iS4_topol_sem]
i_unit [projection, in Topology.iS4_topol_sem]
K
K_finite_intersection [lemma, in Topology.iS4_completeness]K_BoxOne_rule [lemma, in GHC.iS4H_properties]
K_rule [lemma, in GHC.iS4H_properties]
K_list_Imp [lemma, in GHC.iS4H_properties]
L
LEM [axiom, in Topology.iS4_completeness]LEM_prime [lemma, in Topology.iS4_completeness]
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]
Lindenbaum [lemma, in GHC.iS4_Lindenbaum_lem]
Lindenbaum_world [lemma, in Topology.iS4_completeness]
Lindenbaum_lemma [section, in GHC.iS4_Lindenbaum_lem]
Lind_theory_extens [lemma, in GHC.iS4_Lindenbaum_lem]
Lind_theory [definition, in GHC.iS4_Lindenbaum_lem]
list_Imp [definition, in Syntax.iS4_Syntax]
list_nil_or_tail_singleton [lemma, in General.List_lemmasT]
list_insert1 [lemma, in General.List_lemmasT]
list_eq_singleT_nobrac [lemma, in General.List_lemmasT]
list_eq_singleT [lemma, in General.List_lemmasT]
list_eq_single [lemma, in General.List_lemmasT]
list_eq_nil [lemma, in General.List_lemmasT]
list_rearr23 [lemma, in General.List_lemmasT]
list_rearr22 [lemma, in General.List_lemmasT]
list_rearr21 [lemma, in General.List_lemmasT]
list_rearr20 [lemma, in General.List_lemmasT]
list_rearr19 [lemma, in General.List_lemmasT]
list_rearr18 [lemma, in General.List_lemmasT]
list_rearr17_R [lemma, in General.List_lemmasT]
list_rearr16_R [lemma, in General.List_lemmasT]
list_rearr16 [lemma, in General.List_lemmasT]
list_rearr16' [lemma, in General.List_lemmasT]
list_rearr15_R [lemma, in General.List_lemmasT]
list_rearr15 [lemma, in General.List_lemmasT]
list_rearr14 [lemma, in General.List_lemmasT]
list_rearr13 [lemma, in General.List_lemmasT]
list_rearr11 [lemma, in General.List_lemmasT]
list_rearr10 [lemma, in General.List_lemmasT]
list_rearr9 [lemma, in General.List_lemmasT]
list_rearr8 [lemma, in General.List_lemmasT]
list_rearr7 [lemma, in General.List_lemmasT]
list_rearr6 [lemma, in General.List_lemmasT]
list_rearr5 [lemma, in General.List_lemmasT]
list_rearr4 [lemma, in General.List_lemmasT]
list_rearr2 [lemma, in General.List_lemmasT]
list_rearr1 [lemma, in General.List_lemmasT]
List_lemmasT [library]
loc_conseq [definition, in Topology.iS4_topol_sem]
L_ded2 [lemma, in GHC.iS4_enum]
L_ded1 [lemma, in GHC.iS4_enum]
L_ded_cumulative [lemma, in GHC.iS4_enum]
L_ded [definition, in GHC.iS4_enum]
L_enum_exhaustive [lemma, in GHC.iS4_enum]
L_enum_cumulative [lemma, in GHC.iS4_enum]
L_enum [definition, in GHC.iS4_enum]
M
M [instance, in iS4_GG_translation]MAK [definition, in GHC.iS4H]
MAK_I [constructor, in GHC.iS4H]
map_double_BoxOne [lemma, in Syntax.iS4_Syntax]
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]
MAT [definition, in GHC.iS4H]
MAT_I [constructor, in GHC.iS4H]
MAxioms [inductive, in GHC.iS4H]
MAxioms_sind [definition, in GHC.iS4H]
MAxioms_ind [definition, in GHC.iS4H]
MA4 [definition, in GHC.iS4H]
MA4_I [constructor, in GHC.iS4H]
mforces [definition, in Topology.iS4_topol_sem]
model [record, in Topology.iS4_topol_sem]
monotL_Or [lemma, in GHC.iS4H_properties]
monotR_Or [lemma, in GHC.iS4H_properties]
monot_Or2 [lemma, in GHC.iS4H_properties]
MP [constructor, in GHC.iS4H]
MPRule [inductive, in GHC.iS4H]
MPRule_sind [definition, in GHC.iS4H]
MPRule_ind [definition, in GHC.iS4H]
MPRule_I [constructor, in GHC.iS4H]
N
Nec [constructor, in GHC.iS4H]NecRule [inductive, in GHC.iS4H]
NecRule_sind [definition, in GHC.iS4H]
NecRule_ind [definition, in GHC.iS4H]
NecRule_I [constructor, in GHC.iS4H]
Neg [definition, in Syntax.iS4_Syntax]
nil_eq_appT [definition, in General.List_lemmasT]
nil_eq_app [definition, in General.List_lemmasT]
nil_eq_list [definition, in General.List_lemmasT]
nLind_theory_extens_le [lemma, in GHC.iS4_Lindenbaum_lem]
nLind_theory_extens [lemma, in GHC.iS4_Lindenbaum_lem]
nLind_theory [definition, in GHC.iS4_Lindenbaum_lem]
nnn_app_eq [lemma, in General.List_lemmasT]
nodes [projection, in Topology.iS4_topol_sem]
NoDup_remove [lemma, in GHC.iS4H_properties]
non_empty [definition, in General.List_lemmasT]
not_In_Lind_theory_deriv [lemma, in GHC.iS4_Lindenbaum_lem]
O
Or [constructor, in Syntax.iS4_Syntax]or_false [lemma, in General.gen]
P
P [instance, in iS4_GG_translation]pair_eqI [lemma, in General.gen]
partition_singleton_app [lemma, in General.List_lemmasT]
partition_2_3 [lemma, in General.List_lemmasT]
partition_3_2 [lemma, in General.List_lemmasT]
partition_2_2T [lemma, in General.List_lemmasT]
partition_2_2 [lemma, in General.List_lemmasT]
Persistence [lemma, in Topology.iS4_topol_sem]
PiffD1 [lemma, in General.gen]
PiffD2 [lemma, in General.gen]
pre [projection, in Topology.iS4_topol_sem]
preord_set [record, in Topology.iS4_topol_sem]
Prime [section, in GHC.iS4_Lindenbaum_lem]
prime [definition, in GHC.iS4_Lindenbaum_lem]
PrimeProps [section, in GHC.iS4_Lindenbaum_lem]
prod_nat_split [lemma, in General.genT]
prod_mono [lemma, in General.genT]
prv_Top [lemma, in GHC.iS4H_properties]
Q
QuasiCompleteness [lemma, in Topology.iS4_completeness]quasi_prime_Lind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
quasi_prime [definition, in GHC.iS4_Lindenbaum_lem]
R
rappl [lemma, in General.gen]reachable [projection, in Topology.iS4_topol_sem]
reach_tran [projection, in Topology.iS4_topol_sem]
reach_refl [projection, in Topology.iS4_topol_sem]
relationT [definition, in General.genT]
req [definition, in General.gen]
req_trans [lemma, in General.gen]
req_sym [lemma, in General.gen]
req_refl [lemma, in General.gen]
restr_closeder_Lind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
restr_closed [definition, in GHC.iS4_Lindenbaum_lem]
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]
S
Sets_of_forms [section, in GHC.iS4_Lindenbaum_lem]single_eq_listT_nobrac [definition, in General.List_lemmasT]
single_eq_listT [definition, in General.List_lemmasT]
single_eq_list [definition, in General.List_lemmasT]
Soundness [lemma, in Topology.iS4_soundness]
Strong_Completeness [lemma, in Topology.iS4_completeness]
subform [definition, in Syntax.iS4_Syntax]
subformlist [definition, in Syntax.iS4_Syntax]
subform_trans [lemma, in Syntax.iS4_Syntax]
subst [definition, in Syntax.iS4_Syntax]
subst_dep [lemma, in General.List_lemmasT]
subst_Ax [lemma, in GHC.iS4H_logic]
SubTheory [definition, in GHC.iS4_Lindenbaum_lem]
T
tail_inv_singleton2 [lemma, in General.List_lemmasT]tail_inv_singleton [lemma, in General.List_lemmasT]
Theories [definition, in Topology.iS4_completeness]
Theories_upset [lemma, in Topology.iS4_completeness]
Thm_irrel [lemma, in GHC.iS4H_properties]
Top [definition, in Syntax.iS4_Syntax]
TopologicalSemantics [section, in Topology.iS4_topol_sem]
transitiveT [definition, in General.genT]
true_and [lemma, in General.gen]
truthset_upset [instance, in Topology.iS4_topol_sem]
truthset_is_upset [lemma, in Topology.iS4_topol_sem]
truth_lemma [lemma, in Topology.iS4_completeness]
T_BoxOne [lemma, in GHC.iS4H_properties]
U
UnBox [definition, in Syntax.iS4_Syntax]UnBox_BoxOne [lemma, in Syntax.iS4_Syntax]
Under_Lind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
Under_nLind_theory [lemma, in GHC.iS4_Lindenbaum_lem]
unit_eq_appT2 [definition, in General.List_lemmasT]
unit_eq_app [definition, in General.List_lemmasT]
unit_upset [instance, in Topology.iS4_topol_sem]
unit_is_upset [lemma, in Topology.iS4_topol_sem]
upset [record, in Topology.iS4_topol_sem]
upset_prf_irrel [axiom, in Topology.iS4_topol_sem]
upTheories [instance, in Topology.iS4_completeness]
uset [projection, in Topology.iS4_topol_sem]
V
val [projection, in Topology.iS4_topol_sem]valid_form [definition, in Topology.iS4_topol_sem]
val_P [definition, in iS4_GG_translation]
Var [constructor, in Syntax.iS4_Syntax]
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]
wClosed [projection, in Topology.iS4_completeness]
well_foundedT [definition, in General.genT]
wInclClos [projection, in Topology.iS4_completeness]
wNotDer [projection, in Topology.iS4_completeness]
world [projection, in Topology.iS4_completeness]
wPrime [projection, in Topology.iS4_completeness]
other
¬ _ (My_scope) [notation, in Syntax.iS4_Syntax]⊥ (My_scope) [notation, in Syntax.iS4_Syntax]
_ ∧ _ (My_scope) [notation, in Syntax.iS4_Syntax]
_ ∨ _ (My_scope) [notation, in Syntax.iS4_Syntax]
_ --> _ (My_scope) [notation, in Syntax.iS4_Syntax]
# _ (My_scope) [notation, in Syntax.iS4_Syntax]
existsT2 _ .. _ , _ (type_scope) [notation, in General.existsT]
existsT _ .. _ , _ (type_scope) [notation, in General.existsT]
T~ _ [notation, in General.genT]
Notation Index
other
¬ _ (My_scope) [in Syntax.iS4_Syntax]⊥ (My_scope) [in Syntax.iS4_Syntax]
_ ∧ _ (My_scope) [in Syntax.iS4_Syntax]
_ ∨ _ (My_scope) [in Syntax.iS4_Syntax]
_ --> _ (My_scope) [in Syntax.iS4_Syntax]
# _ (My_scope) [in Syntax.iS4_Syntax]
existsT2 _ .. _ , _ (type_scope) [in General.existsT]
existsT _ .. _ , _ (type_scope) [in General.existsT]
T~ _ [in General.genT]
Library Index
E
existsTG
gengeneral_export
genT
I
iS4HiS4H_export
iS4H_logic
iS4H_properties
iS4_topol_export
iS4_GG_translation
iS4_topol_sem
iS4_completeness
iS4_Lindenbaum_lem
iS4_enum
iS4_soundness
iS4_Syntax
L
List_lemmasTLemma Index
A
ABCreach_trans [in iS4_GG_translation]ABCreach_refl [in iS4_GG_translation]
ABC_is_upset [in iS4_GG_translation]
absorp_Or1 [in GHC.iS4H_properties]
AB_is_upset [in iS4_GG_translation]
and_true [in General.gen]
And_Imp [in GHC.iS4H_properties]
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_eq_appT2_single_tlR [in General.List_lemmasT]
app_eq_appT2_single_tlL [in General.List_lemmasT]
app_eq_appT2_single_hdR [in General.List_lemmasT]
app_eq_appT2_single_hdL [in General.List_lemmasT]
app_eq_appT2_nn [in General.List_lemmasT]
app_tl_inversion [in General.List_lemmasT]
app_hd_inversion [in General.List_lemmasT]
app_singleton_tl_inversion [in General.List_lemmasT]
app_singleton_inversion [in General.List_lemmasT]
app_eq_unitT2 [in General.List_lemmasT]
app_eq_appT2 [in General.List_lemmasT]
app_eq_appT [in General.List_lemmasT]
app_eq_app [in General.List_lemmasT]
app_eq_nilT [in General.List_lemmasT]
app_cons_single [in General.List_lemmasT]
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]
asa_eq [in General.List_lemmasT]
Ax_valid [in Topology.iS4_soundness]
B
BC_is_upset [in iS4_GG_translation]BoxOne_UnBox_fixpoint [in Syntax.iS4_Syntax]
Box_UnBox_BoxOne_id [in Syntax.iS4_Syntax]
Box_distrib_list_Imp [in GHC.iS4H_properties]
B_is_upset [in iS4_GG_translation]
C
canonical_form_upset_P [in iS4_GG_translation]Ci_4 [in Topology.iS4_completeness]
Ci_T [in Topology.iS4_completeness]
Ci_inter [in Topology.iS4_completeness]
Ci_unit [in Topology.iS4_completeness]
Ci_upset [in Topology.iS4_completeness]
comm_Or [in GHC.iS4H_properties]
comm_Or_obj [in GHC.iS4H_properties]
comm_And_obj [in GHC.iS4H_properties]
Consist_Lind_theory [in GHC.iS4_Lindenbaum_lem]
Consist_nLind_theory [in GHC.iS4_Lindenbaum_lem]
cons_singleton [in General.List_lemmasT]
cons_eq_appT2 [in General.List_lemmasT]
cons_eq_appT [in General.List_lemmasT]
cons_eq_app [in General.List_lemmasT]
cons_single [in General.List_lemmasT]
Contr_Bot [in GHC.iS4H_properties]
C_val_persist [in Topology.iS4_completeness]
C_R_trans [in Topology.iS4_completeness]
C_R_refl [in Topology.iS4_completeness]
C_is_upset [in iS4_GG_translation]
D
der_Lind_theory_nLind_theory [in GHC.iS4_Lindenbaum_lem]der_nLind_theory_mLind_theory_le [in GHC.iS4_Lindenbaum_lem]
DNE_Box_Bot [in iS4_GG_translation]
double_BoxOne [in Syntax.iS4_Syntax]
E
EFQ [in GHC.iS4H_properties]emptyT_any [in General.genT]
emptyT_any' [in General.genT]
empty_False [in General.genT]
empty_explosion [in General.genT]
Empty_is_upset [in iS4_GG_translation]
eq_S_F [in General.genT]
eq_dec_form [in Syntax.iS4_Syntax]
eq_app_canc2 [in General.List_lemmasT]
eq_app_canc1 [in General.List_lemmasT]
eq_TrueI [in General.gen]
Explosion [in GHC.iS4H_properties]
F
Failure [in iS4_GG_translation]False_empty [in General.genT]
false_or [in General.gen]
ForallT_Forall [in General.genT]
ForallT_Forall' [in General.genT]
ForallT_forall [in General.genT]
ForallT_impl [in General.genT]
ForallT_map_rev [in General.genT]
ForallT_map [in General.genT]
ForallT_map_2 [in General.genT]
ForallT_2 [in General.genT]
ForallT_append [in General.genT]
ForallT_cons_iff [in General.genT]
ForallT_single [in General.genT]
ForallT_cons_inv [in General.genT]
ForallT_inv [in General.genT]
Forall_ForallT' [in General.genT]
Forall_ForallT [in General.genT]
Forall_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]
force_truthset [in Topology.iS4_topol_sem]
force_Box_interior_truthset [in Topology.iS4_topol_sem]
form_enum_ded_spec [in GHC.iS4_enum]
form_index_inj [in GHC.iS4_enum]
form_enum_index [in GHC.iS4_enum]
form_enum_sur [in GHC.iS4_enum]
fun_cong [in General.gen]
G
gen_cong [in General.gen]I
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]
if_rev_eq [in General.List_lemmasT]
if_eq_rev_eq [in General.List_lemmasT]
Imp_list_Imp [in GHC.iS4H_properties]
Imp_And [in GHC.iS4H_properties]
Imp_trans [in GHC.iS4H_properties]
Imp_trans_help427 [in GHC.iS4H_properties]
Imp_trans_help410 [in GHC.iS4H_properties]
Imp_trans_help170 [in GHC.iS4H_properties]
Imp_trans_help54 [in GHC.iS4H_properties]
Imp_trans_help37 [in GHC.iS4H_properties]
Imp_trans_help35 [in GHC.iS4H_properties]
Imp_trans_help14 [in GHC.iS4H_properties]
Imp_trans_help9 [in GHC.iS4H_properties]
Imp_trans_help8 [in GHC.iS4H_properties]
Imp_trans_help7 [in GHC.iS4H_properties]
imp_Id_gen [in GHC.iS4H_properties]
incl_Lind_theory [in GHC.iS4_Lindenbaum_lem]
incl_nLind_theory [in GHC.iS4_Lindenbaum_lem]
Incl_ClosSubform_Clos [in Syntax.iS4_Syntax]
Incl_Set_ClosSubform [in Syntax.iS4_Syntax]
inhabited_anon [in General.genT]
inter_conj [in Topology.iS4_topol_sem]
inter_is_upset [in Topology.iS4_topol_sem]
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_or_app [in General.List_lemmasT]
InT_app_or [in General.List_lemmasT]
InT_singleton_mid [in General.List_lemmasT]
InT_mid [in General.List_lemmasT]
InT_pt_I [in General.List_lemmasT]
InT_remove [in GHC.iS4H_properties]
In_InT [in General.genT]
In_Clos_BoxOne [in Syntax.iS4_Syntax]
In_Clos_not_box [in Syntax.iS4_Syntax]
In_form_dec [in Syntax.iS4_Syntax]
in_single [in General.gen]
In_Box_list_In_list [in GHC.iS4H_properties]
In_list_In_Box_list [in GHC.iS4H_properties]
In_remove [in GHC.iS4H_properties]
iS4H_finite [in GHC.iS4H_logic]
iS4H_struct [in GHC.iS4H_logic]
iS4H_comp [in GHC.iS4H_logic]
iS4H_monot [in GHC.iS4H_logic]
iS4H_Imp_list_Detachment_Deduction_Theorem [in GHC.iS4H_properties]
iS4H_Deduction_Theorem [in GHC.iS4H_properties]
iS4H_Detachment_Theorem [in GHC.iS4H_properties]
i_P_4 [in iS4_GG_translation]
i_P_T [in iS4_GG_translation]
i_P_inter [in iS4_GG_translation]
i_P_unit [in iS4_GG_translation]
i_Empty [in iS4_GG_translation]
i_C [in iS4_GG_translation]
i_B [in iS4_GG_translation]
i_BC [in iS4_GG_translation]
i_AB [in iS4_GG_translation]
i_ABC [in iS4_GG_translation]
i_subset_uset_mon [in Topology.iS4_topol_sem]
i_id_uset_preserv [in Topology.iS4_topol_sem]
K
K_finite_intersection [in Topology.iS4_completeness]K_BoxOne_rule [in GHC.iS4H_properties]
K_rule [in GHC.iS4H_properties]
K_list_Imp [in GHC.iS4H_properties]
L
LEM_prime [in Topology.iS4_completeness]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]
Lindenbaum [in GHC.iS4_Lindenbaum_lem]
Lindenbaum_world [in Topology.iS4_completeness]
Lind_theory_extens [in GHC.iS4_Lindenbaum_lem]
list_nil_or_tail_singleton [in General.List_lemmasT]
list_insert1 [in General.List_lemmasT]
list_eq_singleT_nobrac [in General.List_lemmasT]
list_eq_singleT [in General.List_lemmasT]
list_eq_single [in General.List_lemmasT]
list_eq_nil [in General.List_lemmasT]
list_rearr23 [in General.List_lemmasT]
list_rearr22 [in General.List_lemmasT]
list_rearr21 [in General.List_lemmasT]
list_rearr20 [in General.List_lemmasT]
list_rearr19 [in General.List_lemmasT]
list_rearr18 [in General.List_lemmasT]
list_rearr17_R [in General.List_lemmasT]
list_rearr16_R [in General.List_lemmasT]
list_rearr16 [in General.List_lemmasT]
list_rearr16' [in General.List_lemmasT]
list_rearr15_R [in General.List_lemmasT]
list_rearr15 [in General.List_lemmasT]
list_rearr14 [in General.List_lemmasT]
list_rearr13 [in General.List_lemmasT]
list_rearr11 [in General.List_lemmasT]
list_rearr10 [in General.List_lemmasT]
list_rearr9 [in General.List_lemmasT]
list_rearr8 [in General.List_lemmasT]
list_rearr7 [in General.List_lemmasT]
list_rearr6 [in General.List_lemmasT]
list_rearr5 [in General.List_lemmasT]
list_rearr4 [in General.List_lemmasT]
list_rearr2 [in General.List_lemmasT]
list_rearr1 [in General.List_lemmasT]
L_ded2 [in GHC.iS4_enum]
L_ded1 [in GHC.iS4_enum]
L_ded_cumulative [in GHC.iS4_enum]
L_enum_exhaustive [in GHC.iS4_enum]
L_enum_cumulative [in GHC.iS4_enum]
M
map_double_BoxOne [in Syntax.iS4_Syntax]map_eq_nil [in General.gen]
map_app_ex [in General.gen]
map_cons_ex' [in General.gen]
map_cons_ex [in General.gen]
monotL_Or [in GHC.iS4H_properties]
monotR_Or [in GHC.iS4H_properties]
monot_Or2 [in GHC.iS4H_properties]
N
nLind_theory_extens_le [in GHC.iS4_Lindenbaum_lem]nLind_theory_extens [in GHC.iS4_Lindenbaum_lem]
nnn_app_eq [in General.List_lemmasT]
NoDup_remove [in GHC.iS4H_properties]
not_In_Lind_theory_deriv [in GHC.iS4_Lindenbaum_lem]
O
or_false [in General.gen]P
pair_eqI [in General.gen]partition_singleton_app [in General.List_lemmasT]
partition_2_3 [in General.List_lemmasT]
partition_3_2 [in General.List_lemmasT]
partition_2_2T [in General.List_lemmasT]
partition_2_2 [in General.List_lemmasT]
Persistence [in Topology.iS4_topol_sem]
PiffD1 [in General.gen]
PiffD2 [in General.gen]
prod_nat_split [in General.genT]
prod_mono [in General.genT]
prv_Top [in GHC.iS4H_properties]
Q
QuasiCompleteness [in Topology.iS4_completeness]quasi_prime_Lind_theory [in GHC.iS4_Lindenbaum_lem]
R
rappl [in General.gen]req_trans [in General.gen]
req_sym [in General.gen]
req_refl [in General.gen]
restr_closeder_Lind_theory [in GHC.iS4_Lindenbaum_lem]
rsub_emptyT [in General.genT]
rsub_id [in General.gen]
rsub_trans [in General.gen]
rsub_def [in General.gen]
S
Soundness [in Topology.iS4_soundness]Strong_Completeness [in Topology.iS4_completeness]
subform_trans [in Syntax.iS4_Syntax]
subst_dep [in General.List_lemmasT]
subst_Ax [in GHC.iS4H_logic]
T
tail_inv_singleton2 [in General.List_lemmasT]tail_inv_singleton [in General.List_lemmasT]
Theories_upset [in Topology.iS4_completeness]
Thm_irrel [in GHC.iS4H_properties]
true_and [in General.gen]
truthset_is_upset [in Topology.iS4_topol_sem]
truth_lemma [in Topology.iS4_completeness]
T_BoxOne [in GHC.iS4H_properties]
U
UnBox_BoxOne [in Syntax.iS4_Syntax]Under_Lind_theory [in GHC.iS4_Lindenbaum_lem]
Under_nLind_theory [in GHC.iS4_Lindenbaum_lem]
unit_is_upset [in Topology.iS4_topol_sem]
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]
Axiom Index
L
LEM [in Topology.iS4_completeness]U
upset_prf_irrel [in Topology.iS4_topol_sem]Constructor Index
A
A [in iS4_GG_translation]AccT_intro [in General.genT]
And [in Syntax.iS4_Syntax]
asa_appR [in General.List_lemmasT]
asa_appL [in General.List_lemmasT]
asa_single [in General.List_lemmasT]
Ax [in GHC.iS4H]
AxRule_I [in GHC.iS4H]
B
B [in iS4_GG_translation]Bot [in Syntax.iS4_Syntax]
Box [in Syntax.iS4_Syntax]
C
C [in iS4_GG_translation]F
ForallT_cons [in General.genT]ForallT_nil [in General.genT]
Forall2T_cons [in General.genT]
Forall2T_nil [in General.genT]
I
IA1_I [in GHC.iS4H]IA2_I [in GHC.iS4H]
IA3_I [in GHC.iS4H]
IA4_I [in GHC.iS4H]
IA5_I [in GHC.iS4H]
IA6_I [in GHC.iS4H]
IA7_I [in GHC.iS4H]
IA8_I [in GHC.iS4H]
IA9_I [in GHC.iS4H]
Id [in GHC.iS4H]
IdRule_I [in GHC.iS4H]
Imp [in Syntax.iS4_Syntax]
InT_cons [in General.genT]
InT_eq' [in General.genT]
InT_pt_tl [in General.List_lemmasT]
InT_pt_hd [in General.List_lemmasT]
L
leT_S [in General.genT]leT_n [in General.genT]
M
MAK_I [in GHC.iS4H]MAT_I [in GHC.iS4H]
MA4_I [in GHC.iS4H]
MP [in GHC.iS4H]
MPRule_I [in GHC.iS4H]
N
Nec [in GHC.iS4H]NecRule_I [in GHC.iS4H]
O
Or [in Syntax.iS4_Syntax]V
Var [in Syntax.iS4_Syntax]Projection Index
I
i [in Topology.iS4_topol_sem]is_upset [in Topology.iS4_topol_sem]
i_4 [in Topology.iS4_topol_sem]
i_T [in Topology.iS4_topol_sem]
i_inter [in Topology.iS4_topol_sem]
i_unit [in Topology.iS4_topol_sem]
N
nodes [in Topology.iS4_topol_sem]P
pre [in Topology.iS4_topol_sem]R
reachable [in Topology.iS4_topol_sem]reach_tran [in Topology.iS4_topol_sem]
reach_refl [in Topology.iS4_topol_sem]
U
uset [in Topology.iS4_topol_sem]V
val [in Topology.iS4_topol_sem]W
wClosed [in Topology.iS4_completeness]wInclClos [in Topology.iS4_completeness]
wNotDer [in Topology.iS4_completeness]
world [in Topology.iS4_completeness]
wPrime [in Topology.iS4_completeness]
Inductive Index
A
ABC [in iS4_GG_translation]AccT [in General.genT]
app_split_at [in General.List_lemmasT]
AxRule [in GHC.iS4H]
E
empty [in General.genT]emptyT [in General.genT]
empty_relT [in General.genT]
F
ForallT [in General.genT]Forall2T [in General.genT]
form [in Syntax.iS4_Syntax]
I
IAxioms [in GHC.iS4H]IdRule [in GHC.iS4H]
InT [in General.genT]
InT_pair_triple [in General.List_lemmasT]
iS4H_rules [in GHC.iS4H]
L
leT [in General.genT]M
MAxioms [in GHC.iS4H]MPRule [in GHC.iS4H]
N
NecRule [in GHC.iS4H]Instance Index
A
ABC_upset [in iS4_GG_translation]AB_upset [in iS4_GG_translation]
B
BC_upset [in iS4_GG_translation]B_upset [in iS4_GG_translation]
C
Ci [in Topology.iS4_completeness]CM [in Topology.iS4_completeness]
CPre [in Topology.iS4_completeness]
C_upset [in iS4_GG_translation]
E
Empty_upset [in iS4_GG_translation]I
inter_upset [in Topology.iS4_topol_sem]M
M [in iS4_GG_translation]P
P [in iS4_GG_translation]T
truthset_upset [in Topology.iS4_topol_sem]U
unit_upset [in Topology.iS4_topol_sem]upTheories [in Topology.iS4_completeness]
Section Index
C
Completeness [in Topology.iS4_completeness]F
Failure_of_GG [in iS4_GG_translation]L
Lindenbaum_lemma [in GHC.iS4_Lindenbaum_lem]P
Prime [in GHC.iS4_Lindenbaum_lem]PrimeProps [in GHC.iS4_Lindenbaum_lem]
S
Sets_of_forms [in GHC.iS4_Lindenbaum_lem]T
TopologicalSemantics [in Topology.iS4_topol_sem]Definition Index
A
ABCreach [in iS4_GG_translation]ABC_sind [in iS4_GG_translation]
ABC_rec [in iS4_GG_translation]
ABC_ind [in iS4_GG_translation]
ABC_rect [in iS4_GG_translation]
AccT_sind [in General.genT]
AccT_rec [in General.genT]
AccT_ind [in General.genT]
AccT_rect [in General.genT]
anon [in General.genT]
app_split_at_sind [in General.List_lemmasT]
app_split_at_rec [in General.List_lemmasT]
app_split_at_ind [in General.List_lemmasT]
app_split_at_rect [in General.List_lemmasT]
app_eq_consT [in General.List_lemmasT]
app_eq_consT2 [in General.List_lemmasT]
app_eq_cons [in General.List_lemmasT]
Axioms [in GHC.iS4H]
AxRule_sind [in GHC.iS4H]
AxRule_ind [in GHC.iS4H]
B
BoxOne [in Syntax.iS4_Syntax]Box_list [in Syntax.iS4_Syntax]
C
Canon_val [in Topology.iS4_completeness]Canon_rel [in Topology.iS4_completeness]
choice_code [in GHC.iS4_Lindenbaum_lem]
choice_form [in GHC.iS4_Lindenbaum_lem]
Ci_uset [in Topology.iS4_completeness]
Clos [in Syntax.iS4_Syntax]
ClosOneBox [in Syntax.iS4_Syntax]
ClosSubform [in Syntax.iS4_Syntax]
E
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]
eq_nnn_app [in General.List_lemmasT]
F
Finite_Intersection [in Topology.iS4_completeness]ForallTD_forall [in General.genT]
ForallTI_forall [in General.genT]
ForallT_2I [in General.genT]
ForallT_2I' [in General.genT]
ForallT_D2 [in General.genT]
ForallT_D1 [in General.genT]
ForallT_2D [in General.genT]
ForallT_appendI [in General.genT]
ForallT_appendI' [in General.genT]
ForallT_appendD2 [in General.genT]
ForallT_appendD1 [in General.genT]
ForallT_appendD [in General.genT]
ForallT_singleI [in General.genT]
ForallT_singleD [in General.genT]
ForallT_sind [in General.genT]
ForallT_rec [in General.genT]
ForallT_ind [in General.genT]
ForallT_rect [in General.genT]
Forall2T_sind [in General.genT]
Forall2T_rec [in General.genT]
Forall2T_ind [in General.genT]
Forall2T_rect [in General.genT]
forces [in Topology.iS4_topol_sem]
form_enum_ded [in GHC.iS4_enum]
form_index [in GHC.iS4_enum]
form_index' [in GHC.iS4_enum]
form_enum [in GHC.iS4_enum]
form_sind [in Syntax.iS4_Syntax]
form_rec [in Syntax.iS4_Syntax]
form_ind [in Syntax.iS4_Syntax]
form_rect [in Syntax.iS4_Syntax]
I
IAxioms_sind [in GHC.iS4H]IAxioms_ind [in GHC.iS4H]
IA1 [in GHC.iS4H]
IA2 [in GHC.iS4H]
IA3 [in GHC.iS4H]
IA4 [in GHC.iS4H]
IA5 [in GHC.iS4H]
IA6 [in GHC.iS4H]
IA7 [in GHC.iS4H]
IA8 [in GHC.iS4H]
IA9 [in GHC.iS4H]
IdRule_sind [in GHC.iS4H]
IdRule_ind [in GHC.iS4H]
iffT_D2 [in General.genT]
iffT_D1 [in General.genT]
iffT_sym [in General.genT]
Inf_Union [in Topology.iS4_completeness]
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]
InT_pair_triple_sind [in General.List_lemmasT]
InT_pair_triple_rec [in General.List_lemmasT]
InT_pair_triple_ind [in General.List_lemmasT]
InT_pair_triple_rect [in General.List_lemmasT]
iS4H_prv [in GHC.iS4H]
iS4H_rules_sind [in GHC.iS4H]
iS4H_rules_ind [in GHC.iS4H]
i_P [in iS4_GG_translation]
L
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]
Lind_theory [in GHC.iS4_Lindenbaum_lem]
list_Imp [in Syntax.iS4_Syntax]
loc_conseq [in Topology.iS4_topol_sem]
L_ded [in GHC.iS4_enum]
L_enum [in GHC.iS4_enum]
M
MAK [in GHC.iS4H]MAT [in GHC.iS4H]
MAxioms_sind [in GHC.iS4H]
MAxioms_ind [in GHC.iS4H]
MA4 [in GHC.iS4H]
mforces [in Topology.iS4_topol_sem]
MPRule_sind [in GHC.iS4H]
MPRule_ind [in GHC.iS4H]
N
NecRule_sind [in GHC.iS4H]NecRule_ind [in GHC.iS4H]
Neg [in Syntax.iS4_Syntax]
nil_eq_appT [in General.List_lemmasT]
nil_eq_app [in General.List_lemmasT]
nil_eq_list [in General.List_lemmasT]
nLind_theory [in GHC.iS4_Lindenbaum_lem]
non_empty [in General.List_lemmasT]
P
prime [in GHC.iS4_Lindenbaum_lem]Q
quasi_prime [in GHC.iS4_Lindenbaum_lem]R
relationT [in General.genT]req [in General.gen]
restr_closed [in GHC.iS4_Lindenbaum_lem]
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
single_eq_listT_nobrac [in General.List_lemmasT]single_eq_listT [in General.List_lemmasT]
single_eq_list [in General.List_lemmasT]
subform [in Syntax.iS4_Syntax]
subformlist [in Syntax.iS4_Syntax]
subst [in Syntax.iS4_Syntax]
SubTheory [in GHC.iS4_Lindenbaum_lem]
T
Theories [in Topology.iS4_completeness]Top [in Syntax.iS4_Syntax]
transitiveT [in General.genT]
U
UnBox [in Syntax.iS4_Syntax]unit_eq_appT2 [in General.List_lemmasT]
unit_eq_app [in General.List_lemmasT]
V
valid_form [in Topology.iS4_topol_sem]val_P [in iS4_GG_translation]
W
well_foundedT [in General.genT]Record Index
C
Canon_worlds [in Topology.iS4_completeness]M
model [in Topology.iS4_topol_sem]P
preord_set [in Topology.iS4_topol_sem]U
upset [in Topology.iS4_topol_sem]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (604 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 | (9 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 | (310 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) |
| 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 | (43 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 | (18 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 | (19 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 | (15 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 | (7 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 | (160 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) |