| 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 | (1066 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 | (37 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 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 | (25 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 | (270 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 | (72 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 | (10 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 | (72 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 | (25 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 | (58 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 | (49 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 | (254 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 | (24 entries) |
Global Index
A
add [definition, in Tableaux.Prelude.Sets]add_symbol [definition, in Tableaux.Skolemization]
add_rem [lemma, in Tableaux.Prelude.Sets]
add_inv [lemma, in Tableaux.Prelude.Sets]
add_spec2 [lemma, in Tableaux.Prelude.Sets]
add_spec1 [lemma, in Tableaux.Prelude.Sets]
algo_result [record, in Tableaux.Checker]
All [constructor, in Tableaux.Syntax]
All [library]
All [library]
AlphaNegNeg [constructor, in Tableaux.ProofInstance]
AlphaNegOr [constructor, in Tableaux.ProofInstance]
alpha_rule_sound [lemma, in Tableaux.Checker]
alpha_rule [definition, in Tableaux.Checker]
antisym_subset [instance, in Tableaux.Prelude.Sets]
are_disjoint [definition, in Tableaux.Prelude.Sets]
args [projection, in Tableaux.Skolemization]
args_sound [projection, in Tableaux.Skolemization]
AtomInstances [library]
Atoms [library]
atom_car [projection, in Tableaux.Semantics]
B
BetaOr [constructor, in Tableaux.ProofInstance]beta_rule_sound [lemma, in Tableaux.Checker]
beta_rule [definition, in Tableaux.Checker]
bind [projection, in Tableaux.Prelude.Classes]
Bot [constructor, in Tableaux.Syntax]
Bound [constructor, in Tableaux.Syntax]
Branch [definition, in Tableaux.Proofs]
branching [definition, in branching]
branching [library]
BranchingStep [inductive, in Tableaux.Proofs]
BranchingStep_sind [definition, in Tableaux.Proofs]
BranchingStep_rec [definition, in Tableaux.Proofs]
BranchingStep_ind [definition, in Tableaux.Proofs]
BranchingStep_rect [definition, in Tableaux.Proofs]
branch_extend_left_right [lemma, in Tableaux.Proofs]
bv [projection, in Tableaux.Prelude.LocallyNamelessClasses]
BV [record, in Tableaux.Prelude.LocallyNamelessClasses]
bv [constructor, in Tableaux.Prelude.LocallyNamelessClasses]
BV [inductive, in Tableaux.Prelude.LocallyNamelessClasses]
BVInstances [section, in Tableaux.Prelude.LocallyNamelessClasses]
BVInstances.set_nat [variable, in Tableaux.Prelude.LocallyNamelessClasses]
bv_term [instance, in Tableaux.Syntax]
bv_eform [definition, in Tableaux.ExtendedSyntax]
bv_list [instance, in Tableaux.Prelude.LocallyNamelessClasses]
C
car [projection, in Tableaux.Prelude.Sets]car [projection, in Tableaux.Semantics]
carrier_eq_dec [lemma, in Tableaux.Prelude.Sets]
Checker [library]
CheckerAlgorithm [definition, in Tableaux.Checker]
CheckProof [definition, in Tableaux.Checker]
CheckProof_sound [lemma, in Tableaux.Checker]
CheckProof_Some_Sequence_closed [lemma, in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_closed [lemma, in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_is_expansion_sequence [lemma, in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_Some [lemma, in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_Some__aux [lemma, in Tableaux.Checker]
CheckProof_aux [definition, in Tableaux.Checker]
Classes [library]
closed_in_union_closed_in_right [lemma, in Tableaux.ExtendedSyntax]
closed_in_union_closed_in_left [lemma, in Tableaux.ExtendedSyntax]
closed_in_translate_ETerm [lemma, in Tableaux.ExtendedSyntax]
closed_in_nil [lemma, in Tableaux.ExtendedSyntax]
closed_in [definition, in Tableaux.ExtendedSyntax]
closure_rule [definition, in Tableaux.Checker]
Core [library]
Core [library]
Ctx [module, in Tableaux.Checker]
Ctx.add [definition, in Tableaux.Checker]
Ctx.elements [definition, in Tableaux.Checker]
Ctx.eq [definition, in Tableaux.Checker]
Ctx.existsb [definition, in Tableaux.Checker]
Ctx.existsb_exists [lemma, in Tableaux.Checker]
Ctx.from_list [definition, in Tableaux.Checker]
Ctx.fv [definition, in Tableaux.Checker]
Ctx.In [definition, in Tableaux.Checker]
Ctx.mem [definition, in Tableaux.Checker]
Ctx.mem_spec [lemma, in Tableaux.Checker]
Ctx.pr_ctx [instance, in Tableaux.Checker]
Ctx.singleton [definition, in Tableaux.Checker]
Ctx.t [definition, in Tableaux.Checker]
Ctx.union [definition, in Tableaux.Checker]
D
data [projection, in Tableaux.Skolemization]DecEqForms [section, in Tableaux.Syntax]
DecEqForms.func [variable, in Tableaux.Syntax]
DecEqForms.pred [variable, in Tableaux.Syntax]
DecEqForms.var [variable, in Tableaux.Syntax]
DecEqTerms [section, in Tableaux.Syntax]
DecEqTerms.func [variable, in Tableaux.Syntax]
DecEqTerms.Term [variable, in Tableaux.Syntax]
DecEqTerms.var [variable, in Tableaux.Syntax]
DeltaNegAll [constructor, in Tableaux.ProofInstance]
delta_rule_sound [lemma, in Tableaux.Checker]
delta_rule [definition, in Tableaux.Checker]
diff [projection, in Tableaux.Prelude.Sets]
diff_spec [projection, in Tableaux.Prelude.Sets]
disjoint [definition, in Tableaux.Prelude.Sets]
disjoint_sym [lemma, in Tableaux.Prelude.Sets]
disjoint_are_disjoint [lemma, in Tableaux.Prelude.Sets]
drinker [definition, in drinker]
drinker [library]
drinker0 [definition, in drinker]
E
EAll [constructor, in Tableaux.ExtendedSyntax]EAnd [constructor, in Tableaux.ExtendedSyntax]
EBot [constructor, in Tableaux.ExtendedSyntax]
EEqu [constructor, in Tableaux.ExtendedSyntax]
EEx [constructor, in Tableaux.ExtendedSyntax]
EForm [inductive, in Tableaux.ExtendedSyntax]
EForm_sind [definition, in Tableaux.ExtendedSyntax]
EForm_rec [definition, in Tableaux.ExtendedSyntax]
EForm_ind [definition, in Tableaux.ExtendedSyntax]
EForm_rect [definition, in Tableaux.ExtendedSyntax]
EFun [constructor, in Tableaux.ExtendedSyntax]
EImp [constructor, in Tableaux.ExtendedSyntax]
EmptyBranch [definition, in Tableaux.Proofs]
empty_to_set [projection, in Tableaux.Skolemization]
empty_record [projection, in Tableaux.Skolemization]
empty_disjointr [lemma, in Tableaux.Prelude.Sets]
empty_disjointl [lemma, in Tableaux.Prelude.Sets]
empty_unitr [lemma, in Tableaux.Prelude.Sets]
empty_unitl [lemma, in Tableaux.Prelude.Sets]
empty_is_empty [lemma, in Tableaux.Prelude.Sets]
empty_spec [projection, in Tableaux.Prelude.Sets]
empty_set [projection, in Tableaux.Prelude.Sets]
empty_env [definition, in Tableaux.Semantics]
ENeg [constructor, in Tableaux.ExtendedSyntax]
env [definition, in Tableaux.Semantics]
EOr [constructor, in Tableaux.ExtendedSyntax]
EPred [constructor, in Tableaux.ExtendedSyntax]
eqb [projection, in Tableaux.Prelude.Classes]
eqbIsEq [projection, in Tableaux.Prelude.Classes]
EqBool [record, in Tableaux.Prelude.Classes]
EqBool_neq [lemma, in Tableaux.Prelude.Classes]
EqBool_refl [lemma, in Tableaux.Prelude.Classes]
eqbool_form [instance, in Tableaux.Syntax]
EqBool_term [instance, in Tableaux.Syntax]
eqb_from_eqDec_is_eq [lemma, in Tableaux.Prelude.Classes]
eqb_from_eqDec [definition, in Tableaux.Prelude.Classes]
eqb_form_eq [lemma, in Tableaux.Syntax]
eqb_form [definition, in Tableaux.Syntax]
eqb_term_eq [lemma, in Tableaux.Syntax]
eqb_term [definition, in Tableaux.Syntax]
eqb_list [instance, in Tableaux.Prelude.Utils]
eqb_list_is_eq [lemma, in Tableaux.Prelude.Utils]
eqb_atom [projection, in Tableaux.Prelude.Atoms]
eqDec [projection, in Tableaux.Prelude.Classes]
EqDec [record, in Tableaux.Prelude.Classes]
eqDec [constructor, in Tableaux.Prelude.Classes]
EqDec [inductive, in Tableaux.Prelude.Classes]
EqDecOtherInstances [section, in Tableaux.Prelude.Classes]
EqDecOtherInstances.A [variable, in Tableaux.Prelude.Classes]
EqDec_refl [lemma, in Tableaux.Prelude.Classes]
EqDec_UIP [lemma, in Tableaux.Prelude.Classes]
eqDec_Term [instance, in Tableaux.Syntax]
EqDec_BranchingStep [instance, in Tableaux.Proofs]
equiv [definition, in Tableaux.Semantics]
EquivEqBoolEqDec [section, in Tableaux.Prelude.Classes]
EquivEqBoolEqDec.A [variable, in Tableaux.Prelude.Classes]
EquivForallIn [section, in Tableaux.Prelude.Ind]
EquivForallIn.A [variable, in Tableaux.Prelude.Ind]
EquivForallIn.P [variable, in Tableaux.Prelude.Ind]
equiv_proper_interp [instance, in Tableaux.Semantics]
equiv_imply [lemma, in Tableaux.Semantics]
equiv_equiv [instance, in Tableaux.Semantics]
equiv_trans [instance, in Tableaux.Semantics]
equiv_sym [instance, in Tableaux.Semantics]
equiv_refl [instance, in Tableaux.Semantics]
eq_dec_list [instance, in Tableaux.Prelude.Classes]
eq_bool_unit [instance, in Tableaux.Prelude.Classes]
eq_dec_string [instance, in Tableaux.Prelude.Classes]
eq_bool_string [instance, in Tableaux.Prelude.Classes]
eq_bool_nat [instance, in Tableaux.Prelude.Classes]
eq_dec_nat [instance, in Tableaux.Prelude.Classes]
eq_dec_bool [instance, in Tableaux.Prelude.Classes]
eq_bool_from_eq_dec [instance, in Tableaux.Prelude.Classes]
eq_dec_from_eq_bool [instance, in Tableaux.Prelude.Classes]
error [definition, in Tableaux.Checker]
ESemantics [section, in Tableaux.ExtendedSyntax]
ESyntax [section, in Tableaux.ExtendedSyntax]
ESyntaxTranslation [section, in Tableaux.ExtendedSyntax]
ESyntaxTranslation.ClosedIn [section, in Tableaux.ExtendedSyntax]
ESyntaxTranslation.ClosedIn.Container [variable, in Tableaux.ExtendedSyntax]
ESyntaxTranslation.ClosedIn.mem [variable, in Tableaux.ExtendedSyntax]
ESyntaxTranslation.IndexOf [section, in Tableaux.ExtendedSyntax]
ESyntaxTranslation.IndexOf.A [variable, in Tableaux.ExtendedSyntax]
ETerm [inductive, in Tableaux.ExtendedSyntax]
ETermInd [section, in Tableaux.ExtendedSyntax]
eterm_translation_is_always_locally_closed [lemma, in Tableaux.ExtendedSyntax]
eterm_ind' [definition, in Tableaux.ExtendedSyntax]
eterm_rect' [definition, in Tableaux.ExtendedSyntax]
eterm_ind [definition, in Tableaux.ExtendedSyntax]
eterm_rect [definition, in Tableaux.ExtendedSyntax]
ETerm_sind [definition, in Tableaux.ExtendedSyntax]
ETerm_rec [definition, in Tableaux.ExtendedSyntax]
ETerm_ind [definition, in Tableaux.ExtendedSyntax]
ETerm_rect [definition, in Tableaux.ExtendedSyntax]
ETop [constructor, in Tableaux.ExtendedSyntax]
ETranslation [record, in Tableaux.ExtendedSyntax]
ETranslation [inductive, in Tableaux.ExtendedSyntax]
etranslation_term [instance, in Tableaux.ExtendedSyntax]
etranslation_eform [instance, in Tableaux.ExtendedSyntax]
EVar [constructor, in Tableaux.ExtendedSyntax]
exists_satisfied_branch [definition, in Tableaux.Proofs]
expand_tableau_branch_Some_symbs [lemma, in Tableaux.Proofs]
expand_tableau_branch_Some__aux [lemma, in Tableaux.Proofs]
expand_tableau_branch [definition, in Tableaux.Proofs]
expand_tableau_branch_right [lemma, in Tableaux.Proofs]
expand_tableau_branch_left [lemma, in Tableaux.Proofs]
expand_tableau_branch_Some_is_branch_of [lemma, in Tableaux.Proofs]
expand_tableau_branch__aux [definition, in Tableaux.Proofs]
ExpansionRules [section, in Tableaux.Proofs]
ExpansionRules.Form [variable, in Tableaux.Proofs]
ExpansionRules.func [variable, in Tableaux.Proofs]
ExpansionRules.pred [variable, in Tableaux.Proofs]
ExpansionRules.set_nat [variable, in Tableaux.Proofs]
ExpansionRules.sko [variable, in Tableaux.Proofs]
ExpansionRules.Tableau [variable, in Tableaux.Proofs]
ExpansionRules.Term [variable, in Tableaux.Proofs]
ExpansionRules.var [variable, in Tableaux.Proofs]
_ |> _ [notation, in Tableaux.Proofs]
ExpansionStep [inductive, in Tableaux.Proofs]
ExpansionStep_sind [definition, in Tableaux.Proofs]
ExpansionStep_ind [definition, in Tableaux.Proofs]
expansion_NegAll [constructor, in Tableaux.Proofs]
expansion_All [constructor, in Tableaux.Proofs]
expansion_Or [constructor, in Tableaux.Proofs]
expansion_NegOr [constructor, in Tableaux.Proofs]
expansion_NegNeg [constructor, in Tableaux.Proofs]
explosion_principle [lemma, in Tableaux.Semantics]
ExtendedSyntax [module, in Tableaux.Checker]
ExtendedSyntax [library]
ExtendedSyntaxNotation [module, in Tableaux.ExtendedSyntax]
_ '<=> _ [notation, in Tableaux.ExtendedSyntax]
_ '=> _ [notation, in Tableaux.ExtendedSyntax]
_ '&& _ [notation, in Tableaux.ExtendedSyntax]
_ '|| _ [notation, in Tableaux.ExtendedSyntax]
_ ''( _ ,, _ ,, .. ,, _ ) [notation, in Tableaux.ExtendedSyntax]
_ ''( _ ) [notation, in Tableaux.ExtendedSyntax]
_ ''() [notation, in Tableaux.ExtendedSyntax]
_ '( _ ,, _ ,, .. ,, _ ) [notation, in Tableaux.ExtendedSyntax]
_ '( _ ) [notation, in Tableaux.ExtendedSyntax]
_ '() [notation, in Tableaux.ExtendedSyntax]
'Bot [notation, in Tableaux.ExtendedSyntax]
'Top [notation, in Tableaux.ExtendedSyntax]
'! _ :( _ ) [notation, in Tableaux.ExtendedSyntax]
' _ [notation, in Tableaux.ExtendedSyntax]
'? _ :( _ ) [notation, in Tableaux.ExtendedSyntax]
'~ _ [notation, in Tableaux.ExtendedSyntax]
ExtendedSyntax.compile [definition, in Tableaux.Checker]
ExtendedSyntax.compile__aux [definition, in Tableaux.Checker]
ExtendedSyntax.E [module, in Tableaux.Checker]
ExtendedSyntax.Extended_CheckProof_sound [lemma, in Tableaux.Checker]
ExtendedSyntax.E.AlphaAnd [constructor, in Tableaux.Checker]
ExtendedSyntax.E.AlphaNegImp [constructor, in Tableaux.Checker]
ExtendedSyntax.E.AlphaNegNeg [constructor, in Tableaux.Checker]
ExtendedSyntax.E.AlphaNegOr [constructor, in Tableaux.Checker]
ExtendedSyntax.E.BetaEqu [constructor, in Tableaux.Checker]
ExtendedSyntax.E.BetaImp [constructor, in Tableaux.Checker]
ExtendedSyntax.E.BetaNegAnd [constructor, in Tableaux.Checker]
ExtendedSyntax.E.BetaNegEqu [constructor, in Tableaux.Checker]
ExtendedSyntax.E.BetaOr [constructor, in Tableaux.Checker]
ExtendedSyntax.E.DeltaEx [constructor, in Tableaux.Checker]
ExtendedSyntax.E.DeltaNegAll [constructor, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule [inductive, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree [inductive, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_sind [definition, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_rec [definition, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_ind [definition, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_rect [definition, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_sind [definition, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_rec [definition, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_ind [definition, in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_rect [definition, in Tableaux.Checker]
ExtendedSyntax.E.GammaAll [constructor, in Tableaux.Checker]
ExtendedSyntax.E.GammaNegEx [constructor, in Tableaux.Checker]
ExtendedSyntax.E.Leaf [constructor, in Tableaux.Checker]
ExtendedSyntax.E.mkBinaryNode [definition, in Tableaux.Checker]
ExtendedSyntax.E.mkClosure [definition, in Tableaux.Checker]
ExtendedSyntax.E.mkTrivialClosure [definition, in Tableaux.Checker]
ExtendedSyntax.E.mkUnaryNode [definition, in Tableaux.Checker]
ExtendedSyntax.E.Node [constructor, in Tableaux.Checker]
ExtendedSyntax.get_neg_all [definition, in Tableaux.Checker]
ExtendedSyntax.get_ex [definition, in Tableaux.Checker]
ExtendedSyntax.get_neg_ex [definition, in Tableaux.Checker]
ExtendedSyntax.get_all [definition, in Tableaux.Checker]
ExtendedSyntax.get_neg_equ [definition, in Tableaux.Checker]
ExtendedSyntax.get_equ [definition, in Tableaux.Checker]
ExtendedSyntax.get_neg_and [definition, in Tableaux.Checker]
ExtendedSyntax.get_imp [definition, in Tableaux.Checker]
ExtendedSyntax.get_or [definition, in Tableaux.Checker]
ExtendedSyntax.get_neg_imp [definition, in Tableaux.Checker]
ExtendedSyntax.get_and [definition, in Tableaux.Checker]
ExtendedSyntax.get_neg_or [definition, in Tableaux.Checker]
ExtendedSyntax.get_neg_neg [definition, in Tableaux.Checker]
extended_environment_comp_Some [lemma, in Tableaux.ExtendedSyntax]
extended_environment_comp_None [lemma, in Tableaux.ExtendedSyntax]
extended_environment [definition, in Tableaux.ExtendedSyntax]
extend_subset_preserves_function_symbols [lemma, in Tableaux.Proofs]
extend_function_symbols_value [lemma, in Tableaux.Proofs]
extend_extended_environment [lemma, in Tableaux.ExtendedSyntax]
extend_with_imply_form [lemma, in Tableaux.Semantics]
extend_with_equiv_form [lemma, in Tableaux.Semantics]
Extraction [library]
F
Forall [inductive, in Tableaux.Prelude.Ind]forallb2 [definition, in Tableaux.Prelude.Utils]
forallb2_refl [lemma, in Tableaux.Prelude.Utils]
forallb2_eq [lemma, in Tableaux.Prelude.Utils]
Forall_inv [lemma, in Tableaux.Prelude.Ind]
Forall_tail [lemma, in Tableaux.Prelude.Ind]
Forall_In [lemma, in Tableaux.Prelude.Ind]
Forall_sind [definition, in Tableaux.Prelude.Ind]
Forall_rec [definition, in Tableaux.Prelude.Ind]
Forall_ind [definition, in Tableaux.Prelude.Ind]
Forall_rect [definition, in Tableaux.Prelude.Ind]
Forall_cons [constructor, in Tableaux.Prelude.Ind]
Forall_nil [constructor, in Tableaux.Prelude.Ind]
Form [inductive, in Tableaux.Syntax]
Form [definition, in Tableaux.SyntaxInstance]
formula_contradiction_sound [lemma, in Tableaux.Checker]
formula_contradiction [definition, in Tableaux.Checker]
form_subst_opening [lemma, in Tableaux.Syntax]
Form_sind [definition, in Tableaux.Syntax]
Form_rec [definition, in Tableaux.Syntax]
Form_ind [definition, in Tableaux.Syntax]
Form_rect [definition, in Tableaux.Syntax]
form_env_inst_commutes [lemma, in Tableaux.Semantics]
Free [constructor, in Tableaux.Syntax]
FreeVariables [section, in Tableaux.Prelude.LocallyNamelessClasses]
FreeVariables.set_var [variable, in Tableaux.Prelude.LocallyNamelessClasses]
FreeVariables.var [variable, in Tableaux.Prelude.LocallyNamelessClasses]
from_list [definition, in Tableaux.Prelude.Sets]
FSet [module, in Tableaux.SyntaxInstance]
Fun [constructor, in Tableaux.Syntax]
FunctionSymbols [section, in Tableaux.Syntax]
FunctionSymbols.Form [variable, in Tableaux.Syntax]
FunctionSymbols.func [variable, in Tableaux.Syntax]
FunctionSymbols.pred [variable, in Tableaux.Syntax]
FunctionSymbols.Term [variable, in Tableaux.Syntax]
FunctionSymbols.var [variable, in Tableaux.Syntax]
function_symbols_opening_all_free [lemma, in Tableaux.Syntax]
function_symbols_opening_form' [lemma, in Tableaux.Syntax]
function_symbols_opening_terms' [lemma, in Tableaux.Syntax]
function_symbols_opening [lemma, in Tableaux.Syntax]
function_symbols_opening_terms [lemma, in Tableaux.Syntax]
function_symbols [projection, in Tableaux.Syntax]
function_symbols [constructor, in Tableaux.Syntax]
funext [axiom, in Tableaux.Prelude.Init]
fv [projection, in Tableaux.Prelude.LocallyNamelessClasses]
FV [record, in Tableaux.Prelude.LocallyNamelessClasses]
fv [constructor, in Tableaux.Prelude.LocallyNamelessClasses]
FV [inductive, in Tableaux.Prelude.LocallyNamelessClasses]
FVForms [section, in Tableaux.Syntax]
FVForms.func [variable, in Tableaux.Syntax]
FVForms.pred [variable, in Tableaux.Syntax]
FVForms.set_var [variable, in Tableaux.Syntax]
FVForms.var [variable, in Tableaux.Syntax]
FVInstances [section, in Tableaux.Prelude.LocallyNamelessClasses]
FVInstances.set_var [variable, in Tableaux.Prelude.LocallyNamelessClasses]
FVInstances.var [variable, in Tableaux.Prelude.LocallyNamelessClasses]
FVTerms [section, in Tableaux.Syntax]
FVTerms.func [variable, in Tableaux.Syntax]
FVTerms.set_var [variable, in Tableaux.Syntax]
FVTerms.var [variable, in Tableaux.Syntax]
fv_form [instance, in Tableaux.Syntax]
fv_term [instance, in Tableaux.Syntax]
fv_eterm [definition, in Tableaux.ExtendedSyntax]
fv_list_in [lemma, in Tableaux.Prelude.LocallyNamelessClasses]
fv_list [instance, in Tableaux.Prelude.LocallyNamelessClasses]
G
GammaAll [constructor, in Tableaux.ProofInstance]gamma_rule_sound [lemma, in Tableaux.Checker]
gamma_rule [definition, in Tableaux.Checker]
gen_translation_equivalidity [lemma, in Tableaux.ExtendedSyntax]
gen_interp_term_interp_eterm [lemma, in Tableaux.ExtendedSyntax]
GetFunctSymbols [record, in Tableaux.Syntax]
GetFunctSymbols [inductive, in Tableaux.Syntax]
GetFunctSymbols_form [instance, in Tableaux.Syntax]
GetFunctSymbols_in [lemma, in Tableaux.Syntax]
GetFunctSymbols_opt [instance, in Tableaux.Syntax]
GetFunctSymbols_list [instance, in Tableaux.Syntax]
GetFunctSymbols_term [instance, in Tableaux.Syntax]
getter_neg_neg_sound [lemma, in Tableaux.Checker]
get_symbol [definition, in Tableaux.Syntax]
get_context_extend_oth [lemma, in Tableaux.Proofs]
get_context_extend_right [lemma, in Tableaux.Proofs]
get_context_extend_left [lemma, in Tableaux.Proofs]
get_all_formulas [definition, in Tableaux.Proofs]
get_context_app_fst [lemma, in Tableaux.Proofs]
get_context_replace_child_oth [lemma, in Tableaux.Proofs]
get_context [definition, in Tableaux.Proofs]
get_child_at [definition, in Tableaux.Proofs]
get_label [definition, in Tableaux.Proofs]
get_neg_all [definition, in Tableaux.Checker]
get_all [definition, in Tableaux.Checker]
get_neg_or [definition, in Tableaux.Checker]
get_or [definition, in Tableaux.Checker]
get_neg_neg [definition, in Tableaux.Checker]
get_replace_nth_inv' [lemma, in Tableaux.Prelude.Utils]
get_replace_nth' [lemma, in Tableaux.Prelude.Utils]
get_replace_nth [lemma, in Tableaux.Prelude.Utils]
H
HasSubformulas [record, in Tableaux.Syntax]HasSubformulas [inductive, in Tableaux.Syntax]
HasSubformulas_Form [instance, in Tableaux.Syntax]
HasSubformulas_list [instance, in Tableaux.Syntax]
hasTableau [definition, in Tableaux.Proofs]
hasTableau_inner_drinker_proof [lemma, in drinker]
hasTableau_outer_drinker_proof [lemma, in drinker]
hasTableau_inner_branching_proof [lemma, in branching]
hasTableau_outer_branching_proof [lemma, in branching]
hasTableau_sound [lemma, in Tableaux.Proofs]
hasTableau_not_satisfiable [lemma, in Tableaux.Proofs]
hasTableau_is_evalid [lemma, in Tableaux.ExtendedSyntax]
hd_error_hd [lemma, in Tableaux.Prelude.Utils]
I
imply [definition, in Tableaux.Semantics]In [definition, in Tableaux.Prelude.Ind]
Ind [library]
index_of_None [lemma, in Tableaux.ExtendedSyntax]
index_of_prefix [lemma, in Tableaux.ExtendedSyntax]
index_of_length [lemma, in Tableaux.ExtendedSyntax]
index_of_rapp'' [lemma, in Tableaux.ExtendedSyntax]
index_of_rapp' [lemma, in Tableaux.ExtendedSyntax]
index_of_rapp [lemma, in Tableaux.ExtendedSyntax]
index_of_nth [lemma, in Tableaux.ExtendedSyntax]
index_of_cons' [lemma, in Tableaux.ExtendedSyntax]
index_of_cons [lemma, in Tableaux.ExtendedSyntax]
index_of_In' [lemma, in Tableaux.ExtendedSyntax]
index_of_In [lemma, in Tableaux.ExtendedSyntax]
index_of_inj [lemma, in Tableaux.ExtendedSyntax]
index_of_spec [lemma, in Tableaux.ExtendedSyntax]
index_of [definition, in Tableaux.ExtendedSyntax]
Init [library]
InnerSkolemization [definition, in Tableaux.SkolemizationInstances]
InnerSkolemization [definition, in Tableaux.Skolemization]
InnerSkolemizationData [definition, in Tableaux.Skolemization]
InnerSkolemization_function_symbols [lemma, in Tableaux.Skolemization]
InnerSkolemization_isFunc [lemma, in Tableaux.Skolemization]
InnerSkolemization_isLocallyClosed [lemma, in Tableaux.Skolemization]
InnerSkolemization_args_vars [lemma, in Tableaux.Skolemization]
InnerSkolemization_is_sko_pred_sound [lemma, in Tableaux.Skolemization]
InnerSkolemization_is_sko_pred [definition, in Tableaux.Skolemization]
inner_drinker_proof [definition, in drinker]
inner_subst [definition, in drinker]
instantiate_eform_commutes_instantiate_form [lemma, in Tableaux.ExtendedSyntax]
instantiate_eterm_commutes_instantiate_term [lemma, in Tableaux.ExtendedSyntax]
instantiate_shadowed_form [lemma, in Tableaux.ExtendedSyntax]
instantiate_shadowed_term [lemma, in Tableaux.ExtendedSyntax]
instantiate_eform [definition, in Tableaux.ExtendedSyntax]
instantiate_eterm [definition, in Tableaux.ExtendedSyntax]
instantiate_imply_all [lemma, in Tableaux.Semantics]
inter [projection, in Tableaux.Prelude.Sets]
interpret [projection, in Tableaux.Semantics]
Interpret [record, in Tableaux.Semantics]
interpret [constructor, in Tableaux.Semantics]
Interpret [inductive, in Tableaux.Semantics]
interpret_eform [definition, in Tableaux.ExtendedSyntax]
interpret_eterm [definition, in Tableaux.ExtendedSyntax]
interpret_form [instance, in Tableaux.Semantics]
interpret_term [instance, in Tableaux.Semantics]
interpret_list [instance, in Tableaux.Semantics]
interp_list_commute [lemma, in Tableaux.Semantics]
interp_form_list [lemma, in Tableaux.Semantics]
interp_pred [projection, in Tableaux.Semantics]
interp_func [projection, in Tableaux.Semantics]
inter_sym [lemma, in Tableaux.Prelude.Sets]
inter_spec [projection, in Tableaux.Prelude.Sets]
In_Forall [lemma, in Tableaux.Prelude.Ind]
in_context_is_on_branch [lemma, in Tableaux.Proofs]
in_get_ctx_in_all_formulas [lemma, in Tableaux.Proofs]
in_record [definition, in Tableaux.Skolemization]
In_In_replace_nth [lemma, in Tableaux.Prelude.Utils]
In_replace_nth' [lemma, in Tableaux.Prelude.Utils]
In_replace_nth [lemma, in Tableaux.Prelude.Utils]
In_index_of [lemma, in Tableaux.ExtendedSyntax]
in_form_list_interp [lemma, in Tableaux.Semantics]
in_form_list_models [lemma, in Tableaux.Semantics]
isAtom [record, in Tableaux.Prelude.Atoms]
isClosed [definition, in Tableaux.Prelude.LocallyNamelessClasses]
isClosedLemmas [section, in Tableaux.Syntax]
isClosedLemmas.Form [variable, in Tableaux.Syntax]
isClosedLemmas.func [variable, in Tableaux.Syntax]
isClosedLemmas.pred [variable, in Tableaux.Syntax]
isClosedLemmas.set_nat [variable, in Tableaux.Syntax]
isClosedLemmas.Term [variable, in Tableaux.Syntax]
isClosedLemmas.var [variable, in Tableaux.Syntax]
isClosedList_isClosedFormList [lemma, in Tableaux.Syntax]
isClosedList_isClosedFormisClosed [lemma, in Tableaux.Syntax]
isClosedList_elem [lemma, in Tableaux.Syntax]
isClosed_subst_form [lemma, in Tableaux.Syntax]
isClosed_subst_term [lemma, in Tableaux.Syntax]
isClosed_interp_form_env_eq [lemma, in Tableaux.Semantics]
isClosed_interp_term_env_eq [lemma, in Tableaux.Semantics]
isLocallyClosed [definition, in Tableaux.Prelude.LocallyNamelessClasses]
isLocallyClosed_isLocallyClosed_subst [lemma, in Tableaux.Syntax]
isLocallyClosed_Fun_isLocallyClosed_list' [lemma, in Tableaux.Syntax]
isLocallyClosed_Fun_isLocallyClosed_list [lemma, in Tableaux.Syntax]
isLocallyClosed_interp_env [lemma, in Tableaux.Semantics]
isSkolemization [record, in Tableaux.Skolemization]
isSkolemization_InnerSkolemizationData [lemma, in Tableaux.Skolemization]
isSkolemization_OuterSkolemizationData [lemma, in Tableaux.Skolemization]
isSubst [projection, in Tableaux.Prelude.LocallyNamelessClasses]
is_free_sound [lemma, in Tableaux.Syntax]
is_free [definition, in Tableaux.Syntax]
is_subformula [projection, in Tableaux.Syntax]
is_subformula [constructor, in Tableaux.Syntax]
is_litteral [definition, in Tableaux.Syntax]
is_negative_litteral [definition, in Tableaux.Syntax]
is_positive_litteral [definition, in Tableaux.Syntax]
is_subterm_trans [lemma, in Tableaux.Syntax]
is_subterm [definition, in Tableaux.Syntax]
is_tableau_proof [definition, in Tableaux.Proofs]
is_expansion_sequence_singleton [lemma, in Tableaux.Proofs]
is_expansion_sequence_nil [lemma, in Tableaux.Proofs]
is_expansion_sequence [definition, in Tableaux.Proofs]
is_on_satisfiable_branch [lemma, in Tableaux.Proofs]
is_on_branch_in_context [lemma, in Tableaux.Proofs]
is_satisfiable_extend [lemma, in Tableaux.Proofs]
is_satisfiable_extend_gen [lemma, in Tableaux.Proofs]
is_optional_satisfied [definition, in Tableaux.Proofs]
is_branch_of_expand_tableau_branch [lemma, in Tableaux.Proofs]
is_tableau_satisfiable [definition, in Tableaux.Proofs]
is_tableau_closed [definition, in Tableaux.Proofs]
is_branch_closed [definition, in Tableaux.Proofs]
is_branch_of_replace_child_oth_inv [lemma, in Tableaux.Proofs]
is_branch_of_replace_child_oth [lemma, in Tableaux.Proofs]
is_branch_of_get_child_at [lemma, in Tableaux.Proofs]
is_subbranch_of_has_label [lemma, in Tableaux.Proofs]
is_branch_of_extend_oth [lemma, in Tableaux.Proofs]
is_branch_of_extend_None [lemma, in Tableaux.Proofs]
is_branch_of_extend_right [lemma, in Tableaux.Proofs]
is_branch_of_extend_left' [lemma, in Tableaux.Proofs]
is_branch_of_extend_left [lemma, in Tableaux.Proofs]
is_on_branch_sind [definition, in Tableaux.Proofs]
is_on_branch_ind [definition, in Tableaux.Proofs]
is_on_branch_right [constructor, in Tableaux.Proofs]
is_on_branch_left [constructor, in Tableaux.Proofs]
is_on_branch_node [constructor, in Tableaux.Proofs]
is_on_branch [inductive, in Tableaux.Proofs]
is_branch_of_is_subbranch_of [lemma, in Tableaux.Proofs]
is_subbranch_of_sind [definition, in Tableaux.Proofs]
is_subbranch_of_ind [definition, in Tableaux.Proofs]
is_subbranch_of_right [constructor, in Tableaux.Proofs]
is_subbranch_of_left [constructor, in Tableaux.Proofs]
is_subbranch_of_node [constructor, in Tableaux.Proofs]
is_subbranch_of [inductive, in Tableaux.Proofs]
is_branch_of_dec [lemma, in Tableaux.Proofs]
is_branch_of_sind [definition, in Tableaux.Proofs]
is_branch_of_ind [definition, in Tableaux.Proofs]
is_branch_of_right [constructor, in Tableaux.Proofs]
is_branch_of_left [constructor, in Tableaux.Proofs]
is_branch_of_nil [constructor, in Tableaux.Proofs]
is_branch_of [inductive, in Tableaux.Proofs]
is_fv_in [definition, in Tableaux.Skolemization]
is_skolemization [projection, in Tableaux.Skolemization]
is_sko_sound [projection, in Tableaux.Skolemization]
is_sko_consistent [projection, in Tableaux.Skolemization]
is_func [projection, in Tableaux.Skolemization]
is_sko [projection, in Tableaux.Skolemization]
is_valid_translation_is_valid [lemma, in Tableaux.ExtendedSyntax]
is_evalid [definition, in Tableaux.ExtendedSyntax]
is_empty_union [lemma, in Tableaux.Prelude.Sets]
is_empty_union2 [lemma, in Tableaux.Prelude.Sets]
is_empty_union1 [lemma, in Tableaux.Prelude.Sets]
is_empty_spec' [lemma, in Tableaux.Prelude.Sets]
is_empty_spec [lemma, in Tableaux.Prelude.Sets]
is_empty [definition, in Tableaux.Prelude.Sets]
is_satisfiable_equiv [lemma, in Tableaux.Semantics]
is_satisfiable_is_not_countersat [lemma, in Tableaux.Semantics]
is_satisfiable [definition, in Tableaux.Semantics]
is_valid [definition, in Tableaux.Semantics]
J
join [projection, in Tableaux.Skolemization]join_unitl [lemma, in Tableaux.Skolemization]
join_unitr [lemma, in Tableaux.Skolemization]
join_to_set [projection, in Tableaux.Skolemization]
join_spec [projection, in Tableaux.Skolemization]
L
last_nth_error [lemma, in Tableaux.Prelude.Utils]last_app [lemma, in Tableaux.Prelude.Utils]
last_cons [lemma, in Tableaux.Prelude.Utils]
Leaf [constructor, in Tableaux.Proofs]
Leaf [constructor, in Tableaux.ProofInstance]
Left [constructor, in Tableaux.Proofs]
list_replace [definition, in Tableaux.Prelude.Classes]
list_mem_spec [lemma, in Tableaux.Prelude.Utils]
list_mem [definition, in Tableaux.Prelude.Utils]
LocallyNamelessClasses [library]
locally_closed_subst_translation [lemma, in Tableaux.ExtendedSyntax]
ls_to_form [definition, in Tableaux.Syntax]
ls_to_eform_ls_to_form [lemma, in Tableaux.ExtendedSyntax]
ls_to_eform [definition, in Tableaux.ExtendedSyntax]
ls_to_form_app [lemma, in Tableaux.Semantics]
ls_to_form_commutes [lemma, in Tableaux.Semantics]
ltb_list_false [lemma, in Tableaux.Prelude.Utils]
ltb_list_lt_list [lemma, in Tableaux.Prelude.Utils]
ltb_list [definition, in Tableaux.Prelude.Utils]
ltb_form_false [lemma, in Tableaux.SyntaxInstance]
ltb_form_lt_form [lemma, in Tableaux.SyntaxInstance]
ltb_form [definition, in Tableaux.SyntaxInstance]
ltb_term_false [lemma, in Tableaux.SyntaxInstance]
ltb_term_lt_term [lemma, in Tableaux.SyntaxInstance]
ltb_term [definition, in Tableaux.SyntaxInstance]
lt_list [definition, in Tableaux.Prelude.Utils]
lt_strorder [instance, in Tableaux.SyntaxInstance]
lt_term_strorder [instance, in Tableaux.SyntaxInstance]
lt_form [definition, in Tableaux.SyntaxInstance]
lt_term [definition, in Tableaux.SyntaxInstance]
M
match_eq_dec_eq_bool [lemma, in Tableaux.Prelude.Classes]mem [projection, in Tableaux.Prelude.Sets]
mem_record_spec [lemma, in Tableaux.Skolemization]
mem_record [definition, in Tableaux.Skolemization]
mem_list [definition, in Tableaux.ExtendedSyntax]
mem_spec' [lemma, in Tableaux.Prelude.Sets]
mem_unionr [lemma, in Tableaux.Prelude.Sets]
mem_unionl [lemma, in Tableaux.Prelude.Sets]
mem_spec [projection, in Tableaux.Prelude.Sets]
mkLeaf [definition, in Tableaux.Proofs]
mkOptionalNode [definition, in Tableaux.Proofs]
mkTableau [definition, in Tableaux.Proofs]
mk_env [definition, in Tableaux.Semantics]
Model [record, in Tableaux.Semantics]
models_P_neg_P [lemma, in Tableaux.Semantics]
models_iff [lemma, in Tableaux.Semantics]
Monad [record, in Tableaux.Prelude.Classes]
Monad_Result [instance, in Tableaux.Checker]
MSetAVLCompat [module, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.diff_spec' [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.Empty_eq_empty [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.empty_spec' [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.eqb [instance, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.equal_eq [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.ext [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.in_dec [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.set_equal_is_eq [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.set_equal_eq [axiom, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.singleton_spec' [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.subsetb_spec [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XDec [module, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XFacts [module, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd [module, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrdProps [module, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.compare [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.compare_spec [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.eq [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.eq_dec [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.eq_equiv [lemma, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.lt [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.lt_compat [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.lt_strorder [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.t [definition, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XProps [module, in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XSet [module, in Tableaux.Prelude.SetInstances]
N
nat_set [instance, in Tableaux.Prelude.SetInstances]nat_to_string [definition, in Tableaux.Prelude.Utils]
nat_atom [instance, in Tableaux.Prelude.AtomInstances]
Neg [constructor, in Tableaux.Syntax]
neg_equiv [lemma, in Tableaux.Semantics]
neg_neg_equiv [lemma, in Tableaux.Semantics]
Node [constructor, in Tableaux.Proofs]
Node [constructor, in Tableaux.ProofInstance]
non_empty [projection, in Tableaux.Semantics]
NOrd [module, in Tableaux.Prelude.SetInstances]
NOrd.compare [definition, in Tableaux.Prelude.SetInstances]
NOrd.compare_spec [definition, in Tableaux.Prelude.SetInstances]
NOrd.eq_bool [definition, in Tableaux.Prelude.SetInstances]
NOrd.lt [definition, in Tableaux.Prelude.SetInstances]
NOrd.lt_compat [definition, in Tableaux.Prelude.SetInstances]
NOrd.lt_strorder [definition, in Tableaux.Prelude.SetInstances]
NOrd.t [definition, in Tableaux.Prelude.SetInstances]
not_subbranch_no_ext_is_branch [lemma, in Tableaux.Proofs]
no_skolem_same_interp_form [lemma, in Tableaux.Semantics]
no_skolem_same_interp_term [lemma, in Tableaux.Semantics]
NSet [module, in Tableaux.Prelude.SetInstances]
nth_error_Some' [lemma, in Tableaux.Prelude.Utils]
O
only_fv_in [definition, in Tableaux.Skolemization]only_fv_valuation_matters_in_forms [lemma, in Tableaux.Semantics]
only_fv_valuation_matters_in_terms [lemma, in Tableaux.Semantics]
Opening [record, in Tableaux.Prelude.LocallyNamelessClasses]
Opening [inductive, in Tableaux.Prelude.LocallyNamelessClasses]
OpeningSubstForms [section, in Tableaux.Syntax]
OpeningSubstForms.func [variable, in Tableaux.Syntax]
OpeningSubstForms.pred [variable, in Tableaux.Syntax]
OpeningSubstForms.set_nat [variable, in Tableaux.Syntax]
OpeningSubstForms.var [variable, in Tableaux.Syntax]
OpeningSubstTerms [section, in Tableaux.Syntax]
OpeningSubstTerms.func [variable, in Tableaux.Syntax]
OpeningSubstTerms.set_nat [variable, in Tableaux.Syntax]
OpeningSubstTerms.var [variable, in Tableaux.Syntax]
opening_form [instance, in Tableaux.Syntax]
opening_form_ [definition, in Tableaux.Syntax]
opening_term [instance, in Tableaux.Syntax]
option_get [definition, in Tableaux.Prelude.Utils]
option_Monad [instance, in Tableaux.Prelude.Utils]
Or [constructor, in Tableaux.Syntax]
OrderedForm [module, in Tableaux.SyntaxInstance]
OrderedForm.compare [definition, in Tableaux.SyntaxInstance]
OrderedForm.compare_spec [lemma, in Tableaux.SyntaxInstance]
OrderedForm.eq [definition, in Tableaux.SyntaxInstance]
OrderedForm.eq_dec [definition, in Tableaux.SyntaxInstance]
OrderedForm.eq_equiv [lemma, in Tableaux.SyntaxInstance]
OrderedForm.lt [definition, in Tableaux.SyntaxInstance]
OrderedForm.lt_compat [instance, in Tableaux.SyntaxInstance]
OrderedForm.lt_strorder [lemma, in Tableaux.SyntaxInstance]
OrderedForm.t [definition, in Tableaux.SyntaxInstance]
or_comm [lemma, in Tableaux.Semantics]
or_equiv [lemma, in Tableaux.Semantics]
OuterSkolemization [definition, in Tableaux.SkolemizationInstances]
OuterSkolemization [definition, in Tableaux.Skolemization]
OuterSkolemizationData [definition, in Tableaux.Skolemization]
OuterSkolemization_function_symbols [lemma, in Tableaux.Skolemization]
OuterSkolemization_isFunc [lemma, in Tableaux.Skolemization]
OuterSkolemization_isLocallyClosed [lemma, in Tableaux.Skolemization]
OuterSkolemization_args_vars [lemma, in Tableaux.Skolemization]
OuterSkolemization_is_sko_pred_sound [lemma, in Tableaux.Skolemization]
OuterSkolemization_is_sko_pred [definition, in Tableaux.Skolemization]
outer_drinker_proof [definition, in drinker]
outer_subst [definition, in drinker]
outer_branching_proof [definition, in branching]
P
pr [projection, in Tableaux.Checker]Pr [record, in Tableaux.Checker]
pr [constructor, in Tableaux.Checker]
Pr [inductive, in Tableaux.Checker]
Pred [constructor, in Tableaux.Syntax]
preserves_function_symbols [definition, in Tableaux.Proofs]
preserves_function_symbols_get_neg_all [lemma, in Tableaux.Checker]
preserves_function_symbols_get_all [lemma, in Tableaux.Checker]
preserves_function_symbols_get_or2 [lemma, in Tableaux.Checker]
preserves_function_symbols_get_or1 [lemma, in Tableaux.Checker]
preserves_function_symbols_get_neg_or [lemma, in Tableaux.Checker]
preserves_function_symbols_get_neg_neg [lemma, in Tableaux.Checker]
preserves_function_symbols_None [lemma, in Tableaux.Checker]
prodext [axiom, in Tableaux.Prelude.Init]
ProofCheckerAlgorithm [section, in Tableaux.Checker]
ProofCheckerAlgorithm.sko [variable, in Tableaux.Checker]
ProofInstance [library]
Proofs [library]
pr_form [instance, in Tableaux.Checker]
pr_term [instance, in Tableaux.Checker]
pr_bool [instance, in Tableaux.Checker]
pr_list [definition, in Tableaux.Prelude.Utils]
R
RealReplacementModel [section, in Tableaux.Semantics]RealReplacementModel.f [variable, in Tableaux.Semantics]
RealReplacementModel.F [variable, in Tableaux.Semantics]
RealReplacementModel.Form [variable, in Tableaux.Semantics]
RealReplacementModel.func [variable, in Tableaux.Semantics]
RealReplacementModel.M [variable, in Tableaux.Semantics]
RealReplacementModel.M' [variable, in Tableaux.Semantics]
RealReplacementModel.pred [variable, in Tableaux.Semantics]
RealReplacementModel.set_nat [variable, in Tableaux.Semantics]
RealReplacementModel.t [variable, in Tableaux.Semantics]
RealReplacementModel.Term [variable, in Tableaux.Semantics]
RealReplacementModel.var [variable, in Tableaux.Semantics]
RealReplacementModel.vs [variable, in Tableaux.Semantics]
record [projection, in Tableaux.Skolemization]
record_ext [projection, in Tableaux.Skolemization]
record_eqb [projection, in Tableaux.Skolemization]
reflexive_subset [instance, in Tableaux.Prelude.Sets]
rem [definition, in Tableaux.Prelude.Sets]
removelast_nth_error [lemma, in Tableaux.Prelude.Utils]
removelast_length [lemma, in Tableaux.Prelude.Utils]
rem_spec3 [lemma, in Tableaux.Prelude.Sets]
rem_spec2 [lemma, in Tableaux.Prelude.Sets]
rem_spec1 [lemma, in Tableaux.Prelude.Sets]
ReplaceInterpFunc [section, in Tableaux.Semantics]
ReplaceInterpFunc.f [variable, in Tableaux.Semantics]
ReplaceInterpFunc.F [variable, in Tableaux.Semantics]
ReplaceInterpFunc.func [variable, in Tableaux.Semantics]
ReplaceInterpFunc.M [variable, in Tableaux.Semantics]
ReplaceInterpFunc.pred [variable, in Tableaux.Semantics]
ReplaceInterpFunc.var [variable, in Tableaux.Semantics]
ReplaceInterpFunc.vs [variable, in Tableaux.Semantics]
ReplacementModel [definition, in Tableaux.Semantics]
replace_expanded_child_not_subbranch [lemma, in Tableaux.Proofs]
replace_expanded_child_not_branch_Right [lemma, in Tableaux.Proofs]
replace_expanded_child_not_branch_Left [lemma, in Tableaux.Proofs]
replace_child_Node [lemma, in Tableaux.Proofs]
replace_child_sequence_expand [lemma, in Tableaux.Proofs]
replace_expand_Left [lemma, in Tableaux.Proofs]
replace_child_get_child_at [lemma, in Tableaux.Proofs]
replace_child [definition, in Tableaux.Proofs]
replace_nth_replace_nth [lemma, in Tableaux.Prelude.Utils]
replace_nth_Some [lemma, in Tableaux.Prelude.Utils]
replace_nth [definition, in Tableaux.Prelude.Utils]
replace_in_list [definition, in Tableaux.Prelude.Utils]
replace_interp_func [definition, in Tableaux.Semantics]
result [definition, in Tableaux.Checker]
Result [definition, in Tableaux.Checker]
ret [projection, in Tableaux.Prelude.Classes]
Right [constructor, in Tableaux.Proofs]
Rule [inductive, in Tableaux.ProofInstance]
RulesSoundness [section, in Tableaux.Checker]
RulesSoundness.sko [variable, in Tableaux.Checker]
RuleTree [inductive, in Tableaux.ProofInstance]
RuleTreeToSequence [section, in Tableaux.Checker]
RuleTreeToSequence_Lemmas2.Tableau [variable, in Tableaux.Checker]
RuleTreeToSequence_Lemmas2.sko [variable, in Tableaux.Checker]
RuleTreeToSequence_Lemmas2 [section, in Tableaux.Checker]
RuleTreeToSequence_Lemmas.Tableau [variable, in Tableaux.Checker]
RuleTreeToSequence_Lemmas.sko [variable, in Tableaux.Checker]
RuleTreeToSequence_Lemmas [section, in Tableaux.Checker]
RuleTreeToSequence.sko [variable, in Tableaux.Checker]
RuleTreeToSequence.Tableau [variable, in Tableaux.Checker]
RuleTree_to_Sequence_preserves_function_symbols_last [lemma, in Tableaux.Checker]
RuleTree_to_Sequence_snd_expansion [lemma, in Tableaux.Checker]
RuleTree_to_Sequence_symbols [lemma, in Tableaux.Checker]
RuleTree_to_Sequence [definition, in Tableaux.Checker]
RuleTree_to_Sequence_branch [lemma, in Tableaux.Checker]
RuleTree_to_Sequence_hd [lemma, in Tableaux.Checker]
RuleTree_to_Sequence_not_nil [lemma, in Tableaux.Checker]
RuleTree_to_Sequence__aux [definition, in Tableaux.Checker]
RuleTree_sind [definition, in Tableaux.ProofInstance]
RuleTree_rec [definition, in Tableaux.ProofInstance]
RuleTree_ind [definition, in Tableaux.ProofInstance]
RuleTree_rect [definition, in Tableaux.ProofInstance]
rule_wrapper_sound [lemma, in Tableaux.Checker]
rule_wrapper [definition, in Tableaux.Checker]
Rule_sind [definition, in Tableaux.ProofInstance]
Rule_rec [definition, in Tableaux.ProofInstance]
Rule_ind [definition, in Tableaux.ProofInstance]
Rule_rect [definition, in Tableaux.ProofInstance]
S
satisfiable_tableau_satisfiable_expansion_sequence [lemma, in Tableaux.Proofs]satisfiable_expansion_satisfiable [lemma, in Tableaux.Proofs]
satisfies_opening_with_sko [lemma, in Tableaux.Semantics]
satisfying_symbol_prop [lemma, in Tableaux.Semantics]
satisfying_symbol [definition, in Tableaux.Semantics]
satisfy_delta [lemma, in Tableaux.Semantics]
Semantics [library]
SemanticsDef [section, in Tableaux.Semantics]
SemanticsDef.func [variable, in Tableaux.Semantics]
SemanticsDef.pred [variable, in Tableaux.Semantics]
SemanticsDef.var [variable, in Tableaux.Semantics]
SemanticsFacts [section, in Tableaux.Semantics]
SemanticsFacts.Form [variable, in Tableaux.Semantics]
SemanticsFacts.func [variable, in Tableaux.Semantics]
SemanticsFacts.pred [variable, in Tableaux.Semantics]
SemanticsFacts.set_nat [variable, in Tableaux.Semantics]
SemanticsFacts.Term [variable, in Tableaux.Semantics]
SemanticsFacts.var [variable, in Tableaux.Semantics]
Sequence [definition, in Tableaux.Proofs]
set [record, in Tableaux.Prelude.Sets]
SetInstances [library]
SetProperties [section, in Tableaux.Prelude.Sets]
SetProperties.A [variable, in Tableaux.Prelude.Sets]
SetProperties.set_A [variable, in Tableaux.Prelude.Sets]
Sets [library]
set_atom [projection, in Tableaux.Prelude.Atoms]
set_fold_left [lemma, in Tableaux.Prelude.Sets]
set_in_dec [projection, in Tableaux.Prelude.Sets]
set_ext [projection, in Tableaux.Prelude.Sets]
set_in [projection, in Tableaux.Prelude.Sets]
set_eqb [projection, in Tableaux.Prelude.Sets]
SimpleOrderedType [module, in Tableaux.Prelude.SetInstances]
SimpleOrderedType.compare [axiom, in Tableaux.Prelude.SetInstances]
SimpleOrderedType.compare_spec [axiom, in Tableaux.Prelude.SetInstances]
SimpleOrderedType.eq_bool [axiom, in Tableaux.Prelude.SetInstances]
SimpleOrderedType.lt [axiom, in Tableaux.Prelude.SetInstances]
SimpleOrderedType.lt_compat [axiom, in Tableaux.Prelude.SetInstances]
SimpleOrderedType.lt_strorder [axiom, in Tableaux.Prelude.SetInstances]
SimpleOrderedType.t [axiom, in Tableaux.Prelude.SetInstances]
singleton [projection, in Tableaux.Prelude.Sets]
singleton_spec1 [lemma, in Tableaux.Prelude.Sets]
singleton_spec [projection, in Tableaux.Prelude.Sets]
single_to_set [projection, in Tableaux.Skolemization]
single_spec [projection, in Tableaux.Skolemization]
single_record [projection, in Tableaux.Skolemization]
skoData [projection, in Tableaux.Skolemization]
SkoDefs [section, in Tableaux.Skolemization]
SkoDefs.Form [variable, in Tableaux.Skolemization]
SkoDefs.func [variable, in Tableaux.Skolemization]
SkoDefs.pred [variable, in Tableaux.Skolemization]
SkoDefs.set_func [variable, in Tableaux.Skolemization]
SkoDefs.set_var [variable, in Tableaux.Skolemization]
SkoDefs.sko [variable, in Tableaux.Skolemization]
SkoDefs.Term [variable, in Tableaux.Skolemization]
SkoDefs.var [variable, in Tableaux.Skolemization]
Skolemization [definition, in Tableaux.SkolemizationInstances]
Skolemization [library]
SkolemizationData [record, in Tableaux.Skolemization]
SkolemizationDef [section, in Tableaux.Skolemization]
SkolemizationDef.Ctx [variable, in Tableaux.Skolemization]
SkolemizationDef.Form [variable, in Tableaux.Skolemization]
SkolemizationDef.func [variable, in Tableaux.Skolemization]
SkolemizationDef.pred [variable, in Tableaux.Skolemization]
SkolemizationDef.set_func [variable, in Tableaux.Skolemization]
SkolemizationDef.set_var [variable, in Tableaux.Skolemization]
SkolemizationDef.SkoRecord [section, in Tableaux.Skolemization]
SkolemizationDef.SkoRecord.SkoRecordDataDefs [section, in Tableaux.Skolemization]
SkolemizationDef.SkoRecord.SkoRecordDataDefs.RecordData [variable, in Tableaux.Skolemization]
SkolemizationDef.Term [variable, in Tableaux.Skolemization]
SkolemizationDef.var [variable, in Tableaux.Skolemization]
SkolemizationInstances [section, in Tableaux.Skolemization]
SkolemizationInstances [library]
SkolemizationInstances.Ctx [variable, in Tableaux.Skolemization]
SkolemizationInstances.Form [variable, in Tableaux.Skolemization]
SkolemizationInstances.func [variable, in Tableaux.Skolemization]
SkolemizationInstances.pred [variable, in Tableaux.Skolemization]
SkolemizationInstances.set_func [variable, in Tableaux.Skolemization]
SkolemizationInstances.set_var [variable, in Tableaux.Skolemization]
SkolemizationInstances.set_nat [variable, in Tableaux.Skolemization]
SkolemizationInstances.Term [variable, in Tableaux.Skolemization]
SkolemizationInstances.var [variable, in Tableaux.Skolemization]
Skolemization_ [record, in Tableaux.Skolemization]
SkoRecord [record, in Tableaux.Skolemization]
SkoRecordData [record, in Tableaux.Skolemization]
SkoRecordData_set [definition, in Tableaux.Skolemization]
SkoRecordSpecs [record, in Tableaux.Skolemization]
SkoRecordSpecs_set [lemma, in Tableaux.Skolemization]
SkoSymbolLemmas [section, in Tableaux.Skolemization]
SkoSymbolLemmas.Form [variable, in Tableaux.Skolemization]
SkoSymbolLemmas.func [variable, in Tableaux.Skolemization]
SkoSymbolLemmas.pred [variable, in Tableaux.Skolemization]
SkoSymbolLemmas.record [variable, in Tableaux.Skolemization]
SkoSymbolLemmas.Term [variable, in Tableaux.Skolemization]
SkoSymbolLemmas.var [variable, in Tableaux.Skolemization]
SkoWrapper_args [definition, in Tableaux.Skolemization]
SkoWrapper_symbol [definition, in Tableaux.Skolemization]
SkoWrapper_is_sko [definition, in Tableaux.Skolemization]
sko_record_set [definition, in Tableaux.Skolemization]
sko_function_symbols_sound [lemma, in Tableaux.Skolemization]
sko_function_symbols_args [lemma, in Tableaux.Skolemization]
sko_record [projection, in Tableaux.Skolemization]
SOrd [module, in Tableaux.Prelude.SetInstances]
SOrd.compare [definition, in Tableaux.Prelude.SetInstances]
SOrd.compare_spec [lemma, in Tableaux.Prelude.SetInstances]
SOrd.eq_bool [definition, in Tableaux.Prelude.SetInstances]
SOrd.lt [definition, in Tableaux.Prelude.SetInstances]
SOrd.lt_compat [definition, in Tableaux.Prelude.SetInstances]
SOrd.lt_strorder [lemma, in Tableaux.Prelude.SetInstances]
SOrd.t [definition, in Tableaux.Prelude.SetInstances]
Soundness [section, in Tableaux.Proofs]
Soundness [section, in Tableaux.Checker]
Soundness.Form [variable, in Tableaux.Proofs]
Soundness.func [variable, in Tableaux.Proofs]
Soundness.pred [variable, in Tableaux.Proofs]
Soundness.set_nat [variable, in Tableaux.Proofs]
Soundness.sko [variable, in Tableaux.Proofs]
Soundness.sko [variable, in Tableaux.Checker]
Soundness.Tableau [variable, in Tableaux.Proofs]
Soundness.Tableau [variable, in Tableaux.Checker]
Soundness.Term [variable, in Tableaux.Proofs]
Soundness.var [variable, in Tableaux.Proofs]
specs [projection, in Tableaux.Skolemization]
SSet [module, in Tableaux.Prelude.SetInstances]
status [projection, in Tableaux.Checker]
StringLemmas [section, in Tableaux.Prelude.Utils]
string_set [instance, in Tableaux.Prelude.SetInstances]
string_atom [instance, in Tableaux.Prelude.AtomInstances]
subset [definition, in Tableaux.Prelude.Sets]
subsetb [projection, in Tableaux.Prelude.Sets]
subsetb_spec [projection, in Tableaux.Prelude.Sets]
subst [definition, in branching]
Subst [record, in Tableaux.Prelude.LocallyNamelessClasses]
Subst [inductive, in Tableaux.Prelude.LocallyNamelessClasses]
subst [projection, in Tableaux.Prelude.LocallyNamelessClasses]
SubstInstances [section, in Tableaux.Prelude.LocallyNamelessClasses]
SubstInstances.set_nat [variable, in Tableaux.Prelude.LocallyNamelessClasses]
substitute [projection, in Tableaux.Prelude.LocallyNamelessClasses]
substitute [constructor, in Tableaux.Prelude.LocallyNamelessClasses]
Substitution [record, in Tableaux.Prelude.LocallyNamelessClasses]
Substitution [section, in Tableaux.Prelude.LocallyNamelessClasses]
Substitution.set_nat [variable, in Tableaux.Prelude.LocallyNamelessClasses]
SubstOpeningLemmas [section, in Tableaux.Syntax]
SubstOpeningLemmas.Form [variable, in Tableaux.Syntax]
SubstOpeningLemmas.func [variable, in Tableaux.Syntax]
SubstOpeningLemmas.pred [variable, in Tableaux.Syntax]
SubstOpeningLemmas.set_nat [variable, in Tableaux.Syntax]
SubstOpeningLemmas.Term [variable, in Tableaux.Syntax]
SubstOpeningLemmas.var [variable, in Tableaux.Syntax]
subst_form [instance, in Tableaux.Syntax]
subst_term [instance, in Tableaux.Syntax]
subst_translation [definition, in Tableaux.ExtendedSyntax]
subst_list [instance, in Tableaux.Prelude.LocallyNamelessClasses]
subst_commutes_with_env_forms [lemma, in Tableaux.Semantics]
subst_commutes_with_env_terms [lemma, in Tableaux.Semantics]
subst_to_env [definition, in Tableaux.Semantics]
subterm_not_subterm_not_subterm [lemma, in Tableaux.Syntax]
symbol [projection, in Tableaux.Skolemization]
symbols [projection, in Tableaux.Proofs]
symbol_sound [lemma, in Tableaux.Skolemization]
symbs [projection, in Tableaux.Checker]
Syntax [library]
SyntaxInstance [library]
T
Tableau [record, in Tableaux.Proofs]Tableau [definition, in Tableaux.ProofInstance]
TableauTree [inductive, in Tableaux.Proofs]
TableauTree_sind [definition, in Tableaux.Proofs]
TableauTree_rec [definition, in Tableaux.Proofs]
TableauTree_ind [definition, in Tableaux.Proofs]
TableauTree_rect [definition, in Tableaux.Proofs]
Tableaux [section, in Tableaux.Proofs]
Tableaux.Form [variable, in Tableaux.Proofs]
Tableaux.func [variable, in Tableaux.Proofs]
Tableaux.pred [variable, in Tableaux.Proofs]
Tableaux.set_nat [variable, in Tableaux.Proofs]
Tableaux.sko [variable, in Tableaux.Proofs]
Tableaux.var [variable, in Tableaux.Proofs]
Term [inductive, in Tableaux.Syntax]
Term [definition, in Tableaux.SyntaxInstance]
TermInd [section, in Tableaux.Syntax]
TermInd.func [variable, in Tableaux.Syntax]
TermInd.var [variable, in Tableaux.Syntax]
term_subst_opening [lemma, in Tableaux.Syntax]
term_locally_closed_inst [lemma, in Tableaux.Syntax]
term_ind' [definition, in Tableaux.Syntax]
term_rect' [definition, in Tableaux.Syntax]
term_ind [definition, in Tableaux.Syntax]
term_rect [definition, in Tableaux.Syntax]
Term_sind [definition, in Tableaux.Syntax]
Term_rec [definition, in Tableaux.Syntax]
Term_ind [definition, in Tableaux.Syntax]
Term_rect [definition, in Tableaux.Syntax]
term_env_inst_commutes [lemma, in Tableaux.Semantics]
to_set [projection, in Tableaux.Skolemization]
to_form_list [definition, in Tableaux.ExtendedSyntax]
transitive_subset [instance, in Tableaux.Prelude.Sets]
translate [projection, in Tableaux.ExtendedSyntax]
translate [constructor, in Tableaux.ExtendedSyntax]
TranslateSubst [section, in Tableaux.ExtendedSyntax]
translate_substitution [definition, in Tableaux.ExtendedSyntax]
translate_list [instance, in Tableaux.ExtendedSyntax]
translate_EForm [definition, in Tableaux.ExtendedSyntax]
translate_EForm_aux [definition, in Tableaux.ExtendedSyntax]
translate_ETerm [definition, in Tableaux.ExtendedSyntax]
translation_equivalidity [lemma, in Tableaux.ExtendedSyntax]
tree [projection, in Tableaux.Proofs]
TreeTactics [module, in Tableaux.Proofs]
trivial_pred_is_eq_for_unit [lemma, in Tableaux.Prelude.Classes]
trivial_contradiction_sound [lemma, in Tableaux.Checker]
trivial_contradiction [definition, in Tableaux.Checker]
U
union [projection, in Tableaux.Prelude.Sets]union_comm [lemma, in Tableaux.Prelude.Sets]
union_assoc [lemma, in Tableaux.Prelude.Sets]
union_sym [lemma, in Tableaux.Prelude.Sets]
union_idemp [lemma, in Tableaux.Prelude.Sets]
union_congr [lemma, in Tableaux.Prelude.Sets]
union_congl [lemma, in Tableaux.Prelude.Sets]
union_spec [projection, in Tableaux.Prelude.Sets]
Unnamed_thm [definition, in drinker]
Utils [library]
V
ValidityEquivalence [section, in Tableaux.ExtendedSyntax]ValidityEquivalence.ExtendedEnvironment [section, in Tableaux.ExtendedSyntax]
ValidityEquivalence.ExtendedEnvironment.bvs [variable, in Tableaux.ExtendedSyntax]
ValidityEquivalence.ExtendedEnvironment.M [variable, in Tableaux.ExtendedSyntax]
ValidityEquivalence.ExtendedEnvironment.rho [variable, in Tableaux.ExtendedSyntax]
ValidityEquivalence.ExtendedEnvironment.sigma [variable, in Tableaux.ExtendedSyntax]
ValidityEquivalence.GenTranslationEquivalidity [section, in Tableaux.ExtendedSyntax]
value_record_spec1 [projection, in Tableaux.Skolemization]
value_record [projection, in Tableaux.Skolemization]
varOpening [projection, in Tableaux.Prelude.LocallyNamelessClasses]
varOpening [constructor, in Tableaux.Prelude.LocallyNamelessClasses]
other
_ <- _ ; _ [notation, in Tableaux.Prelude.Classes]_ >>= _ [notation, in Tableaux.Prelude.Classes]
_ == _ [notation, in Tableaux.Prelude.Classes]
_ |> _ [notation, in Tableaux.Proofs]
_ \in _ [notation, in Tableaux.Proofs]
_ @[ _ ] [notation, in Tableaux.Prelude.LocallyNamelessClasses]
_ { _ \to _ } [notation, in Tableaux.Prelude.LocallyNamelessClasses]
_ \subseteq _ [notation, in Tableaux.Prelude.Sets]
_ \inter _ [notation, in Tableaux.Prelude.Sets]
_ \union _ [notation, in Tableaux.Prelude.Sets]
_ .( _ ) [notation, in Tableaux.Prelude.Init]
_ |= _ [notation, in Tableaux.Semantics]
_ \equiv _ [notation, in Tableaux.Semantics]
#| _ | [notation, in Tableaux.Prelude.Init]
[[ _ ]] [notation, in Tableaux.ExtendedSyntax]
[[ _ # _ # _ '|= _ ]] [notation, in Tableaux.Semantics]
\{ _ , _ , .. , _ \} [notation, in Tableaux.Prelude.Sets]
\{ _ \} [notation, in Tableaux.Prelude.Sets]
\{ \} [notation, in Tableaux.Prelude.Sets]
|= _ [notation, in Tableaux.Semantics]
Notation Index
E
_ |> _ [in Tableaux.Proofs]_ '<=> _ [in Tableaux.ExtendedSyntax]
_ '=> _ [in Tableaux.ExtendedSyntax]
_ '&& _ [in Tableaux.ExtendedSyntax]
_ '|| _ [in Tableaux.ExtendedSyntax]
_ ''( _ ,, _ ,, .. ,, _ ) [in Tableaux.ExtendedSyntax]
_ ''( _ ) [in Tableaux.ExtendedSyntax]
_ ''() [in Tableaux.ExtendedSyntax]
_ '( _ ,, _ ,, .. ,, _ ) [in Tableaux.ExtendedSyntax]
_ '( _ ) [in Tableaux.ExtendedSyntax]
_ '() [in Tableaux.ExtendedSyntax]
'Bot [in Tableaux.ExtendedSyntax]
'Top [in Tableaux.ExtendedSyntax]
'! _ :( _ ) [in Tableaux.ExtendedSyntax]
' _ [in Tableaux.ExtendedSyntax]
'? _ :( _ ) [in Tableaux.ExtendedSyntax]
'~ _ [in Tableaux.ExtendedSyntax]
other
_ <- _ ; _ [in Tableaux.Prelude.Classes]_ >>= _ [in Tableaux.Prelude.Classes]
_ == _ [in Tableaux.Prelude.Classes]
_ |> _ [in Tableaux.Proofs]
_ \in _ [in Tableaux.Proofs]
_ @[ _ ] [in Tableaux.Prelude.LocallyNamelessClasses]
_ { _ \to _ } [in Tableaux.Prelude.LocallyNamelessClasses]
_ \subseteq _ [in Tableaux.Prelude.Sets]
_ \inter _ [in Tableaux.Prelude.Sets]
_ \union _ [in Tableaux.Prelude.Sets]
_ .( _ ) [in Tableaux.Prelude.Init]
_ |= _ [in Tableaux.Semantics]
_ \equiv _ [in Tableaux.Semantics]
#| _ | [in Tableaux.Prelude.Init]
[[ _ ]] [in Tableaux.ExtendedSyntax]
[[ _ # _ # _ '|= _ ]] [in Tableaux.Semantics]
\{ _ , _ , .. , _ \} [in Tableaux.Prelude.Sets]
\{ _ \} [in Tableaux.Prelude.Sets]
\{ \} [in Tableaux.Prelude.Sets]
|= _ [in Tableaux.Semantics]
Module Index
C
Ctx [in Tableaux.Checker]E
ExtendedSyntax [in Tableaux.Checker]ExtendedSyntaxNotation [in Tableaux.ExtendedSyntax]
ExtendedSyntax.E [in Tableaux.Checker]
F
FSet [in Tableaux.SyntaxInstance]M
MSetAVLCompat [in Tableaux.Prelude.SetInstances]MSetAVLCompat.XDec [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XFacts [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrdProps [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XProps [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XSet [in Tableaux.Prelude.SetInstances]
N
NOrd [in Tableaux.Prelude.SetInstances]NSet [in Tableaux.Prelude.SetInstances]
O
OrderedForm [in Tableaux.SyntaxInstance]S
SimpleOrderedType [in Tableaux.Prelude.SetInstances]SOrd [in Tableaux.Prelude.SetInstances]
SSet [in Tableaux.Prelude.SetInstances]
T
TreeTactics [in Tableaux.Proofs]Variable Index
B
BVInstances.set_nat [in Tableaux.Prelude.LocallyNamelessClasses]D
DecEqForms.func [in Tableaux.Syntax]DecEqForms.pred [in Tableaux.Syntax]
DecEqForms.var [in Tableaux.Syntax]
DecEqTerms.func [in Tableaux.Syntax]
DecEqTerms.Term [in Tableaux.Syntax]
DecEqTerms.var [in Tableaux.Syntax]
E
EqDecOtherInstances.A [in Tableaux.Prelude.Classes]EquivEqBoolEqDec.A [in Tableaux.Prelude.Classes]
EquivForallIn.A [in Tableaux.Prelude.Ind]
EquivForallIn.P [in Tableaux.Prelude.Ind]
ESyntaxTranslation.ClosedIn.Container [in Tableaux.ExtendedSyntax]
ESyntaxTranslation.ClosedIn.mem [in Tableaux.ExtendedSyntax]
ESyntaxTranslation.IndexOf.A [in Tableaux.ExtendedSyntax]
ExpansionRules.Form [in Tableaux.Proofs]
ExpansionRules.func [in Tableaux.Proofs]
ExpansionRules.pred [in Tableaux.Proofs]
ExpansionRules.set_nat [in Tableaux.Proofs]
ExpansionRules.sko [in Tableaux.Proofs]
ExpansionRules.Tableau [in Tableaux.Proofs]
ExpansionRules.Term [in Tableaux.Proofs]
ExpansionRules.var [in Tableaux.Proofs]
F
FreeVariables.set_var [in Tableaux.Prelude.LocallyNamelessClasses]FreeVariables.var [in Tableaux.Prelude.LocallyNamelessClasses]
FunctionSymbols.Form [in Tableaux.Syntax]
FunctionSymbols.func [in Tableaux.Syntax]
FunctionSymbols.pred [in Tableaux.Syntax]
FunctionSymbols.Term [in Tableaux.Syntax]
FunctionSymbols.var [in Tableaux.Syntax]
FVForms.func [in Tableaux.Syntax]
FVForms.pred [in Tableaux.Syntax]
FVForms.set_var [in Tableaux.Syntax]
FVForms.var [in Tableaux.Syntax]
FVInstances.set_var [in Tableaux.Prelude.LocallyNamelessClasses]
FVInstances.var [in Tableaux.Prelude.LocallyNamelessClasses]
FVTerms.func [in Tableaux.Syntax]
FVTerms.set_var [in Tableaux.Syntax]
FVTerms.var [in Tableaux.Syntax]
I
isClosedLemmas.Form [in Tableaux.Syntax]isClosedLemmas.func [in Tableaux.Syntax]
isClosedLemmas.pred [in Tableaux.Syntax]
isClosedLemmas.set_nat [in Tableaux.Syntax]
isClosedLemmas.Term [in Tableaux.Syntax]
isClosedLemmas.var [in Tableaux.Syntax]
O
OpeningSubstForms.func [in Tableaux.Syntax]OpeningSubstForms.pred [in Tableaux.Syntax]
OpeningSubstForms.set_nat [in Tableaux.Syntax]
OpeningSubstForms.var [in Tableaux.Syntax]
OpeningSubstTerms.func [in Tableaux.Syntax]
OpeningSubstTerms.set_nat [in Tableaux.Syntax]
OpeningSubstTerms.var [in Tableaux.Syntax]
P
ProofCheckerAlgorithm.sko [in Tableaux.Checker]R
RealReplacementModel.f [in Tableaux.Semantics]RealReplacementModel.F [in Tableaux.Semantics]
RealReplacementModel.Form [in Tableaux.Semantics]
RealReplacementModel.func [in Tableaux.Semantics]
RealReplacementModel.M [in Tableaux.Semantics]
RealReplacementModel.M' [in Tableaux.Semantics]
RealReplacementModel.pred [in Tableaux.Semantics]
RealReplacementModel.set_nat [in Tableaux.Semantics]
RealReplacementModel.t [in Tableaux.Semantics]
RealReplacementModel.Term [in Tableaux.Semantics]
RealReplacementModel.var [in Tableaux.Semantics]
RealReplacementModel.vs [in Tableaux.Semantics]
ReplaceInterpFunc.f [in Tableaux.Semantics]
ReplaceInterpFunc.F [in Tableaux.Semantics]
ReplaceInterpFunc.func [in Tableaux.Semantics]
ReplaceInterpFunc.M [in Tableaux.Semantics]
ReplaceInterpFunc.pred [in Tableaux.Semantics]
ReplaceInterpFunc.var [in Tableaux.Semantics]
ReplaceInterpFunc.vs [in Tableaux.Semantics]
RulesSoundness.sko [in Tableaux.Checker]
RuleTreeToSequence_Lemmas2.Tableau [in Tableaux.Checker]
RuleTreeToSequence_Lemmas2.sko [in Tableaux.Checker]
RuleTreeToSequence_Lemmas.Tableau [in Tableaux.Checker]
RuleTreeToSequence_Lemmas.sko [in Tableaux.Checker]
RuleTreeToSequence.sko [in Tableaux.Checker]
RuleTreeToSequence.Tableau [in Tableaux.Checker]
S
SemanticsDef.func [in Tableaux.Semantics]SemanticsDef.pred [in Tableaux.Semantics]
SemanticsDef.var [in Tableaux.Semantics]
SemanticsFacts.Form [in Tableaux.Semantics]
SemanticsFacts.func [in Tableaux.Semantics]
SemanticsFacts.pred [in Tableaux.Semantics]
SemanticsFacts.set_nat [in Tableaux.Semantics]
SemanticsFacts.Term [in Tableaux.Semantics]
SemanticsFacts.var [in Tableaux.Semantics]
SetProperties.A [in Tableaux.Prelude.Sets]
SetProperties.set_A [in Tableaux.Prelude.Sets]
SkoDefs.Form [in Tableaux.Skolemization]
SkoDefs.func [in Tableaux.Skolemization]
SkoDefs.pred [in Tableaux.Skolemization]
SkoDefs.set_func [in Tableaux.Skolemization]
SkoDefs.set_var [in Tableaux.Skolemization]
SkoDefs.sko [in Tableaux.Skolemization]
SkoDefs.Term [in Tableaux.Skolemization]
SkoDefs.var [in Tableaux.Skolemization]
SkolemizationDef.Ctx [in Tableaux.Skolemization]
SkolemizationDef.Form [in Tableaux.Skolemization]
SkolemizationDef.func [in Tableaux.Skolemization]
SkolemizationDef.pred [in Tableaux.Skolemization]
SkolemizationDef.set_func [in Tableaux.Skolemization]
SkolemizationDef.set_var [in Tableaux.Skolemization]
SkolemizationDef.SkoRecord.SkoRecordDataDefs.RecordData [in Tableaux.Skolemization]
SkolemizationDef.Term [in Tableaux.Skolemization]
SkolemizationDef.var [in Tableaux.Skolemization]
SkolemizationInstances.Ctx [in Tableaux.Skolemization]
SkolemizationInstances.Form [in Tableaux.Skolemization]
SkolemizationInstances.func [in Tableaux.Skolemization]
SkolemizationInstances.pred [in Tableaux.Skolemization]
SkolemizationInstances.set_func [in Tableaux.Skolemization]
SkolemizationInstances.set_var [in Tableaux.Skolemization]
SkolemizationInstances.set_nat [in Tableaux.Skolemization]
SkolemizationInstances.Term [in Tableaux.Skolemization]
SkolemizationInstances.var [in Tableaux.Skolemization]
SkoSymbolLemmas.Form [in Tableaux.Skolemization]
SkoSymbolLemmas.func [in Tableaux.Skolemization]
SkoSymbolLemmas.pred [in Tableaux.Skolemization]
SkoSymbolLemmas.record [in Tableaux.Skolemization]
SkoSymbolLemmas.Term [in Tableaux.Skolemization]
SkoSymbolLemmas.var [in Tableaux.Skolemization]
Soundness.Form [in Tableaux.Proofs]
Soundness.func [in Tableaux.Proofs]
Soundness.pred [in Tableaux.Proofs]
Soundness.set_nat [in Tableaux.Proofs]
Soundness.sko [in Tableaux.Proofs]
Soundness.sko [in Tableaux.Checker]
Soundness.Tableau [in Tableaux.Proofs]
Soundness.Tableau [in Tableaux.Checker]
Soundness.Term [in Tableaux.Proofs]
Soundness.var [in Tableaux.Proofs]
SubstInstances.set_nat [in Tableaux.Prelude.LocallyNamelessClasses]
Substitution.set_nat [in Tableaux.Prelude.LocallyNamelessClasses]
SubstOpeningLemmas.Form [in Tableaux.Syntax]
SubstOpeningLemmas.func [in Tableaux.Syntax]
SubstOpeningLemmas.pred [in Tableaux.Syntax]
SubstOpeningLemmas.set_nat [in Tableaux.Syntax]
SubstOpeningLemmas.Term [in Tableaux.Syntax]
SubstOpeningLemmas.var [in Tableaux.Syntax]
T
Tableaux.Form [in Tableaux.Proofs]Tableaux.func [in Tableaux.Proofs]
Tableaux.pred [in Tableaux.Proofs]
Tableaux.set_nat [in Tableaux.Proofs]
Tableaux.sko [in Tableaux.Proofs]
Tableaux.var [in Tableaux.Proofs]
TermInd.func [in Tableaux.Syntax]
TermInd.var [in Tableaux.Syntax]
V
ValidityEquivalence.ExtendedEnvironment.bvs [in Tableaux.ExtendedSyntax]ValidityEquivalence.ExtendedEnvironment.M [in Tableaux.ExtendedSyntax]
ValidityEquivalence.ExtendedEnvironment.rho [in Tableaux.ExtendedSyntax]
ValidityEquivalence.ExtendedEnvironment.sigma [in Tableaux.ExtendedSyntax]
Library Index
A
AllAll
AtomInstances
Atoms
B
branchingC
CheckerClasses
Core
Core
D
drinkerE
ExtendedSyntaxExtraction
I
IndInit
L
LocallyNamelessClassesP
ProofInstanceProofs
S
SemanticsSetInstances
Sets
Skolemization
SkolemizationInstances
Syntax
SyntaxInstance
U
UtilsLemma Index
A
add_rem [in Tableaux.Prelude.Sets]add_inv [in Tableaux.Prelude.Sets]
add_spec2 [in Tableaux.Prelude.Sets]
add_spec1 [in Tableaux.Prelude.Sets]
alpha_rule_sound [in Tableaux.Checker]
B
beta_rule_sound [in Tableaux.Checker]branch_extend_left_right [in Tableaux.Proofs]
C
carrier_eq_dec [in Tableaux.Prelude.Sets]CheckProof_sound [in Tableaux.Checker]
CheckProof_Some_Sequence_closed [in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_closed [in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_is_expansion_sequence [in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_Some [in Tableaux.Checker]
CheckProof_Some_RuleTree_to_Sequence_Some__aux [in Tableaux.Checker]
closed_in_union_closed_in_right [in Tableaux.ExtendedSyntax]
closed_in_union_closed_in_left [in Tableaux.ExtendedSyntax]
closed_in_translate_ETerm [in Tableaux.ExtendedSyntax]
closed_in_nil [in Tableaux.ExtendedSyntax]
Ctx.existsb_exists [in Tableaux.Checker]
Ctx.mem_spec [in Tableaux.Checker]
D
delta_rule_sound [in Tableaux.Checker]disjoint_sym [in Tableaux.Prelude.Sets]
disjoint_are_disjoint [in Tableaux.Prelude.Sets]
E
empty_disjointr [in Tableaux.Prelude.Sets]empty_disjointl [in Tableaux.Prelude.Sets]
empty_unitr [in Tableaux.Prelude.Sets]
empty_unitl [in Tableaux.Prelude.Sets]
empty_is_empty [in Tableaux.Prelude.Sets]
EqBool_neq [in Tableaux.Prelude.Classes]
EqBool_refl [in Tableaux.Prelude.Classes]
eqb_from_eqDec_is_eq [in Tableaux.Prelude.Classes]
eqb_form_eq [in Tableaux.Syntax]
eqb_term_eq [in Tableaux.Syntax]
eqb_list_is_eq [in Tableaux.Prelude.Utils]
EqDec_refl [in Tableaux.Prelude.Classes]
EqDec_UIP [in Tableaux.Prelude.Classes]
equiv_imply [in Tableaux.Semantics]
eterm_translation_is_always_locally_closed [in Tableaux.ExtendedSyntax]
expand_tableau_branch_Some_symbs [in Tableaux.Proofs]
expand_tableau_branch_Some__aux [in Tableaux.Proofs]
expand_tableau_branch_right [in Tableaux.Proofs]
expand_tableau_branch_left [in Tableaux.Proofs]
expand_tableau_branch_Some_is_branch_of [in Tableaux.Proofs]
explosion_principle [in Tableaux.Semantics]
ExtendedSyntax.Extended_CheckProof_sound [in Tableaux.Checker]
extended_environment_comp_Some [in Tableaux.ExtendedSyntax]
extended_environment_comp_None [in Tableaux.ExtendedSyntax]
extend_subset_preserves_function_symbols [in Tableaux.Proofs]
extend_function_symbols_value [in Tableaux.Proofs]
extend_extended_environment [in Tableaux.ExtendedSyntax]
extend_with_imply_form [in Tableaux.Semantics]
extend_with_equiv_form [in Tableaux.Semantics]
F
forallb2_refl [in Tableaux.Prelude.Utils]forallb2_eq [in Tableaux.Prelude.Utils]
Forall_inv [in Tableaux.Prelude.Ind]
Forall_tail [in Tableaux.Prelude.Ind]
Forall_In [in Tableaux.Prelude.Ind]
formula_contradiction_sound [in Tableaux.Checker]
form_subst_opening [in Tableaux.Syntax]
form_env_inst_commutes [in Tableaux.Semantics]
function_symbols_opening_all_free [in Tableaux.Syntax]
function_symbols_opening_form' [in Tableaux.Syntax]
function_symbols_opening_terms' [in Tableaux.Syntax]
function_symbols_opening [in Tableaux.Syntax]
function_symbols_opening_terms [in Tableaux.Syntax]
fv_list_in [in Tableaux.Prelude.LocallyNamelessClasses]
G
gamma_rule_sound [in Tableaux.Checker]gen_translation_equivalidity [in Tableaux.ExtendedSyntax]
gen_interp_term_interp_eterm [in Tableaux.ExtendedSyntax]
GetFunctSymbols_in [in Tableaux.Syntax]
getter_neg_neg_sound [in Tableaux.Checker]
get_context_extend_oth [in Tableaux.Proofs]
get_context_extend_right [in Tableaux.Proofs]
get_context_extend_left [in Tableaux.Proofs]
get_context_app_fst [in Tableaux.Proofs]
get_context_replace_child_oth [in Tableaux.Proofs]
get_replace_nth_inv' [in Tableaux.Prelude.Utils]
get_replace_nth' [in Tableaux.Prelude.Utils]
get_replace_nth [in Tableaux.Prelude.Utils]
H
hasTableau_inner_drinker_proof [in drinker]hasTableau_outer_drinker_proof [in drinker]
hasTableau_inner_branching_proof [in branching]
hasTableau_outer_branching_proof [in branching]
hasTableau_sound [in Tableaux.Proofs]
hasTableau_not_satisfiable [in Tableaux.Proofs]
hasTableau_is_evalid [in Tableaux.ExtendedSyntax]
hd_error_hd [in Tableaux.Prelude.Utils]
I
index_of_None [in Tableaux.ExtendedSyntax]index_of_prefix [in Tableaux.ExtendedSyntax]
index_of_length [in Tableaux.ExtendedSyntax]
index_of_rapp'' [in Tableaux.ExtendedSyntax]
index_of_rapp' [in Tableaux.ExtendedSyntax]
index_of_rapp [in Tableaux.ExtendedSyntax]
index_of_nth [in Tableaux.ExtendedSyntax]
index_of_cons' [in Tableaux.ExtendedSyntax]
index_of_cons [in Tableaux.ExtendedSyntax]
index_of_In' [in Tableaux.ExtendedSyntax]
index_of_In [in Tableaux.ExtendedSyntax]
index_of_inj [in Tableaux.ExtendedSyntax]
index_of_spec [in Tableaux.ExtendedSyntax]
InnerSkolemization_function_symbols [in Tableaux.Skolemization]
InnerSkolemization_isFunc [in Tableaux.Skolemization]
InnerSkolemization_isLocallyClosed [in Tableaux.Skolemization]
InnerSkolemization_args_vars [in Tableaux.Skolemization]
InnerSkolemization_is_sko_pred_sound [in Tableaux.Skolemization]
instantiate_eform_commutes_instantiate_form [in Tableaux.ExtendedSyntax]
instantiate_eterm_commutes_instantiate_term [in Tableaux.ExtendedSyntax]
instantiate_shadowed_form [in Tableaux.ExtendedSyntax]
instantiate_shadowed_term [in Tableaux.ExtendedSyntax]
instantiate_imply_all [in Tableaux.Semantics]
interp_list_commute [in Tableaux.Semantics]
interp_form_list [in Tableaux.Semantics]
inter_sym [in Tableaux.Prelude.Sets]
In_Forall [in Tableaux.Prelude.Ind]
in_context_is_on_branch [in Tableaux.Proofs]
in_get_ctx_in_all_formulas [in Tableaux.Proofs]
In_In_replace_nth [in Tableaux.Prelude.Utils]
In_replace_nth' [in Tableaux.Prelude.Utils]
In_replace_nth [in Tableaux.Prelude.Utils]
In_index_of [in Tableaux.ExtendedSyntax]
in_form_list_interp [in Tableaux.Semantics]
in_form_list_models [in Tableaux.Semantics]
isClosedList_isClosedFormList [in Tableaux.Syntax]
isClosedList_isClosedFormisClosed [in Tableaux.Syntax]
isClosedList_elem [in Tableaux.Syntax]
isClosed_subst_form [in Tableaux.Syntax]
isClosed_subst_term [in Tableaux.Syntax]
isClosed_interp_form_env_eq [in Tableaux.Semantics]
isClosed_interp_term_env_eq [in Tableaux.Semantics]
isLocallyClosed_isLocallyClosed_subst [in Tableaux.Syntax]
isLocallyClosed_Fun_isLocallyClosed_list' [in Tableaux.Syntax]
isLocallyClosed_Fun_isLocallyClosed_list [in Tableaux.Syntax]
isLocallyClosed_interp_env [in Tableaux.Semantics]
isSkolemization_InnerSkolemizationData [in Tableaux.Skolemization]
isSkolemization_OuterSkolemizationData [in Tableaux.Skolemization]
is_free_sound [in Tableaux.Syntax]
is_subterm_trans [in Tableaux.Syntax]
is_expansion_sequence_singleton [in Tableaux.Proofs]
is_expansion_sequence_nil [in Tableaux.Proofs]
is_on_satisfiable_branch [in Tableaux.Proofs]
is_on_branch_in_context [in Tableaux.Proofs]
is_satisfiable_extend [in Tableaux.Proofs]
is_satisfiable_extend_gen [in Tableaux.Proofs]
is_branch_of_expand_tableau_branch [in Tableaux.Proofs]
is_branch_of_replace_child_oth_inv [in Tableaux.Proofs]
is_branch_of_replace_child_oth [in Tableaux.Proofs]
is_branch_of_get_child_at [in Tableaux.Proofs]
is_subbranch_of_has_label [in Tableaux.Proofs]
is_branch_of_extend_oth [in Tableaux.Proofs]
is_branch_of_extend_None [in Tableaux.Proofs]
is_branch_of_extend_right [in Tableaux.Proofs]
is_branch_of_extend_left' [in Tableaux.Proofs]
is_branch_of_extend_left [in Tableaux.Proofs]
is_branch_of_is_subbranch_of [in Tableaux.Proofs]
is_branch_of_dec [in Tableaux.Proofs]
is_valid_translation_is_valid [in Tableaux.ExtendedSyntax]
is_empty_union [in Tableaux.Prelude.Sets]
is_empty_union2 [in Tableaux.Prelude.Sets]
is_empty_union1 [in Tableaux.Prelude.Sets]
is_empty_spec' [in Tableaux.Prelude.Sets]
is_empty_spec [in Tableaux.Prelude.Sets]
is_satisfiable_equiv [in Tableaux.Semantics]
is_satisfiable_is_not_countersat [in Tableaux.Semantics]
J
join_unitl [in Tableaux.Skolemization]join_unitr [in Tableaux.Skolemization]
L
last_nth_error [in Tableaux.Prelude.Utils]last_app [in Tableaux.Prelude.Utils]
last_cons [in Tableaux.Prelude.Utils]
list_mem_spec [in Tableaux.Prelude.Utils]
locally_closed_subst_translation [in Tableaux.ExtendedSyntax]
ls_to_eform_ls_to_form [in Tableaux.ExtendedSyntax]
ls_to_form_app [in Tableaux.Semantics]
ls_to_form_commutes [in Tableaux.Semantics]
ltb_list_false [in Tableaux.Prelude.Utils]
ltb_list_lt_list [in Tableaux.Prelude.Utils]
ltb_form_false [in Tableaux.SyntaxInstance]
ltb_form_lt_form [in Tableaux.SyntaxInstance]
ltb_term_false [in Tableaux.SyntaxInstance]
ltb_term_lt_term [in Tableaux.SyntaxInstance]
M
match_eq_dec_eq_bool [in Tableaux.Prelude.Classes]mem_record_spec [in Tableaux.Skolemization]
mem_spec' [in Tableaux.Prelude.Sets]
mem_unionr [in Tableaux.Prelude.Sets]
mem_unionl [in Tableaux.Prelude.Sets]
models_P_neg_P [in Tableaux.Semantics]
models_iff [in Tableaux.Semantics]
MSetAVLCompat.diff_spec' [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.Empty_eq_empty [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.empty_spec' [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.equal_eq [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.ext [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.in_dec [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.set_equal_is_eq [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.singleton_spec' [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.subsetb_spec [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.eq_equiv [in Tableaux.Prelude.SetInstances]
N
neg_equiv [in Tableaux.Semantics]neg_neg_equiv [in Tableaux.Semantics]
not_subbranch_no_ext_is_branch [in Tableaux.Proofs]
no_skolem_same_interp_form [in Tableaux.Semantics]
no_skolem_same_interp_term [in Tableaux.Semantics]
nth_error_Some' [in Tableaux.Prelude.Utils]
O
only_fv_valuation_matters_in_forms [in Tableaux.Semantics]only_fv_valuation_matters_in_terms [in Tableaux.Semantics]
OrderedForm.compare_spec [in Tableaux.SyntaxInstance]
OrderedForm.eq_equiv [in Tableaux.SyntaxInstance]
OrderedForm.lt_strorder [in Tableaux.SyntaxInstance]
or_comm [in Tableaux.Semantics]
or_equiv [in Tableaux.Semantics]
OuterSkolemization_function_symbols [in Tableaux.Skolemization]
OuterSkolemization_isFunc [in Tableaux.Skolemization]
OuterSkolemization_isLocallyClosed [in Tableaux.Skolemization]
OuterSkolemization_args_vars [in Tableaux.Skolemization]
OuterSkolemization_is_sko_pred_sound [in Tableaux.Skolemization]
P
preserves_function_symbols_get_neg_all [in Tableaux.Checker]preserves_function_symbols_get_all [in Tableaux.Checker]
preserves_function_symbols_get_or2 [in Tableaux.Checker]
preserves_function_symbols_get_or1 [in Tableaux.Checker]
preserves_function_symbols_get_neg_or [in Tableaux.Checker]
preserves_function_symbols_get_neg_neg [in Tableaux.Checker]
preserves_function_symbols_None [in Tableaux.Checker]
R
removelast_nth_error [in Tableaux.Prelude.Utils]removelast_length [in Tableaux.Prelude.Utils]
rem_spec3 [in Tableaux.Prelude.Sets]
rem_spec2 [in Tableaux.Prelude.Sets]
rem_spec1 [in Tableaux.Prelude.Sets]
replace_expanded_child_not_subbranch [in Tableaux.Proofs]
replace_expanded_child_not_branch_Right [in Tableaux.Proofs]
replace_expanded_child_not_branch_Left [in Tableaux.Proofs]
replace_child_Node [in Tableaux.Proofs]
replace_child_sequence_expand [in Tableaux.Proofs]
replace_expand_Left [in Tableaux.Proofs]
replace_child_get_child_at [in Tableaux.Proofs]
replace_nth_replace_nth [in Tableaux.Prelude.Utils]
replace_nth_Some [in Tableaux.Prelude.Utils]
RuleTree_to_Sequence_preserves_function_symbols_last [in Tableaux.Checker]
RuleTree_to_Sequence_snd_expansion [in Tableaux.Checker]
RuleTree_to_Sequence_symbols [in Tableaux.Checker]
RuleTree_to_Sequence_branch [in Tableaux.Checker]
RuleTree_to_Sequence_hd [in Tableaux.Checker]
RuleTree_to_Sequence_not_nil [in Tableaux.Checker]
rule_wrapper_sound [in Tableaux.Checker]
S
satisfiable_tableau_satisfiable_expansion_sequence [in Tableaux.Proofs]satisfiable_expansion_satisfiable [in Tableaux.Proofs]
satisfies_opening_with_sko [in Tableaux.Semantics]
satisfying_symbol_prop [in Tableaux.Semantics]
satisfy_delta [in Tableaux.Semantics]
set_fold_left [in Tableaux.Prelude.Sets]
singleton_spec1 [in Tableaux.Prelude.Sets]
SkoRecordSpecs_set [in Tableaux.Skolemization]
sko_function_symbols_sound [in Tableaux.Skolemization]
sko_function_symbols_args [in Tableaux.Skolemization]
SOrd.compare_spec [in Tableaux.Prelude.SetInstances]
SOrd.lt_strorder [in Tableaux.Prelude.SetInstances]
subst_commutes_with_env_forms [in Tableaux.Semantics]
subst_commutes_with_env_terms [in Tableaux.Semantics]
subterm_not_subterm_not_subterm [in Tableaux.Syntax]
symbol_sound [in Tableaux.Skolemization]
T
term_subst_opening [in Tableaux.Syntax]term_locally_closed_inst [in Tableaux.Syntax]
term_env_inst_commutes [in Tableaux.Semantics]
translation_equivalidity [in Tableaux.ExtendedSyntax]
trivial_pred_is_eq_for_unit [in Tableaux.Prelude.Classes]
trivial_contradiction_sound [in Tableaux.Checker]
U
union_comm [in Tableaux.Prelude.Sets]union_assoc [in Tableaux.Prelude.Sets]
union_sym [in Tableaux.Prelude.Sets]
union_idemp [in Tableaux.Prelude.Sets]
union_congr [in Tableaux.Prelude.Sets]
union_congl [in Tableaux.Prelude.Sets]
Constructor Index
A
All [in Tableaux.Syntax]AlphaNegNeg [in Tableaux.ProofInstance]
AlphaNegOr [in Tableaux.ProofInstance]
B
BetaOr [in Tableaux.ProofInstance]Bot [in Tableaux.Syntax]
Bound [in Tableaux.Syntax]
bv [in Tableaux.Prelude.LocallyNamelessClasses]
D
DeltaNegAll [in Tableaux.ProofInstance]E
EAll [in Tableaux.ExtendedSyntax]EAnd [in Tableaux.ExtendedSyntax]
EBot [in Tableaux.ExtendedSyntax]
EEqu [in Tableaux.ExtendedSyntax]
EEx [in Tableaux.ExtendedSyntax]
EFun [in Tableaux.ExtendedSyntax]
EImp [in Tableaux.ExtendedSyntax]
ENeg [in Tableaux.ExtendedSyntax]
EOr [in Tableaux.ExtendedSyntax]
EPred [in Tableaux.ExtendedSyntax]
eqDec [in Tableaux.Prelude.Classes]
ETop [in Tableaux.ExtendedSyntax]
EVar [in Tableaux.ExtendedSyntax]
expansion_NegAll [in Tableaux.Proofs]
expansion_All [in Tableaux.Proofs]
expansion_Or [in Tableaux.Proofs]
expansion_NegOr [in Tableaux.Proofs]
expansion_NegNeg [in Tableaux.Proofs]
ExtendedSyntax.E.AlphaAnd [in Tableaux.Checker]
ExtendedSyntax.E.AlphaNegImp [in Tableaux.Checker]
ExtendedSyntax.E.AlphaNegNeg [in Tableaux.Checker]
ExtendedSyntax.E.AlphaNegOr [in Tableaux.Checker]
ExtendedSyntax.E.BetaEqu [in Tableaux.Checker]
ExtendedSyntax.E.BetaImp [in Tableaux.Checker]
ExtendedSyntax.E.BetaNegAnd [in Tableaux.Checker]
ExtendedSyntax.E.BetaNegEqu [in Tableaux.Checker]
ExtendedSyntax.E.BetaOr [in Tableaux.Checker]
ExtendedSyntax.E.DeltaEx [in Tableaux.Checker]
ExtendedSyntax.E.DeltaNegAll [in Tableaux.Checker]
ExtendedSyntax.E.GammaAll [in Tableaux.Checker]
ExtendedSyntax.E.GammaNegEx [in Tableaux.Checker]
ExtendedSyntax.E.Leaf [in Tableaux.Checker]
ExtendedSyntax.E.Node [in Tableaux.Checker]
F
Forall_cons [in Tableaux.Prelude.Ind]Forall_nil [in Tableaux.Prelude.Ind]
Free [in Tableaux.Syntax]
Fun [in Tableaux.Syntax]
function_symbols [in Tableaux.Syntax]
fv [in Tableaux.Prelude.LocallyNamelessClasses]
G
GammaAll [in Tableaux.ProofInstance]I
interpret [in Tableaux.Semantics]is_subformula [in Tableaux.Syntax]
is_on_branch_right [in Tableaux.Proofs]
is_on_branch_left [in Tableaux.Proofs]
is_on_branch_node [in Tableaux.Proofs]
is_subbranch_of_right [in Tableaux.Proofs]
is_subbranch_of_left [in Tableaux.Proofs]
is_subbranch_of_node [in Tableaux.Proofs]
is_branch_of_right [in Tableaux.Proofs]
is_branch_of_left [in Tableaux.Proofs]
is_branch_of_nil [in Tableaux.Proofs]
L
Leaf [in Tableaux.Proofs]Leaf [in Tableaux.ProofInstance]
Left [in Tableaux.Proofs]
N
Neg [in Tableaux.Syntax]Node [in Tableaux.Proofs]
Node [in Tableaux.ProofInstance]
O
Or [in Tableaux.Syntax]P
pr [in Tableaux.Checker]Pred [in Tableaux.Syntax]
R
Right [in Tableaux.Proofs]S
substitute [in Tableaux.Prelude.LocallyNamelessClasses]T
translate [in Tableaux.ExtendedSyntax]V
varOpening [in Tableaux.Prelude.LocallyNamelessClasses]Axiom Index
F
funext [in Tableaux.Prelude.Init]M
MSetAVLCompat.set_equal_eq [in Tableaux.Prelude.SetInstances]P
prodext [in Tableaux.Prelude.Init]S
SimpleOrderedType.compare [in Tableaux.Prelude.SetInstances]SimpleOrderedType.compare_spec [in Tableaux.Prelude.SetInstances]
SimpleOrderedType.eq_bool [in Tableaux.Prelude.SetInstances]
SimpleOrderedType.lt [in Tableaux.Prelude.SetInstances]
SimpleOrderedType.lt_compat [in Tableaux.Prelude.SetInstances]
SimpleOrderedType.lt_strorder [in Tableaux.Prelude.SetInstances]
SimpleOrderedType.t [in Tableaux.Prelude.SetInstances]
Projection Index
A
args [in Tableaux.Skolemization]args_sound [in Tableaux.Skolemization]
atom_car [in Tableaux.Semantics]
B
bind [in Tableaux.Prelude.Classes]bv [in Tableaux.Prelude.LocallyNamelessClasses]
C
car [in Tableaux.Prelude.Sets]car [in Tableaux.Semantics]
D
data [in Tableaux.Skolemization]diff [in Tableaux.Prelude.Sets]
diff_spec [in Tableaux.Prelude.Sets]
E
empty_to_set [in Tableaux.Skolemization]empty_record [in Tableaux.Skolemization]
empty_spec [in Tableaux.Prelude.Sets]
empty_set [in Tableaux.Prelude.Sets]
eqb [in Tableaux.Prelude.Classes]
eqbIsEq [in Tableaux.Prelude.Classes]
eqb_atom [in Tableaux.Prelude.Atoms]
eqDec [in Tableaux.Prelude.Classes]
F
function_symbols [in Tableaux.Syntax]fv [in Tableaux.Prelude.LocallyNamelessClasses]
I
inter [in Tableaux.Prelude.Sets]interpret [in Tableaux.Semantics]
interp_pred [in Tableaux.Semantics]
interp_func [in Tableaux.Semantics]
inter_spec [in Tableaux.Prelude.Sets]
isSubst [in Tableaux.Prelude.LocallyNamelessClasses]
is_subformula [in Tableaux.Syntax]
is_skolemization [in Tableaux.Skolemization]
is_sko_sound [in Tableaux.Skolemization]
is_sko_consistent [in Tableaux.Skolemization]
is_func [in Tableaux.Skolemization]
is_sko [in Tableaux.Skolemization]
J
join [in Tableaux.Skolemization]join_to_set [in Tableaux.Skolemization]
join_spec [in Tableaux.Skolemization]
M
mem [in Tableaux.Prelude.Sets]mem_spec [in Tableaux.Prelude.Sets]
N
non_empty [in Tableaux.Semantics]P
pr [in Tableaux.Checker]R
record [in Tableaux.Skolemization]record_ext [in Tableaux.Skolemization]
record_eqb [in Tableaux.Skolemization]
ret [in Tableaux.Prelude.Classes]
S
set_atom [in Tableaux.Prelude.Atoms]set_in_dec [in Tableaux.Prelude.Sets]
set_ext [in Tableaux.Prelude.Sets]
set_in [in Tableaux.Prelude.Sets]
set_eqb [in Tableaux.Prelude.Sets]
singleton [in Tableaux.Prelude.Sets]
singleton_spec [in Tableaux.Prelude.Sets]
single_to_set [in Tableaux.Skolemization]
single_spec [in Tableaux.Skolemization]
single_record [in Tableaux.Skolemization]
skoData [in Tableaux.Skolemization]
sko_record [in Tableaux.Skolemization]
specs [in Tableaux.Skolemization]
status [in Tableaux.Checker]
subsetb [in Tableaux.Prelude.Sets]
subsetb_spec [in Tableaux.Prelude.Sets]
subst [in Tableaux.Prelude.LocallyNamelessClasses]
substitute [in Tableaux.Prelude.LocallyNamelessClasses]
symbol [in Tableaux.Skolemization]
symbols [in Tableaux.Proofs]
symbs [in Tableaux.Checker]
T
to_set [in Tableaux.Skolemization]translate [in Tableaux.ExtendedSyntax]
tree [in Tableaux.Proofs]
U
union [in Tableaux.Prelude.Sets]union_spec [in Tableaux.Prelude.Sets]
V
value_record_spec1 [in Tableaux.Skolemization]value_record [in Tableaux.Skolemization]
varOpening [in Tableaux.Prelude.LocallyNamelessClasses]
Inductive Index
B
BranchingStep [in Tableaux.Proofs]BV [in Tableaux.Prelude.LocallyNamelessClasses]
E
EForm [in Tableaux.ExtendedSyntax]EqDec [in Tableaux.Prelude.Classes]
ETerm [in Tableaux.ExtendedSyntax]
ETranslation [in Tableaux.ExtendedSyntax]
ExpansionStep [in Tableaux.Proofs]
ExtendedSyntax.E.ExtendedRule [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree [in Tableaux.Checker]
F
Forall [in Tableaux.Prelude.Ind]Form [in Tableaux.Syntax]
FV [in Tableaux.Prelude.LocallyNamelessClasses]
G
GetFunctSymbols [in Tableaux.Syntax]H
HasSubformulas [in Tableaux.Syntax]I
Interpret [in Tableaux.Semantics]is_on_branch [in Tableaux.Proofs]
is_subbranch_of [in Tableaux.Proofs]
is_branch_of [in Tableaux.Proofs]
O
Opening [in Tableaux.Prelude.LocallyNamelessClasses]P
Pr [in Tableaux.Checker]R
Rule [in Tableaux.ProofInstance]RuleTree [in Tableaux.ProofInstance]
S
Subst [in Tableaux.Prelude.LocallyNamelessClasses]T
TableauTree [in Tableaux.Proofs]Term [in Tableaux.Syntax]
Instance Index
A
antisym_subset [in Tableaux.Prelude.Sets]B
bv_term [in Tableaux.Syntax]bv_list [in Tableaux.Prelude.LocallyNamelessClasses]
C
Ctx.pr_ctx [in Tableaux.Checker]E
eqbool_form [in Tableaux.Syntax]EqBool_term [in Tableaux.Syntax]
eqb_list [in Tableaux.Prelude.Utils]
eqDec_Term [in Tableaux.Syntax]
EqDec_BranchingStep [in Tableaux.Proofs]
equiv_proper_interp [in Tableaux.Semantics]
equiv_equiv [in Tableaux.Semantics]
equiv_trans [in Tableaux.Semantics]
equiv_sym [in Tableaux.Semantics]
equiv_refl [in Tableaux.Semantics]
eq_dec_list [in Tableaux.Prelude.Classes]
eq_bool_unit [in Tableaux.Prelude.Classes]
eq_dec_string [in Tableaux.Prelude.Classes]
eq_bool_string [in Tableaux.Prelude.Classes]
eq_bool_nat [in Tableaux.Prelude.Classes]
eq_dec_nat [in Tableaux.Prelude.Classes]
eq_dec_bool [in Tableaux.Prelude.Classes]
eq_bool_from_eq_dec [in Tableaux.Prelude.Classes]
eq_dec_from_eq_bool [in Tableaux.Prelude.Classes]
etranslation_term [in Tableaux.ExtendedSyntax]
etranslation_eform [in Tableaux.ExtendedSyntax]
F
fv_form [in Tableaux.Syntax]fv_term [in Tableaux.Syntax]
fv_list [in Tableaux.Prelude.LocallyNamelessClasses]
G
GetFunctSymbols_form [in Tableaux.Syntax]GetFunctSymbols_opt [in Tableaux.Syntax]
GetFunctSymbols_list [in Tableaux.Syntax]
GetFunctSymbols_term [in Tableaux.Syntax]
H
HasSubformulas_Form [in Tableaux.Syntax]HasSubformulas_list [in Tableaux.Syntax]
I
interpret_form [in Tableaux.Semantics]interpret_term [in Tableaux.Semantics]
interpret_list [in Tableaux.Semantics]
L
lt_strorder [in Tableaux.SyntaxInstance]lt_term_strorder [in Tableaux.SyntaxInstance]
M
Monad_Result [in Tableaux.Checker]MSetAVLCompat.eqb [in Tableaux.Prelude.SetInstances]
N
nat_set [in Tableaux.Prelude.SetInstances]nat_atom [in Tableaux.Prelude.AtomInstances]
O
opening_form [in Tableaux.Syntax]opening_term [in Tableaux.Syntax]
option_Monad [in Tableaux.Prelude.Utils]
OrderedForm.lt_compat [in Tableaux.SyntaxInstance]
P
pr_form [in Tableaux.Checker]pr_term [in Tableaux.Checker]
pr_bool [in Tableaux.Checker]
R
reflexive_subset [in Tableaux.Prelude.Sets]S
string_set [in Tableaux.Prelude.SetInstances]string_atom [in Tableaux.Prelude.AtomInstances]
subst_form [in Tableaux.Syntax]
subst_term [in Tableaux.Syntax]
subst_list [in Tableaux.Prelude.LocallyNamelessClasses]
T
transitive_subset [in Tableaux.Prelude.Sets]translate_list [in Tableaux.ExtendedSyntax]
Section Index
B
BVInstances [in Tableaux.Prelude.LocallyNamelessClasses]D
DecEqForms [in Tableaux.Syntax]DecEqTerms [in Tableaux.Syntax]
E
EqDecOtherInstances [in Tableaux.Prelude.Classes]EquivEqBoolEqDec [in Tableaux.Prelude.Classes]
EquivForallIn [in Tableaux.Prelude.Ind]
ESemantics [in Tableaux.ExtendedSyntax]
ESyntax [in Tableaux.ExtendedSyntax]
ESyntaxTranslation [in Tableaux.ExtendedSyntax]
ESyntaxTranslation.ClosedIn [in Tableaux.ExtendedSyntax]
ESyntaxTranslation.IndexOf [in Tableaux.ExtendedSyntax]
ETermInd [in Tableaux.ExtendedSyntax]
ExpansionRules [in Tableaux.Proofs]
F
FreeVariables [in Tableaux.Prelude.LocallyNamelessClasses]FunctionSymbols [in Tableaux.Syntax]
FVForms [in Tableaux.Syntax]
FVInstances [in Tableaux.Prelude.LocallyNamelessClasses]
FVTerms [in Tableaux.Syntax]
I
isClosedLemmas [in Tableaux.Syntax]O
OpeningSubstForms [in Tableaux.Syntax]OpeningSubstTerms [in Tableaux.Syntax]
P
ProofCheckerAlgorithm [in Tableaux.Checker]R
RealReplacementModel [in Tableaux.Semantics]ReplaceInterpFunc [in Tableaux.Semantics]
RulesSoundness [in Tableaux.Checker]
RuleTreeToSequence [in Tableaux.Checker]
RuleTreeToSequence_Lemmas2 [in Tableaux.Checker]
RuleTreeToSequence_Lemmas [in Tableaux.Checker]
S
SemanticsDef [in Tableaux.Semantics]SemanticsFacts [in Tableaux.Semantics]
SetProperties [in Tableaux.Prelude.Sets]
SkoDefs [in Tableaux.Skolemization]
SkolemizationDef [in Tableaux.Skolemization]
SkolemizationDef.SkoRecord [in Tableaux.Skolemization]
SkolemizationDef.SkoRecord.SkoRecordDataDefs [in Tableaux.Skolemization]
SkolemizationInstances [in Tableaux.Skolemization]
SkoSymbolLemmas [in Tableaux.Skolemization]
Soundness [in Tableaux.Proofs]
Soundness [in Tableaux.Checker]
StringLemmas [in Tableaux.Prelude.Utils]
SubstInstances [in Tableaux.Prelude.LocallyNamelessClasses]
Substitution [in Tableaux.Prelude.LocallyNamelessClasses]
SubstOpeningLemmas [in Tableaux.Syntax]
T
Tableaux [in Tableaux.Proofs]TermInd [in Tableaux.Syntax]
TranslateSubst [in Tableaux.ExtendedSyntax]
V
ValidityEquivalence [in Tableaux.ExtendedSyntax]ValidityEquivalence.ExtendedEnvironment [in Tableaux.ExtendedSyntax]
ValidityEquivalence.GenTranslationEquivalidity [in Tableaux.ExtendedSyntax]
Definition Index
A
add [in Tableaux.Prelude.Sets]add_symbol [in Tableaux.Skolemization]
alpha_rule [in Tableaux.Checker]
are_disjoint [in Tableaux.Prelude.Sets]
B
beta_rule [in Tableaux.Checker]Branch [in Tableaux.Proofs]
branching [in branching]
BranchingStep_sind [in Tableaux.Proofs]
BranchingStep_rec [in Tableaux.Proofs]
BranchingStep_ind [in Tableaux.Proofs]
BranchingStep_rect [in Tableaux.Proofs]
bv_eform [in Tableaux.ExtendedSyntax]
C
CheckerAlgorithm [in Tableaux.Checker]CheckProof [in Tableaux.Checker]
CheckProof_aux [in Tableaux.Checker]
closed_in [in Tableaux.ExtendedSyntax]
closure_rule [in Tableaux.Checker]
Ctx.add [in Tableaux.Checker]
Ctx.elements [in Tableaux.Checker]
Ctx.eq [in Tableaux.Checker]
Ctx.existsb [in Tableaux.Checker]
Ctx.from_list [in Tableaux.Checker]
Ctx.fv [in Tableaux.Checker]
Ctx.In [in Tableaux.Checker]
Ctx.mem [in Tableaux.Checker]
Ctx.singleton [in Tableaux.Checker]
Ctx.t [in Tableaux.Checker]
Ctx.union [in Tableaux.Checker]
D
delta_rule [in Tableaux.Checker]disjoint [in Tableaux.Prelude.Sets]
drinker [in drinker]
drinker0 [in drinker]
E
EForm_sind [in Tableaux.ExtendedSyntax]EForm_rec [in Tableaux.ExtendedSyntax]
EForm_ind [in Tableaux.ExtendedSyntax]
EForm_rect [in Tableaux.ExtendedSyntax]
EmptyBranch [in Tableaux.Proofs]
empty_env [in Tableaux.Semantics]
env [in Tableaux.Semantics]
eqb_from_eqDec [in Tableaux.Prelude.Classes]
eqb_form [in Tableaux.Syntax]
eqb_term [in Tableaux.Syntax]
equiv [in Tableaux.Semantics]
error [in Tableaux.Checker]
eterm_ind' [in Tableaux.ExtendedSyntax]
eterm_rect' [in Tableaux.ExtendedSyntax]
eterm_ind [in Tableaux.ExtendedSyntax]
eterm_rect [in Tableaux.ExtendedSyntax]
ETerm_sind [in Tableaux.ExtendedSyntax]
ETerm_rec [in Tableaux.ExtendedSyntax]
ETerm_ind [in Tableaux.ExtendedSyntax]
ETerm_rect [in Tableaux.ExtendedSyntax]
exists_satisfied_branch [in Tableaux.Proofs]
expand_tableau_branch [in Tableaux.Proofs]
expand_tableau_branch__aux [in Tableaux.Proofs]
ExpansionStep_sind [in Tableaux.Proofs]
ExpansionStep_ind [in Tableaux.Proofs]
ExtendedSyntax.compile [in Tableaux.Checker]
ExtendedSyntax.compile__aux [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_sind [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_rec [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_ind [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRuleTree_rect [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_sind [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_rec [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_ind [in Tableaux.Checker]
ExtendedSyntax.E.ExtendedRule_rect [in Tableaux.Checker]
ExtendedSyntax.E.mkBinaryNode [in Tableaux.Checker]
ExtendedSyntax.E.mkClosure [in Tableaux.Checker]
ExtendedSyntax.E.mkTrivialClosure [in Tableaux.Checker]
ExtendedSyntax.E.mkUnaryNode [in Tableaux.Checker]
ExtendedSyntax.get_neg_all [in Tableaux.Checker]
ExtendedSyntax.get_ex [in Tableaux.Checker]
ExtendedSyntax.get_neg_ex [in Tableaux.Checker]
ExtendedSyntax.get_all [in Tableaux.Checker]
ExtendedSyntax.get_neg_equ [in Tableaux.Checker]
ExtendedSyntax.get_equ [in Tableaux.Checker]
ExtendedSyntax.get_neg_and [in Tableaux.Checker]
ExtendedSyntax.get_imp [in Tableaux.Checker]
ExtendedSyntax.get_or [in Tableaux.Checker]
ExtendedSyntax.get_neg_imp [in Tableaux.Checker]
ExtendedSyntax.get_and [in Tableaux.Checker]
ExtendedSyntax.get_neg_or [in Tableaux.Checker]
ExtendedSyntax.get_neg_neg [in Tableaux.Checker]
extended_environment [in Tableaux.ExtendedSyntax]
F
forallb2 [in Tableaux.Prelude.Utils]Forall_sind [in Tableaux.Prelude.Ind]
Forall_rec [in Tableaux.Prelude.Ind]
Forall_ind [in Tableaux.Prelude.Ind]
Forall_rect [in Tableaux.Prelude.Ind]
Form [in Tableaux.SyntaxInstance]
formula_contradiction [in Tableaux.Checker]
Form_sind [in Tableaux.Syntax]
Form_rec [in Tableaux.Syntax]
Form_ind [in Tableaux.Syntax]
Form_rect [in Tableaux.Syntax]
from_list [in Tableaux.Prelude.Sets]
fv_eterm [in Tableaux.ExtendedSyntax]
G
gamma_rule [in Tableaux.Checker]get_symbol [in Tableaux.Syntax]
get_all_formulas [in Tableaux.Proofs]
get_context [in Tableaux.Proofs]
get_child_at [in Tableaux.Proofs]
get_label [in Tableaux.Proofs]
get_neg_all [in Tableaux.Checker]
get_all [in Tableaux.Checker]
get_neg_or [in Tableaux.Checker]
get_or [in Tableaux.Checker]
get_neg_neg [in Tableaux.Checker]
H
hasTableau [in Tableaux.Proofs]I
imply [in Tableaux.Semantics]In [in Tableaux.Prelude.Ind]
index_of [in Tableaux.ExtendedSyntax]
InnerSkolemization [in Tableaux.SkolemizationInstances]
InnerSkolemization [in Tableaux.Skolemization]
InnerSkolemizationData [in Tableaux.Skolemization]
InnerSkolemization_is_sko_pred [in Tableaux.Skolemization]
inner_drinker_proof [in drinker]
inner_subst [in drinker]
instantiate_eform [in Tableaux.ExtendedSyntax]
instantiate_eterm [in Tableaux.ExtendedSyntax]
interpret_eform [in Tableaux.ExtendedSyntax]
interpret_eterm [in Tableaux.ExtendedSyntax]
in_record [in Tableaux.Skolemization]
isClosed [in Tableaux.Prelude.LocallyNamelessClasses]
isLocallyClosed [in Tableaux.Prelude.LocallyNamelessClasses]
is_free [in Tableaux.Syntax]
is_litteral [in Tableaux.Syntax]
is_negative_litteral [in Tableaux.Syntax]
is_positive_litteral [in Tableaux.Syntax]
is_subterm [in Tableaux.Syntax]
is_tableau_proof [in Tableaux.Proofs]
is_expansion_sequence [in Tableaux.Proofs]
is_optional_satisfied [in Tableaux.Proofs]
is_tableau_satisfiable [in Tableaux.Proofs]
is_tableau_closed [in Tableaux.Proofs]
is_branch_closed [in Tableaux.Proofs]
is_on_branch_sind [in Tableaux.Proofs]
is_on_branch_ind [in Tableaux.Proofs]
is_subbranch_of_sind [in Tableaux.Proofs]
is_subbranch_of_ind [in Tableaux.Proofs]
is_branch_of_sind [in Tableaux.Proofs]
is_branch_of_ind [in Tableaux.Proofs]
is_fv_in [in Tableaux.Skolemization]
is_evalid [in Tableaux.ExtendedSyntax]
is_empty [in Tableaux.Prelude.Sets]
is_satisfiable [in Tableaux.Semantics]
is_valid [in Tableaux.Semantics]
L
list_replace [in Tableaux.Prelude.Classes]list_mem [in Tableaux.Prelude.Utils]
ls_to_form [in Tableaux.Syntax]
ls_to_eform [in Tableaux.ExtendedSyntax]
ltb_list [in Tableaux.Prelude.Utils]
ltb_form [in Tableaux.SyntaxInstance]
ltb_term [in Tableaux.SyntaxInstance]
lt_list [in Tableaux.Prelude.Utils]
lt_form [in Tableaux.SyntaxInstance]
lt_term [in Tableaux.SyntaxInstance]
M
mem_record [in Tableaux.Skolemization]mem_list [in Tableaux.ExtendedSyntax]
mkLeaf [in Tableaux.Proofs]
mkOptionalNode [in Tableaux.Proofs]
mkTableau [in Tableaux.Proofs]
mk_env [in Tableaux.Semantics]
MSetAVLCompat.XOrd.compare [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.compare_spec [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.eq [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.eq_dec [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.lt [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.lt_compat [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.lt_strorder [in Tableaux.Prelude.SetInstances]
MSetAVLCompat.XOrd.t [in Tableaux.Prelude.SetInstances]
N
nat_to_string [in Tableaux.Prelude.Utils]NOrd.compare [in Tableaux.Prelude.SetInstances]
NOrd.compare_spec [in Tableaux.Prelude.SetInstances]
NOrd.eq_bool [in Tableaux.Prelude.SetInstances]
NOrd.lt [in Tableaux.Prelude.SetInstances]
NOrd.lt_compat [in Tableaux.Prelude.SetInstances]
NOrd.lt_strorder [in Tableaux.Prelude.SetInstances]
NOrd.t [in Tableaux.Prelude.SetInstances]
O
only_fv_in [in Tableaux.Skolemization]opening_form_ [in Tableaux.Syntax]
option_get [in Tableaux.Prelude.Utils]
OrderedForm.compare [in Tableaux.SyntaxInstance]
OrderedForm.eq [in Tableaux.SyntaxInstance]
OrderedForm.eq_dec [in Tableaux.SyntaxInstance]
OrderedForm.lt [in Tableaux.SyntaxInstance]
OrderedForm.t [in Tableaux.SyntaxInstance]
OuterSkolemization [in Tableaux.SkolemizationInstances]
OuterSkolemization [in Tableaux.Skolemization]
OuterSkolemizationData [in Tableaux.Skolemization]
OuterSkolemization_is_sko_pred [in Tableaux.Skolemization]
outer_drinker_proof [in drinker]
outer_subst [in drinker]
outer_branching_proof [in branching]
P
preserves_function_symbols [in Tableaux.Proofs]pr_list [in Tableaux.Prelude.Utils]
R
rem [in Tableaux.Prelude.Sets]ReplacementModel [in Tableaux.Semantics]
replace_child [in Tableaux.Proofs]
replace_nth [in Tableaux.Prelude.Utils]
replace_in_list [in Tableaux.Prelude.Utils]
replace_interp_func [in Tableaux.Semantics]
result [in Tableaux.Checker]
Result [in Tableaux.Checker]
RuleTree_to_Sequence [in Tableaux.Checker]
RuleTree_to_Sequence__aux [in Tableaux.Checker]
RuleTree_sind [in Tableaux.ProofInstance]
RuleTree_rec [in Tableaux.ProofInstance]
RuleTree_ind [in Tableaux.ProofInstance]
RuleTree_rect [in Tableaux.ProofInstance]
rule_wrapper [in Tableaux.Checker]
Rule_sind [in Tableaux.ProofInstance]
Rule_rec [in Tableaux.ProofInstance]
Rule_ind [in Tableaux.ProofInstance]
Rule_rect [in Tableaux.ProofInstance]
S
satisfying_symbol [in Tableaux.Semantics]Sequence [in Tableaux.Proofs]
Skolemization [in Tableaux.SkolemizationInstances]
SkoRecordData_set [in Tableaux.Skolemization]
SkoWrapper_args [in Tableaux.Skolemization]
SkoWrapper_symbol [in Tableaux.Skolemization]
SkoWrapper_is_sko [in Tableaux.Skolemization]
sko_record_set [in Tableaux.Skolemization]
SOrd.compare [in Tableaux.Prelude.SetInstances]
SOrd.eq_bool [in Tableaux.Prelude.SetInstances]
SOrd.lt [in Tableaux.Prelude.SetInstances]
SOrd.lt_compat [in Tableaux.Prelude.SetInstances]
SOrd.t [in Tableaux.Prelude.SetInstances]
subset [in Tableaux.Prelude.Sets]
subst [in branching]
subst_translation [in Tableaux.ExtendedSyntax]
subst_to_env [in Tableaux.Semantics]
T
Tableau [in Tableaux.ProofInstance]TableauTree_sind [in Tableaux.Proofs]
TableauTree_rec [in Tableaux.Proofs]
TableauTree_ind [in Tableaux.Proofs]
TableauTree_rect [in Tableaux.Proofs]
Term [in Tableaux.SyntaxInstance]
term_ind' [in Tableaux.Syntax]
term_rect' [in Tableaux.Syntax]
term_ind [in Tableaux.Syntax]
term_rect [in Tableaux.Syntax]
Term_sind [in Tableaux.Syntax]
Term_rec [in Tableaux.Syntax]
Term_ind [in Tableaux.Syntax]
Term_rect [in Tableaux.Syntax]
to_form_list [in Tableaux.ExtendedSyntax]
translate_substitution [in Tableaux.ExtendedSyntax]
translate_EForm [in Tableaux.ExtendedSyntax]
translate_EForm_aux [in Tableaux.ExtendedSyntax]
translate_ETerm [in Tableaux.ExtendedSyntax]
trivial_contradiction [in Tableaux.Checker]
U
Unnamed_thm [in drinker]Record Index
A
algo_result [in Tableaux.Checker]B
BV [in Tableaux.Prelude.LocallyNamelessClasses]E
EqBool [in Tableaux.Prelude.Classes]EqDec [in Tableaux.Prelude.Classes]
ETranslation [in Tableaux.ExtendedSyntax]
F
FV [in Tableaux.Prelude.LocallyNamelessClasses]G
GetFunctSymbols [in Tableaux.Syntax]H
HasSubformulas [in Tableaux.Syntax]I
Interpret [in Tableaux.Semantics]isAtom [in Tableaux.Prelude.Atoms]
isSkolemization [in Tableaux.Skolemization]
M
Model [in Tableaux.Semantics]Monad [in Tableaux.Prelude.Classes]
O
Opening [in Tableaux.Prelude.LocallyNamelessClasses]P
Pr [in Tableaux.Checker]S
set [in Tableaux.Prelude.Sets]SkolemizationData [in Tableaux.Skolemization]
Skolemization_ [in Tableaux.Skolemization]
SkoRecord [in Tableaux.Skolemization]
SkoRecordData [in Tableaux.Skolemization]
SkoRecordSpecs [in Tableaux.Skolemization]
Subst [in Tableaux.Prelude.LocallyNamelessClasses]
Substitution [in Tableaux.Prelude.LocallyNamelessClasses]
T
Tableau [in Tableaux.Proofs]| 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 | (1066 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 | (37 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 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 | (25 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 | (270 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 | (72 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 | (10 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 | (72 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 | (25 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 | (58 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 | (49 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 | (254 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 | (24 entries) |