| 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 | (2108 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 | (169 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 | (151 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 | (35 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 | (730 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 | (206 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (86 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 | (67 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 | (106 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 | (119 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 | (11 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 | (26 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 | (400 entries) |
Global Index
A
AAll [constructor, in Undecidability.FOLC.DialogFull]AAll [constructor, in Undecidability.FOLC.DialogFragment]
AAnd [constructor, in Undecidability.FOLC.DialogFull]
ABot [constructor, in Undecidability.FOLC.DialogFull]
ABot [constructor, in Undecidability.FOLC.DialogFragment]
Absurd [constructor, in Undecidability.FOLC.Gentzen]
Acc_iff [lemma, in Undecidability.FOLC.WFexp]
Acc_perm' [lemma, in Undecidability.FOLC.WFexp]
Acc_perm [lemma, in Undecidability.FOLC.WFexp]
Acc_app_rev [lemma, in Undecidability.FOLC.WFexp]
Acc_app [lemma, in Undecidability.FOLC.WFexp]
AExt [constructor, in Undecidability.FOLC.DialogFull]
AImpl [constructor, in Undecidability.FOLC.DialogFull]
AImpl [constructor, in Undecidability.FOLC.DialogFragment]
AL [constructor, in Undecidability.FOLC.FullSequent]
All [constructor, in Undecidability.FOLC.FullSyntax]
All [constructor, in Undecidability.FOLC.Syntax]
AllE [constructor, in Undecidability.FOLC.FullND]
AllE [constructor, in Undecidability.FOLC.ND]
AllI [constructor, in Undecidability.FOLC.FullND]
AllI [constructor, in Undecidability.FOLC.ND]
AllL [constructor, in Undecidability.FOLC.Gentzen]
AllL [constructor, in Undecidability.FOLC.FullSequent]
AllR [constructor, in Undecidability.FOLC.Gentzen]
AllR [constructor, in Undecidability.FOLC.FullSequent]
All' [constructor, in Undecidability.FOLC.LEnum]
Analysis [library]
And [definition, in Undecidability.FOLC.WKL]
And_sat [lemma, in Undecidability.FOLC.WKL]
any_T_map_closed [lemma, in Undecidability.FOLC.Stability]
any_T [definition, in Undecidability.FOLC.Stability]
AOr [constructor, in Undecidability.FOLC.DialogFull]
ap [definition, in Undecidability.FOLC.unscoped]
apc [definition, in Undecidability.FOLC.unscoped]
appCtx [lemma, in Undecidability.FOLC.BPCP_CND]
app_split_two [lemma, in Undecidability.FOLC.WFexp]
App' [constructor, in Undecidability.FOLC.LEnum]
App'' [definition, in Undecidability.FOLC.LEnum]
app1 [lemma, in Undecidability.FOLC.BPCP_CND]
app2 [lemma, in Undecidability.FOLC.BPCP_CND]
app3 [lemma, in Undecidability.FOLC.BPCP_CND]
AR [constructor, in Undecidability.FOLC.FullSequent]
ar_inj_Preds [projection, in Undecidability.FOLC.Extend]
ar_inj_Funcs [projection, in Undecidability.FOLC.Extend]
atomic [projection, in Undecidability.FOLC.SDialogues]
atomic [projection, in Undecidability.FOLC.Sorensen]
atomic_dec [lemma, in Undecidability.FOLC.DialogFull]
atomic_form [definition, in Undecidability.FOLC.DialogFull]
atomic_dec [lemma, in Undecidability.FOLC.DialogFragment]
atomic_form [definition, in Undecidability.FOLC.DialogFragment]
Att [constructor, in Undecidability.FOLC.SDialogues]
Att [constructor, in Undecidability.FOLC.Sorensen]
attack [projection, in Undecidability.FOLC.SDialogues]
attack [projection, in Undecidability.FOLC.Sorensen]
attack_form_inv_ext [lemma, in Undecidability.FOLC.DialogFull]
attack_form_inv_all [lemma, in Undecidability.FOLC.DialogFull]
attack_form_inv_or [lemma, in Undecidability.FOLC.DialogFull]
attack_form_inv_and [lemma, in Undecidability.FOLC.DialogFull]
attack_form_inv_impl [lemma, in Undecidability.FOLC.DialogFull]
attack_form [inductive, in Undecidability.FOLC.DialogFull]
attack_form_inv_all [lemma, in Undecidability.FOLC.DialogFragment]
attack_form_inv_impl [lemma, in Undecidability.FOLC.DialogFragment]
attack_form [inductive, in Undecidability.FOLC.DialogFragment]
at_pos [definition, in Undecidability.FOLC.Enumeration]
Ax [constructor, in Undecidability.FOLC.Gentzen]
Ax [constructor, in Undecidability.FOLC.FullSequent]
axioms [library]
AXM [lemma, in Undecidability.FOLC.FullND]
AXM [lemma, in Undecidability.FOLC.ND]
B
bcompleteness [lemma, in Undecidability.FOLC.Lindenbaum]big_imp [definition, in Undecidability.FOLC.FullFOL]
big_imp [definition, in Undecidability.FOLC.FOL]
big_imp_extract [lemma, in Undecidability.FOLC.FullND]
big_imp_valid_L [lemma, in Undecidability.FOLC.GenTarski]
big_or [definition, in Undecidability.FOLC.FullSequent]
big_imp_extract [lemma, in Undecidability.FOLC.ND]
BLM [definition, in Undecidability.FOLC.GenTarski]
BL_E_subsumption [lemma, in Undecidability.FOLC.GenTarski]
boolean [definition, in Undecidability.FOLC.Lindenbaum]
boolean_completion [lemma, in Undecidability.FOLC.Lindenbaum]
bool_true_Prop [lemma, in Undecidability.FOLC.LEnum]
Bot [projection, in Undecidability.FOLC.Heyting]
bottom [inductive, in Undecidability.FOLC.FullND]
bottom [inductive, in Undecidability.FOLC.ND]
Bot1 [projection, in Undecidability.FOLC.Heyting]
bounded_infinite_contra [lemma, in Undecidability.FOLC.WKL]
bounded_tree [definition, in Undecidability.FOLC.WKL]
BPCP_prv [lemma, in Undecidability.FOLC.BPCP_FOL]
BPCP_prv' [lemma, in Undecidability.FOLC.BPCP_FOL]
BPCP_valid [lemma, in Undecidability.FOLC.BPCP_FOL]
BPCP_CND [lemma, in Undecidability.FOLC.BPCP_CND]
BPCP_to_CND [lemma, in Undecidability.FOLC.BPCP_CND]
BPCP_CND.R [variable, in Undecidability.FOLC.BPCP_CND]
BPCP_CND [section, in Undecidability.FOLC.BPCP_CND]
BPCP_FOL [library]
BPCP_CND [library]
bsoundness [lemma, in Undecidability.FOLC.Lindenbaum]
BSoundness [lemma, in Undecidability.FOLC.Lindenbaum]
BSoundness' [lemma, in Undecidability.FOLC.Lindenbaum]
bvalid [definition, in Undecidability.FOLC.Lindenbaum]
B_S [constructor, in Undecidability.FOLC.Terms]
B_I [constructor, in Undecidability.FOLC.GenTarski]
C
C [constructor, in Undecidability.FOLC.SDialogues]C [constructor, in Undecidability.FOLC.Sorensen]
capture [definition, in Undecidability.FOLC.FullFOL]
capture [definition, in Undecidability.FOLC.FOL]
capture_captures [lemma, in Undecidability.FOLC.FullFOL]
capture_captures [lemma, in Undecidability.FOLC.FOL]
capture_extract [lemma, in Undecidability.FOLC.FullND]
capture_subs [definition, in Undecidability.FOLC.FullND]
capture_extract [lemma, in Undecidability.FOLC.ND]
capture_subs [definition, in Undecidability.FOLC.ND]
cast_trans [lemma, in Undecidability.FOLC.Extend]
cast_eq [lemma, in Undecidability.FOLC.Extend]
cast_app [lemma, in Undecidability.FOLC.LEnum]
cast_nil [lemma, in Undecidability.FOLC.LEnum]
cast_refl [lemma, in Undecidability.FOLC.WKL]
cend_dn [lemma, in Undecidability.FOLC.KripkeCompleteness]
CE1 [constructor, in Undecidability.FOLC.FullND]
CE2 [constructor, in Undecidability.FOLC.FullND]
challenge [inductive, in Undecidability.FOLC.SDialogues]
challenge [inductive, in Undecidability.FOLC.Sorensen]
CHAProperty [section, in Undecidability.FOLC.Heyting]
_ <~> _ (type_scope) [notation, in Undecidability.FOLC.Heyting]
CI [constructor, in Undecidability.FOLC.FullND]
class [constructor, in Undecidability.FOLC.FullND]
class [constructor, in Undecidability.FOLC.ND]
classical [definition, in Undecidability.FOLC.FullTarski]
classical [definition, in Undecidability.FOLC.GenTarski]
clb_alg_boolean [lemma, in Undecidability.FOLC.Lindenbaum]
clb_Pr [definition, in Undecidability.FOLC.Lindenbaum]
clb_calg [instance, in Undecidability.FOLC.Lindenbaum]
clb_alg [instance, in Undecidability.FOLC.Lindenbaum]
close [definition, in Undecidability.FOLC.FullFOL]
close [definition, in Undecidability.FOLC.FOL]
closed [definition, in Undecidability.FOLC.FullFOL]
closed [definition, in Undecidability.FOLC.FOL]
closed_T_extend [lemma, in Undecidability.FOLC.FullFOL]
closed_T [definition, in Undecidability.FOLC.FullFOL]
closed_T_extend [lemma, in Undecidability.FOLC.FOL]
closed_T [definition, in Undecidability.FOLC.FOL]
closed_F [lemma, in Undecidability.FOLC.BPCP_FOL]
closed_Th [lemma, in Undecidability.FOLC.WKL]
close_closed [lemma, in Undecidability.FOLC.FullFOL]
close_closed [lemma, in Undecidability.FOLC.FOL]
close_extract [lemma, in Undecidability.FOLC.FullND]
close_valid_L [lemma, in Undecidability.FOLC.GenTarski]
close_extract [lemma, in Undecidability.FOLC.ND]
ClosingBigImp [section, in Undecidability.FOLC.GenTarski]
ClosingValidity [section, in Undecidability.FOLC.GenTarski]
ClosingValidity.C [variable, in Undecidability.FOLC.GenTarski]
ClosingValidity.HC [variable, in Undecidability.FOLC.GenTarski]
ClosingValidity.Hprv [variable, in Undecidability.FOLC.GenTarski]
ClosingValidity.phi [variable, in Undecidability.FOLC.GenTarski]
ClosingValidity.T [variable, in Undecidability.FOLC.GenTarski]
CND_BPCP [lemma, in Undecidability.FOLC.BPCP_CND]
cod [definition, in Undecidability.FOLC.axioms]
cod_comp [definition, in Undecidability.FOLC.axioms]
cod_ext' [definition, in Undecidability.FOLC.axioms]
cod_ext [definition, in Undecidability.FOLC.axioms]
cod_id [definition, in Undecidability.FOLC.axioms]
cod_map [definition, in Undecidability.FOLC.axioms]
compactness [definition, in Undecidability.FOLC.WKL]
compact_implies_WKL_D [lemma, in Undecidability.FOLC.WKL]
compact_OM_implies_WKL [lemma, in Undecidability.FOLC.WKL]
compact_OM_implies_WKL' [lemma, in Undecidability.FOLC.WKL]
compact_implies_WKL [lemma, in Undecidability.FOLC.WKL]
compact_implies_WKL' [lemma, in Undecidability.FOLC.WKL]
compact_DM_WKLD [lemma, in Undecidability.FOLC.WKL]
compact_OM_WKL [lemma, in Undecidability.FOLC.WKL]
compact_DM_WKL [lemma, in Undecidability.FOLC.WKL]
compact_standard [lemma, in Undecidability.FOLC.WKL]
compComp_form [lemma, in Undecidability.FOLC.FullSyntax]
compComp_form [lemma, in Undecidability.FOLC.Syntax]
compComp_term [lemma, in Undecidability.FOLC.Terms]
compComp'_form [lemma, in Undecidability.FOLC.FullSyntax]
compComp'_form [lemma, in Undecidability.FOLC.Syntax]
compComp'_term [lemma, in Undecidability.FOLC.Terms]
CompleteHeytingAlgebra [record, in Undecidability.FOLC.Heyting]
Completeness [section, in Undecidability.FOLC.GenCompleteness]
completeness [definition, in Undecidability.FOLC.WKL]
completeness_expl [lemma, in Undecidability.FOLC.GenCompleteness]
completeness_standard_stability [lemma, in Undecidability.FOLC.GenCompleteness]
completeness_transport [lemma, in Undecidability.FOLC.Analysis]
completeness_iff_XM [lemma, in Undecidability.FOLC.Analysis]
completeness_enum_iff_MP [lemma, in Undecidability.FOLC.Analysis]
completeness_context_iff_MPL [lemma, in Undecidability.FOLC.Analysis]
Completeness.BotModel [section, in Undecidability.FOLC.GenCompleteness]
Completeness.BotModel.T [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.BotModel.T_closed [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes [section, in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.Hphi [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.HT [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.phi [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.T [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentCompleteness [section, in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel [section, in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.GBot [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.GBot_closed [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.T [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.T_closed [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness [section, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.He [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.Hphi [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.HT [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.L [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.mp [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.phi [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.T [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes [section, in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.Hphi [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.HT [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.phi [variable, in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.T [variable, in Undecidability.FOLC.GenCompleteness]
completion_calgebra [definition, in Undecidability.FOLC.Heyting]
completion_algebra [definition, in Undecidability.FOLC.Heyting]
Composition [section, in Undecidability.FOLC.GenConstructions]
compSubstSubst_form [definition, in Undecidability.FOLC.FullSyntax]
compSubstSubst_form [definition, in Undecidability.FOLC.Syntax]
compSubstSubst_term [definition, in Undecidability.FOLC.Terms]
computable_L_sprvie [instance, in Undecidability.FOLC.LEnum]
computable_f9 [instance, in Undecidability.FOLC.LEnum]
computable_f8 [instance, in Undecidability.FOLC.LEnum]
computable_ineqb [instance, in Undecidability.FOLC.LEnum]
computable_enum_eqb [instance, in Undecidability.FOLC.LEnum]
computable_option_form_eqb [instance, in Undecidability.FOLC.LEnum]
computable_list_form_eqb [instance, in Undecidability.FOLC.LEnum]
computable_form_eqb [instance, in Undecidability.FOLC.LEnum]
computable_list_eqb [instance, in Undecidability.FOLC.LEnum]
computable_term_eqb [instance, in Undecidability.FOLC.LEnum]
comp_modex [lemma, in Undecidability.FOLC.WKL]
congr_Ex [definition, in Undecidability.FOLC.FullSyntax]
congr_All [definition, in Undecidability.FOLC.FullSyntax]
congr_Disj [definition, in Undecidability.FOLC.FullSyntax]
congr_Conj [definition, in Undecidability.FOLC.FullSyntax]
congr_Impl [definition, in Undecidability.FOLC.FullSyntax]
congr_Pred [definition, in Undecidability.FOLC.FullSyntax]
congr_Fal [definition, in Undecidability.FOLC.FullSyntax]
congr_All [definition, in Undecidability.FOLC.Syntax]
congr_Impl [definition, in Undecidability.FOLC.Syntax]
congr_Pred [definition, in Undecidability.FOLC.Syntax]
congr_Fal [definition, in Undecidability.FOLC.Syntax]
congr_Func [definition, in Undecidability.FOLC.Terms]
Conj [constructor, in Undecidability.FOLC.FullSyntax]
cons [definition, in Undecidability.FOLC.KripkeCompleteness]
Consistency [section, in Undecidability.FOLC.Consistency]
Consistency [lemma, in Undecidability.FOLC.GenTarski]
Consistency [library]
consistency_inheritance [lemma, in Undecidability.FOLC.Consistency]
Consistency.Classical [section, in Undecidability.FOLC.Consistency]
Consistency.Classical.XM [variable, in Undecidability.FOLC.Consistency]
consistent [definition, in Undecidability.FOLC.Consistency]
consistent_join_step [lemma, in Undecidability.FOLC.GenConstructions]
consistent_max_out2 [lemma, in Undecidability.FOLC.Consistency]
consistent_max_impl [lemma, in Undecidability.FOLC.Consistency]
consistent_max_out [lemma, in Undecidability.FOLC.Consistency]
consistent_neg2 [lemma, in Undecidability.FOLC.Consistency]
consistent_neg [lemma, in Undecidability.FOLC.Consistency]
consistent_prv [lemma, in Undecidability.FOLC.Consistency]
consistent_max [definition, in Undecidability.FOLC.Consistency]
constraint [definition, in Undecidability.FOLC.FullTarski]
constraint [definition, in Undecidability.FOLC.GenTarski]
ConstructionInputs [record, in Undecidability.FOLC.GenConstructions]
ConstructionOutputs [record, in Undecidability.FOLC.GenConstructions]
construct_construction [lemma, in Undecidability.FOLC.GenConstructions]
cons_ctx [definition, in Undecidability.FOLC.KripkeCompleteness]
cons'' [definition, in Undecidability.FOLC.LEnum]
cons''' [definition, in Undecidability.FOLC.LEnum]
contains [definition, in Undecidability.FOLC.FullFOL]
contains [definition, in Undecidability.FOLC.FOL]
contains_extend3 [lemma, in Undecidability.FOLC.FullFOL]
contains_extend2 [lemma, in Undecidability.FOLC.FullFOL]
contains_extend1 [lemma, in Undecidability.FOLC.FullFOL]
contains_app [lemma, in Undecidability.FOLC.FullFOL]
contains_cons2 [lemma, in Undecidability.FOLC.FullFOL]
contains_cons [lemma, in Undecidability.FOLC.FullFOL]
contains_nil [lemma, in Undecidability.FOLC.FullFOL]
contains_L [definition, in Undecidability.FOLC.FullFOL]
contains_extend3 [lemma, in Undecidability.FOLC.FOL]
contains_extend2 [lemma, in Undecidability.FOLC.FOL]
contains_extend1 [lemma, in Undecidability.FOLC.FOL]
contains_app [lemma, in Undecidability.FOLC.FOL]
contains_cons2 [lemma, in Undecidability.FOLC.FOL]
contains_cons [lemma, in Undecidability.FOLC.FOL]
contains_nil [lemma, in Undecidability.FOLC.FOL]
contains_L [definition, in Undecidability.FOLC.FOL]
context_shift [lemma, in Undecidability.FOLC.FullSequent]
Contr [constructor, in Undecidability.FOLC.Gentzen]
Contr [constructor, in Undecidability.FOLC.FullSequent]
converges_eva [lemma, in Undecidability.FOLC.Markov]
convert [definition, in Undecidability.FOLC.DeMorgan]
convert_embed [lemma, in Undecidability.FOLC.DeMorgan]
con_subs [definition, in Undecidability.FOLC.FullTarski]
con_T_correct [lemma, in Undecidability.FOLC.Stability]
con_T [definition, in Undecidability.FOLC.Stability]
con_subs [definition, in Undecidability.FOLC.GenTarski]
countable [definition, in Undecidability.FOLC.WKL]
count_conjs [definition, in Undecidability.FOLC.WKL]
count_sig [definition, in Undecidability.FOLC.WKL]
CO_iff_EM_WKL [lemma, in Undecidability.FOLC.WKL]
cprv [definition, in Undecidability.FOLC.Markov]
cprv_iprv_stable [lemma, in Undecidability.FOLC.Markov]
cprv_iprv [lemma, in Undecidability.FOLC.Markov]
cprv_red [lemma, in Undecidability.FOLC.BPCP_CND]
Ctx [constructor, in Undecidability.FOLC.FullND]
Ctx [constructor, in Undecidability.FOLC.ND]
ctx_incl [definition, in Undecidability.FOLC.KripkeCompleteness]
ctx_S [definition, in Undecidability.FOLC.BPCP_FOL]
ctx_in [lemma, in Undecidability.FOLC.FullSequent]
ctx_out [lemma, in Undecidability.FOLC.FullSequent]
cutfree_seq_ND [lemma, in Undecidability.FOLC.Gentzen]
cycle_shift_subject [lemma, in Undecidability.FOLC.FullND]
cycle_shift_shift [lemma, in Undecidability.FOLC.FullND]
cycle_shift [definition, in Undecidability.FOLC.FullND]
cycle_shift_subject [lemma, in Undecidability.FOLC.FullSequent]
cycle_shift_shift [lemma, in Undecidability.FOLC.FullSequent]
cycle_shift [definition, in Undecidability.FOLC.FullSequent]
cycle_shift_subject [lemma, in Undecidability.FOLC.ND]
cycle_shift_shift [lemma, in Undecidability.FOLC.ND]
cycle_shift [definition, in Undecidability.FOLC.ND]
D
Dadmission [definition, in Undecidability.FOLC.SDialogues]Dadmission' [definition, in Undecidability.FOLC.SDialogues]
DAll [constructor, in Undecidability.FOLC.DialogFull]
DAll [constructor, in Undecidability.FOLC.DialogFragment]
DAndL [constructor, in Undecidability.FOLC.DialogFull]
DAndR [constructor, in Undecidability.FOLC.DialogFull]
Dchallenge [definition, in Undecidability.FOLC.SDialogues]
Dchallenge' [definition, in Undecidability.FOLC.SDialogues]
dclosed [definition, in Undecidability.FOLC.Heyting]
dcompleteness [lemma, in Undecidability.FOLC.Sorensen]
Ddeferred [definition, in Undecidability.FOLC.SDialogues]
Ddeferred' [definition, in Undecidability.FOLC.SDialogues]
DE [constructor, in Undecidability.FOLC.FullND]
decidable [definition, in Undecidability.FOLC.WKL]
decidable_to_decidable_data [lemma, in Undecidability.FOLC.WKL]
decidable_to_decidable [lemma, in Undecidability.FOLC.WKL]
decidable_to_decidable_n [lemma, in Undecidability.FOLC.WKL]
decidable_to_omniscient [lemma, in Undecidability.FOLC.WKL]
decidable_model [definition, in Undecidability.FOLC.WKL]
dec_f [projection, in Undecidability.FOLC.SDialogues]
dec_form [instance, in Undecidability.FOLC.FullFOL]
dec_term [instance, in Undecidability.FOLC.FullFOL]
dec_vec [instance, in Undecidability.FOLC.FullFOL]
dec_vec_in [lemma, in Undecidability.FOLC.FullFOL]
dec_sig_ext_Preds [instance, in Undecidability.FOLC.FOL]
dec_sig_ext_Funcs [instance, in Undecidability.FOLC.FOL]
dec_form [instance, in Undecidability.FOLC.FOL]
dec_term [instance, in Undecidability.FOLC.FOL]
dec_vec [instance, in Undecidability.FOLC.FOL]
dec_vec_in [lemma, in Undecidability.FOLC.FOL]
dec_f [projection, in Undecidability.FOLC.Sorensen]
dec2bool_iff [lemma, in Undecidability.FOLC.WKL]
Def [constructor, in Undecidability.FOLC.SDialogues]
Def [constructor, in Undecidability.FOLC.Sorensen]
defense [projection, in Undecidability.FOLC.SDialogues]
defense [projection, in Undecidability.FOLC.Sorensen]
defense_form [inductive, in Undecidability.FOLC.DialogFull]
defense_form [inductive, in Undecidability.FOLC.DialogFragment]
deferred [definition, in Undecidability.FOLC.SDialogues]
deferred [definition, in Undecidability.FOLC.Sorensen]
DeMorgan [library]
DExt [constructor, in Undecidability.FOLC.DialogFull]
DGame [section, in Undecidability.FOLC.Sorensen]
DGame.f [variable, in Undecidability.FOLC.Sorensen]
DGame.R [variable, in Undecidability.FOLC.Sorensen]
DialogFragment [section, in Undecidability.FOLC.DialogFragment]
DialogFragment [library]
DialogFull [section, in Undecidability.FOLC.DialogFull]
DialogFull [library]
DialogFull.eq_dec_Preds [variable, in Undecidability.FOLC.DialogFull]
DialogFull.eq_dec_Funcs [variable, in Undecidability.FOLC.DialogFull]
DImpl [constructor, in Undecidability.FOLC.DialogFull]
DImpl [constructor, in Undecidability.FOLC.DialogFragment]
discrete_sig [definition, in Undecidability.FOLC.Markov]
Disj [constructor, in Undecidability.FOLC.FullSyntax]
DI1 [constructor, in Undecidability.FOLC.FullND]
DI2 [constructor, in Undecidability.FOLC.FullND]
DlA [constructor, in Undecidability.FOLC.SDialogues]
DlA' [definition, in Undecidability.FOLC.SDialogues]
DlA'' [definition, in Undecidability.FOLC.SDialogues]
DlC [constructor, in Undecidability.FOLC.SDialogues]
DlC' [definition, in Undecidability.FOLC.SDialogues]
DlD [constructor, in Undecidability.FOLC.SDialogues]
DlD' [definition, in Undecidability.FOLC.SDialogues]
DlD'' [definition, in Undecidability.FOLC.SDialogues]
Dlift [inductive, in Undecidability.FOLC.SDialogues]
Dlift_le_wf [lemma, in Undecidability.FOLC.SDialogues]
Dlift_le [definition, in Undecidability.FOLC.SDialogues]
Dlift_le' [definition, in Undecidability.FOLC.SDialogues]
DM [definition, in Undecidability.FOLC.DeMorgan]
DM [section, in Undecidability.FOLC.DeMorgan]
DM [definition, in Undecidability.FOLC.WKL]
DMT [definition, in Undecidability.FOLC.DeMorgan]
DMTT [definition, in Undecidability.FOLC.DeMorgan]
DMT_sat_back [lemma, in Undecidability.FOLC.DeMorgan]
DMT_closed [lemma, in Undecidability.FOLC.DeMorgan]
DMT_unused [lemma, in Undecidability.FOLC.DeMorgan]
DMT_incl [lemma, in Undecidability.FOLC.DeMorgan]
DMT_valid [lemma, in Undecidability.FOLC.DeMorgan]
DMT_sat [lemma, in Undecidability.FOLC.DeMorgan]
DMT_prv [lemma, in Undecidability.FOLC.DeMorgan]
DMT_subst [lemma, in Undecidability.FOLC.DeMorgan]
DM_prv [lemma, in Undecidability.FOLC.DeMorgan]
DN [definition, in Undecidability.FOLC.DeMorgan]
DN [lemma, in Undecidability.FOLC.FullND]
DN [definition, in Undecidability.FOLC.Stability]
DN [lemma, in Undecidability.FOLC.ND]
dnQ [definition, in Undecidability.FOLC.BPCP_CND]
dnt [definition, in Undecidability.FOLC.FullND]
DNT [section, in Undecidability.FOLC.FullND]
dnt [definition, in Undecidability.FOLC.ND]
DNT [section, in Undecidability.FOLC.ND]
dnt_to_CE [lemma, in Undecidability.FOLC.FullND]
dnt_remove_ctx [lemma, in Undecidability.FOLC.FullND]
dnt_CE [lemma, in Undecidability.FOLC.FullND]
dnt_to_IE [lemma, in Undecidability.FOLC.FullND]
dnt_float [lemma, in Undecidability.FOLC.FullND]
dnt_subst [lemma, in Undecidability.FOLC.FullND]
dnt_to_TCE [lemma, in Undecidability.FOLC.ND]
dnt_to_CE [lemma, in Undecidability.FOLC.ND]
dnt_remove_ctx [lemma, in Undecidability.FOLC.ND]
dnt_unused [lemma, in Undecidability.FOLC.ND]
dnt_CE [lemma, in Undecidability.FOLC.ND]
dnt_to_TIE [lemma, in Undecidability.FOLC.ND]
dnt_to_IE [lemma, in Undecidability.FOLC.ND]
dnt_float [lemma, in Undecidability.FOLC.ND]
dnt_subst [lemma, in Undecidability.FOLC.ND]
dn_inherit [lemma, in Undecidability.FOLC.GenCompleteness]
dn_to_sta [lemma, in Undecidability.FOLC.Stability]
DN_T [lemma, in Undecidability.FOLC.ND]
DOAtk [constructor, in Undecidability.FOLC.Sorensen]
DODef [constructor, in Undecidability.FOLC.Sorensen]
domove [inductive, in Undecidability.FOLC.Sorensen]
DOrL [constructor, in Undecidability.FOLC.DialogFull]
DOrR [constructor, in Undecidability.FOLC.DialogFull]
Double [lemma, in Undecidability.FOLC.BPCP_CND]
Double' [lemma, in Undecidability.FOLC.BPCP_CND]
down [definition, in Undecidability.FOLC.Heyting]
down_inf [lemma, in Undecidability.FOLC.Heyting]
down_impl [lemma, in Undecidability.FOLC.Heyting]
down_join [lemma, in Undecidability.FOLC.Heyting]
down_meet [lemma, in Undecidability.FOLC.Heyting]
down_top [lemma, in Undecidability.FOLC.Heyting]
down_bot [lemma, in Undecidability.FOLC.Heyting]
down_mono [lemma, in Undecidability.FOLC.Heyting]
down_inj [lemma, in Undecidability.FOLC.Heyting]
down_normal [lemma, in Undecidability.FOLC.Heyting]
DP [lemma, in Undecidability.FOLC.FullND]
DP [lemma, in Undecidability.FOLC.ND]
DPAtk [constructor, in Undecidability.FOLC.Sorensen]
DPDef [constructor, in Undecidability.FOLC.Sorensen]
DPexp1 [definition, in Undecidability.FOLC.GenConstructions]
DPexp2 [definition, in Undecidability.FOLC.GenConstructions]
DPexp3 [definition, in Undecidability.FOLC.GenConstructions]
dpmove [inductive, in Undecidability.FOLC.Sorensen]
Dprv [inductive, in Undecidability.FOLC.SDialogues]
Dprv [inductive, in Undecidability.FOLC.Sorensen]
Dprv_svalid [lemma, in Undecidability.FOLC.SDialogues]
Dprv_swin [lemma, in Undecidability.FOLC.SDialogues]
Dprv_fprv_equiv [lemma, in Undecidability.FOLC.DialogFull]
Dprv_fprv [lemma, in Undecidability.FOLC.DialogFull]
Dprv_fprv' [lemma, in Undecidability.FOLC.DialogFull]
Dprv_ND [lemma, in Undecidability.FOLC.DialogFragment]
Dprv_just [lemma, in Undecidability.FOLC.Sorensen]
Dprv_ax [lemma, in Undecidability.FOLC.Sorensen]
Dprv_echo [lemma, in Undecidability.FOLC.Sorensen]
Dprv_exp [lemma, in Undecidability.FOLC.Sorensen]
Dprv_defend [lemma, in Undecidability.FOLC.Sorensen]
Dprv_weak [lemma, in Undecidability.FOLC.Sorensen]
Dprv_ewin [lemma, in Undecidability.FOLC.Sorensen]
droppable [definition, in Undecidability.FOLC.GenTarski]
droppable_BL [lemma, in Undecidability.FOLC.GenTarski]
droppable_E [lemma, in Undecidability.FOLC.GenTarski]
droppable_S [lemma, in Undecidability.FOLC.GenTarski]
droppable_exploding_bot [lemma, in Undecidability.FOLC.GenTarski]
droppable_standard_bot [lemma, in Undecidability.FOLC.GenTarski]
droppable_classical [lemma, in Undecidability.FOLC.GenTarski]
drop_interp [definition, in Undecidability.FOLC.GenTarski]
drop_interp'_sat [lemma, in Undecidability.FOLC.GenTarski]
drop_interp'_eval [lemma, in Undecidability.FOLC.GenTarski]
drop_interp' [definition, in Undecidability.FOLC.GenTarski]
drv_prv [lemma, in Undecidability.FOLC.BPCP_FOL]
drv_val [lemma, in Undecidability.FOLC.BPCP_FOL]
dstate [definition, in Undecidability.FOLC.Sorensen]
dummy_sig [definition, in Undecidability.FOLC.Stability]
dummy_SM [lemma, in Undecidability.FOLC.GenTarski]
dummy_xm [lemma, in Undecidability.FOLC.GenTarski]
dummy_interp [definition, in Undecidability.FOLC.GenTarski]
dvalid [definition, in Undecidability.FOLC.Sorensen]
dwin_Dprv [lemma, in Undecidability.FOLC.Sorensen]
dwin_Dprv_embed [definition, in Undecidability.FOLC.Sorensen]
dwin_strat [inductive, in Undecidability.FOLC.Sorensen]
DWS [constructor, in Undecidability.FOLC.Sorensen]
E
ecompleteness [lemma, in Undecidability.FOLC.Sorensen]econsistency_trans [lemma, in Undecidability.FOLC.GenConstructions]
econsistency_inheritance [lemma, in Undecidability.FOLC.GenConstructions]
econsistent [definition, in Undecidability.FOLC.GenConstructions]
econsistent_prv [lemma, in Undecidability.FOLC.GenConstructions]
econsistent_Omega [lemma, in Undecidability.FOLC.GenConstructions]
econsistent_join_sub [lemma, in Undecidability.FOLC.GenConstructions]
econsistent_join [definition, in Undecidability.FOLC.GenConstructions]
eequiv [lemma, in Undecidability.FOLC.Sorensen]
EGame [section, in Undecidability.FOLC.Sorensen]
EGame.f [variable, in Undecidability.FOLC.Sorensen]
EGame.R [variable, in Undecidability.FOLC.Sorensen]
elem_prv [lemma, in Undecidability.FOLC.FullND]
elem_prv [lemma, in Undecidability.FOLC.ND]
el_at_pos [lemma, in Undecidability.FOLC.Enumeration]
EM [definition, in Undecidability.FOLC.GenTarski]
embed [definition, in Undecidability.FOLC.Extend]
embed [definition, in Undecidability.FOLC.DeMorgan]
embed [definition, in Undecidability.FOLC.Gentzen]
embed [definition, in Undecidability.FOLC.Heyting]
embed_subst [lemma, in Undecidability.FOLC.Extend]
embed_subst_term [lemma, in Undecidability.FOLC.Extend]
embed_term [definition, in Undecidability.FOLC.Extend]
embed_prv [lemma, in Undecidability.FOLC.DeMorgan]
embed_subst [lemma, in Undecidability.FOLC.DeMorgan]
embed_DMT [lemma, in Undecidability.FOLC.DeMorgan]
enc [definition, in Undecidability.FOLC.BPCP_FOL]
enum [projection, in Undecidability.FOLC.GenConstructions]
Enumerability [section, in Undecidability.FOLC.FOL]
Enumerability [section, in Undecidability.FOLC.ND]
Enumerability.enum_Preds [variable, in Undecidability.FOLC.FOL]
Enumerability.enum_Funcs [variable, in Undecidability.FOLC.FOL]
enumerable_sig [definition, in Undecidability.FOLC.Markov]
Enumeration [section, in Undecidability.FOLC.Enumeration]
Enumeration [library]
enumeration_stability [lemma, in Undecidability.FOLC.Stability]
enumeration_semi_decidable [lemma, in Undecidability.FOLC.Stability]
Enumeration.Hlen [variable, in Undecidability.FOLC.Enumeration]
Enumeration.X [variable, in Undecidability.FOLC.Enumeration]
enumT_sum [instance, in Undecidability.FOLC.GenCompleteness]
enumT_term [instance, in Undecidability.FOLC.Markov]
enumT_sig_ext_Preds [instance, in Undecidability.FOLC.FOL]
enumT_sig_ext_Funcs [instance, in Undecidability.FOLC.FOL]
enumT_form [instance, in Undecidability.FOLC.FOL]
enumT_term [instance, in Undecidability.FOLC.FOL]
enumT_vec [instance, in Undecidability.FOLC.FOL]
enumT_unit [instance, in Undecidability.FOLC.WKL]
enum_unused [projection, in Undecidability.FOLC.GenConstructions]
enum_enum [projection, in Undecidability.FOLC.GenConstructions]
enum_tmap [lemma, in Undecidability.FOLC.FullFOL]
enum_inj.H [variable, in Undecidability.FOLC.Markov]
enum_inj.XD [variable, in Undecidability.FOLC.Markov]
enum_inj.X [variable, in Undecidability.FOLC.Markov]
enum_inj [section, in Undecidability.FOLC.Markov]
enum_halt [lemma, in Undecidability.FOLC.Markov]
enum_tmap [lemma, in Undecidability.FOLC.FOL]
enum_stprv [lemma, in Undecidability.FOLC.Gentzen]
enum_sprv [lemma, in Undecidability.FOLC.Gentzen]
enum_tsat_T [lemma, in Undecidability.FOLC.Stability]
enum_T_map_closed_homo [lemma, in Undecidability.FOLC.Stability]
enum_T_map_closed_closing [lemma, in Undecidability.FOLC.Stability]
enum_T [definition, in Undecidability.FOLC.Stability]
enum_sprvie [lemma, in Undecidability.FOLC.LEnum]
enum_sprv [lemma, in Undecidability.FOLC.LEnum]
enum_eqb [definition, in Undecidability.FOLC.LEnum]
enum_form' [instance, in Undecidability.FOLC.LEnum]
enum_wf [lemma, in Undecidability.FOLC.LEnum]
enum_term' [instance, in Undecidability.FOLC.LEnum]
enum_tprv [lemma, in Undecidability.FOLC.ND]
enum_containsL [lemma, in Undecidability.FOLC.ND]
enum_p [lemma, in Undecidability.FOLC.ND]
enum_el [lemma, in Undecidability.FOLC.ND]
enum_prv [lemma, in Undecidability.FOLC.ND]
env [definition, in Undecidability.FOLC.GenTarski]
EOAtk [constructor, in Undecidability.FOLC.Sorensen]
EOCounter [constructor, in Undecidability.FOLC.Sorensen]
EODef [constructor, in Undecidability.FOLC.Sorensen]
eomove [inductive, in Undecidability.FOLC.Sorensen]
EPAtk [constructor, in Undecidability.FOLC.Sorensen]
EPDef [constructor, in Undecidability.FOLC.Sorensen]
epmove [inductive, in Undecidability.FOLC.Sorensen]
EqDec [section, in Undecidability.FOLC.FullFOL]
EqDec [section, in Undecidability.FOLC.FOL]
EqDec.eq_dec_Preds [variable, in Undecidability.FOLC.FullFOL]
EqDec.eq_dec_Funcs [variable, in Undecidability.FOLC.FullFOL]
EqDec.eq_dec_Preds [variable, in Undecidability.FOLC.FOL]
EqDec.eq_dec_Funcs [variable, in Undecidability.FOLC.FOL]
eqH [definition, in Undecidability.FOLC.Heyting]
equiv_HA_refl [instance, in Undecidability.FOLC.Heyting]
equiv_HA [definition, in Undecidability.FOLC.Heyting]
eq_incl [lemma, in Undecidability.FOLC.DialogFull]
eq_dec_term [instance, in Undecidability.FOLC.Markov]
eq_incl [lemma, in Undecidability.FOLC.DialogFragment]
esoundness [lemma, in Undecidability.FOLC.Sorensen]
eval [definition, in Undecidability.FOLC.GenTarski]
evalid [definition, in Undecidability.FOLC.Sorensen]
evalid_fprv_equiv [lemma, in Undecidability.FOLC.DialogFull]
eval_retract [lemma, in Undecidability.FOLC.Extend]
eval_ident_fragment [lemma, in Undecidability.FOLC.GenCompleteness]
eval_ident [lemma, in Undecidability.FOLC.GenCompleteness]
eval_id [lemma, in Undecidability.FOLC.KripkeCompleteness]
eval_comp [lemma, in Undecidability.FOLC.FullTarski]
eval_ext [lemma, in Undecidability.FOLC.FullTarski]
eval_comp [lemma, in Undecidability.FOLC.GenTarski]
eval_ext [lemma, in Undecidability.FOLC.GenTarski]
eval_ext_unused [lemma, in Undecidability.FOLC.GenTarski]
ewin_Dprv [lemma, in Undecidability.FOLC.Sorensen]
ewin_strat [inductive, in Undecidability.FOLC.Sorensen]
EWS [constructor, in Undecidability.FOLC.Sorensen]
Ex [constructor, in Undecidability.FOLC.FullSyntax]
ExE [constructor, in Undecidability.FOLC.FullND]
ExE [lemma, in Undecidability.FOLC.ND]
ExE' [lemma, in Undecidability.FOLC.FullND]
ExI [constructor, in Undecidability.FOLC.FullND]
ExI [lemma, in Undecidability.FOLC.ND]
exists_quasi_path [lemma, in Undecidability.FOLC.WKL]
ExI' [lemma, in Undecidability.FOLC.FullND]
ExL [constructor, in Undecidability.FOLC.FullSequent]
Exp [definition, in Undecidability.FOLC.GenConstructions]
exp [definition, in Undecidability.FOLC.GenConstructions]
Exp [constructor, in Undecidability.FOLC.FullND]
Exp [constructor, in Undecidability.FOLC.FullSequent]
Exp [constructor, in Undecidability.FOLC.ND]
expl [constructor, in Undecidability.FOLC.FullND]
expl [constructor, in Undecidability.FOLC.ND]
exploding [definition, in Undecidability.FOLC.GenConstructions]
exploding_inherit [lemma, in Undecidability.FOLC.GenConstructions]
exploding_bot [definition, in Undecidability.FOLC.GenTarski]
Exp_exploding [lemma, in Undecidability.FOLC.GenConstructions]
Exp_closed [lemma, in Undecidability.FOLC.GenConstructions]
Exp_econsistent [lemma, in Undecidability.FOLC.GenConstructions]
Exp_sub [lemma, in Undecidability.FOLC.GenConstructions]
exp_axiom_lift [lemma, in Undecidability.FOLC.GenConstructions]
exp_axiom [definition, in Undecidability.FOLC.GenConstructions]
ExR [constructor, in Undecidability.FOLC.FullSequent]
extend [definition, in Undecidability.FOLC.FullFOL]
extend [definition, in Undecidability.FOLC.FOL]
Extend [library]
ext_c'_unused [lemma, in Undecidability.FOLC.FOL]
ext_c'_unused_term [lemma, in Undecidability.FOLC.FOL]
ext_c [definition, in Undecidability.FOLC.FOL]
ext_c' [definition, in Undecidability.FOLC.FOL]
ext_form [definition, in Undecidability.FOLC.FullSyntax]
ext_form [definition, in Undecidability.FOLC.Syntax]
ext_form' [lemma, in Undecidability.FOLC.LEnum]
ext_term' [lemma, in Undecidability.FOLC.LEnum]
ext_term [definition, in Undecidability.FOLC.Terms]
E_S_subsumption [lemma, in Undecidability.FOLC.GenTarski]
F
f [definition, in Undecidability.FOLC.Markov]F [definition, in Undecidability.FOLC.BPCP_FOL]
Fal [constructor, in Undecidability.FOLC.FullSyntax]
Fal [constructor, in Undecidability.FOLC.Syntax]
fAll [definition, in Undecidability.FOLC.WKL]
fAll_sat [lemma, in Undecidability.FOLC.WKL]
fAll_sat' [lemma, in Undecidability.FOLC.WKL]
False_enumT [instance, in Undecidability.FOLC.Stability]
Fal' [constructor, in Undecidability.FOLC.LEnum]
fExists [definition, in Undecidability.FOLC.WKL]
fExists_sat [lemma, in Undecidability.FOLC.WKL]
fExists_sat' [lemma, in Undecidability.FOLC.WKL]
fin [abbreviation, in Undecidability.FOLC.unscoped]
find_unused_L [lemma, in Undecidability.FOLC.FullFOL]
find_unused [lemma, in Undecidability.FOLC.FullFOL]
find_unused_L [lemma, in Undecidability.FOLC.FOL]
find_unused [lemma, in Undecidability.FOLC.FOL]
find_unused_term [lemma, in Undecidability.FOLC.Terms]
FiniteCompleteness [section, in Undecidability.FOLC.GenCompleteness]
fin_minus [definition, in Undecidability.FOLC.FOL]
fin_T_to_context [lemma, in Undecidability.FOLC.Stability]
fin_T_con_T [lemma, in Undecidability.FOLC.Stability]
fin_T_map_closed [lemma, in Undecidability.FOLC.Stability]
fin_T [definition, in Undecidability.FOLC.Stability]
fix_sig [section, in Undecidability.FOLC.FullSyntax]
fix_sig [section, in Undecidability.FOLC.Syntax]
fix_sig [section, in Undecidability.FOLC.Terms]
flat_map_app [lemma, in Undecidability.FOLC.Enumeration]
focus_el [lemma, in Undecidability.FOLC.FullSequent]
FOL [section, in Undecidability.FOLC.FOL]
FOL [library]
FOL.ContainsAutomation [section, in Undecidability.FOLC.FOL]
_ ⋄ _ [notation, in Undecidability.FOLC.FOL]
_ ∈ _ [notation, in Undecidability.FOLC.FOL]
_ ⊑ _ [notation, in Undecidability.FOLC.FOL]
_ ⊏ _ [notation, in Undecidability.FOLC.FOL]
Forall [inductive, in Undecidability.FOLC.Terms]
Forall_cons [constructor, in Undecidability.FOLC.Terms]
Forall_nil [constructor, in Undecidability.FOLC.Terms]
Forall_app [lemma, in Undecidability.FOLC.WKL]
Forall2_length [lemma, in Undecidability.FOLC.WKL]
Forall2_In1 [lemma, in Undecidability.FOLC.WKL]
Forall2_In [lemma, in Undecidability.FOLC.WKL]
form [inductive, in Undecidability.FOLC.FullSyntax]
form [inductive, in Undecidability.FOLC.Syntax]
form_ind_subst [lemma, in Undecidability.FOLC.FullFOL]
form_shift [definition, in Undecidability.FOLC.FullFOL]
form_rules [instance, in Undecidability.FOLC.DialogFull]
form_shift [definition, in Undecidability.FOLC.FOL]
form_ind_subst [lemma, in Undecidability.FOLC.FOL]
form_ind_subst' [lemma, in Undecidability.FOLC.FullND]
form_shift [definition, in Undecidability.FOLC.FullND]
form_eqb_spec [lemma, in Undecidability.FOLC.LEnum]
form_eqb [definition, in Undecidability.FOLC.LEnum]
form_shift' [definition, in Undecidability.FOLC.LEnum]
form_enum_fresh [lemma, in Undecidability.FOLC.Enumeration]
form_enum_enumerates [lemma, in Undecidability.FOLC.Enumeration]
form_enum [definition, in Undecidability.FOLC.Enumeration]
form_rules [instance, in Undecidability.FOLC.DialogFragment]
form' [inductive, in Undecidability.FOLC.LEnum]
fprv [inductive, in Undecidability.FOLC.FullSequent]
fprv_defend [lemma, in Undecidability.FOLC.DialogFull]
fprv_Dprv [lemma, in Undecidability.FOLC.DialogFull]
FullFOL [section, in Undecidability.FOLC.FullFOL]
FullFOL [library]
FullFOL.ContainsAutomation [section, in Undecidability.FOLC.FullFOL]
_ ⋄ _ [notation, in Undecidability.FOLC.FullFOL]
_ ∈ _ [notation, in Undecidability.FOLC.FullFOL]
_ ⊑ _ [notation, in Undecidability.FOLC.FullFOL]
_ ⊏ _ [notation, in Undecidability.FOLC.FullFOL]
↑ [notation, in Undecidability.FOLC.FullFOL]
FullND [library]
FullSequent [section, in Undecidability.FOLC.FullSequent]
FullSequent [library]
_ ⊢f _ [notation, in Undecidability.FOLC.FullSequent]
⋁ _ [notation, in Undecidability.FOLC.FullSequent]
FullSyntax [library]
FullTarski [library]
full_completeness [lemma, in Undecidability.FOLC.DeMorgan]
Func [constructor, in Undecidability.FOLC.Terms]
funcomp [definition, in Undecidability.FOLC.axioms]
funcomp [definition, in Undecidability.FOLC.unscoped]
Funcs [projection, in Undecidability.FOLC.Terms]
Func_cast [lemma, in Undecidability.FOLC.LEnum]
Func' [constructor, in Undecidability.FOLC.LEnum]
fun_ar [projection, in Undecidability.FOLC.Terms]
F_sup [projection, in Undecidability.FOLC.Heyting]
F_inf [projection, in Undecidability.FOLC.Heyting]
F_impl [projection, in Undecidability.FOLC.Heyting]
F_join [projection, in Undecidability.FOLC.Heyting]
F_meet [projection, in Undecidability.FOLC.Heyting]
F_bot [projection, in Undecidability.FOLC.Heyting]
F_mono [projection, in Undecidability.FOLC.Heyting]
F_inj [projection, in Undecidability.FOLC.Heyting]
F1 [definition, in Undecidability.FOLC.BPCP_FOL]
f1 [definition, in Undecidability.FOLC.LEnum]
F2 [definition, in Undecidability.FOLC.BPCP_FOL]
f2 [definition, in Undecidability.FOLC.LEnum]
F3 [definition, in Undecidability.FOLC.BPCP_FOL]
f3 [definition, in Undecidability.FOLC.LEnum]
f4 [definition, in Undecidability.FOLC.LEnum]
f5 [definition, in Undecidability.FOLC.LEnum]
f6 [definition, in Undecidability.FOLC.LEnum]
f7 [definition, in Undecidability.FOLC.LEnum]
f8 [definition, in Undecidability.FOLC.LEnum]
f9 [definition, in Undecidability.FOLC.LEnum]
G
GDN [lemma, in Undecidability.FOLC.GenConstructions]GDP [lemma, in Undecidability.FOLC.GenConstructions]
GenCompleteness [library]
GenCons [section, in Undecidability.FOLC.GenConstructions]
GenConstructions [library]
GenCons.Explosion [section, in Undecidability.FOLC.GenConstructions]
GenCons.Explosion.e [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Explosion.Hclosed [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Explosion.He [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Explosion.T [variable, in Undecidability.FOLC.GenConstructions]
GenCons.GBot [variable, in Undecidability.FOLC.GenConstructions]
GenCons.GBot_closed [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Henkin [section, in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.e [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.Hclosed [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.He [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.Hexp [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.Hunused [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.T [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Omega [section, in Undecidability.FOLC.GenConstructions]
GenCons.Omega.e [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Omega.He [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Omega.Hexp [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Omega.Hhenkin [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Omega.T [variable, in Undecidability.FOLC.GenConstructions]
_ ∘ _ [notation, in Undecidability.FOLC.GenConstructions]
GenCons.Union [section, in Undecidability.FOLC.GenConstructions]
GenCons.Union.econsistent_f [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Union.f [variable, in Undecidability.FOLC.GenConstructions]
GenCons.Union.f_le [variable, in Undecidability.FOLC.GenConstructions]
_ ⊩G _ [notation, in Undecidability.FOLC.GenConstructions]
_ ⊢G _ [notation, in Undecidability.FOLC.GenConstructions]
¬ _ [notation, in Undecidability.FOLC.GenConstructions]
∃ _ [notation, in Undecidability.FOLC.GenConstructions]
⊥ [notation, in Undecidability.FOLC.GenConstructions]
GenTarski [library]
Gentzen [section, in Undecidability.FOLC.Gentzen]
Gentzen [library]
Gentzen.CutElimination [section, in Undecidability.FOLC.Gentzen]
Gentzen.Enumerability [section, in Undecidability.FOLC.Gentzen]
Gentzen.Soundness [section, in Undecidability.FOLC.Gentzen]
Gentzen.Weakening [section, in Undecidability.FOLC.Gentzen]
_ ;; _ ⊢s _ [notation, in Undecidability.FOLC.Gentzen]
_ ⊢S _ [notation, in Undecidability.FOLC.Gentzen]
get_n [definition, in Undecidability.FOLC.WKL]
get_index_list [lemma, in Undecidability.FOLC.WKL]
GExE [lemma, in Undecidability.FOLC.GenConstructions]
GExI [lemma, in Undecidability.FOLC.GenConstructions]
GExp [lemma, in Undecidability.FOLC.GenConstructions]
glb_calg_iff [lemma, in Undecidability.FOLC.Lindenbaum]
glb_Pr [definition, in Undecidability.FOLC.Lindenbaum]
glb_calg [instance, in Undecidability.FOLC.Lindenbaum]
glb_alg_iff [lemma, in Undecidability.FOLC.Lindenbaum]
glb_alg [instance, in Undecidability.FOLC.Lindenbaum]
glindenbaum_eqH [lemma, in Undecidability.FOLC.Lindenbaum]
glindenbaum_hsat [lemma, in Undecidability.FOLC.Lindenbaum]
GXM [lemma, in Undecidability.FOLC.GenConstructions]
H
H [projection, in Undecidability.FOLC.Heyting]HA [projection, in Undecidability.FOLC.Heyting]
halting_dec [definition, in Undecidability.FOLC.Markov]
halt_cprv_stable [lemma, in Undecidability.FOLC.Markov]
halt_cprv [lemma, in Undecidability.FOLC.Markov]
HAProperty [section, in Undecidability.FOLC.Heyting]
_ ≡ _ [notation, in Undecidability.FOLC.Heyting]
has_model [definition, in Undecidability.FOLC.FullTarski]
has_model [definition, in Undecidability.FOLC.GenTarski]
has_model_OM_DM [lemma, in Undecidability.FOLC.WKL]
hcompleteness [lemma, in Undecidability.FOLC.Lindenbaum]
HdF [instance, in Undecidability.FOLC.LEnum]
HdP [instance, in Undecidability.FOLC.LEnum]
HeF [instance, in Undecidability.FOLC.LEnum]
help [instance, in Undecidability.FOLC.Markov]
Henkin [definition, in Undecidability.FOLC.GenConstructions]
henkin [definition, in Undecidability.FOLC.GenConstructions]
Henkin_T [lemma, in Undecidability.FOLC.GenConstructions]
Henkin_is_Henkin [lemma, in Undecidability.FOLC.GenConstructions]
Henkin_consistent [lemma, in Undecidability.FOLC.GenConstructions]
henkin_le [lemma, in Undecidability.FOLC.GenConstructions]
henkin_unused [lemma, in Undecidability.FOLC.GenConstructions]
henkin_axiom_unused [lemma, in Undecidability.FOLC.GenConstructions]
henkin_axiom [definition, in Undecidability.FOLC.GenConstructions]
HeP [instance, in Undecidability.FOLC.LEnum]
Heyting [library]
HeytingAlgebra [record, in Undecidability.FOLC.Heyting]
HeytingMorphism [record, in Undecidability.FOLC.Heyting]
hsat [definition, in Undecidability.FOLC.Lindenbaum]
hsat_L [definition, in Undecidability.FOLC.Lindenbaum]
hset [definition, in Undecidability.FOLC.Heyting]
hset_inf1 [lemma, in Undecidability.FOLC.Heyting]
hset_impl1 [lemma, in Undecidability.FOLC.Heyting]
hset_join1 [lemma, in Undecidability.FOLC.Heyting]
hset_meet1 [lemma, in Undecidability.FOLC.Heyting]
hset_bot1 [lemma, in Undecidability.FOLC.Heyting]
hset_impl_normal [lemma, in Undecidability.FOLC.Heyting]
hset_impl_equiv [lemma, in Undecidability.FOLC.Heyting]
hset_impl_proper [instance, in Undecidability.FOLC.Heyting]
hset_impl [definition, in Undecidability.FOLC.Heyting]
hset_inf_normal [lemma, in Undecidability.FOLC.Heyting]
hset_inf [definition, in Undecidability.FOLC.Heyting]
hset_join_normal [lemma, in Undecidability.FOLC.Heyting]
hset_join_proper [instance, in Undecidability.FOLC.Heyting]
hset_join [definition, in Undecidability.FOLC.Heyting]
hset_meet_normal [lemma, in Undecidability.FOLC.Heyting]
hset_meet_proper [instance, in Undecidability.FOLC.Heyting]
hset_meet [definition, in Undecidability.FOLC.Heyting]
hset_bot_normal [lemma, in Undecidability.FOLC.Heyting]
hset_bot [definition, in Undecidability.FOLC.Heyting]
hset_sub_proper [instance, in Undecidability.FOLC.Heyting]
hset_elem_proper [instance, in Undecidability.FOLC.Heyting]
hset_equiv_equiv [instance, in Undecidability.FOLC.Heyting]
hset_equiv [definition, in Undecidability.FOLC.Heyting]
hset_sub [definition, in Undecidability.FOLC.Heyting]
hset_elem [definition, in Undecidability.FOLC.Heyting]
hsoundness [lemma, in Undecidability.FOLC.Lindenbaum]
hvalid [definition, in Undecidability.FOLC.Lindenbaum]
I
IB [instance, in Undecidability.FOLC.BPCP_FOL]IB_F [lemma, in Undecidability.FOLC.BPCP_FOL]
IB_F3 [lemma, in Undecidability.FOLC.BPCP_FOL]
IB_F2 [lemma, in Undecidability.FOLC.BPCP_FOL]
IB_F1 [lemma, in Undecidability.FOLC.BPCP_FOL]
IB_drv [lemma, in Undecidability.FOLC.BPCP_FOL]
IB_enc [lemma, in Undecidability.FOLC.BPCP_FOL]
IB_prep [lemma, in Undecidability.FOLC.BPCP_FOL]
id [definition, in Undecidability.FOLC.unscoped]
ids [projection, in Undecidability.FOLC.unscoped]
ids [constructor, in Undecidability.FOLC.unscoped]
idsRen [instance, in Undecidability.FOLC.unscoped]
idSubst_form [definition, in Undecidability.FOLC.FullSyntax]
idSubst_form [definition, in Undecidability.FOLC.Syntax]
idSubst_term [definition, in Undecidability.FOLC.Terms]
IE [constructor, in Undecidability.FOLC.FullND]
IE [constructor, in Undecidability.FOLC.ND]
ieAbsurd [constructor, in Undecidability.FOLC.LEnum]
ieAllL [constructor, in Undecidability.FOLC.LEnum]
ieAllR [constructor, in Undecidability.FOLC.LEnum]
ieAx [constructor, in Undecidability.FOLC.LEnum]
ieContr [constructor, in Undecidability.FOLC.LEnum]
ieIL [constructor, in Undecidability.FOLC.LEnum]
ieIR [constructor, in Undecidability.FOLC.LEnum]
IE_to_CE [lemma, in Undecidability.FOLC.FullND]
IE_to_CE [lemma, in Undecidability.FOLC.ND]
iff_1b_2b [lemma, in Undecidability.FOLC.Analysis]
iff_1a_2a [lemma, in Undecidability.FOLC.Analysis]
II [constructor, in Undecidability.FOLC.FullND]
II [constructor, in Undecidability.FOLC.ND]
IL [constructor, in Undecidability.FOLC.Gentzen]
IL [constructor, in Undecidability.FOLC.FullSequent]
Impl [constructor, in Undecidability.FOLC.FullSyntax]
Impl [projection, in Undecidability.FOLC.Heyting]
Impl [constructor, in Undecidability.FOLC.Syntax]
impl_prv [lemma, in Undecidability.FOLC.BPCP_FOL]
impl_sat [lemma, in Undecidability.FOLC.BPCP_FOL]
impl_5_2a [lemma, in Undecidability.FOLC.Analysis]
impl_4_5 [lemma, in Undecidability.FOLC.Analysis]
impl_3b_4 [lemma, in Undecidability.FOLC.Analysis]
impl_3a_4 [lemma, in Undecidability.FOLC.Analysis]
impl_2b_3b [lemma, in Undecidability.FOLC.Analysis]
impl_2a_3a [lemma, in Undecidability.FOLC.Analysis]
impl_2a_2b [lemma, in Undecidability.FOLC.Analysis]
impl_trans [lemma, in Undecidability.FOLC.BPCP_CND]
Impl' [constructor, in Undecidability.FOLC.LEnum]
Impl'' [definition, in Undecidability.FOLC.LEnum]
Impl1 [projection, in Undecidability.FOLC.Heyting]
Imp_bot [lemma, in Undecidability.FOLC.Heyting]
Imp2 [lemma, in Undecidability.FOLC.Heyting]
incl_eq [lemma, in Undecidability.FOLC.DeMorgan]
inconsistent [lemma, in Undecidability.FOLC.Consistency]
Inf [projection, in Undecidability.FOLC.Heyting]
infinite_finitely_satisfiable' [lemma, in Undecidability.FOLC.WKL]
infinite_finitely_satisfiable [lemma, in Undecidability.FOLC.WKL]
infinite_iff [lemma, in Undecidability.FOLC.WKL]
infinite_path [definition, in Undecidability.FOLC.WKL]
infinite_tree [definition, in Undecidability.FOLC.WKL]
Inf_indexed1 [lemma, in Undecidability.FOLC.Heyting]
Inf_indexed [definition, in Undecidability.FOLC.Heyting]
Inf1 [projection, in Undecidability.FOLC.Heyting]
Inf2 [lemma, in Undecidability.FOLC.Heyting]
inj [definition, in Undecidability.FOLC.Markov]
inj_enum.d [variable, in Undecidability.FOLC.Markov]
inj_enum.e [variable, in Undecidability.FOLC.Markov]
inj_enum.Sigma [variable, in Undecidability.FOLC.Markov]
inj_enum [section, in Undecidability.FOLC.Markov]
input_fragment [definition, in Undecidability.FOLC.GenCompleteness]
input_bot [definition, in Undecidability.FOLC.GenCompleteness]
instId_form [lemma, in Undecidability.FOLC.FullSyntax]
instId_form [lemma, in Undecidability.FOLC.Syntax]
instId_term [lemma, in Undecidability.FOLC.Terms]
interp [record, in Undecidability.FOLC.GenTarski]
intu [constructor, in Undecidability.FOLC.FullND]
intu [constructor, in Undecidability.FOLC.ND]
In_T_closed [projection, in Undecidability.FOLC.GenConstructions]
In_T [projection, in Undecidability.FOLC.GenConstructions]
in_eqb_spec [lemma, in Undecidability.FOLC.LEnum]
in_eqb [definition, in Undecidability.FOLC.LEnum]
in_mapi_iff [lemma, in Undecidability.FOLC.WKL]
IP [definition, in Undecidability.FOLC.Markov]
iprep [definition, in Undecidability.FOLC.BPCP_FOL]
iprep_app [lemma, in Undecidability.FOLC.BPCP_FOL]
iprep_eval [lemma, in Undecidability.FOLC.BPCP_FOL]
iprv [definition, in Undecidability.FOLC.Markov]
iprv_halt_stable [lemma, in Undecidability.FOLC.Markov]
iprv_halt [lemma, in Undecidability.FOLC.Markov]
iprv_maxprv [lemma, in Undecidability.FOLC.Markov]
IR [constructor, in Undecidability.FOLC.Gentzen]
IR [constructor, in Undecidability.FOLC.FullSequent]
isprv [definition, in Undecidability.FOLC.Markov]
isvar [constructor, in Undecidability.FOLC.LEnum]
is_Henkin_inherit [lemma, in Undecidability.FOLC.GenConstructions]
is_Henkin [definition, in Undecidability.FOLC.GenConstructions]
is_inj_Preds [projection, in Undecidability.FOLC.Extend]
is_inj_Funcs [projection, in Undecidability.FOLC.Extend]
is_sup [abbreviation, in Undecidability.FOLC.Heyting]
is_inf [abbreviation, in Undecidability.FOLC.Heyting]
is_phi [definition, in Undecidability.FOLC.WKL]
Is_filter_exists [lemma, in Undecidability.FOLC.WKL]
Is_Filter_func [lemma, in Undecidability.FOLC.WKL]
Is_Filter_In [lemma, in Undecidability.FOLC.WKL]
Is_Filter_filter [lemma, in Undecidability.FOLC.WKL]
Is_Filter_false [constructor, in Undecidability.FOLC.WKL]
Is_Filter_true [constructor, in Undecidability.FOLC.WKL]
Is_Filter_nil [constructor, in Undecidability.FOLC.WKL]
Is_Filter [inductive, in Undecidability.FOLC.WKL]
is_tree [record, in Undecidability.FOLC.WKL]
IVec [definition, in Undecidability.FOLC.SDialogues]
I_Preds [projection, in Undecidability.FOLC.Extend]
I_Funcs [projection, in Undecidability.FOLC.Extend]
i_F [projection, in Undecidability.FOLC.GenTarski]
i_P [projection, in Undecidability.FOLC.GenTarski]
i_f [projection, in Undecidability.FOLC.GenTarski]
J
Join [projection, in Undecidability.FOLC.Heyting]Join_com [lemma, in Undecidability.FOLC.Heyting]
Join1 [projection, in Undecidability.FOLC.Heyting]
Join2 [lemma, in Undecidability.FOLC.Heyting]
Join3 [lemma, in Undecidability.FOLC.Heyting]
justified [definition, in Undecidability.FOLC.SDialogues]
justified [definition, in Undecidability.FOLC.Sorensen]
justified_weak [lemma, in Undecidability.FOLC.SDialogues]
justified_weak [lemma, in Undecidability.FOLC.Sorensen]
K
kbottomless [definition, in Undecidability.FOLC.Kripke]kcompleteness [definition, in Undecidability.FOLC.Analysis]
kcompleteness_implies_XM [lemma, in Undecidability.FOLC.Analysis]
kcompleteness_enum_implies_MP [lemma, in Undecidability.FOLC.Analysis]
kcompleteness_iff_MPL [lemma, in Undecidability.FOLC.Analysis]
kconstraint [definition, in Undecidability.FOLC.Kripke]
kcon_subs [definition, in Undecidability.FOLC.Kripke]
kexploding [definition, in Undecidability.FOLC.Kripke]
kexploding_retract [lemma, in Undecidability.FOLC.Extend]
kexploding_preds [lemma, in Undecidability.FOLC.Extend]
kexploding' [definition, in Undecidability.FOLC.Kripke]
kmodel [record, in Undecidability.FOLC.Kripke]
kmodel_reach_trans [instance, in Undecidability.FOLC.Kripke]
kmodel_reach_refl [instance, in Undecidability.FOLC.Kripke]
Kripke [section, in Undecidability.FOLC.Extend]
Kripke [section, in Undecidability.FOLC.Kripke]
Kripke [library]
KripkeCompleteness [section, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness [library]
KripkeCompleteness.BottomlessCompleteness [section, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.Contexts [section, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.ExplodingCompleteness [section, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.MPRequired [section, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.MPRequired.C [variable, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.MPRequired.HC [variable, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.MPRequired.K_completeness [variable, in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.StandardCompleteness [section, in Undecidability.FOLC.KripkeCompleteness]
_ ;; _ ⊢sC _ [notation, in Undecidability.FOLC.KripkeCompleteness]
_ ⊢SC _ [notation, in Undecidability.FOLC.KripkeCompleteness]
_ <<=C _ [notation, in Undecidability.FOLC.KripkeCompleteness]
Kripke.d [variable, in Undecidability.FOLC.Extend]
Kripke.D [variable, in Undecidability.FOLC.Extend]
Kripke.inj [variable, in Undecidability.FOLC.Extend]
Kripke.M [variable, in Undecidability.FOLC.Extend]
Kripke.Model [section, in Undecidability.FOLC.Kripke]
Kripke.Model.domain [variable, in Undecidability.FOLC.Kripke]
Kripke.Model.M [variable, in Undecidability.FOLC.Kripke]
Kripke.Substs [section, in Undecidability.FOLC.Kripke]
Kripke.Substs.D [variable, in Undecidability.FOLC.Kripke]
_ ⊨( _ , _ ) _ [notation, in Undecidability.FOLC.Kripke]
_ ⊨( _ ) _ [notation, in Undecidability.FOLC.Kripke]
Kripke.Σ [variable, in Undecidability.FOLC.Extend]
Kripke.Σ' [variable, in Undecidability.FOLC.Extend]
ksat [definition, in Undecidability.FOLC.Kripke]
ksat_retract [lemma, in Undecidability.FOLC.Extend]
ksat_comp [lemma, in Undecidability.FOLC.Kripke]
ksat_ext [lemma, in Undecidability.FOLC.Kripke]
ksat_iff [lemma, in Undecidability.FOLC.Kripke]
ksat_mon [lemma, in Undecidability.FOLC.Kripke]
ksemantic_explosion [lemma, in Undecidability.FOLC.Kripke]
ksoundness [lemma, in Undecidability.FOLC.Kripke]
KSoundness [section, in Undecidability.FOLC.Kripke]
ksoundness_seq [lemma, in Undecidability.FOLC.Gentzen]
ksoundness' [lemma, in Undecidability.FOLC.Kripke]
kstandard [definition, in Undecidability.FOLC.Kripke]
kstandard_explodes [lemma, in Undecidability.FOLC.Kripke]
kvalid_L_subs [lemma, in Undecidability.FOLC.Kripke]
kvalid_T [definition, in Undecidability.FOLC.Kripke]
kvalid_L [definition, in Undecidability.FOLC.Kripke]
K_std_seq_ksoundness [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_std_completeness [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_std_ksat [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_std_sprv' [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_std_sprv [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_std_correct [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_std_standard [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_std [instance, in Undecidability.FOLC.KripkeCompleteness]
K_bottomless_completeness [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_exp_seq_ksoundness [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_exp_completeness [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx_exploding [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx_ksat [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx_sprv' [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx_subst [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx_sprv [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx_constraint [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx_correct [lemma, in Undecidability.FOLC.KripkeCompleteness]
K_ctx [instance, in Undecidability.FOLC.KripkeCompleteness]
k_Bot [projection, in Undecidability.FOLC.Kripke]
k_P [projection, in Undecidability.FOLC.Kripke]
k_interp [projection, in Undecidability.FOLC.Kripke]
L
lb [definition, in Undecidability.FOLC.Heyting]lb_calg_iff [lemma, in Undecidability.FOLC.Lindenbaum]
lb_Pr [definition, in Undecidability.FOLC.Lindenbaum]
lb_calg [instance, in Undecidability.FOLC.Lindenbaum]
lb_alg_iff [lemma, in Undecidability.FOLC.Lindenbaum]
lb_alg [instance, in Undecidability.FOLC.Lindenbaum]
lb_normal [lemma, in Undecidability.FOLC.Heyting]
lb_proper [instance, in Undecidability.FOLC.Heyting]
lconst [constructor, in Undecidability.FOLC.FullND]
lconst [constructor, in Undecidability.FOLC.ND]
ldecidable [definition, in Undecidability.FOLC.WKL]
LEnum [library]
lexp [definition, in Undecidability.FOLC.WFexp]
lexp_perm_lexp' [lemma, in Undecidability.FOLC.WFexp]
lexp' [definition, in Undecidability.FOLC.WFexp]
lexp'_app_r [lemma, in Undecidability.FOLC.WFexp]
lexp'_app_l [lemma, in Undecidability.FOLC.WFexp]
lexp'_single [lemma, in Undecidability.FOLC.WFexp]
lexp'_nil [lemma, in Undecidability.FOLC.WFexp]
lexp'_app [lemma, in Undecidability.FOLC.WFexp]
lift_ext_c_closes_T [lemma, in Undecidability.FOLC.FOL]
lift_ext_c_closes [lemma, in Undecidability.FOLC.FOL]
lift_drop_inverse [lemma, in Undecidability.FOLC.FOL]
lift_drop_inverse' [lemma, in Undecidability.FOLC.FOL]
lift_drop_inverse_term' [lemma, in Undecidability.FOLC.FOL]
lift_interp_sat [lemma, in Undecidability.FOLC.GenTarski]
lift_interp_eval [lemma, in Undecidability.FOLC.GenTarski]
lift_interp [definition, in Undecidability.FOLC.GenTarski]
Lindenbaum [section, in Undecidability.FOLC.Lindenbaum]
Lindenbaum [library]
lindenbaum_eqH [lemma, in Undecidability.FOLC.Lindenbaum]
lindenbaum_hsat [lemma, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.BSoundness [section, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.CHAEval [section, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.CHAEval.hinter_Pr [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness [section, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness [section, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gAllE [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gAllI [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCE1 [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCE2 [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCI [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCtx [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gDE [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gDI1 [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gDI2 [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gExE [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gExI [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gExp [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gIE [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gII [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gnameless_equiv_ex' [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gnameless_equiv_all' [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gprv [variable, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gWeak [variable, in Undecidability.FOLC.Lindenbaum]
_ ⊢ _ [notation, in Undecidability.FOLC.Lindenbaum]
_ ⊢E _ [notation, in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Soundness [section, in Undecidability.FOLC.Lindenbaum]
listable [definition, in Undecidability.FOLC.WKL]
listable_list_length [lemma, in Undecidability.FOLC.WKL]
list_completeness_fragment [lemma, in Undecidability.FOLC.GenCompleteness]
list_completeness_expl [lemma, in Undecidability.FOLC.GenCompleteness]
list_completeness_standard [lemma, in Undecidability.FOLC.GenCompleteness]
list_comp [definition, in Undecidability.FOLC.axioms]
list_id [definition, in Undecidability.FOLC.axioms]
list_ext [definition, in Undecidability.FOLC.axioms]
list_T [definition, in Undecidability.FOLC.FullFOL]
list_prod_in [lemma, in Undecidability.FOLC.FOL]
list_T [definition, in Undecidability.FOLC.FOL]
list_or_spec [lemma, in Undecidability.FOLC.FullTarski]
list_or [definition, in Undecidability.FOLC.FullTarski]
list_form_eqb [definition, in Undecidability.FOLC.LEnum]
list_term_eqb [definition, in Undecidability.FOLC.LEnum]
LJD [section, in Undecidability.FOLC.Sorensen]
LJD.f [variable, in Undecidability.FOLC.Sorensen]
LJD.R [variable, in Undecidability.FOLC.Sorensen]
_ ⊢D _ [notation, in Undecidability.FOLC.Sorensen]
lu_idem [lemma, in Undecidability.FOLC.Heyting]
lu_sub [lemma, in Undecidability.FOLC.Heyting]
L_form_cml [lemma, in Undecidability.FOLC.FOL]
L_form [definition, in Undecidability.FOLC.FOL]
L_term_cml [lemma, in Undecidability.FOLC.FOL]
L_term [definition, in Undecidability.FOLC.FOL]
L_vec [definition, in Undecidability.FOLC.FOL]
L_tseq [definition, in Undecidability.FOLC.Gentzen]
L_seq [definition, in Undecidability.FOLC.Gentzen]
L_tsat_T [definition, in Undecidability.FOLC.Stability]
L_sprvie [definition, in Undecidability.FOLC.LEnum]
L_seq [definition, in Undecidability.FOLC.LEnum]
L_form' [definition, in Undecidability.FOLC.LEnum]
L_wf [definition, in Undecidability.FOLC.LEnum]
L_term' [definition, in Undecidability.FOLC.LEnum]
L_T_form_len [lemma, in Undecidability.FOLC.Enumeration]
L_T_Enumeration [section, in Undecidability.FOLC.Enumeration]
L_T_sub_or [lemma, in Undecidability.FOLC.Enumeration]
L_T_sub [lemma, in Undecidability.FOLC.Enumeration]
L_T_unused [lemma, in Undecidability.FOLC.Enumeration]
L_T_unused_v [lemma, in Undecidability.FOLC.Enumeration]
L_T_unused_t [lemma, in Undecidability.FOLC.Enumeration]
L_T_nat_le [lemma, in Undecidability.FOLC.Enumeration]
L_T_unused.enum_Preds [variable, in Undecidability.FOLC.Enumeration]
L_T_unused.enum_Funcs [variable, in Undecidability.FOLC.Enumeration]
L_T_unused [section, in Undecidability.FOLC.Enumeration]
L_tded [definition, in Undecidability.FOLC.ND]
L_con [definition, in Undecidability.FOLC.ND]
L_ded [definition, in Undecidability.FOLC.ND]
M
MacNeille [section, in Undecidability.FOLC.Heyting]_ ≡ _ [notation, in Undecidability.FOLC.Heyting]
_ ⊆ _ [notation, in Undecidability.FOLC.Heyting]
_ ∈ _ [notation, in Undecidability.FOLC.Heyting]
make_subst [abbreviation, in Undecidability.FOLC.Extend]
mapi [definition, in Undecidability.FOLC.WKL]
mapi_app [lemma, in Undecidability.FOLC.WKL]
map_subst [lemma, in Undecidability.FOLC.Lindenbaum]
map_closed [definition, in Undecidability.FOLC.Stability]
map_nth_id [lemma, in Undecidability.FOLC.WKL]
Markov [library]
max [instance, in Undecidability.FOLC.LEnum]
maximal [definition, in Undecidability.FOLC.GenConstructions]
maximal_prv [lemma, in Undecidability.FOLC.GenConstructions]
maximal_Omega [lemma, in Undecidability.FOLC.GenConstructions]
maxprv_sprv [lemma, in Undecidability.FOLC.Markov]
max_list_spec' [lemma, in Undecidability.FOLC.WKL]
max_list_spec [lemma, in Undecidability.FOLC.WKL]
max_list [abbreviation, in Undecidability.FOLC.WKL]
max_list_with [definition, in Undecidability.FOLC.WKL]
Meet [projection, in Undecidability.FOLC.Heyting]
Meet_hsat_L [lemma, in Undecidability.FOLC.Lindenbaum]
meet_sup_expansion [lemma, in Undecidability.FOLC.Heyting]
meet_sup_distr [lemma, in Undecidability.FOLC.Heyting]
meet_join_expansion [lemma, in Undecidability.FOLC.Heyting]
meet_join_distr [lemma, in Undecidability.FOLC.Heyting]
Meet_extend [lemma, in Undecidability.FOLC.Heyting]
Meet_assoc [lemma, in Undecidability.FOLC.Heyting]
Meet_left [lemma, in Undecidability.FOLC.Heyting]
Meet_com [lemma, in Undecidability.FOLC.Heyting]
Meet1 [projection, in Undecidability.FOLC.Heyting]
Meet2 [lemma, in Undecidability.FOLC.Heyting]
Meet3 [lemma, in Undecidability.FOLC.Heyting]
min_sig [instance, in Undecidability.FOLC.BPCP_FOL]
min_sig_fun_ar [definition, in Undecidability.FOLC.BPCP_FOL]
min_sig_funcs_dec [instance, in Undecidability.FOLC.BPCP_FOL]
min_sig_funcs [inductive, in Undecidability.FOLC.BPCP_FOL]
min_sig_pred_ar [definition, in Undecidability.FOLC.BPCP_FOL]
min_sig_preds_dec [instance, in Undecidability.FOLC.BPCP_FOL]
min_sig_preds [inductive, in Undecidability.FOLC.BPCP_FOL]
mkApps [definition, in Undecidability.FOLC.LEnum]
model_fragment_classical [lemma, in Undecidability.FOLC.GenCompleteness]
model_fragment_correct [lemma, in Undecidability.FOLC.GenCompleteness]
model_fragment [instance, in Undecidability.FOLC.GenCompleteness]
model_bot_exploding [lemma, in Undecidability.FOLC.GenCompleteness]
model_bot_standard [lemma, in Undecidability.FOLC.GenCompleteness]
model_bot_classical [lemma, in Undecidability.FOLC.GenCompleteness]
model_bot_correct [lemma, in Undecidability.FOLC.GenCompleteness]
model_bot [instance, in Undecidability.FOLC.GenCompleteness]
model_u [lemma, in Undecidability.FOLC.WKL]
model_existence [definition, in Undecidability.FOLC.WKL]
modex_comp [lemma, in Undecidability.FOLC.Analysis]
modex_impl_OM_DM [lemma, in Undecidability.FOLC.WKL]
modex_impl [lemma, in Undecidability.FOLC.WKL]
modex_compact [lemma, in Undecidability.FOLC.WKL]
modex_standard [lemma, in Undecidability.FOLC.WKL]
mon_Bot [projection, in Undecidability.FOLC.Kripke]
mon_P [projection, in Undecidability.FOLC.Kripke]
MP [definition, in Undecidability.FOLC.Stability]
MPL [definition, in Undecidability.FOLC.Markov]
MPL_independent [lemma, in Undecidability.FOLC.Markov]
mp_standard_completeness [lemma, in Undecidability.FOLC.GenCompleteness]
mp_tprv_stability [lemma, in Undecidability.FOLC.GenCompleteness]
MP_MPL [lemma, in Undecidability.FOLC.Markov]
MP_enum_stable_iff [lemma, in Undecidability.FOLC.Markov]
mp_to_ste [lemma, in Undecidability.FOLC.Stability]
mu [definition, in Undecidability.FOLC.Markov]
M_u_omni [lemma, in Undecidability.FOLC.WKL]
M_u_dec [lemma, in Undecidability.FOLC.WKL]
M_u_SB [lemma, in Undecidability.FOLC.WKL]
M_u [definition, in Undecidability.FOLC.WKL]
N
nameless_equiv_ex' [lemma, in Undecidability.FOLC.FullND]nameless_equiv_all' [lemma, in Undecidability.FOLC.FullND]
nameless_equiv_ex [lemma, in Undecidability.FOLC.FullND]
nameless_equiv_all [lemma, in Undecidability.FOLC.FullND]
nameless_equiv' [lemma, in Undecidability.FOLC.FullSequent]
nameless_equiv [lemma, in Undecidability.FOLC.FullSequent]
nameless_equiv_all' [lemma, in Undecidability.FOLC.BPCP_CND]
nameless_equiv [lemma, in Undecidability.FOLC.ND]
nat [abbreviation, in Undecidability.FOLC.WKL]
natinj [definition, in Undecidability.FOLC.Markov]
natinj_inj [lemma, in Undecidability.FOLC.Markov]
NBot [projection, in Undecidability.FOLC.GenConstructions]
NBot_closed [projection, in Undecidability.FOLC.GenConstructions]
ND [library]
ND_def.Weakening [section, in Undecidability.FOLC.FullND]
_ ⊩IE _ [notation, in Undecidability.FOLC.FullND]
_ ⊩CL _ [notation, in Undecidability.FOLC.FullND]
_ ⊩CE _ [notation, in Undecidability.FOLC.FullND]
_ ⊩( _ , _ ) _ [notation, in Undecidability.FOLC.FullND]
_ ⊩ _ [notation, in Undecidability.FOLC.FullND]
_ ⊢IE _ [notation, in Undecidability.FOLC.FullND]
_ ⊢CL _ [notation, in Undecidability.FOLC.FullND]
_ ⊢CE _ [notation, in Undecidability.FOLC.FullND]
_ ⊢( _ , _ ) _ [notation, in Undecidability.FOLC.FullND]
_ ⊢ _ [notation, in Undecidability.FOLC.FullND]
_ ⊢ _ [notation, in Undecidability.FOLC.FullND]
↑ [notation, in Undecidability.FOLC.FullND]
ND_def [section, in Undecidability.FOLC.FullND]
nd_to_sequent [lemma, in Undecidability.FOLC.Analysis]
ND_def.Weakening [section, in Undecidability.FOLC.ND]
_ ⊩IE _ [notation, in Undecidability.FOLC.ND]
_ ⊩CL _ [notation, in Undecidability.FOLC.ND]
_ ⊩CE _ [notation, in Undecidability.FOLC.ND]
_ ⊩( _ , _ ) _ [notation, in Undecidability.FOLC.ND]
_ ⊩ _ [notation, in Undecidability.FOLC.ND]
_ ⊢IE _ [notation, in Undecidability.FOLC.ND]
_ ⊢CL _ [notation, in Undecidability.FOLC.ND]
_ ⊢CE _ [notation, in Undecidability.FOLC.ND]
_ ⊢( _ , _ ) _ [notation, in Undecidability.FOLC.ND]
_ ⊢ _ [notation, in Undecidability.FOLC.ND]
ND_def [section, in Undecidability.FOLC.ND]
ND_defend [lemma, in Undecidability.FOLC.DialogFragment]
Neg [definition, in Undecidability.FOLC.WKL]
Neg_sat [lemma, in Undecidability.FOLC.WKL]
nodes [projection, in Undecidability.FOLC.Kripke]
normal [definition, in Undecidability.FOLC.Gentzen]
normal [definition, in Undecidability.FOLC.Heyting]
normal_bot [lemma, in Undecidability.FOLC.Heyting]
normal_dclosed [lemma, in Undecidability.FOLC.Heyting]
normal_proper [instance, in Undecidability.FOLC.Heyting]
not_AllI [definition, in Undecidability.FOLC.Gentzen]
not_II [definition, in Undecidability.FOLC.Gentzen]
novar [constructor, in Undecidability.FOLC.LEnum]
nthe_seq [lemma, in Undecidability.FOLC.WKL]
nth_order_map [lemma, in Undecidability.FOLC.FOL]
O
ocons [definition, in Undecidability.FOLC.SDialogues]ocons [definition, in Undecidability.FOLC.Sorensen]
ocons_sub' [lemma, in Undecidability.FOLC.SDialogues]
ocons_sub [lemma, in Undecidability.FOLC.SDialogues]
ocons_sub [lemma, in Undecidability.FOLC.Sorensen]
ofNat [definition, in Undecidability.FOLC.Markov]
ofnat_natinj [lemma, in Undecidability.FOLC.Markov]
ofNat_correct [lemma, in Undecidability.FOLC.Markov]
of_form_wf [lemma, in Undecidability.FOLC.LEnum]
of_list_wf [lemma, in Undecidability.FOLC.LEnum]
of_term_wf [lemma, in Undecidability.FOLC.LEnum]
of_term_wf' [lemma, in Undecidability.FOLC.LEnum]
of_form [definition, in Undecidability.FOLC.LEnum]
of_term [definition, in Undecidability.FOLC.LEnum]
OL [constructor, in Undecidability.FOLC.FullSequent]
OM [definition, in Undecidability.FOLC.WKL]
Omega [definition, in Undecidability.FOLC.GenConstructions]
omega [definition, in Undecidability.FOLC.GenConstructions]
Omega_all [lemma, in Undecidability.FOLC.GenConstructions]
Omega_impl [lemma, in Undecidability.FOLC.GenConstructions]
Omega_T [lemma, in Undecidability.FOLC.GenConstructions]
Omega_prv [lemma, in Undecidability.FOLC.GenConstructions]
omega_le [lemma, in Undecidability.FOLC.GenConstructions]
omniscient [definition, in Undecidability.FOLC.WKL]
omniscient_on_fAll_sat [lemma, in Undecidability.FOLC.WKL]
omniscient_on_fExists_sat [lemma, in Undecidability.FOLC.WKL]
omniscient_on_And [lemma, in Undecidability.FOLC.WKL]
omniscient_on_Or [lemma, in Undecidability.FOLC.WKL]
omniscient_on_Neg [lemma, in Undecidability.FOLC.WKL]
omniscient_to_decidable [lemma, in Undecidability.FOLC.WKL]
omniscient_to_classical [lemma, in Undecidability.FOLC.WKL]
omniscient_on [abbreviation, in Undecidability.FOLC.WKL]
OP [constructor, in Undecidability.FOLC.SDialogues]
OP [constructor, in Undecidability.FOLC.Sorensen]
opening [inductive, in Undecidability.FOLC.SDialogues]
opening [inductive, in Undecidability.FOLC.Sorensen]
opred [definition, in Undecidability.FOLC.SDialogues]
opred [definition, in Undecidability.FOLC.Sorensen]
option_form_eqb [definition, in Undecidability.FOLC.LEnum]
option_map_map [lemma, in Undecidability.FOLC.LEnum]
option_map_id [lemma, in Undecidability.FOLC.LEnum]
option_pred [definition, in Undecidability.FOLC.LEnum]
Or [definition, in Undecidability.FOLC.WKL]
or_single [lemma, in Undecidability.FOLC.FullSequent]
or_weak [lemma, in Undecidability.FOLC.FullSequent]
or_el [lemma, in Undecidability.FOLC.FullSequent]
or_char [lemma, in Undecidability.FOLC.FullSequent]
or_subst [lemma, in Undecidability.FOLC.FullSequent]
Or_sat [lemma, in Undecidability.FOLC.WKL]
OR1 [constructor, in Undecidability.FOLC.FullSequent]
OR2 [constructor, in Undecidability.FOLC.FullSequent]
output_fragment [definition, in Undecidability.FOLC.GenCompleteness]
output_bot [definition, in Undecidability.FOLC.GenCompleteness]
Out_T_impl [projection, in Undecidability.FOLC.GenConstructions]
Out_T_all [projection, in Undecidability.FOLC.GenConstructions]
Out_T_prv [projection, in Undecidability.FOLC.GenConstructions]
Out_T_sub [projection, in Undecidability.FOLC.GenConstructions]
Out_T_econsistent [projection, in Undecidability.FOLC.GenConstructions]
Out_T [projection, in Undecidability.FOLC.GenConstructions]
P
P [constructor, in Undecidability.FOLC.BPCP_FOL]path_wellfounded_contra [lemma, in Undecidability.FOLC.WKL]
Pc [constructor, in Undecidability.FOLC.FullND]
Pc [constructor, in Undecidability.FOLC.ND]
PCO_implies_modex [lemma, in Undecidability.FOLC.WKL]
peirce [inductive, in Undecidability.FOLC.FullND]
peirce [inductive, in Undecidability.FOLC.ND]
perm [definition, in Undecidability.FOLC.WFexp]
Perm [constructor, in Undecidability.FOLC.FullSequent]
Permutation_cons_split [lemma, in Undecidability.FOLC.WFexp]
perm_R [lemma, in Undecidability.FOLC.WFexp]
pext [axiom, in Undecidability.FOLC.axioms]
phi_exists [lemma, in Undecidability.FOLC.WKL]
phi_down [lemma, in Undecidability.FOLC.WKL]
pi [lemma, in Undecidability.FOLC.axioms]
plain_enum_slow [lemma, in Undecidability.FOLC.Enumeration]
plain_enum_enumerates [lemma, in Undecidability.FOLC.Enumeration]
plain_enum [definition, in Undecidability.FOLC.Enumeration]
Pr [definition, in Undecidability.FOLC.BPCP_FOL]
Pred [constructor, in Undecidability.FOLC.FullSyntax]
Pred [constructor, in Undecidability.FOLC.Syntax]
Preds [projection, in Undecidability.FOLC.Terms]
Pred_cast [lemma, in Undecidability.FOLC.LEnum]
pred_ar [projection, in Undecidability.FOLC.Terms]
Pred' [constructor, in Undecidability.FOLC.LEnum]
Pred'' [definition, in Undecidability.FOLC.LEnum]
pref [definition, in Undecidability.FOLC.FOL]
prefix [definition, in Undecidability.FOLC.WKL]
preorder_HA [instance, in Undecidability.FOLC.Heyting]
prep [definition, in Undecidability.FOLC.BPCP_FOL]
prep_subst [lemma, in Undecidability.FOLC.BPCP_FOL]
prod_comp [definition, in Undecidability.FOLC.axioms]
prod_ext [definition, in Undecidability.FOLC.axioms]
prod_id [definition, in Undecidability.FOLC.axioms]
prod_map [definition, in Undecidability.FOLC.axioms]
proper_HA_Inf_indexed [instance, in Undecidability.FOLC.Heyting]
proper_HA_Sup_indexed [instance, in Undecidability.FOLC.Heyting]
proper_HA_Sup [instance, in Undecidability.FOLC.Heyting]
proper_HA_Inf [instance, in Undecidability.FOLC.Heyting]
proper_HA_Impl [instance, in Undecidability.FOLC.Heyting]
proper_HA_Join [instance, in Undecidability.FOLC.Heyting]
proper_HA_Meet [instance, in Undecidability.FOLC.Heyting]
PropT [section, in Undecidability.FOLC.Stability]
prop_T_correct [lemma, in Undecidability.FOLC.Stability]
prop_T [definition, in Undecidability.FOLC.Stability]
prv [inductive, in Undecidability.FOLC.FullND]
prv [inductive, in Undecidability.FOLC.ND]
prvie_prv [lemma, in Undecidability.FOLC.LEnum]
prvie_prv' [lemma, in Undecidability.FOLC.LEnum]
prv_back [lemma, in Undecidability.FOLC.Extend]
prv_embed [lemma, in Undecidability.FOLC.Extend]
prv_cut_list [lemma, in Undecidability.FOLC.DeMorgan]
prv_T_comp [lemma, in Undecidability.FOLC.FullND]
prv_T_remove [lemma, in Undecidability.FOLC.FullND]
prv_T_impl [lemma, in Undecidability.FOLC.FullND]
prv_from_single [lemma, in Undecidability.FOLC.FullND]
prv_cut [lemma, in Undecidability.FOLC.FullND]
prv_prvie [lemma, in Undecidability.FOLC.LEnum]
prv_T_comp [lemma, in Undecidability.FOLC.ND]
prv_T_remove [lemma, in Undecidability.FOLC.ND]
prv_T_impl [lemma, in Undecidability.FOLC.ND]
prv_from_single [lemma, in Undecidability.FOLC.ND]
prv_cut [lemma, in Undecidability.FOLC.ND]
Q
Q [constructor, in Undecidability.FOLC.BPCP_FOL]QQ [abbreviation, in Undecidability.FOLC.BPCP_CND]
R
R [projection, in Undecidability.FOLC.Heyting]raise [definition, in Undecidability.FOLC.FOL]
reachable [projection, in Undecidability.FOLC.Kripke]
reach_tran [projection, in Undecidability.FOLC.Kripke]
reach_refl [projection, in Undecidability.FOLC.Kripke]
RefutationComp [section, in Undecidability.FOLC.FullND]
RefutationComp [section, in Undecidability.FOLC.ND]
refutation_prv [lemma, in Undecidability.FOLC.FullND]
refutation_prv [lemma, in Undecidability.FOLC.ND]
ren_form_to_form [lemma, in Undecidability.FOLC.LEnum]
ren_term_to_term' [lemma, in Undecidability.FOLC.LEnum]
ren_term_to_term [lemma, in Undecidability.FOLC.LEnum]
ren1 [projection, in Undecidability.FOLC.unscoped]
Ren1 [record, in Undecidability.FOLC.unscoped]
ren1 [constructor, in Undecidability.FOLC.unscoped]
Ren1 [inductive, in Undecidability.FOLC.unscoped]
ren2 [projection, in Undecidability.FOLC.unscoped]
Ren2 [record, in Undecidability.FOLC.unscoped]
ren2 [constructor, in Undecidability.FOLC.unscoped]
Ren2 [inductive, in Undecidability.FOLC.unscoped]
ren3 [projection, in Undecidability.FOLC.unscoped]
Ren3 [record, in Undecidability.FOLC.unscoped]
ren3 [constructor, in Undecidability.FOLC.unscoped]
Ren3 [inductive, in Undecidability.FOLC.unscoped]
ren4 [projection, in Undecidability.FOLC.unscoped]
Ren4 [record, in Undecidability.FOLC.unscoped]
ren4 [constructor, in Undecidability.FOLC.unscoped]
Ren4 [inductive, in Undecidability.FOLC.unscoped]
ren5 [projection, in Undecidability.FOLC.unscoped]
Ren5 [record, in Undecidability.FOLC.unscoped]
ren5 [constructor, in Undecidability.FOLC.unscoped]
Ren5 [inductive, in Undecidability.FOLC.unscoped]
RI [instance, in Undecidability.FOLC.Extend]
RM [instance, in Undecidability.FOLC.Extend]
Rref [projection, in Undecidability.FOLC.Heyting]
Rtra [projection, in Undecidability.FOLC.Heyting]
rule_set [record, in Undecidability.FOLC.SDialogues]
rule_set [record, in Undecidability.FOLC.Sorensen]
R_Preds [projection, in Undecidability.FOLC.Extend]
R_Funcs [projection, in Undecidability.FOLC.Extend]
S
SAll [constructor, in Undecidability.FOLC.FullFOL]SAll [constructor, in Undecidability.FOLC.FOL]
sat [definition, in Undecidability.FOLC.FullTarski]
sat [definition, in Undecidability.FOLC.GenTarski]
sat_subst [lemma, in Undecidability.FOLC.FullTarski]
sat_comp [lemma, in Undecidability.FOLC.FullTarski]
sat_ext [lemma, in Undecidability.FOLC.FullTarski]
sat_subst [lemma, in Undecidability.FOLC.GenTarski]
sat_comp [lemma, in Undecidability.FOLC.GenTarski]
sat_ext [lemma, in Undecidability.FOLC.GenTarski]
sat_ext_unused [lemma, in Undecidability.FOLC.GenTarski]
SConjL [constructor, in Undecidability.FOLC.FullFOL]
SConjR [constructor, in Undecidability.FOLC.FullFOL]
scons [definition, in Undecidability.FOLC.unscoped]
scons_comp [lemma, in Undecidability.FOLC.unscoped]
scons_eta_id [lemma, in Undecidability.FOLC.unscoped]
scons_eta [lemma, in Undecidability.FOLC.unscoped]
SDialogues [section, in Undecidability.FOLC.SDialogues]
SDialogues [library]
SDialogues.f [variable, in Undecidability.FOLC.SDialogues]
SDialogues.R [variable, in Undecidability.FOLC.SDialogues]
SDialogues.Up [section, in Undecidability.FOLC.SDialogues]
SDialogues.Up.g [variable, in Undecidability.FOLC.SDialogues]
SDialogues.Up.P [variable, in Undecidability.FOLC.SDialogues]
SDialogues.Up.X [variable, in Undecidability.FOLC.SDialogues]
SDialogues.Up.Y [variable, in Undecidability.FOLC.SDialogues]
SDialogues.Up.Z [variable, in Undecidability.FOLC.SDialogues]
_ ⪍' _ [notation, in Undecidability.FOLC.SDialogues]
_ ⪍ _ [notation, in Undecidability.FOLC.SDialogues]
_ ⊢D _ [notation, in Undecidability.FOLC.SDialogues]
SDisjL [constructor, in Undecidability.FOLC.FullFOL]
SDisjR [constructor, in Undecidability.FOLC.FullFOL]
semantic_dm [lemma, in Undecidability.FOLC.GenTarski]
semi_completeness_fragment [lemma, in Undecidability.FOLC.GenCompleteness]
semi_completeness_standard [lemma, in Undecidability.FOLC.GenCompleteness]
seq_ND_T [lemma, in Undecidability.FOLC.Gentzen]
seq_ND [lemma, in Undecidability.FOLC.Gentzen]
seq_nameless_equiv [lemma, in Undecidability.FOLC.Gentzen]
seq_subst_Weak [lemma, in Undecidability.FOLC.Gentzen]
seq_Weak [lemma, in Undecidability.FOLC.Gentzen]
seq_consistent [lemma, in Undecidability.FOLC.Gentzen]
SEx [constructor, in Undecidability.FOLC.FullFOL]
SE_cut [lemma, in Undecidability.FOLC.KripkeCompleteness]
sf [inductive, in Undecidability.FOLC.FullFOL]
sf [inductive, in Undecidability.FOLC.FOL]
sf_well_founded [lemma, in Undecidability.FOLC.FullFOL]
sf_acc [lemma, in Undecidability.FOLC.FullFOL]
sf_form_rules [lemma, in Undecidability.FOLC.DialogFull]
sf_well_founded [lemma, in Undecidability.FOLC.FOL]
sf_acc [lemma, in Undecidability.FOLC.FOL]
sf_form_rules [lemma, in Undecidability.FOLC.DialogFragment]
SGame [section, in Undecidability.FOLC.Sorensen]
SGame.f [variable, in Undecidability.FOLC.Sorensen]
SGame.R [variable, in Undecidability.FOLC.Sorensen]
shift [definition, in Undecidability.FOLC.unscoped]
shift_P [definition, in Undecidability.FOLC.FullFOL]
shift_P [definition, in Undecidability.FOLC.FOL]
SigExt [section, in Undecidability.FOLC.FOL]
SigExt [section, in Undecidability.FOLC.GenTarski]
SigExt [section, in Undecidability.FOLC.ND]
SigExt.D [variable, in Undecidability.FOLC.GenTarski]
SigExt.F [variable, in Undecidability.FOLC.GenTarski]
SigExt.F_ar [variable, in Undecidability.FOLC.GenTarski]
SigExt.P [variable, in Undecidability.FOLC.GenTarski]
SigExt.P_ar [variable, in Undecidability.FOLC.GenTarski]
Signature [record, in Undecidability.FOLC.Terms]
Signature_inj [record, in Undecidability.FOLC.Extend]
sig_drop_subst' [lemma, in Undecidability.FOLC.FOL]
sig_drop_subst_term' [lemma, in Undecidability.FOLC.FOL]
sig_drop [definition, in Undecidability.FOLC.FOL]
sig_drop' [definition, in Undecidability.FOLC.FOL]
sig_drop_term [definition, in Undecidability.FOLC.FOL]
sig_drop_term' [definition, in Undecidability.FOLC.FOL]
sig_lift_subst [lemma, in Undecidability.FOLC.FOL]
sig_lift_subst_term [lemma, in Undecidability.FOLC.FOL]
sig_lift [definition, in Undecidability.FOLC.FOL]
sig_lift' [definition, in Undecidability.FOLC.FOL]
sig_lift_term [definition, in Undecidability.FOLC.FOL]
sig_lift_term' [definition, in Undecidability.FOLC.FOL]
sig_ext [definition, in Undecidability.FOLC.FOL]
sig_lift_subst_valid [lemma, in Undecidability.FOLC.GenTarski]
sig_lift_subst_sat [lemma, in Undecidability.FOLC.GenTarski]
sig_lift_out_T [lemma, in Undecidability.FOLC.ND]
sig_lift_out [lemma, in Undecidability.FOLC.ND]
sig_drop_Weak [lemma, in Undecidability.FOLC.ND]
sig_lift_Weak [lemma, in Undecidability.FOLC.ND]
SImplL [constructor, in Undecidability.FOLC.FullFOL]
SImplL [constructor, in Undecidability.FOLC.FOL]
SImplR [constructor, in Undecidability.FOLC.FullFOL]
SImplR [constructor, in Undecidability.FOLC.FOL]
size [definition, in Undecidability.FOLC.FullFOL]
size [definition, in Undecidability.FOLC.FOL]
size_ind [lemma, in Undecidability.FOLC.FullFOL]
size_ind [lemma, in Undecidability.FOLC.FOL]
SM [definition, in Undecidability.FOLC.GenTarski]
SOAtk [constructor, in Undecidability.FOLC.SDialogues]
SOAtk [constructor, in Undecidability.FOLC.Sorensen]
SODef [constructor, in Undecidability.FOLC.SDialogues]
SODef [constructor, in Undecidability.FOLC.Sorensen]
somove [inductive, in Undecidability.FOLC.SDialogues]
somove [inductive, in Undecidability.FOLC.Sorensen]
Sorensen [library]
Soundness [lemma, in Undecidability.FOLC.Lindenbaum]
Soundness [lemma, in Undecidability.FOLC.GenTarski]
Soundness' [lemma, in Undecidability.FOLC.Lindenbaum]
Soundness' [lemma, in Undecidability.FOLC.GenTarski]
SPAtk [constructor, in Undecidability.FOLC.SDialogues]
SPAtk [constructor, in Undecidability.FOLC.Sorensen]
SPDef [constructor, in Undecidability.FOLC.SDialogues]
SPDef [constructor, in Undecidability.FOLC.Sorensen]
split_right [lemma, in Undecidability.FOLC.Sorensen]
spmove [inductive, in Undecidability.FOLC.SDialogues]
spmove [inductive, in Undecidability.FOLC.Sorensen]
sprv [inductive, in Undecidability.FOLC.Gentzen]
sprvie [inductive, in Undecidability.FOLC.LEnum]
sprv_prv_iff [lemma, in Undecidability.FOLC.Extend]
sprv_sprvie [lemma, in Undecidability.FOLC.Markov]
sprv_Dprv [lemma, in Undecidability.FOLC.DialogFragment]
sstate [definition, in Undecidability.FOLC.SDialogues]
sstate [definition, in Undecidability.FOLC.Sorensen]
ST [definition, in Undecidability.FOLC.Stability]
stA [constructor, in Undecidability.FOLC.FOL]
Stability [library]
StabilityClasses [section, in Undecidability.FOLC.Stability]
StabilityClasses.DN [section, in Undecidability.FOLC.Stability]
StabilityClasses.ObjMP [section, in Undecidability.FOLC.Stability]
StabilityClasses.ObjMP.ConT [section, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP [section, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum [section, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.HL [variable, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.HX [variable, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.L [variable, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.mp [variable, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.P [variable, in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.X [variable, in Undecidability.FOLC.Stability]
stable [definition, in Undecidability.FOLC.Stability]
stable [definition, in Undecidability.FOLC.WKL]
stable_red [lemma, in Undecidability.FOLC.Markov]
stable_equiv [lemma, in Undecidability.FOLC.Stability]
stab_class [definition, in Undecidability.FOLC.Stability]
standard_bot [definition, in Undecidability.FOLC.GenTarski]
sta_to_dn [lemma, in Undecidability.FOLC.Stability]
stB [constructor, in Undecidability.FOLC.FOL]
ste_to_mp [lemma, in Undecidability.FOLC.Stability]
stF [constructor, in Undecidability.FOLC.FOL]
stf_to_st_context [lemma, in Undecidability.FOLC.Stability]
stIL [constructor, in Undecidability.FOLC.FOL]
stIR [constructor, in Undecidability.FOLC.FOL]
stP [constructor, in Undecidability.FOLC.FOL]
stprv [definition, in Undecidability.FOLC.Gentzen]
StrongCompleteness [section, in Undecidability.FOLC.GenCompleteness]
StrongSoundness [lemma, in Undecidability.FOLC.GenTarski]
strong_completeness_fragment [lemma, in Undecidability.FOLC.GenCompleteness]
strong_completeness_expl [lemma, in Undecidability.FOLC.GenCompleteness]
strong_completeness_standard [lemma, in Undecidability.FOLC.GenCompleteness]
strong_term_ind [lemma, in Undecidability.FOLC.Terms]
strong_term_ind' [lemma, in Undecidability.FOLC.Terms]
strong_ksoundness [lemma, in Undecidability.FOLC.Kripke]
ST__f [definition, in Undecidability.FOLC.Stability]
ST__e [definition, in Undecidability.FOLC.Stability]
ST__a [definition, in Undecidability.FOLC.Stability]
subrelation_HA_flip [instance, in Undecidability.FOLC.Heyting]
subrelation_HA [instance, in Undecidability.FOLC.Heyting]
subset_T_trans [instance, in Undecidability.FOLC.FullFOL]
subset_T [definition, in Undecidability.FOLC.FullFOL]
subset_T_trans [instance, in Undecidability.FOLC.FOL]
subset_T [definition, in Undecidability.FOLC.FOL]
subst_unused_closed' [lemma, in Undecidability.FOLC.FullFOL]
subst_unused_closed [lemma, in Undecidability.FOLC.FullFOL]
subst_unused_range [lemma, in Undecidability.FOLC.FullFOL]
subst_unused_single [lemma, in Undecidability.FOLC.FullFOL]
subst_unused_form [lemma, in Undecidability.FOLC.FullFOL]
subst_unused_term [lemma, in Undecidability.FOLC.FullFOL]
subst_size [lemma, in Undecidability.FOLC.FullFOL]
subst_unused_closed' [lemma, in Undecidability.FOLC.FOL]
subst_unused_closed [lemma, in Undecidability.FOLC.FOL]
subst_unused_range [lemma, in Undecidability.FOLC.FOL]
subst_unused_single [lemma, in Undecidability.FOLC.FOL]
subst_unused_form [lemma, in Undecidability.FOLC.FOL]
subst_unused_term [lemma, in Undecidability.FOLC.FOL]
subst_size [lemma, in Undecidability.FOLC.FOL]
subst_Weak [lemma, in Undecidability.FOLC.FullND]
Subst_form [instance, in Undecidability.FOLC.FullSyntax]
Subst_term [instance, in Undecidability.FOLC.FullSyntax]
subst_form [definition, in Undecidability.FOLC.FullSyntax]
Subst_form [instance, in Undecidability.FOLC.Syntax]
Subst_term [instance, in Undecidability.FOLC.Syntax]
subst_form [definition, in Undecidability.FOLC.Syntax]
subst_form_of_form [lemma, in Undecidability.FOLC.LEnum]
subst_term_map [lemma, in Undecidability.FOLC.LEnum]
subst_term_of_term [lemma, in Undecidability.FOLC.LEnum]
subst_form' [definition, in Undecidability.FOLC.LEnum]
subst_term'' [definition, in Undecidability.FOLC.LEnum]
subst_term' [definition, in Undecidability.FOLC.LEnum]
subst_term [definition, in Undecidability.FOLC.Terms]
subst_Weak [lemma, in Undecidability.FOLC.FullSequent]
subst_Weak [lemma, in Undecidability.FOLC.ND]
subst1 [projection, in Undecidability.FOLC.unscoped]
Subst1 [record, in Undecidability.FOLC.unscoped]
subst1 [constructor, in Undecidability.FOLC.unscoped]
Subst1 [inductive, in Undecidability.FOLC.unscoped]
subst2 [projection, in Undecidability.FOLC.unscoped]
Subst2 [record, in Undecidability.FOLC.unscoped]
subst2 [constructor, in Undecidability.FOLC.unscoped]
Subst2 [inductive, in Undecidability.FOLC.unscoped]
subst3 [projection, in Undecidability.FOLC.unscoped]
Subst3 [record, in Undecidability.FOLC.unscoped]
subst3 [constructor, in Undecidability.FOLC.unscoped]
Subst3 [inductive, in Undecidability.FOLC.unscoped]
subst4 [projection, in Undecidability.FOLC.unscoped]
Subst4 [record, in Undecidability.FOLC.unscoped]
subst4 [constructor, in Undecidability.FOLC.unscoped]
Subst4 [inductive, in Undecidability.FOLC.unscoped]
subst5 [projection, in Undecidability.FOLC.unscoped]
Subst5 [record, in Undecidability.FOLC.unscoped]
subst5 [constructor, in Undecidability.FOLC.unscoped]
Subst5 [inductive, in Undecidability.FOLC.unscoped]
subs_sat' [lemma, in Undecidability.FOLC.GenTarski]
subs_sat [lemma, in Undecidability.FOLC.GenTarski]
subs_eval [lemma, in Undecidability.FOLC.GenTarski]
subs_interp_sat' [lemma, in Undecidability.FOLC.GenTarski]
subs_interp_sat [lemma, in Undecidability.FOLC.GenTarski]
subs_interp_eval [lemma, in Undecidability.FOLC.GenTarski]
subs_interp [definition, in Undecidability.FOLC.GenTarski]
subterm [inductive, in Undecidability.FOLC.FOL]
Subterm [section, in Undecidability.FOLC.FOL]
subterm_form [inductive, in Undecidability.FOLC.FOL]
↑ [notation, in Undecidability.FOLC.FOL]
Sup [definition, in Undecidability.FOLC.Heyting]
Sup_indexed1 [lemma, in Undecidability.FOLC.Heyting]
Sup_indexed [definition, in Undecidability.FOLC.Heyting]
Sup1 [lemma, in Undecidability.FOLC.Heyting]
Sup2 [lemma, in Undecidability.FOLC.Heyting]
svalid [definition, in Undecidability.FOLC.SDialogues]
svalid [definition, in Undecidability.FOLC.Sorensen]
svalid_dvalid [lemma, in Undecidability.FOLC.Sorensen]
swin_strat [inductive, in Undecidability.FOLC.SDialogues]
swin_dwin [lemma, in Undecidability.FOLC.Sorensen]
swin_dwin_embed [definition, in Undecidability.FOLC.Sorensen]
swin_strat [inductive, in Undecidability.FOLC.Sorensen]
switch_map [lemma, in Undecidability.FOLC.Enumeration]
SWS [constructor, in Undecidability.FOLC.SDialogues]
SWS [constructor, in Undecidability.FOLC.Sorensen]
Syntax [library]
T
TAbsurd [constructor, in Undecidability.FOLC.Gentzen]TAllE [constructor, in Undecidability.FOLC.Gentzen]
TAllI [constructor, in Undecidability.FOLC.Gentzen]
TAllL [constructor, in Undecidability.FOLC.Gentzen]
TAllR [constructor, in Undecidability.FOLC.Gentzen]
Tarski [section, in Undecidability.FOLC.Extend]
Tarski [section, in Undecidability.FOLC.FullTarski]
Tarski [section, in Undecidability.FOLC.GenTarski]
Tarski.d [variable, in Undecidability.FOLC.Extend]
Tarski.D [variable, in Undecidability.FOLC.Extend]
Tarski.I [variable, in Undecidability.FOLC.Extend]
Tarski.inj [variable, in Undecidability.FOLC.Extend]
Tarski.Semantics [section, in Undecidability.FOLC.FullTarski]
Tarski.Semantics [section, in Undecidability.FOLC.GenTarski]
Tarski.Semantics.domain [variable, in Undecidability.FOLC.FullTarski]
Tarski.Semantics.domain [variable, in Undecidability.FOLC.GenTarski]
Tarski.Soundness [section, in Undecidability.FOLC.GenTarski]
Tarski.Substs [section, in Undecidability.FOLC.FullTarski]
Tarski.Substs [section, in Undecidability.FOLC.GenTarski]
Tarski.Substs.D [variable, in Undecidability.FOLC.FullTarski]
Tarski.Substs.D [variable, in Undecidability.FOLC.GenTarski]
Tarski.Substs.I [variable, in Undecidability.FOLC.FullTarski]
Tarski.Substs.I [variable, in Undecidability.FOLC.GenTarski]
_ ⊫< _ > _ [notation, in Undecidability.FOLC.FullTarski]
_ ⊨ _ [notation, in Undecidability.FOLC.FullTarski]
_ ⊫M _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊫E _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊫S _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊫< _ > _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊨ _ [notation, in Undecidability.FOLC.GenTarski]
Tarski.Σ [variable, in Undecidability.FOLC.Extend]
Tarski.Σ' [variable, in Undecidability.FOLC.Extend]
TAx [constructor, in Undecidability.FOLC.Gentzen]
TContr [constructor, in Undecidability.FOLC.Gentzen]
TCtx [constructor, in Undecidability.FOLC.Gentzen]
tembed [definition, in Undecidability.FOLC.Gentzen]
term [inductive, in Undecidability.FOLC.Terms]
Terms [library]
term_T_form' [instance, in Undecidability.FOLC.LEnum]
term_cons''' [instance, in Undecidability.FOLC.LEnum]
term_L_seq [instance, in Undecidability.FOLC.LEnum]
term_form_shift' [instance, in Undecidability.FOLC.LEnum]
term_f5 [instance, in Undecidability.FOLC.LEnum]
term_subst_form' [instance, in Undecidability.FOLC.LEnum]
term_up_term_term' [instance, in Undecidability.FOLC.LEnum]
term_f7 [instance, in Undecidability.FOLC.LEnum]
term_f6 [instance, in Undecidability.FOLC.LEnum]
term_subst_term' [instance, in Undecidability.FOLC.LEnum]
term_scons [instance, in Undecidability.FOLC.LEnum]
term_f4 [instance, in Undecidability.FOLC.LEnum]
term_f3 [instance, in Undecidability.FOLC.LEnum]
term_existsb [instance, in Undecidability.FOLC.LEnum]
term_f2 [instance, in Undecidability.FOLC.LEnum]
term_f1 [instance, in Undecidability.FOLC.LEnum]
term_eqb_spec [lemma, in Undecidability.FOLC.LEnum]
term_eqb [definition, in Undecidability.FOLC.LEnum]
term_L_form' [instance, in Undecidability.FOLC.LEnum]
term_T_list' [instance, in Undecidability.FOLC.LEnum]
term_cons'' [instance, in Undecidability.FOLC.LEnum]
term_Pred'' [instance, in Undecidability.FOLC.LEnum]
term_Impl'' [instance, in Undecidability.FOLC.LEnum]
term_All' [instance, in Undecidability.FOLC.LEnum]
term_Impl' [instance, in Undecidability.FOLC.LEnum]
term_Pred' [instance, in Undecidability.FOLC.LEnum]
term_L_wf [instance, in Undecidability.FOLC.LEnum]
term_L_term' [instance, in Undecidability.FOLC.LEnum]
term_App'' [instance, in Undecidability.FOLC.LEnum]
term_App' [instance, in Undecidability.FOLC.LEnum]
term_Func' [instance, in Undecidability.FOLC.LEnum]
term_var_term' [instance, in Undecidability.FOLC.LEnum]
term' [inductive, in Undecidability.FOLC.LEnum]
TExp [constructor, in Undecidability.FOLC.Gentzen]
Th [definition, in Undecidability.FOLC.WKL]
theory [definition, in Undecidability.FOLC.FullFOL]
theory [definition, in Undecidability.FOLC.FOL]
TheoryManipulation [section, in Undecidability.FOLC.FullND]
TheoryManipulation [section, in Undecidability.FOLC.ND]
TIE [constructor, in Undecidability.FOLC.Gentzen]
TII [constructor, in Undecidability.FOLC.Gentzen]
TIL [constructor, in Undecidability.FOLC.Gentzen]
TIR [constructor, in Undecidability.FOLC.Gentzen]
tlexp [definition, in Undecidability.FOLC.WFexp]
tmap [definition, in Undecidability.FOLC.FullFOL]
tmap [definition, in Undecidability.FOLC.FOL]
tmap_contains_L [lemma, in Undecidability.FOLC.FullFOL]
tmap_contains_L [lemma, in Undecidability.FOLC.FOL]
todo [axiom, in Undecidability.FOLC.Lindenbaum]
tone [constructor, in Undecidability.FOLC.WFexp]
Top [definition, in Undecidability.FOLC.Heyting]
top_hsat_L [lemma, in Undecidability.FOLC.Lindenbaum]
Top1 [lemma, in Undecidability.FOLC.Heyting]
to_form_of_form [lemma, in Undecidability.FOLC.LEnum]
to_list_length [lemma, in Undecidability.FOLC.LEnum]
to_form [definition, in Undecidability.FOLC.LEnum]
to_term_of_term [lemma, in Undecidability.FOLC.LEnum]
to_term_mkApps [lemma, in Undecidability.FOLC.LEnum]
to_term [definition, in Undecidability.FOLC.LEnum]
to_False_iff [lemma, in Undecidability.FOLC.WKL]
to_list_length [lemma, in Undecidability.FOLC.WKL]
to_list_cast_of_list [lemma, in Undecidability.FOLC.WKL]
to_list_inj [lemma, in Undecidability.FOLC.WKL]
tprv [definition, in Undecidability.FOLC.FullND]
tprv [inductive, in Undecidability.FOLC.Gentzen]
tprv [definition, in Undecidability.FOLC.ND]
tprv_list_T [lemma, in Undecidability.FOLC.FullND]
tprv_list_T [lemma, in Undecidability.FOLC.ND]
trans [inductive, in Undecidability.FOLC.WFexp]
trans [definition, in Undecidability.FOLC.BPCP_CND]
Transitivity [section, in Undecidability.FOLC.WFexp]
Transitivity.R [variable, in Undecidability.FOLC.WFexp]
Transitivity.wf_R [variable, in Undecidability.FOLC.WFexp]
Transitivity.X [variable, in Undecidability.FOLC.WFexp]
TransWFexp [section, in Undecidability.FOLC.WFexp]
TransWFexp.R [variable, in Undecidability.FOLC.WFexp]
TransWFexp.wf_R [variable, in Undecidability.FOLC.WFexp]
TransWFexp.X [variable, in Undecidability.FOLC.WFexp]
trans_Transitive [instance, in Undecidability.FOLC.WFexp]
trans_trans [lemma, in Undecidability.FOLC.BPCP_CND]
trans_subst [lemma, in Undecidability.FOLC.BPCP_CND]
tree [record, in Undecidability.FOLC.WKL]
tree_is_tree [projection, in Undecidability.FOLC.WKL]
tree_T [projection, in Undecidability.FOLC.WKL]
tree_p [projection, in Undecidability.FOLC.WKL]
tree_inhab [projection, in Undecidability.FOLC.WKL]
tsat [definition, in Undecidability.FOLC.Stability]
tsprv [inductive, in Undecidability.FOLC.Gentzen]
ttwo [constructor, in Undecidability.FOLC.WFexp]
t_f [definition, in Undecidability.FOLC.BPCP_FOL]
t_e [definition, in Undecidability.FOLC.BPCP_FOL]
t_e' [constructor, in Undecidability.FOLC.BPCP_FOL]
t_f' [constructor, in Undecidability.FOLC.BPCP_FOL]
T_form_term' [definition, in Undecidability.FOLC.LEnum]
T_list_term' [definition, in Undecidability.FOLC.LEnum]
U
u [abbreviation, in Undecidability.FOLC.BPCP_FOL]ub [definition, in Undecidability.FOLC.Heyting]
ub_join [lemma, in Undecidability.FOLC.Heyting]
ub_proper [instance, in Undecidability.FOLC.Heyting]
uft_Func [constructor, in Undecidability.FOLC.Terms]
uft_var [constructor, in Undecidability.FOLC.Terms]
uf_Ex [constructor, in Undecidability.FOLC.FullFOL]
uf_All [constructor, in Undecidability.FOLC.FullFOL]
uf_O [constructor, in Undecidability.FOLC.FullFOL]
uf_A [constructor, in Undecidability.FOLC.FullFOL]
uf_I [constructor, in Undecidability.FOLC.FullFOL]
uf_Pred [constructor, in Undecidability.FOLC.FullFOL]
uf_Fal [constructor, in Undecidability.FOLC.FullFOL]
uf_All [constructor, in Undecidability.FOLC.FOL]
uf_Impl [constructor, in Undecidability.FOLC.FOL]
uf_Pred [constructor, in Undecidability.FOLC.FOL]
uf_Fal [constructor, in Undecidability.FOLC.FOL]
union [definition, in Undecidability.FOLC.GenConstructions]
union_closed [lemma, in Undecidability.FOLC.GenConstructions]
union_econsistent [lemma, in Undecidability.FOLC.GenConstructions]
union_sub [lemma, in Undecidability.FOLC.GenConstructions]
union_f [lemma, in Undecidability.FOLC.GenConstructions]
universal_interp_eval [lemma, in Undecidability.FOLC.KripkeCompleteness]
universal_interp [instance, in Undecidability.FOLC.KripkeCompleteness]
unscoped [library]
unused [inductive, in Undecidability.FOLC.FullFOL]
unused [inductive, in Undecidability.FOLC.FOL]
unused_L [definition, in Undecidability.FOLC.FullFOL]
unused_after_subst [lemma, in Undecidability.FOLC.FOL]
unused_after_subst_term [lemma, in Undecidability.FOLC.FOL]
unused_L [definition, in Undecidability.FOLC.FOL]
unused_enc [lemma, in Undecidability.FOLC.BPCP_FOL]
unused_prep [lemma, in Undecidability.FOLC.BPCP_FOL]
unused_big_imp [lemma, in Undecidability.FOLC.BPCP_FOL]
unused_term [inductive, in Undecidability.FOLC.Terms]
up [definition, in Undecidability.FOLC.SDialogues]
Up [definition, in Undecidability.FOLC.SDialogues]
upExt_term_term [definition, in Undecidability.FOLC.Terms]
upI [definition, in Undecidability.FOLC.SDialogues]
upId_term_term [definition, in Undecidability.FOLC.Terms]
upL [definition, in Undecidability.FOLC.SDialogues]
upV [definition, in Undecidability.FOLC.SDialogues]
up_upI [lemma, in Undecidability.FOLC.SDialogues]
up_upL [lemma, in Undecidability.FOLC.SDialogues]
up_ren_ren [lemma, in Undecidability.FOLC.unscoped]
up_ren [definition, in Undecidability.FOLC.unscoped]
up_term_term_pref_raise [lemma, in Undecidability.FOLC.FOL]
up_term_term_pref_ext_c' [lemma, in Undecidability.FOLC.FOL]
up_term_term_vsubs [lemma, in Undecidability.FOLC.FOL]
up_term_form [lemma, in Undecidability.FOLC.FullND]
up_term_term [lemma, in Undecidability.FOLC.FullND]
Up_term_term [instance, in Undecidability.FOLC.FullSyntax]
up_term [projection, in Undecidability.FOLC.FullSyntax]
Up_term [record, in Undecidability.FOLC.FullSyntax]
up_term [constructor, in Undecidability.FOLC.FullSyntax]
Up_term [inductive, in Undecidability.FOLC.FullSyntax]
Up_term_term [instance, in Undecidability.FOLC.Syntax]
up_term [projection, in Undecidability.FOLC.Syntax]
Up_term [record, in Undecidability.FOLC.Syntax]
up_term [constructor, in Undecidability.FOLC.Syntax]
Up_term [inductive, in Undecidability.FOLC.Syntax]
up_term_term' [definition, in Undecidability.FOLC.LEnum]
up_subst_subst_term_term [definition, in Undecidability.FOLC.Terms]
up_term_term [definition, in Undecidability.FOLC.Terms]
V
v [abbreviation, in Undecidability.FOLC.BPCP_FOL]validity [section, in Undecidability.FOLC.BPCP_FOL]
validity.R [variable, in Undecidability.FOLC.BPCP_FOL]
_ ⊫ _ [notation, in Undecidability.FOLC.BPCP_FOL]
valid_T_fragment [lemma, in Undecidability.FOLC.GenCompleteness]
valid_standard_expld_stability [lemma, in Undecidability.FOLC.GenCompleteness]
valid_T_model_bot [lemma, in Undecidability.FOLC.GenCompleteness]
valid_T_subsumption [lemma, in Undecidability.FOLC.FullTarski]
valid_L [definition, in Undecidability.FOLC.FullTarski]
valid_T [definition, in Undecidability.FOLC.FullTarski]
valid_L_to_single [lemma, in Undecidability.FOLC.GenTarski]
valid_L_valid_T [lemma, in Undecidability.FOLC.GenTarski]
valid_T_standard_dm [lemma, in Undecidability.FOLC.GenTarski]
valid_T_subsumption [lemma, in Undecidability.FOLC.GenTarski]
valid_L [definition, in Undecidability.FOLC.GenTarski]
valid_T [definition, in Undecidability.FOLC.GenTarski]
vapp [definition, in Undecidability.FOLC.SDialogues]
vapp_vmap [lemma, in Undecidability.FOLC.SDialogues]
Var [record, in Undecidability.FOLC.unscoped]
Var [inductive, in Undecidability.FOLC.unscoped]
variant [projection, in Undecidability.FOLC.GenConstructions]
VarInstance_term [instance, in Undecidability.FOLC.FullSyntax]
VarInstance_term [instance, in Undecidability.FOLC.Syntax]
varL_term [lemma, in Undecidability.FOLC.Terms]
varornot [inductive, in Undecidability.FOLC.LEnum]
var_subst_L [lemma, in Undecidability.FOLC.FullFOL]
var_subst [lemma, in Undecidability.FOLC.FullFOL]
var_zero [definition, in Undecidability.FOLC.unscoped]
var_term' [constructor, in Undecidability.FOLC.LEnum]
var_term [constructor, in Undecidability.FOLC.Terms]
vecs_from_correct [lemma, in Undecidability.FOLC.FOL]
vecs_from [definition, in Undecidability.FOLC.FOL]
vector [abbreviation, in Undecidability.FOLC.Terms]
Vector_to_list_map [lemma, in Undecidability.FOLC.WKL]
vec_map_map [lemma, in Undecidability.FOLC.Extend]
vec_comp [definition, in Undecidability.FOLC.Extend]
vec_comp [definition, in Undecidability.FOLC.axioms]
vec_id [definition, in Undecidability.FOLC.axioms]
vec_ext [definition, in Undecidability.FOLC.axioms]
vec_forall_map [lemma, in Undecidability.FOLC.FullFOL]
vec_map_ext [lemma, in Undecidability.FOLC.FullFOL]
vec_forall_cml [lemma, in Undecidability.FOLC.FOL]
vec_forall_map [lemma, in Undecidability.FOLC.FOL]
vec_map_ext [lemma, in Undecidability.FOLC.FOL]
vec_unused [lemma, in Undecidability.FOLC.Terms]
vec_inS [constructor, in Undecidability.FOLC.Terms]
vec_inB [constructor, in Undecidability.FOLC.Terms]
vec_in [inductive, in Undecidability.FOLC.Terms]
vec_to_env [definition, in Undecidability.FOLC.WKL]
vec2env [definition, in Undecidability.FOLC.Extend]
vec2env_correct [lemma, in Undecidability.FOLC.Extend]
vec2env_map [lemma, in Undecidability.FOLC.Extend]
vec2vars [definition, in Undecidability.FOLC.Extend]
venv [definition, in Undecidability.FOLC.GenTarski]
venv_empty [lemma, in Undecidability.FOLC.GenTarski]
venv_sat [lemma, in Undecidability.FOLC.GenTarski]
vmap [definition, in Undecidability.FOLC.SDialogues]
vmap_upV [lemma, in Undecidability.FOLC.SDialogues]
vsplit [definition, in Undecidability.FOLC.SDialogues]
vsubs [definition, in Undecidability.FOLC.FOL]
vsubs_single_subst [lemma, in Undecidability.FOLC.ND]
vsubs_form_shift [lemma, in Undecidability.FOLC.ND]
W
Weak [lemma, in Undecidability.FOLC.FullND]Weak [constructor, in Undecidability.FOLC.FullSequent]
Weak [lemma, in Undecidability.FOLC.ND]
weaken [lemma, in Undecidability.FOLC.FullSequent]
Weak_T [lemma, in Undecidability.FOLC.FullND]
Weak_T [lemma, in Undecidability.FOLC.ND]
wellfounded_tree [definition, in Undecidability.FOLC.WKL]
well_founded_tlexp [lemma, in Undecidability.FOLC.WFexp]
well_founded_trans [lemma, in Undecidability.FOLC.WFexp]
well_founded_lexp [lemma, in Undecidability.FOLC.WFexp]
well_founded_perm [lemma, in Undecidability.FOLC.WFexp]
well_founded_singleton_full [lemma, in Undecidability.FOLC.WFexp]
wf [inductive, in Undecidability.FOLC.LEnum]
WFexp [section, in Undecidability.FOLC.WFexp]
WFexp [library]
WFexp.R [variable, in Undecidability.FOLC.WFexp]
WFexp.wf_R [variable, in Undecidability.FOLC.WFexp]
WFexp.X [variable, in Undecidability.FOLC.WFexp]
WFlist [section, in Undecidability.FOLC.WFexp]
WFlist.R [variable, in Undecidability.FOLC.WFexp]
WFlist.R_app_r [variable, in Undecidability.FOLC.WFexp]
WFlist.R_app_l [variable, in Undecidability.FOLC.WFexp]
WFlist.R_app [variable, in Undecidability.FOLC.WFexp]
WFlist.X [variable, in Undecidability.FOLC.WFexp]
wf_of_form [lemma, in Undecidability.FOLC.LEnum]
wf_form [definition, in Undecidability.FOLC.LEnum]
wf_of_term [lemma, in Undecidability.FOLC.LEnum]
wf_app [constructor, in Undecidability.FOLC.LEnum]
wf_fun [constructor, in Undecidability.FOLC.LEnum]
wf_var [constructor, in Undecidability.FOLC.LEnum]
WKL [section, in Undecidability.FOLC.WKL]
WKL [definition, in Undecidability.FOLC.WKL]
WKL [library]
WKL_implies_modex [lemma, in Undecidability.FOLC.WKL]
WKL_to_decidable_data [lemma, in Undecidability.FOLC.WKL]
WKL_to_decidable [lemma, in Undecidability.FOLC.WKL]
WKL.T [variable, in Undecidability.FOLC.WKL]
X
XM [definition, in Undecidability.FOLC.DeMorgan]XM [definition, in Undecidability.FOLC.WKL]
XM_DN [lemma, in Undecidability.FOLC.DeMorgan]
other
[ _ ] (fscope) [notation, in Undecidability.FOLC.Syntax][ _ ] (fscope) [notation, in Undecidability.FOLC.Syntax]
⟨ _ ; _ ⟩ (fscope) [notation, in Undecidability.FOLC.unscoped]
⟨ _ ⟩ (fscope) [notation, in Undecidability.FOLC.unscoped]
_ .. (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ >> _ (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ [ _ ] (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in Undecidability.FOLC.unscoped]
_ [ _ ] (subst_scope) [notation, in Undecidability.FOLC.FullSyntax]
_ [ _ ] (subst_scope) [notation, in Undecidability.FOLC.FullSyntax]
↑__term (subst_scope) [notation, in Undecidability.FOLC.FullSyntax]
↑__term (subst_scope) [notation, in Undecidability.FOLC.FullSyntax]
var (subst_scope) [notation, in Undecidability.FOLC.FullSyntax]
_ __term (subst_scope) [notation, in Undecidability.FOLC.FullSyntax]
_ __term (subst_scope) [notation, in Undecidability.FOLC.FullSyntax]
_ [ _ ] (subst_scope) [notation, in Undecidability.FOLC.Syntax]
_ [ _ ] (subst_scope) [notation, in Undecidability.FOLC.Syntax]
↑__term (subst_scope) [notation, in Undecidability.FOLC.Syntax]
↑__term (subst_scope) [notation, in Undecidability.FOLC.Syntax]
var (subst_scope) [notation, in Undecidability.FOLC.Syntax]
_ __term (subst_scope) [notation, in Undecidability.FOLC.Syntax]
_ __term (subst_scope) [notation, in Undecidability.FOLC.Syntax]
_ o:: _ [notation, in Undecidability.FOLC.SDialogues]
_ ⟹ _ [notation, in Undecidability.FOLC.FullFOL]
_ ⋄ _ [notation, in Undecidability.FOLC.FullFOL]
_ ∈ _ [notation, in Undecidability.FOLC.FullFOL]
_ ⊑ _ [notation, in Undecidability.FOLC.FullFOL]
_ ⊏ _ [notation, in Undecidability.FOLC.FullFOL]
_ ∨ _ [notation, in Undecidability.FOLC.FullFOL]
_ ∧ _ [notation, in Undecidability.FOLC.FullFOL]
_ --> _ [notation, in Undecidability.FOLC.FullFOL]
_ .: _ [notation, in Undecidability.FOLC.unscoped]
_ ⟹ _ [notation, in Undecidability.FOLC.FOL]
_ ⋄ _ [notation, in Undecidability.FOLC.FOL]
_ ∈ _ [notation, in Undecidability.FOLC.FOL]
_ ⊑ _ [notation, in Undecidability.FOLC.FOL]
_ ⊏ _ [notation, in Undecidability.FOLC.FOL]
_ --> _ [notation, in Undecidability.FOLC.FOL]
_ ⊫< _ > _ [notation, in Undecidability.FOLC.FullTarski]
_ ⊨ _ [notation, in Undecidability.FOLC.FullTarski]
_ ⊩IE _ [notation, in Undecidability.FOLC.FullND]
_ ⊩CL _ [notation, in Undecidability.FOLC.FullND]
_ ⊩CE _ [notation, in Undecidability.FOLC.FullND]
_ ⊩( _ , _ ) _ [notation, in Undecidability.FOLC.FullND]
_ ⊩ _ [notation, in Undecidability.FOLC.FullND]
_ ⊢IE _ [notation, in Undecidability.FOLC.FullND]
_ ⊢CL _ [notation, in Undecidability.FOLC.FullND]
_ ⊢CE _ [notation, in Undecidability.FOLC.FullND]
_ ⊢( _ , _ ) _ [notation, in Undecidability.FOLC.FullND]
_ ⊢ _ [notation, in Undecidability.FOLC.FullND]
_ ⊩SE _ [notation, in Undecidability.FOLC.Gentzen]
_ ;; _ ⊢sL _ [notation, in Undecidability.FOLC.Gentzen]
_ ⊢SL _ [notation, in Undecidability.FOLC.Gentzen]
_ ;; _ ⊢sE _ [notation, in Undecidability.FOLC.Gentzen]
_ ⊢SE _ [notation, in Undecidability.FOLC.Gentzen]
_ ;; _ ⊢s _ [notation, in Undecidability.FOLC.Gentzen]
_ ⊢S _ [notation, in Undecidability.FOLC.Gentzen]
_ == _ [notation, in Undecidability.FOLC.WFexp]
_ ≡ _ [notation, in Undecidability.FOLC.Heyting]
_ ⊆ _ [notation, in Undecidability.FOLC.Heyting]
_ ∈ _ [notation, in Undecidability.FOLC.Heyting]
_ <= _ [notation, in Undecidability.FOLC.Heyting]
_ ⊫KBL _ [notation, in Undecidability.FOLC.Kripke]
_ ⊫KS _ [notation, in Undecidability.FOLC.Kripke]
_ ⊫KE _ [notation, in Undecidability.FOLC.Kripke]
_ ⊨( _ , _ ) _ [notation, in Undecidability.FOLC.Kripke]
_ ⊨( _ ) _ [notation, in Undecidability.FOLC.Kripke]
_ ⊫M _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊫E _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊫S _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊫< _ > _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊨ _ [notation, in Undecidability.FOLC.GenTarski]
_ ⊢f _ [notation, in Undecidability.FOLC.FullSequent]
_ ⊩IE _ [notation, in Undecidability.FOLC.ND]
_ ⊩CL _ [notation, in Undecidability.FOLC.ND]
_ ⊩CE _ [notation, in Undecidability.FOLC.ND]
_ ⊩( _ , _ ) _ [notation, in Undecidability.FOLC.ND]
_ ⊩ _ [notation, in Undecidability.FOLC.ND]
_ ⊢IE _ [notation, in Undecidability.FOLC.ND]
_ ⊢CL _ [notation, in Undecidability.FOLC.ND]
_ ⊢CE _ [notation, in Undecidability.FOLC.ND]
_ ⊢( _ , _ ) _ [notation, in Undecidability.FOLC.ND]
_ ⊢ _ [notation, in Undecidability.FOLC.ND]
_ ⊢D _ [notation, in Undecidability.FOLC.Sorensen]
_ o:: _ [notation, in Undecidability.FOLC.Sorensen]
c∃ _ [notation, in Undecidability.FOLC.FullND]
¬ _ [notation, in Undecidability.FOLC.FullFOL]
¬ _ [notation, in Undecidability.FOLC.FOL]
↑ [notation, in Undecidability.FOLC.FullFOL]
↑ [notation, in Undecidability.FOLC.unscoped]
↑ [notation, in Undecidability.FOLC.FOL]
∀ _ [notation, in Undecidability.FOLC.FullFOL]
∀ _ [notation, in Undecidability.FOLC.FOL]
∃ _ [notation, in Undecidability.FOLC.FullFOL]
∃ _ [notation, in Undecidability.FOLC.FOL]
⊥ [notation, in Undecidability.FOLC.FullFOL]
⊥ [notation, in Undecidability.FOLC.FOL]
⋁ _ [notation, in Undecidability.FOLC.FullSequent]
Notation Index
C
_ <~> _ (type_scope) [in Undecidability.FOLC.Heyting]F
_ ⋄ _ [in Undecidability.FOLC.FOL]_ ∈ _ [in Undecidability.FOLC.FOL]
_ ⊑ _ [in Undecidability.FOLC.FOL]
_ ⊏ _ [in Undecidability.FOLC.FOL]
_ ⋄ _ [in Undecidability.FOLC.FullFOL]
_ ∈ _ [in Undecidability.FOLC.FullFOL]
_ ⊑ _ [in Undecidability.FOLC.FullFOL]
_ ⊏ _ [in Undecidability.FOLC.FullFOL]
↑ [in Undecidability.FOLC.FullFOL]
_ ⊢f _ [in Undecidability.FOLC.FullSequent]
⋁ _ [in Undecidability.FOLC.FullSequent]
G
_ ∘ _ [in Undecidability.FOLC.GenConstructions]_ ⊩G _ [in Undecidability.FOLC.GenConstructions]
_ ⊢G _ [in Undecidability.FOLC.GenConstructions]
¬ _ [in Undecidability.FOLC.GenConstructions]
∃ _ [in Undecidability.FOLC.GenConstructions]
⊥ [in Undecidability.FOLC.GenConstructions]
_ ;; _ ⊢s _ [in Undecidability.FOLC.Gentzen]
_ ⊢S _ [in Undecidability.FOLC.Gentzen]
H
_ ≡ _ [in Undecidability.FOLC.Heyting]K
_ ;; _ ⊢sC _ [in Undecidability.FOLC.KripkeCompleteness]_ ⊢SC _ [in Undecidability.FOLC.KripkeCompleteness]
_ <<=C _ [in Undecidability.FOLC.KripkeCompleteness]
_ ⊨( _ , _ ) _ [in Undecidability.FOLC.Kripke]
_ ⊨( _ ) _ [in Undecidability.FOLC.Kripke]
L
_ ⊢ _ [in Undecidability.FOLC.Lindenbaum]_ ⊢E _ [in Undecidability.FOLC.Lindenbaum]
_ ⊢D _ [in Undecidability.FOLC.Sorensen]
M
_ ≡ _ [in Undecidability.FOLC.Heyting]_ ⊆ _ [in Undecidability.FOLC.Heyting]
_ ∈ _ [in Undecidability.FOLC.Heyting]
N
_ ⊩IE _ [in Undecidability.FOLC.FullND]_ ⊩CL _ [in Undecidability.FOLC.FullND]
_ ⊩CE _ [in Undecidability.FOLC.FullND]
_ ⊩( _ , _ ) _ [in Undecidability.FOLC.FullND]
_ ⊩ _ [in Undecidability.FOLC.FullND]
_ ⊢IE _ [in Undecidability.FOLC.FullND]
_ ⊢CL _ [in Undecidability.FOLC.FullND]
_ ⊢CE _ [in Undecidability.FOLC.FullND]
_ ⊢( _ , _ ) _ [in Undecidability.FOLC.FullND]
_ ⊢ _ [in Undecidability.FOLC.FullND]
_ ⊢ _ [in Undecidability.FOLC.FullND]
↑ [in Undecidability.FOLC.FullND]
_ ⊩IE _ [in Undecidability.FOLC.ND]
_ ⊩CL _ [in Undecidability.FOLC.ND]
_ ⊩CE _ [in Undecidability.FOLC.ND]
_ ⊩( _ , _ ) _ [in Undecidability.FOLC.ND]
_ ⊩ _ [in Undecidability.FOLC.ND]
_ ⊢IE _ [in Undecidability.FOLC.ND]
_ ⊢CL _ [in Undecidability.FOLC.ND]
_ ⊢CE _ [in Undecidability.FOLC.ND]
_ ⊢( _ , _ ) _ [in Undecidability.FOLC.ND]
_ ⊢ _ [in Undecidability.FOLC.ND]
S
_ ⪍' _ [in Undecidability.FOLC.SDialogues]_ ⪍ _ [in Undecidability.FOLC.SDialogues]
_ ⊢D _ [in Undecidability.FOLC.SDialogues]
↑ [in Undecidability.FOLC.FOL]
T
_ ⊫< _ > _ [in Undecidability.FOLC.FullTarski]_ ⊨ _ [in Undecidability.FOLC.FullTarski]
_ ⊫M _ [in Undecidability.FOLC.GenTarski]
_ ⊫E _ [in Undecidability.FOLC.GenTarski]
_ ⊫S _ [in Undecidability.FOLC.GenTarski]
_ ⊫< _ > _ [in Undecidability.FOLC.GenTarski]
_ ⊨ _ [in Undecidability.FOLC.GenTarski]
V
_ ⊫ _ [in Undecidability.FOLC.BPCP_FOL]other
[ _ ] (fscope) [in Undecidability.FOLC.Syntax][ _ ] (fscope) [in Undecidability.FOLC.Syntax]
⟨ _ ; _ ⟩ (fscope) [in Undecidability.FOLC.unscoped]
⟨ _ ⟩ (fscope) [in Undecidability.FOLC.unscoped]
_ .. (subst_scope) [in Undecidability.FOLC.unscoped]
_ >> _ (subst_scope) [in Undecidability.FOLC.unscoped]
_ [ _ ; _ ] (subst_scope) [in Undecidability.FOLC.unscoped]
_ [ _ ] (subst_scope) [in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in Undecidability.FOLC.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in Undecidability.FOLC.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in Undecidability.FOLC.unscoped]
_ [ _ ] (subst_scope) [in Undecidability.FOLC.FullSyntax]
_ [ _ ] (subst_scope) [in Undecidability.FOLC.FullSyntax]
↑__term (subst_scope) [in Undecidability.FOLC.FullSyntax]
↑__term (subst_scope) [in Undecidability.FOLC.FullSyntax]
var (subst_scope) [in Undecidability.FOLC.FullSyntax]
_ __term (subst_scope) [in Undecidability.FOLC.FullSyntax]
_ __term (subst_scope) [in Undecidability.FOLC.FullSyntax]
_ [ _ ] (subst_scope) [in Undecidability.FOLC.Syntax]
_ [ _ ] (subst_scope) [in Undecidability.FOLC.Syntax]
↑__term (subst_scope) [in Undecidability.FOLC.Syntax]
↑__term (subst_scope) [in Undecidability.FOLC.Syntax]
var (subst_scope) [in Undecidability.FOLC.Syntax]
_ __term (subst_scope) [in Undecidability.FOLC.Syntax]
_ __term (subst_scope) [in Undecidability.FOLC.Syntax]
_ o:: _ [in Undecidability.FOLC.SDialogues]
_ ⟹ _ [in Undecidability.FOLC.FullFOL]
_ ⋄ _ [in Undecidability.FOLC.FullFOL]
_ ∈ _ [in Undecidability.FOLC.FullFOL]
_ ⊑ _ [in Undecidability.FOLC.FullFOL]
_ ⊏ _ [in Undecidability.FOLC.FullFOL]
_ ∨ _ [in Undecidability.FOLC.FullFOL]
_ ∧ _ [in Undecidability.FOLC.FullFOL]
_ --> _ [in Undecidability.FOLC.FullFOL]
_ .: _ [in Undecidability.FOLC.unscoped]
_ ⟹ _ [in Undecidability.FOLC.FOL]
_ ⋄ _ [in Undecidability.FOLC.FOL]
_ ∈ _ [in Undecidability.FOLC.FOL]
_ ⊑ _ [in Undecidability.FOLC.FOL]
_ ⊏ _ [in Undecidability.FOLC.FOL]
_ --> _ [in Undecidability.FOLC.FOL]
_ ⊫< _ > _ [in Undecidability.FOLC.FullTarski]
_ ⊨ _ [in Undecidability.FOLC.FullTarski]
_ ⊩IE _ [in Undecidability.FOLC.FullND]
_ ⊩CL _ [in Undecidability.FOLC.FullND]
_ ⊩CE _ [in Undecidability.FOLC.FullND]
_ ⊩( _ , _ ) _ [in Undecidability.FOLC.FullND]
_ ⊩ _ [in Undecidability.FOLC.FullND]
_ ⊢IE _ [in Undecidability.FOLC.FullND]
_ ⊢CL _ [in Undecidability.FOLC.FullND]
_ ⊢CE _ [in Undecidability.FOLC.FullND]
_ ⊢( _ , _ ) _ [in Undecidability.FOLC.FullND]
_ ⊢ _ [in Undecidability.FOLC.FullND]
_ ⊩SE _ [in Undecidability.FOLC.Gentzen]
_ ;; _ ⊢sL _ [in Undecidability.FOLC.Gentzen]
_ ⊢SL _ [in Undecidability.FOLC.Gentzen]
_ ;; _ ⊢sE _ [in Undecidability.FOLC.Gentzen]
_ ⊢SE _ [in Undecidability.FOLC.Gentzen]
_ ;; _ ⊢s _ [in Undecidability.FOLC.Gentzen]
_ ⊢S _ [in Undecidability.FOLC.Gentzen]
_ == _ [in Undecidability.FOLC.WFexp]
_ ≡ _ [in Undecidability.FOLC.Heyting]
_ ⊆ _ [in Undecidability.FOLC.Heyting]
_ ∈ _ [in Undecidability.FOLC.Heyting]
_ <= _ [in Undecidability.FOLC.Heyting]
_ ⊫KBL _ [in Undecidability.FOLC.Kripke]
_ ⊫KS _ [in Undecidability.FOLC.Kripke]
_ ⊫KE _ [in Undecidability.FOLC.Kripke]
_ ⊨( _ , _ ) _ [in Undecidability.FOLC.Kripke]
_ ⊨( _ ) _ [in Undecidability.FOLC.Kripke]
_ ⊫M _ [in Undecidability.FOLC.GenTarski]
_ ⊫E _ [in Undecidability.FOLC.GenTarski]
_ ⊫S _ [in Undecidability.FOLC.GenTarski]
_ ⊫< _ > _ [in Undecidability.FOLC.GenTarski]
_ ⊨ _ [in Undecidability.FOLC.GenTarski]
_ ⊢f _ [in Undecidability.FOLC.FullSequent]
_ ⊩IE _ [in Undecidability.FOLC.ND]
_ ⊩CL _ [in Undecidability.FOLC.ND]
_ ⊩CE _ [in Undecidability.FOLC.ND]
_ ⊩( _ , _ ) _ [in Undecidability.FOLC.ND]
_ ⊩ _ [in Undecidability.FOLC.ND]
_ ⊢IE _ [in Undecidability.FOLC.ND]
_ ⊢CL _ [in Undecidability.FOLC.ND]
_ ⊢CE _ [in Undecidability.FOLC.ND]
_ ⊢( _ , _ ) _ [in Undecidability.FOLC.ND]
_ ⊢ _ [in Undecidability.FOLC.ND]
_ ⊢D _ [in Undecidability.FOLC.Sorensen]
_ o:: _ [in Undecidability.FOLC.Sorensen]
c∃ _ [in Undecidability.FOLC.FullND]
¬ _ [in Undecidability.FOLC.FullFOL]
¬ _ [in Undecidability.FOLC.FOL]
↑ [in Undecidability.FOLC.FullFOL]
↑ [in Undecidability.FOLC.unscoped]
↑ [in Undecidability.FOLC.FOL]
∀ _ [in Undecidability.FOLC.FullFOL]
∀ _ [in Undecidability.FOLC.FOL]
∃ _ [in Undecidability.FOLC.FullFOL]
∃ _ [in Undecidability.FOLC.FOL]
⊥ [in Undecidability.FOLC.FullFOL]
⊥ [in Undecidability.FOLC.FOL]
⋁ _ [in Undecidability.FOLC.FullSequent]
Variable Index
B
BPCP_CND.R [in Undecidability.FOLC.BPCP_CND]C
ClosingValidity.C [in Undecidability.FOLC.GenTarski]ClosingValidity.HC [in Undecidability.FOLC.GenTarski]
ClosingValidity.Hprv [in Undecidability.FOLC.GenTarski]
ClosingValidity.phi [in Undecidability.FOLC.GenTarski]
ClosingValidity.T [in Undecidability.FOLC.GenTarski]
Completeness.BotModel.T [in Undecidability.FOLC.GenCompleteness]
Completeness.BotModel.T_closed [in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.Hphi [in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.HT [in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.phi [in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes.T [in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.GBot [in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.GBot_closed [in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.T [in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel.T_closed [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.He [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.Hphi [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.HT [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.L [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.mp [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.phi [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness.T [in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.Hphi [in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.HT [in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.phi [in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes.T [in Undecidability.FOLC.GenCompleteness]
Consistency.Classical.XM [in Undecidability.FOLC.Consistency]
D
DGame.f [in Undecidability.FOLC.Sorensen]DGame.R [in Undecidability.FOLC.Sorensen]
DialogFull.eq_dec_Preds [in Undecidability.FOLC.DialogFull]
DialogFull.eq_dec_Funcs [in Undecidability.FOLC.DialogFull]
E
EGame.f [in Undecidability.FOLC.Sorensen]EGame.R [in Undecidability.FOLC.Sorensen]
Enumerability.enum_Preds [in Undecidability.FOLC.FOL]
Enumerability.enum_Funcs [in Undecidability.FOLC.FOL]
Enumeration.Hlen [in Undecidability.FOLC.Enumeration]
Enumeration.X [in Undecidability.FOLC.Enumeration]
enum_inj.H [in Undecidability.FOLC.Markov]
enum_inj.XD [in Undecidability.FOLC.Markov]
enum_inj.X [in Undecidability.FOLC.Markov]
EqDec.eq_dec_Preds [in Undecidability.FOLC.FullFOL]
EqDec.eq_dec_Funcs [in Undecidability.FOLC.FullFOL]
EqDec.eq_dec_Preds [in Undecidability.FOLC.FOL]
EqDec.eq_dec_Funcs [in Undecidability.FOLC.FOL]
G
GenCons.Explosion.e [in Undecidability.FOLC.GenConstructions]GenCons.Explosion.Hclosed [in Undecidability.FOLC.GenConstructions]
GenCons.Explosion.He [in Undecidability.FOLC.GenConstructions]
GenCons.Explosion.T [in Undecidability.FOLC.GenConstructions]
GenCons.GBot [in Undecidability.FOLC.GenConstructions]
GenCons.GBot_closed [in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.e [in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.Hclosed [in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.He [in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.Hexp [in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.Hunused [in Undecidability.FOLC.GenConstructions]
GenCons.Henkin.T [in Undecidability.FOLC.GenConstructions]
GenCons.Omega.e [in Undecidability.FOLC.GenConstructions]
GenCons.Omega.He [in Undecidability.FOLC.GenConstructions]
GenCons.Omega.Hexp [in Undecidability.FOLC.GenConstructions]
GenCons.Omega.Hhenkin [in Undecidability.FOLC.GenConstructions]
GenCons.Omega.T [in Undecidability.FOLC.GenConstructions]
GenCons.Union.econsistent_f [in Undecidability.FOLC.GenConstructions]
GenCons.Union.f [in Undecidability.FOLC.GenConstructions]
GenCons.Union.f_le [in Undecidability.FOLC.GenConstructions]
I
inj_enum.d [in Undecidability.FOLC.Markov]inj_enum.e [in Undecidability.FOLC.Markov]
inj_enum.Sigma [in Undecidability.FOLC.Markov]
K
KripkeCompleteness.MPRequired.C [in Undecidability.FOLC.KripkeCompleteness]KripkeCompleteness.MPRequired.HC [in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.MPRequired.K_completeness [in Undecidability.FOLC.KripkeCompleteness]
Kripke.d [in Undecidability.FOLC.Extend]
Kripke.D [in Undecidability.FOLC.Extend]
Kripke.inj [in Undecidability.FOLC.Extend]
Kripke.M [in Undecidability.FOLC.Extend]
Kripke.Model.domain [in Undecidability.FOLC.Kripke]
Kripke.Model.M [in Undecidability.FOLC.Kripke]
Kripke.Substs.D [in Undecidability.FOLC.Kripke]
Kripke.Σ [in Undecidability.FOLC.Extend]
Kripke.Σ' [in Undecidability.FOLC.Extend]
L
Lindenbaum.CHAEval.hinter_Pr [in Undecidability.FOLC.Lindenbaum]Lindenbaum.Completeness.gAllE [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gAllI [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCE1 [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCE2 [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCI [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gCtx [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gDE [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gDI1 [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gDI2 [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gExE [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gExI [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gExp [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gIE [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gII [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gnameless_equiv_ex' [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gnameless_equiv_all' [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gprv [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness.gWeak [in Undecidability.FOLC.Lindenbaum]
LJD.f [in Undecidability.FOLC.Sorensen]
LJD.R [in Undecidability.FOLC.Sorensen]
L_T_unused.enum_Preds [in Undecidability.FOLC.Enumeration]
L_T_unused.enum_Funcs [in Undecidability.FOLC.Enumeration]
S
SDialogues.f [in Undecidability.FOLC.SDialogues]SDialogues.R [in Undecidability.FOLC.SDialogues]
SDialogues.Up.g [in Undecidability.FOLC.SDialogues]
SDialogues.Up.P [in Undecidability.FOLC.SDialogues]
SDialogues.Up.X [in Undecidability.FOLC.SDialogues]
SDialogues.Up.Y [in Undecidability.FOLC.SDialogues]
SDialogues.Up.Z [in Undecidability.FOLC.SDialogues]
SGame.f [in Undecidability.FOLC.Sorensen]
SGame.R [in Undecidability.FOLC.Sorensen]
SigExt.D [in Undecidability.FOLC.GenTarski]
SigExt.F [in Undecidability.FOLC.GenTarski]
SigExt.F_ar [in Undecidability.FOLC.GenTarski]
SigExt.P [in Undecidability.FOLC.GenTarski]
SigExt.P_ar [in Undecidability.FOLC.GenTarski]
StabilityClasses.SyntMP.MPEnum.HL [in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.HX [in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.L [in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.mp [in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.P [in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum.X [in Undecidability.FOLC.Stability]
T
Tarski.d [in Undecidability.FOLC.Extend]Tarski.D [in Undecidability.FOLC.Extend]
Tarski.I [in Undecidability.FOLC.Extend]
Tarski.inj [in Undecidability.FOLC.Extend]
Tarski.Semantics.domain [in Undecidability.FOLC.FullTarski]
Tarski.Semantics.domain [in Undecidability.FOLC.GenTarski]
Tarski.Substs.D [in Undecidability.FOLC.FullTarski]
Tarski.Substs.D [in Undecidability.FOLC.GenTarski]
Tarski.Substs.I [in Undecidability.FOLC.FullTarski]
Tarski.Substs.I [in Undecidability.FOLC.GenTarski]
Tarski.Σ [in Undecidability.FOLC.Extend]
Tarski.Σ' [in Undecidability.FOLC.Extend]
Transitivity.R [in Undecidability.FOLC.WFexp]
Transitivity.wf_R [in Undecidability.FOLC.WFexp]
Transitivity.X [in Undecidability.FOLC.WFexp]
TransWFexp.R [in Undecidability.FOLC.WFexp]
TransWFexp.wf_R [in Undecidability.FOLC.WFexp]
TransWFexp.X [in Undecidability.FOLC.WFexp]
V
validity.R [in Undecidability.FOLC.BPCP_FOL]W
WFexp.R [in Undecidability.FOLC.WFexp]WFexp.wf_R [in Undecidability.FOLC.WFexp]
WFexp.X [in Undecidability.FOLC.WFexp]
WFlist.R [in Undecidability.FOLC.WFexp]
WFlist.R_app_r [in Undecidability.FOLC.WFexp]
WFlist.R_app_l [in Undecidability.FOLC.WFexp]
WFlist.R_app [in Undecidability.FOLC.WFexp]
WFlist.X [in Undecidability.FOLC.WFexp]
WKL.T [in Undecidability.FOLC.WKL]
Library Index
A
Analysisaxioms
B
BPCP_FOLBPCP_CND
C
ConsistencyD
DeMorganDialogFragment
DialogFull
E
EnumerationExtend
F
FOLFullFOL
FullND
FullSequent
FullSyntax
FullTarski
G
GenCompletenessGenConstructions
GenTarski
Gentzen
H
HeytingK
KripkeKripkeCompleteness
L
LEnumLindenbaum
M
MarkovN
NDS
SDialoguesSorensen
Stability
Syntax
T
TermsU
unscopedW
WFexpWKL
Lemma Index
A
Acc_iff [in Undecidability.FOLC.WFexp]Acc_perm' [in Undecidability.FOLC.WFexp]
Acc_perm [in Undecidability.FOLC.WFexp]
Acc_app_rev [in Undecidability.FOLC.WFexp]
Acc_app [in Undecidability.FOLC.WFexp]
And_sat [in Undecidability.FOLC.WKL]
any_T_map_closed [in Undecidability.FOLC.Stability]
appCtx [in Undecidability.FOLC.BPCP_CND]
app_split_two [in Undecidability.FOLC.WFexp]
app1 [in Undecidability.FOLC.BPCP_CND]
app2 [in Undecidability.FOLC.BPCP_CND]
app3 [in Undecidability.FOLC.BPCP_CND]
atomic_dec [in Undecidability.FOLC.DialogFull]
atomic_dec [in Undecidability.FOLC.DialogFragment]
attack_form_inv_ext [in Undecidability.FOLC.DialogFull]
attack_form_inv_all [in Undecidability.FOLC.DialogFull]
attack_form_inv_or [in Undecidability.FOLC.DialogFull]
attack_form_inv_and [in Undecidability.FOLC.DialogFull]
attack_form_inv_impl [in Undecidability.FOLC.DialogFull]
attack_form_inv_all [in Undecidability.FOLC.DialogFragment]
attack_form_inv_impl [in Undecidability.FOLC.DialogFragment]
AXM [in Undecidability.FOLC.FullND]
AXM [in Undecidability.FOLC.ND]
B
bcompleteness [in Undecidability.FOLC.Lindenbaum]big_imp_extract [in Undecidability.FOLC.FullND]
big_imp_valid_L [in Undecidability.FOLC.GenTarski]
big_imp_extract [in Undecidability.FOLC.ND]
BL_E_subsumption [in Undecidability.FOLC.GenTarski]
boolean_completion [in Undecidability.FOLC.Lindenbaum]
bool_true_Prop [in Undecidability.FOLC.LEnum]
bounded_infinite_contra [in Undecidability.FOLC.WKL]
BPCP_prv [in Undecidability.FOLC.BPCP_FOL]
BPCP_prv' [in Undecidability.FOLC.BPCP_FOL]
BPCP_valid [in Undecidability.FOLC.BPCP_FOL]
BPCP_CND [in Undecidability.FOLC.BPCP_CND]
BPCP_to_CND [in Undecidability.FOLC.BPCP_CND]
bsoundness [in Undecidability.FOLC.Lindenbaum]
BSoundness [in Undecidability.FOLC.Lindenbaum]
BSoundness' [in Undecidability.FOLC.Lindenbaum]
C
capture_captures [in Undecidability.FOLC.FullFOL]capture_captures [in Undecidability.FOLC.FOL]
capture_extract [in Undecidability.FOLC.FullND]
capture_extract [in Undecidability.FOLC.ND]
cast_trans [in Undecidability.FOLC.Extend]
cast_eq [in Undecidability.FOLC.Extend]
cast_app [in Undecidability.FOLC.LEnum]
cast_nil [in Undecidability.FOLC.LEnum]
cast_refl [in Undecidability.FOLC.WKL]
cend_dn [in Undecidability.FOLC.KripkeCompleteness]
clb_alg_boolean [in Undecidability.FOLC.Lindenbaum]
closed_T_extend [in Undecidability.FOLC.FullFOL]
closed_T_extend [in Undecidability.FOLC.FOL]
closed_F [in Undecidability.FOLC.BPCP_FOL]
closed_Th [in Undecidability.FOLC.WKL]
close_closed [in Undecidability.FOLC.FullFOL]
close_closed [in Undecidability.FOLC.FOL]
close_extract [in Undecidability.FOLC.FullND]
close_valid_L [in Undecidability.FOLC.GenTarski]
close_extract [in Undecidability.FOLC.ND]
CND_BPCP [in Undecidability.FOLC.BPCP_CND]
compact_implies_WKL_D [in Undecidability.FOLC.WKL]
compact_OM_implies_WKL [in Undecidability.FOLC.WKL]
compact_OM_implies_WKL' [in Undecidability.FOLC.WKL]
compact_implies_WKL [in Undecidability.FOLC.WKL]
compact_implies_WKL' [in Undecidability.FOLC.WKL]
compact_DM_WKLD [in Undecidability.FOLC.WKL]
compact_OM_WKL [in Undecidability.FOLC.WKL]
compact_DM_WKL [in Undecidability.FOLC.WKL]
compact_standard [in Undecidability.FOLC.WKL]
compComp_form [in Undecidability.FOLC.FullSyntax]
compComp_form [in Undecidability.FOLC.Syntax]
compComp_term [in Undecidability.FOLC.Terms]
compComp'_form [in Undecidability.FOLC.FullSyntax]
compComp'_form [in Undecidability.FOLC.Syntax]
compComp'_term [in Undecidability.FOLC.Terms]
completeness_expl [in Undecidability.FOLC.GenCompleteness]
completeness_standard_stability [in Undecidability.FOLC.GenCompleteness]
completeness_transport [in Undecidability.FOLC.Analysis]
completeness_iff_XM [in Undecidability.FOLC.Analysis]
completeness_enum_iff_MP [in Undecidability.FOLC.Analysis]
completeness_context_iff_MPL [in Undecidability.FOLC.Analysis]
comp_modex [in Undecidability.FOLC.WKL]
Consistency [in Undecidability.FOLC.GenTarski]
consistency_inheritance [in Undecidability.FOLC.Consistency]
consistent_join_step [in Undecidability.FOLC.GenConstructions]
consistent_max_out2 [in Undecidability.FOLC.Consistency]
consistent_max_impl [in Undecidability.FOLC.Consistency]
consistent_max_out [in Undecidability.FOLC.Consistency]
consistent_neg2 [in Undecidability.FOLC.Consistency]
consistent_neg [in Undecidability.FOLC.Consistency]
consistent_prv [in Undecidability.FOLC.Consistency]
construct_construction [in Undecidability.FOLC.GenConstructions]
contains_extend3 [in Undecidability.FOLC.FullFOL]
contains_extend2 [in Undecidability.FOLC.FullFOL]
contains_extend1 [in Undecidability.FOLC.FullFOL]
contains_app [in Undecidability.FOLC.FullFOL]
contains_cons2 [in Undecidability.FOLC.FullFOL]
contains_cons [in Undecidability.FOLC.FullFOL]
contains_nil [in Undecidability.FOLC.FullFOL]
contains_extend3 [in Undecidability.FOLC.FOL]
contains_extend2 [in Undecidability.FOLC.FOL]
contains_extend1 [in Undecidability.FOLC.FOL]
contains_app [in Undecidability.FOLC.FOL]
contains_cons2 [in Undecidability.FOLC.FOL]
contains_cons [in Undecidability.FOLC.FOL]
contains_nil [in Undecidability.FOLC.FOL]
context_shift [in Undecidability.FOLC.FullSequent]
converges_eva [in Undecidability.FOLC.Markov]
convert_embed [in Undecidability.FOLC.DeMorgan]
con_T_correct [in Undecidability.FOLC.Stability]
CO_iff_EM_WKL [in Undecidability.FOLC.WKL]
cprv_iprv_stable [in Undecidability.FOLC.Markov]
cprv_iprv [in Undecidability.FOLC.Markov]
cprv_red [in Undecidability.FOLC.BPCP_CND]
ctx_in [in Undecidability.FOLC.FullSequent]
ctx_out [in Undecidability.FOLC.FullSequent]
cutfree_seq_ND [in Undecidability.FOLC.Gentzen]
cycle_shift_subject [in Undecidability.FOLC.FullND]
cycle_shift_shift [in Undecidability.FOLC.FullND]
cycle_shift_subject [in Undecidability.FOLC.FullSequent]
cycle_shift_shift [in Undecidability.FOLC.FullSequent]
cycle_shift_subject [in Undecidability.FOLC.ND]
cycle_shift_shift [in Undecidability.FOLC.ND]
D
dcompleteness [in Undecidability.FOLC.Sorensen]decidable_to_decidable_data [in Undecidability.FOLC.WKL]
decidable_to_decidable [in Undecidability.FOLC.WKL]
decidable_to_decidable_n [in Undecidability.FOLC.WKL]
decidable_to_omniscient [in Undecidability.FOLC.WKL]
dec_vec_in [in Undecidability.FOLC.FullFOL]
dec_vec_in [in Undecidability.FOLC.FOL]
dec2bool_iff [in Undecidability.FOLC.WKL]
Dlift_le_wf [in Undecidability.FOLC.SDialogues]
DMT_sat_back [in Undecidability.FOLC.DeMorgan]
DMT_closed [in Undecidability.FOLC.DeMorgan]
DMT_unused [in Undecidability.FOLC.DeMorgan]
DMT_incl [in Undecidability.FOLC.DeMorgan]
DMT_valid [in Undecidability.FOLC.DeMorgan]
DMT_sat [in Undecidability.FOLC.DeMorgan]
DMT_prv [in Undecidability.FOLC.DeMorgan]
DMT_subst [in Undecidability.FOLC.DeMorgan]
DM_prv [in Undecidability.FOLC.DeMorgan]
DN [in Undecidability.FOLC.FullND]
DN [in Undecidability.FOLC.ND]
dnt_to_CE [in Undecidability.FOLC.FullND]
dnt_remove_ctx [in Undecidability.FOLC.FullND]
dnt_CE [in Undecidability.FOLC.FullND]
dnt_to_IE [in Undecidability.FOLC.FullND]
dnt_float [in Undecidability.FOLC.FullND]
dnt_subst [in Undecidability.FOLC.FullND]
dnt_to_TCE [in Undecidability.FOLC.ND]
dnt_to_CE [in Undecidability.FOLC.ND]
dnt_remove_ctx [in Undecidability.FOLC.ND]
dnt_unused [in Undecidability.FOLC.ND]
dnt_CE [in Undecidability.FOLC.ND]
dnt_to_TIE [in Undecidability.FOLC.ND]
dnt_to_IE [in Undecidability.FOLC.ND]
dnt_float [in Undecidability.FOLC.ND]
dnt_subst [in Undecidability.FOLC.ND]
dn_inherit [in Undecidability.FOLC.GenCompleteness]
dn_to_sta [in Undecidability.FOLC.Stability]
DN_T [in Undecidability.FOLC.ND]
Double [in Undecidability.FOLC.BPCP_CND]
Double' [in Undecidability.FOLC.BPCP_CND]
down_inf [in Undecidability.FOLC.Heyting]
down_impl [in Undecidability.FOLC.Heyting]
down_join [in Undecidability.FOLC.Heyting]
down_meet [in Undecidability.FOLC.Heyting]
down_top [in Undecidability.FOLC.Heyting]
down_bot [in Undecidability.FOLC.Heyting]
down_mono [in Undecidability.FOLC.Heyting]
down_inj [in Undecidability.FOLC.Heyting]
down_normal [in Undecidability.FOLC.Heyting]
DP [in Undecidability.FOLC.FullND]
DP [in Undecidability.FOLC.ND]
Dprv_svalid [in Undecidability.FOLC.SDialogues]
Dprv_swin [in Undecidability.FOLC.SDialogues]
Dprv_fprv_equiv [in Undecidability.FOLC.DialogFull]
Dprv_fprv [in Undecidability.FOLC.DialogFull]
Dprv_fprv' [in Undecidability.FOLC.DialogFull]
Dprv_ND [in Undecidability.FOLC.DialogFragment]
Dprv_just [in Undecidability.FOLC.Sorensen]
Dprv_ax [in Undecidability.FOLC.Sorensen]
Dprv_echo [in Undecidability.FOLC.Sorensen]
Dprv_exp [in Undecidability.FOLC.Sorensen]
Dprv_defend [in Undecidability.FOLC.Sorensen]
Dprv_weak [in Undecidability.FOLC.Sorensen]
Dprv_ewin [in Undecidability.FOLC.Sorensen]
droppable_BL [in Undecidability.FOLC.GenTarski]
droppable_E [in Undecidability.FOLC.GenTarski]
droppable_S [in Undecidability.FOLC.GenTarski]
droppable_exploding_bot [in Undecidability.FOLC.GenTarski]
droppable_standard_bot [in Undecidability.FOLC.GenTarski]
droppable_classical [in Undecidability.FOLC.GenTarski]
drop_interp'_sat [in Undecidability.FOLC.GenTarski]
drop_interp'_eval [in Undecidability.FOLC.GenTarski]
drv_prv [in Undecidability.FOLC.BPCP_FOL]
drv_val [in Undecidability.FOLC.BPCP_FOL]
dummy_SM [in Undecidability.FOLC.GenTarski]
dummy_xm [in Undecidability.FOLC.GenTarski]
dwin_Dprv [in Undecidability.FOLC.Sorensen]
E
ecompleteness [in Undecidability.FOLC.Sorensen]econsistency_trans [in Undecidability.FOLC.GenConstructions]
econsistency_inheritance [in Undecidability.FOLC.GenConstructions]
econsistent_prv [in Undecidability.FOLC.GenConstructions]
econsistent_Omega [in Undecidability.FOLC.GenConstructions]
econsistent_join_sub [in Undecidability.FOLC.GenConstructions]
eequiv [in Undecidability.FOLC.Sorensen]
elem_prv [in Undecidability.FOLC.FullND]
elem_prv [in Undecidability.FOLC.ND]
el_at_pos [in Undecidability.FOLC.Enumeration]
embed_subst [in Undecidability.FOLC.Extend]
embed_subst_term [in Undecidability.FOLC.Extend]
embed_prv [in Undecidability.FOLC.DeMorgan]
embed_subst [in Undecidability.FOLC.DeMorgan]
embed_DMT [in Undecidability.FOLC.DeMorgan]
enumeration_stability [in Undecidability.FOLC.Stability]
enumeration_semi_decidable [in Undecidability.FOLC.Stability]
enum_tmap [in Undecidability.FOLC.FullFOL]
enum_halt [in Undecidability.FOLC.Markov]
enum_tmap [in Undecidability.FOLC.FOL]
enum_stprv [in Undecidability.FOLC.Gentzen]
enum_sprv [in Undecidability.FOLC.Gentzen]
enum_tsat_T [in Undecidability.FOLC.Stability]
enum_T_map_closed_homo [in Undecidability.FOLC.Stability]
enum_T_map_closed_closing [in Undecidability.FOLC.Stability]
enum_sprvie [in Undecidability.FOLC.LEnum]
enum_sprv [in Undecidability.FOLC.LEnum]
enum_wf [in Undecidability.FOLC.LEnum]
enum_tprv [in Undecidability.FOLC.ND]
enum_containsL [in Undecidability.FOLC.ND]
enum_p [in Undecidability.FOLC.ND]
enum_el [in Undecidability.FOLC.ND]
enum_prv [in Undecidability.FOLC.ND]
eq_incl [in Undecidability.FOLC.DialogFull]
eq_incl [in Undecidability.FOLC.DialogFragment]
esoundness [in Undecidability.FOLC.Sorensen]
evalid_fprv_equiv [in Undecidability.FOLC.DialogFull]
eval_retract [in Undecidability.FOLC.Extend]
eval_ident_fragment [in Undecidability.FOLC.GenCompleteness]
eval_ident [in Undecidability.FOLC.GenCompleteness]
eval_id [in Undecidability.FOLC.KripkeCompleteness]
eval_comp [in Undecidability.FOLC.FullTarski]
eval_ext [in Undecidability.FOLC.FullTarski]
eval_comp [in Undecidability.FOLC.GenTarski]
eval_ext [in Undecidability.FOLC.GenTarski]
eval_ext_unused [in Undecidability.FOLC.GenTarski]
ewin_Dprv [in Undecidability.FOLC.Sorensen]
ExE [in Undecidability.FOLC.ND]
ExE' [in Undecidability.FOLC.FullND]
ExI [in Undecidability.FOLC.ND]
exists_quasi_path [in Undecidability.FOLC.WKL]
ExI' [in Undecidability.FOLC.FullND]
exploding_inherit [in Undecidability.FOLC.GenConstructions]
Exp_exploding [in Undecidability.FOLC.GenConstructions]
Exp_closed [in Undecidability.FOLC.GenConstructions]
Exp_econsistent [in Undecidability.FOLC.GenConstructions]
Exp_sub [in Undecidability.FOLC.GenConstructions]
exp_axiom_lift [in Undecidability.FOLC.GenConstructions]
ext_c'_unused [in Undecidability.FOLC.FOL]
ext_c'_unused_term [in Undecidability.FOLC.FOL]
ext_form' [in Undecidability.FOLC.LEnum]
ext_term' [in Undecidability.FOLC.LEnum]
E_S_subsumption [in Undecidability.FOLC.GenTarski]
F
fAll_sat [in Undecidability.FOLC.WKL]fAll_sat' [in Undecidability.FOLC.WKL]
fExists_sat [in Undecidability.FOLC.WKL]
fExists_sat' [in Undecidability.FOLC.WKL]
find_unused_L [in Undecidability.FOLC.FullFOL]
find_unused [in Undecidability.FOLC.FullFOL]
find_unused_L [in Undecidability.FOLC.FOL]
find_unused [in Undecidability.FOLC.FOL]
find_unused_term [in Undecidability.FOLC.Terms]
fin_T_to_context [in Undecidability.FOLC.Stability]
fin_T_con_T [in Undecidability.FOLC.Stability]
fin_T_map_closed [in Undecidability.FOLC.Stability]
flat_map_app [in Undecidability.FOLC.Enumeration]
focus_el [in Undecidability.FOLC.FullSequent]
Forall_app [in Undecidability.FOLC.WKL]
Forall2_length [in Undecidability.FOLC.WKL]
Forall2_In1 [in Undecidability.FOLC.WKL]
Forall2_In [in Undecidability.FOLC.WKL]
form_ind_subst [in Undecidability.FOLC.FullFOL]
form_ind_subst [in Undecidability.FOLC.FOL]
form_ind_subst' [in Undecidability.FOLC.FullND]
form_eqb_spec [in Undecidability.FOLC.LEnum]
form_enum_fresh [in Undecidability.FOLC.Enumeration]
form_enum_enumerates [in Undecidability.FOLC.Enumeration]
fprv_defend [in Undecidability.FOLC.DialogFull]
fprv_Dprv [in Undecidability.FOLC.DialogFull]
full_completeness [in Undecidability.FOLC.DeMorgan]
Func_cast [in Undecidability.FOLC.LEnum]
G
GDN [in Undecidability.FOLC.GenConstructions]GDP [in Undecidability.FOLC.GenConstructions]
get_index_list [in Undecidability.FOLC.WKL]
GExE [in Undecidability.FOLC.GenConstructions]
GExI [in Undecidability.FOLC.GenConstructions]
GExp [in Undecidability.FOLC.GenConstructions]
glb_calg_iff [in Undecidability.FOLC.Lindenbaum]
glb_alg_iff [in Undecidability.FOLC.Lindenbaum]
glindenbaum_eqH [in Undecidability.FOLC.Lindenbaum]
glindenbaum_hsat [in Undecidability.FOLC.Lindenbaum]
GXM [in Undecidability.FOLC.GenConstructions]
H
halt_cprv_stable [in Undecidability.FOLC.Markov]halt_cprv [in Undecidability.FOLC.Markov]
has_model_OM_DM [in Undecidability.FOLC.WKL]
hcompleteness [in Undecidability.FOLC.Lindenbaum]
Henkin_T [in Undecidability.FOLC.GenConstructions]
Henkin_is_Henkin [in Undecidability.FOLC.GenConstructions]
Henkin_consistent [in Undecidability.FOLC.GenConstructions]
henkin_le [in Undecidability.FOLC.GenConstructions]
henkin_unused [in Undecidability.FOLC.GenConstructions]
henkin_axiom_unused [in Undecidability.FOLC.GenConstructions]
hset_inf1 [in Undecidability.FOLC.Heyting]
hset_impl1 [in Undecidability.FOLC.Heyting]
hset_join1 [in Undecidability.FOLC.Heyting]
hset_meet1 [in Undecidability.FOLC.Heyting]
hset_bot1 [in Undecidability.FOLC.Heyting]
hset_impl_normal [in Undecidability.FOLC.Heyting]
hset_impl_equiv [in Undecidability.FOLC.Heyting]
hset_inf_normal [in Undecidability.FOLC.Heyting]
hset_join_normal [in Undecidability.FOLC.Heyting]
hset_meet_normal [in Undecidability.FOLC.Heyting]
hset_bot_normal [in Undecidability.FOLC.Heyting]
hsoundness [in Undecidability.FOLC.Lindenbaum]
I
IB_F [in Undecidability.FOLC.BPCP_FOL]IB_F3 [in Undecidability.FOLC.BPCP_FOL]
IB_F2 [in Undecidability.FOLC.BPCP_FOL]
IB_F1 [in Undecidability.FOLC.BPCP_FOL]
IB_drv [in Undecidability.FOLC.BPCP_FOL]
IB_enc [in Undecidability.FOLC.BPCP_FOL]
IB_prep [in Undecidability.FOLC.BPCP_FOL]
IE_to_CE [in Undecidability.FOLC.FullND]
IE_to_CE [in Undecidability.FOLC.ND]
iff_1b_2b [in Undecidability.FOLC.Analysis]
iff_1a_2a [in Undecidability.FOLC.Analysis]
impl_prv [in Undecidability.FOLC.BPCP_FOL]
impl_sat [in Undecidability.FOLC.BPCP_FOL]
impl_5_2a [in Undecidability.FOLC.Analysis]
impl_4_5 [in Undecidability.FOLC.Analysis]
impl_3b_4 [in Undecidability.FOLC.Analysis]
impl_3a_4 [in Undecidability.FOLC.Analysis]
impl_2b_3b [in Undecidability.FOLC.Analysis]
impl_2a_3a [in Undecidability.FOLC.Analysis]
impl_2a_2b [in Undecidability.FOLC.Analysis]
impl_trans [in Undecidability.FOLC.BPCP_CND]
Imp_bot [in Undecidability.FOLC.Heyting]
Imp2 [in Undecidability.FOLC.Heyting]
incl_eq [in Undecidability.FOLC.DeMorgan]
inconsistent [in Undecidability.FOLC.Consistency]
infinite_finitely_satisfiable' [in Undecidability.FOLC.WKL]
infinite_finitely_satisfiable [in Undecidability.FOLC.WKL]
infinite_iff [in Undecidability.FOLC.WKL]
Inf_indexed1 [in Undecidability.FOLC.Heyting]
Inf2 [in Undecidability.FOLC.Heyting]
instId_form [in Undecidability.FOLC.FullSyntax]
instId_form [in Undecidability.FOLC.Syntax]
instId_term [in Undecidability.FOLC.Terms]
in_eqb_spec [in Undecidability.FOLC.LEnum]
in_mapi_iff [in Undecidability.FOLC.WKL]
iprep_app [in Undecidability.FOLC.BPCP_FOL]
iprep_eval [in Undecidability.FOLC.BPCP_FOL]
iprv_halt_stable [in Undecidability.FOLC.Markov]
iprv_halt [in Undecidability.FOLC.Markov]
iprv_maxprv [in Undecidability.FOLC.Markov]
is_Henkin_inherit [in Undecidability.FOLC.GenConstructions]
Is_filter_exists [in Undecidability.FOLC.WKL]
Is_Filter_func [in Undecidability.FOLC.WKL]
Is_Filter_In [in Undecidability.FOLC.WKL]
Is_Filter_filter [in Undecidability.FOLC.WKL]
J
Join_com [in Undecidability.FOLC.Heyting]Join2 [in Undecidability.FOLC.Heyting]
Join3 [in Undecidability.FOLC.Heyting]
justified_weak [in Undecidability.FOLC.SDialogues]
justified_weak [in Undecidability.FOLC.Sorensen]
K
kcompleteness_implies_XM [in Undecidability.FOLC.Analysis]kcompleteness_enum_implies_MP [in Undecidability.FOLC.Analysis]
kcompleteness_iff_MPL [in Undecidability.FOLC.Analysis]
kexploding_retract [in Undecidability.FOLC.Extend]
kexploding_preds [in Undecidability.FOLC.Extend]
ksat_retract [in Undecidability.FOLC.Extend]
ksat_comp [in Undecidability.FOLC.Kripke]
ksat_ext [in Undecidability.FOLC.Kripke]
ksat_iff [in Undecidability.FOLC.Kripke]
ksat_mon [in Undecidability.FOLC.Kripke]
ksemantic_explosion [in Undecidability.FOLC.Kripke]
ksoundness [in Undecidability.FOLC.Kripke]
ksoundness_seq [in Undecidability.FOLC.Gentzen]
ksoundness' [in Undecidability.FOLC.Kripke]
kstandard_explodes [in Undecidability.FOLC.Kripke]
kvalid_L_subs [in Undecidability.FOLC.Kripke]
K_std_seq_ksoundness [in Undecidability.FOLC.KripkeCompleteness]
K_std_completeness [in Undecidability.FOLC.KripkeCompleteness]
K_std_ksat [in Undecidability.FOLC.KripkeCompleteness]
K_std_sprv' [in Undecidability.FOLC.KripkeCompleteness]
K_std_sprv [in Undecidability.FOLC.KripkeCompleteness]
K_std_correct [in Undecidability.FOLC.KripkeCompleteness]
K_std_standard [in Undecidability.FOLC.KripkeCompleteness]
K_bottomless_completeness [in Undecidability.FOLC.KripkeCompleteness]
K_exp_seq_ksoundness [in Undecidability.FOLC.KripkeCompleteness]
K_exp_completeness [in Undecidability.FOLC.KripkeCompleteness]
K_ctx_exploding [in Undecidability.FOLC.KripkeCompleteness]
K_ctx_ksat [in Undecidability.FOLC.KripkeCompleteness]
K_ctx_sprv' [in Undecidability.FOLC.KripkeCompleteness]
K_ctx_subst [in Undecidability.FOLC.KripkeCompleteness]
K_ctx_sprv [in Undecidability.FOLC.KripkeCompleteness]
K_ctx_constraint [in Undecidability.FOLC.KripkeCompleteness]
K_ctx_correct [in Undecidability.FOLC.KripkeCompleteness]
L
lb_calg_iff [in Undecidability.FOLC.Lindenbaum]lb_alg_iff [in Undecidability.FOLC.Lindenbaum]
lb_normal [in Undecidability.FOLC.Heyting]
lexp_perm_lexp' [in Undecidability.FOLC.WFexp]
lexp'_app_r [in Undecidability.FOLC.WFexp]
lexp'_app_l [in Undecidability.FOLC.WFexp]
lexp'_single [in Undecidability.FOLC.WFexp]
lexp'_nil [in Undecidability.FOLC.WFexp]
lexp'_app [in Undecidability.FOLC.WFexp]
lift_ext_c_closes_T [in Undecidability.FOLC.FOL]
lift_ext_c_closes [in Undecidability.FOLC.FOL]
lift_drop_inverse [in Undecidability.FOLC.FOL]
lift_drop_inverse' [in Undecidability.FOLC.FOL]
lift_drop_inverse_term' [in Undecidability.FOLC.FOL]
lift_interp_sat [in Undecidability.FOLC.GenTarski]
lift_interp_eval [in Undecidability.FOLC.GenTarski]
lindenbaum_eqH [in Undecidability.FOLC.Lindenbaum]
lindenbaum_hsat [in Undecidability.FOLC.Lindenbaum]
listable_list_length [in Undecidability.FOLC.WKL]
list_completeness_fragment [in Undecidability.FOLC.GenCompleteness]
list_completeness_expl [in Undecidability.FOLC.GenCompleteness]
list_completeness_standard [in Undecidability.FOLC.GenCompleteness]
list_prod_in [in Undecidability.FOLC.FOL]
list_or_spec [in Undecidability.FOLC.FullTarski]
lu_idem [in Undecidability.FOLC.Heyting]
lu_sub [in Undecidability.FOLC.Heyting]
L_form_cml [in Undecidability.FOLC.FOL]
L_term_cml [in Undecidability.FOLC.FOL]
L_T_form_len [in Undecidability.FOLC.Enumeration]
L_T_sub_or [in Undecidability.FOLC.Enumeration]
L_T_sub [in Undecidability.FOLC.Enumeration]
L_T_unused [in Undecidability.FOLC.Enumeration]
L_T_unused_v [in Undecidability.FOLC.Enumeration]
L_T_unused_t [in Undecidability.FOLC.Enumeration]
L_T_nat_le [in Undecidability.FOLC.Enumeration]
M
mapi_app [in Undecidability.FOLC.WKL]map_subst [in Undecidability.FOLC.Lindenbaum]
map_nth_id [in Undecidability.FOLC.WKL]
maximal_prv [in Undecidability.FOLC.GenConstructions]
maximal_Omega [in Undecidability.FOLC.GenConstructions]
maxprv_sprv [in Undecidability.FOLC.Markov]
max_list_spec' [in Undecidability.FOLC.WKL]
max_list_spec [in Undecidability.FOLC.WKL]
Meet_hsat_L [in Undecidability.FOLC.Lindenbaum]
meet_sup_expansion [in Undecidability.FOLC.Heyting]
meet_sup_distr [in Undecidability.FOLC.Heyting]
meet_join_expansion [in Undecidability.FOLC.Heyting]
meet_join_distr [in Undecidability.FOLC.Heyting]
Meet_extend [in Undecidability.FOLC.Heyting]
Meet_assoc [in Undecidability.FOLC.Heyting]
Meet_left [in Undecidability.FOLC.Heyting]
Meet_com [in Undecidability.FOLC.Heyting]
Meet2 [in Undecidability.FOLC.Heyting]
Meet3 [in Undecidability.FOLC.Heyting]
model_fragment_classical [in Undecidability.FOLC.GenCompleteness]
model_fragment_correct [in Undecidability.FOLC.GenCompleteness]
model_bot_exploding [in Undecidability.FOLC.GenCompleteness]
model_bot_standard [in Undecidability.FOLC.GenCompleteness]
model_bot_classical [in Undecidability.FOLC.GenCompleteness]
model_bot_correct [in Undecidability.FOLC.GenCompleteness]
model_u [in Undecidability.FOLC.WKL]
modex_comp [in Undecidability.FOLC.Analysis]
modex_impl_OM_DM [in Undecidability.FOLC.WKL]
modex_impl [in Undecidability.FOLC.WKL]
modex_compact [in Undecidability.FOLC.WKL]
modex_standard [in Undecidability.FOLC.WKL]
MPL_independent [in Undecidability.FOLC.Markov]
mp_standard_completeness [in Undecidability.FOLC.GenCompleteness]
mp_tprv_stability [in Undecidability.FOLC.GenCompleteness]
MP_MPL [in Undecidability.FOLC.Markov]
MP_enum_stable_iff [in Undecidability.FOLC.Markov]
mp_to_ste [in Undecidability.FOLC.Stability]
M_u_omni [in Undecidability.FOLC.WKL]
M_u_dec [in Undecidability.FOLC.WKL]
M_u_SB [in Undecidability.FOLC.WKL]
N
nameless_equiv_ex' [in Undecidability.FOLC.FullND]nameless_equiv_all' [in Undecidability.FOLC.FullND]
nameless_equiv_ex [in Undecidability.FOLC.FullND]
nameless_equiv_all [in Undecidability.FOLC.FullND]
nameless_equiv' [in Undecidability.FOLC.FullSequent]
nameless_equiv [in Undecidability.FOLC.FullSequent]
nameless_equiv_all' [in Undecidability.FOLC.BPCP_CND]
nameless_equiv [in Undecidability.FOLC.ND]
natinj_inj [in Undecidability.FOLC.Markov]
nd_to_sequent [in Undecidability.FOLC.Analysis]
ND_defend [in Undecidability.FOLC.DialogFragment]
Neg_sat [in Undecidability.FOLC.WKL]
normal_bot [in Undecidability.FOLC.Heyting]
normal_dclosed [in Undecidability.FOLC.Heyting]
nthe_seq [in Undecidability.FOLC.WKL]
nth_order_map [in Undecidability.FOLC.FOL]
O
ocons_sub' [in Undecidability.FOLC.SDialogues]ocons_sub [in Undecidability.FOLC.SDialogues]
ocons_sub [in Undecidability.FOLC.Sorensen]
ofnat_natinj [in Undecidability.FOLC.Markov]
ofNat_correct [in Undecidability.FOLC.Markov]
of_form_wf [in Undecidability.FOLC.LEnum]
of_list_wf [in Undecidability.FOLC.LEnum]
of_term_wf [in Undecidability.FOLC.LEnum]
of_term_wf' [in Undecidability.FOLC.LEnum]
Omega_all [in Undecidability.FOLC.GenConstructions]
Omega_impl [in Undecidability.FOLC.GenConstructions]
Omega_T [in Undecidability.FOLC.GenConstructions]
Omega_prv [in Undecidability.FOLC.GenConstructions]
omega_le [in Undecidability.FOLC.GenConstructions]
omniscient_on_fAll_sat [in Undecidability.FOLC.WKL]
omniscient_on_fExists_sat [in Undecidability.FOLC.WKL]
omniscient_on_And [in Undecidability.FOLC.WKL]
omniscient_on_Or [in Undecidability.FOLC.WKL]
omniscient_on_Neg [in Undecidability.FOLC.WKL]
omniscient_to_decidable [in Undecidability.FOLC.WKL]
omniscient_to_classical [in Undecidability.FOLC.WKL]
option_map_map [in Undecidability.FOLC.LEnum]
option_map_id [in Undecidability.FOLC.LEnum]
or_single [in Undecidability.FOLC.FullSequent]
or_weak [in Undecidability.FOLC.FullSequent]
or_el [in Undecidability.FOLC.FullSequent]
or_char [in Undecidability.FOLC.FullSequent]
or_subst [in Undecidability.FOLC.FullSequent]
Or_sat [in Undecidability.FOLC.WKL]
P
path_wellfounded_contra [in Undecidability.FOLC.WKL]PCO_implies_modex [in Undecidability.FOLC.WKL]
Permutation_cons_split [in Undecidability.FOLC.WFexp]
perm_R [in Undecidability.FOLC.WFexp]
phi_exists [in Undecidability.FOLC.WKL]
phi_down [in Undecidability.FOLC.WKL]
pi [in Undecidability.FOLC.axioms]
plain_enum_slow [in Undecidability.FOLC.Enumeration]
plain_enum_enumerates [in Undecidability.FOLC.Enumeration]
Pred_cast [in Undecidability.FOLC.LEnum]
prep_subst [in Undecidability.FOLC.BPCP_FOL]
prop_T_correct [in Undecidability.FOLC.Stability]
prvie_prv [in Undecidability.FOLC.LEnum]
prvie_prv' [in Undecidability.FOLC.LEnum]
prv_back [in Undecidability.FOLC.Extend]
prv_embed [in Undecidability.FOLC.Extend]
prv_cut_list [in Undecidability.FOLC.DeMorgan]
prv_T_comp [in Undecidability.FOLC.FullND]
prv_T_remove [in Undecidability.FOLC.FullND]
prv_T_impl [in Undecidability.FOLC.FullND]
prv_from_single [in Undecidability.FOLC.FullND]
prv_cut [in Undecidability.FOLC.FullND]
prv_prvie [in Undecidability.FOLC.LEnum]
prv_T_comp [in Undecidability.FOLC.ND]
prv_T_remove [in Undecidability.FOLC.ND]
prv_T_impl [in Undecidability.FOLC.ND]
prv_from_single [in Undecidability.FOLC.ND]
prv_cut [in Undecidability.FOLC.ND]
R
refutation_prv [in Undecidability.FOLC.FullND]refutation_prv [in Undecidability.FOLC.ND]
ren_form_to_form [in Undecidability.FOLC.LEnum]
ren_term_to_term' [in Undecidability.FOLC.LEnum]
ren_term_to_term [in Undecidability.FOLC.LEnum]
S
sat_subst [in Undecidability.FOLC.FullTarski]sat_comp [in Undecidability.FOLC.FullTarski]
sat_ext [in Undecidability.FOLC.FullTarski]
sat_subst [in Undecidability.FOLC.GenTarski]
sat_comp [in Undecidability.FOLC.GenTarski]
sat_ext [in Undecidability.FOLC.GenTarski]
sat_ext_unused [in Undecidability.FOLC.GenTarski]
scons_comp [in Undecidability.FOLC.unscoped]
scons_eta_id [in Undecidability.FOLC.unscoped]
scons_eta [in Undecidability.FOLC.unscoped]
semantic_dm [in Undecidability.FOLC.GenTarski]
semi_completeness_fragment [in Undecidability.FOLC.GenCompleteness]
semi_completeness_standard [in Undecidability.FOLC.GenCompleteness]
seq_ND_T [in Undecidability.FOLC.Gentzen]
seq_ND [in Undecidability.FOLC.Gentzen]
seq_nameless_equiv [in Undecidability.FOLC.Gentzen]
seq_subst_Weak [in Undecidability.FOLC.Gentzen]
seq_Weak [in Undecidability.FOLC.Gentzen]
seq_consistent [in Undecidability.FOLC.Gentzen]
SE_cut [in Undecidability.FOLC.KripkeCompleteness]
sf_well_founded [in Undecidability.FOLC.FullFOL]
sf_acc [in Undecidability.FOLC.FullFOL]
sf_form_rules [in Undecidability.FOLC.DialogFull]
sf_well_founded [in Undecidability.FOLC.FOL]
sf_acc [in Undecidability.FOLC.FOL]
sf_form_rules [in Undecidability.FOLC.DialogFragment]
sig_drop_subst' [in Undecidability.FOLC.FOL]
sig_drop_subst_term' [in Undecidability.FOLC.FOL]
sig_lift_subst [in Undecidability.FOLC.FOL]
sig_lift_subst_term [in Undecidability.FOLC.FOL]
sig_lift_subst_valid [in Undecidability.FOLC.GenTarski]
sig_lift_subst_sat [in Undecidability.FOLC.GenTarski]
sig_lift_out_T [in Undecidability.FOLC.ND]
sig_lift_out [in Undecidability.FOLC.ND]
sig_drop_Weak [in Undecidability.FOLC.ND]
sig_lift_Weak [in Undecidability.FOLC.ND]
size_ind [in Undecidability.FOLC.FullFOL]
size_ind [in Undecidability.FOLC.FOL]
Soundness [in Undecidability.FOLC.Lindenbaum]
Soundness [in Undecidability.FOLC.GenTarski]
Soundness' [in Undecidability.FOLC.Lindenbaum]
Soundness' [in Undecidability.FOLC.GenTarski]
split_right [in Undecidability.FOLC.Sorensen]
sprv_prv_iff [in Undecidability.FOLC.Extend]
sprv_sprvie [in Undecidability.FOLC.Markov]
sprv_Dprv [in Undecidability.FOLC.DialogFragment]
stable_red [in Undecidability.FOLC.Markov]
stable_equiv [in Undecidability.FOLC.Stability]
sta_to_dn [in Undecidability.FOLC.Stability]
ste_to_mp [in Undecidability.FOLC.Stability]
stf_to_st_context [in Undecidability.FOLC.Stability]
StrongSoundness [in Undecidability.FOLC.GenTarski]
strong_completeness_fragment [in Undecidability.FOLC.GenCompleteness]
strong_completeness_expl [in Undecidability.FOLC.GenCompleteness]
strong_completeness_standard [in Undecidability.FOLC.GenCompleteness]
strong_term_ind [in Undecidability.FOLC.Terms]
strong_term_ind' [in Undecidability.FOLC.Terms]
strong_ksoundness [in Undecidability.FOLC.Kripke]
subst_unused_closed' [in Undecidability.FOLC.FullFOL]
subst_unused_closed [in Undecidability.FOLC.FullFOL]
subst_unused_range [in Undecidability.FOLC.FullFOL]
subst_unused_single [in Undecidability.FOLC.FullFOL]
subst_unused_form [in Undecidability.FOLC.FullFOL]
subst_unused_term [in Undecidability.FOLC.FullFOL]
subst_size [in Undecidability.FOLC.FullFOL]
subst_unused_closed' [in Undecidability.FOLC.FOL]
subst_unused_closed [in Undecidability.FOLC.FOL]
subst_unused_range [in Undecidability.FOLC.FOL]
subst_unused_single [in Undecidability.FOLC.FOL]
subst_unused_form [in Undecidability.FOLC.FOL]
subst_unused_term [in Undecidability.FOLC.FOL]
subst_size [in Undecidability.FOLC.FOL]
subst_Weak [in Undecidability.FOLC.FullND]
subst_form_of_form [in Undecidability.FOLC.LEnum]
subst_term_map [in Undecidability.FOLC.LEnum]
subst_term_of_term [in Undecidability.FOLC.LEnum]
subst_Weak [in Undecidability.FOLC.FullSequent]
subst_Weak [in Undecidability.FOLC.ND]
subs_sat' [in Undecidability.FOLC.GenTarski]
subs_sat [in Undecidability.FOLC.GenTarski]
subs_eval [in Undecidability.FOLC.GenTarski]
subs_interp_sat' [in Undecidability.FOLC.GenTarski]
subs_interp_sat [in Undecidability.FOLC.GenTarski]
subs_interp_eval [in Undecidability.FOLC.GenTarski]
Sup_indexed1 [in Undecidability.FOLC.Heyting]
Sup1 [in Undecidability.FOLC.Heyting]
Sup2 [in Undecidability.FOLC.Heyting]
svalid_dvalid [in Undecidability.FOLC.Sorensen]
swin_dwin [in Undecidability.FOLC.Sorensen]
switch_map [in Undecidability.FOLC.Enumeration]
T
term_eqb_spec [in Undecidability.FOLC.LEnum]tmap_contains_L [in Undecidability.FOLC.FullFOL]
tmap_contains_L [in Undecidability.FOLC.FOL]
top_hsat_L [in Undecidability.FOLC.Lindenbaum]
Top1 [in Undecidability.FOLC.Heyting]
to_form_of_form [in Undecidability.FOLC.LEnum]
to_list_length [in Undecidability.FOLC.LEnum]
to_term_of_term [in Undecidability.FOLC.LEnum]
to_term_mkApps [in Undecidability.FOLC.LEnum]
to_False_iff [in Undecidability.FOLC.WKL]
to_list_length [in Undecidability.FOLC.WKL]
to_list_cast_of_list [in Undecidability.FOLC.WKL]
to_list_inj [in Undecidability.FOLC.WKL]
tprv_list_T [in Undecidability.FOLC.FullND]
tprv_list_T [in Undecidability.FOLC.ND]
trans_trans [in Undecidability.FOLC.BPCP_CND]
trans_subst [in Undecidability.FOLC.BPCP_CND]
U
ub_join [in Undecidability.FOLC.Heyting]union_closed [in Undecidability.FOLC.GenConstructions]
union_econsistent [in Undecidability.FOLC.GenConstructions]
union_sub [in Undecidability.FOLC.GenConstructions]
union_f [in Undecidability.FOLC.GenConstructions]
universal_interp_eval [in Undecidability.FOLC.KripkeCompleteness]
unused_after_subst [in Undecidability.FOLC.FOL]
unused_after_subst_term [in Undecidability.FOLC.FOL]
unused_enc [in Undecidability.FOLC.BPCP_FOL]
unused_prep [in Undecidability.FOLC.BPCP_FOL]
unused_big_imp [in Undecidability.FOLC.BPCP_FOL]
up_upI [in Undecidability.FOLC.SDialogues]
up_upL [in Undecidability.FOLC.SDialogues]
up_ren_ren [in Undecidability.FOLC.unscoped]
up_term_term_pref_raise [in Undecidability.FOLC.FOL]
up_term_term_pref_ext_c' [in Undecidability.FOLC.FOL]
up_term_term_vsubs [in Undecidability.FOLC.FOL]
up_term_form [in Undecidability.FOLC.FullND]
up_term_term [in Undecidability.FOLC.FullND]
V
valid_T_fragment [in Undecidability.FOLC.GenCompleteness]valid_standard_expld_stability [in Undecidability.FOLC.GenCompleteness]
valid_T_model_bot [in Undecidability.FOLC.GenCompleteness]
valid_T_subsumption [in Undecidability.FOLC.FullTarski]
valid_L_to_single [in Undecidability.FOLC.GenTarski]
valid_L_valid_T [in Undecidability.FOLC.GenTarski]
valid_T_standard_dm [in Undecidability.FOLC.GenTarski]
valid_T_subsumption [in Undecidability.FOLC.GenTarski]
vapp_vmap [in Undecidability.FOLC.SDialogues]
varL_term [in Undecidability.FOLC.Terms]
var_subst_L [in Undecidability.FOLC.FullFOL]
var_subst [in Undecidability.FOLC.FullFOL]
vecs_from_correct [in Undecidability.FOLC.FOL]
Vector_to_list_map [in Undecidability.FOLC.WKL]
vec_map_map [in Undecidability.FOLC.Extend]
vec_forall_map [in Undecidability.FOLC.FullFOL]
vec_map_ext [in Undecidability.FOLC.FullFOL]
vec_forall_cml [in Undecidability.FOLC.FOL]
vec_forall_map [in Undecidability.FOLC.FOL]
vec_map_ext [in Undecidability.FOLC.FOL]
vec_unused [in Undecidability.FOLC.Terms]
vec2env_correct [in Undecidability.FOLC.Extend]
vec2env_map [in Undecidability.FOLC.Extend]
venv_empty [in Undecidability.FOLC.GenTarski]
venv_sat [in Undecidability.FOLC.GenTarski]
vmap_upV [in Undecidability.FOLC.SDialogues]
vsubs_single_subst [in Undecidability.FOLC.ND]
vsubs_form_shift [in Undecidability.FOLC.ND]
W
Weak [in Undecidability.FOLC.FullND]Weak [in Undecidability.FOLC.ND]
weaken [in Undecidability.FOLC.FullSequent]
Weak_T [in Undecidability.FOLC.FullND]
Weak_T [in Undecidability.FOLC.ND]
well_founded_tlexp [in Undecidability.FOLC.WFexp]
well_founded_trans [in Undecidability.FOLC.WFexp]
well_founded_lexp [in Undecidability.FOLC.WFexp]
well_founded_perm [in Undecidability.FOLC.WFexp]
well_founded_singleton_full [in Undecidability.FOLC.WFexp]
wf_of_form [in Undecidability.FOLC.LEnum]
wf_of_term [in Undecidability.FOLC.LEnum]
WKL_implies_modex [in Undecidability.FOLC.WKL]
WKL_to_decidable_data [in Undecidability.FOLC.WKL]
WKL_to_decidable [in Undecidability.FOLC.WKL]
X
XM_DN [in Undecidability.FOLC.DeMorgan]Constructor Index
A
AAll [in Undecidability.FOLC.DialogFull]AAll [in Undecidability.FOLC.DialogFragment]
AAnd [in Undecidability.FOLC.DialogFull]
ABot [in Undecidability.FOLC.DialogFull]
ABot [in Undecidability.FOLC.DialogFragment]
Absurd [in Undecidability.FOLC.Gentzen]
AExt [in Undecidability.FOLC.DialogFull]
AImpl [in Undecidability.FOLC.DialogFull]
AImpl [in Undecidability.FOLC.DialogFragment]
AL [in Undecidability.FOLC.FullSequent]
All [in Undecidability.FOLC.FullSyntax]
All [in Undecidability.FOLC.Syntax]
AllE [in Undecidability.FOLC.FullND]
AllE [in Undecidability.FOLC.ND]
AllI [in Undecidability.FOLC.FullND]
AllI [in Undecidability.FOLC.ND]
AllL [in Undecidability.FOLC.Gentzen]
AllL [in Undecidability.FOLC.FullSequent]
AllR [in Undecidability.FOLC.Gentzen]
AllR [in Undecidability.FOLC.FullSequent]
All' [in Undecidability.FOLC.LEnum]
AOr [in Undecidability.FOLC.DialogFull]
App' [in Undecidability.FOLC.LEnum]
AR [in Undecidability.FOLC.FullSequent]
Att [in Undecidability.FOLC.SDialogues]
Att [in Undecidability.FOLC.Sorensen]
Ax [in Undecidability.FOLC.Gentzen]
Ax [in Undecidability.FOLC.FullSequent]
B
B_S [in Undecidability.FOLC.Terms]B_I [in Undecidability.FOLC.GenTarski]
C
C [in Undecidability.FOLC.SDialogues]C [in Undecidability.FOLC.Sorensen]
CE1 [in Undecidability.FOLC.FullND]
CE2 [in Undecidability.FOLC.FullND]
CI [in Undecidability.FOLC.FullND]
class [in Undecidability.FOLC.FullND]
class [in Undecidability.FOLC.ND]
Conj [in Undecidability.FOLC.FullSyntax]
Contr [in Undecidability.FOLC.Gentzen]
Contr [in Undecidability.FOLC.FullSequent]
Ctx [in Undecidability.FOLC.FullND]
Ctx [in Undecidability.FOLC.ND]
D
DAll [in Undecidability.FOLC.DialogFull]DAll [in Undecidability.FOLC.DialogFragment]
DAndL [in Undecidability.FOLC.DialogFull]
DAndR [in Undecidability.FOLC.DialogFull]
DE [in Undecidability.FOLC.FullND]
Def [in Undecidability.FOLC.SDialogues]
Def [in Undecidability.FOLC.Sorensen]
DExt [in Undecidability.FOLC.DialogFull]
DImpl [in Undecidability.FOLC.DialogFull]
DImpl [in Undecidability.FOLC.DialogFragment]
Disj [in Undecidability.FOLC.FullSyntax]
DI1 [in Undecidability.FOLC.FullND]
DI2 [in Undecidability.FOLC.FullND]
DlA [in Undecidability.FOLC.SDialogues]
DlC [in Undecidability.FOLC.SDialogues]
DlD [in Undecidability.FOLC.SDialogues]
DOAtk [in Undecidability.FOLC.Sorensen]
DODef [in Undecidability.FOLC.Sorensen]
DOrL [in Undecidability.FOLC.DialogFull]
DOrR [in Undecidability.FOLC.DialogFull]
DPAtk [in Undecidability.FOLC.Sorensen]
DPDef [in Undecidability.FOLC.Sorensen]
DWS [in Undecidability.FOLC.Sorensen]
E
EOAtk [in Undecidability.FOLC.Sorensen]EOCounter [in Undecidability.FOLC.Sorensen]
EODef [in Undecidability.FOLC.Sorensen]
EPAtk [in Undecidability.FOLC.Sorensen]
EPDef [in Undecidability.FOLC.Sorensen]
EWS [in Undecidability.FOLC.Sorensen]
Ex [in Undecidability.FOLC.FullSyntax]
ExE [in Undecidability.FOLC.FullND]
ExI [in Undecidability.FOLC.FullND]
ExL [in Undecidability.FOLC.FullSequent]
Exp [in Undecidability.FOLC.FullND]
Exp [in Undecidability.FOLC.FullSequent]
Exp [in Undecidability.FOLC.ND]
expl [in Undecidability.FOLC.FullND]
expl [in Undecidability.FOLC.ND]
ExR [in Undecidability.FOLC.FullSequent]
F
Fal [in Undecidability.FOLC.FullSyntax]Fal [in Undecidability.FOLC.Syntax]
Fal' [in Undecidability.FOLC.LEnum]
Forall_cons [in Undecidability.FOLC.Terms]
Forall_nil [in Undecidability.FOLC.Terms]
Func [in Undecidability.FOLC.Terms]
Func' [in Undecidability.FOLC.LEnum]
I
ids [in Undecidability.FOLC.unscoped]IE [in Undecidability.FOLC.FullND]
IE [in Undecidability.FOLC.ND]
ieAbsurd [in Undecidability.FOLC.LEnum]
ieAllL [in Undecidability.FOLC.LEnum]
ieAllR [in Undecidability.FOLC.LEnum]
ieAx [in Undecidability.FOLC.LEnum]
ieContr [in Undecidability.FOLC.LEnum]
ieIL [in Undecidability.FOLC.LEnum]
ieIR [in Undecidability.FOLC.LEnum]
II [in Undecidability.FOLC.FullND]
II [in Undecidability.FOLC.ND]
IL [in Undecidability.FOLC.Gentzen]
IL [in Undecidability.FOLC.FullSequent]
Impl [in Undecidability.FOLC.FullSyntax]
Impl [in Undecidability.FOLC.Syntax]
Impl' [in Undecidability.FOLC.LEnum]
intu [in Undecidability.FOLC.FullND]
intu [in Undecidability.FOLC.ND]
IR [in Undecidability.FOLC.Gentzen]
IR [in Undecidability.FOLC.FullSequent]
isvar [in Undecidability.FOLC.LEnum]
Is_Filter_false [in Undecidability.FOLC.WKL]
Is_Filter_true [in Undecidability.FOLC.WKL]
Is_Filter_nil [in Undecidability.FOLC.WKL]
L
lconst [in Undecidability.FOLC.FullND]lconst [in Undecidability.FOLC.ND]
N
novar [in Undecidability.FOLC.LEnum]O
OL [in Undecidability.FOLC.FullSequent]OP [in Undecidability.FOLC.SDialogues]
OP [in Undecidability.FOLC.Sorensen]
OR1 [in Undecidability.FOLC.FullSequent]
OR2 [in Undecidability.FOLC.FullSequent]
P
P [in Undecidability.FOLC.BPCP_FOL]Pc [in Undecidability.FOLC.FullND]
Pc [in Undecidability.FOLC.ND]
Perm [in Undecidability.FOLC.FullSequent]
Pred [in Undecidability.FOLC.FullSyntax]
Pred [in Undecidability.FOLC.Syntax]
Pred' [in Undecidability.FOLC.LEnum]
Q
Q [in Undecidability.FOLC.BPCP_FOL]R
ren1 [in Undecidability.FOLC.unscoped]ren2 [in Undecidability.FOLC.unscoped]
ren3 [in Undecidability.FOLC.unscoped]
ren4 [in Undecidability.FOLC.unscoped]
ren5 [in Undecidability.FOLC.unscoped]
S
SAll [in Undecidability.FOLC.FullFOL]SAll [in Undecidability.FOLC.FOL]
SConjL [in Undecidability.FOLC.FullFOL]
SConjR [in Undecidability.FOLC.FullFOL]
SDisjL [in Undecidability.FOLC.FullFOL]
SDisjR [in Undecidability.FOLC.FullFOL]
SEx [in Undecidability.FOLC.FullFOL]
SImplL [in Undecidability.FOLC.FullFOL]
SImplL [in Undecidability.FOLC.FOL]
SImplR [in Undecidability.FOLC.FullFOL]
SImplR [in Undecidability.FOLC.FOL]
SOAtk [in Undecidability.FOLC.SDialogues]
SOAtk [in Undecidability.FOLC.Sorensen]
SODef [in Undecidability.FOLC.SDialogues]
SODef [in Undecidability.FOLC.Sorensen]
SPAtk [in Undecidability.FOLC.SDialogues]
SPAtk [in Undecidability.FOLC.Sorensen]
SPDef [in Undecidability.FOLC.SDialogues]
SPDef [in Undecidability.FOLC.Sorensen]
stA [in Undecidability.FOLC.FOL]
stB [in Undecidability.FOLC.FOL]
stF [in Undecidability.FOLC.FOL]
stIL [in Undecidability.FOLC.FOL]
stIR [in Undecidability.FOLC.FOL]
stP [in Undecidability.FOLC.FOL]
subst1 [in Undecidability.FOLC.unscoped]
subst2 [in Undecidability.FOLC.unscoped]
subst3 [in Undecidability.FOLC.unscoped]
subst4 [in Undecidability.FOLC.unscoped]
subst5 [in Undecidability.FOLC.unscoped]
SWS [in Undecidability.FOLC.SDialogues]
SWS [in Undecidability.FOLC.Sorensen]
T
TAbsurd [in Undecidability.FOLC.Gentzen]TAllE [in Undecidability.FOLC.Gentzen]
TAllI [in Undecidability.FOLC.Gentzen]
TAllL [in Undecidability.FOLC.Gentzen]
TAllR [in Undecidability.FOLC.Gentzen]
TAx [in Undecidability.FOLC.Gentzen]
TContr [in Undecidability.FOLC.Gentzen]
TCtx [in Undecidability.FOLC.Gentzen]
TExp [in Undecidability.FOLC.Gentzen]
TIE [in Undecidability.FOLC.Gentzen]
TII [in Undecidability.FOLC.Gentzen]
TIL [in Undecidability.FOLC.Gentzen]
TIR [in Undecidability.FOLC.Gentzen]
tone [in Undecidability.FOLC.WFexp]
ttwo [in Undecidability.FOLC.WFexp]
t_e' [in Undecidability.FOLC.BPCP_FOL]
t_f' [in Undecidability.FOLC.BPCP_FOL]
U
uft_Func [in Undecidability.FOLC.Terms]uft_var [in Undecidability.FOLC.Terms]
uf_Ex [in Undecidability.FOLC.FullFOL]
uf_All [in Undecidability.FOLC.FullFOL]
uf_O [in Undecidability.FOLC.FullFOL]
uf_A [in Undecidability.FOLC.FullFOL]
uf_I [in Undecidability.FOLC.FullFOL]
uf_Pred [in Undecidability.FOLC.FullFOL]
uf_Fal [in Undecidability.FOLC.FullFOL]
uf_All [in Undecidability.FOLC.FOL]
uf_Impl [in Undecidability.FOLC.FOL]
uf_Pred [in Undecidability.FOLC.FOL]
uf_Fal [in Undecidability.FOLC.FOL]
up_term [in Undecidability.FOLC.FullSyntax]
up_term [in Undecidability.FOLC.Syntax]
V
var_term' [in Undecidability.FOLC.LEnum]var_term [in Undecidability.FOLC.Terms]
vec_inS [in Undecidability.FOLC.Terms]
vec_inB [in Undecidability.FOLC.Terms]
W
Weak [in Undecidability.FOLC.FullSequent]wf_app [in Undecidability.FOLC.LEnum]
wf_fun [in Undecidability.FOLC.LEnum]
wf_var [in Undecidability.FOLC.LEnum]
Axiom Index
P
pext [in Undecidability.FOLC.axioms]T
todo [in Undecidability.FOLC.Lindenbaum]Projection Index
A
ar_inj_Preds [in Undecidability.FOLC.Extend]ar_inj_Funcs [in Undecidability.FOLC.Extend]
atomic [in Undecidability.FOLC.SDialogues]
atomic [in Undecidability.FOLC.Sorensen]
attack [in Undecidability.FOLC.SDialogues]
attack [in Undecidability.FOLC.Sorensen]
B
Bot [in Undecidability.FOLC.Heyting]Bot1 [in Undecidability.FOLC.Heyting]
D
dec_f [in Undecidability.FOLC.SDialogues]dec_f [in Undecidability.FOLC.Sorensen]
defense [in Undecidability.FOLC.SDialogues]
defense [in Undecidability.FOLC.Sorensen]
E
enum [in Undecidability.FOLC.GenConstructions]enum_unused [in Undecidability.FOLC.GenConstructions]
enum_enum [in Undecidability.FOLC.GenConstructions]
F
Funcs [in Undecidability.FOLC.Terms]fun_ar [in Undecidability.FOLC.Terms]
F_sup [in Undecidability.FOLC.Heyting]
F_inf [in Undecidability.FOLC.Heyting]
F_impl [in Undecidability.FOLC.Heyting]
F_join [in Undecidability.FOLC.Heyting]
F_meet [in Undecidability.FOLC.Heyting]
F_bot [in Undecidability.FOLC.Heyting]
F_mono [in Undecidability.FOLC.Heyting]
F_inj [in Undecidability.FOLC.Heyting]
H
H [in Undecidability.FOLC.Heyting]HA [in Undecidability.FOLC.Heyting]
I
ids [in Undecidability.FOLC.unscoped]Impl [in Undecidability.FOLC.Heyting]
Impl1 [in Undecidability.FOLC.Heyting]
Inf [in Undecidability.FOLC.Heyting]
Inf1 [in Undecidability.FOLC.Heyting]
In_T_closed [in Undecidability.FOLC.GenConstructions]
In_T [in Undecidability.FOLC.GenConstructions]
is_inj_Preds [in Undecidability.FOLC.Extend]
is_inj_Funcs [in Undecidability.FOLC.Extend]
I_Preds [in Undecidability.FOLC.Extend]
I_Funcs [in Undecidability.FOLC.Extend]
i_F [in Undecidability.FOLC.GenTarski]
i_P [in Undecidability.FOLC.GenTarski]
i_f [in Undecidability.FOLC.GenTarski]
J
Join [in Undecidability.FOLC.Heyting]Join1 [in Undecidability.FOLC.Heyting]
K
k_Bot [in Undecidability.FOLC.Kripke]k_P [in Undecidability.FOLC.Kripke]
k_interp [in Undecidability.FOLC.Kripke]
M
Meet [in Undecidability.FOLC.Heyting]Meet1 [in Undecidability.FOLC.Heyting]
mon_Bot [in Undecidability.FOLC.Kripke]
mon_P [in Undecidability.FOLC.Kripke]
N
NBot [in Undecidability.FOLC.GenConstructions]NBot_closed [in Undecidability.FOLC.GenConstructions]
nodes [in Undecidability.FOLC.Kripke]
O
Out_T_impl [in Undecidability.FOLC.GenConstructions]Out_T_all [in Undecidability.FOLC.GenConstructions]
Out_T_prv [in Undecidability.FOLC.GenConstructions]
Out_T_sub [in Undecidability.FOLC.GenConstructions]
Out_T_econsistent [in Undecidability.FOLC.GenConstructions]
Out_T [in Undecidability.FOLC.GenConstructions]
P
Preds [in Undecidability.FOLC.Terms]pred_ar [in Undecidability.FOLC.Terms]
R
R [in Undecidability.FOLC.Heyting]reachable [in Undecidability.FOLC.Kripke]
reach_tran [in Undecidability.FOLC.Kripke]
reach_refl [in Undecidability.FOLC.Kripke]
ren1 [in Undecidability.FOLC.unscoped]
ren2 [in Undecidability.FOLC.unscoped]
ren3 [in Undecidability.FOLC.unscoped]
ren4 [in Undecidability.FOLC.unscoped]
ren5 [in Undecidability.FOLC.unscoped]
Rref [in Undecidability.FOLC.Heyting]
Rtra [in Undecidability.FOLC.Heyting]
R_Preds [in Undecidability.FOLC.Extend]
R_Funcs [in Undecidability.FOLC.Extend]
S
subst1 [in Undecidability.FOLC.unscoped]subst2 [in Undecidability.FOLC.unscoped]
subst3 [in Undecidability.FOLC.unscoped]
subst4 [in Undecidability.FOLC.unscoped]
subst5 [in Undecidability.FOLC.unscoped]
T
tree_is_tree [in Undecidability.FOLC.WKL]tree_T [in Undecidability.FOLC.WKL]
tree_p [in Undecidability.FOLC.WKL]
tree_inhab [in Undecidability.FOLC.WKL]
U
up_term [in Undecidability.FOLC.FullSyntax]up_term [in Undecidability.FOLC.Syntax]
V
variant [in Undecidability.FOLC.GenConstructions]Inductive Index
A
attack_form [in Undecidability.FOLC.DialogFull]attack_form [in Undecidability.FOLC.DialogFragment]
B
bottom [in Undecidability.FOLC.FullND]bottom [in Undecidability.FOLC.ND]
C
challenge [in Undecidability.FOLC.SDialogues]challenge [in Undecidability.FOLC.Sorensen]
D
defense_form [in Undecidability.FOLC.DialogFull]defense_form [in Undecidability.FOLC.DialogFragment]
Dlift [in Undecidability.FOLC.SDialogues]
domove [in Undecidability.FOLC.Sorensen]
dpmove [in Undecidability.FOLC.Sorensen]
Dprv [in Undecidability.FOLC.SDialogues]
Dprv [in Undecidability.FOLC.Sorensen]
dwin_strat [in Undecidability.FOLC.Sorensen]
E
eomove [in Undecidability.FOLC.Sorensen]epmove [in Undecidability.FOLC.Sorensen]
ewin_strat [in Undecidability.FOLC.Sorensen]
F
Forall [in Undecidability.FOLC.Terms]form [in Undecidability.FOLC.FullSyntax]
form [in Undecidability.FOLC.Syntax]
form' [in Undecidability.FOLC.LEnum]
fprv [in Undecidability.FOLC.FullSequent]
I
Is_Filter [in Undecidability.FOLC.WKL]M
min_sig_funcs [in Undecidability.FOLC.BPCP_FOL]min_sig_preds [in Undecidability.FOLC.BPCP_FOL]
O
opening [in Undecidability.FOLC.SDialogues]opening [in Undecidability.FOLC.Sorensen]
P
peirce [in Undecidability.FOLC.FullND]peirce [in Undecidability.FOLC.ND]
prv [in Undecidability.FOLC.FullND]
prv [in Undecidability.FOLC.ND]
R
Ren1 [in Undecidability.FOLC.unscoped]Ren2 [in Undecidability.FOLC.unscoped]
Ren3 [in Undecidability.FOLC.unscoped]
Ren4 [in Undecidability.FOLC.unscoped]
Ren5 [in Undecidability.FOLC.unscoped]
S
sf [in Undecidability.FOLC.FullFOL]sf [in Undecidability.FOLC.FOL]
somove [in Undecidability.FOLC.SDialogues]
somove [in Undecidability.FOLC.Sorensen]
spmove [in Undecidability.FOLC.SDialogues]
spmove [in Undecidability.FOLC.Sorensen]
sprv [in Undecidability.FOLC.Gentzen]
sprvie [in Undecidability.FOLC.LEnum]
Subst1 [in Undecidability.FOLC.unscoped]
Subst2 [in Undecidability.FOLC.unscoped]
Subst3 [in Undecidability.FOLC.unscoped]
Subst4 [in Undecidability.FOLC.unscoped]
Subst5 [in Undecidability.FOLC.unscoped]
subterm [in Undecidability.FOLC.FOL]
subterm_form [in Undecidability.FOLC.FOL]
swin_strat [in Undecidability.FOLC.SDialogues]
swin_strat [in Undecidability.FOLC.Sorensen]
T
term [in Undecidability.FOLC.Terms]term' [in Undecidability.FOLC.LEnum]
tprv [in Undecidability.FOLC.Gentzen]
trans [in Undecidability.FOLC.WFexp]
tsprv [in Undecidability.FOLC.Gentzen]
U
unused [in Undecidability.FOLC.FullFOL]unused [in Undecidability.FOLC.FOL]
unused_term [in Undecidability.FOLC.Terms]
Up_term [in Undecidability.FOLC.FullSyntax]
Up_term [in Undecidability.FOLC.Syntax]
V
Var [in Undecidability.FOLC.unscoped]varornot [in Undecidability.FOLC.LEnum]
vec_in [in Undecidability.FOLC.Terms]
W
wf [in Undecidability.FOLC.LEnum]Section Index
B
BPCP_CND [in Undecidability.FOLC.BPCP_CND]C
CHAProperty [in Undecidability.FOLC.Heyting]ClosingBigImp [in Undecidability.FOLC.GenTarski]
ClosingValidity [in Undecidability.FOLC.GenTarski]
Completeness [in Undecidability.FOLC.GenCompleteness]
Completeness.BotModel [in Undecidability.FOLC.GenCompleteness]
Completeness.ExplodingCompletenes [in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentCompleteness [in Undecidability.FOLC.GenCompleteness]
Completeness.FragmentModel [in Undecidability.FOLC.GenCompleteness]
Completeness.MPStrongCompleteness [in Undecidability.FOLC.GenCompleteness]
Completeness.StandardCompletenes [in Undecidability.FOLC.GenCompleteness]
Composition [in Undecidability.FOLC.GenConstructions]
Consistency [in Undecidability.FOLC.Consistency]
Consistency.Classical [in Undecidability.FOLC.Consistency]
D
DGame [in Undecidability.FOLC.Sorensen]DialogFragment [in Undecidability.FOLC.DialogFragment]
DialogFull [in Undecidability.FOLC.DialogFull]
DM [in Undecidability.FOLC.DeMorgan]
DNT [in Undecidability.FOLC.FullND]
DNT [in Undecidability.FOLC.ND]
E
EGame [in Undecidability.FOLC.Sorensen]Enumerability [in Undecidability.FOLC.FOL]
Enumerability [in Undecidability.FOLC.ND]
Enumeration [in Undecidability.FOLC.Enumeration]
enum_inj [in Undecidability.FOLC.Markov]
EqDec [in Undecidability.FOLC.FullFOL]
EqDec [in Undecidability.FOLC.FOL]
F
FiniteCompleteness [in Undecidability.FOLC.GenCompleteness]fix_sig [in Undecidability.FOLC.FullSyntax]
fix_sig [in Undecidability.FOLC.Syntax]
fix_sig [in Undecidability.FOLC.Terms]
FOL [in Undecidability.FOLC.FOL]
FOL.ContainsAutomation [in Undecidability.FOLC.FOL]
FullFOL [in Undecidability.FOLC.FullFOL]
FullFOL.ContainsAutomation [in Undecidability.FOLC.FullFOL]
FullSequent [in Undecidability.FOLC.FullSequent]
G
GenCons [in Undecidability.FOLC.GenConstructions]GenCons.Explosion [in Undecidability.FOLC.GenConstructions]
GenCons.Henkin [in Undecidability.FOLC.GenConstructions]
GenCons.Omega [in Undecidability.FOLC.GenConstructions]
GenCons.Union [in Undecidability.FOLC.GenConstructions]
Gentzen [in Undecidability.FOLC.Gentzen]
Gentzen.CutElimination [in Undecidability.FOLC.Gentzen]
Gentzen.Enumerability [in Undecidability.FOLC.Gentzen]
Gentzen.Soundness [in Undecidability.FOLC.Gentzen]
Gentzen.Weakening [in Undecidability.FOLC.Gentzen]
H
HAProperty [in Undecidability.FOLC.Heyting]I
inj_enum [in Undecidability.FOLC.Markov]K
Kripke [in Undecidability.FOLC.Extend]Kripke [in Undecidability.FOLC.Kripke]
KripkeCompleteness [in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.BottomlessCompleteness [in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.Contexts [in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.ExplodingCompleteness [in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.MPRequired [in Undecidability.FOLC.KripkeCompleteness]
KripkeCompleteness.StandardCompleteness [in Undecidability.FOLC.KripkeCompleteness]
Kripke.Model [in Undecidability.FOLC.Kripke]
Kripke.Substs [in Undecidability.FOLC.Kripke]
KSoundness [in Undecidability.FOLC.Kripke]
L
Lindenbaum [in Undecidability.FOLC.Lindenbaum]Lindenbaum.BSoundness [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.CHAEval [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Completeness [in Undecidability.FOLC.Lindenbaum]
Lindenbaum.Soundness [in Undecidability.FOLC.Lindenbaum]
LJD [in Undecidability.FOLC.Sorensen]
L_T_Enumeration [in Undecidability.FOLC.Enumeration]
L_T_unused [in Undecidability.FOLC.Enumeration]
M
MacNeille [in Undecidability.FOLC.Heyting]N
ND_def.Weakening [in Undecidability.FOLC.FullND]ND_def [in Undecidability.FOLC.FullND]
ND_def.Weakening [in Undecidability.FOLC.ND]
ND_def [in Undecidability.FOLC.ND]
P
PropT [in Undecidability.FOLC.Stability]R
RefutationComp [in Undecidability.FOLC.FullND]RefutationComp [in Undecidability.FOLC.ND]
S
SDialogues [in Undecidability.FOLC.SDialogues]SDialogues.Up [in Undecidability.FOLC.SDialogues]
SGame [in Undecidability.FOLC.Sorensen]
SigExt [in Undecidability.FOLC.FOL]
SigExt [in Undecidability.FOLC.GenTarski]
SigExt [in Undecidability.FOLC.ND]
StabilityClasses [in Undecidability.FOLC.Stability]
StabilityClasses.DN [in Undecidability.FOLC.Stability]
StabilityClasses.ObjMP [in Undecidability.FOLC.Stability]
StabilityClasses.ObjMP.ConT [in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP [in Undecidability.FOLC.Stability]
StabilityClasses.SyntMP.MPEnum [in Undecidability.FOLC.Stability]
StrongCompleteness [in Undecidability.FOLC.GenCompleteness]
Subterm [in Undecidability.FOLC.FOL]
T
Tarski [in Undecidability.FOLC.Extend]Tarski [in Undecidability.FOLC.FullTarski]
Tarski [in Undecidability.FOLC.GenTarski]
Tarski.Semantics [in Undecidability.FOLC.FullTarski]
Tarski.Semantics [in Undecidability.FOLC.GenTarski]
Tarski.Soundness [in Undecidability.FOLC.GenTarski]
Tarski.Substs [in Undecidability.FOLC.FullTarski]
Tarski.Substs [in Undecidability.FOLC.GenTarski]
TheoryManipulation [in Undecidability.FOLC.FullND]
TheoryManipulation [in Undecidability.FOLC.ND]
Transitivity [in Undecidability.FOLC.WFexp]
TransWFexp [in Undecidability.FOLC.WFexp]
V
validity [in Undecidability.FOLC.BPCP_FOL]W
WFexp [in Undecidability.FOLC.WFexp]WFlist [in Undecidability.FOLC.WFexp]
WKL [in Undecidability.FOLC.WKL]
Instance Index
C
clb_calg [in Undecidability.FOLC.Lindenbaum]clb_alg [in Undecidability.FOLC.Lindenbaum]
computable_L_sprvie [in Undecidability.FOLC.LEnum]
computable_f9 [in Undecidability.FOLC.LEnum]
computable_f8 [in Undecidability.FOLC.LEnum]
computable_ineqb [in Undecidability.FOLC.LEnum]
computable_enum_eqb [in Undecidability.FOLC.LEnum]
computable_option_form_eqb [in Undecidability.FOLC.LEnum]
computable_list_form_eqb [in Undecidability.FOLC.LEnum]
computable_form_eqb [in Undecidability.FOLC.LEnum]
computable_list_eqb [in Undecidability.FOLC.LEnum]
computable_term_eqb [in Undecidability.FOLC.LEnum]
D
dec_form [in Undecidability.FOLC.FullFOL]dec_term [in Undecidability.FOLC.FullFOL]
dec_vec [in Undecidability.FOLC.FullFOL]
dec_sig_ext_Preds [in Undecidability.FOLC.FOL]
dec_sig_ext_Funcs [in Undecidability.FOLC.FOL]
dec_form [in Undecidability.FOLC.FOL]
dec_term [in Undecidability.FOLC.FOL]
dec_vec [in Undecidability.FOLC.FOL]
E
enumT_sum [in Undecidability.FOLC.GenCompleteness]enumT_term [in Undecidability.FOLC.Markov]
enumT_sig_ext_Preds [in Undecidability.FOLC.FOL]
enumT_sig_ext_Funcs [in Undecidability.FOLC.FOL]
enumT_form [in Undecidability.FOLC.FOL]
enumT_term [in Undecidability.FOLC.FOL]
enumT_vec [in Undecidability.FOLC.FOL]
enumT_unit [in Undecidability.FOLC.WKL]
enum_form' [in Undecidability.FOLC.LEnum]
enum_term' [in Undecidability.FOLC.LEnum]
equiv_HA_refl [in Undecidability.FOLC.Heyting]
eq_dec_term [in Undecidability.FOLC.Markov]
F
False_enumT [in Undecidability.FOLC.Stability]form_rules [in Undecidability.FOLC.DialogFull]
form_rules [in Undecidability.FOLC.DialogFragment]
G
glb_calg [in Undecidability.FOLC.Lindenbaum]glb_alg [in Undecidability.FOLC.Lindenbaum]
H
HdF [in Undecidability.FOLC.LEnum]HdP [in Undecidability.FOLC.LEnum]
HeF [in Undecidability.FOLC.LEnum]
help [in Undecidability.FOLC.Markov]
HeP [in Undecidability.FOLC.LEnum]
hset_impl_proper [in Undecidability.FOLC.Heyting]
hset_join_proper [in Undecidability.FOLC.Heyting]
hset_meet_proper [in Undecidability.FOLC.Heyting]
hset_sub_proper [in Undecidability.FOLC.Heyting]
hset_elem_proper [in Undecidability.FOLC.Heyting]
hset_equiv_equiv [in Undecidability.FOLC.Heyting]
I
IB [in Undecidability.FOLC.BPCP_FOL]idsRen [in Undecidability.FOLC.unscoped]
K
kmodel_reach_trans [in Undecidability.FOLC.Kripke]kmodel_reach_refl [in Undecidability.FOLC.Kripke]
K_std [in Undecidability.FOLC.KripkeCompleteness]
K_ctx [in Undecidability.FOLC.KripkeCompleteness]
L
lb_calg [in Undecidability.FOLC.Lindenbaum]lb_alg [in Undecidability.FOLC.Lindenbaum]
lb_proper [in Undecidability.FOLC.Heyting]
M
max [in Undecidability.FOLC.LEnum]min_sig [in Undecidability.FOLC.BPCP_FOL]
min_sig_funcs_dec [in Undecidability.FOLC.BPCP_FOL]
min_sig_preds_dec [in Undecidability.FOLC.BPCP_FOL]
model_fragment [in Undecidability.FOLC.GenCompleteness]
model_bot [in Undecidability.FOLC.GenCompleteness]
N
normal_proper [in Undecidability.FOLC.Heyting]P
preorder_HA [in Undecidability.FOLC.Heyting]proper_HA_Inf_indexed [in Undecidability.FOLC.Heyting]
proper_HA_Sup_indexed [in Undecidability.FOLC.Heyting]
proper_HA_Sup [in Undecidability.FOLC.Heyting]
proper_HA_Inf [in Undecidability.FOLC.Heyting]
proper_HA_Impl [in Undecidability.FOLC.Heyting]
proper_HA_Join [in Undecidability.FOLC.Heyting]
proper_HA_Meet [in Undecidability.FOLC.Heyting]
R
RI [in Undecidability.FOLC.Extend]RM [in Undecidability.FOLC.Extend]
S
subrelation_HA_flip [in Undecidability.FOLC.Heyting]subrelation_HA [in Undecidability.FOLC.Heyting]
subset_T_trans [in Undecidability.FOLC.FullFOL]
subset_T_trans [in Undecidability.FOLC.FOL]
Subst_form [in Undecidability.FOLC.FullSyntax]
Subst_term [in Undecidability.FOLC.FullSyntax]
Subst_form [in Undecidability.FOLC.Syntax]
Subst_term [in Undecidability.FOLC.Syntax]
T
term_T_form' [in Undecidability.FOLC.LEnum]term_cons''' [in Undecidability.FOLC.LEnum]
term_L_seq [in Undecidability.FOLC.LEnum]
term_form_shift' [in Undecidability.FOLC.LEnum]
term_f5 [in Undecidability.FOLC.LEnum]
term_subst_form' [in Undecidability.FOLC.LEnum]
term_up_term_term' [in Undecidability.FOLC.LEnum]
term_f7 [in Undecidability.FOLC.LEnum]
term_f6 [in Undecidability.FOLC.LEnum]
term_subst_term' [in Undecidability.FOLC.LEnum]
term_scons [in Undecidability.FOLC.LEnum]
term_f4 [in Undecidability.FOLC.LEnum]
term_f3 [in Undecidability.FOLC.LEnum]
term_existsb [in Undecidability.FOLC.LEnum]
term_f2 [in Undecidability.FOLC.LEnum]
term_f1 [in Undecidability.FOLC.LEnum]
term_L_form' [in Undecidability.FOLC.LEnum]
term_T_list' [in Undecidability.FOLC.LEnum]
term_cons'' [in Undecidability.FOLC.LEnum]
term_Pred'' [in Undecidability.FOLC.LEnum]
term_Impl'' [in Undecidability.FOLC.LEnum]
term_All' [in Undecidability.FOLC.LEnum]
term_Impl' [in Undecidability.FOLC.LEnum]
term_Pred' [in Undecidability.FOLC.LEnum]
term_L_wf [in Undecidability.FOLC.LEnum]
term_L_term' [in Undecidability.FOLC.LEnum]
term_App'' [in Undecidability.FOLC.LEnum]
term_App' [in Undecidability.FOLC.LEnum]
term_Func' [in Undecidability.FOLC.LEnum]
term_var_term' [in Undecidability.FOLC.LEnum]
trans_Transitive [in Undecidability.FOLC.WFexp]
U
ub_proper [in Undecidability.FOLC.Heyting]universal_interp [in Undecidability.FOLC.KripkeCompleteness]
Up_term_term [in Undecidability.FOLC.FullSyntax]
Up_term_term [in Undecidability.FOLC.Syntax]
V
VarInstance_term [in Undecidability.FOLC.FullSyntax]VarInstance_term [in Undecidability.FOLC.Syntax]
Abbreviation Index
F
fin [in Undecidability.FOLC.unscoped]I
is_sup [in Undecidability.FOLC.Heyting]is_inf [in Undecidability.FOLC.Heyting]
M
make_subst [in Undecidability.FOLC.Extend]max_list [in Undecidability.FOLC.WKL]
N
nat [in Undecidability.FOLC.WKL]O
omniscient_on [in Undecidability.FOLC.WKL]Q
QQ [in Undecidability.FOLC.BPCP_CND]U
u [in Undecidability.FOLC.BPCP_FOL]V
v [in Undecidability.FOLC.BPCP_FOL]vector [in Undecidability.FOLC.Terms]
Record Index
C
CompleteHeytingAlgebra [in Undecidability.FOLC.Heyting]ConstructionInputs [in Undecidability.FOLC.GenConstructions]
ConstructionOutputs [in Undecidability.FOLC.GenConstructions]
H
HeytingAlgebra [in Undecidability.FOLC.Heyting]HeytingMorphism [in Undecidability.FOLC.Heyting]
I
interp [in Undecidability.FOLC.GenTarski]is_tree [in Undecidability.FOLC.WKL]
K
kmodel [in Undecidability.FOLC.Kripke]R
Ren1 [in Undecidability.FOLC.unscoped]Ren2 [in Undecidability.FOLC.unscoped]
Ren3 [in Undecidability.FOLC.unscoped]
Ren4 [in Undecidability.FOLC.unscoped]
Ren5 [in Undecidability.FOLC.unscoped]
rule_set [in Undecidability.FOLC.SDialogues]
rule_set [in Undecidability.FOLC.Sorensen]
S
Signature [in Undecidability.FOLC.Terms]Signature_inj [in Undecidability.FOLC.Extend]
Subst1 [in Undecidability.FOLC.unscoped]
Subst2 [in Undecidability.FOLC.unscoped]
Subst3 [in Undecidability.FOLC.unscoped]
Subst4 [in Undecidability.FOLC.unscoped]
Subst5 [in Undecidability.FOLC.unscoped]
T
tree [in Undecidability.FOLC.WKL]U
Up_term [in Undecidability.FOLC.FullSyntax]Up_term [in Undecidability.FOLC.Syntax]
V
Var [in Undecidability.FOLC.unscoped]Definition Index
A
And [in Undecidability.FOLC.WKL]any_T [in Undecidability.FOLC.Stability]
ap [in Undecidability.FOLC.unscoped]
apc [in Undecidability.FOLC.unscoped]
App'' [in Undecidability.FOLC.LEnum]
atomic_form [in Undecidability.FOLC.DialogFull]
atomic_form [in Undecidability.FOLC.DialogFragment]
at_pos [in Undecidability.FOLC.Enumeration]
B
big_imp [in Undecidability.FOLC.FullFOL]big_imp [in Undecidability.FOLC.FOL]
big_or [in Undecidability.FOLC.FullSequent]
BLM [in Undecidability.FOLC.GenTarski]
boolean [in Undecidability.FOLC.Lindenbaum]
bounded_tree [in Undecidability.FOLC.WKL]
bvalid [in Undecidability.FOLC.Lindenbaum]
C
capture [in Undecidability.FOLC.FullFOL]capture [in Undecidability.FOLC.FOL]
capture_subs [in Undecidability.FOLC.FullND]
capture_subs [in Undecidability.FOLC.ND]
classical [in Undecidability.FOLC.FullTarski]
classical [in Undecidability.FOLC.GenTarski]
clb_Pr [in Undecidability.FOLC.Lindenbaum]
close [in Undecidability.FOLC.FullFOL]
close [in Undecidability.FOLC.FOL]
closed [in Undecidability.FOLC.FullFOL]
closed [in Undecidability.FOLC.FOL]
closed_T [in Undecidability.FOLC.FullFOL]
closed_T [in Undecidability.FOLC.FOL]
cod [in Undecidability.FOLC.axioms]
cod_comp [in Undecidability.FOLC.axioms]
cod_ext' [in Undecidability.FOLC.axioms]
cod_ext [in Undecidability.FOLC.axioms]
cod_id [in Undecidability.FOLC.axioms]
cod_map [in Undecidability.FOLC.axioms]
compactness [in Undecidability.FOLC.WKL]
completeness [in Undecidability.FOLC.WKL]
completion_calgebra [in Undecidability.FOLC.Heyting]
completion_algebra [in Undecidability.FOLC.Heyting]
compSubstSubst_form [in Undecidability.FOLC.FullSyntax]
compSubstSubst_form [in Undecidability.FOLC.Syntax]
compSubstSubst_term [in Undecidability.FOLC.Terms]
congr_Ex [in Undecidability.FOLC.FullSyntax]
congr_All [in Undecidability.FOLC.FullSyntax]
congr_Disj [in Undecidability.FOLC.FullSyntax]
congr_Conj [in Undecidability.FOLC.FullSyntax]
congr_Impl [in Undecidability.FOLC.FullSyntax]
congr_Pred [in Undecidability.FOLC.FullSyntax]
congr_Fal [in Undecidability.FOLC.FullSyntax]
congr_All [in Undecidability.FOLC.Syntax]
congr_Impl [in Undecidability.FOLC.Syntax]
congr_Pred [in Undecidability.FOLC.Syntax]
congr_Fal [in Undecidability.FOLC.Syntax]
congr_Func [in Undecidability.FOLC.Terms]
cons [in Undecidability.FOLC.KripkeCompleteness]
consistent [in Undecidability.FOLC.Consistency]
consistent_max [in Undecidability.FOLC.Consistency]
constraint [in Undecidability.FOLC.FullTarski]
constraint [in Undecidability.FOLC.GenTarski]
cons_ctx [in Undecidability.FOLC.KripkeCompleteness]
cons'' [in Undecidability.FOLC.LEnum]
cons''' [in Undecidability.FOLC.LEnum]
contains [in Undecidability.FOLC.FullFOL]
contains [in Undecidability.FOLC.FOL]
contains_L [in Undecidability.FOLC.FullFOL]
contains_L [in Undecidability.FOLC.FOL]
convert [in Undecidability.FOLC.DeMorgan]
con_subs [in Undecidability.FOLC.FullTarski]
con_T [in Undecidability.FOLC.Stability]
con_subs [in Undecidability.FOLC.GenTarski]
countable [in Undecidability.FOLC.WKL]
count_conjs [in Undecidability.FOLC.WKL]
count_sig [in Undecidability.FOLC.WKL]
cprv [in Undecidability.FOLC.Markov]
ctx_incl [in Undecidability.FOLC.KripkeCompleteness]
ctx_S [in Undecidability.FOLC.BPCP_FOL]
cycle_shift [in Undecidability.FOLC.FullND]
cycle_shift [in Undecidability.FOLC.FullSequent]
cycle_shift [in Undecidability.FOLC.ND]
D
Dadmission [in Undecidability.FOLC.SDialogues]Dadmission' [in Undecidability.FOLC.SDialogues]
Dchallenge [in Undecidability.FOLC.SDialogues]
Dchallenge' [in Undecidability.FOLC.SDialogues]
dclosed [in Undecidability.FOLC.Heyting]
Ddeferred [in Undecidability.FOLC.SDialogues]
Ddeferred' [in Undecidability.FOLC.SDialogues]
decidable [in Undecidability.FOLC.WKL]
decidable_model [in Undecidability.FOLC.WKL]
deferred [in Undecidability.FOLC.SDialogues]
deferred [in Undecidability.FOLC.Sorensen]
discrete_sig [in Undecidability.FOLC.Markov]
DlA' [in Undecidability.FOLC.SDialogues]
DlA'' [in Undecidability.FOLC.SDialogues]
DlC' [in Undecidability.FOLC.SDialogues]
DlD' [in Undecidability.FOLC.SDialogues]
DlD'' [in Undecidability.FOLC.SDialogues]
Dlift_le [in Undecidability.FOLC.SDialogues]
Dlift_le' [in Undecidability.FOLC.SDialogues]
DM [in Undecidability.FOLC.DeMorgan]
DM [in Undecidability.FOLC.WKL]
DMT [in Undecidability.FOLC.DeMorgan]
DMTT [in Undecidability.FOLC.DeMorgan]
DN [in Undecidability.FOLC.DeMorgan]
DN [in Undecidability.FOLC.Stability]
dnQ [in Undecidability.FOLC.BPCP_CND]
dnt [in Undecidability.FOLC.FullND]
dnt [in Undecidability.FOLC.ND]
down [in Undecidability.FOLC.Heyting]
DPexp1 [in Undecidability.FOLC.GenConstructions]
DPexp2 [in Undecidability.FOLC.GenConstructions]
DPexp3 [in Undecidability.FOLC.GenConstructions]
droppable [in Undecidability.FOLC.GenTarski]
drop_interp [in Undecidability.FOLC.GenTarski]
drop_interp' [in Undecidability.FOLC.GenTarski]
dstate [in Undecidability.FOLC.Sorensen]
dummy_sig [in Undecidability.FOLC.Stability]
dummy_interp [in Undecidability.FOLC.GenTarski]
dvalid [in Undecidability.FOLC.Sorensen]
dwin_Dprv_embed [in Undecidability.FOLC.Sorensen]
E
econsistent [in Undecidability.FOLC.GenConstructions]econsistent_join [in Undecidability.FOLC.GenConstructions]
EM [in Undecidability.FOLC.GenTarski]
embed [in Undecidability.FOLC.Extend]
embed [in Undecidability.FOLC.DeMorgan]
embed [in Undecidability.FOLC.Gentzen]
embed [in Undecidability.FOLC.Heyting]
embed_term [in Undecidability.FOLC.Extend]
enc [in Undecidability.FOLC.BPCP_FOL]
enumerable_sig [in Undecidability.FOLC.Markov]
enum_T [in Undecidability.FOLC.Stability]
enum_eqb [in Undecidability.FOLC.LEnum]
env [in Undecidability.FOLC.GenTarski]
eqH [in Undecidability.FOLC.Heyting]
equiv_HA [in Undecidability.FOLC.Heyting]
eval [in Undecidability.FOLC.GenTarski]
evalid [in Undecidability.FOLC.Sorensen]
Exp [in Undecidability.FOLC.GenConstructions]
exp [in Undecidability.FOLC.GenConstructions]
exploding [in Undecidability.FOLC.GenConstructions]
exploding_bot [in Undecidability.FOLC.GenTarski]
exp_axiom [in Undecidability.FOLC.GenConstructions]
extend [in Undecidability.FOLC.FullFOL]
extend [in Undecidability.FOLC.FOL]
ext_c [in Undecidability.FOLC.FOL]
ext_c' [in Undecidability.FOLC.FOL]
ext_form [in Undecidability.FOLC.FullSyntax]
ext_form [in Undecidability.FOLC.Syntax]
ext_term [in Undecidability.FOLC.Terms]
F
f [in Undecidability.FOLC.Markov]F [in Undecidability.FOLC.BPCP_FOL]
fAll [in Undecidability.FOLC.WKL]
fExists [in Undecidability.FOLC.WKL]
fin_minus [in Undecidability.FOLC.FOL]
fin_T [in Undecidability.FOLC.Stability]
form_shift [in Undecidability.FOLC.FullFOL]
form_shift [in Undecidability.FOLC.FOL]
form_shift [in Undecidability.FOLC.FullND]
form_eqb [in Undecidability.FOLC.LEnum]
form_shift' [in Undecidability.FOLC.LEnum]
form_enum [in Undecidability.FOLC.Enumeration]
funcomp [in Undecidability.FOLC.axioms]
funcomp [in Undecidability.FOLC.unscoped]
F1 [in Undecidability.FOLC.BPCP_FOL]
f1 [in Undecidability.FOLC.LEnum]
F2 [in Undecidability.FOLC.BPCP_FOL]
f2 [in Undecidability.FOLC.LEnum]
F3 [in Undecidability.FOLC.BPCP_FOL]
f3 [in Undecidability.FOLC.LEnum]
f4 [in Undecidability.FOLC.LEnum]
f5 [in Undecidability.FOLC.LEnum]
f6 [in Undecidability.FOLC.LEnum]
f7 [in Undecidability.FOLC.LEnum]
f8 [in Undecidability.FOLC.LEnum]
f9 [in Undecidability.FOLC.LEnum]
G
get_n [in Undecidability.FOLC.WKL]glb_Pr [in Undecidability.FOLC.Lindenbaum]
H
halting_dec [in Undecidability.FOLC.Markov]has_model [in Undecidability.FOLC.FullTarski]
has_model [in Undecidability.FOLC.GenTarski]
Henkin [in Undecidability.FOLC.GenConstructions]
henkin [in Undecidability.FOLC.GenConstructions]
henkin_axiom [in Undecidability.FOLC.GenConstructions]
hsat [in Undecidability.FOLC.Lindenbaum]
hsat_L [in Undecidability.FOLC.Lindenbaum]
hset [in Undecidability.FOLC.Heyting]
hset_impl [in Undecidability.FOLC.Heyting]
hset_inf [in Undecidability.FOLC.Heyting]
hset_join [in Undecidability.FOLC.Heyting]
hset_meet [in Undecidability.FOLC.Heyting]
hset_bot [in Undecidability.FOLC.Heyting]
hset_equiv [in Undecidability.FOLC.Heyting]
hset_sub [in Undecidability.FOLC.Heyting]
hset_elem [in Undecidability.FOLC.Heyting]
hvalid [in Undecidability.FOLC.Lindenbaum]
I
id [in Undecidability.FOLC.unscoped]idSubst_form [in Undecidability.FOLC.FullSyntax]
idSubst_form [in Undecidability.FOLC.Syntax]
idSubst_term [in Undecidability.FOLC.Terms]
Impl'' [in Undecidability.FOLC.LEnum]
infinite_path [in Undecidability.FOLC.WKL]
infinite_tree [in Undecidability.FOLC.WKL]
Inf_indexed [in Undecidability.FOLC.Heyting]
inj [in Undecidability.FOLC.Markov]
input_fragment [in Undecidability.FOLC.GenCompleteness]
input_bot [in Undecidability.FOLC.GenCompleteness]
in_eqb [in Undecidability.FOLC.LEnum]
IP [in Undecidability.FOLC.Markov]
iprep [in Undecidability.FOLC.BPCP_FOL]
iprv [in Undecidability.FOLC.Markov]
isprv [in Undecidability.FOLC.Markov]
is_Henkin [in Undecidability.FOLC.GenConstructions]
is_phi [in Undecidability.FOLC.WKL]
IVec [in Undecidability.FOLC.SDialogues]
J
justified [in Undecidability.FOLC.SDialogues]justified [in Undecidability.FOLC.Sorensen]
K
kbottomless [in Undecidability.FOLC.Kripke]kcompleteness [in Undecidability.FOLC.Analysis]
kconstraint [in Undecidability.FOLC.Kripke]
kcon_subs [in Undecidability.FOLC.Kripke]
kexploding [in Undecidability.FOLC.Kripke]
kexploding' [in Undecidability.FOLC.Kripke]
ksat [in Undecidability.FOLC.Kripke]
kstandard [in Undecidability.FOLC.Kripke]
kvalid_T [in Undecidability.FOLC.Kripke]
kvalid_L [in Undecidability.FOLC.Kripke]
L
lb [in Undecidability.FOLC.Heyting]lb_Pr [in Undecidability.FOLC.Lindenbaum]
ldecidable [in Undecidability.FOLC.WKL]
lexp [in Undecidability.FOLC.WFexp]
lexp' [in Undecidability.FOLC.WFexp]
lift_interp [in Undecidability.FOLC.GenTarski]
listable [in Undecidability.FOLC.WKL]
list_comp [in Undecidability.FOLC.axioms]
list_id [in Undecidability.FOLC.axioms]
list_ext [in Undecidability.FOLC.axioms]
list_T [in Undecidability.FOLC.FullFOL]
list_T [in Undecidability.FOLC.FOL]
list_or [in Undecidability.FOLC.FullTarski]
list_form_eqb [in Undecidability.FOLC.LEnum]
list_term_eqb [in Undecidability.FOLC.LEnum]
L_form [in Undecidability.FOLC.FOL]
L_term [in Undecidability.FOLC.FOL]
L_vec [in Undecidability.FOLC.FOL]
L_tseq [in Undecidability.FOLC.Gentzen]
L_seq [in Undecidability.FOLC.Gentzen]
L_tsat_T [in Undecidability.FOLC.Stability]
L_sprvie [in Undecidability.FOLC.LEnum]
L_seq [in Undecidability.FOLC.LEnum]
L_form' [in Undecidability.FOLC.LEnum]
L_wf [in Undecidability.FOLC.LEnum]
L_term' [in Undecidability.FOLC.LEnum]
L_tded [in Undecidability.FOLC.ND]
L_con [in Undecidability.FOLC.ND]
L_ded [in Undecidability.FOLC.ND]
M
mapi [in Undecidability.FOLC.WKL]map_closed [in Undecidability.FOLC.Stability]
maximal [in Undecidability.FOLC.GenConstructions]
max_list_with [in Undecidability.FOLC.WKL]
min_sig_fun_ar [in Undecidability.FOLC.BPCP_FOL]
min_sig_pred_ar [in Undecidability.FOLC.BPCP_FOL]
mkApps [in Undecidability.FOLC.LEnum]
model_existence [in Undecidability.FOLC.WKL]
MP [in Undecidability.FOLC.Stability]
MPL [in Undecidability.FOLC.Markov]
mu [in Undecidability.FOLC.Markov]
M_u [in Undecidability.FOLC.WKL]
N
natinj [in Undecidability.FOLC.Markov]Neg [in Undecidability.FOLC.WKL]
normal [in Undecidability.FOLC.Gentzen]
normal [in Undecidability.FOLC.Heyting]
not_AllI [in Undecidability.FOLC.Gentzen]
not_II [in Undecidability.FOLC.Gentzen]
O
ocons [in Undecidability.FOLC.SDialogues]ocons [in Undecidability.FOLC.Sorensen]
ofNat [in Undecidability.FOLC.Markov]
of_form [in Undecidability.FOLC.LEnum]
of_term [in Undecidability.FOLC.LEnum]
OM [in Undecidability.FOLC.WKL]
Omega [in Undecidability.FOLC.GenConstructions]
omega [in Undecidability.FOLC.GenConstructions]
omniscient [in Undecidability.FOLC.WKL]
opred [in Undecidability.FOLC.SDialogues]
opred [in Undecidability.FOLC.Sorensen]
option_form_eqb [in Undecidability.FOLC.LEnum]
option_pred [in Undecidability.FOLC.LEnum]
Or [in Undecidability.FOLC.WKL]
output_fragment [in Undecidability.FOLC.GenCompleteness]
output_bot [in Undecidability.FOLC.GenCompleteness]
P
perm [in Undecidability.FOLC.WFexp]plain_enum [in Undecidability.FOLC.Enumeration]
Pr [in Undecidability.FOLC.BPCP_FOL]
Pred'' [in Undecidability.FOLC.LEnum]
pref [in Undecidability.FOLC.FOL]
prefix [in Undecidability.FOLC.WKL]
prep [in Undecidability.FOLC.BPCP_FOL]
prod_comp [in Undecidability.FOLC.axioms]
prod_ext [in Undecidability.FOLC.axioms]
prod_id [in Undecidability.FOLC.axioms]
prod_map [in Undecidability.FOLC.axioms]
prop_T [in Undecidability.FOLC.Stability]
R
raise [in Undecidability.FOLC.FOL]S
sat [in Undecidability.FOLC.FullTarski]sat [in Undecidability.FOLC.GenTarski]
scons [in Undecidability.FOLC.unscoped]
shift [in Undecidability.FOLC.unscoped]
shift_P [in Undecidability.FOLC.FullFOL]
shift_P [in Undecidability.FOLC.FOL]
sig_drop [in Undecidability.FOLC.FOL]
sig_drop' [in Undecidability.FOLC.FOL]
sig_drop_term [in Undecidability.FOLC.FOL]
sig_drop_term' [in Undecidability.FOLC.FOL]
sig_lift [in Undecidability.FOLC.FOL]
sig_lift' [in Undecidability.FOLC.FOL]
sig_lift_term [in Undecidability.FOLC.FOL]
sig_lift_term' [in Undecidability.FOLC.FOL]
sig_ext [in Undecidability.FOLC.FOL]
size [in Undecidability.FOLC.FullFOL]
size [in Undecidability.FOLC.FOL]
SM [in Undecidability.FOLC.GenTarski]
sstate [in Undecidability.FOLC.SDialogues]
sstate [in Undecidability.FOLC.Sorensen]
ST [in Undecidability.FOLC.Stability]
stable [in Undecidability.FOLC.Stability]
stable [in Undecidability.FOLC.WKL]
stab_class [in Undecidability.FOLC.Stability]
standard_bot [in Undecidability.FOLC.GenTarski]
stprv [in Undecidability.FOLC.Gentzen]
ST__f [in Undecidability.FOLC.Stability]
ST__e [in Undecidability.FOLC.Stability]
ST__a [in Undecidability.FOLC.Stability]
subset_T [in Undecidability.FOLC.FullFOL]
subset_T [in Undecidability.FOLC.FOL]
subst_form [in Undecidability.FOLC.FullSyntax]
subst_form [in Undecidability.FOLC.Syntax]
subst_form' [in Undecidability.FOLC.LEnum]
subst_term'' [in Undecidability.FOLC.LEnum]
subst_term' [in Undecidability.FOLC.LEnum]
subst_term [in Undecidability.FOLC.Terms]
subs_interp [in Undecidability.FOLC.GenTarski]
Sup [in Undecidability.FOLC.Heyting]
Sup_indexed [in Undecidability.FOLC.Heyting]
svalid [in Undecidability.FOLC.SDialogues]
svalid [in Undecidability.FOLC.Sorensen]
swin_dwin_embed [in Undecidability.FOLC.Sorensen]
T
tembed [in Undecidability.FOLC.Gentzen]term_eqb [in Undecidability.FOLC.LEnum]
Th [in Undecidability.FOLC.WKL]
theory [in Undecidability.FOLC.FullFOL]
theory [in Undecidability.FOLC.FOL]
tlexp [in Undecidability.FOLC.WFexp]
tmap [in Undecidability.FOLC.FullFOL]
tmap [in Undecidability.FOLC.FOL]
Top [in Undecidability.FOLC.Heyting]
to_form [in Undecidability.FOLC.LEnum]
to_term [in Undecidability.FOLC.LEnum]
tprv [in Undecidability.FOLC.FullND]
tprv [in Undecidability.FOLC.ND]
trans [in Undecidability.FOLC.BPCP_CND]
tsat [in Undecidability.FOLC.Stability]
t_f [in Undecidability.FOLC.BPCP_FOL]
t_e [in Undecidability.FOLC.BPCP_FOL]
T_form_term' [in Undecidability.FOLC.LEnum]
T_list_term' [in Undecidability.FOLC.LEnum]
U
ub [in Undecidability.FOLC.Heyting]union [in Undecidability.FOLC.GenConstructions]
unused_L [in Undecidability.FOLC.FullFOL]
unused_L [in Undecidability.FOLC.FOL]
up [in Undecidability.FOLC.SDialogues]
Up [in Undecidability.FOLC.SDialogues]
upExt_term_term [in Undecidability.FOLC.Terms]
upI [in Undecidability.FOLC.SDialogues]
upId_term_term [in Undecidability.FOLC.Terms]
upL [in Undecidability.FOLC.SDialogues]
upV [in Undecidability.FOLC.SDialogues]
up_ren [in Undecidability.FOLC.unscoped]
up_term_term' [in Undecidability.FOLC.LEnum]
up_subst_subst_term_term [in Undecidability.FOLC.Terms]
up_term_term [in Undecidability.FOLC.Terms]
V
valid_L [in Undecidability.FOLC.FullTarski]valid_T [in Undecidability.FOLC.FullTarski]
valid_L [in Undecidability.FOLC.GenTarski]
valid_T [in Undecidability.FOLC.GenTarski]
vapp [in Undecidability.FOLC.SDialogues]
var_zero [in Undecidability.FOLC.unscoped]
vecs_from [in Undecidability.FOLC.FOL]
vec_comp [in Undecidability.FOLC.Extend]
vec_comp [in Undecidability.FOLC.axioms]
vec_id [in Undecidability.FOLC.axioms]
vec_ext [in Undecidability.FOLC.axioms]
vec_to_env [in Undecidability.FOLC.WKL]
vec2env [in Undecidability.FOLC.Extend]
vec2vars [in Undecidability.FOLC.Extend]
venv [in Undecidability.FOLC.GenTarski]
vmap [in Undecidability.FOLC.SDialogues]
vsplit [in Undecidability.FOLC.SDialogues]
vsubs [in Undecidability.FOLC.FOL]
W
wellfounded_tree [in Undecidability.FOLC.WKL]wf_form [in Undecidability.FOLC.LEnum]
WKL [in Undecidability.FOLC.WKL]
X
XM [in Undecidability.FOLC.DeMorgan]XM [in Undecidability.FOLC.WKL]
| 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 | (2108 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 | (169 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 | (151 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 | (35 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 | (730 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 | (206 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (86 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 | (67 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 | (106 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 | (119 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 | (11 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 | (26 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 | (400 entries) |