| 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 | (520 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 | (25 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 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 | (16 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 | (237 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 | (26 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 | (4 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 | (26 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 | (80 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 | (100 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
Global Index
A
app_Proper [instance, in InqLog.ListLib]assignment [definition, in InqLog.FO.Models]
B
Bot [constructor, in InqLog.FO.Syntax]C
Casari [definition, in InqLog.FO.Casari]Casari [library]
CasariAnt [definition, in InqLog.FO.Casari]
CasariImpl [definition, in InqLog.FO.Casari]
CasariSuc [definition, in InqLog.FO.Casari]
Casari_fails.not_support_valid_Casari_IES [lemma, in InqLog.FO.Casari]
Casari_fails.counter_state_contains_all_ltb [lemma, in InqLog.FO.Casari]
Casari_fails.counter_state_contains_all_odds [lemma, in InqLog.FO.Casari]
Casari_fails.counter_state [definition, in InqLog.FO.Casari]
Casari_fails.support_CasariAnt_IES [lemma, in InqLog.FO.Casari]
Casari_fails.support_CasariImpl_IES_other_direction [lemma, in InqLog.FO.Casari]
Casari_fails.support_CasariSuc_IES_other_direction [lemma, in InqLog.FO.Casari]
Casari_fails.support_CasariSuc_IES [lemma, in InqLog.FO.Casari]
Casari_fails.support_IES_even_other_direction [lemma, in InqLog.FO.Casari]
Casari_fails.support_IES_even [lemma, in InqLog.FO.Casari]
Casari_fails.support_IES_odd [lemma, in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_3 [lemma, in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_3_state [definition, in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_2 [lemma, in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_1 [lemma, in InqLog.FO.Casari]
Casari_fails.not_E_finitely_many_complement [lemma, in InqLog.FO.Casari]
Casari_fails.not_E_contains_all [lemma, in InqLog.FO.Casari]
Casari_fails.E_Proper_substate [instance, in InqLog.FO.Casari]
Casari_fails.E [definition, in InqLog.FO.Casari]
Casari_fails.infinitely_many_Proper_substate [instance, in InqLog.FO.Casari]
Casari_fails.not_infinitely_many_finitely_many [lemma, in InqLog.FO.Casari]
Casari_fails.infinitely_many_Proper [instance, in InqLog.FO.Casari]
Casari_fails.infinitely_many [definition, in InqLog.FO.Casari]
Casari_fails.successor_Proper [instance, in InqLog.FO.Casari]
Casari_fails.successor [definition, in InqLog.FO.Casari]
Casari_fails.substate_finitely_many [lemma, in InqLog.FO.Casari]
Casari_fails.finitely_many_Proper [instance, in InqLog.FO.Casari]
Casari_fails.finitely_many [definition, in InqLog.FO.Casari]
Casari_fails.is_border [definition, in InqLog.FO.Casari]
Casari_fails.not_contains_any_contains_all_complement [lemma, in InqLog.FO.Casari]
Casari_fails.contains_any_Proper_substate [instance, in InqLog.FO.Casari]
Casari_fails.contains_any_Proper [instance, in InqLog.FO.Casari]
Casari_fails.contains_any [definition, in InqLog.FO.Casari]
Casari_fails.substate_contains_all [lemma, in InqLog.FO.Casari]
Casari_fails.contains_all_Proper [instance, in InqLog.FO.Casari]
Casari_fails.contains_all [definition, in InqLog.FO.Casari]
boolpred:~ _ (form_scope) [notation, in InqLog.FO.Casari]
boolpred:_ || _ (form_scope) [notation, in InqLog.FO.Casari]
boolpred:_ && _ (form_scope) [notation, in InqLog.FO.Casari]
boolpred:_ _ .. _ (form_scope) [notation, in InqLog.FO.Casari]
boolpred:_ (form_scope) [notation, in InqLog.FO.Casari]
boolpred:( _ ) (form_scope) [notation, in InqLog.FO.Casari]
(? _ ?) (form_scope) [notation, in InqLog.FO.Casari]
Casari_fails.not_forall_exists_not [lemma, in InqLog.FO.Casari]
Casari_fails.not_exists_forall_not [lemma, in InqLog.FO.Casari]
Casari_fails.M [instance, in InqLog.FO.Casari]
Casari_fails.rel [definition, in InqLog.FO.Casari]
Casari_fails.highest_occ_free_var_IES [lemma, in InqLog.FO.Casari]
Casari_fails.IES [definition, in InqLog.FO.Casari]
Casari_fails [module, in InqLog.FO.Casari]
Casari_with_atoms.support_valid_Casari_Atomic [lemma, in InqLog.FO.Casari]
Casari_with_atoms.Atomic [definition, in InqLog.FO.Casari]
Casari_with_atoms [module, in InqLog.FO.Casari]
CD [definition, in InqLog.FO.CD]
CD [library]
classical [definition, in InqLog.FO.Syntax]
classical_variant_is_classical [lemma, in InqLog.FO.Syntax]
classical_variant [definition, in InqLog.FO.Syntax]
classical_hsubst [lemma, in InqLog.FO.Syntax]
classical_Iquest [lemma, in InqLog.FO.Syntax]
classical_Exists [lemma, in InqLog.FO.Syntax]
classical_Iff [lemma, in InqLog.FO.Syntax]
classical_Disj [lemma, in InqLog.FO.Syntax]
classical_Top [lemma, in InqLog.FO.Syntax]
classical_Neg [lemma, in InqLog.FO.Syntax]
classical_Iexists [lemma, in InqLog.FO.Syntax]
classical_Forall [lemma, in InqLog.FO.Syntax]
classical_Idisj [lemma, in InqLog.FO.Syntax]
classical_Conj [lemma, in InqLog.FO.Syntax]
classical_Impl [lemma, in InqLog.FO.Syntax]
classical_Bot [lemma, in InqLog.FO.Syntax]
classical_Pred [lemma, in InqLog.FO.Syntax]
classical_truth_conditional [lemma, in InqLog.FO.Truth]
complement [definition, in InqLog.FO.Models]
complement_involutive [lemma, in InqLog.FO.Models]
complement_Proper [instance, in InqLog.FO.Models]
complement_substate_complement_iff [lemma, in InqLog.FO.Models]
complement_Proper_substate [instance, in InqLog.FO.Models]
Conj [constructor, in InqLog.FO.Syntax]
consistent [definition, in InqLog.FO.Models]
consistent_singleton_I [lemma, in InqLog.FO.Models]
consistent_most_inconsistent_I [lemma, in InqLog.FO.Models]
consistent_Proper [instance, in InqLog.FO.Models]
consistent_Proper_substate [instance, in InqLog.FO.Models]
cons_Proper_InS_eq [instance, in InqLog.ListLib]
cons_Proper_InS_sublist [instance, in InqLog.ListLib]
cons_InS_sublist_E_tl [lemma, in InqLog.ListLib]
cons_InS_sublist_E_hd [lemma, in InqLog.ListLib]
cons_InS_sublist_I [lemma, in InqLog.ListLib]
contains [definition, in InqLog.FO.Models]
contains_unrestricted_state_iff [lemma, in InqLog.FO.Models]
contains_restricted_state_iff [lemma, in InqLog.FO.Models]
contains_mapping_state_iff [lemma, in InqLog.FO.Models]
contains_mapping_state_E [lemma, in InqLog.FO.Models]
contains_mapping_state_I [lemma, in InqLog.FO.Models]
contains_excluding_state_iff [lemma, in InqLog.FO.Models]
contains_complement_iff [lemma, in InqLog.FO.Models]
contains_singleton_refl [lemma, in InqLog.FO.Models]
contains_singleton_iff [lemma, in InqLog.FO.Models]
contains_most_inconsistent_I [lemma, in InqLog.FO.Models]
contains_empty_state_E [lemma, in InqLog.FO.Models]
contains_iff_contains_Morph [lemma, in InqLog.FO.Models]
contains_Morph [definition, in InqLog.FO.Models]
contains_Proper [instance, in InqLog.FO.Models]
contains_Proper_substate [instance, in InqLog.FO.Models]
contains_dec [lemma, in InqLog.FO.Models]
D
Disj [definition, in InqLog.FO.Syntax]DNE [definition, in InqLog.FO.DNE]
DNE [library]
E
empty_state_property [lemma, in InqLog.FO.Support]empty_state_substate_I [lemma, in InqLog.FO.Models]
empty_state [definition, in InqLog.FO.Models]
excluding_state_irrelevance [lemma, in InqLog.FO.Models]
excluding_state_substate_I [lemma, in InqLog.FO.Models]
excluding_state [definition, in InqLog.FO.Models]
Exists [definition, in InqLog.FO.Syntax]
ext_eq_Setoid [instance, in InqLog.SetoidLib]
ext_eq_Equiv [instance, in InqLog.SetoidLib]
ext_eq [definition, in InqLog.SetoidLib]
F
FAri [projection, in InqLog.FO.Signatures]FAri_enum_charac [projection, in InqLog.FO.Signatures]
FAri_enum [projection, in InqLog.FO.Signatures]
filter_InS_sublist_I [lemma, in InqLog.ListLib]
finite_choice [lemma, in InqLog.ListLib]
FInterpretation [projection, in InqLog.FO.Models]
FInterpretation_Proper_inner [projection, in InqLog.FO.Models]
FInterpretation_Proper_outer [projection, in InqLog.FO.Models]
Forall [constructor, in InqLog.FO.Syntax]
form [inductive, in InqLog.FO.Syntax]
form_EqDec [instance, in InqLog.FO.Syntax]
form_Setoid [instance, in InqLog.FO.Syntax]
form_eq_Equiv [instance, in InqLog.FO.Syntax]
form_eq [definition, in InqLog.FO.Syntax]
form_eq_Pred_Pred_EqDec [definition, in InqLog.FO.Syntax]
form_sind [definition, in InqLog.FO.Syntax]
form_rec [definition, in InqLog.FO.Syntax]
form_ind [definition, in InqLog.FO.Syntax]
form_rect [definition, in InqLog.FO.Syntax]
fst_Proper [instance, in InqLog.FO.Seq]
FSymb [projection, in InqLog.FO.Signatures]
FSymb_EqDec [projection, in InqLog.FO.Signatures]
Func [constructor, in InqLog.FO.Syntax]
G
GenericModels [library]H
highest_occ_free_var [definition, in InqLog.FO.Syntax]HSubstLemmas_form [instance, in InqLog.FO.Syntax]
hsubst_Pred' [lemma, in InqLog.FO.SingleBinaryPredicate]
hsubst_Pred' [lemma, in InqLog.FO.SingleUnaryPredicate]
hsubst_comp' [lemma, in InqLog.FO.Syntax]
hsubst_id' [lemma, in InqLog.FO.Syntax]
hsubst_Proper [instance, in InqLog.FO.Syntax]
HSubst_form [instance, in InqLog.FO.Syntax]
I
Idisj [constructor, in InqLog.FO.Syntax]Ids_form [instance, in InqLog.FO.Syntax]
Ids_term [instance, in InqLog.FO.Syntax]
id_hsubst' [lemma, in InqLog.FO.Syntax]
id_subst' [lemma, in InqLog.FO.Syntax]
Iexists [constructor, in InqLog.FO.Syntax]
Iff [definition, in InqLog.FO.Syntax]
Impl [constructor, in InqLog.FO.Syntax]
inbS [definition, in InqLog.ListLib]
Individual [projection, in InqLog.FO.Models]
Individual_EqDec [projection, in InqLog.FO.Models]
Individual_inh [projection, in InqLog.FO.Models]
InS [definition, in InqLog.ListLib]
InS_sublist_order_ind [definition, in InqLog.ListLib]
InS_sublist_order_wf [lemma, in InqLog.ListLib]
InS_sublist_order_Acc [lemma, in InqLog.ListLib]
InS_sublist_order [definition, in InqLog.ListLib]
InS_sublist_singleton_E [lemma, in InqLog.ListLib]
InS_eq_dec [instance, in InqLog.ListLib]
InS_eq_app_comm [lemma, in InqLog.ListLib]
InS_eq_cons_cons [lemma, in InqLog.ListLib]
InS_eq_nil [lemma, in InqLog.ListLib]
InS_eq_Setoid [instance, in InqLog.ListLib]
InS_eq_equiv [instance, in InqLog.ListLib]
InS_eq [definition, in InqLog.ListLib]
InS_sublist_dec [lemma, in InqLog.ListLib]
InS_sublist_cons_I [lemma, in InqLog.ListLib]
InS_sublist_nil_E [lemma, in InqLog.ListLib]
InS_sublist_PreOrder [instance, in InqLog.ListLib]
InS_sublist [definition, in InqLog.ListLib]
InS_dec [lemma, in InqLog.ListLib]
InS_iff_inbS [lemma, in InqLog.ListLib]
InS_iff_inbS_false [lemma, in InqLog.ListLib]
InS_iff_inbS_true [lemma, in InqLog.ListLib]
InS_reflect_inbS [lemma, in InqLog.ListLib]
InS_map_E [lemma, in InqLog.ListLib]
InS_map_I [lemma, in InqLog.ListLib]
InS_filter_E [lemma, in InqLog.ListLib]
InS_filter_I [lemma, in InqLog.ListLib]
InS_app_E [lemma, in InqLog.ListLib]
InS_app_I_2 [lemma, in InqLog.ListLib]
InS_app_I_1 [lemma, in InqLog.ListLib]
InS_cons_E [lemma, in InqLog.ListLib]
InS_cons_I_tl [lemma, in InqLog.ListLib]
InS_cons_I_hd [lemma, in InqLog.ListLib]
InS_nil_E [lemma, in InqLog.ListLib]
In_InS [lemma, in InqLog.ListLib]
Iquest [definition, in InqLog.FO.Syntax]
K
Kuroda [definition, in InqLog.FO.Kuroda]Kuroda [library]
L
label [definition, in InqLog.FO.Seq]lb_form_hsubst [definition, in InqLog.FO.Seq]
lb_form_Proper [instance, in InqLog.FO.Seq]
lb_form_EqDec [instance, in InqLog.FO.Seq]
lb_form_Setoid [instance, in InqLog.FO.Seq]
lb_form_eq_Equiv [instance, in InqLog.FO.Seq]
lb_form_eq_sind [definition, in InqLog.FO.Seq]
lb_form_eq_ind [definition, in InqLog.FO.Seq]
lb_form_eq_1 [constructor, in InqLog.FO.Seq]
lb_form_eq [inductive, in InqLog.FO.Seq]
lb_form [definition, in InqLog.FO.Seq]
length_order_filter [lemma, in InqLog.ListLib]
length_order_ind [definition, in InqLog.ListLib]
length_order_wf [lemma, in InqLog.ListLib]
length_order_Acc [lemma, in InqLog.ListLib]
length_order [definition, in InqLog.ListLib]
ListLib [library]
list_choose [lemma, in InqLog.ListLib]
locality [lemma, in InqLog.FO.Support]
M
mapping_state_nil_state_eq_empty_state [lemma, in InqLog.FO.Models]mapping_state_Proper [instance, in InqLog.FO.Models]
mapping_state_Proper_substate [instance, in InqLog.FO.Models]
mapping_state [definition, in InqLog.FO.Models]
map_Proper_InS_eq [instance, in InqLog.ListLib]
map_Proper_InS_sublist [instance, in InqLog.ListLib]
Model [record, in InqLog.FO.Models]
Models [library]
morph [projection, in InqLog.SetoidLib]
Morph [record, in InqLog.SetoidLib]
morph_Proper_outer [instance, in InqLog.SetoidLib]
Morph_Setoid [instance, in InqLog.SetoidLib]
Morph_eq_Equiv [instance, in InqLog.SetoidLib]
Morph_eq [definition, in InqLog.SetoidLib]
morph_Proper [projection, in InqLog.SetoidLib]
most_inconsistent_substate_E [lemma, in InqLog.FO.Models]
most_inconsistent [definition, in InqLog.FO.Models]
mult [definition, in InqLog.ListLib]
mult_app_E_2 [lemma, in InqLog.ListLib]
mult_app_E_1 [lemma, in InqLog.ListLib]
mult_app_I [lemma, in InqLog.ListLib]
mult_cons_E_tl [lemma, in InqLog.ListLib]
mult_cons_E_hd [lemma, in InqLog.ListLib]
mult_cons_I [lemma, in InqLog.ListLib]
mult_nil_I [lemma, in InqLog.ListLib]
mult_Proper_InS_eq [instance, in InqLog.ListLib]
N
Neg [definition, in InqLog.FO.Syntax]nequiv_decb_Morph_irreflexive [lemma, in InqLog.ListLib]
nequiv_decb_Morph [definition, in InqLog.ListLib]
nil_InS_sublist_I [lemma, in InqLog.ListLib]
not_contains_unrestricted_state_I_domain [lemma, in InqLog.FO.Models]
not_contains_excluding_state_iff [lemma, in InqLog.FO.Models]
not_contains_complement_iff [lemma, in InqLog.FO.Models]
not_contains_singleton_iff [lemma, in InqLog.FO.Models]
not_support_valid_DNE.not_support_valid_DNE [lemma, in InqLog.FO.DNE]
not_support_valid_DNE.DNE_counterex [lemma, in InqLog.FO.DNE]
not_support_valid_DNE.DNE_counterex_part_2 [lemma, in InqLog.FO.DNE]
not_support_valid_DNE.DNE_counterex_part_1 [lemma, in InqLog.FO.DNE]
not_support_valid_DNE [module, in InqLog.FO.DNE]
P
PAri [projection, in InqLog.FO.Signatures]PAri_enum_charac [projection, in InqLog.FO.Signatures]
PAri_enum [projection, in InqLog.FO.Signatures]
persistency [lemma, in InqLog.FO.Support]
persistency_support_some [lemma, in InqLog.FO.Support]
persistency_support_mult [lemma, in InqLog.FO.Support]
PInterpretation [projection, in InqLog.FO.Models]
PInterpretation_Proper_inner [projection, in InqLog.FO.Models]
PInterpretation_Proper_outer [projection, in InqLog.FO.Models]
pointed_assignment [definition, in InqLog.FO.Models]
Pred [constructor, in InqLog.FO.Syntax]
Pred' [definition, in InqLog.FO.SingleBinaryPredicate]
Pred' [definition, in InqLog.FO.SingleUnaryPredicate]
Prelude [library]
proj1_sig_Proper [instance, in InqLog.SetoidLib]
PSymb [projection, in InqLog.FO.Signatures]
PSymb_EqDec [projection, in InqLog.FO.Signatures]
R
referent [definition, in InqLog.FO.Support]referent_subst_var [lemma, in InqLog.FO.Support]
referent_subst [lemma, in InqLog.FO.Support]
referent_Proper [instance, in InqLog.FO.Support]
Rename_form [instance, in InqLog.FO.Syntax]
rename_subst' [lemma, in InqLog.FO.Syntax]
rename_Proper [instance, in InqLog.FO.Syntax]
Rename_term [instance, in InqLog.FO.Syntax]
repeater [definition, in InqLog.FO.Syntax]
repeater_up_ids [lemma, in InqLog.FO.Syntax]
restricted_referent [lemma, in InqLog.FO.Support]
restricted_state [definition, in InqLog.FO.Models]
restricted_Model [definition, in InqLog.FO.Models]
rigid [projection, in InqLog.FO.Signatures]
rigidity [projection, in InqLog.FO.Models]
rigidity_referent [lemma, in InqLog.FO.Support]
ruling_out [definition, in InqLog.FO.Support]
S
satisfaction [definition, in InqLog.FO.Seq]satisfaction_conseq_cut [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Iexists_l [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Iexists_r [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Forall_l [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Forall_r [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Idisj_l [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Idisj_r [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Conj_l [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Conj_r [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Impl_l [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Impl_r [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Pred_l [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Pred_r [lemma, in InqLog.FO.Seq]
satisfaction_conseq_Bot_l [lemma, in InqLog.FO.Seq]
satisfaction_conseq_id [lemma, in InqLog.FO.Seq]
satisfaction_conseq_empty [lemma, in InqLog.FO.Seq]
satisfaction_conseq [definition, in InqLog.FO.Seq]
satisfaction_some_hsubst_var [lemma, in InqLog.FO.Seq]
satisfaction_some_Proper [instance, in InqLog.FO.Seq]
satisfaction_some [definition, in InqLog.FO.Seq]
satisfaction_mult_hsubst_var [lemma, in InqLog.FO.Seq]
satisfaction_mult_Proper [instance, in InqLog.FO.Seq]
satisfaction_mult [definition, in InqLog.FO.Seq]
satisfaction_hsubst_var [lemma, in InqLog.FO.Seq]
satisfaction_hsubst [lemma, in InqLog.FO.Seq]
satisfaction_Proper [instance, in InqLog.FO.Seq]
scomp_up [lemma, in InqLog.FO.Syntax]
scons_Proper [instance, in InqLog.SetoidLib]
Seq [inductive, in InqLog.FO.Seq]
Seq [library]
Seq_Neg_l [lemma, in InqLog.FO.Seq]
Seq_Neg_r [lemma, in InqLog.FO.Seq]
Seq_mon [lemma, in InqLog.FO.Seq]
Seq_persistency [lemma, in InqLog.FO.Seq]
Seq_Proper [instance, in InqLog.FO.Seq]
Seq_weakening [lemma, in InqLog.FO.Seq]
Seq_sind [definition, in InqLog.FO.Seq]
Seq_ind [definition, in InqLog.FO.Seq]
Seq_cut [constructor, in InqLog.FO.Seq]
Seq_Iexists_l [constructor, in InqLog.FO.Seq]
Seq_Iexists_r [constructor, in InqLog.FO.Seq]
Seq_Forall_l [constructor, in InqLog.FO.Seq]
Seq_Forall_r [constructor, in InqLog.FO.Seq]
Seq_Idisj_l [constructor, in InqLog.FO.Seq]
Seq_Idisj_r [constructor, in InqLog.FO.Seq]
Seq_Conj_l [constructor, in InqLog.FO.Seq]
Seq_Conj_r [constructor, in InqLog.FO.Seq]
Seq_Impl_l [constructor, in InqLog.FO.Seq]
Seq_Impl_r [constructor, in InqLog.FO.Seq]
Seq_Pred_l [constructor, in InqLog.FO.Seq]
Seq_Pred_r [constructor, in InqLog.FO.Seq]
Seq_Bot_l [constructor, in InqLog.FO.Seq]
Seq_id [constructor, in InqLog.FO.Seq]
Seq_empty [constructor, in InqLog.FO.Seq]
Seq_Casari [lemma, in InqLog.FO.Casari]
Seq_CasariAnt_CasariSuc [lemma, in InqLog.FO.Casari]
Seq_CD [lemma, in InqLog.FO.CD]
Seq_Kuroda [lemma, in InqLog.FO.Kuroda]
SetoidLib [library]
signature [instance, in InqLog.FO.SingleBinaryPredicate]
signature [instance, in InqLog.FO.SingleUnaryPredicate]
Signature [record, in InqLog.FO.Signatures]
Signatures [library]
sig_eq_lifting [lemma, in InqLog.SetoidLib]
sig_EqDec [instance, in InqLog.SetoidLib]
sig_Setoid [instance, in InqLog.SetoidLib]
sig_eq_Equiv [instance, in InqLog.SetoidLib]
sig_eq [definition, in InqLog.SetoidLib]
SingleBinaryPredicate [library]
singleton [definition, in InqLog.FO.Models]
singleton_Proper [instance, in InqLog.FO.Models]
singleton_substate_iff [lemma, in InqLog.FO.Models]
SingleUnaryPredicate [library]
snd_Proper [instance, in InqLog.FO.Seq]
some [definition, in InqLog.ListLib]
some_app_E [lemma, in InqLog.ListLib]
some_app_I_2 [lemma, in InqLog.ListLib]
some_app_I_1 [lemma, in InqLog.ListLib]
some_cons_E [lemma, in InqLog.ListLib]
some_cons_I_tl [lemma, in InqLog.ListLib]
some_cons_I_hd [lemma, in InqLog.ListLib]
some_nil_E [lemma, in InqLog.ListLib]
some_Proper_InS_eq [instance, in InqLog.ListLib]
soundness [lemma, in InqLog.FO.Seq]
state [definition, in InqLog.FO.Models]
state_eq_restricted_state_unrestricted_state [lemma, in InqLog.FO.Models]
state_eq_empty_state_iff_not_consistent [lemma, in InqLog.FO.Models]
state_eq_iff_substate [lemma, in InqLog.FO.Models]
state_eq_iff_contains [lemma, in InqLog.FO.Models]
state_eq [definition, in InqLog.FO.Models]
substate [definition, in InqLog.FO.Models]
substate_mapping_state_E [lemma, in InqLog.FO.Models]
substate_singleton_E [lemma, in InqLog.FO.Models]
substate_most_inconsistent_I [lemma, in InqLog.FO.Models]
substate_empty_state_E [lemma, in InqLog.FO.Models]
substate_Proper [instance, in InqLog.FO.Models]
substate_contrapos [lemma, in InqLog.FO.Models]
substate_PreOrder [instance, in InqLog.FO.Models]
SubstHSubstComp_term_form [instance, in InqLog.FO.Syntax]
SubstLemmas_form [instance, in InqLog.FO.Syntax]
SubstLemmas_term [instance, in InqLog.FO.Syntax]
Subst_form [instance, in InqLog.FO.Syntax]
subst_comp' [lemma, in InqLog.FO.Syntax]
subst_id' [lemma, in InqLog.FO.Syntax]
subst_Proper [instance, in InqLog.FO.Syntax]
Subst_term [instance, in InqLog.FO.Syntax]
support [definition, in InqLog.FO.Support]
Support [library]
support_valid_Casari_bd [lemma, in InqLog.FO.Casari]
support_valid_CD [lemma, in InqLog.FO.CD]
support_valid [definition, in InqLog.FO.Support]
support_some_hsubst_var [lemma, in InqLog.FO.Support]
support_some [definition, in InqLog.FO.Support]
support_mult_hsubst_var [lemma, in InqLog.FO.Support]
support_mult [definition, in InqLog.FO.Support]
support_hsubst_var [lemma, in InqLog.FO.Support]
support_hsubst [lemma, in InqLog.FO.Support]
support_Iff [lemma, in InqLog.FO.Support]
support_Disj [lemma, in InqLog.FO.Support]
support_Top [lemma, in InqLog.FO.Support]
support_Neg [lemma, in InqLog.FO.Support]
support_Proper_substate [instance, in InqLog.FO.Support]
support_Morph [definition, in InqLog.FO.Support]
support_Proper [instance, in InqLog.FO.Support]
support_Iexists [lemma, in InqLog.FO.Support]
support_Forall [lemma, in InqLog.FO.Support]
support_Idisj [lemma, in InqLog.FO.Support]
support_Conj [lemma, in InqLog.FO.Support]
support_Impl [lemma, in InqLog.FO.Support]
support_Bot [lemma, in InqLog.FO.Support]
support_Pred [lemma, in InqLog.FO.Support]
support_valid_Kuroda [lemma, in InqLog.FO.Kuroda]
support_valid_DNE [lemma, in InqLog.FO.DNE]
support_valid_DNE_Pred [lemma, in InqLog.FO.DNE]
Syntax [library]
T
term [inductive, in InqLog.FO.Syntax]term_rigid_subst [lemma, in InqLog.FO.Syntax]
term_rigid_Proper [instance, in InqLog.FO.Syntax]
term_rigid [definition, in InqLog.FO.Syntax]
term_EqDec [instance, in InqLog.FO.Syntax]
term_Setoid [instance, in InqLog.FO.Syntax]
term_eq_Equiv [instance, in InqLog.FO.Syntax]
term_eq [definition, in InqLog.FO.Syntax]
term_eq_Func_Func_EqDec [definition, in InqLog.FO.Syntax]
term_sind [definition, in InqLog.FO.Syntax]
term_rec [definition, in InqLog.FO.Syntax]
term_ind [definition, in InqLog.FO.Syntax]
term_rect [definition, in InqLog.FO.Syntax]
Top [definition, in InqLog.FO.Syntax]
to_Morph_Proper [instance, in InqLog.SetoidLib]
to_Morph [definition, in InqLog.SetoidLib]
truth [definition, in InqLog.FO.Truth]
Truth [library]
truth_conditional_Casari [lemma, in InqLog.FO.Casari]
truth_conditional_Kuroda [lemma, in InqLog.FO.Kuroda]
truth_hsubst [lemma, in InqLog.FO.Truth]
truth_conditional_Exists [lemma, in InqLog.FO.Truth]
truth_conditional_Iff [lemma, in InqLog.FO.Truth]
truth_conditional_Disj [lemma, in InqLog.FO.Truth]
truth_conditional_Neg [lemma, in InqLog.FO.Truth]
truth_conditional_Forall [lemma, in InqLog.FO.Truth]
truth_conditional_Conj [lemma, in InqLog.FO.Truth]
truth_conditional_Impl [lemma, in InqLog.FO.Truth]
truth_conditional_Bot [lemma, in InqLog.FO.Truth]
truth_conditional_Pred [lemma, in InqLog.FO.Truth]
truth_conditional_other_direction [lemma, in InqLog.FO.Truth]
truth_conditional [definition, in InqLog.FO.Truth]
truth_some_support_some [lemma, in InqLog.FO.Truth]
truth_some [definition, in InqLog.FO.Truth]
truth_mult_support_mult [lemma, in InqLog.FO.Truth]
truth_mult [definition, in InqLog.FO.Truth]
truth_classical_variant [lemma, in InqLog.FO.Truth]
truth_Iquest [lemma, in InqLog.FO.Truth]
truth_Exists [lemma, in InqLog.FO.Truth]
truth_Iff [lemma, in InqLog.FO.Truth]
truth_Disj [lemma, in InqLog.FO.Truth]
truth_Top [lemma, in InqLog.FO.Truth]
truth_Neg [lemma, in InqLog.FO.Truth]
truth_Morph [definition, in InqLog.FO.Truth]
truth_Proper [instance, in InqLog.FO.Truth]
truth_Iexists [lemma, in InqLog.FO.Truth]
truth_Forall [lemma, in InqLog.FO.Truth]
truth_Idisj [lemma, in InqLog.FO.Truth]
truth_Conj [lemma, in InqLog.FO.Truth]
truth_Impl [lemma, in InqLog.FO.Truth]
truth_Bot [lemma, in InqLog.FO.Truth]
truth_Pred [lemma, in InqLog.FO.Truth]
truth_conditional_support_valid_DNE_iff [lemma, in InqLog.FO.DNE]
truth_valid_DNE [lemma, in InqLog.FO.DNE]
truth_conditional_DNE [lemma, in InqLog.FO.DNE]
two_Worlds_Model [definition, in InqLog.FO.GenericModels]
U
unnamed_helper_Support_24 [lemma, in InqLog.FO.Support]unnamed_helper_Syntax_3 [lemma, in InqLog.FO.Syntax]
unrestricted_substate [lemma, in InqLog.FO.Models]
unrestricted_state [definition, in InqLog.FO.Models]
up_Proper [instance, in InqLog.FO.Syntax]
V
Var [constructor, in InqLog.FO.Syntax]W
World [projection, in InqLog.FO.Models]World_Setoid_EqDec [projection, in InqLog.FO.Models]
World_Setoid [projection, in InqLog.FO.Models]
other
form:? _ (form_scope) [notation, in InqLog.FO.Syntax]form:exists _ (form_scope) [notation, in InqLog.FO.Syntax]
form:_ <-> _ (form_scope) [notation, in InqLog.FO.Syntax]
form:_ \/ _ (form_scope) [notation, in InqLog.FO.Syntax]
form:~ _ (form_scope) [notation, in InqLog.FO.Syntax]
form:iexists _ (form_scope) [notation, in InqLog.FO.Syntax]
form:forall _ (form_scope) [notation, in InqLog.FO.Syntax]
form:_ \\/ _ (form_scope) [notation, in InqLog.FO.Syntax]
form:_ /\ _ (form_scope) [notation, in InqLog.FO.Syntax]
form:_ -> _ (form_scope) [notation, in InqLog.FO.Syntax]
form:_ _ .. _ (form_scope) [notation, in InqLog.FO.Syntax]
form:_ (form_scope) [notation, in InqLog.FO.Syntax]
form:( _ ) (form_scope) [notation, in InqLog.FO.Syntax]
_ , _ _||_ _ (form_scope) [notation, in InqLog.FO.Support]
_ , _ , _ _||_ _ (form_scope) [notation, in InqLog.FO.Support]
_ , _ |= _ (form_scope) [notation, in InqLog.FO.Support]
_ , _ , _ |= _ (form_scope) [notation, in InqLog.FO.Support]
<{ _ }> (form_scope) [notation, in InqLog.FO.Syntax]
Notation Index
C
boolpred:~ _ (form_scope) [in InqLog.FO.Casari]boolpred:_ || _ (form_scope) [in InqLog.FO.Casari]
boolpred:_ && _ (form_scope) [in InqLog.FO.Casari]
boolpred:_ _ .. _ (form_scope) [in InqLog.FO.Casari]
boolpred:_ (form_scope) [in InqLog.FO.Casari]
boolpred:( _ ) (form_scope) [in InqLog.FO.Casari]
(? _ ?) (form_scope) [in InqLog.FO.Casari]
other
form:? _ (form_scope) [in InqLog.FO.Syntax]form:exists _ (form_scope) [in InqLog.FO.Syntax]
form:_ <-> _ (form_scope) [in InqLog.FO.Syntax]
form:_ \/ _ (form_scope) [in InqLog.FO.Syntax]
form:~ _ (form_scope) [in InqLog.FO.Syntax]
form:iexists _ (form_scope) [in InqLog.FO.Syntax]
form:forall _ (form_scope) [in InqLog.FO.Syntax]
form:_ \\/ _ (form_scope) [in InqLog.FO.Syntax]
form:_ /\ _ (form_scope) [in InqLog.FO.Syntax]
form:_ -> _ (form_scope) [in InqLog.FO.Syntax]
form:_ _ .. _ (form_scope) [in InqLog.FO.Syntax]
form:_ (form_scope) [in InqLog.FO.Syntax]
form:( _ ) (form_scope) [in InqLog.FO.Syntax]
_ , _ _||_ _ (form_scope) [in InqLog.FO.Support]
_ , _ , _ _||_ _ (form_scope) [in InqLog.FO.Support]
_ , _ |= _ (form_scope) [in InqLog.FO.Support]
_ , _ , _ |= _ (form_scope) [in InqLog.FO.Support]
<{ _ }> (form_scope) [in InqLog.FO.Syntax]
Module Index
C
Casari_fails [in InqLog.FO.Casari]Casari_with_atoms [in InqLog.FO.Casari]
N
not_support_valid_DNE [in InqLog.FO.DNE]Library Index
C
CasariCD
D
DNEG
GenericModelsK
KurodaL
ListLibM
ModelsP
PreludeS
SeqSetoidLib
Signatures
SingleBinaryPredicate
SingleUnaryPredicate
Support
Syntax
T
TruthLemma Index
C
Casari_fails.not_support_valid_Casari_IES [in InqLog.FO.Casari]Casari_fails.counter_state_contains_all_ltb [in InqLog.FO.Casari]
Casari_fails.counter_state_contains_all_odds [in InqLog.FO.Casari]
Casari_fails.support_CasariAnt_IES [in InqLog.FO.Casari]
Casari_fails.support_CasariImpl_IES_other_direction [in InqLog.FO.Casari]
Casari_fails.support_CasariSuc_IES_other_direction [in InqLog.FO.Casari]
Casari_fails.support_CasariSuc_IES [in InqLog.FO.Casari]
Casari_fails.support_IES_even_other_direction [in InqLog.FO.Casari]
Casari_fails.support_IES_even [in InqLog.FO.Casari]
Casari_fails.support_IES_odd [in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_3 [in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_2 [in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_1 [in InqLog.FO.Casari]
Casari_fails.not_E_finitely_many_complement [in InqLog.FO.Casari]
Casari_fails.not_E_contains_all [in InqLog.FO.Casari]
Casari_fails.not_infinitely_many_finitely_many [in InqLog.FO.Casari]
Casari_fails.substate_finitely_many [in InqLog.FO.Casari]
Casari_fails.not_contains_any_contains_all_complement [in InqLog.FO.Casari]
Casari_fails.substate_contains_all [in InqLog.FO.Casari]
Casari_fails.not_forall_exists_not [in InqLog.FO.Casari]
Casari_fails.not_exists_forall_not [in InqLog.FO.Casari]
Casari_fails.highest_occ_free_var_IES [in InqLog.FO.Casari]
Casari_with_atoms.support_valid_Casari_Atomic [in InqLog.FO.Casari]
classical_variant_is_classical [in InqLog.FO.Syntax]
classical_hsubst [in InqLog.FO.Syntax]
classical_Iquest [in InqLog.FO.Syntax]
classical_Exists [in InqLog.FO.Syntax]
classical_Iff [in InqLog.FO.Syntax]
classical_Disj [in InqLog.FO.Syntax]
classical_Top [in InqLog.FO.Syntax]
classical_Neg [in InqLog.FO.Syntax]
classical_Iexists [in InqLog.FO.Syntax]
classical_Forall [in InqLog.FO.Syntax]
classical_Idisj [in InqLog.FO.Syntax]
classical_Conj [in InqLog.FO.Syntax]
classical_Impl [in InqLog.FO.Syntax]
classical_Bot [in InqLog.FO.Syntax]
classical_Pred [in InqLog.FO.Syntax]
classical_truth_conditional [in InqLog.FO.Truth]
complement_involutive [in InqLog.FO.Models]
complement_substate_complement_iff [in InqLog.FO.Models]
consistent_singleton_I [in InqLog.FO.Models]
consistent_most_inconsistent_I [in InqLog.FO.Models]
cons_InS_sublist_E_tl [in InqLog.ListLib]
cons_InS_sublist_E_hd [in InqLog.ListLib]
cons_InS_sublist_I [in InqLog.ListLib]
contains_unrestricted_state_iff [in InqLog.FO.Models]
contains_restricted_state_iff [in InqLog.FO.Models]
contains_mapping_state_iff [in InqLog.FO.Models]
contains_mapping_state_E [in InqLog.FO.Models]
contains_mapping_state_I [in InqLog.FO.Models]
contains_excluding_state_iff [in InqLog.FO.Models]
contains_complement_iff [in InqLog.FO.Models]
contains_singleton_refl [in InqLog.FO.Models]
contains_singleton_iff [in InqLog.FO.Models]
contains_most_inconsistent_I [in InqLog.FO.Models]
contains_empty_state_E [in InqLog.FO.Models]
contains_iff_contains_Morph [in InqLog.FO.Models]
contains_dec [in InqLog.FO.Models]
E
empty_state_property [in InqLog.FO.Support]empty_state_substate_I [in InqLog.FO.Models]
excluding_state_irrelevance [in InqLog.FO.Models]
excluding_state_substate_I [in InqLog.FO.Models]
F
filter_InS_sublist_I [in InqLog.ListLib]finite_choice [in InqLog.ListLib]
H
hsubst_Pred' [in InqLog.FO.SingleBinaryPredicate]hsubst_Pred' [in InqLog.FO.SingleUnaryPredicate]
hsubst_comp' [in InqLog.FO.Syntax]
hsubst_id' [in InqLog.FO.Syntax]
I
id_hsubst' [in InqLog.FO.Syntax]id_subst' [in InqLog.FO.Syntax]
InS_sublist_order_wf [in InqLog.ListLib]
InS_sublist_order_Acc [in InqLog.ListLib]
InS_sublist_singleton_E [in InqLog.ListLib]
InS_eq_app_comm [in InqLog.ListLib]
InS_eq_cons_cons [in InqLog.ListLib]
InS_eq_nil [in InqLog.ListLib]
InS_sublist_dec [in InqLog.ListLib]
InS_sublist_cons_I [in InqLog.ListLib]
InS_sublist_nil_E [in InqLog.ListLib]
InS_dec [in InqLog.ListLib]
InS_iff_inbS [in InqLog.ListLib]
InS_iff_inbS_false [in InqLog.ListLib]
InS_iff_inbS_true [in InqLog.ListLib]
InS_reflect_inbS [in InqLog.ListLib]
InS_map_E [in InqLog.ListLib]
InS_map_I [in InqLog.ListLib]
InS_filter_E [in InqLog.ListLib]
InS_filter_I [in InqLog.ListLib]
InS_app_E [in InqLog.ListLib]
InS_app_I_2 [in InqLog.ListLib]
InS_app_I_1 [in InqLog.ListLib]
InS_cons_E [in InqLog.ListLib]
InS_cons_I_tl [in InqLog.ListLib]
InS_cons_I_hd [in InqLog.ListLib]
InS_nil_E [in InqLog.ListLib]
In_InS [in InqLog.ListLib]
L
length_order_filter [in InqLog.ListLib]length_order_wf [in InqLog.ListLib]
length_order_Acc [in InqLog.ListLib]
list_choose [in InqLog.ListLib]
locality [in InqLog.FO.Support]
M
mapping_state_nil_state_eq_empty_state [in InqLog.FO.Models]most_inconsistent_substate_E [in InqLog.FO.Models]
mult_app_E_2 [in InqLog.ListLib]
mult_app_E_1 [in InqLog.ListLib]
mult_app_I [in InqLog.ListLib]
mult_cons_E_tl [in InqLog.ListLib]
mult_cons_E_hd [in InqLog.ListLib]
mult_cons_I [in InqLog.ListLib]
mult_nil_I [in InqLog.ListLib]
N
nequiv_decb_Morph_irreflexive [in InqLog.ListLib]nil_InS_sublist_I [in InqLog.ListLib]
not_contains_unrestricted_state_I_domain [in InqLog.FO.Models]
not_contains_excluding_state_iff [in InqLog.FO.Models]
not_contains_complement_iff [in InqLog.FO.Models]
not_contains_singleton_iff [in InqLog.FO.Models]
not_support_valid_DNE.not_support_valid_DNE [in InqLog.FO.DNE]
not_support_valid_DNE.DNE_counterex [in InqLog.FO.DNE]
not_support_valid_DNE.DNE_counterex_part_2 [in InqLog.FO.DNE]
not_support_valid_DNE.DNE_counterex_part_1 [in InqLog.FO.DNE]
P
persistency [in InqLog.FO.Support]persistency_support_some [in InqLog.FO.Support]
persistency_support_mult [in InqLog.FO.Support]
R
referent_subst_var [in InqLog.FO.Support]referent_subst [in InqLog.FO.Support]
rename_subst' [in InqLog.FO.Syntax]
repeater_up_ids [in InqLog.FO.Syntax]
restricted_referent [in InqLog.FO.Support]
rigidity_referent [in InqLog.FO.Support]
S
satisfaction_conseq_cut [in InqLog.FO.Seq]satisfaction_conseq_Iexists_l [in InqLog.FO.Seq]
satisfaction_conseq_Iexists_r [in InqLog.FO.Seq]
satisfaction_conseq_Forall_l [in InqLog.FO.Seq]
satisfaction_conseq_Forall_r [in InqLog.FO.Seq]
satisfaction_conseq_Idisj_l [in InqLog.FO.Seq]
satisfaction_conseq_Idisj_r [in InqLog.FO.Seq]
satisfaction_conseq_Conj_l [in InqLog.FO.Seq]
satisfaction_conseq_Conj_r [in InqLog.FO.Seq]
satisfaction_conseq_Impl_l [in InqLog.FO.Seq]
satisfaction_conseq_Impl_r [in InqLog.FO.Seq]
satisfaction_conseq_Pred_l [in InqLog.FO.Seq]
satisfaction_conseq_Pred_r [in InqLog.FO.Seq]
satisfaction_conseq_Bot_l [in InqLog.FO.Seq]
satisfaction_conseq_id [in InqLog.FO.Seq]
satisfaction_conseq_empty [in InqLog.FO.Seq]
satisfaction_some_hsubst_var [in InqLog.FO.Seq]
satisfaction_mult_hsubst_var [in InqLog.FO.Seq]
satisfaction_hsubst_var [in InqLog.FO.Seq]
satisfaction_hsubst [in InqLog.FO.Seq]
scomp_up [in InqLog.FO.Syntax]
Seq_Neg_l [in InqLog.FO.Seq]
Seq_Neg_r [in InqLog.FO.Seq]
Seq_mon [in InqLog.FO.Seq]
Seq_persistency [in InqLog.FO.Seq]
Seq_weakening [in InqLog.FO.Seq]
Seq_Casari [in InqLog.FO.Casari]
Seq_CasariAnt_CasariSuc [in InqLog.FO.Casari]
Seq_CD [in InqLog.FO.CD]
Seq_Kuroda [in InqLog.FO.Kuroda]
sig_eq_lifting [in InqLog.SetoidLib]
singleton_substate_iff [in InqLog.FO.Models]
some_app_E [in InqLog.ListLib]
some_app_I_2 [in InqLog.ListLib]
some_app_I_1 [in InqLog.ListLib]
some_cons_E [in InqLog.ListLib]
some_cons_I_tl [in InqLog.ListLib]
some_cons_I_hd [in InqLog.ListLib]
some_nil_E [in InqLog.ListLib]
soundness [in InqLog.FO.Seq]
state_eq_restricted_state_unrestricted_state [in InqLog.FO.Models]
state_eq_empty_state_iff_not_consistent [in InqLog.FO.Models]
state_eq_iff_substate [in InqLog.FO.Models]
state_eq_iff_contains [in InqLog.FO.Models]
substate_mapping_state_E [in InqLog.FO.Models]
substate_singleton_E [in InqLog.FO.Models]
substate_most_inconsistent_I [in InqLog.FO.Models]
substate_empty_state_E [in InqLog.FO.Models]
substate_contrapos [in InqLog.FO.Models]
subst_comp' [in InqLog.FO.Syntax]
subst_id' [in InqLog.FO.Syntax]
support_valid_Casari_bd [in InqLog.FO.Casari]
support_valid_CD [in InqLog.FO.CD]
support_some_hsubst_var [in InqLog.FO.Support]
support_mult_hsubst_var [in InqLog.FO.Support]
support_hsubst_var [in InqLog.FO.Support]
support_hsubst [in InqLog.FO.Support]
support_Iff [in InqLog.FO.Support]
support_Disj [in InqLog.FO.Support]
support_Top [in InqLog.FO.Support]
support_Neg [in InqLog.FO.Support]
support_Iexists [in InqLog.FO.Support]
support_Forall [in InqLog.FO.Support]
support_Idisj [in InqLog.FO.Support]
support_Conj [in InqLog.FO.Support]
support_Impl [in InqLog.FO.Support]
support_Bot [in InqLog.FO.Support]
support_Pred [in InqLog.FO.Support]
support_valid_Kuroda [in InqLog.FO.Kuroda]
support_valid_DNE [in InqLog.FO.DNE]
support_valid_DNE_Pred [in InqLog.FO.DNE]
T
term_rigid_subst [in InqLog.FO.Syntax]truth_conditional_Casari [in InqLog.FO.Casari]
truth_conditional_Kuroda [in InqLog.FO.Kuroda]
truth_hsubst [in InqLog.FO.Truth]
truth_conditional_Exists [in InqLog.FO.Truth]
truth_conditional_Iff [in InqLog.FO.Truth]
truth_conditional_Disj [in InqLog.FO.Truth]
truth_conditional_Neg [in InqLog.FO.Truth]
truth_conditional_Forall [in InqLog.FO.Truth]
truth_conditional_Conj [in InqLog.FO.Truth]
truth_conditional_Impl [in InqLog.FO.Truth]
truth_conditional_Bot [in InqLog.FO.Truth]
truth_conditional_Pred [in InqLog.FO.Truth]
truth_conditional_other_direction [in InqLog.FO.Truth]
truth_some_support_some [in InqLog.FO.Truth]
truth_mult_support_mult [in InqLog.FO.Truth]
truth_classical_variant [in InqLog.FO.Truth]
truth_Iquest [in InqLog.FO.Truth]
truth_Exists [in InqLog.FO.Truth]
truth_Iff [in InqLog.FO.Truth]
truth_Disj [in InqLog.FO.Truth]
truth_Top [in InqLog.FO.Truth]
truth_Neg [in InqLog.FO.Truth]
truth_Iexists [in InqLog.FO.Truth]
truth_Forall [in InqLog.FO.Truth]
truth_Idisj [in InqLog.FO.Truth]
truth_Conj [in InqLog.FO.Truth]
truth_Impl [in InqLog.FO.Truth]
truth_Bot [in InqLog.FO.Truth]
truth_Pred [in InqLog.FO.Truth]
truth_conditional_support_valid_DNE_iff [in InqLog.FO.DNE]
truth_valid_DNE [in InqLog.FO.DNE]
truth_conditional_DNE [in InqLog.FO.DNE]
U
unnamed_helper_Support_24 [in InqLog.FO.Support]unnamed_helper_Syntax_3 [in InqLog.FO.Syntax]
unrestricted_substate [in InqLog.FO.Models]
Constructor Index
B
Bot [in InqLog.FO.Syntax]C
Conj [in InqLog.FO.Syntax]F
Forall [in InqLog.FO.Syntax]Func [in InqLog.FO.Syntax]
I
Idisj [in InqLog.FO.Syntax]Iexists [in InqLog.FO.Syntax]
Impl [in InqLog.FO.Syntax]
L
lb_form_eq_1 [in InqLog.FO.Seq]P
Pred [in InqLog.FO.Syntax]S
Seq_cut [in InqLog.FO.Seq]Seq_Iexists_l [in InqLog.FO.Seq]
Seq_Iexists_r [in InqLog.FO.Seq]
Seq_Forall_l [in InqLog.FO.Seq]
Seq_Forall_r [in InqLog.FO.Seq]
Seq_Idisj_l [in InqLog.FO.Seq]
Seq_Idisj_r [in InqLog.FO.Seq]
Seq_Conj_l [in InqLog.FO.Seq]
Seq_Conj_r [in InqLog.FO.Seq]
Seq_Impl_l [in InqLog.FO.Seq]
Seq_Impl_r [in InqLog.FO.Seq]
Seq_Pred_l [in InqLog.FO.Seq]
Seq_Pred_r [in InqLog.FO.Seq]
Seq_Bot_l [in InqLog.FO.Seq]
Seq_id [in InqLog.FO.Seq]
Seq_empty [in InqLog.FO.Seq]
V
Var [in InqLog.FO.Syntax]Inductive Index
F
form [in InqLog.FO.Syntax]L
lb_form_eq [in InqLog.FO.Seq]S
Seq [in InqLog.FO.Seq]T
term [in InqLog.FO.Syntax]Projection Index
F
FAri [in InqLog.FO.Signatures]FAri_enum_charac [in InqLog.FO.Signatures]
FAri_enum [in InqLog.FO.Signatures]
FInterpretation [in InqLog.FO.Models]
FInterpretation_Proper_inner [in InqLog.FO.Models]
FInterpretation_Proper_outer [in InqLog.FO.Models]
FSymb [in InqLog.FO.Signatures]
FSymb_EqDec [in InqLog.FO.Signatures]
I
Individual [in InqLog.FO.Models]Individual_EqDec [in InqLog.FO.Models]
Individual_inh [in InqLog.FO.Models]
M
morph [in InqLog.SetoidLib]morph_Proper [in InqLog.SetoidLib]
P
PAri [in InqLog.FO.Signatures]PAri_enum_charac [in InqLog.FO.Signatures]
PAri_enum [in InqLog.FO.Signatures]
PInterpretation [in InqLog.FO.Models]
PInterpretation_Proper_inner [in InqLog.FO.Models]
PInterpretation_Proper_outer [in InqLog.FO.Models]
PSymb [in InqLog.FO.Signatures]
PSymb_EqDec [in InqLog.FO.Signatures]
R
rigid [in InqLog.FO.Signatures]rigidity [in InqLog.FO.Models]
W
World [in InqLog.FO.Models]World_Setoid_EqDec [in InqLog.FO.Models]
World_Setoid [in InqLog.FO.Models]
Instance Index
A
app_Proper [in InqLog.ListLib]C
Casari_fails.E_Proper_substate [in InqLog.FO.Casari]Casari_fails.infinitely_many_Proper_substate [in InqLog.FO.Casari]
Casari_fails.infinitely_many_Proper [in InqLog.FO.Casari]
Casari_fails.successor_Proper [in InqLog.FO.Casari]
Casari_fails.finitely_many_Proper [in InqLog.FO.Casari]
Casari_fails.contains_any_Proper_substate [in InqLog.FO.Casari]
Casari_fails.contains_any_Proper [in InqLog.FO.Casari]
Casari_fails.contains_all_Proper [in InqLog.FO.Casari]
Casari_fails.M [in InqLog.FO.Casari]
complement_Proper [in InqLog.FO.Models]
complement_Proper_substate [in InqLog.FO.Models]
consistent_Proper [in InqLog.FO.Models]
consistent_Proper_substate [in InqLog.FO.Models]
cons_Proper_InS_eq [in InqLog.ListLib]
cons_Proper_InS_sublist [in InqLog.ListLib]
contains_Proper [in InqLog.FO.Models]
contains_Proper_substate [in InqLog.FO.Models]
E
ext_eq_Setoid [in InqLog.SetoidLib]ext_eq_Equiv [in InqLog.SetoidLib]
F
form_EqDec [in InqLog.FO.Syntax]form_Setoid [in InqLog.FO.Syntax]
form_eq_Equiv [in InqLog.FO.Syntax]
fst_Proper [in InqLog.FO.Seq]
H
HSubstLemmas_form [in InqLog.FO.Syntax]hsubst_Proper [in InqLog.FO.Syntax]
HSubst_form [in InqLog.FO.Syntax]
I
Ids_form [in InqLog.FO.Syntax]Ids_term [in InqLog.FO.Syntax]
InS_eq_dec [in InqLog.ListLib]
InS_eq_Setoid [in InqLog.ListLib]
InS_eq_equiv [in InqLog.ListLib]
InS_sublist_PreOrder [in InqLog.ListLib]
L
lb_form_Proper [in InqLog.FO.Seq]lb_form_EqDec [in InqLog.FO.Seq]
lb_form_Setoid [in InqLog.FO.Seq]
lb_form_eq_Equiv [in InqLog.FO.Seq]
M
mapping_state_Proper [in InqLog.FO.Models]mapping_state_Proper_substate [in InqLog.FO.Models]
map_Proper_InS_eq [in InqLog.ListLib]
map_Proper_InS_sublist [in InqLog.ListLib]
morph_Proper_outer [in InqLog.SetoidLib]
Morph_Setoid [in InqLog.SetoidLib]
Morph_eq_Equiv [in InqLog.SetoidLib]
mult_Proper_InS_eq [in InqLog.ListLib]
P
proj1_sig_Proper [in InqLog.SetoidLib]R
referent_Proper [in InqLog.FO.Support]Rename_form [in InqLog.FO.Syntax]
rename_Proper [in InqLog.FO.Syntax]
Rename_term [in InqLog.FO.Syntax]
S
satisfaction_some_Proper [in InqLog.FO.Seq]satisfaction_mult_Proper [in InqLog.FO.Seq]
satisfaction_Proper [in InqLog.FO.Seq]
scons_Proper [in InqLog.SetoidLib]
Seq_Proper [in InqLog.FO.Seq]
signature [in InqLog.FO.SingleBinaryPredicate]
signature [in InqLog.FO.SingleUnaryPredicate]
sig_EqDec [in InqLog.SetoidLib]
sig_Setoid [in InqLog.SetoidLib]
sig_eq_Equiv [in InqLog.SetoidLib]
singleton_Proper [in InqLog.FO.Models]
snd_Proper [in InqLog.FO.Seq]
some_Proper_InS_eq [in InqLog.ListLib]
substate_Proper [in InqLog.FO.Models]
substate_PreOrder [in InqLog.FO.Models]
SubstHSubstComp_term_form [in InqLog.FO.Syntax]
SubstLemmas_form [in InqLog.FO.Syntax]
SubstLemmas_term [in InqLog.FO.Syntax]
Subst_form [in InqLog.FO.Syntax]
subst_Proper [in InqLog.FO.Syntax]
Subst_term [in InqLog.FO.Syntax]
support_Proper_substate [in InqLog.FO.Support]
support_Proper [in InqLog.FO.Support]
T
term_rigid_Proper [in InqLog.FO.Syntax]term_EqDec [in InqLog.FO.Syntax]
term_Setoid [in InqLog.FO.Syntax]
term_eq_Equiv [in InqLog.FO.Syntax]
to_Morph_Proper [in InqLog.SetoidLib]
truth_Proper [in InqLog.FO.Truth]
U
up_Proper [in InqLog.FO.Syntax]Definition Index
A
assignment [in InqLog.FO.Models]C
Casari [in InqLog.FO.Casari]CasariAnt [in InqLog.FO.Casari]
CasariImpl [in InqLog.FO.Casari]
CasariSuc [in InqLog.FO.Casari]
Casari_fails.counter_state [in InqLog.FO.Casari]
Casari_fails.unnamed_helper_Casari_3_state [in InqLog.FO.Casari]
Casari_fails.E [in InqLog.FO.Casari]
Casari_fails.infinitely_many [in InqLog.FO.Casari]
Casari_fails.successor [in InqLog.FO.Casari]
Casari_fails.finitely_many [in InqLog.FO.Casari]
Casari_fails.is_border [in InqLog.FO.Casari]
Casari_fails.contains_any [in InqLog.FO.Casari]
Casari_fails.contains_all [in InqLog.FO.Casari]
Casari_fails.rel [in InqLog.FO.Casari]
Casari_fails.IES [in InqLog.FO.Casari]
Casari_with_atoms.Atomic [in InqLog.FO.Casari]
CD [in InqLog.FO.CD]
classical [in InqLog.FO.Syntax]
classical_variant [in InqLog.FO.Syntax]
complement [in InqLog.FO.Models]
consistent [in InqLog.FO.Models]
contains [in InqLog.FO.Models]
contains_Morph [in InqLog.FO.Models]
D
Disj [in InqLog.FO.Syntax]DNE [in InqLog.FO.DNE]
E
empty_state [in InqLog.FO.Models]excluding_state [in InqLog.FO.Models]
Exists [in InqLog.FO.Syntax]
ext_eq [in InqLog.SetoidLib]
F
form_eq [in InqLog.FO.Syntax]form_eq_Pred_Pred_EqDec [in InqLog.FO.Syntax]
form_sind [in InqLog.FO.Syntax]
form_rec [in InqLog.FO.Syntax]
form_ind [in InqLog.FO.Syntax]
form_rect [in InqLog.FO.Syntax]
H
highest_occ_free_var [in InqLog.FO.Syntax]I
Iff [in InqLog.FO.Syntax]inbS [in InqLog.ListLib]
InS [in InqLog.ListLib]
InS_sublist_order_ind [in InqLog.ListLib]
InS_sublist_order [in InqLog.ListLib]
InS_eq [in InqLog.ListLib]
InS_sublist [in InqLog.ListLib]
Iquest [in InqLog.FO.Syntax]
K
Kuroda [in InqLog.FO.Kuroda]L
label [in InqLog.FO.Seq]lb_form_hsubst [in InqLog.FO.Seq]
lb_form_eq_sind [in InqLog.FO.Seq]
lb_form_eq_ind [in InqLog.FO.Seq]
lb_form [in InqLog.FO.Seq]
length_order_ind [in InqLog.ListLib]
length_order [in InqLog.ListLib]
M
mapping_state [in InqLog.FO.Models]Morph_eq [in InqLog.SetoidLib]
most_inconsistent [in InqLog.FO.Models]
mult [in InqLog.ListLib]
N
Neg [in InqLog.FO.Syntax]nequiv_decb_Morph [in InqLog.ListLib]
P
pointed_assignment [in InqLog.FO.Models]Pred' [in InqLog.FO.SingleBinaryPredicate]
Pred' [in InqLog.FO.SingleUnaryPredicate]
R
referent [in InqLog.FO.Support]repeater [in InqLog.FO.Syntax]
restricted_state [in InqLog.FO.Models]
restricted_Model [in InqLog.FO.Models]
ruling_out [in InqLog.FO.Support]
S
satisfaction [in InqLog.FO.Seq]satisfaction_conseq [in InqLog.FO.Seq]
satisfaction_some [in InqLog.FO.Seq]
satisfaction_mult [in InqLog.FO.Seq]
Seq_sind [in InqLog.FO.Seq]
Seq_ind [in InqLog.FO.Seq]
sig_eq [in InqLog.SetoidLib]
singleton [in InqLog.FO.Models]
some [in InqLog.ListLib]
state [in InqLog.FO.Models]
state_eq [in InqLog.FO.Models]
substate [in InqLog.FO.Models]
support [in InqLog.FO.Support]
support_valid [in InqLog.FO.Support]
support_some [in InqLog.FO.Support]
support_mult [in InqLog.FO.Support]
support_Morph [in InqLog.FO.Support]
T
term_rigid [in InqLog.FO.Syntax]term_eq [in InqLog.FO.Syntax]
term_eq_Func_Func_EqDec [in InqLog.FO.Syntax]
term_sind [in InqLog.FO.Syntax]
term_rec [in InqLog.FO.Syntax]
term_ind [in InqLog.FO.Syntax]
term_rect [in InqLog.FO.Syntax]
Top [in InqLog.FO.Syntax]
to_Morph [in InqLog.SetoidLib]
truth [in InqLog.FO.Truth]
truth_conditional [in InqLog.FO.Truth]
truth_some [in InqLog.FO.Truth]
truth_mult [in InqLog.FO.Truth]
truth_Morph [in InqLog.FO.Truth]
two_Worlds_Model [in InqLog.FO.GenericModels]
U
unrestricted_state [in InqLog.FO.Models]Record Index
M
Model [in InqLog.FO.Models]Morph [in InqLog.SetoidLib]
S
Signature [in InqLog.FO.Signatures]| 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 | (520 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 | (25 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 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 | (16 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 | (237 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 | (26 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 | (4 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 | (26 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 | (80 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 | (100 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |