| 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 | (383 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 | (7 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 | (1 entry) |
| 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 | (27 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 | (4 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 | (189 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 | (33 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 | (8 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 | (6 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 | (16 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 | (31 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 | (60 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 | (1 entry) |
Global Index
A
andlist [definition, in ICL.PropL]andlistEq [lemma, in ICL.PropL]
and_dec [instance, in ICL.Base]
app_equi_proper [instance, in ICL.Base]
app_incl_proper [instance, in ICL.Base]
assn [definition, in ICL.PropL]
B
Base [library]bent [definition, in ICL.ctab]
bent_iff_unsat [lemma, in ICL.ctab]
bool_eq_dec [instance, in ICL.Base]
bsc [definition, in ICL.PropL]
C
card [definition, in ICL.Base]Cardinality [section, in ICL.Base]
Cardinality.X [variable, in ICL.Base]
card_equi_proper [instance, in ICL.Base]
card_or [lemma, in ICL.Base]
card_lt [lemma, in ICL.Base]
card_equi [lemma, in ICL.Base]
card_ex [lemma, in ICL.Base]
card_0 [lemma, in ICL.Base]
card_cons_rem [lemma, in ICL.Base]
card_eq [lemma, in ICL.Base]
card_le [lemma, in ICL.Base]
card_not_in_rem [lemma, in ICL.Base]
card_in_rem [lemma, in ICL.Base]
cent [definition, in ICL.ctab]
cent_solved_sat [lemma, in ICL.ctab]
cent_sat [lemma, in ICL.ctab]
cent_weak [lemma, in ICL.ctab]
CharFal [definition, in ICL.PropL]
CharImp [definition, in ICL.PropL]
clause [definition, in ICL.ctab]
Consistency [definition, in ICL.PropL]
cons_equi_proper [instance, in ICL.Base]
cons_incl_proper [instance, in ICL.Base]
context [definition, in ICL.PropL]
ctab [library]
Cut [definition, in ICL.PropL]
D
dec [definition, in ICL.Base]Decidability [section, in ICL.Gentzen]
Decidability.A0 [variable, in ICL.Gentzen]
Decidability.s0 [variable, in ICL.Gentzen]
decider [definition, in ICL.ctab]
decision [definition, in ICL.Base]
dec_prop_iff [lemma, in ICL.Base]
dec_DM_impl [lemma, in ICL.Base]
dec_DM_and [lemma, in ICL.Base]
dec_DN [lemma, in ICL.Base]
disjoint [definition, in ICL.Base]
disjoint_app [lemma, in ICL.Base]
disjoint_cons [lemma, in ICL.Base]
disjoint_nil' [lemma, in ICL.Base]
disjoint_nil [lemma, in ICL.Base]
disjoint_incl [lemma, in ICL.Base]
disjoint_symm [lemma, in ICL.Base]
disjoint_forall [lemma, in ICL.Base]
DM_exists [lemma, in ICL.Base]
DM_or [lemma, in ICL.Base]
Dupfree [section, in ICL.Base]
dupfree [inductive, in ICL.Base]
dupfreeC [constructor, in ICL.Base]
dupfreeN [constructor, in ICL.Base]
dupfree_inv [definition, in ICL.Base]
dupfree_in_power [lemma, in ICL.Base]
dupfree_power [lemma, in ICL.Base]
dupfree_undup [lemma, in ICL.Base]
dupfree_card [lemma, in ICL.Base]
dupfree_dec [lemma, in ICL.Base]
dupfree_filter [lemma, in ICL.Base]
dupfree_map [lemma, in ICL.Base]
dupfree_app [lemma, in ICL.Base]
dupfree_cons [lemma, in ICL.Base]
Dupfree.X [variable, in ICL.Base]
E
EntailRelAllProps [definition, in ICL.PropL]Equi [section, in ICL.Base]
equi [definition, in ICL.Base]
equi_rotate [lemma, in ICL.Base]
equi_shift [lemma, in ICL.Base]
equi_swap [lemma, in ICL.Base]
equi_dup [lemma, in ICL.Base]
equi_push [lemma, in ICL.Base]
equi_Equivalence [instance, in ICL.Base]
Equi.X [variable, in ICL.Base]
eval [definition, in ICL.ctab]
F
F [section, in ICL.PropL]Fal [constructor, in ICL.PropL]
False_dec [instance, in ICL.Base]
FCI [module, in ICL.Base]
FCI.C [definition, in ICL.Base]
FCI.closure [lemma, in ICL.Base]
FCI.F [definition, in ICL.Base]
FCI.FCI [section, in ICL.Base]
FCI.FCI.step [variable, in ICL.Base]
FCI.FCI.V [variable, in ICL.Base]
FCI.FCI.X [variable, in ICL.Base]
FCI.fp [lemma, in ICL.Base]
FCI.incl [lemma, in ICL.Base]
FCI.ind [lemma, in ICL.Base]
FCI.it_incl [lemma, in ICL.Base]
FCI.pick [lemma, in ICL.Base]
filter [definition, in ICL.Base]
FilterComm [section, in ICL.Base]
FilterComm.p [variable, in ICL.Base]
FilterComm.q [variable, in ICL.Base]
FilterComm.X [variable, in ICL.Base]
FilterLemmas [section, in ICL.Base]
FilterLemmas_pq.q [variable, in ICL.Base]
FilterLemmas_pq.p [variable, in ICL.Base]
FilterLemmas_pq.X [variable, in ICL.Base]
FilterLemmas_pq [section, in ICL.Base]
FilterLemmas.p [variable, in ICL.Base]
FilterLemmas.X [variable, in ICL.Base]
filter_comm [lemma, in ICL.Base]
filter_and [lemma, in ICL.Base]
filter_pq_eq [lemma, in ICL.Base]
filter_pq_mono [lemma, in ICL.Base]
filter_fst' [lemma, in ICL.Base]
filter_fst [lemma, in ICL.Base]
filter_app [lemma, in ICL.Base]
filter_id [lemma, in ICL.Base]
filter_mono [lemma, in ICL.Base]
filter_incl [lemma, in ICL.Base]
FK [definition, in ICL.PropL]
form [inductive, in ICL.PropL]
form_eq_dec [instance, in ICL.PropL]
FP [definition, in ICL.Base]
FS [definition, in ICL.PropL]
F.E [variable, in ICL.PropL]
F.F [variable, in ICL.PropL]
G
Gamma [definition, in ICL.Gentzen]gen [inductive, in ICL.Gentzen]
genA [lemma, in ICL.Gentzen]
genC [lemma, in ICL.Gentzen]
genC' [lemma, in ICL.Gentzen]
genF [constructor, in ICL.Gentzen]
genIL [constructor, in ICL.Gentzen]
genIR [constructor, in ICL.Gentzen]
Gentzen [library]
genV [constructor, in ICL.Gentzen]
genW [lemma, in ICL.Gentzen]
gen_lambda [lemma, in ICL.Gentzen]
gen_iff_nd [lemma, in ICL.Gentzen]
gen_DN [lemma, in ICL.Gentzen]
gen_DN' [lemma, in ICL.Gentzen]
gen_con [lemma, in ICL.Gentzen]
gen_nd [lemma, in ICL.Gentzen]
Glivenko [lemma, in ICL.PropL]
Glivenko_refute [lemma, in ICL.PropL]
goal [definition, in ICL.Gentzen]
goal_eq_dec [instance, in ICL.Gentzen]
H
hil [inductive, in ICL.PropL]hilA [constructor, in ICL.PropL]
hilAK [lemma, in ICL.PropL]
hilAS [lemma, in ICL.PropL]
hilD [lemma, in ICL.PropL]
hilE [constructor, in ICL.PropL]
hilI [lemma, in ICL.PropL]
hilK [constructor, in ICL.PropL]
hilMP [constructor, in ICL.PropL]
hilS [constructor, in ICL.PropL]
hil_iff_nd [lemma, in ICL.PropL]
hil_nd [lemma, in ICL.PropL]
I
iff_dec [instance, in ICL.Base]Imp [constructor, in ICL.PropL]
impl_dec [instance, in ICL.Base]
inclp [definition, in ICL.Base]
Inclusion [section, in ICL.Base]
Inclusion.X [variable, in ICL.Base]
incl_equi_proper [instance, in ICL.Base]
incl_preorder [instance, in ICL.Base]
incl_app_left [lemma, in ICL.Base]
incl_lrcons [lemma, in ICL.Base]
incl_rcons [lemma, in ICL.Base]
incl_sing [lemma, in ICL.Base]
incl_lcons [lemma, in ICL.Base]
incl_shift [lemma, in ICL.Base]
incl_nil_eq [lemma, in ICL.Base]
incl_map [lemma, in ICL.Base]
incl_nil [lemma, in ICL.Base]
in_rem_iff [lemma, in ICL.Base]
in_filter_iff [lemma, in ICL.Base]
in_equi_proper [instance, in ICL.Base]
in_incl_proper [instance, in ICL.Base]
in_cons_neq [lemma, in ICL.Base]
in_sing [lemma, in ICL.Base]
it [definition, in ICL.Base]
Iteration [section, in ICL.Base]
Iteration.f [variable, in ICL.Base]
Iteration.X [variable, in ICL.Base]
it_fp [lemma, in ICL.Base]
it_ind [lemma, in ICL.Base]
L
Lambda [definition, in ICL.Gentzen]lambda_gen [lemma, in ICL.Gentzen]
lambda_ind [lemma, in ICL.Gentzen]
lambda_closure [lemma, in ICL.Gentzen]
list_cc [lemma, in ICL.Base]
list_exists_not_incl [lemma, in ICL.Base]
list_exists_DM [lemma, in ICL.Base]
list_exists_dec [instance, in ICL.Base]
list_forall_dec [instance, in ICL.Base]
list_sigma_forall [lemma, in ICL.Base]
list_in_dec [instance, in ICL.Base]
list_eq_dec [instance, in ICL.Base]
list_cycle [lemma, in ICL.Base]
M
Membership [section, in ICL.Base]Membership.X [variable, in ICL.Base]
Monotonicity [definition, in ICL.PropL]
N
nat_le_dec [instance, in ICL.Base]nat_eq_dec [instance, in ICL.Base]
nd [inductive, in ICL.PropL]
ndA [constructor, in ICL.PropL]
ndapp [lemma, in ICL.PropL]
ndapp1 [lemma, in ICL.PropL]
ndapp2 [lemma, in ICL.PropL]
ndapp3 [lemma, in ICL.PropL]
ndc [inductive, in ICL.PropL]
ndcA [constructor, in ICL.PropL]
ndcapp [lemma, in ICL.PropL]
ndcapp1 [lemma, in ICL.PropL]
ndcapp2 [lemma, in ICL.PropL]
ndcapp3 [lemma, in ICL.PropL]
ndcC [constructor, in ICL.PropL]
ndcE [lemma, in ICL.PropL]
ndcIE [constructor, in ICL.PropL]
ndcII [constructor, in ICL.PropL]
ndcW [lemma, in ICL.PropL]
ndc_refute [lemma, in ICL.PropL]
ndc_weak [lemma, in ICL.PropL]
ndc_iff_sem [lemma, in ICL.ctab]
ndc_dec [instance, in ICL.ctab]
ndc_bent [lemma, in ICL.ctab]
ndDN [lemma, in ICL.PropL]
ndE [constructor, in ICL.PropL]
ndIE [constructor, in ICL.PropL]
ndIE_weak [lemma, in ICL.PropL]
ndII [constructor, in ICL.PropL]
ndW [lemma, in ICL.PropL]
nd_hil [lemma, in ICL.PropL]
nd_embeds_ndc [lemma, in ICL.PropL]
nd_ndc [lemma, in ICL.PropL]
nd_subst [lemma, in ICL.PropL]
nd_con [lemma, in ICL.PropL]
nd_bool_sound [lemma, in ICL.PropL]
nd_weak [lemma, in ICL.PropL]
nd_dec [lemma, in ICL.Gentzen]
nd_gen [lemma, in ICL.Gentzen]
Neg [constructor, in ICL.ctab]
Not [definition, in ICL.PropL]
not_in_cons [lemma, in ICL.Base]
not_dec [instance, in ICL.Base]
O
or_dec [instance, in ICL.Base]P
phi [definition, in ICL.ctab]Pos [constructor, in ICL.ctab]
power [definition, in ICL.Base]
PowerRep [section, in ICL.Base]
PowerRep.X [variable, in ICL.Base]
power_extensional [lemma, in ICL.Base]
power_nil [lemma, in ICL.Base]
power_incl [lemma, in ICL.Base]
PropL [library]
provider [definition, in ICL.ctab]
R
rec [inductive, in ICL.ctab]recNF [constructor, in ICL.ctab]
recNI [constructor, in ICL.ctab]
recNil [constructor, in ICL.ctab]
recNV [constructor, in ICL.ctab]
recNV' [constructor, in ICL.ctab]
recPF [constructor, in ICL.ctab]
recPI [constructor, in ICL.ctab]
recPV [constructor, in ICL.ctab]
recPV' [constructor, in ICL.ctab]
Reflexivity [definition, in ICL.PropL]
refutation [lemma, in ICL.ctab]
ref_dec [lemma, in ICL.ctab]
ref_iff_unsat [lemma, in ICL.ctab]
ref_ndc [lemma, in ICL.ctab]
ref_unsat [lemma, in ICL.ctab]
ref_sound [projection, in ICL.ctab]
ref_neg_imp [projection, in ICL.ctab]
ref_pos_imp [projection, in ICL.ctab]
ref_clash [projection, in ICL.ctab]
ref_weak [projection, in ICL.ctab]
ref_Fal [projection, in ICL.ctab]
ref_pred [record, in ICL.ctab]
rem [definition, in ICL.Base]
Removal [section, in ICL.Base]
Removal.X [variable, in ICL.Base]
rem_inclr [lemma, in ICL.Base]
rem_reorder [lemma, in ICL.Base]
rem_id [lemma, in ICL.Base]
rem_fst' [lemma, in ICL.Base]
rem_fst [lemma, in ICL.Base]
rem_comm [lemma, in ICL.Base]
rem_equi [lemma, in ICL.Base]
rem_app' [lemma, in ICL.Base]
rem_app [lemma, in ICL.Base]
rem_neq [lemma, in ICL.Base]
rem_in [lemma, in ICL.Base]
rem_cons' [lemma, in ICL.Base]
rem_cons [lemma, in ICL.Base]
rem_mono [lemma, in ICL.Base]
rem_incl [lemma, in ICL.Base]
rem_not_in [lemma, in ICL.Base]
rep [definition, in ICL.Base]
rep_dupfree [lemma, in ICL.Base]
rep_idempotent [lemma, in ICL.Base]
rep_injective [lemma, in ICL.Base]
rep_eq [lemma, in ICL.Base]
rep_eq' [lemma, in ICL.Base]
rep_mono [lemma, in ICL.Base]
rep_equi [lemma, in ICL.Base]
rep_in [lemma, in ICL.Base]
rep_incl [lemma, in ICL.Base]
rep_power [lemma, in ICL.Base]
RL [section, in ICL.ctab]
RL.Rho [variable, in ICL.ctab]
RL.rho [variable, in ICL.ctab]
S
sat [definition, in ICL.ctab]satis [definition, in ICL.PropL]
satis [definition, in ICL.ctab]
satis_dec [instance, in ICL.PropL]
satis_pos [lemma, in ICL.ctab]
satis_weak [lemma, in ICL.ctab]
satis_in [lemma, in ICL.ctab]
satis_iff [lemma, in ICL.ctab]
satis_neg_imp [lemma, in ICL.ctab]
satis_pos_imp [lemma, in ICL.ctab]
satis_dec [instance, in ICL.ctab]
satis_eval [lemma, in ICL.ctab]
satis' [definition, in ICL.ctab]
sat_weak [lemma, in ICL.ctab]
scl [definition, in ICL.Gentzen]
scl_closed [lemma, in ICL.Gentzen]
scl_incl [lemma, in ICL.Gentzen]
scl_incl' [lemma, in ICL.Gentzen]
scl' [definition, in ICL.Gentzen]
scl'_closed [lemma, in ICL.Gentzen]
scl'_in [lemma, in ICL.Gentzen]
sform [inductive, in ICL.ctab]
sform_eq_dec [instance, in ICL.ctab]
sf_closed_cons [lemma, in ICL.Gentzen]
sf_closed_app [lemma, in ICL.Gentzen]
sf_closed [definition, in ICL.Gentzen]
size [definition, in ICL.ctab]
sizeF [definition, in ICL.ctab]
size_recursion [lemma, in ICL.Base]
solved [definition, in ICL.ctab]
solved_ref [lemma, in ICL.ctab]
solved_neg_var [lemma, in ICL.ctab]
solved_pos_var [lemma, in ICL.ctab]
solved_nil [lemma, in ICL.ctab]
solved_sat [lemma, in ICL.ctab]
solved_phi [lemma, in ICL.ctab]
step [definition, in ICL.Gentzen]
step_dec [instance, in ICL.Gentzen]
subst [definition, in ICL.PropL]
Substitution [definition, in ICL.PropL]
svar [definition, in ICL.ctab]
T
True_dec [instance, in ICL.Base]U
U [definition, in ICL.Gentzen]undup [definition, in ICL.Base]
Undup [section, in ICL.Base]
undup_idempotent [lemma, in ICL.Base]
undup_id [lemma, in ICL.Base]
undup_equi [lemma, in ICL.Base]
undup_incl [lemma, in ICL.Base]
undup_id_equi [lemma, in ICL.Base]
Undup.X [variable, in ICL.Base]
uns [definition, in ICL.ctab]
uns_pos [lemma, in ICL.ctab]
U_sfc [definition, in ICL.Gentzen]
V
valid [definition, in ICL.ctab]valid_unsat [lemma, in ICL.ctab]
Var [constructor, in ICL.PropL]
var [definition, in ICL.PropL]
vars [definition, in ICL.PropL]
other
_ === _ [notation, in ICL.Base]_ <<= _ [notation, in ICL.Base]
_ el _ [notation, in ICL.Base]
eq_dec _ [notation, in ICL.Base]
+ _ [notation, in ICL.ctab]
- _ [notation, in ICL.ctab]
| _ | [notation, in ICL.Base]
Notation Index
other
_ === _ [in ICL.Base]_ <<= _ [in ICL.Base]
_ el _ [in ICL.Base]
eq_dec _ [in ICL.Base]
+ _ [in ICL.ctab]
- _ [in ICL.ctab]
| _ | [in ICL.Base]
Module Index
F
FCI [in ICL.Base]Variable Index
C
Cardinality.X [in ICL.Base]D
Decidability.A0 [in ICL.Gentzen]Decidability.s0 [in ICL.Gentzen]
Dupfree.X [in ICL.Base]
E
Equi.X [in ICL.Base]F
FCI.FCI.step [in ICL.Base]FCI.FCI.V [in ICL.Base]
FCI.FCI.X [in ICL.Base]
FilterComm.p [in ICL.Base]
FilterComm.q [in ICL.Base]
FilterComm.X [in ICL.Base]
FilterLemmas_pq.q [in ICL.Base]
FilterLemmas_pq.p [in ICL.Base]
FilterLemmas_pq.X [in ICL.Base]
FilterLemmas.p [in ICL.Base]
FilterLemmas.X [in ICL.Base]
F.E [in ICL.PropL]
F.F [in ICL.PropL]
I
Inclusion.X [in ICL.Base]Iteration.f [in ICL.Base]
Iteration.X [in ICL.Base]
M
Membership.X [in ICL.Base]P
PowerRep.X [in ICL.Base]R
Removal.X [in ICL.Base]RL.Rho [in ICL.ctab]
RL.rho [in ICL.ctab]
U
Undup.X [in ICL.Base]Library Index
B
BaseC
ctabG
GentzenP
PropLLemma Index
A
andlistEq [in ICL.PropL]B
bent_iff_unsat [in ICL.ctab]C
card_or [in ICL.Base]card_lt [in ICL.Base]
card_equi [in ICL.Base]
card_ex [in ICL.Base]
card_0 [in ICL.Base]
card_cons_rem [in ICL.Base]
card_eq [in ICL.Base]
card_le [in ICL.Base]
card_not_in_rem [in ICL.Base]
card_in_rem [in ICL.Base]
cent_solved_sat [in ICL.ctab]
cent_sat [in ICL.ctab]
cent_weak [in ICL.ctab]
D
dec_prop_iff [in ICL.Base]dec_DM_impl [in ICL.Base]
dec_DM_and [in ICL.Base]
dec_DN [in ICL.Base]
disjoint_app [in ICL.Base]
disjoint_cons [in ICL.Base]
disjoint_nil' [in ICL.Base]
disjoint_nil [in ICL.Base]
disjoint_incl [in ICL.Base]
disjoint_symm [in ICL.Base]
disjoint_forall [in ICL.Base]
DM_exists [in ICL.Base]
DM_or [in ICL.Base]
dupfree_in_power [in ICL.Base]
dupfree_power [in ICL.Base]
dupfree_undup [in ICL.Base]
dupfree_card [in ICL.Base]
dupfree_dec [in ICL.Base]
dupfree_filter [in ICL.Base]
dupfree_map [in ICL.Base]
dupfree_app [in ICL.Base]
dupfree_cons [in ICL.Base]
E
equi_rotate [in ICL.Base]equi_shift [in ICL.Base]
equi_swap [in ICL.Base]
equi_dup [in ICL.Base]
equi_push [in ICL.Base]
F
FCI.closure [in ICL.Base]FCI.fp [in ICL.Base]
FCI.incl [in ICL.Base]
FCI.ind [in ICL.Base]
FCI.it_incl [in ICL.Base]
FCI.pick [in ICL.Base]
filter_comm [in ICL.Base]
filter_and [in ICL.Base]
filter_pq_eq [in ICL.Base]
filter_pq_mono [in ICL.Base]
filter_fst' [in ICL.Base]
filter_fst [in ICL.Base]
filter_app [in ICL.Base]
filter_id [in ICL.Base]
filter_mono [in ICL.Base]
filter_incl [in ICL.Base]
G
genA [in ICL.Gentzen]genC [in ICL.Gentzen]
genC' [in ICL.Gentzen]
genW [in ICL.Gentzen]
gen_lambda [in ICL.Gentzen]
gen_iff_nd [in ICL.Gentzen]
gen_DN [in ICL.Gentzen]
gen_DN' [in ICL.Gentzen]
gen_con [in ICL.Gentzen]
gen_nd [in ICL.Gentzen]
Glivenko [in ICL.PropL]
Glivenko_refute [in ICL.PropL]
H
hilAK [in ICL.PropL]hilAS [in ICL.PropL]
hilD [in ICL.PropL]
hilI [in ICL.PropL]
hil_iff_nd [in ICL.PropL]
hil_nd [in ICL.PropL]
I
incl_app_left [in ICL.Base]incl_lrcons [in ICL.Base]
incl_rcons [in ICL.Base]
incl_sing [in ICL.Base]
incl_lcons [in ICL.Base]
incl_shift [in ICL.Base]
incl_nil_eq [in ICL.Base]
incl_map [in ICL.Base]
incl_nil [in ICL.Base]
in_rem_iff [in ICL.Base]
in_filter_iff [in ICL.Base]
in_cons_neq [in ICL.Base]
in_sing [in ICL.Base]
it_fp [in ICL.Base]
it_ind [in ICL.Base]
L
lambda_gen [in ICL.Gentzen]lambda_ind [in ICL.Gentzen]
lambda_closure [in ICL.Gentzen]
list_cc [in ICL.Base]
list_exists_not_incl [in ICL.Base]
list_exists_DM [in ICL.Base]
list_sigma_forall [in ICL.Base]
list_cycle [in ICL.Base]
N
ndapp [in ICL.PropL]ndapp1 [in ICL.PropL]
ndapp2 [in ICL.PropL]
ndapp3 [in ICL.PropL]
ndcapp [in ICL.PropL]
ndcapp1 [in ICL.PropL]
ndcapp2 [in ICL.PropL]
ndcapp3 [in ICL.PropL]
ndcE [in ICL.PropL]
ndcW [in ICL.PropL]
ndc_refute [in ICL.PropL]
ndc_weak [in ICL.PropL]
ndc_iff_sem [in ICL.ctab]
ndc_bent [in ICL.ctab]
ndDN [in ICL.PropL]
ndIE_weak [in ICL.PropL]
ndW [in ICL.PropL]
nd_hil [in ICL.PropL]
nd_embeds_ndc [in ICL.PropL]
nd_ndc [in ICL.PropL]
nd_subst [in ICL.PropL]
nd_con [in ICL.PropL]
nd_bool_sound [in ICL.PropL]
nd_weak [in ICL.PropL]
nd_dec [in ICL.Gentzen]
nd_gen [in ICL.Gentzen]
not_in_cons [in ICL.Base]
P
power_extensional [in ICL.Base]power_nil [in ICL.Base]
power_incl [in ICL.Base]
R
refutation [in ICL.ctab]ref_dec [in ICL.ctab]
ref_iff_unsat [in ICL.ctab]
ref_ndc [in ICL.ctab]
ref_unsat [in ICL.ctab]
rem_inclr [in ICL.Base]
rem_reorder [in ICL.Base]
rem_id [in ICL.Base]
rem_fst' [in ICL.Base]
rem_fst [in ICL.Base]
rem_comm [in ICL.Base]
rem_equi [in ICL.Base]
rem_app' [in ICL.Base]
rem_app [in ICL.Base]
rem_neq [in ICL.Base]
rem_in [in ICL.Base]
rem_cons' [in ICL.Base]
rem_cons [in ICL.Base]
rem_mono [in ICL.Base]
rem_incl [in ICL.Base]
rem_not_in [in ICL.Base]
rep_dupfree [in ICL.Base]
rep_idempotent [in ICL.Base]
rep_injective [in ICL.Base]
rep_eq [in ICL.Base]
rep_eq' [in ICL.Base]
rep_mono [in ICL.Base]
rep_equi [in ICL.Base]
rep_in [in ICL.Base]
rep_incl [in ICL.Base]
rep_power [in ICL.Base]
S
satis_pos [in ICL.ctab]satis_weak [in ICL.ctab]
satis_in [in ICL.ctab]
satis_iff [in ICL.ctab]
satis_neg_imp [in ICL.ctab]
satis_pos_imp [in ICL.ctab]
satis_eval [in ICL.ctab]
sat_weak [in ICL.ctab]
scl_closed [in ICL.Gentzen]
scl_incl [in ICL.Gentzen]
scl_incl' [in ICL.Gentzen]
scl'_closed [in ICL.Gentzen]
scl'_in [in ICL.Gentzen]
sf_closed_cons [in ICL.Gentzen]
sf_closed_app [in ICL.Gentzen]
size_recursion [in ICL.Base]
solved_ref [in ICL.ctab]
solved_neg_var [in ICL.ctab]
solved_pos_var [in ICL.ctab]
solved_nil [in ICL.ctab]
solved_sat [in ICL.ctab]
solved_phi [in ICL.ctab]
U
undup_idempotent [in ICL.Base]undup_id [in ICL.Base]
undup_equi [in ICL.Base]
undup_incl [in ICL.Base]
undup_id_equi [in ICL.Base]
uns_pos [in ICL.ctab]
V
valid_unsat [in ICL.ctab]Constructor Index
D
dupfreeC [in ICL.Base]dupfreeN [in ICL.Base]
F
Fal [in ICL.PropL]G
genF [in ICL.Gentzen]genIL [in ICL.Gentzen]
genIR [in ICL.Gentzen]
genV [in ICL.Gentzen]
H
hilA [in ICL.PropL]hilE [in ICL.PropL]
hilK [in ICL.PropL]
hilMP [in ICL.PropL]
hilS [in ICL.PropL]
I
Imp [in ICL.PropL]N
ndA [in ICL.PropL]ndcA [in ICL.PropL]
ndcC [in ICL.PropL]
ndcIE [in ICL.PropL]
ndcII [in ICL.PropL]
ndE [in ICL.PropL]
ndIE [in ICL.PropL]
ndII [in ICL.PropL]
Neg [in ICL.ctab]
P
Pos [in ICL.ctab]R
recNF [in ICL.ctab]recNI [in ICL.ctab]
recNil [in ICL.ctab]
recNV [in ICL.ctab]
recNV' [in ICL.ctab]
recPF [in ICL.ctab]
recPI [in ICL.ctab]
recPV [in ICL.ctab]
recPV' [in ICL.ctab]
V
Var [in ICL.PropL]Inductive Index
D
dupfree [in ICL.Base]F
form [in ICL.PropL]G
gen [in ICL.Gentzen]H
hil [in ICL.PropL]N
nd [in ICL.PropL]ndc [in ICL.PropL]
R
rec [in ICL.ctab]S
sform [in ICL.ctab]Projection Index
R
ref_sound [in ICL.ctab]ref_neg_imp [in ICL.ctab]
ref_pos_imp [in ICL.ctab]
ref_clash [in ICL.ctab]
ref_weak [in ICL.ctab]
ref_Fal [in ICL.ctab]
Section Index
C
Cardinality [in ICL.Base]D
Decidability [in ICL.Gentzen]Dupfree [in ICL.Base]
E
Equi [in ICL.Base]F
F [in ICL.PropL]FCI.FCI [in ICL.Base]
FilterComm [in ICL.Base]
FilterLemmas [in ICL.Base]
FilterLemmas_pq [in ICL.Base]
I
Inclusion [in ICL.Base]Iteration [in ICL.Base]
M
Membership [in ICL.Base]P
PowerRep [in ICL.Base]R
Removal [in ICL.Base]RL [in ICL.ctab]
U
Undup [in ICL.Base]Instance Index
A
and_dec [in ICL.Base]app_equi_proper [in ICL.Base]
app_incl_proper [in ICL.Base]
B
bool_eq_dec [in ICL.Base]C
card_equi_proper [in ICL.Base]cons_equi_proper [in ICL.Base]
cons_incl_proper [in ICL.Base]
E
equi_Equivalence [in ICL.Base]F
False_dec [in ICL.Base]form_eq_dec [in ICL.PropL]
G
goal_eq_dec [in ICL.Gentzen]I
iff_dec [in ICL.Base]impl_dec [in ICL.Base]
incl_equi_proper [in ICL.Base]
incl_preorder [in ICL.Base]
in_equi_proper [in ICL.Base]
in_incl_proper [in ICL.Base]
L
list_exists_dec [in ICL.Base]list_forall_dec [in ICL.Base]
list_in_dec [in ICL.Base]
list_eq_dec [in ICL.Base]
N
nat_le_dec [in ICL.Base]nat_eq_dec [in ICL.Base]
ndc_dec [in ICL.ctab]
not_dec [in ICL.Base]
O
or_dec [in ICL.Base]S
satis_dec [in ICL.PropL]satis_dec [in ICL.ctab]
sform_eq_dec [in ICL.ctab]
step_dec [in ICL.Gentzen]
T
True_dec [in ICL.Base]Definition Index
A
andlist [in ICL.PropL]assn [in ICL.PropL]
B
bent [in ICL.ctab]bsc [in ICL.PropL]
C
card [in ICL.Base]cent [in ICL.ctab]
CharFal [in ICL.PropL]
CharImp [in ICL.PropL]
clause [in ICL.ctab]
Consistency [in ICL.PropL]
context [in ICL.PropL]
Cut [in ICL.PropL]
D
dec [in ICL.Base]decider [in ICL.ctab]
decision [in ICL.Base]
disjoint [in ICL.Base]
dupfree_inv [in ICL.Base]
E
EntailRelAllProps [in ICL.PropL]equi [in ICL.Base]
eval [in ICL.ctab]
F
FCI.C [in ICL.Base]FCI.F [in ICL.Base]
filter [in ICL.Base]
FK [in ICL.PropL]
FP [in ICL.Base]
FS [in ICL.PropL]
G
Gamma [in ICL.Gentzen]goal [in ICL.Gentzen]
I
inclp [in ICL.Base]it [in ICL.Base]
L
Lambda [in ICL.Gentzen]M
Monotonicity [in ICL.PropL]N
Not [in ICL.PropL]P
phi [in ICL.ctab]power [in ICL.Base]
provider [in ICL.ctab]
R
Reflexivity [in ICL.PropL]rem [in ICL.Base]
rep [in ICL.Base]
S
sat [in ICL.ctab]satis [in ICL.PropL]
satis [in ICL.ctab]
satis' [in ICL.ctab]
scl [in ICL.Gentzen]
scl' [in ICL.Gentzen]
sf_closed [in ICL.Gentzen]
size [in ICL.ctab]
sizeF [in ICL.ctab]
solved [in ICL.ctab]
step [in ICL.Gentzen]
subst [in ICL.PropL]
Substitution [in ICL.PropL]
svar [in ICL.ctab]
U
U [in ICL.Gentzen]undup [in ICL.Base]
uns [in ICL.ctab]
U_sfc [in ICL.Gentzen]
V
valid [in ICL.ctab]var [in ICL.PropL]
vars [in ICL.PropL]
Record Index
R
ref_pred [in ICL.ctab]| 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 | (383 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 | (7 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 | (1 entry) |
| 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 | (27 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 | (4 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 | (189 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 | (33 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 | (8 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 | (6 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 | (16 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 | (31 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 | (60 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 | (1 entry) |