| 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 | (1509 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 | (138 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (119 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 | (23 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 | (499 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 | (171 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 | (1 entry) |
| 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 | (60 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 | (60 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 | (88 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 | (68 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (255 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 | (23 entries) |
Global Index
A
AAll [constructor, in Completeness.DialogFull]AAll [constructor, in Completeness.DialogFragment]
AAnd [constructor, in Completeness.DialogFull]
ABot [constructor, in Completeness.DialogFull]
ABot [constructor, in Completeness.DialogFragment]
Absurd [constructor, in Completeness.Gentzen]
AExt [constructor, in Completeness.DialogFull]
AImpl [constructor, in Completeness.DialogFull]
AImpl [constructor, in Completeness.DialogFragment]
AL [constructor, in Completeness.FullSequent]
All [constructor, in Completeness.Syntax]
All [constructor, in Completeness.FullSyntax]
AllE [constructor, in Completeness.ND]
AllI [constructor, in Completeness.ND]
AllL [constructor, in Completeness.Gentzen]
AllL [constructor, in Completeness.FullSequent]
AllR [constructor, in Completeness.Gentzen]
AllR [constructor, in Completeness.FullSequent]
and_dec [instance, in Completeness.Prelim]
any_T_map_closed [lemma, in Completeness.Stability]
any_T [definition, in Completeness.Stability]
AOr [constructor, in Completeness.DialogFull]
ap [definition, in Completeness.unscoped]
apc [definition, in Completeness.unscoped]
app_equi_proper [instance, in Completeness.Prelim]
app_incl_proper [instance, in Completeness.Prelim]
app_incl_R [lemma, in Completeness.Prelim]
app_incl_l [lemma, in Completeness.Prelim]
AR [constructor, in Completeness.FullSequent]
atomic [projection, in Completeness.Sorensen]
atomic [projection, in Completeness.SDialogues]
atomic_dec [lemma, in Completeness.DialogFull]
atomic_form [definition, in Completeness.DialogFull]
atomic_dec [lemma, in Completeness.DialogFragment]
atomic_form [definition, in Completeness.DialogFragment]
Att [constructor, in Completeness.Sorensen]
Att [constructor, in Completeness.SDialogues]
attack [projection, in Completeness.Sorensen]
attack [projection, in Completeness.SDialogues]
attack_form_inv_ext [lemma, in Completeness.DialogFull]
attack_form_inv_all [lemma, in Completeness.DialogFull]
attack_form_inv_or [lemma, in Completeness.DialogFull]
attack_form_inv_and [lemma, in Completeness.DialogFull]
attack_form_inv_impl [lemma, in Completeness.DialogFull]
attack_form [inductive, in Completeness.DialogFull]
attack_form_inv_all [lemma, in Completeness.DialogFragment]
attack_form_inv_impl [lemma, in Completeness.DialogFragment]
attack_form [inductive, in Completeness.DialogFragment]
at_pos [definition, in Completeness.Enumeration]
Ax [constructor, in Completeness.Gentzen]
Ax [constructor, in Completeness.FullSequent]
axioms [library]
AXM [lemma, in Completeness.ND]
B
big_imp_extract [lemma, in Completeness.ND]big_imp [definition, in Completeness.FOL]
big_imp_valid_L [lemma, in Completeness.GenTarski]
big_or [definition, in Completeness.FullSequent]
BLM [definition, in Completeness.GenTarski]
BL_E_subsumption [lemma, in Completeness.GenTarski]
bool_eq_dec [instance, in Completeness.Prelim]
bool_dec [instance, in Completeness.Prelim]
bool_Prop_false [lemma, in Completeness.Prelim]
bool_Prop_true [lemma, in Completeness.Prelim]
bottom [inductive, in Completeness.ND]
B_S [constructor, in Completeness.Syntax]
B_I [constructor, in Completeness.GenTarski]
C
C [constructor, in Completeness.Sorensen]C [constructor, in Completeness.SDialogues]
capture [definition, in Completeness.FOL]
capture_extract [lemma, in Completeness.ND]
capture_subs [definition, in Completeness.ND]
capture_captures [lemma, in Completeness.FOL]
cend_dn [lemma, in Completeness.KripkeCompleteness]
cfind [lemma, in Completeness.Prelim]
challenge [inductive, in Completeness.Sorensen]
challenge [inductive, in Completeness.SDialogues]
class [constructor, in Completeness.ND]
classical [definition, in Completeness.GenTarski]
close [definition, in Completeness.FOL]
closed [definition, in Completeness.FOL]
closed [definition, in Completeness.FullFOL]
closed_T_extend [lemma, in Completeness.FOL]
closed_T [definition, in Completeness.FOL]
closed_T_extend [lemma, in Completeness.FullFOL]
closed_T [definition, in Completeness.FullFOL]
close_extract [lemma, in Completeness.ND]
close_closed [lemma, in Completeness.FOL]
close_valid_L [lemma, in Completeness.GenTarski]
ClosingBigImp [section, in Completeness.GenTarski]
ClosingValidity [section, in Completeness.GenTarski]
ClosingValidity.C [variable, in Completeness.GenTarski]
ClosingValidity.HC [variable, in Completeness.GenTarski]
ClosingValidity.Hprv [variable, in Completeness.GenTarski]
ClosingValidity.phi [variable, in Completeness.GenTarski]
ClosingValidity.T [variable, in Completeness.GenTarski]
cod [definition, in Completeness.axioms]
cod_comp [definition, in Completeness.axioms]
cod_ext' [definition, in Completeness.axioms]
cod_ext [definition, in Completeness.axioms]
cod_id [definition, in Completeness.axioms]
cod_map [definition, in Completeness.axioms]
compComp_form [lemma, in Completeness.Syntax]
compComp_term [lemma, in Completeness.Syntax]
compComp_form [lemma, in Completeness.FullSyntax]
compComp_term [lemma, in Completeness.FullSyntax]
compComp'_form [lemma, in Completeness.Syntax]
compComp'_term [lemma, in Completeness.Syntax]
compComp'_form [lemma, in Completeness.FullSyntax]
compComp'_term [lemma, in Completeness.FullSyntax]
compl [definition, in Completeness.DecidableEnumerable]
Completeness [section, in Completeness.GenCompleteness]
completeness_expl [lemma, in Completeness.GenCompleteness]
completeness_standard_stability [lemma, in Completeness.GenCompleteness]
Completeness.BotModel [section, in Completeness.GenCompleteness]
Completeness.BotModel.T [variable, in Completeness.GenCompleteness]
Completeness.BotModel.T_closed [variable, in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes [section, in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.Hphi [variable, in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.HT [variable, in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.phi [variable, in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.T [variable, in Completeness.GenCompleteness]
Completeness.FragmentCompleteness [section, in Completeness.GenCompleteness]
Completeness.FragmentModel [section, in Completeness.GenCompleteness]
Completeness.FragmentModel.GBot [variable, in Completeness.GenCompleteness]
Completeness.FragmentModel.GBot_closed [variable, in Completeness.GenCompleteness]
Completeness.FragmentModel.T [variable, in Completeness.GenCompleteness]
Completeness.FragmentModel.T_closed [variable, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness [section, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.He [variable, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.Hphi [variable, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.HT [variable, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.L [variable, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.mp [variable, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.phi [variable, in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.T [variable, in Completeness.GenCompleteness]
Completeness.StandardCompletenes [section, in Completeness.GenCompleteness]
Completeness.StandardCompletenes.Hphi [variable, in Completeness.GenCompleteness]
Completeness.StandardCompletenes.HT [variable, in Completeness.GenCompleteness]
Completeness.StandardCompletenes.phi [variable, in Completeness.GenCompleteness]
Completeness.StandardCompletenes.T [variable, in Completeness.GenCompleteness]
Composition [section, in Completeness.GenConstructions]
compSubstSubst_form [definition, in Completeness.Syntax]
compSubstSubst_term [definition, in Completeness.Syntax]
compSubstSubst_form [definition, in Completeness.FullSyntax]
compSubstSubst_term [definition, in Completeness.FullSyntax]
congr_All [definition, in Completeness.Syntax]
congr_Impl [definition, in Completeness.Syntax]
congr_Pred [definition, in Completeness.Syntax]
congr_Fal [definition, in Completeness.Syntax]
congr_Func [definition, in Completeness.Syntax]
congr_Ex [definition, in Completeness.FullSyntax]
congr_All [definition, in Completeness.FullSyntax]
congr_Disj [definition, in Completeness.FullSyntax]
congr_Conj [definition, in Completeness.FullSyntax]
congr_Impl [definition, in Completeness.FullSyntax]
congr_Pred [definition, in Completeness.FullSyntax]
congr_Top [definition, in Completeness.FullSyntax]
congr_Fal [definition, in Completeness.FullSyntax]
congr_Func [definition, in Completeness.FullSyntax]
Conj [constructor, in Completeness.FullSyntax]
cons [definition, in Completeness.KripkeCompleteness]
Consistency [lemma, in Completeness.GenTarski]
Consistency [section, in Completeness.Consistency]
Consistency [library]
consistency_inheritance [lemma, in Completeness.Consistency]
Consistency.Classical [section, in Completeness.Consistency]
Consistency.Classical.XM [variable, in Completeness.Consistency]
consistent [definition, in Completeness.Consistency]
consistent_join_step [lemma, in Completeness.GenConstructions]
consistent_max_out2 [lemma, in Completeness.Consistency]
consistent_max_impl [lemma, in Completeness.Consistency]
consistent_max_out [lemma, in Completeness.Consistency]
consistent_neg2 [lemma, in Completeness.Consistency]
consistent_neg [lemma, in Completeness.Consistency]
consistent_prv [lemma, in Completeness.Consistency]
consistent_max [definition, in Completeness.Consistency]
constraint [definition, in Completeness.GenTarski]
ConstructionInputs [record, in Completeness.GenConstructions]
ConstructionOutputs [record, in Completeness.GenConstructions]
construct_construction [lemma, in Completeness.GenConstructions]
cons_ctx [definition, in Completeness.KripkeCompleteness]
cons_equi_proper [instance, in Completeness.Prelim]
cons_incl_proper [instance, in Completeness.Prelim]
cons_incl [lemma, in Completeness.Prelim]
contains [definition, in Completeness.FOL]
contains [definition, in Completeness.FullFOL]
contains_extend3 [lemma, in Completeness.FOL]
contains_extend2 [lemma, in Completeness.FOL]
contains_extend1 [lemma, in Completeness.FOL]
contains_app [lemma, in Completeness.FOL]
contains_cons2 [lemma, in Completeness.FOL]
contains_cons [lemma, in Completeness.FOL]
contains_nil [lemma, in Completeness.FOL]
contains_L [definition, in Completeness.FOL]
contains_extend3 [lemma, in Completeness.FullFOL]
contains_extend2 [lemma, in Completeness.FullFOL]
contains_extend1 [lemma, in Completeness.FullFOL]
contains_app [lemma, in Completeness.FullFOL]
contains_cons2 [lemma, in Completeness.FullFOL]
contains_cons [lemma, in Completeness.FullFOL]
contains_nil [lemma, in Completeness.FullFOL]
contains_L [definition, in Completeness.FullFOL]
context_shift [lemma, in Completeness.FullSequent]
continuation [definition, in Completeness.SDialogues]
continuation_lift [definition, in Completeness.SDialogues]
Contr [constructor, in Completeness.Gentzen]
Contr [constructor, in Completeness.FullSequent]
con_T_correct [lemma, in Completeness.Stability]
con_T [definition, in Completeness.Stability]
con_subs [definition, in Completeness.GenTarski]
counter_safe_lift [definition, in Completeness.SDialogues]
counter_safe [definition, in Completeness.SDialogues]
count_nat [lemma, in Completeness.DecidableEnumerable]
count_bool [lemma, in Completeness.DecidableEnumerable]
count_enum' [lemma, in Completeness.DecidableEnumerable]
Ctx [constructor, in Completeness.ND]
ctx_incl [definition, in Completeness.KripkeCompleteness]
ctx_in [lemma, in Completeness.FullSequent]
ctx_out [lemma, in Completeness.FullSequent]
cumulative [definition, in Completeness.DecidableEnumerable]
cum_T [projection, in Completeness.DecidableEnumerable]
cum_ge' [lemma, in Completeness.DecidableEnumerable]
cum_ge [lemma, in Completeness.DecidableEnumerable]
cutfree_seq_ND [lemma, in Completeness.Gentzen]
cycle_shift_subject [lemma, in Completeness.ND]
cycle_shift_shift [lemma, in Completeness.ND]
cycle_shift [definition, in Completeness.ND]
cycle_shift_subject [lemma, in Completeness.FullSequent]
cycle_shift_shift [lemma, in Completeness.FullSequent]
cycle_shift [definition, in Completeness.FullSequent]
C_longenough [lemma, in Completeness.DecidableEnumerable]
C_exhaustive [lemma, in Completeness.DecidableEnumerable]
D
DAll [constructor, in Completeness.DialogFull]DAll [constructor, in Completeness.DialogFragment]
DAndL [constructor, in Completeness.DialogFull]
DAndR [constructor, in Completeness.DialogFull]
dcompleteness [lemma, in Completeness.Sorensen]
Dec [definition, in Completeness.Prelim]
dec [definition, in Completeness.Prelim]
Decb [abbreviation, in Completeness.Prelim]
decidable [definition, in Completeness.DecidableEnumerable]
DecidableEnumerable [library]
decidable_iff [lemma, in Completeness.DecidableEnumerable]
dec_f [projection, in Completeness.Sorensen]
dec_count_enum' [lemma, in Completeness.DecidableEnumerable]
dec_count_enum [lemma, in Completeness.DecidableEnumerable]
dec_disj [lemma, in Completeness.DecidableEnumerable]
dec_conj [lemma, in Completeness.DecidableEnumerable]
dec_compl [lemma, in Completeness.DecidableEnumerable]
dec_decidable' [lemma, in Completeness.DecidableEnumerable]
dec_f [projection, in Completeness.SDialogues]
dec_transfer [lemma, in Completeness.Prelim]
dec_DM_impl [lemma, in Completeness.Prelim]
dec_DM_and [lemma, in Completeness.Prelim]
dec_DN [lemma, in Completeness.Prelim]
Dec_false [lemma, in Completeness.Prelim]
Dec_true [lemma, in Completeness.Prelim]
Dec_auto_not [lemma, in Completeness.Prelim]
Dec_auto [lemma, in Completeness.Prelim]
Dec_reflect_eq [lemma, in Completeness.Prelim]
Dec_reflect [lemma, in Completeness.Prelim]
dec_sig_ext_Preds [instance, in Completeness.FOL]
dec_sig_ext_Funcs [instance, in Completeness.FOL]
dec_form [instance, in Completeness.FOL]
dec_term [instance, in Completeness.FOL]
dec_vec [instance, in Completeness.FOL]
dec_vec_in [lemma, in Completeness.FOL]
dec_form [instance, in Completeness.FullFOL]
dec_term [instance, in Completeness.FullFOL]
dec_vec [instance, in Completeness.FullFOL]
dec_vec_in [lemma, in Completeness.FullFOL]
Def [constructor, in Completeness.Sorensen]
Def [constructor, in Completeness.SDialogues]
defense [projection, in Completeness.Sorensen]
defense [projection, in Completeness.SDialogues]
defense_form [inductive, in Completeness.DialogFull]
defense_form [inductive, in Completeness.DialogFragment]
deferred [definition, in Completeness.Sorensen]
deferred [definition, in Completeness.SDialogues]
DExt [constructor, in Completeness.DialogFull]
DGame [section, in Completeness.Sorensen]
DGame.f [variable, in Completeness.Sorensen]
DGame.R [variable, in Completeness.Sorensen]
DialogFragment [section, in Completeness.DialogFragment]
DialogFragment [library]
DialogFull [section, in Completeness.DialogFull]
DialogFull [library]
DialogFull.eq_dec_Preds [variable, in Completeness.DialogFull]
DialogFull.eq_dec_Funcs [variable, in Completeness.DialogFull]
DImpl [constructor, in Completeness.DialogFull]
DImpl [constructor, in Completeness.DialogFragment]
discrete [definition, in Completeness.DecidableEnumerable]
discrete_list [lemma, in Completeness.DecidableEnumerable]
discrete_option [lemma, in Completeness.DecidableEnumerable]
discrete_sum [lemma, in Completeness.DecidableEnumerable]
discrete_prod [lemma, in Completeness.DecidableEnumerable]
discrete_nat_nat [lemma, in Completeness.DecidableEnumerable]
discrete_nat [lemma, in Completeness.DecidableEnumerable]
discrete_bool [lemma, in Completeness.DecidableEnumerable]
discrete_iff [lemma, in Completeness.DecidableEnumerable]
Disj [constructor, in Completeness.FullSyntax]
disjoint [definition, in Completeness.Prelim]
disjoint_app [lemma, in Completeness.Prelim]
disjoint_cons [lemma, in Completeness.Prelim]
disjoint_nil' [lemma, in Completeness.Prelim]
disjoint_nil [lemma, in Completeness.Prelim]
disjoint_incl [lemma, in Completeness.Prelim]
disjoint_symm [lemma, in Completeness.Prelim]
disjoint_forall [lemma, in Completeness.Prelim]
DN [definition, in Completeness.Stability]
DN [lemma, in Completeness.ND]
dnt [definition, in Completeness.ND]
DNT [section, in Completeness.ND]
dnt_to_TCE [lemma, in Completeness.ND]
dnt_to_CE [lemma, in Completeness.ND]
dnt_remove_ctx [lemma, in Completeness.ND]
dnt_CE [lemma, in Completeness.ND]
dnt_to_TIE [lemma, in Completeness.ND]
dnt_to_IE [lemma, in Completeness.ND]
dnt_float [lemma, in Completeness.ND]
dnt_subst [lemma, in Completeness.ND]
dn_to_sta [lemma, in Completeness.Stability]
DN_T [lemma, in Completeness.ND]
dn_inherit [lemma, in Completeness.GenCompleteness]
DOAtk [constructor, in Completeness.Sorensen]
DODef [constructor, in Completeness.Sorensen]
domove [inductive, in Completeness.Sorensen]
DOrL [constructor, in Completeness.DialogFull]
DOrR [constructor, in Completeness.DialogFull]
DP [lemma, in Completeness.ND]
DPAtk [constructor, in Completeness.Sorensen]
DPDef [constructor, in Completeness.Sorensen]
DPexp1 [definition, in Completeness.GenConstructions]
DPexp2 [definition, in Completeness.GenConstructions]
DPexp3 [definition, in Completeness.GenConstructions]
dpmove [inductive, in Completeness.Sorensen]
Dprv [inductive, in Completeness.Sorensen]
Dprv [inductive, in Completeness.SDialogues]
Dprv_just [lemma, in Completeness.Sorensen]
Dprv_ax [lemma, in Completeness.Sorensen]
Dprv_echo [lemma, in Completeness.Sorensen]
Dprv_exp [lemma, in Completeness.Sorensen]
Dprv_defend [lemma, in Completeness.Sorensen]
Dprv_weak [lemma, in Completeness.Sorensen]
Dprv_ewin [lemma, in Completeness.Sorensen]
Dprv_fprv [lemma, in Completeness.DialogFull]
Dprv_fprv' [lemma, in Completeness.DialogFull]
Dprv_state_size [definition, in Completeness.SDialogues]
Dprv_size [definition, in Completeness.SDialogues]
Dprv_state [inductive, in Completeness.SDialogues]
Dprv_ND [lemma, in Completeness.DialogFragment]
droppable [definition, in Completeness.GenTarski]
droppable_BL [lemma, in Completeness.GenTarski]
droppable_E [lemma, in Completeness.GenTarski]
droppable_S [lemma, in Completeness.GenTarski]
droppable_exploding_bot [lemma, in Completeness.GenTarski]
droppable_standard_bot [lemma, in Completeness.GenTarski]
droppable_classical [lemma, in Completeness.GenTarski]
drop_interp [definition, in Completeness.GenTarski]
drop_interp'_sat [lemma, in Completeness.GenTarski]
drop_interp'_eval [lemma, in Completeness.GenTarski]
drop_interp' [definition, in Completeness.GenTarski]
DS [constructor, in Completeness.SDialogues]
dstate [definition, in Completeness.Sorensen]
dummy_sig [definition, in Completeness.Stability]
dummy_SM [lemma, in Completeness.GenTarski]
dummy_xm [lemma, in Completeness.GenTarski]
dummy_interp [definition, in Completeness.GenTarski]
dvalid [definition, in Completeness.Sorensen]
dwin_Dprv [lemma, in Completeness.Sorensen]
dwin_Dprv_embed [definition, in Completeness.Sorensen]
dwin_strat [inductive, in Completeness.Sorensen]
DWS [constructor, in Completeness.Sorensen]
E
ecompleteness [lemma, in Completeness.Sorensen]econsistency_trans [lemma, in Completeness.GenConstructions]
econsistency_inheritance [lemma, in Completeness.GenConstructions]
econsistent [definition, in Completeness.GenConstructions]
econsistent_prv [lemma, in Completeness.GenConstructions]
econsistent_Omega [lemma, in Completeness.GenConstructions]
econsistent_join_sub [lemma, in Completeness.GenConstructions]
econsistent_join [definition, in Completeness.GenConstructions]
EGame [section, in Completeness.Sorensen]
EGame.f [variable, in Completeness.Sorensen]
EGame.R [variable, in Completeness.Sorensen]
elem_prv [lemma, in Completeness.ND]
el_T [projection, in Completeness.DecidableEnumerable]
el_at_pos [lemma, in Completeness.Enumeration]
el_pos [lemma, in Completeness.Prelim]
EM [definition, in Completeness.GenTarski]
embed [definition, in Completeness.Gentzen]
Empty_set_eq_dec [instance, in Completeness.Prelim]
enum [projection, in Completeness.GenConstructions]
enum [definition, in Completeness.DecidableEnumerable]
Enumerability [section, in Completeness.ND]
Enumerability [section, in Completeness.FOL]
Enumerability.enum_Preds [variable, in Completeness.FOL]
Enumerability.enum_Funcs [variable, in Completeness.FOL]
enumerable [definition, in Completeness.DecidableEnumerable]
enumerable_conj [lemma, in Completeness.DecidableEnumerable]
enumerable_disj [lemma, in Completeness.DecidableEnumerable]
enumerable__T_list [lemma, in Completeness.DecidableEnumerable]
enumerable_list [instance, in Completeness.DecidableEnumerable]
enumerable_list.fixL.LX [variable, in Completeness.DecidableEnumerable]
enumerable_list.fixL [section, in Completeness.DecidableEnumerable]
enumerable_list.X [variable, in Completeness.DecidableEnumerable]
enumerable_list [section, in Completeness.DecidableEnumerable]
enumerable__T_option [lemma, in Completeness.DecidableEnumerable]
enumerable__T_sum [lemma, in Completeness.DecidableEnumerable]
enumerable__T_prod [lemma, in Completeness.DecidableEnumerable]
enumerable_enum [lemma, in Completeness.DecidableEnumerable]
enumerable_nat_nat [lemma, in Completeness.DecidableEnumerable]
enumerable_prod.fixLs.L_Y [variable, in Completeness.DecidableEnumerable]
enumerable_prod.fixLs.L_X [variable, in Completeness.DecidableEnumerable]
enumerable_prod.fixLs [section, in Completeness.DecidableEnumerable]
enumerable_prod.Y [variable, in Completeness.DecidableEnumerable]
enumerable_prod.X [variable, in Completeness.DecidableEnumerable]
enumerable_prod [section, in Completeness.DecidableEnumerable]
enumerable_enum.e [variable, in Completeness.DecidableEnumerable]
enumerable_enum.p [variable, in Completeness.DecidableEnumerable]
enumerable_enum.X [variable, in Completeness.DecidableEnumerable]
enumerable_enum [section, in Completeness.DecidableEnumerable]
enumerable_enumerable_T [lemma, in Completeness.DecidableEnumerable]
enumerable__T [definition, in Completeness.DecidableEnumerable]
Enumeration [section, in Completeness.Enumeration]
Enumeration [library]
enumeration_stability [lemma, in Completeness.Stability]
enumeration_semi_decidable [lemma, in Completeness.Stability]
Enumeration.Hlen [variable, in Completeness.Enumeration]
Enumeration.X [variable, in Completeness.Enumeration]
enumT [record, in Completeness.DecidableEnumerable]
enumT_nat [instance, in Completeness.DecidableEnumerable]
enumT_sig_ext_Preds [instance, in Completeness.FOL]
enumT_sig_ext_Funcs [instance, in Completeness.FOL]
enumT_form [instance, in Completeness.FOL]
enumT_term [instance, in Completeness.FOL]
enumT_vec [instance, in Completeness.FOL]
enum_tsat_T [lemma, in Completeness.Stability]
enum_T_map_closed_homo [lemma, in Completeness.Stability]
enum_T_map_closed_closing [lemma, in Completeness.Stability]
enum_T [definition, in Completeness.Stability]
enum_tprv [lemma, in Completeness.ND]
enum_containsL [lemma, in Completeness.ND]
enum_p [lemma, in Completeness.ND]
enum_el [lemma, in Completeness.ND]
enum_prv [lemma, in Completeness.ND]
enum_unused [projection, in Completeness.GenConstructions]
enum_enum [projection, in Completeness.GenConstructions]
enum_enumT [lemma, in Completeness.DecidableEnumerable]
enum_count [lemma, in Completeness.DecidableEnumerable]
enum_enumerable [section, in Completeness.DecidableEnumerable]
enum_bool [instance, in Completeness.DecidableEnumerable]
enum_to_cumulative [lemma, in Completeness.DecidableEnumerable]
enum_stprv [lemma, in Completeness.Gentzen]
enum_sprv [lemma, in Completeness.Gentzen]
enum_tmap [lemma, in Completeness.FOL]
enum_tmap [lemma, in Completeness.FullFOL]
env [definition, in Completeness.GenTarski]
EOAtk [constructor, in Completeness.Sorensen]
EOCounter [constructor, in Completeness.Sorensen]
EODef [constructor, in Completeness.Sorensen]
eomove [inductive, in Completeness.Sorensen]
EPAtk [constructor, in Completeness.Sorensen]
EPDef [constructor, in Completeness.Sorensen]
epmove [inductive, in Completeness.Sorensen]
EqDec [section, in Completeness.FOL]
EqDec [section, in Completeness.FullFOL]
EqDec.eq_dec_Preds [variable, in Completeness.FOL]
EqDec.eq_dec_Funcs [variable, in Completeness.FOL]
EqDec.eq_dec_Preds [variable, in Completeness.FullFOL]
EqDec.eq_dec_Funcs [variable, in Completeness.FullFOL]
eqType [record, in Completeness.Prelim]
EqType [constructor, in Completeness.Prelim]
eqType_dec [projection, in Completeness.Prelim]
eqType_X [projection, in Completeness.Prelim]
Equi [section, in Completeness.Prelim]
equi [definition, in Completeness.Prelim]
equi_rotate [lemma, in Completeness.Prelim]
equi_shift [lemma, in Completeness.Prelim]
equi_swap [lemma, in Completeness.Prelim]
equi_dup [lemma, in Completeness.Prelim]
equi_push [lemma, in Completeness.Prelim]
equi_Equivalence [instance, in Completeness.Prelim]
Equi.X [variable, in Completeness.Prelim]
eq_incl [lemma, in Completeness.DialogFull]
eq_incl [lemma, in Completeness.DialogFragment]
esoundsess [lemma, in Completeness.Sorensen]
eval [definition, in Completeness.GenTarski]
evalid [definition, in Completeness.Sorensen]
eval_ident_fragment [lemma, in Completeness.GenCompleteness]
eval_ident [lemma, in Completeness.GenCompleteness]
eval_comp [lemma, in Completeness.GenTarski]
eval_ext [lemma, in Completeness.GenTarski]
ewin_Dprv [lemma, in Completeness.Sorensen]
ewin_strat [inductive, in Completeness.Sorensen]
EWS [constructor, in Completeness.Sorensen]
Ex [constructor, in Completeness.FullSyntax]
ExE [lemma, in Completeness.ND]
ExI [lemma, in Completeness.ND]
ExL [constructor, in Completeness.FullSequent]
Exp [constructor, in Completeness.ND]
Exp [definition, in Completeness.GenConstructions]
exp [definition, in Completeness.GenConstructions]
Exp [constructor, in Completeness.FullSequent]
expl [constructor, in Completeness.ND]
exploding [definition, in Completeness.GenConstructions]
exploding_inherit [lemma, in Completeness.GenConstructions]
exploding_bot [definition, in Completeness.GenTarski]
Exp_exploding [lemma, in Completeness.GenConstructions]
Exp_closed [lemma, in Completeness.GenConstructions]
Exp_econsistent [lemma, in Completeness.GenConstructions]
Exp_sub [lemma, in Completeness.GenConstructions]
exp_axiom_lift [lemma, in Completeness.GenConstructions]
exp_axiom [definition, in Completeness.GenConstructions]
ExR [constructor, in Completeness.FullSequent]
extend [definition, in Completeness.FOL]
extend [definition, in Completeness.FullFOL]
ext_form [definition, in Completeness.Syntax]
ext_term [definition, in Completeness.Syntax]
ext_form [definition, in Completeness.FullSyntax]
ext_term [definition, in Completeness.FullSyntax]
ext_c'_unused [lemma, in Completeness.FOL]
ext_c'_unused_term [lemma, in Completeness.FOL]
ext_c [definition, in Completeness.FOL]
ext_c' [definition, in Completeness.FOL]
E_S_subsumption [lemma, in Completeness.GenTarski]
F
Fal [constructor, in Completeness.Syntax]Fal [constructor, in Completeness.FullSyntax]
False_enumT [instance, in Completeness.Stability]
False_eq_dec [instance, in Completeness.Prelim]
False_dec [instance, in Completeness.Prelim]
filter [definition, in Completeness.Prelim]
Filter [section, in Completeness.Prelim]
filter_comm [lemma, in Completeness.Prelim]
filter_and [lemma, in Completeness.Prelim]
filter_pq_eq [lemma, in Completeness.Prelim]
filter_pq_mono [lemma, in Completeness.Prelim]
filter_fst' [lemma, in Completeness.Prelim]
filter_fst [lemma, in Completeness.Prelim]
filter_app [lemma, in Completeness.Prelim]
filter_id [lemma, in Completeness.Prelim]
filter_mono [lemma, in Completeness.Prelim]
filter_incl [lemma, in Completeness.Prelim]
Filter.X [variable, in Completeness.Prelim]
fin [abbreviation, in Completeness.unscoped]
find_unused_L [lemma, in Completeness.FOL]
find_unused [lemma, in Completeness.FOL]
find_unused_term [lemma, in Completeness.FOL]
find_unused_L [lemma, in Completeness.FullFOL]
find_unused [lemma, in Completeness.FullFOL]
find_unused_term [lemma, in Completeness.FullFOL]
FiniteCompleteness [section, in Completeness.GenCompleteness]
fin_T_to_context [lemma, in Completeness.Stability]
fin_T_con_T [lemma, in Completeness.Stability]
fin_T_map_closed [lemma, in Completeness.Stability]
fin_T [definition, in Completeness.Stability]
fin_minus [definition, in Completeness.FOL]
fix_sig [section, in Completeness.Syntax]
fix_sig [section, in Completeness.FullSyntax]
flat_map_app [lemma, in Completeness.Enumeration]
focus_el [lemma, in Completeness.FullSequent]
FOL [section, in Completeness.FOL]
FOL [library]
FOL.ContainsAutomation [section, in Completeness.FOL]
_ ⋄ _ [notation, in Completeness.FOL]
_ ∈ _ [notation, in Completeness.FOL]
_ ⊑ _ [notation, in Completeness.FOL]
_ ⊏ _ [notation, in Completeness.FOL]
Forall [inductive, in Completeness.FOL]
Forall [inductive, in Completeness.FullFOL]
Forall_cons [constructor, in Completeness.FOL]
Forall_nil [constructor, in Completeness.FOL]
Forall_cons [constructor, in Completeness.FullFOL]
Forall_nil [constructor, in Completeness.FullFOL]
form [inductive, in Completeness.Syntax]
form [inductive, in Completeness.FullSyntax]
form_rules [instance, in Completeness.DialogFull]
form_enum_fresh [lemma, in Completeness.Enumeration]
form_enum_enumerates [lemma, in Completeness.Enumeration]
form_enum [definition, in Completeness.Enumeration]
form_rules [instance, in Completeness.DialogFragment]
form_shift [definition, in Completeness.FOL]
form_shift [definition, in Completeness.FullFOL]
fprv [inductive, in Completeness.FullSequent]
fprv_defend [lemma, in Completeness.DialogFull]
fprv_Dprv [lemma, in Completeness.DialogFull]
FullFOL [section, in Completeness.FullFOL]
FullFOL [library]
FullFOL.ContainsAutomation [section, in Completeness.FullFOL]
_ ⋄ _ [notation, in Completeness.FullFOL]
_ ∈ _ [notation, in Completeness.FullFOL]
_ ⊑ _ [notation, in Completeness.FullFOL]
_ ⊏ _ [notation, in Completeness.FullFOL]
↑ [notation, in Completeness.FullFOL]
FullSequent [section, in Completeness.FullSequent]
FullSequent [library]
_ ⊢f _ [notation, in Completeness.FullSequent]
⋁ _ [notation, in Completeness.FullSequent]
FullSyntax [library]
Func [constructor, in Completeness.Syntax]
Func [constructor, in Completeness.FullSyntax]
funcomp [definition, in Completeness.axioms]
funcomp [definition, in Completeness.unscoped]
Funcs [projection, in Completeness.Syntax]
Funcs [projection, in Completeness.FullSyntax]
fun_ar [projection, in Completeness.Syntax]
fun_ar [projection, in Completeness.FullSyntax]
G
GDN [lemma, in Completeness.GenConstructions]GDP [lemma, in Completeness.GenConstructions]
GenCompleteness [library]
GenCons [section, in Completeness.GenConstructions]
GenConstructions [library]
GenCons.Explosion [section, in Completeness.GenConstructions]
GenCons.Explosion.e [variable, in Completeness.GenConstructions]
GenCons.Explosion.Hclosed [variable, in Completeness.GenConstructions]
GenCons.Explosion.He [variable, in Completeness.GenConstructions]
GenCons.Explosion.T [variable, in Completeness.GenConstructions]
GenCons.GBot [variable, in Completeness.GenConstructions]
GenCons.GBot_closed [variable, in Completeness.GenConstructions]
GenCons.Henkin [section, in Completeness.GenConstructions]
GenCons.Henkin.e [variable, in Completeness.GenConstructions]
GenCons.Henkin.Hclosed [variable, in Completeness.GenConstructions]
GenCons.Henkin.He [variable, in Completeness.GenConstructions]
GenCons.Henkin.Hexp [variable, in Completeness.GenConstructions]
GenCons.Henkin.Hunused [variable, in Completeness.GenConstructions]
GenCons.Henkin.T [variable, in Completeness.GenConstructions]
GenCons.Omega [section, in Completeness.GenConstructions]
GenCons.Omega.e [variable, in Completeness.GenConstructions]
GenCons.Omega.He [variable, in Completeness.GenConstructions]
GenCons.Omega.Hexp [variable, in Completeness.GenConstructions]
GenCons.Omega.Hhenkin [variable, in Completeness.GenConstructions]
GenCons.Omega.T [variable, in Completeness.GenConstructions]
_ ∘ _ [notation, in Completeness.GenConstructions]
GenCons.Union [section, in Completeness.GenConstructions]
GenCons.Union.econsistent_f [variable, in Completeness.GenConstructions]
GenCons.Union.f [variable, in Completeness.GenConstructions]
GenCons.Union.f_le [variable, in Completeness.GenConstructions]
_ ⊩G _ [notation, in Completeness.GenConstructions]
_ ⊢G _ [notation, in Completeness.GenConstructions]
∃ _ [notation, in Completeness.GenConstructions]
⊥ [notation, in Completeness.GenConstructions]
¬ _ [notation, in Completeness.GenConstructions]
GenTarski [library]
Gentzen [section, in Completeness.Gentzen]
Gentzen [library]
Gentzen.CutElimination [section, in Completeness.Gentzen]
Gentzen.Enumerability [section, in Completeness.Gentzen]
Gentzen.Soundness [section, in Completeness.Gentzen]
Gentzen.Weakening [section, in Completeness.Gentzen]
_ ;; _ ⊢s _ [notation, in Completeness.Gentzen]
_ ⊢S _ [notation, in Completeness.Gentzen]
GExE [lemma, in Completeness.GenConstructions]
GExI [lemma, in Completeness.GenConstructions]
GExp [lemma, in Completeness.GenConstructions]
GXM [lemma, in Completeness.GenConstructions]
H
has_model [definition, in Completeness.GenTarski]Henkin [definition, in Completeness.GenConstructions]
henkin [definition, in Completeness.GenConstructions]
Henkin_T [lemma, in Completeness.GenConstructions]
Henkin_is_Henkin [lemma, in Completeness.GenConstructions]
Henkin_consistent [lemma, in Completeness.GenConstructions]
henkin_le [lemma, in Completeness.GenConstructions]
henkin_unused [lemma, in Completeness.GenConstructions]
henkin_axiom_unused [lemma, in Completeness.GenConstructions]
henkin_axiom [definition, in Completeness.GenConstructions]
I
id [definition, in Completeness.unscoped]ids [projection, in Completeness.unscoped]
ids [constructor, in Completeness.unscoped]
idsRen [instance, in Completeness.unscoped]
idSubst_form [definition, in Completeness.Syntax]
idSubst_term [definition, in Completeness.Syntax]
idSubst_form [definition, in Completeness.FullSyntax]
idSubst_term [definition, in Completeness.FullSyntax]
IE [constructor, in Completeness.ND]
IE_to_CE [lemma, in Completeness.ND]
iff_dec [instance, in Completeness.Prelim]
II [constructor, in Completeness.ND]
IL [constructor, in Completeness.Gentzen]
IL [constructor, in Completeness.FullSequent]
Impl [constructor, in Completeness.Syntax]
Impl [constructor, in Completeness.FullSyntax]
impl_dec [instance, in Completeness.Prelim]
inclp [definition, in Completeness.Prelim]
Inclusion [section, in Completeness.Prelim]
Inclusion.X [variable, in Completeness.Prelim]
incl_equi_proper [instance, in Completeness.Prelim]
incl_preorder [instance, in Completeness.Prelim]
incl_app_left [lemma, in Completeness.Prelim]
incl_lrcons [lemma, in Completeness.Prelim]
incl_rcons [lemma, in Completeness.Prelim]
incl_lcons [lemma, in Completeness.Prelim]
incl_shift [lemma, in Completeness.Prelim]
incl_nil_eq [lemma, in Completeness.Prelim]
incl_map [lemma, in Completeness.Prelim]
incl_sing [lemma, in Completeness.Prelim]
incl_nil [lemma, in Completeness.Prelim]
inconsistent [lemma, in Completeness.Consistency]
input_fragment [definition, in Completeness.GenCompleteness]
input_bot [definition, in Completeness.GenCompleteness]
instId_form [lemma, in Completeness.Syntax]
instId_term [lemma, in Completeness.Syntax]
instId_form [lemma, in Completeness.FullSyntax]
instId_term [lemma, in Completeness.FullSyntax]
interp [record, in Completeness.GenTarski]
intu [constructor, in Completeness.ND]
In_T_closed [projection, in Completeness.GenConstructions]
In_T [projection, in Completeness.GenConstructions]
in_rem_iff [lemma, in Completeness.Prelim]
in_filter_iff [lemma, in Completeness.Prelim]
in_concat_iff [lemma, in Completeness.Prelim]
in_equi_proper [instance, in Completeness.Prelim]
in_incl_proper [instance, in Completeness.Prelim]
in_cons_neq [lemma, in Completeness.Prelim]
in_sing [lemma, in Completeness.Prelim]
in_omap_iff [lemma, in Completeness.Prelim]
IR [constructor, in Completeness.Gentzen]
IR [constructor, in Completeness.FullSequent]
is_Henkin_inherit [lemma, in Completeness.GenConstructions]
is_Henkin [definition, in Completeness.GenConstructions]
IVec [inductive, in Completeness.SDialogues]
i_F [projection, in Completeness.GenTarski]
i_P [projection, in Completeness.GenTarski]
i_f [projection, in Completeness.GenTarski]
J
justified [definition, in Completeness.Sorensen]justified [definition, in Completeness.SDialogues]
justified_weak [lemma, in Completeness.Sorensen]
justified_weak [lemma, in Completeness.SDialogues]
K
kbottomless [definition, in Completeness.Kripke]kconstraint [definition, in Completeness.Kripke]
kcon_subs [definition, in Completeness.Kripke]
kexploding [definition, in Completeness.Kripke]
kmodel [record, in Completeness.Kripke]
kmodel_reach_trans [instance, in Completeness.Kripke]
kmodel_reach_refl [instance, in Completeness.Kripke]
Kripke [section, in Completeness.Kripke]
Kripke [library]
KripkeCompleteness [section, in Completeness.KripkeCompleteness]
KripkeCompleteness [library]
KripkeCompleteness.BottomlessCompleteness [section, in Completeness.KripkeCompleteness]
KripkeCompleteness.Contexts [section, in Completeness.KripkeCompleteness]
KripkeCompleteness.ExplodingCompleteness [section, in Completeness.KripkeCompleteness]
KripkeCompleteness.MPRequired [section, in Completeness.KripkeCompleteness]
KripkeCompleteness.MPRequired.C [variable, in Completeness.KripkeCompleteness]
KripkeCompleteness.MPRequired.HC [variable, in Completeness.KripkeCompleteness]
KripkeCompleteness.MPRequired.K_completeness [variable, in Completeness.KripkeCompleteness]
KripkeCompleteness.StandardCompleteness [section, in Completeness.KripkeCompleteness]
KripkeCompleteness.StandardCompleteness.sprv_stab [variable, in Completeness.KripkeCompleteness]
_ ;; _ ⊢sC _ [notation, in Completeness.KripkeCompleteness]
_ ⊢SC _ [notation, in Completeness.KripkeCompleteness]
_ <<=C _ [notation, in Completeness.KripkeCompleteness]
Kripke.Model [section, in Completeness.Kripke]
Kripke.Model.domain [variable, in Completeness.Kripke]
Kripke.Model.M [variable, in Completeness.Kripke]
Kripke.Substs [section, in Completeness.Kripke]
Kripke.Substs.D [variable, in Completeness.Kripke]
_ ⊨( _ , _ ) _ [notation, in Completeness.Kripke]
_ ⊨( _ ) _ [notation, in Completeness.Kripke]
ksat [definition, in Completeness.Kripke]
ksat_comp [lemma, in Completeness.Kripke]
ksat_ext [lemma, in Completeness.Kripke]
ksat_iff [lemma, in Completeness.Kripke]
ksat_mon [lemma, in Completeness.Kripke]
ksemantic_explosion [lemma, in Completeness.Kripke]
ksoundness [lemma, in Completeness.Kripke]
KSoundness [section, in Completeness.Kripke]
ksoundness_seq [lemma, in Completeness.Gentzen]
kstandard [definition, in Completeness.Kripke]
kstandard_explodes [lemma, in Completeness.Kripke]
kvalid_L_subs [lemma, in Completeness.Kripke]
kvalid_T [definition, in Completeness.Kripke]
kvalid_L [definition, in Completeness.Kripke]
K_std_seq_ksoundness [lemma, in Completeness.KripkeCompleteness]
K_std_completeness [lemma, in Completeness.KripkeCompleteness]
K_std_standard [lemma, in Completeness.KripkeCompleteness]
K_std_ksat [lemma, in Completeness.KripkeCompleteness]
K_std_sprv [lemma, in Completeness.KripkeCompleteness]
K_std_correct [lemma, in Completeness.KripkeCompleteness]
K_std [instance, in Completeness.KripkeCompleteness]
K_bottomless_completeness [lemma, in Completeness.KripkeCompleteness]
K_exp_seq_ksoundness [lemma, in Completeness.KripkeCompleteness]
K_exp_completeness [lemma, in Completeness.KripkeCompleteness]
K_ctx_exploding [lemma, in Completeness.KripkeCompleteness]
K_ctx_ksat [lemma, in Completeness.KripkeCompleteness]
K_ctx_sprv [lemma, in Completeness.KripkeCompleteness]
K_ctx_correct [lemma, in Completeness.KripkeCompleteness]
K_ctx [instance, in Completeness.KripkeCompleteness]
k_Bot [projection, in Completeness.Kripke]
k_P [projection, in Completeness.Kripke]
k_interp [projection, in Completeness.Kripke]
L
lconst [constructor, in Completeness.ND]lift_ext_c_closes_T [lemma, in Completeness.FOL]
lift_ext_c_closes [lemma, in Completeness.FOL]
lift_drop_inverse [lemma, in Completeness.FOL]
lift_drop_inverse' [lemma, in Completeness.FOL]
lift_drop_inverse_term' [lemma, in Completeness.FOL]
lift_interp_sat [lemma, in Completeness.GenTarski]
lift_interp_eval [lemma, in Completeness.GenTarski]
lift_interp [definition, in Completeness.GenTarski]
list_completeness_fragment [lemma, in Completeness.GenCompleteness]
list_completeness_expl [lemma, in Completeness.GenCompleteness]
list_completeness_standard [lemma, in Completeness.GenCompleteness]
list_cc [lemma, in Completeness.Prelim]
list_exists_not_incl [lemma, in Completeness.Prelim]
list_exists_DM [lemma, in Completeness.Prelim]
list_exists_dec [instance, in Completeness.Prelim]
list_forall_dec [instance, in Completeness.Prelim]
list_in_dec [instance, in Completeness.Prelim]
list_cycle [lemma, in Completeness.Prelim]
list_eq_dec [instance, in Completeness.Prelim]
list_ind_ne [lemma, in Completeness.Prelim]
list_comp [definition, in Completeness.axioms]
list_id [definition, in Completeness.axioms]
list_ext [definition, in Completeness.axioms]
list_prod_in [lemma, in Completeness.FOL]
list_T [definition, in Completeness.FOL]
list_T [definition, in Completeness.FullFOL]
LJD [section, in Completeness.Sorensen]
LJD.f [variable, in Completeness.Sorensen]
LJD.R [variable, in Completeness.Sorensen]
_ ⊢D _ [notation, in Completeness.Sorensen]
L_tsat_T [definition, in Completeness.Stability]
L_tded [definition, in Completeness.ND]
L_con [definition, in Completeness.ND]
L_ded [definition, in Completeness.ND]
L_T [projection, in Completeness.DecidableEnumerable]
L_T_form_len [lemma, in Completeness.Enumeration]
L_T_Enumeration [section, in Completeness.Enumeration]
L_T_sub_or [lemma, in Completeness.Enumeration]
L_T_sub [lemma, in Completeness.Enumeration]
L_T_unused [lemma, in Completeness.Enumeration]
L_T_unused_v [lemma, in Completeness.Enumeration]
L_T_unused_t [lemma, in Completeness.Enumeration]
L_T_nat_le [lemma, in Completeness.Enumeration]
L_T_unused.enum_Preds [variable, in Completeness.Enumeration]
L_T_unused.enum_Funcs [variable, in Completeness.Enumeration]
L_T_unused [section, in Completeness.Enumeration]
L_tseq [definition, in Completeness.Gentzen]
L_seq [definition, in Completeness.Gentzen]
L_form_cml [lemma, in Completeness.FOL]
L_form [definition, in Completeness.FOL]
L_term_cml [lemma, in Completeness.FOL]
L_term [definition, in Completeness.FOL]
L_vec [definition, in Completeness.FOL]
M
map_closed [definition, in Completeness.Stability]maximal [definition, in Completeness.GenConstructions]
maximal_prv [lemma, in Completeness.GenConstructions]
maximal_Omega [lemma, in Completeness.GenConstructions]
Membership [section, in Completeness.Prelim]
Membership.X [variable, in Completeness.Prelim]
model_fragment_classical [lemma, in Completeness.GenCompleteness]
model_fragment_correct [lemma, in Completeness.GenCompleteness]
model_fragment [instance, in Completeness.GenCompleteness]
model_bot_exploding [lemma, in Completeness.GenCompleteness]
model_bot_standard [lemma, in Completeness.GenCompleteness]
model_bot_classical [lemma, in Completeness.GenCompleteness]
model_bot_correct [lemma, in Completeness.GenCompleteness]
model_bot [instance, in Completeness.GenCompleteness]
mon_Bot [projection, in Completeness.Kripke]
mon_P [projection, in Completeness.Kripke]
MP [definition, in Completeness.Stability]
mp_to_ste [lemma, in Completeness.Stability]
mp_standard_completeness [lemma, in Completeness.GenCompleteness]
mp_tprv_stability [lemma, in Completeness.GenCompleteness]
N
nameless_equiv [lemma, in Completeness.ND]nameless_equiv' [lemma, in Completeness.FullSequent]
nameless_equiv [lemma, in Completeness.FullSequent]
nat_eq_dec [instance, in Completeness.Prelim]
NBot [projection, in Completeness.GenConstructions]
NBot_closed [projection, in Completeness.GenConstructions]
ND [library]
ND_def.Weakening [section, in Completeness.ND]
_ ⊩IE _ [notation, in Completeness.ND]
_ ⊩CL _ [notation, in Completeness.ND]
_ ⊩CE _ [notation, in Completeness.ND]
_ ⊩( _ , _ ) _ [notation, in Completeness.ND]
_ ⊩ _ [notation, in Completeness.ND]
_ ⊢IE _ [notation, in Completeness.ND]
_ ⊢CL _ [notation, in Completeness.ND]
_ ⊢CE _ [notation, in Completeness.ND]
_ ⊢( _ , _ ) _ [notation, in Completeness.ND]
_ ⊢ _ [notation, in Completeness.ND]
ND_def [section, in Completeness.ND]
ND_defend [lemma, in Completeness.DialogFragment]
neList [section, in Completeness.Prelim]
neList.B [variable, in Completeness.Prelim]
neList.P [variable, in Completeness.Prelim]
neList.S [variable, in Completeness.Prelim]
neList.X [variable, in Completeness.Prelim]
nodes [projection, in Completeness.Kripke]
normal [definition, in Completeness.Gentzen]
not_AllI [definition, in Completeness.Gentzen]
not_II [definition, in Completeness.Gentzen]
not_in_cons [lemma, in Completeness.Prelim]
not_dec [instance, in Completeness.Prelim]
nsprv_cons [lemma, in Completeness.KripkeCompleteness]
nthe [abbreviation, in Completeness.Prelim]
nthe [abbreviation, in Completeness.Prelim]
nthe_app_l [lemma, in Completeness.Prelim]
nthe_length [lemma, in Completeness.Prelim]
nth_order_map [lemma, in Completeness.FOL]
O
ocons [definition, in Completeness.Sorensen]ocons [definition, in Completeness.SDialogues]
ocons_sub [lemma, in Completeness.Sorensen]
ocons_sub [lemma, in Completeness.SDialogues]
ofNat [definition, in Completeness.DecidableEnumerable]
OL [constructor, in Completeness.FullSequent]
omap [definition, in Completeness.Prelim]
Omega [definition, in Completeness.GenConstructions]
omega [definition, in Completeness.GenConstructions]
Omega_all [lemma, in Completeness.GenConstructions]
Omega_impl [lemma, in Completeness.GenConstructions]
Omega_T [lemma, in Completeness.GenConstructions]
Omega_prv [lemma, in Completeness.GenConstructions]
omega_le [lemma, in Completeness.GenConstructions]
OP [constructor, in Completeness.Sorensen]
OP [constructor, in Completeness.SDialogues]
opening [inductive, in Completeness.Sorensen]
opening [inductive, in Completeness.SDialogues]
opred [definition, in Completeness.Sorensen]
opred [definition, in Completeness.SDialogues]
option_eq_dec [instance, in Completeness.Prelim]
or_dec [instance, in Completeness.Prelim]
or_single [lemma, in Completeness.FullSequent]
or_weak [lemma, in Completeness.FullSequent]
or_el [lemma, in Completeness.FullSequent]
or_char [lemma, in Completeness.FullSequent]
or_subst [lemma, in Completeness.FullSequent]
OR1 [constructor, in Completeness.FullSequent]
OR2 [constructor, in Completeness.FullSequent]
osum [definition, in Completeness.SDialogues]
output_fragment [definition, in Completeness.GenCompleteness]
output_bot [definition, in Completeness.GenCompleteness]
Out_T_impl [projection, in Completeness.GenConstructions]
Out_T_all [projection, in Completeness.GenConstructions]
Out_T_prv [projection, in Completeness.GenConstructions]
Out_T_sub [projection, in Completeness.GenConstructions]
Out_T_econsistent [projection, in Completeness.GenConstructions]
Out_T [projection, in Completeness.GenConstructions]
P
pairs_retract [lemma, in Completeness.DecidableEnumerable]Pc [constructor, in Completeness.ND]
peirce [inductive, in Completeness.ND]
Perm [constructor, in Completeness.FullSequent]
pext [axiom, in Completeness.axioms]
pi [lemma, in Completeness.axioms]
plain_enum_slow [lemma, in Completeness.Enumeration]
plain_enum_enumerates [lemma, in Completeness.Enumeration]
plain_enum [definition, in Completeness.Enumeration]
plan [definition, in Completeness.SDialogues]
plan_lift [definition, in Completeness.SDialogues]
pos [definition, in Completeness.Prelim]
Positions [section, in Completeness.Prelim]
Positions.d [variable, in Completeness.Prelim]
Positions.X [variable, in Completeness.Prelim]
pos_length [lemma, in Completeness.Prelim]
pos_nth [lemma, in Completeness.Prelim]
pos_nthe [lemma, in Completeness.Prelim]
Pred [constructor, in Completeness.Syntax]
Pred [constructor, in Completeness.FullSyntax]
Preds [projection, in Completeness.Syntax]
Preds [projection, in Completeness.FullSyntax]
pred_ar [projection, in Completeness.Syntax]
pred_ar [projection, in Completeness.FullSyntax]
pref [definition, in Completeness.FOL]
Prelim [library]
prod_enumerable [instance, in Completeness.DecidableEnumerable]
prod_eq_dec [instance, in Completeness.Prelim]
prod_comp [definition, in Completeness.axioms]
prod_ext [definition, in Completeness.axioms]
prod_id [definition, in Completeness.axioms]
prod_map [definition, in Completeness.axioms]
projection [lemma, in Completeness.DecidableEnumerable]
projection' [lemma, in Completeness.DecidableEnumerable]
PropT [section, in Completeness.Stability]
prop_T_correct [lemma, in Completeness.Stability]
prop_T [definition, in Completeness.Stability]
prv [inductive, in Completeness.ND]
prv_T_comp [lemma, in Completeness.ND]
prv_T_remove [lemma, in Completeness.ND]
prv_T_impl [lemma, in Completeness.ND]
prv_from_single [lemma, in Completeness.ND]
prv_cut [lemma, in Completeness.ND]
R
raise [definition, in Completeness.FOL]reachable [projection, in Completeness.Kripke]
reach_tran [projection, in Completeness.Kripke]
reach_refl [projection, in Completeness.Kripke]
RefutationComp [section, in Completeness.ND]
refutation_prv [lemma, in Completeness.ND]
rem [definition, in Completeness.Prelim]
Removal [section, in Completeness.Prelim]
Removal.X [variable, in Completeness.Prelim]
rem_inclr [lemma, in Completeness.Prelim]
rem_reorder [lemma, in Completeness.Prelim]
rem_id [lemma, in Completeness.Prelim]
rem_fst' [lemma, in Completeness.Prelim]
rem_fst [lemma, in Completeness.Prelim]
rem_comm [lemma, in Completeness.Prelim]
rem_equi [lemma, in Completeness.Prelim]
rem_app' [lemma, in Completeness.Prelim]
rem_app [lemma, in Completeness.Prelim]
rem_neq [lemma, in Completeness.Prelim]
rem_in [lemma, in Completeness.Prelim]
rem_cons' [lemma, in Completeness.Prelim]
rem_cons [lemma, in Completeness.Prelim]
rem_mono [lemma, in Completeness.Prelim]
rem_incl [lemma, in Completeness.Prelim]
rem_not_in [lemma, in Completeness.Prelim]
ren1 [projection, in Completeness.unscoped]
Ren1 [record, in Completeness.unscoped]
ren1 [constructor, in Completeness.unscoped]
Ren1 [inductive, in Completeness.unscoped]
ren2 [projection, in Completeness.unscoped]
Ren2 [record, in Completeness.unscoped]
ren2 [constructor, in Completeness.unscoped]
Ren2 [inductive, in Completeness.unscoped]
ren3 [projection, in Completeness.unscoped]
Ren3 [record, in Completeness.unscoped]
ren3 [constructor, in Completeness.unscoped]
Ren3 [inductive, in Completeness.unscoped]
ren4 [projection, in Completeness.unscoped]
Ren4 [record, in Completeness.unscoped]
ren4 [constructor, in Completeness.unscoped]
Ren4 [inductive, in Completeness.unscoped]
ren5 [projection, in Completeness.unscoped]
Ren5 [record, in Completeness.unscoped]
ren5 [constructor, in Completeness.unscoped]
Ren5 [inductive, in Completeness.unscoped]
rule_set [record, in Completeness.Sorensen]
rule_set [record, in Completeness.SDialogues]
R_nat_nat [definition, in Completeness.DecidableEnumerable]
S
SAll [constructor, in Completeness.FOL]SAll [constructor, in Completeness.FullFOL]
sat [definition, in Completeness.GenTarski]
sat_subst [lemma, in Completeness.GenTarski]
sat_comp [lemma, in Completeness.GenTarski]
sat_ext [lemma, in Completeness.GenTarski]
SConjL [constructor, in Completeness.FullFOL]
SConjR [constructor, in Completeness.FullFOL]
scons [definition, in Completeness.unscoped]
scons_comp [lemma, in Completeness.unscoped]
scons_eta_id [lemma, in Completeness.unscoped]
scons_eta [lemma, in Completeness.unscoped]
SDialogues [section, in Completeness.SDialogues]
SDialogues [library]
SDialogues.enum_def [variable, in Completeness.SDialogues]
SDialogues.enum_att [variable, in Completeness.SDialogues]
SDialogues.f [variable, in Completeness.SDialogues]
SDialogues.olt [variable, in Completeness.SDialogues]
SDialogues.oplus [variable, in Completeness.SDialogues]
SDialogues.ord [variable, in Completeness.SDialogues]
SDialogues.ord_ind [variable, in Completeness.SDialogues]
SDialogues.osuc [variable, in Completeness.SDialogues]
SDialogues.osup [variable, in Completeness.SDialogues]
SDialogues.ozero [variable, in Completeness.SDialogues]
SDialogues.R [variable, in Completeness.SDialogues]
_ ⊢D _ [notation, in Completeness.SDialogues]
SDisjL [constructor, in Completeness.FullFOL]
SDisjR [constructor, in Completeness.FullFOL]
semantic_dm [lemma, in Completeness.GenTarski]
semantic_explosion [lemma, in Completeness.GenTarski]
semi_completeness_fragment [lemma, in Completeness.GenCompleteness]
semi_completeness_standard [lemma, in Completeness.GenCompleteness]
seq_ND_T [lemma, in Completeness.Gentzen]
seq_ND [lemma, in Completeness.Gentzen]
seq_nameless_equiv [lemma, in Completeness.Gentzen]
seq_subst_Weak [lemma, in Completeness.Gentzen]
seq_Weak [lemma, in Completeness.Gentzen]
seq_consistent [lemma, in Completeness.Gentzen]
SEx [constructor, in Completeness.FullFOL]
sf [inductive, in Completeness.FOL]
sf [inductive, in Completeness.FullFOL]
sf_form_rules [lemma, in Completeness.DialogFull]
sf_form_rules [lemma, in Completeness.DialogFragment]
sf_well_founded [lemma, in Completeness.FOL]
sf_acc [lemma, in Completeness.FOL]
sf_well_founded [lemma, in Completeness.FullFOL]
sf_acc [lemma, in Completeness.FullFOL]
SGame [section, in Completeness.Sorensen]
SGame.f [variable, in Completeness.Sorensen]
SGame.R [variable, in Completeness.Sorensen]
shift [definition, in Completeness.unscoped]
shift_P [definition, in Completeness.FOL]
shift_P [definition, in Completeness.FullFOL]
SigExt [section, in Completeness.ND]
SigExt [section, in Completeness.FOL]
SigExt [section, in Completeness.GenTarski]
SigExt.D [variable, in Completeness.GenTarski]
SigExt.F [variable, in Completeness.GenTarski]
SigExt.F_ar [variable, in Completeness.GenTarski]
SigExt.P [variable, in Completeness.GenTarski]
SigExt.P_ar [variable, in Completeness.GenTarski]
Signature [record, in Completeness.Syntax]
Signature [record, in Completeness.FullSyntax]
sig_lift_out_T [lemma, in Completeness.ND]
sig_lift_out [lemma, in Completeness.ND]
sig_drop_Weak [lemma, in Completeness.ND]
sig_lift_Weak [lemma, in Completeness.ND]
sig_drop_subst' [lemma, in Completeness.FOL]
sig_drop_subst_term' [lemma, in Completeness.FOL]
sig_drop [definition, in Completeness.FOL]
sig_drop' [definition, in Completeness.FOL]
sig_drop_term [definition, in Completeness.FOL]
sig_drop_term' [definition, in Completeness.FOL]
sig_lift_subst [lemma, in Completeness.FOL]
sig_lift_subst_term [lemma, in Completeness.FOL]
sig_lift [definition, in Completeness.FOL]
sig_lift' [definition, in Completeness.FOL]
sig_lift_term [definition, in Completeness.FOL]
sig_lift_term' [definition, in Completeness.FOL]
sig_ext [definition, in Completeness.FOL]
sig_lift_subst_valid [lemma, in Completeness.GenTarski]
sig_lift_subst_sat [lemma, in Completeness.GenTarski]
SImplL [constructor, in Completeness.FOL]
SImplL [constructor, in Completeness.FullFOL]
SImplR [constructor, in Completeness.FOL]
SImplR [constructor, in Completeness.FullFOL]
size [definition, in Completeness.FOL]
size_induction_dep [lemma, in Completeness.Prelim]
size_induction [lemma, in Completeness.Prelim]
size_ind [lemma, in Completeness.FOL]
SM [definition, in Completeness.GenTarski]
SOAtk [constructor, in Completeness.Sorensen]
SOAtk [constructor, in Completeness.SDialogues]
SODef [constructor, in Completeness.Sorensen]
SODef [constructor, in Completeness.SDialogues]
somove [inductive, in Completeness.Sorensen]
somove [inductive, in Completeness.SDialogues]
Sorensen [library]
Soundness [lemma, in Completeness.GenTarski]
SPAtk [constructor, in Completeness.Sorensen]
SPAtk [constructor, in Completeness.SDialogues]
SPDef [constructor, in Completeness.Sorensen]
SPDef [constructor, in Completeness.SDialogues]
split_right [lemma, in Completeness.Sorensen]
spmove [inductive, in Completeness.Sorensen]
spmove [inductive, in Completeness.SDialogues]
sprv [inductive, in Completeness.Gentzen]
sprv_Dprv [lemma, in Completeness.DialogFragment]
sstate [definition, in Completeness.Sorensen]
sstate [definition, in Completeness.SDialogues]
ST [definition, in Completeness.Stability]
stA [constructor, in Completeness.FOL]
Stability [library]
StabilityClasses [section, in Completeness.Stability]
StabilityClasses.DN [section, in Completeness.Stability]
StabilityClasses.ObjMP [section, in Completeness.Stability]
StabilityClasses.ObjMP.ConT [section, in Completeness.Stability]
StabilityClasses.SyntMP [section, in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum [section, in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.HL [variable, in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.HX [variable, in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.L [variable, in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.mp [variable, in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.P [variable, in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.X [variable, in Completeness.Stability]
stable [definition, in Completeness.Stability]
stable_equiv [lemma, in Completeness.Stability]
stab_class [definition, in Completeness.Stability]
standard_bot [definition, in Completeness.GenTarski]
sta_to_dn [lemma, in Completeness.Stability]
stB [constructor, in Completeness.FOL]
ste_to_mp [lemma, in Completeness.Stability]
stF [constructor, in Completeness.FOL]
stf_to_st_context [lemma, in Completeness.Stability]
stIL [constructor, in Completeness.FOL]
stIR [constructor, in Completeness.FOL]
stP [constructor, in Completeness.FOL]
stprv [definition, in Completeness.Gentzen]
StrongCompleteness [section, in Completeness.GenCompleteness]
StrongSoundness [lemma, in Completeness.GenTarski]
strong_completeness_fragment [lemma, in Completeness.GenCompleteness]
strong_completeness_expl [lemma, in Completeness.GenCompleteness]
strong_completeness_standard [lemma, in Completeness.GenCompleteness]
strong_term_ind [lemma, in Completeness.FOL]
strong_term_ind' [lemma, in Completeness.FOL]
strong_term_ind [lemma, in Completeness.FullFOL]
strong_term_ind' [lemma, in Completeness.FullFOL]
strong_ksoundness [lemma, in Completeness.Kripke]
ST__f [definition, in Completeness.Stability]
ST__e [definition, in Completeness.Stability]
ST__a [definition, in Completeness.Stability]
subctx [definition, in Completeness.SDialogues]
subctx_lift [definition, in Completeness.SDialogues]
subset_T_trans [instance, in Completeness.FOL]
subset_T [definition, in Completeness.FOL]
subset_T_trans [instance, in Completeness.FullFOL]
subset_T [definition, in Completeness.FullFOL]
Subst_form [instance, in Completeness.Syntax]
Subst_term [instance, in Completeness.Syntax]
subst_form [definition, in Completeness.Syntax]
subst_term [definition, in Completeness.Syntax]
Subst_form [instance, in Completeness.FullSyntax]
Subst_term [instance, in Completeness.FullSyntax]
subst_form [definition, in Completeness.FullSyntax]
subst_term [definition, in Completeness.FullSyntax]
subst_Weak [lemma, in Completeness.ND]
subst_unused_closed' [lemma, in Completeness.FOL]
subst_unused_closed [lemma, in Completeness.FOL]
subst_unused_range [lemma, in Completeness.FOL]
subst_unused_single [lemma, in Completeness.FOL]
subst_unused_form [lemma, in Completeness.FOL]
subst_unused_term [lemma, in Completeness.FOL]
subst_size [lemma, in Completeness.FOL]
subst_unused_closed' [lemma, in Completeness.FullFOL]
subst_unused_closed [lemma, in Completeness.FullFOL]
subst_unused_range [lemma, in Completeness.FullFOL]
subst_unused_single [lemma, in Completeness.FullFOL]
subst_unused_form [lemma, in Completeness.FullFOL]
subst_unused_term [lemma, in Completeness.FullFOL]
subst_Weak [lemma, in Completeness.FullSequent]
subst1 [projection, in Completeness.unscoped]
Subst1 [record, in Completeness.unscoped]
subst1 [constructor, in Completeness.unscoped]
Subst1 [inductive, in Completeness.unscoped]
subst2 [projection, in Completeness.unscoped]
Subst2 [record, in Completeness.unscoped]
subst2 [constructor, in Completeness.unscoped]
Subst2 [inductive, in Completeness.unscoped]
subst3 [projection, in Completeness.unscoped]
Subst3 [record, in Completeness.unscoped]
subst3 [constructor, in Completeness.unscoped]
Subst3 [inductive, in Completeness.unscoped]
subst4 [projection, in Completeness.unscoped]
Subst4 [record, in Completeness.unscoped]
subst4 [constructor, in Completeness.unscoped]
Subst4 [inductive, in Completeness.unscoped]
subst5 [projection, in Completeness.unscoped]
Subst5 [record, in Completeness.unscoped]
subst5 [constructor, in Completeness.unscoped]
Subst5 [inductive, in Completeness.unscoped]
subs_sat' [lemma, in Completeness.GenTarski]
subs_sat [lemma, in Completeness.GenTarski]
subs_eval [lemma, in Completeness.GenTarski]
subs_interp_sat' [lemma, in Completeness.GenTarski]
subs_interp_sat [lemma, in Completeness.GenTarski]
subs_interp_eval [lemma, in Completeness.GenTarski]
subs_interp [definition, in Completeness.GenTarski]
subterm [inductive, in Completeness.FOL]
Subterm [section, in Completeness.FOL]
subterm_form [inductive, in Completeness.FOL]
↑ [notation, in Completeness.FOL]
sum_eq_dec [instance, in Completeness.Prelim]
svalid [definition, in Completeness.Sorensen]
svalid [definition, in Completeness.SDialogues]
svalid_dvalid [lemma, in Completeness.Sorensen]
swin_dwin [lemma, in Completeness.Sorensen]
swin_dwin_embed [definition, in Completeness.Sorensen]
swin_strat [inductive, in Completeness.Sorensen]
swin_strat [inductive, in Completeness.SDialogues]
switch_map [lemma, in Completeness.Enumeration]
SWS [constructor, in Completeness.Sorensen]
SWS [constructor, in Completeness.SDialogues]
Syntax [library]
s_sound [lemma, in Completeness.SDialogues]
T
TAbsurd [constructor, in Completeness.Gentzen]TAllE [constructor, in Completeness.Gentzen]
TAllI [constructor, in Completeness.Gentzen]
TAllL [constructor, in Completeness.Gentzen]
TAllR [constructor, in Completeness.Gentzen]
Tarski [section, in Completeness.GenTarski]
Tarski.Semantics [section, in Completeness.GenTarski]
Tarski.Semantics.domain [variable, in Completeness.GenTarski]
Tarski.Soundness [section, in Completeness.GenTarski]
Tarski.Substs [section, in Completeness.GenTarski]
Tarski.Substs.D [variable, in Completeness.GenTarski]
Tarski.Substs.I [variable, in Completeness.GenTarski]
_ ⊫M _ [notation, in Completeness.GenTarski]
_ ⊫E _ [notation, in Completeness.GenTarski]
_ ⊫S _ [notation, in Completeness.GenTarski]
_ ⊫< _ > _ [notation, in Completeness.GenTarski]
_ ⊨ _ [notation, in Completeness.GenTarski]
TAx [constructor, in Completeness.Gentzen]
TContr [constructor, in Completeness.Gentzen]
TCtx [constructor, in Completeness.Gentzen]
tembed [definition, in Completeness.Gentzen]
term [inductive, in Completeness.Syntax]
term [inductive, in Completeness.FullSyntax]
TExp [constructor, in Completeness.Gentzen]
theory [definition, in Completeness.FOL]
theory [definition, in Completeness.FullFOL]
TheoryManipulation [section, in Completeness.ND]
TIE [constructor, in Completeness.Gentzen]
TII [constructor, in Completeness.Gentzen]
TIL [constructor, in Completeness.Gentzen]
TIR [constructor, in Completeness.Gentzen]
tmap [definition, in Completeness.FOL]
tmap [definition, in Completeness.FullFOL]
tmap_contains_L [lemma, in Completeness.FOL]
tmap_contains_L [lemma, in Completeness.FullFOL]
Top [constructor, in Completeness.FullSyntax]
to_dec [lemma, in Completeness.Prelim]
tprv [definition, in Completeness.ND]
tprv [inductive, in Completeness.Gentzen]
tprv_list_T [lemma, in Completeness.ND]
TR [constructor, in Completeness.FullSequent]
True_eq_dec [instance, in Completeness.Prelim]
True_dec [instance, in Completeness.Prelim]
tsat [definition, in Completeness.Stability]
tsprv [inductive, in Completeness.Gentzen]
T_list_el [lemma, in Completeness.DecidableEnumerable]
T_list_cum [lemma, in Completeness.DecidableEnumerable]
T_list [definition, in Completeness.DecidableEnumerable]
T_prod_el [lemma, in Completeness.DecidableEnumerable]
T_prod_cum [lemma, in Completeness.DecidableEnumerable]
T_prod [definition, in Completeness.DecidableEnumerable]
T_nat_length [lemma, in Completeness.DecidableEnumerable]
T_nat_in [lemma, in Completeness.DecidableEnumerable]
T_ [definition, in Completeness.DecidableEnumerable]
U
uft_Func [constructor, in Completeness.FOL]uft_var [constructor, in Completeness.FOL]
uft_Func [constructor, in Completeness.FullFOL]
uft_var [constructor, in Completeness.FullFOL]
uf_All [constructor, in Completeness.FOL]
uf_Impl [constructor, in Completeness.FOL]
uf_Pred [constructor, in Completeness.FOL]
uf_Fal [constructor, in Completeness.FOL]
uf_Ex [constructor, in Completeness.FullFOL]
uf_All [constructor, in Completeness.FullFOL]
uf_O [constructor, in Completeness.FullFOL]
uf_A [constructor, in Completeness.FullFOL]
uf_I [constructor, in Completeness.FullFOL]
uf_Pred [constructor, in Completeness.FullFOL]
uf_Top [constructor, in Completeness.FullFOL]
uf_Fal [constructor, in Completeness.FullFOL]
union [definition, in Completeness.GenConstructions]
union_closed [lemma, in Completeness.GenConstructions]
union_econsistent [lemma, in Completeness.GenConstructions]
union_sub [lemma, in Completeness.GenConstructions]
union_f [lemma, in Completeness.GenConstructions]
unit_eq_dec [instance, in Completeness.Prelim]
universal_interp_eval [lemma, in Completeness.KripkeCompleteness]
universal_interp [instance, in Completeness.KripkeCompleteness]
unscoped [library]
unused [inductive, in Completeness.FOL]
unused [inductive, in Completeness.FullFOL]
unused_after_subst [lemma, in Completeness.FOL]
unused_after_subst_term [lemma, in Completeness.FOL]
unused_L [definition, in Completeness.FOL]
unused_term [inductive, in Completeness.FOL]
unused_L [definition, in Completeness.FullFOL]
unused_term [inductive, in Completeness.FullFOL]
upExt_term_term [definition, in Completeness.Syntax]
upExt_term_term [definition, in Completeness.FullSyntax]
upId_term_term [definition, in Completeness.Syntax]
upId_term_term [definition, in Completeness.FullSyntax]
Up_term_term [instance, in Completeness.Syntax]
up_term [projection, in Completeness.Syntax]
Up_term [record, in Completeness.Syntax]
up_term [constructor, in Completeness.Syntax]
Up_term [inductive, in Completeness.Syntax]
up_subst_subst_term_term [definition, in Completeness.Syntax]
up_term_term [definition, in Completeness.Syntax]
Up_term_term [instance, in Completeness.FullSyntax]
up_term [projection, in Completeness.FullSyntax]
Up_term [record, in Completeness.FullSyntax]
up_term [constructor, in Completeness.FullSyntax]
Up_term [inductive, in Completeness.FullSyntax]
up_subst_subst_term_term [definition, in Completeness.FullSyntax]
up_term_term [definition, in Completeness.FullSyntax]
up_term_term_pref_raise [lemma, in Completeness.FOL]
up_term_term_pref_ext_c' [lemma, in Completeness.FOL]
up_term_term_vsubs [lemma, in Completeness.FOL]
up_ren_ren [lemma, in Completeness.unscoped]
up_ren [definition, in Completeness.unscoped]
V
valid_T_fragment [lemma, in Completeness.GenCompleteness]valid_standard_expld_stability [lemma, in Completeness.GenCompleteness]
valid_T_model_bot [lemma, in Completeness.GenCompleteness]
valid_L_to_single [lemma, in Completeness.GenTarski]
valid_L_valid_T [lemma, in Completeness.GenTarski]
valid_T_standard_dm [lemma, in Completeness.GenTarski]
valid_T_subsumption [lemma, in Completeness.GenTarski]
valid_L [definition, in Completeness.GenTarski]
valid_T [definition, in Completeness.GenTarski]
Var [record, in Completeness.unscoped]
Var [inductive, in Completeness.unscoped]
variant [projection, in Completeness.GenConstructions]
VarInstance_term [instance, in Completeness.Syntax]
VarInstance_term [instance, in Completeness.FullSyntax]
varL_term [lemma, in Completeness.Syntax]
varL_term [lemma, in Completeness.FullSyntax]
var_term [constructor, in Completeness.Syntax]
var_term [constructor, in Completeness.FullSyntax]
var_zero [definition, in Completeness.unscoped]
vCons [constructor, in Completeness.SDialogues]
vecs_from_correct [lemma, in Completeness.FOL]
vecs_from [definition, in Completeness.FOL]
vec_comp [definition, in Completeness.axioms]
vec_id [definition, in Completeness.axioms]
vec_ext [definition, in Completeness.axioms]
vec_forall_cml [lemma, in Completeness.FOL]
vec_forall_map [lemma, in Completeness.FOL]
vec_map_ext [lemma, in Completeness.FOL]
vec_unused [lemma, in Completeness.FOL]
vec_inS [constructor, in Completeness.FOL]
vec_inB [constructor, in Completeness.FOL]
vec_in [inductive, in Completeness.FOL]
vec_forall_map [lemma, in Completeness.FullFOL]
vec_map_ext [lemma, in Completeness.FullFOL]
vec_unused [lemma, in Completeness.FullFOL]
vec_inS [constructor, in Completeness.FullFOL]
vec_inB [constructor, in Completeness.FullFOL]
vec_in [inductive, in Completeness.FullFOL]
venv [definition, in Completeness.GenTarski]
venv_empty [lemma, in Completeness.GenTarski]
venv_sat [lemma, in Completeness.GenTarski]
vix [definition, in Completeness.SDialogues]
vmap [definition, in Completeness.SDialogues]
vNil [constructor, in Completeness.SDialogues]
vsubs [definition, in Completeness.FOL]
vsubs_single_subst [lemma, in Completeness.ND]
vsubs_form_shift [lemma, in Completeness.ND]
W
Weak [lemma, in Completeness.ND]Weak [constructor, in Completeness.FullSequent]
weaken [lemma, in Completeness.FullSequent]
Weak_T [lemma, in Completeness.ND]
other
[ _ ] (fscope) [notation, in Completeness.Syntax][ _ ] (fscope) [notation, in Completeness.Syntax]
⟨ _ ; _ ⟩ (fscope) [notation, in Completeness.unscoped]
⟨ _ ⟩ (fscope) [notation, in Completeness.unscoped]
_ [ _ ] (subst_scope) [notation, in Completeness.Syntax]
_ [ _ ] (subst_scope) [notation, in Completeness.Syntax]
↑__term (subst_scope) [notation, in Completeness.Syntax]
↑__term (subst_scope) [notation, in Completeness.Syntax]
var (subst_scope) [notation, in Completeness.Syntax]
_ __term (subst_scope) [notation, in Completeness.Syntax]
_ __term (subst_scope) [notation, in Completeness.Syntax]
_ [ _ ] (subst_scope) [notation, in Completeness.FullSyntax]
_ [ _ ] (subst_scope) [notation, in Completeness.FullSyntax]
↑__term (subst_scope) [notation, in Completeness.FullSyntax]
↑__term (subst_scope) [notation, in Completeness.FullSyntax]
var (subst_scope) [notation, in Completeness.FullSyntax]
_ __term (subst_scope) [notation, in Completeness.FullSyntax]
_ __term (subst_scope) [notation, in Completeness.FullSyntax]
_ .. (subst_scope) [notation, in Completeness.unscoped]
_ >> _ (subst_scope) [notation, in Completeness.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in Completeness.unscoped]
_ [ _ ] (subst_scope) [notation, in Completeness.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in Completeness.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in Completeness.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in Completeness.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Completeness.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in Completeness.unscoped]
_ ⊢D _ [notation, in Completeness.Sorensen]
_ o:: _ [notation, in Completeness.Sorensen]
_ ⊩IE _ [notation, in Completeness.ND]
_ ⊩CL _ [notation, in Completeness.ND]
_ ⊩CE _ [notation, in Completeness.ND]
_ ⊩( _ , _ ) _ [notation, in Completeness.ND]
_ ⊩ _ [notation, in Completeness.ND]
_ ⊢IE _ [notation, in Completeness.ND]
_ ⊢CL _ [notation, in Completeness.ND]
_ ⊢CE _ [notation, in Completeness.ND]
_ ⊢( _ , _ ) _ [notation, in Completeness.ND]
_ ⊢ _ [notation, in Completeness.ND]
_ o:: _ [notation, in Completeness.SDialogues]
_ ⊩SE _ [notation, in Completeness.Gentzen]
_ ;; _ ⊢sL _ [notation, in Completeness.Gentzen]
_ ⊢SL _ [notation, in Completeness.Gentzen]
_ ;; _ ⊢sE _ [notation, in Completeness.Gentzen]
_ ⊢SE _ [notation, in Completeness.Gentzen]
_ ;; _ ⊢s _ [notation, in Completeness.Gentzen]
_ ⊢S _ [notation, in Completeness.Gentzen]
_ === _ [notation, in Completeness.Prelim]
_ <<= _ [notation, in Completeness.Prelim]
_ el _ [notation, in Completeness.Prelim]
_ <<= _ [notation, in Completeness.Prelim]
_ el _ [notation, in Completeness.Prelim]
_ ⟹ _ [notation, in Completeness.FOL]
_ ⋄ _ [notation, in Completeness.FOL]
_ ∈ _ [notation, in Completeness.FOL]
_ ⊑ _ [notation, in Completeness.FOL]
_ ⊏ _ [notation, in Completeness.FOL]
_ --> _ [notation, in Completeness.FOL]
_ .: _ [notation, in Completeness.unscoped]
_ ⊫M _ [notation, in Completeness.GenTarski]
_ ⊫E _ [notation, in Completeness.GenTarski]
_ ⊫S _ [notation, in Completeness.GenTarski]
_ ⊫< _ > _ [notation, in Completeness.GenTarski]
_ ⊨ _ [notation, in Completeness.GenTarski]
_ ⋄ _ [notation, in Completeness.FullFOL]
_ ∈ _ [notation, in Completeness.FullFOL]
_ ⊑ _ [notation, in Completeness.FullFOL]
_ ⊏ _ [notation, in Completeness.FullFOL]
_ ∨ _ [notation, in Completeness.FullFOL]
_ ∧ _ [notation, in Completeness.FullFOL]
_ --> _ [notation, in Completeness.FullFOL]
_ ⊫KBL _ [notation, in Completeness.Kripke]
_ ⊫KS _ [notation, in Completeness.Kripke]
_ ⊫KE _ [notation, in Completeness.Kripke]
_ ⊨( _ , _ ) _ [notation, in Completeness.Kripke]
_ ⊨( _ ) _ [notation, in Completeness.Kripke]
_ ⊢f _ [notation, in Completeness.FullSequent]
eq_dec _ [notation, in Completeness.Prelim]
( _ × _ × .. × _ ) [notation, in Completeness.Prelim]
[ _ | _ ∈ _ ] [notation, in Completeness.Prelim]
[ _ | _ ∈ _ , _ ] [notation, in Completeness.Prelim]
| _ | [notation, in Completeness.Prelim]
| _ | [notation, in Completeness.Prelim]
↑ [notation, in Completeness.FOL]
↑ [notation, in Completeness.unscoped]
↑ [notation, in Completeness.FullFOL]
∀ _ [notation, in Completeness.FOL]
∀ _ [notation, in Completeness.FullFOL]
∃ _ [notation, in Completeness.FOL]
∃ _ [notation, in Completeness.FullFOL]
⊤ [notation, in Completeness.FullFOL]
⊥ [notation, in Completeness.FOL]
⊥ [notation, in Completeness.FullFOL]
⋁ _ [notation, in Completeness.FullSequent]
¬ _ [notation, in Completeness.FOL]
¬ _ [notation, in Completeness.FullFOL]
Notation Index
F
_ ⋄ _ [in Completeness.FOL]_ ∈ _ [in Completeness.FOL]
_ ⊑ _ [in Completeness.FOL]
_ ⊏ _ [in Completeness.FOL]
_ ⋄ _ [in Completeness.FullFOL]
_ ∈ _ [in Completeness.FullFOL]
_ ⊑ _ [in Completeness.FullFOL]
_ ⊏ _ [in Completeness.FullFOL]
↑ [in Completeness.FullFOL]
_ ⊢f _ [in Completeness.FullSequent]
⋁ _ [in Completeness.FullSequent]
G
_ ∘ _ [in Completeness.GenConstructions]_ ⊩G _ [in Completeness.GenConstructions]
_ ⊢G _ [in Completeness.GenConstructions]
∃ _ [in Completeness.GenConstructions]
⊥ [in Completeness.GenConstructions]
¬ _ [in Completeness.GenConstructions]
_ ;; _ ⊢s _ [in Completeness.Gentzen]
_ ⊢S _ [in Completeness.Gentzen]
K
_ ;; _ ⊢sC _ [in Completeness.KripkeCompleteness]_ ⊢SC _ [in Completeness.KripkeCompleteness]
_ <<=C _ [in Completeness.KripkeCompleteness]
_ ⊨( _ , _ ) _ [in Completeness.Kripke]
_ ⊨( _ ) _ [in Completeness.Kripke]
L
_ ⊢D _ [in Completeness.Sorensen]N
_ ⊩IE _ [in Completeness.ND]_ ⊩CL _ [in Completeness.ND]
_ ⊩CE _ [in Completeness.ND]
_ ⊩( _ , _ ) _ [in Completeness.ND]
_ ⊩ _ [in Completeness.ND]
_ ⊢IE _ [in Completeness.ND]
_ ⊢CL _ [in Completeness.ND]
_ ⊢CE _ [in Completeness.ND]
_ ⊢( _ , _ ) _ [in Completeness.ND]
_ ⊢ _ [in Completeness.ND]
S
_ ⊢D _ [in Completeness.SDialogues]↑ [in Completeness.FOL]
T
_ ⊫M _ [in Completeness.GenTarski]_ ⊫E _ [in Completeness.GenTarski]
_ ⊫S _ [in Completeness.GenTarski]
_ ⊫< _ > _ [in Completeness.GenTarski]
_ ⊨ _ [in Completeness.GenTarski]
other
[ _ ] (fscope) [in Completeness.Syntax][ _ ] (fscope) [in Completeness.Syntax]
⟨ _ ; _ ⟩ (fscope) [in Completeness.unscoped]
⟨ _ ⟩ (fscope) [in Completeness.unscoped]
_ [ _ ] (subst_scope) [in Completeness.Syntax]
_ [ _ ] (subst_scope) [in Completeness.Syntax]
↑__term (subst_scope) [in Completeness.Syntax]
↑__term (subst_scope) [in Completeness.Syntax]
var (subst_scope) [in Completeness.Syntax]
_ __term (subst_scope) [in Completeness.Syntax]
_ __term (subst_scope) [in Completeness.Syntax]
_ [ _ ] (subst_scope) [in Completeness.FullSyntax]
_ [ _ ] (subst_scope) [in Completeness.FullSyntax]
↑__term (subst_scope) [in Completeness.FullSyntax]
↑__term (subst_scope) [in Completeness.FullSyntax]
var (subst_scope) [in Completeness.FullSyntax]
_ __term (subst_scope) [in Completeness.FullSyntax]
_ __term (subst_scope) [in Completeness.FullSyntax]
_ .. (subst_scope) [in Completeness.unscoped]
_ >> _ (subst_scope) [in Completeness.unscoped]
_ [ _ ; _ ] (subst_scope) [in Completeness.unscoped]
_ [ _ ] (subst_scope) [in Completeness.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in Completeness.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in Completeness.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in Completeness.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Completeness.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in Completeness.unscoped]
_ ⊢D _ [in Completeness.Sorensen]
_ o:: _ [in Completeness.Sorensen]
_ ⊩IE _ [in Completeness.ND]
_ ⊩CL _ [in Completeness.ND]
_ ⊩CE _ [in Completeness.ND]
_ ⊩( _ , _ ) _ [in Completeness.ND]
_ ⊩ _ [in Completeness.ND]
_ ⊢IE _ [in Completeness.ND]
_ ⊢CL _ [in Completeness.ND]
_ ⊢CE _ [in Completeness.ND]
_ ⊢( _ , _ ) _ [in Completeness.ND]
_ ⊢ _ [in Completeness.ND]
_ o:: _ [in Completeness.SDialogues]
_ ⊩SE _ [in Completeness.Gentzen]
_ ;; _ ⊢sL _ [in Completeness.Gentzen]
_ ⊢SL _ [in Completeness.Gentzen]
_ ;; _ ⊢sE _ [in Completeness.Gentzen]
_ ⊢SE _ [in Completeness.Gentzen]
_ ;; _ ⊢s _ [in Completeness.Gentzen]
_ ⊢S _ [in Completeness.Gentzen]
_ === _ [in Completeness.Prelim]
_ <<= _ [in Completeness.Prelim]
_ el _ [in Completeness.Prelim]
_ <<= _ [in Completeness.Prelim]
_ el _ [in Completeness.Prelim]
_ ⟹ _ [in Completeness.FOL]
_ ⋄ _ [in Completeness.FOL]
_ ∈ _ [in Completeness.FOL]
_ ⊑ _ [in Completeness.FOL]
_ ⊏ _ [in Completeness.FOL]
_ --> _ [in Completeness.FOL]
_ .: _ [in Completeness.unscoped]
_ ⊫M _ [in Completeness.GenTarski]
_ ⊫E _ [in Completeness.GenTarski]
_ ⊫S _ [in Completeness.GenTarski]
_ ⊫< _ > _ [in Completeness.GenTarski]
_ ⊨ _ [in Completeness.GenTarski]
_ ⋄ _ [in Completeness.FullFOL]
_ ∈ _ [in Completeness.FullFOL]
_ ⊑ _ [in Completeness.FullFOL]
_ ⊏ _ [in Completeness.FullFOL]
_ ∨ _ [in Completeness.FullFOL]
_ ∧ _ [in Completeness.FullFOL]
_ --> _ [in Completeness.FullFOL]
_ ⊫KBL _ [in Completeness.Kripke]
_ ⊫KS _ [in Completeness.Kripke]
_ ⊫KE _ [in Completeness.Kripke]
_ ⊨( _ , _ ) _ [in Completeness.Kripke]
_ ⊨( _ ) _ [in Completeness.Kripke]
_ ⊢f _ [in Completeness.FullSequent]
eq_dec _ [in Completeness.Prelim]
( _ × _ × .. × _ ) [in Completeness.Prelim]
[ _ | _ ∈ _ ] [in Completeness.Prelim]
[ _ | _ ∈ _ , _ ] [in Completeness.Prelim]
| _ | [in Completeness.Prelim]
| _ | [in Completeness.Prelim]
↑ [in Completeness.FOL]
↑ [in Completeness.unscoped]
↑ [in Completeness.FullFOL]
∀ _ [in Completeness.FOL]
∀ _ [in Completeness.FullFOL]
∃ _ [in Completeness.FOL]
∃ _ [in Completeness.FullFOL]
⊤ [in Completeness.FullFOL]
⊥ [in Completeness.FOL]
⊥ [in Completeness.FullFOL]
⋁ _ [in Completeness.FullSequent]
¬ _ [in Completeness.FOL]
¬ _ [in Completeness.FullFOL]
Variable Index
C
ClosingValidity.C [in Completeness.GenTarski]ClosingValidity.HC [in Completeness.GenTarski]
ClosingValidity.Hprv [in Completeness.GenTarski]
ClosingValidity.phi [in Completeness.GenTarski]
ClosingValidity.T [in Completeness.GenTarski]
Completeness.BotModel.T [in Completeness.GenCompleteness]
Completeness.BotModel.T_closed [in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.Hphi [in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.HT [in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.phi [in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes.T [in Completeness.GenCompleteness]
Completeness.FragmentModel.GBot [in Completeness.GenCompleteness]
Completeness.FragmentModel.GBot_closed [in Completeness.GenCompleteness]
Completeness.FragmentModel.T [in Completeness.GenCompleteness]
Completeness.FragmentModel.T_closed [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.He [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.Hphi [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.HT [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.L [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.mp [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.phi [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness.T [in Completeness.GenCompleteness]
Completeness.StandardCompletenes.Hphi [in Completeness.GenCompleteness]
Completeness.StandardCompletenes.HT [in Completeness.GenCompleteness]
Completeness.StandardCompletenes.phi [in Completeness.GenCompleteness]
Completeness.StandardCompletenes.T [in Completeness.GenCompleteness]
Consistency.Classical.XM [in Completeness.Consistency]
D
DGame.f [in Completeness.Sorensen]DGame.R [in Completeness.Sorensen]
DialogFull.eq_dec_Preds [in Completeness.DialogFull]
DialogFull.eq_dec_Funcs [in Completeness.DialogFull]
E
EGame.f [in Completeness.Sorensen]EGame.R [in Completeness.Sorensen]
Enumerability.enum_Preds [in Completeness.FOL]
Enumerability.enum_Funcs [in Completeness.FOL]
enumerable_list.fixL.LX [in Completeness.DecidableEnumerable]
enumerable_list.X [in Completeness.DecidableEnumerable]
enumerable_prod.fixLs.L_Y [in Completeness.DecidableEnumerable]
enumerable_prod.fixLs.L_X [in Completeness.DecidableEnumerable]
enumerable_prod.Y [in Completeness.DecidableEnumerable]
enumerable_prod.X [in Completeness.DecidableEnumerable]
enumerable_enum.e [in Completeness.DecidableEnumerable]
enumerable_enum.p [in Completeness.DecidableEnumerable]
enumerable_enum.X [in Completeness.DecidableEnumerable]
Enumeration.Hlen [in Completeness.Enumeration]
Enumeration.X [in Completeness.Enumeration]
EqDec.eq_dec_Preds [in Completeness.FOL]
EqDec.eq_dec_Funcs [in Completeness.FOL]
EqDec.eq_dec_Preds [in Completeness.FullFOL]
EqDec.eq_dec_Funcs [in Completeness.FullFOL]
Equi.X [in Completeness.Prelim]
F
Filter.X [in Completeness.Prelim]G
GenCons.Explosion.e [in Completeness.GenConstructions]GenCons.Explosion.Hclosed [in Completeness.GenConstructions]
GenCons.Explosion.He [in Completeness.GenConstructions]
GenCons.Explosion.T [in Completeness.GenConstructions]
GenCons.GBot [in Completeness.GenConstructions]
GenCons.GBot_closed [in Completeness.GenConstructions]
GenCons.Henkin.e [in Completeness.GenConstructions]
GenCons.Henkin.Hclosed [in Completeness.GenConstructions]
GenCons.Henkin.He [in Completeness.GenConstructions]
GenCons.Henkin.Hexp [in Completeness.GenConstructions]
GenCons.Henkin.Hunused [in Completeness.GenConstructions]
GenCons.Henkin.T [in Completeness.GenConstructions]
GenCons.Omega.e [in Completeness.GenConstructions]
GenCons.Omega.He [in Completeness.GenConstructions]
GenCons.Omega.Hexp [in Completeness.GenConstructions]
GenCons.Omega.Hhenkin [in Completeness.GenConstructions]
GenCons.Omega.T [in Completeness.GenConstructions]
GenCons.Union.econsistent_f [in Completeness.GenConstructions]
GenCons.Union.f [in Completeness.GenConstructions]
GenCons.Union.f_le [in Completeness.GenConstructions]
I
Inclusion.X [in Completeness.Prelim]K
KripkeCompleteness.MPRequired.C [in Completeness.KripkeCompleteness]KripkeCompleteness.MPRequired.HC [in Completeness.KripkeCompleteness]
KripkeCompleteness.MPRequired.K_completeness [in Completeness.KripkeCompleteness]
KripkeCompleteness.StandardCompleteness.sprv_stab [in Completeness.KripkeCompleteness]
Kripke.Model.domain [in Completeness.Kripke]
Kripke.Model.M [in Completeness.Kripke]
Kripke.Substs.D [in Completeness.Kripke]
L
LJD.f [in Completeness.Sorensen]LJD.R [in Completeness.Sorensen]
L_T_unused.enum_Preds [in Completeness.Enumeration]
L_T_unused.enum_Funcs [in Completeness.Enumeration]
M
Membership.X [in Completeness.Prelim]N
neList.B [in Completeness.Prelim]neList.P [in Completeness.Prelim]
neList.S [in Completeness.Prelim]
neList.X [in Completeness.Prelim]
P
Positions.d [in Completeness.Prelim]Positions.X [in Completeness.Prelim]
R
Removal.X [in Completeness.Prelim]S
SDialogues.enum_def [in Completeness.SDialogues]SDialogues.enum_att [in Completeness.SDialogues]
SDialogues.f [in Completeness.SDialogues]
SDialogues.olt [in Completeness.SDialogues]
SDialogues.oplus [in Completeness.SDialogues]
SDialogues.ord [in Completeness.SDialogues]
SDialogues.ord_ind [in Completeness.SDialogues]
SDialogues.osuc [in Completeness.SDialogues]
SDialogues.osup [in Completeness.SDialogues]
SDialogues.ozero [in Completeness.SDialogues]
SDialogues.R [in Completeness.SDialogues]
SGame.f [in Completeness.Sorensen]
SGame.R [in Completeness.Sorensen]
SigExt.D [in Completeness.GenTarski]
SigExt.F [in Completeness.GenTarski]
SigExt.F_ar [in Completeness.GenTarski]
SigExt.P [in Completeness.GenTarski]
SigExt.P_ar [in Completeness.GenTarski]
StabilityClasses.SyntMP.MPEnum.HL [in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.HX [in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.L [in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.mp [in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.P [in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum.X [in Completeness.Stability]
T
Tarski.Semantics.domain [in Completeness.GenTarski]Tarski.Substs.D [in Completeness.GenTarski]
Tarski.Substs.I [in Completeness.GenTarski]
Library Index
A
axiomsC
ConsistencyD
DecidableEnumerableDialogFragment
DialogFull
E
EnumerationF
FOLFullFOL
FullSequent
FullSyntax
G
GenCompletenessGenConstructions
GenTarski
Gentzen
K
KripkeKripkeCompleteness
N
NDP
PrelimS
SDialoguesSorensen
Stability
Syntax
U
unscopedLemma Index
A
any_T_map_closed [in Completeness.Stability]app_incl_R [in Completeness.Prelim]
app_incl_l [in Completeness.Prelim]
atomic_dec [in Completeness.DialogFull]
atomic_dec [in Completeness.DialogFragment]
attack_form_inv_ext [in Completeness.DialogFull]
attack_form_inv_all [in Completeness.DialogFull]
attack_form_inv_or [in Completeness.DialogFull]
attack_form_inv_and [in Completeness.DialogFull]
attack_form_inv_impl [in Completeness.DialogFull]
attack_form_inv_all [in Completeness.DialogFragment]
attack_form_inv_impl [in Completeness.DialogFragment]
AXM [in Completeness.ND]
B
big_imp_extract [in Completeness.ND]big_imp_valid_L [in Completeness.GenTarski]
BL_E_subsumption [in Completeness.GenTarski]
bool_Prop_false [in Completeness.Prelim]
bool_Prop_true [in Completeness.Prelim]
C
capture_extract [in Completeness.ND]capture_captures [in Completeness.FOL]
cend_dn [in Completeness.KripkeCompleteness]
cfind [in Completeness.Prelim]
closed_T_extend [in Completeness.FOL]
closed_T_extend [in Completeness.FullFOL]
close_extract [in Completeness.ND]
close_closed [in Completeness.FOL]
close_valid_L [in Completeness.GenTarski]
compComp_form [in Completeness.Syntax]
compComp_term [in Completeness.Syntax]
compComp_form [in Completeness.FullSyntax]
compComp_term [in Completeness.FullSyntax]
compComp'_form [in Completeness.Syntax]
compComp'_term [in Completeness.Syntax]
compComp'_form [in Completeness.FullSyntax]
compComp'_term [in Completeness.FullSyntax]
completeness_expl [in Completeness.GenCompleteness]
completeness_standard_stability [in Completeness.GenCompleteness]
Consistency [in Completeness.GenTarski]
consistency_inheritance [in Completeness.Consistency]
consistent_join_step [in Completeness.GenConstructions]
consistent_max_out2 [in Completeness.Consistency]
consistent_max_impl [in Completeness.Consistency]
consistent_max_out [in Completeness.Consistency]
consistent_neg2 [in Completeness.Consistency]
consistent_neg [in Completeness.Consistency]
consistent_prv [in Completeness.Consistency]
construct_construction [in Completeness.GenConstructions]
cons_incl [in Completeness.Prelim]
contains_extend3 [in Completeness.FOL]
contains_extend2 [in Completeness.FOL]
contains_extend1 [in Completeness.FOL]
contains_app [in Completeness.FOL]
contains_cons2 [in Completeness.FOL]
contains_cons [in Completeness.FOL]
contains_nil [in Completeness.FOL]
contains_extend3 [in Completeness.FullFOL]
contains_extend2 [in Completeness.FullFOL]
contains_extend1 [in Completeness.FullFOL]
contains_app [in Completeness.FullFOL]
contains_cons2 [in Completeness.FullFOL]
contains_cons [in Completeness.FullFOL]
contains_nil [in Completeness.FullFOL]
context_shift [in Completeness.FullSequent]
con_T_correct [in Completeness.Stability]
count_nat [in Completeness.DecidableEnumerable]
count_bool [in Completeness.DecidableEnumerable]
count_enum' [in Completeness.DecidableEnumerable]
ctx_in [in Completeness.FullSequent]
ctx_out [in Completeness.FullSequent]
cum_ge' [in Completeness.DecidableEnumerable]
cum_ge [in Completeness.DecidableEnumerable]
cutfree_seq_ND [in Completeness.Gentzen]
cycle_shift_subject [in Completeness.ND]
cycle_shift_shift [in Completeness.ND]
cycle_shift_subject [in Completeness.FullSequent]
cycle_shift_shift [in Completeness.FullSequent]
C_longenough [in Completeness.DecidableEnumerable]
C_exhaustive [in Completeness.DecidableEnumerable]
D
dcompleteness [in Completeness.Sorensen]decidable_iff [in Completeness.DecidableEnumerable]
dec_count_enum' [in Completeness.DecidableEnumerable]
dec_count_enum [in Completeness.DecidableEnumerable]
dec_disj [in Completeness.DecidableEnumerable]
dec_conj [in Completeness.DecidableEnumerable]
dec_compl [in Completeness.DecidableEnumerable]
dec_decidable' [in Completeness.DecidableEnumerable]
dec_transfer [in Completeness.Prelim]
dec_DM_impl [in Completeness.Prelim]
dec_DM_and [in Completeness.Prelim]
dec_DN [in Completeness.Prelim]
Dec_false [in Completeness.Prelim]
Dec_true [in Completeness.Prelim]
Dec_auto_not [in Completeness.Prelim]
Dec_auto [in Completeness.Prelim]
Dec_reflect_eq [in Completeness.Prelim]
Dec_reflect [in Completeness.Prelim]
dec_vec_in [in Completeness.FOL]
dec_vec_in [in Completeness.FullFOL]
discrete_list [in Completeness.DecidableEnumerable]
discrete_option [in Completeness.DecidableEnumerable]
discrete_sum [in Completeness.DecidableEnumerable]
discrete_prod [in Completeness.DecidableEnumerable]
discrete_nat_nat [in Completeness.DecidableEnumerable]
discrete_nat [in Completeness.DecidableEnumerable]
discrete_bool [in Completeness.DecidableEnumerable]
discrete_iff [in Completeness.DecidableEnumerable]
disjoint_app [in Completeness.Prelim]
disjoint_cons [in Completeness.Prelim]
disjoint_nil' [in Completeness.Prelim]
disjoint_nil [in Completeness.Prelim]
disjoint_incl [in Completeness.Prelim]
disjoint_symm [in Completeness.Prelim]
disjoint_forall [in Completeness.Prelim]
DN [in Completeness.ND]
dnt_to_TCE [in Completeness.ND]
dnt_to_CE [in Completeness.ND]
dnt_remove_ctx [in Completeness.ND]
dnt_CE [in Completeness.ND]
dnt_to_TIE [in Completeness.ND]
dnt_to_IE [in Completeness.ND]
dnt_float [in Completeness.ND]
dnt_subst [in Completeness.ND]
dn_to_sta [in Completeness.Stability]
DN_T [in Completeness.ND]
dn_inherit [in Completeness.GenCompleteness]
DP [in Completeness.ND]
Dprv_just [in Completeness.Sorensen]
Dprv_ax [in Completeness.Sorensen]
Dprv_echo [in Completeness.Sorensen]
Dprv_exp [in Completeness.Sorensen]
Dprv_defend [in Completeness.Sorensen]
Dprv_weak [in Completeness.Sorensen]
Dprv_ewin [in Completeness.Sorensen]
Dprv_fprv [in Completeness.DialogFull]
Dprv_fprv' [in Completeness.DialogFull]
Dprv_ND [in Completeness.DialogFragment]
droppable_BL [in Completeness.GenTarski]
droppable_E [in Completeness.GenTarski]
droppable_S [in Completeness.GenTarski]
droppable_exploding_bot [in Completeness.GenTarski]
droppable_standard_bot [in Completeness.GenTarski]
droppable_classical [in Completeness.GenTarski]
drop_interp'_sat [in Completeness.GenTarski]
drop_interp'_eval [in Completeness.GenTarski]
dummy_SM [in Completeness.GenTarski]
dummy_xm [in Completeness.GenTarski]
dwin_Dprv [in Completeness.Sorensen]
E
ecompleteness [in Completeness.Sorensen]econsistency_trans [in Completeness.GenConstructions]
econsistency_inheritance [in Completeness.GenConstructions]
econsistent_prv [in Completeness.GenConstructions]
econsistent_Omega [in Completeness.GenConstructions]
econsistent_join_sub [in Completeness.GenConstructions]
elem_prv [in Completeness.ND]
el_at_pos [in Completeness.Enumeration]
el_pos [in Completeness.Prelim]
enumerable_conj [in Completeness.DecidableEnumerable]
enumerable_disj [in Completeness.DecidableEnumerable]
enumerable__T_list [in Completeness.DecidableEnumerable]
enumerable__T_option [in Completeness.DecidableEnumerable]
enumerable__T_sum [in Completeness.DecidableEnumerable]
enumerable__T_prod [in Completeness.DecidableEnumerable]
enumerable_enum [in Completeness.DecidableEnumerable]
enumerable_nat_nat [in Completeness.DecidableEnumerable]
enumerable_enumerable_T [in Completeness.DecidableEnumerable]
enumeration_stability [in Completeness.Stability]
enumeration_semi_decidable [in Completeness.Stability]
enum_tsat_T [in Completeness.Stability]
enum_T_map_closed_homo [in Completeness.Stability]
enum_T_map_closed_closing [in Completeness.Stability]
enum_tprv [in Completeness.ND]
enum_containsL [in Completeness.ND]
enum_p [in Completeness.ND]
enum_el [in Completeness.ND]
enum_prv [in Completeness.ND]
enum_enumT [in Completeness.DecidableEnumerable]
enum_count [in Completeness.DecidableEnumerable]
enum_to_cumulative [in Completeness.DecidableEnumerable]
enum_stprv [in Completeness.Gentzen]
enum_sprv [in Completeness.Gentzen]
enum_tmap [in Completeness.FOL]
enum_tmap [in Completeness.FullFOL]
equi_rotate [in Completeness.Prelim]
equi_shift [in Completeness.Prelim]
equi_swap [in Completeness.Prelim]
equi_dup [in Completeness.Prelim]
equi_push [in Completeness.Prelim]
eq_incl [in Completeness.DialogFull]
eq_incl [in Completeness.DialogFragment]
esoundsess [in Completeness.Sorensen]
eval_ident_fragment [in Completeness.GenCompleteness]
eval_ident [in Completeness.GenCompleteness]
eval_comp [in Completeness.GenTarski]
eval_ext [in Completeness.GenTarski]
ewin_Dprv [in Completeness.Sorensen]
ExE [in Completeness.ND]
ExI [in Completeness.ND]
exploding_inherit [in Completeness.GenConstructions]
Exp_exploding [in Completeness.GenConstructions]
Exp_closed [in Completeness.GenConstructions]
Exp_econsistent [in Completeness.GenConstructions]
Exp_sub [in Completeness.GenConstructions]
exp_axiom_lift [in Completeness.GenConstructions]
ext_c'_unused [in Completeness.FOL]
ext_c'_unused_term [in Completeness.FOL]
E_S_subsumption [in Completeness.GenTarski]
F
filter_comm [in Completeness.Prelim]filter_and [in Completeness.Prelim]
filter_pq_eq [in Completeness.Prelim]
filter_pq_mono [in Completeness.Prelim]
filter_fst' [in Completeness.Prelim]
filter_fst [in Completeness.Prelim]
filter_app [in Completeness.Prelim]
filter_id [in Completeness.Prelim]
filter_mono [in Completeness.Prelim]
filter_incl [in Completeness.Prelim]
find_unused_L [in Completeness.FOL]
find_unused [in Completeness.FOL]
find_unused_term [in Completeness.FOL]
find_unused_L [in Completeness.FullFOL]
find_unused [in Completeness.FullFOL]
find_unused_term [in Completeness.FullFOL]
fin_T_to_context [in Completeness.Stability]
fin_T_con_T [in Completeness.Stability]
fin_T_map_closed [in Completeness.Stability]
flat_map_app [in Completeness.Enumeration]
focus_el [in Completeness.FullSequent]
form_enum_fresh [in Completeness.Enumeration]
form_enum_enumerates [in Completeness.Enumeration]
fprv_defend [in Completeness.DialogFull]
fprv_Dprv [in Completeness.DialogFull]
G
GDN [in Completeness.GenConstructions]GDP [in Completeness.GenConstructions]
GExE [in Completeness.GenConstructions]
GExI [in Completeness.GenConstructions]
GExp [in Completeness.GenConstructions]
GXM [in Completeness.GenConstructions]
H
Henkin_T [in Completeness.GenConstructions]Henkin_is_Henkin [in Completeness.GenConstructions]
Henkin_consistent [in Completeness.GenConstructions]
henkin_le [in Completeness.GenConstructions]
henkin_unused [in Completeness.GenConstructions]
henkin_axiom_unused [in Completeness.GenConstructions]
I
IE_to_CE [in Completeness.ND]incl_app_left [in Completeness.Prelim]
incl_lrcons [in Completeness.Prelim]
incl_rcons [in Completeness.Prelim]
incl_lcons [in Completeness.Prelim]
incl_shift [in Completeness.Prelim]
incl_nil_eq [in Completeness.Prelim]
incl_map [in Completeness.Prelim]
incl_sing [in Completeness.Prelim]
incl_nil [in Completeness.Prelim]
inconsistent [in Completeness.Consistency]
instId_form [in Completeness.Syntax]
instId_term [in Completeness.Syntax]
instId_form [in Completeness.FullSyntax]
instId_term [in Completeness.FullSyntax]
in_rem_iff [in Completeness.Prelim]
in_filter_iff [in Completeness.Prelim]
in_concat_iff [in Completeness.Prelim]
in_cons_neq [in Completeness.Prelim]
in_sing [in Completeness.Prelim]
in_omap_iff [in Completeness.Prelim]
is_Henkin_inherit [in Completeness.GenConstructions]
J
justified_weak [in Completeness.Sorensen]justified_weak [in Completeness.SDialogues]
K
ksat_comp [in Completeness.Kripke]ksat_ext [in Completeness.Kripke]
ksat_iff [in Completeness.Kripke]
ksat_mon [in Completeness.Kripke]
ksemantic_explosion [in Completeness.Kripke]
ksoundness [in Completeness.Kripke]
ksoundness_seq [in Completeness.Gentzen]
kstandard_explodes [in Completeness.Kripke]
kvalid_L_subs [in Completeness.Kripke]
K_std_seq_ksoundness [in Completeness.KripkeCompleteness]
K_std_completeness [in Completeness.KripkeCompleteness]
K_std_standard [in Completeness.KripkeCompleteness]
K_std_ksat [in Completeness.KripkeCompleteness]
K_std_sprv [in Completeness.KripkeCompleteness]
K_std_correct [in Completeness.KripkeCompleteness]
K_bottomless_completeness [in Completeness.KripkeCompleteness]
K_exp_seq_ksoundness [in Completeness.KripkeCompleteness]
K_exp_completeness [in Completeness.KripkeCompleteness]
K_ctx_exploding [in Completeness.KripkeCompleteness]
K_ctx_ksat [in Completeness.KripkeCompleteness]
K_ctx_sprv [in Completeness.KripkeCompleteness]
K_ctx_correct [in Completeness.KripkeCompleteness]
L
lift_ext_c_closes_T [in Completeness.FOL]lift_ext_c_closes [in Completeness.FOL]
lift_drop_inverse [in Completeness.FOL]
lift_drop_inverse' [in Completeness.FOL]
lift_drop_inverse_term' [in Completeness.FOL]
lift_interp_sat [in Completeness.GenTarski]
lift_interp_eval [in Completeness.GenTarski]
list_completeness_fragment [in Completeness.GenCompleteness]
list_completeness_expl [in Completeness.GenCompleteness]
list_completeness_standard [in Completeness.GenCompleteness]
list_cc [in Completeness.Prelim]
list_exists_not_incl [in Completeness.Prelim]
list_exists_DM [in Completeness.Prelim]
list_cycle [in Completeness.Prelim]
list_ind_ne [in Completeness.Prelim]
list_prod_in [in Completeness.FOL]
L_T_form_len [in Completeness.Enumeration]
L_T_sub_or [in Completeness.Enumeration]
L_T_sub [in Completeness.Enumeration]
L_T_unused [in Completeness.Enumeration]
L_T_unused_v [in Completeness.Enumeration]
L_T_unused_t [in Completeness.Enumeration]
L_T_nat_le [in Completeness.Enumeration]
L_form_cml [in Completeness.FOL]
L_term_cml [in Completeness.FOL]
M
maximal_prv [in Completeness.GenConstructions]maximal_Omega [in Completeness.GenConstructions]
model_fragment_classical [in Completeness.GenCompleteness]
model_fragment_correct [in Completeness.GenCompleteness]
model_bot_exploding [in Completeness.GenCompleteness]
model_bot_standard [in Completeness.GenCompleteness]
model_bot_classical [in Completeness.GenCompleteness]
model_bot_correct [in Completeness.GenCompleteness]
mp_to_ste [in Completeness.Stability]
mp_standard_completeness [in Completeness.GenCompleteness]
mp_tprv_stability [in Completeness.GenCompleteness]
N
nameless_equiv [in Completeness.ND]nameless_equiv' [in Completeness.FullSequent]
nameless_equiv [in Completeness.FullSequent]
ND_defend [in Completeness.DialogFragment]
not_in_cons [in Completeness.Prelim]
nsprv_cons [in Completeness.KripkeCompleteness]
nthe_app_l [in Completeness.Prelim]
nthe_length [in Completeness.Prelim]
nth_order_map [in Completeness.FOL]
O
ocons_sub [in Completeness.Sorensen]ocons_sub [in Completeness.SDialogues]
Omega_all [in Completeness.GenConstructions]
Omega_impl [in Completeness.GenConstructions]
Omega_T [in Completeness.GenConstructions]
Omega_prv [in Completeness.GenConstructions]
omega_le [in Completeness.GenConstructions]
or_single [in Completeness.FullSequent]
or_weak [in Completeness.FullSequent]
or_el [in Completeness.FullSequent]
or_char [in Completeness.FullSequent]
or_subst [in Completeness.FullSequent]
P
pairs_retract [in Completeness.DecidableEnumerable]pi [in Completeness.axioms]
plain_enum_slow [in Completeness.Enumeration]
plain_enum_enumerates [in Completeness.Enumeration]
pos_length [in Completeness.Prelim]
pos_nth [in Completeness.Prelim]
pos_nthe [in Completeness.Prelim]
projection [in Completeness.DecidableEnumerable]
projection' [in Completeness.DecidableEnumerable]
prop_T_correct [in Completeness.Stability]
prv_T_comp [in Completeness.ND]
prv_T_remove [in Completeness.ND]
prv_T_impl [in Completeness.ND]
prv_from_single [in Completeness.ND]
prv_cut [in Completeness.ND]
R
refutation_prv [in Completeness.ND]rem_inclr [in Completeness.Prelim]
rem_reorder [in Completeness.Prelim]
rem_id [in Completeness.Prelim]
rem_fst' [in Completeness.Prelim]
rem_fst [in Completeness.Prelim]
rem_comm [in Completeness.Prelim]
rem_equi [in Completeness.Prelim]
rem_app' [in Completeness.Prelim]
rem_app [in Completeness.Prelim]
rem_neq [in Completeness.Prelim]
rem_in [in Completeness.Prelim]
rem_cons' [in Completeness.Prelim]
rem_cons [in Completeness.Prelim]
rem_mono [in Completeness.Prelim]
rem_incl [in Completeness.Prelim]
rem_not_in [in Completeness.Prelim]
S
sat_subst [in Completeness.GenTarski]sat_comp [in Completeness.GenTarski]
sat_ext [in Completeness.GenTarski]
scons_comp [in Completeness.unscoped]
scons_eta_id [in Completeness.unscoped]
scons_eta [in Completeness.unscoped]
semantic_dm [in Completeness.GenTarski]
semantic_explosion [in Completeness.GenTarski]
semi_completeness_fragment [in Completeness.GenCompleteness]
semi_completeness_standard [in Completeness.GenCompleteness]
seq_ND_T [in Completeness.Gentzen]
seq_ND [in Completeness.Gentzen]
seq_nameless_equiv [in Completeness.Gentzen]
seq_subst_Weak [in Completeness.Gentzen]
seq_Weak [in Completeness.Gentzen]
seq_consistent [in Completeness.Gentzen]
sf_form_rules [in Completeness.DialogFull]
sf_form_rules [in Completeness.DialogFragment]
sf_well_founded [in Completeness.FOL]
sf_acc [in Completeness.FOL]
sf_well_founded [in Completeness.FullFOL]
sf_acc [in Completeness.FullFOL]
sig_lift_out_T [in Completeness.ND]
sig_lift_out [in Completeness.ND]
sig_drop_Weak [in Completeness.ND]
sig_lift_Weak [in Completeness.ND]
sig_drop_subst' [in Completeness.FOL]
sig_drop_subst_term' [in Completeness.FOL]
sig_lift_subst [in Completeness.FOL]
sig_lift_subst_term [in Completeness.FOL]
sig_lift_subst_valid [in Completeness.GenTarski]
sig_lift_subst_sat [in Completeness.GenTarski]
size_induction_dep [in Completeness.Prelim]
size_induction [in Completeness.Prelim]
size_ind [in Completeness.FOL]
Soundness [in Completeness.GenTarski]
split_right [in Completeness.Sorensen]
sprv_Dprv [in Completeness.DialogFragment]
stable_equiv [in Completeness.Stability]
sta_to_dn [in Completeness.Stability]
ste_to_mp [in Completeness.Stability]
stf_to_st_context [in Completeness.Stability]
StrongSoundness [in Completeness.GenTarski]
strong_completeness_fragment [in Completeness.GenCompleteness]
strong_completeness_expl [in Completeness.GenCompleteness]
strong_completeness_standard [in Completeness.GenCompleteness]
strong_term_ind [in Completeness.FOL]
strong_term_ind' [in Completeness.FOL]
strong_term_ind [in Completeness.FullFOL]
strong_term_ind' [in Completeness.FullFOL]
strong_ksoundness [in Completeness.Kripke]
subst_Weak [in Completeness.ND]
subst_unused_closed' [in Completeness.FOL]
subst_unused_closed [in Completeness.FOL]
subst_unused_range [in Completeness.FOL]
subst_unused_single [in Completeness.FOL]
subst_unused_form [in Completeness.FOL]
subst_unused_term [in Completeness.FOL]
subst_size [in Completeness.FOL]
subst_unused_closed' [in Completeness.FullFOL]
subst_unused_closed [in Completeness.FullFOL]
subst_unused_range [in Completeness.FullFOL]
subst_unused_single [in Completeness.FullFOL]
subst_unused_form [in Completeness.FullFOL]
subst_unused_term [in Completeness.FullFOL]
subst_Weak [in Completeness.FullSequent]
subs_sat' [in Completeness.GenTarski]
subs_sat [in Completeness.GenTarski]
subs_eval [in Completeness.GenTarski]
subs_interp_sat' [in Completeness.GenTarski]
subs_interp_sat [in Completeness.GenTarski]
subs_interp_eval [in Completeness.GenTarski]
svalid_dvalid [in Completeness.Sorensen]
swin_dwin [in Completeness.Sorensen]
switch_map [in Completeness.Enumeration]
s_sound [in Completeness.SDialogues]
T
tmap_contains_L [in Completeness.FOL]tmap_contains_L [in Completeness.FullFOL]
to_dec [in Completeness.Prelim]
tprv_list_T [in Completeness.ND]
T_list_el [in Completeness.DecidableEnumerable]
T_list_cum [in Completeness.DecidableEnumerable]
T_prod_el [in Completeness.DecidableEnumerable]
T_prod_cum [in Completeness.DecidableEnumerable]
T_nat_length [in Completeness.DecidableEnumerable]
T_nat_in [in Completeness.DecidableEnumerable]
U
union_closed [in Completeness.GenConstructions]union_econsistent [in Completeness.GenConstructions]
union_sub [in Completeness.GenConstructions]
union_f [in Completeness.GenConstructions]
universal_interp_eval [in Completeness.KripkeCompleteness]
unused_after_subst [in Completeness.FOL]
unused_after_subst_term [in Completeness.FOL]
up_term_term_pref_raise [in Completeness.FOL]
up_term_term_pref_ext_c' [in Completeness.FOL]
up_term_term_vsubs [in Completeness.FOL]
up_ren_ren [in Completeness.unscoped]
V
valid_T_fragment [in Completeness.GenCompleteness]valid_standard_expld_stability [in Completeness.GenCompleteness]
valid_T_model_bot [in Completeness.GenCompleteness]
valid_L_to_single [in Completeness.GenTarski]
valid_L_valid_T [in Completeness.GenTarski]
valid_T_standard_dm [in Completeness.GenTarski]
valid_T_subsumption [in Completeness.GenTarski]
varL_term [in Completeness.Syntax]
varL_term [in Completeness.FullSyntax]
vecs_from_correct [in Completeness.FOL]
vec_forall_cml [in Completeness.FOL]
vec_forall_map [in Completeness.FOL]
vec_map_ext [in Completeness.FOL]
vec_unused [in Completeness.FOL]
vec_forall_map [in Completeness.FullFOL]
vec_map_ext [in Completeness.FullFOL]
vec_unused [in Completeness.FullFOL]
venv_empty [in Completeness.GenTarski]
venv_sat [in Completeness.GenTarski]
vsubs_single_subst [in Completeness.ND]
vsubs_form_shift [in Completeness.ND]
W
Weak [in Completeness.ND]weaken [in Completeness.FullSequent]
Weak_T [in Completeness.ND]
Constructor Index
A
AAll [in Completeness.DialogFull]AAll [in Completeness.DialogFragment]
AAnd [in Completeness.DialogFull]
ABot [in Completeness.DialogFull]
ABot [in Completeness.DialogFragment]
Absurd [in Completeness.Gentzen]
AExt [in Completeness.DialogFull]
AImpl [in Completeness.DialogFull]
AImpl [in Completeness.DialogFragment]
AL [in Completeness.FullSequent]
All [in Completeness.Syntax]
All [in Completeness.FullSyntax]
AllE [in Completeness.ND]
AllI [in Completeness.ND]
AllL [in Completeness.Gentzen]
AllL [in Completeness.FullSequent]
AllR [in Completeness.Gentzen]
AllR [in Completeness.FullSequent]
AOr [in Completeness.DialogFull]
AR [in Completeness.FullSequent]
Att [in Completeness.Sorensen]
Att [in Completeness.SDialogues]
Ax [in Completeness.Gentzen]
Ax [in Completeness.FullSequent]
B
B_S [in Completeness.Syntax]B_I [in Completeness.GenTarski]
C
C [in Completeness.Sorensen]C [in Completeness.SDialogues]
class [in Completeness.ND]
Conj [in Completeness.FullSyntax]
Contr [in Completeness.Gentzen]
Contr [in Completeness.FullSequent]
Ctx [in Completeness.ND]
D
DAll [in Completeness.DialogFull]DAll [in Completeness.DialogFragment]
DAndL [in Completeness.DialogFull]
DAndR [in Completeness.DialogFull]
Def [in Completeness.Sorensen]
Def [in Completeness.SDialogues]
DExt [in Completeness.DialogFull]
DImpl [in Completeness.DialogFull]
DImpl [in Completeness.DialogFragment]
Disj [in Completeness.FullSyntax]
DOAtk [in Completeness.Sorensen]
DODef [in Completeness.Sorensen]
DOrL [in Completeness.DialogFull]
DOrR [in Completeness.DialogFull]
DPAtk [in Completeness.Sorensen]
DPDef [in Completeness.Sorensen]
DS [in Completeness.SDialogues]
DWS [in Completeness.Sorensen]
E
EOAtk [in Completeness.Sorensen]EOCounter [in Completeness.Sorensen]
EODef [in Completeness.Sorensen]
EPAtk [in Completeness.Sorensen]
EPDef [in Completeness.Sorensen]
EqType [in Completeness.Prelim]
EWS [in Completeness.Sorensen]
Ex [in Completeness.FullSyntax]
ExL [in Completeness.FullSequent]
Exp [in Completeness.ND]
Exp [in Completeness.FullSequent]
expl [in Completeness.ND]
ExR [in Completeness.FullSequent]
F
Fal [in Completeness.Syntax]Fal [in Completeness.FullSyntax]
Forall_cons [in Completeness.FOL]
Forall_nil [in Completeness.FOL]
Forall_cons [in Completeness.FullFOL]
Forall_nil [in Completeness.FullFOL]
Func [in Completeness.Syntax]
Func [in Completeness.FullSyntax]
I
ids [in Completeness.unscoped]IE [in Completeness.ND]
II [in Completeness.ND]
IL [in Completeness.Gentzen]
IL [in Completeness.FullSequent]
Impl [in Completeness.Syntax]
Impl [in Completeness.FullSyntax]
intu [in Completeness.ND]
IR [in Completeness.Gentzen]
IR [in Completeness.FullSequent]
L
lconst [in Completeness.ND]O
OL [in Completeness.FullSequent]OP [in Completeness.Sorensen]
OP [in Completeness.SDialogues]
OR1 [in Completeness.FullSequent]
OR2 [in Completeness.FullSequent]
P
Pc [in Completeness.ND]Perm [in Completeness.FullSequent]
Pred [in Completeness.Syntax]
Pred [in Completeness.FullSyntax]
R
ren1 [in Completeness.unscoped]ren2 [in Completeness.unscoped]
ren3 [in Completeness.unscoped]
ren4 [in Completeness.unscoped]
ren5 [in Completeness.unscoped]
S
SAll [in Completeness.FOL]SAll [in Completeness.FullFOL]
SConjL [in Completeness.FullFOL]
SConjR [in Completeness.FullFOL]
SDisjL [in Completeness.FullFOL]
SDisjR [in Completeness.FullFOL]
SEx [in Completeness.FullFOL]
SImplL [in Completeness.FOL]
SImplL [in Completeness.FullFOL]
SImplR [in Completeness.FOL]
SImplR [in Completeness.FullFOL]
SOAtk [in Completeness.Sorensen]
SOAtk [in Completeness.SDialogues]
SODef [in Completeness.Sorensen]
SODef [in Completeness.SDialogues]
SPAtk [in Completeness.Sorensen]
SPAtk [in Completeness.SDialogues]
SPDef [in Completeness.Sorensen]
SPDef [in Completeness.SDialogues]
stA [in Completeness.FOL]
stB [in Completeness.FOL]
stF [in Completeness.FOL]
stIL [in Completeness.FOL]
stIR [in Completeness.FOL]
stP [in Completeness.FOL]
subst1 [in Completeness.unscoped]
subst2 [in Completeness.unscoped]
subst3 [in Completeness.unscoped]
subst4 [in Completeness.unscoped]
subst5 [in Completeness.unscoped]
SWS [in Completeness.Sorensen]
SWS [in Completeness.SDialogues]
T
TAbsurd [in Completeness.Gentzen]TAllE [in Completeness.Gentzen]
TAllI [in Completeness.Gentzen]
TAllL [in Completeness.Gentzen]
TAllR [in Completeness.Gentzen]
TAx [in Completeness.Gentzen]
TContr [in Completeness.Gentzen]
TCtx [in Completeness.Gentzen]
TExp [in Completeness.Gentzen]
TIE [in Completeness.Gentzen]
TII [in Completeness.Gentzen]
TIL [in Completeness.Gentzen]
TIR [in Completeness.Gentzen]
Top [in Completeness.FullSyntax]
TR [in Completeness.FullSequent]
U
uft_Func [in Completeness.FOL]uft_var [in Completeness.FOL]
uft_Func [in Completeness.FullFOL]
uft_var [in Completeness.FullFOL]
uf_All [in Completeness.FOL]
uf_Impl [in Completeness.FOL]
uf_Pred [in Completeness.FOL]
uf_Fal [in Completeness.FOL]
uf_Ex [in Completeness.FullFOL]
uf_All [in Completeness.FullFOL]
uf_O [in Completeness.FullFOL]
uf_A [in Completeness.FullFOL]
uf_I [in Completeness.FullFOL]
uf_Pred [in Completeness.FullFOL]
uf_Top [in Completeness.FullFOL]
uf_Fal [in Completeness.FullFOL]
up_term [in Completeness.Syntax]
up_term [in Completeness.FullSyntax]
V
var_term [in Completeness.Syntax]var_term [in Completeness.FullSyntax]
vCons [in Completeness.SDialogues]
vec_inS [in Completeness.FOL]
vec_inB [in Completeness.FOL]
vec_inS [in Completeness.FullFOL]
vec_inB [in Completeness.FullFOL]
vNil [in Completeness.SDialogues]
W
Weak [in Completeness.FullSequent]Axiom Index
P
pext [in Completeness.axioms]Projection Index
A
atomic [in Completeness.Sorensen]atomic [in Completeness.SDialogues]
attack [in Completeness.Sorensen]
attack [in Completeness.SDialogues]
C
cum_T [in Completeness.DecidableEnumerable]D
dec_f [in Completeness.Sorensen]dec_f [in Completeness.SDialogues]
defense [in Completeness.Sorensen]
defense [in Completeness.SDialogues]
E
el_T [in Completeness.DecidableEnumerable]enum [in Completeness.GenConstructions]
enum_unused [in Completeness.GenConstructions]
enum_enum [in Completeness.GenConstructions]
eqType_dec [in Completeness.Prelim]
eqType_X [in Completeness.Prelim]
F
Funcs [in Completeness.Syntax]Funcs [in Completeness.FullSyntax]
fun_ar [in Completeness.Syntax]
fun_ar [in Completeness.FullSyntax]
I
ids [in Completeness.unscoped]In_T_closed [in Completeness.GenConstructions]
In_T [in Completeness.GenConstructions]
i_F [in Completeness.GenTarski]
i_P [in Completeness.GenTarski]
i_f [in Completeness.GenTarski]
K
k_Bot [in Completeness.Kripke]k_P [in Completeness.Kripke]
k_interp [in Completeness.Kripke]
L
L_T [in Completeness.DecidableEnumerable]M
mon_Bot [in Completeness.Kripke]mon_P [in Completeness.Kripke]
N
NBot [in Completeness.GenConstructions]NBot_closed [in Completeness.GenConstructions]
nodes [in Completeness.Kripke]
O
Out_T_impl [in Completeness.GenConstructions]Out_T_all [in Completeness.GenConstructions]
Out_T_prv [in Completeness.GenConstructions]
Out_T_sub [in Completeness.GenConstructions]
Out_T_econsistent [in Completeness.GenConstructions]
Out_T [in Completeness.GenConstructions]
P
Preds [in Completeness.Syntax]Preds [in Completeness.FullSyntax]
pred_ar [in Completeness.Syntax]
pred_ar [in Completeness.FullSyntax]
R
reachable [in Completeness.Kripke]reach_tran [in Completeness.Kripke]
reach_refl [in Completeness.Kripke]
ren1 [in Completeness.unscoped]
ren2 [in Completeness.unscoped]
ren3 [in Completeness.unscoped]
ren4 [in Completeness.unscoped]
ren5 [in Completeness.unscoped]
S
subst1 [in Completeness.unscoped]subst2 [in Completeness.unscoped]
subst3 [in Completeness.unscoped]
subst4 [in Completeness.unscoped]
subst5 [in Completeness.unscoped]
U
up_term [in Completeness.Syntax]up_term [in Completeness.FullSyntax]
V
variant [in Completeness.GenConstructions]Inductive Index
A
attack_form [in Completeness.DialogFull]attack_form [in Completeness.DialogFragment]
B
bottom [in Completeness.ND]C
challenge [in Completeness.Sorensen]challenge [in Completeness.SDialogues]
D
defense_form [in Completeness.DialogFull]defense_form [in Completeness.DialogFragment]
domove [in Completeness.Sorensen]
dpmove [in Completeness.Sorensen]
Dprv [in Completeness.Sorensen]
Dprv [in Completeness.SDialogues]
Dprv_state [in Completeness.SDialogues]
dwin_strat [in Completeness.Sorensen]
E
eomove [in Completeness.Sorensen]epmove [in Completeness.Sorensen]
ewin_strat [in Completeness.Sorensen]
F
Forall [in Completeness.FOL]Forall [in Completeness.FullFOL]
form [in Completeness.Syntax]
form [in Completeness.FullSyntax]
fprv [in Completeness.FullSequent]
I
IVec [in Completeness.SDialogues]O
opening [in Completeness.Sorensen]opening [in Completeness.SDialogues]
P
peirce [in Completeness.ND]prv [in Completeness.ND]
R
Ren1 [in Completeness.unscoped]Ren2 [in Completeness.unscoped]
Ren3 [in Completeness.unscoped]
Ren4 [in Completeness.unscoped]
Ren5 [in Completeness.unscoped]
S
sf [in Completeness.FOL]sf [in Completeness.FullFOL]
somove [in Completeness.Sorensen]
somove [in Completeness.SDialogues]
spmove [in Completeness.Sorensen]
spmove [in Completeness.SDialogues]
sprv [in Completeness.Gentzen]
Subst1 [in Completeness.unscoped]
Subst2 [in Completeness.unscoped]
Subst3 [in Completeness.unscoped]
Subst4 [in Completeness.unscoped]
Subst5 [in Completeness.unscoped]
subterm [in Completeness.FOL]
subterm_form [in Completeness.FOL]
swin_strat [in Completeness.Sorensen]
swin_strat [in Completeness.SDialogues]
T
term [in Completeness.Syntax]term [in Completeness.FullSyntax]
tprv [in Completeness.Gentzen]
tsprv [in Completeness.Gentzen]
U
unused [in Completeness.FOL]unused [in Completeness.FullFOL]
unused_term [in Completeness.FOL]
unused_term [in Completeness.FullFOL]
Up_term [in Completeness.Syntax]
Up_term [in Completeness.FullSyntax]
V
Var [in Completeness.unscoped]vec_in [in Completeness.FOL]
vec_in [in Completeness.FullFOL]
Section Index
C
ClosingBigImp [in Completeness.GenTarski]ClosingValidity [in Completeness.GenTarski]
Completeness [in Completeness.GenCompleteness]
Completeness.BotModel [in Completeness.GenCompleteness]
Completeness.ExplodingCompletenes [in Completeness.GenCompleteness]
Completeness.FragmentCompleteness [in Completeness.GenCompleteness]
Completeness.FragmentModel [in Completeness.GenCompleteness]
Completeness.MPStrongCompleteness [in Completeness.GenCompleteness]
Completeness.StandardCompletenes [in Completeness.GenCompleteness]
Composition [in Completeness.GenConstructions]
Consistency [in Completeness.Consistency]
Consistency.Classical [in Completeness.Consistency]
D
DGame [in Completeness.Sorensen]DialogFragment [in Completeness.DialogFragment]
DialogFull [in Completeness.DialogFull]
DNT [in Completeness.ND]
E
EGame [in Completeness.Sorensen]Enumerability [in Completeness.ND]
Enumerability [in Completeness.FOL]
enumerable_list.fixL [in Completeness.DecidableEnumerable]
enumerable_list [in Completeness.DecidableEnumerable]
enumerable_prod.fixLs [in Completeness.DecidableEnumerable]
enumerable_prod [in Completeness.DecidableEnumerable]
enumerable_enum [in Completeness.DecidableEnumerable]
Enumeration [in Completeness.Enumeration]
enum_enumerable [in Completeness.DecidableEnumerable]
EqDec [in Completeness.FOL]
EqDec [in Completeness.FullFOL]
Equi [in Completeness.Prelim]
F
Filter [in Completeness.Prelim]FiniteCompleteness [in Completeness.GenCompleteness]
fix_sig [in Completeness.Syntax]
fix_sig [in Completeness.FullSyntax]
FOL [in Completeness.FOL]
FOL.ContainsAutomation [in Completeness.FOL]
FullFOL [in Completeness.FullFOL]
FullFOL.ContainsAutomation [in Completeness.FullFOL]
FullSequent [in Completeness.FullSequent]
G
GenCons [in Completeness.GenConstructions]GenCons.Explosion [in Completeness.GenConstructions]
GenCons.Henkin [in Completeness.GenConstructions]
GenCons.Omega [in Completeness.GenConstructions]
GenCons.Union [in Completeness.GenConstructions]
Gentzen [in Completeness.Gentzen]
Gentzen.CutElimination [in Completeness.Gentzen]
Gentzen.Enumerability [in Completeness.Gentzen]
Gentzen.Soundness [in Completeness.Gentzen]
Gentzen.Weakening [in Completeness.Gentzen]
I
Inclusion [in Completeness.Prelim]K
Kripke [in Completeness.Kripke]KripkeCompleteness [in Completeness.KripkeCompleteness]
KripkeCompleteness.BottomlessCompleteness [in Completeness.KripkeCompleteness]
KripkeCompleteness.Contexts [in Completeness.KripkeCompleteness]
KripkeCompleteness.ExplodingCompleteness [in Completeness.KripkeCompleteness]
KripkeCompleteness.MPRequired [in Completeness.KripkeCompleteness]
KripkeCompleteness.StandardCompleteness [in Completeness.KripkeCompleteness]
Kripke.Model [in Completeness.Kripke]
Kripke.Substs [in Completeness.Kripke]
KSoundness [in Completeness.Kripke]
L
LJD [in Completeness.Sorensen]L_T_Enumeration [in Completeness.Enumeration]
L_T_unused [in Completeness.Enumeration]
M
Membership [in Completeness.Prelim]N
ND_def.Weakening [in Completeness.ND]ND_def [in Completeness.ND]
neList [in Completeness.Prelim]
P
Positions [in Completeness.Prelim]PropT [in Completeness.Stability]
R
RefutationComp [in Completeness.ND]Removal [in Completeness.Prelim]
S
SDialogues [in Completeness.SDialogues]SGame [in Completeness.Sorensen]
SigExt [in Completeness.ND]
SigExt [in Completeness.FOL]
SigExt [in Completeness.GenTarski]
StabilityClasses [in Completeness.Stability]
StabilityClasses.DN [in Completeness.Stability]
StabilityClasses.ObjMP [in Completeness.Stability]
StabilityClasses.ObjMP.ConT [in Completeness.Stability]
StabilityClasses.SyntMP [in Completeness.Stability]
StabilityClasses.SyntMP.MPEnum [in Completeness.Stability]
StrongCompleteness [in Completeness.GenCompleteness]
Subterm [in Completeness.FOL]
T
Tarski [in Completeness.GenTarski]Tarski.Semantics [in Completeness.GenTarski]
Tarski.Soundness [in Completeness.GenTarski]
Tarski.Substs [in Completeness.GenTarski]
TheoryManipulation [in Completeness.ND]
Instance Index
A
and_dec [in Completeness.Prelim]app_equi_proper [in Completeness.Prelim]
app_incl_proper [in Completeness.Prelim]
B
bool_eq_dec [in Completeness.Prelim]bool_dec [in Completeness.Prelim]
C
cons_equi_proper [in Completeness.Prelim]cons_incl_proper [in Completeness.Prelim]
D
dec_sig_ext_Preds [in Completeness.FOL]dec_sig_ext_Funcs [in Completeness.FOL]
dec_form [in Completeness.FOL]
dec_term [in Completeness.FOL]
dec_vec [in Completeness.FOL]
dec_form [in Completeness.FullFOL]
dec_term [in Completeness.FullFOL]
dec_vec [in Completeness.FullFOL]
E
Empty_set_eq_dec [in Completeness.Prelim]enumerable_list [in Completeness.DecidableEnumerable]
enumT_nat [in Completeness.DecidableEnumerable]
enumT_sig_ext_Preds [in Completeness.FOL]
enumT_sig_ext_Funcs [in Completeness.FOL]
enumT_form [in Completeness.FOL]
enumT_term [in Completeness.FOL]
enumT_vec [in Completeness.FOL]
enum_bool [in Completeness.DecidableEnumerable]
equi_Equivalence [in Completeness.Prelim]
F
False_enumT [in Completeness.Stability]False_eq_dec [in Completeness.Prelim]
False_dec [in Completeness.Prelim]
form_rules [in Completeness.DialogFull]
form_rules [in Completeness.DialogFragment]
I
idsRen [in Completeness.unscoped]iff_dec [in Completeness.Prelim]
impl_dec [in Completeness.Prelim]
incl_equi_proper [in Completeness.Prelim]
incl_preorder [in Completeness.Prelim]
in_equi_proper [in Completeness.Prelim]
in_incl_proper [in Completeness.Prelim]
K
kmodel_reach_trans [in Completeness.Kripke]kmodel_reach_refl [in Completeness.Kripke]
K_std [in Completeness.KripkeCompleteness]
K_ctx [in Completeness.KripkeCompleteness]
L
list_exists_dec [in Completeness.Prelim]list_forall_dec [in Completeness.Prelim]
list_in_dec [in Completeness.Prelim]
list_eq_dec [in Completeness.Prelim]
M
model_fragment [in Completeness.GenCompleteness]model_bot [in Completeness.GenCompleteness]
N
nat_eq_dec [in Completeness.Prelim]not_dec [in Completeness.Prelim]
O
option_eq_dec [in Completeness.Prelim]or_dec [in Completeness.Prelim]
P
prod_enumerable [in Completeness.DecidableEnumerable]prod_eq_dec [in Completeness.Prelim]
S
subset_T_trans [in Completeness.FOL]subset_T_trans [in Completeness.FullFOL]
Subst_form [in Completeness.Syntax]
Subst_term [in Completeness.Syntax]
Subst_form [in Completeness.FullSyntax]
Subst_term [in Completeness.FullSyntax]
sum_eq_dec [in Completeness.Prelim]
T
True_eq_dec [in Completeness.Prelim]True_dec [in Completeness.Prelim]
U
unit_eq_dec [in Completeness.Prelim]universal_interp [in Completeness.KripkeCompleteness]
Up_term_term [in Completeness.Syntax]
Up_term_term [in Completeness.FullSyntax]
V
VarInstance_term [in Completeness.Syntax]VarInstance_term [in Completeness.FullSyntax]
Abbreviation Index
D
Decb [in Completeness.Prelim]F
fin [in Completeness.unscoped]N
nthe [in Completeness.Prelim]nthe [in Completeness.Prelim]
Definition Index
A
any_T [in Completeness.Stability]ap [in Completeness.unscoped]
apc [in Completeness.unscoped]
atomic_form [in Completeness.DialogFull]
atomic_form [in Completeness.DialogFragment]
at_pos [in Completeness.Enumeration]
B
big_imp [in Completeness.FOL]big_or [in Completeness.FullSequent]
BLM [in Completeness.GenTarski]
C
capture [in Completeness.FOL]capture_subs [in Completeness.ND]
classical [in Completeness.GenTarski]
close [in Completeness.FOL]
closed [in Completeness.FOL]
closed [in Completeness.FullFOL]
closed_T [in Completeness.FOL]
closed_T [in Completeness.FullFOL]
cod [in Completeness.axioms]
cod_comp [in Completeness.axioms]
cod_ext' [in Completeness.axioms]
cod_ext [in Completeness.axioms]
cod_id [in Completeness.axioms]
cod_map [in Completeness.axioms]
compl [in Completeness.DecidableEnumerable]
compSubstSubst_form [in Completeness.Syntax]
compSubstSubst_term [in Completeness.Syntax]
compSubstSubst_form [in Completeness.FullSyntax]
compSubstSubst_term [in Completeness.FullSyntax]
congr_All [in Completeness.Syntax]
congr_Impl [in Completeness.Syntax]
congr_Pred [in Completeness.Syntax]
congr_Fal [in Completeness.Syntax]
congr_Func [in Completeness.Syntax]
congr_Ex [in Completeness.FullSyntax]
congr_All [in Completeness.FullSyntax]
congr_Disj [in Completeness.FullSyntax]
congr_Conj [in Completeness.FullSyntax]
congr_Impl [in Completeness.FullSyntax]
congr_Pred [in Completeness.FullSyntax]
congr_Top [in Completeness.FullSyntax]
congr_Fal [in Completeness.FullSyntax]
congr_Func [in Completeness.FullSyntax]
cons [in Completeness.KripkeCompleteness]
consistent [in Completeness.Consistency]
consistent_max [in Completeness.Consistency]
constraint [in Completeness.GenTarski]
cons_ctx [in Completeness.KripkeCompleteness]
contains [in Completeness.FOL]
contains [in Completeness.FullFOL]
contains_L [in Completeness.FOL]
contains_L [in Completeness.FullFOL]
continuation [in Completeness.SDialogues]
continuation_lift [in Completeness.SDialogues]
con_T [in Completeness.Stability]
con_subs [in Completeness.GenTarski]
counter_safe_lift [in Completeness.SDialogues]
counter_safe [in Completeness.SDialogues]
ctx_incl [in Completeness.KripkeCompleteness]
cumulative [in Completeness.DecidableEnumerable]
cycle_shift [in Completeness.ND]
cycle_shift [in Completeness.FullSequent]
D
Dec [in Completeness.Prelim]dec [in Completeness.Prelim]
decidable [in Completeness.DecidableEnumerable]
deferred [in Completeness.Sorensen]
deferred [in Completeness.SDialogues]
discrete [in Completeness.DecidableEnumerable]
disjoint [in Completeness.Prelim]
DN [in Completeness.Stability]
dnt [in Completeness.ND]
DPexp1 [in Completeness.GenConstructions]
DPexp2 [in Completeness.GenConstructions]
DPexp3 [in Completeness.GenConstructions]
Dprv_state_size [in Completeness.SDialogues]
Dprv_size [in Completeness.SDialogues]
droppable [in Completeness.GenTarski]
drop_interp [in Completeness.GenTarski]
drop_interp' [in Completeness.GenTarski]
dstate [in Completeness.Sorensen]
dummy_sig [in Completeness.Stability]
dummy_interp [in Completeness.GenTarski]
dvalid [in Completeness.Sorensen]
dwin_Dprv_embed [in Completeness.Sorensen]
E
econsistent [in Completeness.GenConstructions]econsistent_join [in Completeness.GenConstructions]
EM [in Completeness.GenTarski]
embed [in Completeness.Gentzen]
enum [in Completeness.DecidableEnumerable]
enumerable [in Completeness.DecidableEnumerable]
enumerable__T [in Completeness.DecidableEnumerable]
enum_T [in Completeness.Stability]
env [in Completeness.GenTarski]
equi [in Completeness.Prelim]
eval [in Completeness.GenTarski]
evalid [in Completeness.Sorensen]
Exp [in Completeness.GenConstructions]
exp [in Completeness.GenConstructions]
exploding [in Completeness.GenConstructions]
exploding_bot [in Completeness.GenTarski]
exp_axiom [in Completeness.GenConstructions]
extend [in Completeness.FOL]
extend [in Completeness.FullFOL]
ext_form [in Completeness.Syntax]
ext_term [in Completeness.Syntax]
ext_form [in Completeness.FullSyntax]
ext_term [in Completeness.FullSyntax]
ext_c [in Completeness.FOL]
ext_c' [in Completeness.FOL]
F
filter [in Completeness.Prelim]fin_T [in Completeness.Stability]
fin_minus [in Completeness.FOL]
form_enum [in Completeness.Enumeration]
form_shift [in Completeness.FOL]
form_shift [in Completeness.FullFOL]
funcomp [in Completeness.axioms]
funcomp [in Completeness.unscoped]
H
has_model [in Completeness.GenTarski]Henkin [in Completeness.GenConstructions]
henkin [in Completeness.GenConstructions]
henkin_axiom [in Completeness.GenConstructions]
I
id [in Completeness.unscoped]idSubst_form [in Completeness.Syntax]
idSubst_term [in Completeness.Syntax]
idSubst_form [in Completeness.FullSyntax]
idSubst_term [in Completeness.FullSyntax]
inclp [in Completeness.Prelim]
input_fragment [in Completeness.GenCompleteness]
input_bot [in Completeness.GenCompleteness]
is_Henkin [in Completeness.GenConstructions]
J
justified [in Completeness.Sorensen]justified [in Completeness.SDialogues]
K
kbottomless [in Completeness.Kripke]kconstraint [in Completeness.Kripke]
kcon_subs [in Completeness.Kripke]
kexploding [in Completeness.Kripke]
ksat [in Completeness.Kripke]
kstandard [in Completeness.Kripke]
kvalid_T [in Completeness.Kripke]
kvalid_L [in Completeness.Kripke]
L
lift_interp [in Completeness.GenTarski]list_comp [in Completeness.axioms]
list_id [in Completeness.axioms]
list_ext [in Completeness.axioms]
list_T [in Completeness.FOL]
list_T [in Completeness.FullFOL]
L_tsat_T [in Completeness.Stability]
L_tded [in Completeness.ND]
L_con [in Completeness.ND]
L_ded [in Completeness.ND]
L_tseq [in Completeness.Gentzen]
L_seq [in Completeness.Gentzen]
L_form [in Completeness.FOL]
L_term [in Completeness.FOL]
L_vec [in Completeness.FOL]
M
map_closed [in Completeness.Stability]maximal [in Completeness.GenConstructions]
MP [in Completeness.Stability]
N
normal [in Completeness.Gentzen]not_AllI [in Completeness.Gentzen]
not_II [in Completeness.Gentzen]
O
ocons [in Completeness.Sorensen]ocons [in Completeness.SDialogues]
ofNat [in Completeness.DecidableEnumerable]
omap [in Completeness.Prelim]
Omega [in Completeness.GenConstructions]
omega [in Completeness.GenConstructions]
opred [in Completeness.Sorensen]
opred [in Completeness.SDialogues]
osum [in Completeness.SDialogues]
output_fragment [in Completeness.GenCompleteness]
output_bot [in Completeness.GenCompleteness]
P
plain_enum [in Completeness.Enumeration]plan [in Completeness.SDialogues]
plan_lift [in Completeness.SDialogues]
pos [in Completeness.Prelim]
pref [in Completeness.FOL]
prod_comp [in Completeness.axioms]
prod_ext [in Completeness.axioms]
prod_id [in Completeness.axioms]
prod_map [in Completeness.axioms]
prop_T [in Completeness.Stability]
R
raise [in Completeness.FOL]rem [in Completeness.Prelim]
R_nat_nat [in Completeness.DecidableEnumerable]
S
sat [in Completeness.GenTarski]scons [in Completeness.unscoped]
shift [in Completeness.unscoped]
shift_P [in Completeness.FOL]
shift_P [in Completeness.FullFOL]
sig_drop [in Completeness.FOL]
sig_drop' [in Completeness.FOL]
sig_drop_term [in Completeness.FOL]
sig_drop_term' [in Completeness.FOL]
sig_lift [in Completeness.FOL]
sig_lift' [in Completeness.FOL]
sig_lift_term [in Completeness.FOL]
sig_lift_term' [in Completeness.FOL]
sig_ext [in Completeness.FOL]
size [in Completeness.FOL]
SM [in Completeness.GenTarski]
sstate [in Completeness.Sorensen]
sstate [in Completeness.SDialogues]
ST [in Completeness.Stability]
stable [in Completeness.Stability]
stab_class [in Completeness.Stability]
standard_bot [in Completeness.GenTarski]
stprv [in Completeness.Gentzen]
ST__f [in Completeness.Stability]
ST__e [in Completeness.Stability]
ST__a [in Completeness.Stability]
subctx [in Completeness.SDialogues]
subctx_lift [in Completeness.SDialogues]
subset_T [in Completeness.FOL]
subset_T [in Completeness.FullFOL]
subst_form [in Completeness.Syntax]
subst_term [in Completeness.Syntax]
subst_form [in Completeness.FullSyntax]
subst_term [in Completeness.FullSyntax]
subs_interp [in Completeness.GenTarski]
svalid [in Completeness.Sorensen]
svalid [in Completeness.SDialogues]
swin_dwin_embed [in Completeness.Sorensen]
T
tembed [in Completeness.Gentzen]theory [in Completeness.FOL]
theory [in Completeness.FullFOL]
tmap [in Completeness.FOL]
tmap [in Completeness.FullFOL]
tprv [in Completeness.ND]
tsat [in Completeness.Stability]
T_list [in Completeness.DecidableEnumerable]
T_prod [in Completeness.DecidableEnumerable]
T_ [in Completeness.DecidableEnumerable]
U
union [in Completeness.GenConstructions]unused_L [in Completeness.FOL]
unused_L [in Completeness.FullFOL]
upExt_term_term [in Completeness.Syntax]
upExt_term_term [in Completeness.FullSyntax]
upId_term_term [in Completeness.Syntax]
upId_term_term [in Completeness.FullSyntax]
up_subst_subst_term_term [in Completeness.Syntax]
up_term_term [in Completeness.Syntax]
up_subst_subst_term_term [in Completeness.FullSyntax]
up_term_term [in Completeness.FullSyntax]
up_ren [in Completeness.unscoped]
V
valid_L [in Completeness.GenTarski]valid_T [in Completeness.GenTarski]
var_zero [in Completeness.unscoped]
vecs_from [in Completeness.FOL]
vec_comp [in Completeness.axioms]
vec_id [in Completeness.axioms]
vec_ext [in Completeness.axioms]
venv [in Completeness.GenTarski]
vix [in Completeness.SDialogues]
vmap [in Completeness.SDialogues]
vsubs [in Completeness.FOL]
Record Index
C
ConstructionInputs [in Completeness.GenConstructions]ConstructionOutputs [in Completeness.GenConstructions]
E
enumT [in Completeness.DecidableEnumerable]eqType [in Completeness.Prelim]
I
interp [in Completeness.GenTarski]K
kmodel [in Completeness.Kripke]R
Ren1 [in Completeness.unscoped]Ren2 [in Completeness.unscoped]
Ren3 [in Completeness.unscoped]
Ren4 [in Completeness.unscoped]
Ren5 [in Completeness.unscoped]
rule_set [in Completeness.Sorensen]
rule_set [in Completeness.SDialogues]
S
Signature [in Completeness.Syntax]Signature [in Completeness.FullSyntax]
Subst1 [in Completeness.unscoped]
Subst2 [in Completeness.unscoped]
Subst3 [in Completeness.unscoped]
Subst4 [in Completeness.unscoped]
Subst5 [in Completeness.unscoped]
U
Up_term [in Completeness.Syntax]Up_term [in Completeness.FullSyntax]
V
Var [in Completeness.unscoped]| 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 | (1509 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 | (138 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (119 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 | (23 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 | (499 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 | (171 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 | (1 entry) |
| 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 | (60 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 | (60 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 | (88 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 | (68 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (255 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 | (23 entries) |