| 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 | (424 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 | (12 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 | (94 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 | (8 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 | (92 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 | (27 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 | (25 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 | (9 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 | (24 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (131 entries) |
Global Index
A
abs [lemma, in HistoricalExamples.Manna]abs [lemma, in HistoricalExamples.MannaCIC]
absO [axiom, in HistoricalExamples.Manna]
absO [axiom, in HistoricalExamples.MannaCIC]
add [definition, in HistoricalExamples.Manna]
add [definition, in HistoricalExamples.MannaCIC]
add_ass [lemma, in HistoricalExamples.Manna]
add_nO [lemma, in HistoricalExamples.Manna]
add_ass [lemma, in HistoricalExamples.MannaCIC]
add_nO [lemma, in HistoricalExamples.MannaCIC]
and [lemma, in HistoricalExamples.Tarski]
AND [definition, in HistoricalExamples.Tarski]
AND [section, in HistoricalExamples.Tarski]
and [definition, in HistoricalExamples.Base]
and_projections.x [variable, in HistoricalExamples.Base]
and_projections.B [variable, in HistoricalExamples.Base]
and_projections.A [variable, in HistoricalExamples.Base]
and_projections [section, in HistoricalExamples.Base]
AND.h1 [variable, in HistoricalExamples.Tarski]
AND.h2 [variable, in HistoricalExamples.Tarski]
AND.p [variable, in HistoricalExamples.Tarski]
AND.q [variable, in HistoricalExamples.Tarski]
app [definition, in HistoricalExamples.Format]
app [definition, in HistoricalExamples.FormatCIC]
applf [definition, in HistoricalExamples.Format]
appsp [definition, in HistoricalExamples.Format]
ax1 [variable, in HistoricalExamples.Format]
ax1 [axiom, in HistoricalExamples.FormatCIC]
B
Base [library]bd [definition, in HistoricalExamples.Manna]
bd [definition, in HistoricalExamples.MannaCIC]
bound [definition, in HistoricalExamples.Manna]
bound [definition, in HistoricalExamples.MannaCIC]
C
Casebl [definition, in HistoricalExamples.Format]Casebl [section, in HistoricalExamples.Format]
Casebl [definition, in HistoricalExamples.FormatCIC]
Casebl.A [variable, in HistoricalExamples.Format]
caseRxy [lemma, in HistoricalExamples.Newman]
cas_ind [lemma, in HistoricalExamples.Manna]
cas_base [lemma, in HistoricalExamples.Manna]
cas_ind [lemma, in HistoricalExamples.MannaCIC]
cas_base [lemma, in HistoricalExamples.MannaCIC]
Class [definition, in HistoricalExamples.Tarski]
coherence [definition, in HistoricalExamples.Newman]
coherence_sym [lemma, in HistoricalExamples.Newman]
coherence_intro [lemma, in HistoricalExamples.Newman]
commut [definition, in HistoricalExamples.Rstar]
confluence [definition, in HistoricalExamples.Newman]
conj [definition, in HistoricalExamples.Base]
conj [section, in HistoricalExamples.Base]
conj.A [variable, in HistoricalExamples.Base]
conj.B [variable, in HistoricalExamples.Base]
consbl [definition, in HistoricalExamples.Format]
consbl [constructor, in HistoricalExamples.FormatCIC]
conslf [definition, in HistoricalExamples.Format]
consltr [definition, in HistoricalExamples.Format]
consltr [constructor, in HistoricalExamples.FormatCIC]
conssp [definition, in HistoricalExamples.Format]
D
Data [abbreviation, in HistoricalExamples.Base]Diagram [lemma, in HistoricalExamples.Newman]
E
Eq [definition, in HistoricalExamples.Format]Eq [inductive, in HistoricalExamples.FormatCIC]
eq [definition, in HistoricalExamples.Base]
Equal [definition, in HistoricalExamples.Tarski]
Eq_re [definition, in HistoricalExamples.Format]
Eq_tran [definition, in HistoricalExamples.Format]
Eq_bl_bl [definition, in HistoricalExamples.Format]
Eq_co_ltr [definition, in HistoricalExamples.Format]
Eq_co_bl [definition, in HistoricalExamples.Format]
Eq_bl_nil [definition, in HistoricalExamples.Format]
Eq_nil [definition, in HistoricalExamples.Format]
Eq_space [lemma, in HistoricalExamples.FormatCIC]
Eq_space_nil [lemma, in HistoricalExamples.FormatCIC]
Eq_space_bl [lemma, in HistoricalExamples.FormatCIC]
Eq_app_nil [lemma, in HistoricalExamples.FormatCIC]
Eq_app [lemma, in HistoricalExamples.FormatCIC]
Eq_re [lemma, in HistoricalExamples.FormatCIC]
Eq_tran [constructor, in HistoricalExamples.FormatCIC]
Eq_bl_bl [constructor, in HistoricalExamples.FormatCIC]
Eq_co_ltr [constructor, in HistoricalExamples.FormatCIC]
Eq_co_bl [constructor, in HistoricalExamples.FormatCIC]
Eq_bl_nil [constructor, in HistoricalExamples.FormatCIC]
Eq_nil [constructor, in HistoricalExamples.FormatCIC]
except [axiom, in HistoricalExamples.Manna]
ExFormat [constructor, in HistoricalExamples.FormatCIC]
exist [definition, in HistoricalExamples.Base]
exist2 [definition, in HistoricalExamples.Base]
F
f [variable, in HistoricalExamples.Manna]f [variable, in HistoricalExamples.MannaCIC]
fact1 [lemma, in HistoricalExamples.Tarski]
fact2 [lemma, in HistoricalExamples.Tarski]
format [lemma, in HistoricalExamples.FormatCIC]
Format [section, in HistoricalExamples.FormatCIC]
Format [library]
FormatCIC [library]
format_all [lemma, in HistoricalExamples.FormatCIC]
Format.applf [variable, in HistoricalExamples.FormatCIC]
Format.appsp [variable, in HistoricalExamples.FormatCIC]
Format.Casebl_section.xltr [variable, in HistoricalExamples.FormatCIC]
Format.Casebl_section.xbl [variable, in HistoricalExamples.FormatCIC]
Format.Casebl_section.xnil [variable, in HistoricalExamples.FormatCIC]
Format.Casebl_section.c [variable, in HistoricalExamples.FormatCIC]
Format.Casebl_section.A [variable, in HistoricalExamples.FormatCIC]
Format.Casebl_section [section, in HistoricalExamples.FormatCIC]
Format.conslf [variable, in HistoricalExamples.FormatCIC]
Format.conssp [variable, in HistoricalExamples.FormatCIC]
Format.Equivalence [section, in HistoricalExamples.FormatCIC]
Format.inflg [variable, in HistoricalExamples.FormatCIC]
Format.infmax [variable, in HistoricalExamples.FormatCIC]
Format.plus_l_ch [variable, in HistoricalExamples.FormatCIC]
Format.prop2 [variable, in HistoricalExamples.FormatCIC]
Format.suplg [variable, in HistoricalExamples.FormatCIC]
formn [inductive, in HistoricalExamples.FormatCIC]
fsp [constructor, in HistoricalExamples.FormatCIC]
fst [lemma, in HistoricalExamples.Base]
fword [constructor, in HistoricalExamples.FormatCIC]
fwordinf [constructor, in HistoricalExamples.FormatCIC]
fwordsup [constructor, in HistoricalExamples.FormatCIC]
f_equal [lemma, in HistoricalExamples.Base]
f_equal.y [variable, in HistoricalExamples.Base]
f_equal.x [variable, in HistoricalExamples.Base]
f_equal.f [variable, in HistoricalExamples.Base]
f_equal.B [variable, in HistoricalExamples.Base]
f_equal.A [variable, in HistoricalExamples.Base]
f_equal [section, in HistoricalExamples.Base]
I
Increas [axiom, in HistoricalExamples.Manna]Increas [variable, in HistoricalExamples.MannaCIC]
Ind [definition, in HistoricalExamples.Manna]
Ind [variable, in HistoricalExamples.Format]
Induct [definition, in HistoricalExamples.MannaCIC]
Induct [axiom, in HistoricalExamples.FormatCIC]
Ind_proof [lemma, in HistoricalExamples.Newman]
Inf [definition, in HistoricalExamples.Manna]
inf [variable, in HistoricalExamples.Manna]
Inf [definition, in HistoricalExamples.MannaCIC]
inf [axiom, in HistoricalExamples.MannaCIC]
inf [variable, in HistoricalExamples.Format]
inf [axiom, in HistoricalExamples.FormatCIC]
infInf [lemma, in HistoricalExamples.Manna]
infInf [lemma, in HistoricalExamples.MannaCIC]
inflg [definition, in HistoricalExamples.Format]
infmax [variable, in HistoricalExamples.Format]
infO [lemma, in HistoricalExamples.Manna]
infO [lemma, in HistoricalExamples.MannaCIC]
infOO [axiom, in HistoricalExamples.Manna]
infOO [axiom, in HistoricalExamples.MannaCIC]
infS [axiom, in HistoricalExamples.Manna]
infS [axiom, in HistoricalExamples.MannaCIC]
infSn_n [lemma, in HistoricalExamples.Manna]
infSn_n [lemma, in HistoricalExamples.MannaCIC]
infS_O [lemma, in HistoricalExamples.Manna]
infS_inf [axiom, in HistoricalExamples.Manna]
infS_O [lemma, in HistoricalExamples.MannaCIC]
infS_inf [axiom, in HistoricalExamples.MannaCIC]
Inf_Sup_abs [definition, in HistoricalExamples.Manna]
Inf_Sup [definition, in HistoricalExamples.Manna]
inf_sup0 [axiom, in HistoricalExamples.Manna]
inf_sup [axiom, in HistoricalExamples.Manna]
inf_add [lemma, in HistoricalExamples.Manna]
inf_sup_abs [lemma, in HistoricalExamples.Manna]
inf_infS [axiom, in HistoricalExamples.Manna]
Inf_Sup_abs [definition, in HistoricalExamples.MannaCIC]
Inf_Sup [definition, in HistoricalExamples.MannaCIC]
inf_sup0 [axiom, in HistoricalExamples.MannaCIC]
inf_sup [axiom, in HistoricalExamples.MannaCIC]
inf_add [lemma, in HistoricalExamples.MannaCIC]
inf_sup_abs [lemma, in HistoricalExamples.MannaCIC]
inf_infS [axiom, in HistoricalExamples.MannaCIC]
inleft [definition, in HistoricalExamples.Base]
inNV [definition, in HistoricalExamples.Format]
inNV [constructor, in HistoricalExamples.FormatCIC]
inright [definition, in HistoricalExamples.Base]
inval [definition, in HistoricalExamples.Format]
inval [constructor, in HistoricalExamples.FormatCIC]
K
Knaster [lemma, in HistoricalExamples.Tarski]Knaster [section, in HistoricalExamples.Tarski]
Knaster.Incr [variable, in HistoricalExamples.Tarski]
Knaster.Phi [variable, in HistoricalExamples.Tarski]
Knaster.U [variable, in HistoricalExamples.Tarski]
L
Lambo [definition, in HistoricalExamples.Manna]Lambo [definition, in HistoricalExamples.MannaCIC]
LamboProg [lemma, in HistoricalExamples.Manna]
LamboProg [lemma, in HistoricalExamples.MannaCIC]
Lambo1 [definition, in HistoricalExamples.Manna]
Lambo1 [definition, in HistoricalExamples.MannaCIC]
LCH_rec [variable, in HistoricalExamples.Format]
LCH_Ind [variable, in HistoricalExamples.Format]
lemme1 [lemma, in HistoricalExamples.Tarski]
Lem1 [lemma, in HistoricalExamples.Manna]
Lem1 [lemma, in HistoricalExamples.MannaCIC]
Lem1 [lemma, in HistoricalExamples.FormatCIC]
Lem2 [lemma, in HistoricalExamples.Manna]
Lem2 [lemma, in HistoricalExamples.MannaCIC]
Lem2 [lemma, in HistoricalExamples.FormatCIC]
Lem3 [lemma, in HistoricalExamples.Manna]
Lem3 [lemma, in HistoricalExamples.MannaCIC]
Lem4 [lemma, in HistoricalExamples.Manna]
Lem4 [lemma, in HistoricalExamples.MannaCIC]
lgth [definition, in HistoricalExamples.Format]
lgth [definition, in HistoricalExamples.FormatCIC]
Limbo [definition, in HistoricalExamples.Manna]
Limbo [definition, in HistoricalExamples.MannaCIC]
LimboLem [lemma, in HistoricalExamples.Manna]
LimboLem [lemma, in HistoricalExamples.MannaCIC]
LimboSig [definition, in HistoricalExamples.Manna]
LimboSig [definition, in HistoricalExamples.MannaCIC]
local_confluence [definition, in HistoricalExamples.Newman]
l_ch [definition, in HistoricalExamples.Format]
l_ch_it [definition, in HistoricalExamples.FormatCIC]
l_ch [inductive, in HistoricalExamples.FormatCIC]
M
Manna [library]MannaCIC [library]
Map [definition, in HistoricalExamples.Tarski]
max [variable, in HistoricalExamples.Format]
max [axiom, in HistoricalExamples.FormatCIC]
N
n [variable, in HistoricalExamples.Manna]n [variable, in HistoricalExamples.MannaCIC]
nat [definition, in HistoricalExamples.Base]
nat_rec [axiom, in HistoricalExamples.Manna]
nat_match [definition, in HistoricalExamples.Manna]
nat_ind [axiom, in HistoricalExamples.Manna]
nat_match [definition, in HistoricalExamples.MannaCIC]
nat_it [definition, in HistoricalExamples.FormatCIC]
Newman [lemma, in HistoricalExamples.Newman]
Newman [section, in HistoricalExamples.Newman]
Newman [library]
Newman.A [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.Newman_.t2 [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.Newman_.t1 [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.Newman_.u [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.Newman_ [section, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.h2 [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.h1 [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.z [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.y [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.hyp_ind [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct.x [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Induct [section, in HistoricalExamples.Newman]
Newman.Newman_section.Hyp2 [variable, in HistoricalExamples.Newman]
Newman.Newman_section.Hyp1 [variable, in HistoricalExamples.Newman]
Newman.Newman_section [section, in HistoricalExamples.Newman]
Newman.R [variable, in HistoricalExamples.Newman]
Newman.Rstar [variable, in HistoricalExamples.Newman]
Newman.Rstar_Rstar' [variable, in HistoricalExamples.Newman]
Newman.Rstar_transitive [variable, in HistoricalExamples.Newman]
Newman.Rstar_reflexive [variable, in HistoricalExamples.Newman]
nil [definition, in HistoricalExamples.Format]
nil [constructor, in HistoricalExamples.FormatCIC]
noetherian [definition, in HistoricalExamples.Newman]
NV [definition, in HistoricalExamples.Format]
NV [inductive, in HistoricalExamples.FormatCIC]
NVapp1 [definition, in HistoricalExamples.Format]
NVapp1 [constructor, in HistoricalExamples.FormatCIC]
NVapp2 [definition, in HistoricalExamples.Format]
NVapp2 [constructor, in HistoricalExamples.FormatCIC]
NVword [definition, in HistoricalExamples.Format]
NVword [constructor, in HistoricalExamples.FormatCIC]
O
O [definition, in HistoricalExamples.Base]one [definition, in HistoricalExamples.Manna]
one [definition, in HistoricalExamples.MannaCIC]
one [definition, in HistoricalExamples.Base]
or [section, in HistoricalExamples.Base]
or [definition, in HistoricalExamples.Base]
or_intror [definition, in HistoricalExamples.Base]
or_introl [definition, in HistoricalExamples.Base]
or.A [variable, in HistoricalExamples.Base]
or.B [variable, in HistoricalExamples.Base]
Over [definition, in HistoricalExamples.Tarski]
P
pair [definition, in HistoricalExamples.Base]peano [definition, in HistoricalExamples.MannaCIC]
peano_set [definition, in HistoricalExamples.MannaCIC]
plus [definition, in HistoricalExamples.Format]
preproc [definition, in HistoricalExamples.Format]
preproc [lemma, in HistoricalExamples.FormatCIC]
prod [section, in HistoricalExamples.Base]
prod [definition, in HistoricalExamples.Base]
prod.A [variable, in HistoricalExamples.Base]
prod.B [variable, in HistoricalExamples.Base]
Prog [lemma, in HistoricalExamples.Manna]
Prog [lemma, in HistoricalExamples.MannaCIC]
projections [section, in HistoricalExamples.Base]
projections.A [variable, in HistoricalExamples.Base]
projections.B [variable, in HistoricalExamples.Base]
projections.x [variable, in HistoricalExamples.Base]
proj1 [lemma, in HistoricalExamples.Base]
proj2 [lemma, in HistoricalExamples.Base]
P0 [definition, in HistoricalExamples.Tarski]
R
Reduct1 [lemma, in HistoricalExamples.Manna]Reduct1 [lemma, in HistoricalExamples.MannaCIC]
Reduct2 [lemma, in HistoricalExamples.Manna]
Reduct2 [lemma, in HistoricalExamples.MannaCIC]
refl_equal [lemma, in HistoricalExamples.Base]
refl_equal.x [variable, in HistoricalExamples.Base]
refl_equal.A [variable, in HistoricalExamples.Base]
refl_equal [section, in HistoricalExamples.Base]
re_inf [lemma, in HistoricalExamples.Manna]
re_inf [lemma, in HistoricalExamples.MannaCIC]
Rstar [definition, in HistoricalExamples.Rstar]
Rstar [section, in HistoricalExamples.Rstar]
Rstar [library]
Rstar_Rstar' [lemma, in HistoricalExamples.Rstar]
Rstar_transitive [lemma, in HistoricalExamples.Rstar]
Rstar_R [lemma, in HistoricalExamples.Rstar]
Rstar_reflexive [lemma, in HistoricalExamples.Rstar]
Rstar_coherence [lemma, in HistoricalExamples.Newman]
Rstar' [definition, in HistoricalExamples.Rstar]
Rstar'_Rstar [lemma, in HistoricalExamples.Rstar]
Rstar'_R [lemma, in HistoricalExamples.Rstar]
Rstar'_reflexive [lemma, in HistoricalExamples.Rstar]
Rstar.A [variable, in HistoricalExamples.Rstar]
Rstar.R [variable, in HistoricalExamples.Rstar]
S
S [definition, in HistoricalExamples.Tarski]S [definition, in HistoricalExamples.Base]
set [definition, in HistoricalExamples.Tarski]
sig [section, in HistoricalExamples.Base]
Sig [definition, in HistoricalExamples.Base]
SigFormat [inductive, in HistoricalExamples.FormatCIC]
sig.A [variable, in HistoricalExamples.Base]
sig.P [variable, in HistoricalExamples.Base]
sig2 [section, in HistoricalExamples.Base]
Sig2 [definition, in HistoricalExamples.Base]
sig2.A [variable, in HistoricalExamples.Base]
sig2.P [variable, in HistoricalExamples.Base]
sig2.Q [variable, in HistoricalExamples.Base]
Small [definition, in HistoricalExamples.Manna]
Small [definition, in HistoricalExamples.MannaCIC]
SmallO [lemma, in HistoricalExamples.Manna]
SmallO [lemma, in HistoricalExamples.MannaCIC]
snd [lemma, in HistoricalExamples.Base]
space [definition, in HistoricalExamples.Format]
space [inductive, in HistoricalExamples.FormatCIC]
space_co_bl [definition, in HistoricalExamples.Format]
space_bl [definition, in HistoricalExamples.Format]
space_co_bl [constructor, in HistoricalExamples.FormatCIC]
space_bl [constructor, in HistoricalExamples.FormatCIC]
Spec [abbreviation, in HistoricalExamples.Base]
Stable [definition, in HistoricalExamples.Tarski]
Subset [definition, in HistoricalExamples.Tarski]
Subset_trans [definition, in HistoricalExamples.Tarski]
sumbool [definition, in HistoricalExamples.Base]
sumor [section, in HistoricalExamples.Base]
sumor [definition, in HistoricalExamples.Base]
sumor.A [variable, in HistoricalExamples.Base]
sumor.B [variable, in HistoricalExamples.Base]
Sup [definition, in HistoricalExamples.Manna]
sup [definition, in HistoricalExamples.Manna]
Sup [definition, in HistoricalExamples.MannaCIC]
sup [definition, in HistoricalExamples.MannaCIC]
sup [variable, in HistoricalExamples.Format]
sup [axiom, in HistoricalExamples.FormatCIC]
suplg [definition, in HistoricalExamples.Format]
sup_twice [lemma, in HistoricalExamples.Manna]
sup_twice [lemma, in HistoricalExamples.MannaCIC]
T
Tarski [lemma, in HistoricalExamples.Tarski]Tarski [section, in HistoricalExamples.Tarski]
Tarski [library]
Tarski.A [variable, in HistoricalExamples.Tarski]
Tarski.f [variable, in HistoricalExamples.Tarski]
Tarski.F [variable, in HistoricalExamples.Tarski]
Tarski.Incr [variable, in HistoricalExamples.Tarski]
Tarski.Least [variable, in HistoricalExamples.Tarski]
Tarski.lemme1 [section, in HistoricalExamples.Tarski]
Tarski.lemme1.h1 [variable, in HistoricalExamples.Tarski]
Tarski.lemme1.x [variable, in HistoricalExamples.Tarski]
Tarski.R [variable, in HistoricalExamples.Tarski]
Tarski.Rtrans [variable, in HistoricalExamples.Tarski]
Tarski.Upperb [variable, in HistoricalExamples.Tarski]
Term [lemma, in HistoricalExamples.Manna]
Term [lemma, in HistoricalExamples.MannaCIC]
trans [definition, in HistoricalExamples.Base]
tran_inf [axiom, in HistoricalExamples.Manna]
tran_inf [axiom, in HistoricalExamples.MannaCIC]
twice [definition, in HistoricalExamples.Manna]
twice [definition, in HistoricalExamples.MannaCIC]
U
Unbound [axiom, in HistoricalExamples.Manna]Unbound [variable, in HistoricalExamples.MannaCIC]
Union [definition, in HistoricalExamples.Tarski]
Union_least [definition, in HistoricalExamples.Tarski]
Union_upperb [definition, in HistoricalExamples.Tarski]
V
valbl [definition, in HistoricalExamples.Format]valbl [lemma, in HistoricalExamples.FormatCIC]
valide [definition, in HistoricalExamples.Format]
valide [inductive, in HistoricalExamples.FormatCIC]
valltr [lemma, in HistoricalExamples.Format]
Valltr [definition, in HistoricalExamples.Format]
Valltr [section, in HistoricalExamples.Format]
valltr [lemma, in HistoricalExamples.FormatCIC]
Valltr.i [variable, in HistoricalExamples.Format]
Valltr.l [variable, in HistoricalExamples.Format]
val_or_no [definition, in HistoricalExamples.Format]
val_or_no [inductive, in HistoricalExamples.FormatCIC]
Vand [definition, in HistoricalExamples.Format]
vapp [definition, in HistoricalExamples.Format]
vapp [constructor, in HistoricalExamples.FormatCIC]
Vfst [definition, in HistoricalExamples.Format]
void [definition, in HistoricalExamples.Base]
Vsnd [definition, in HistoricalExamples.Format]
vword [definition, in HistoricalExamples.Format]
vword [constructor, in HistoricalExamples.FormatCIC]
W
Wf [lemma, in HistoricalExamples.Manna]wf_Ind [lemma, in HistoricalExamples.Manna]
wf_bd [definition, in HistoricalExamples.Manna]
wf_Ind [lemma, in HistoricalExamples.MannaCIC]
wf_bd [definition, in HistoricalExamples.MannaCIC]
Wf1 [lemma, in HistoricalExamples.MannaCIC]
word [definition, in HistoricalExamples.Format]
word [inductive, in HistoricalExamples.FormatCIC]
wordltr [definition, in HistoricalExamples.Format]
wordltr [constructor, in HistoricalExamples.FormatCIC]
wordnil [definition, in HistoricalExamples.Format]
wordnil [constructor, in HistoricalExamples.FormatCIC]
X
x0 [definition, in HistoricalExamples.Tarski]other
_ /\ _ (type_scope) [notation, in HistoricalExamples.Tarski]_ \/ _ (type_scope) [notation, in HistoricalExamples.Base]
{ _ } + { _ } (type_scope) [notation, in HistoricalExamples.Base]
_ + { _ } (type_scope) [notation, in HistoricalExamples.Base]
_ /\ _ (type_scope) [notation, in HistoricalExamples.Base]
_ & _ [notation, in HistoricalExamples.Base]
< _ > _ = _ [notation, in HistoricalExamples.Base]
< _ > Sig ( _ ) [notation, in HistoricalExamples.Base]
< _ , _ > Snd ( _ ) [notation, in HistoricalExamples.Base]
< _ , _ > Fst ( _ ) [notation, in HistoricalExamples.Base]
< _ , _ > ( _ , _ ) [notation, in HistoricalExamples.Base]
{} [notation, in HistoricalExamples.Base]
Notation Index
other
_ /\ _ (type_scope) [in HistoricalExamples.Tarski]_ \/ _ (type_scope) [in HistoricalExamples.Base]
{ _ } + { _ } (type_scope) [in HistoricalExamples.Base]
_ + { _ } (type_scope) [in HistoricalExamples.Base]
_ /\ _ (type_scope) [in HistoricalExamples.Base]
_ & _ [in HistoricalExamples.Base]
< _ > _ = _ [in HistoricalExamples.Base]
< _ > Sig ( _ ) [in HistoricalExamples.Base]
< _ , _ > Snd ( _ ) [in HistoricalExamples.Base]
< _ , _ > Fst ( _ ) [in HistoricalExamples.Base]
< _ , _ > ( _ , _ ) [in HistoricalExamples.Base]
{} [in HistoricalExamples.Base]
Variable Index
A
and_projections.x [in HistoricalExamples.Base]and_projections.B [in HistoricalExamples.Base]
and_projections.A [in HistoricalExamples.Base]
AND.h1 [in HistoricalExamples.Tarski]
AND.h2 [in HistoricalExamples.Tarski]
AND.p [in HistoricalExamples.Tarski]
AND.q [in HistoricalExamples.Tarski]
ax1 [in HistoricalExamples.Format]
C
Casebl.A [in HistoricalExamples.Format]conj.A [in HistoricalExamples.Base]
conj.B [in HistoricalExamples.Base]
F
f [in HistoricalExamples.Manna]f [in HistoricalExamples.MannaCIC]
Format.applf [in HistoricalExamples.FormatCIC]
Format.appsp [in HistoricalExamples.FormatCIC]
Format.Casebl_section.xltr [in HistoricalExamples.FormatCIC]
Format.Casebl_section.xbl [in HistoricalExamples.FormatCIC]
Format.Casebl_section.xnil [in HistoricalExamples.FormatCIC]
Format.Casebl_section.c [in HistoricalExamples.FormatCIC]
Format.Casebl_section.A [in HistoricalExamples.FormatCIC]
Format.conslf [in HistoricalExamples.FormatCIC]
Format.conssp [in HistoricalExamples.FormatCIC]
Format.inflg [in HistoricalExamples.FormatCIC]
Format.infmax [in HistoricalExamples.FormatCIC]
Format.plus_l_ch [in HistoricalExamples.FormatCIC]
Format.prop2 [in HistoricalExamples.FormatCIC]
Format.suplg [in HistoricalExamples.FormatCIC]
f_equal.y [in HistoricalExamples.Base]
f_equal.x [in HistoricalExamples.Base]
f_equal.f [in HistoricalExamples.Base]
f_equal.B [in HistoricalExamples.Base]
f_equal.A [in HistoricalExamples.Base]
I
Increas [in HistoricalExamples.MannaCIC]Ind [in HistoricalExamples.Format]
inf [in HistoricalExamples.Manna]
inf [in HistoricalExamples.Format]
infmax [in HistoricalExamples.Format]
K
Knaster.Incr [in HistoricalExamples.Tarski]Knaster.Phi [in HistoricalExamples.Tarski]
Knaster.U [in HistoricalExamples.Tarski]
L
LCH_rec [in HistoricalExamples.Format]LCH_Ind [in HistoricalExamples.Format]
M
max [in HistoricalExamples.Format]N
n [in HistoricalExamples.Manna]n [in HistoricalExamples.MannaCIC]
Newman.A [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.Newman_.t2 [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.Newman_.t1 [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.Newman_.u [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.h2 [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.h1 [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.z [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.y [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.hyp_ind [in HistoricalExamples.Newman]
Newman.Newman_section.Induct.x [in HistoricalExamples.Newman]
Newman.Newman_section.Hyp2 [in HistoricalExamples.Newman]
Newman.Newman_section.Hyp1 [in HistoricalExamples.Newman]
Newman.R [in HistoricalExamples.Newman]
Newman.Rstar [in HistoricalExamples.Newman]
Newman.Rstar_Rstar' [in HistoricalExamples.Newman]
Newman.Rstar_transitive [in HistoricalExamples.Newman]
Newman.Rstar_reflexive [in HistoricalExamples.Newman]
O
or.A [in HistoricalExamples.Base]or.B [in HistoricalExamples.Base]
P
prod.A [in HistoricalExamples.Base]prod.B [in HistoricalExamples.Base]
projections.A [in HistoricalExamples.Base]
projections.B [in HistoricalExamples.Base]
projections.x [in HistoricalExamples.Base]
R
refl_equal.x [in HistoricalExamples.Base]refl_equal.A [in HistoricalExamples.Base]
Rstar.A [in HistoricalExamples.Rstar]
Rstar.R [in HistoricalExamples.Rstar]
S
sig.A [in HistoricalExamples.Base]sig.P [in HistoricalExamples.Base]
sig2.A [in HistoricalExamples.Base]
sig2.P [in HistoricalExamples.Base]
sig2.Q [in HistoricalExamples.Base]
sumor.A [in HistoricalExamples.Base]
sumor.B [in HistoricalExamples.Base]
sup [in HistoricalExamples.Format]
T
Tarski.A [in HistoricalExamples.Tarski]Tarski.f [in HistoricalExamples.Tarski]
Tarski.F [in HistoricalExamples.Tarski]
Tarski.Incr [in HistoricalExamples.Tarski]
Tarski.Least [in HistoricalExamples.Tarski]
Tarski.lemme1.h1 [in HistoricalExamples.Tarski]
Tarski.lemme1.x [in HistoricalExamples.Tarski]
Tarski.R [in HistoricalExamples.Tarski]
Tarski.Rtrans [in HistoricalExamples.Tarski]
Tarski.Upperb [in HistoricalExamples.Tarski]
U
Unbound [in HistoricalExamples.MannaCIC]V
Valltr.i [in HistoricalExamples.Format]Valltr.l [in HistoricalExamples.Format]
Library Index
B
BaseF
FormatFormatCIC
M
MannaMannaCIC
N
NewmanR
RstarT
TarskiLemma Index
A
abs [in HistoricalExamples.Manna]abs [in HistoricalExamples.MannaCIC]
add_ass [in HistoricalExamples.Manna]
add_nO [in HistoricalExamples.Manna]
add_ass [in HistoricalExamples.MannaCIC]
add_nO [in HistoricalExamples.MannaCIC]
and [in HistoricalExamples.Tarski]
C
caseRxy [in HistoricalExamples.Newman]cas_ind [in HistoricalExamples.Manna]
cas_base [in HistoricalExamples.Manna]
cas_ind [in HistoricalExamples.MannaCIC]
cas_base [in HistoricalExamples.MannaCIC]
coherence_sym [in HistoricalExamples.Newman]
coherence_intro [in HistoricalExamples.Newman]
D
Diagram [in HistoricalExamples.Newman]E
Eq_space [in HistoricalExamples.FormatCIC]Eq_space_nil [in HistoricalExamples.FormatCIC]
Eq_space_bl [in HistoricalExamples.FormatCIC]
Eq_app_nil [in HistoricalExamples.FormatCIC]
Eq_app [in HistoricalExamples.FormatCIC]
Eq_re [in HistoricalExamples.FormatCIC]
F
fact1 [in HistoricalExamples.Tarski]fact2 [in HistoricalExamples.Tarski]
format [in HistoricalExamples.FormatCIC]
format_all [in HistoricalExamples.FormatCIC]
fst [in HistoricalExamples.Base]
f_equal [in HistoricalExamples.Base]
I
Ind_proof [in HistoricalExamples.Newman]infInf [in HistoricalExamples.Manna]
infInf [in HistoricalExamples.MannaCIC]
infO [in HistoricalExamples.Manna]
infO [in HistoricalExamples.MannaCIC]
infSn_n [in HistoricalExamples.Manna]
infSn_n [in HistoricalExamples.MannaCIC]
infS_O [in HistoricalExamples.Manna]
infS_O [in HistoricalExamples.MannaCIC]
inf_add [in HistoricalExamples.Manna]
inf_sup_abs [in HistoricalExamples.Manna]
inf_add [in HistoricalExamples.MannaCIC]
inf_sup_abs [in HistoricalExamples.MannaCIC]
K
Knaster [in HistoricalExamples.Tarski]L
LamboProg [in HistoricalExamples.Manna]LamboProg [in HistoricalExamples.MannaCIC]
lemme1 [in HistoricalExamples.Tarski]
Lem1 [in HistoricalExamples.Manna]
Lem1 [in HistoricalExamples.MannaCIC]
Lem1 [in HistoricalExamples.FormatCIC]
Lem2 [in HistoricalExamples.Manna]
Lem2 [in HistoricalExamples.MannaCIC]
Lem2 [in HistoricalExamples.FormatCIC]
Lem3 [in HistoricalExamples.Manna]
Lem3 [in HistoricalExamples.MannaCIC]
Lem4 [in HistoricalExamples.Manna]
Lem4 [in HistoricalExamples.MannaCIC]
LimboLem [in HistoricalExamples.Manna]
LimboLem [in HistoricalExamples.MannaCIC]
N
Newman [in HistoricalExamples.Newman]P
preproc [in HistoricalExamples.FormatCIC]Prog [in HistoricalExamples.Manna]
Prog [in HistoricalExamples.MannaCIC]
proj1 [in HistoricalExamples.Base]
proj2 [in HistoricalExamples.Base]
R
Reduct1 [in HistoricalExamples.Manna]Reduct1 [in HistoricalExamples.MannaCIC]
Reduct2 [in HistoricalExamples.Manna]
Reduct2 [in HistoricalExamples.MannaCIC]
refl_equal [in HistoricalExamples.Base]
re_inf [in HistoricalExamples.Manna]
re_inf [in HistoricalExamples.MannaCIC]
Rstar_Rstar' [in HistoricalExamples.Rstar]
Rstar_transitive [in HistoricalExamples.Rstar]
Rstar_R [in HistoricalExamples.Rstar]
Rstar_reflexive [in HistoricalExamples.Rstar]
Rstar_coherence [in HistoricalExamples.Newman]
Rstar'_Rstar [in HistoricalExamples.Rstar]
Rstar'_R [in HistoricalExamples.Rstar]
Rstar'_reflexive [in HistoricalExamples.Rstar]
S
SmallO [in HistoricalExamples.Manna]SmallO [in HistoricalExamples.MannaCIC]
snd [in HistoricalExamples.Base]
sup_twice [in HistoricalExamples.Manna]
sup_twice [in HistoricalExamples.MannaCIC]
T
Tarski [in HistoricalExamples.Tarski]Term [in HistoricalExamples.Manna]
Term [in HistoricalExamples.MannaCIC]
V
valbl [in HistoricalExamples.FormatCIC]valltr [in HistoricalExamples.Format]
valltr [in HistoricalExamples.FormatCIC]
W
Wf [in HistoricalExamples.Manna]wf_Ind [in HistoricalExamples.Manna]
wf_Ind [in HistoricalExamples.MannaCIC]
Wf1 [in HistoricalExamples.MannaCIC]
Axiom Index
A
absO [in HistoricalExamples.Manna]absO [in HistoricalExamples.MannaCIC]
ax1 [in HistoricalExamples.FormatCIC]
E
except [in HistoricalExamples.Manna]I
Increas [in HistoricalExamples.Manna]Induct [in HistoricalExamples.FormatCIC]
inf [in HistoricalExamples.MannaCIC]
inf [in HistoricalExamples.FormatCIC]
infOO [in HistoricalExamples.Manna]
infOO [in HistoricalExamples.MannaCIC]
infS [in HistoricalExamples.Manna]
infS [in HistoricalExamples.MannaCIC]
infS_inf [in HistoricalExamples.Manna]
infS_inf [in HistoricalExamples.MannaCIC]
inf_sup0 [in HistoricalExamples.Manna]
inf_sup [in HistoricalExamples.Manna]
inf_infS [in HistoricalExamples.Manna]
inf_sup0 [in HistoricalExamples.MannaCIC]
inf_sup [in HistoricalExamples.MannaCIC]
inf_infS [in HistoricalExamples.MannaCIC]
M
max [in HistoricalExamples.FormatCIC]N
nat_rec [in HistoricalExamples.Manna]nat_ind [in HistoricalExamples.Manna]
S
sup [in HistoricalExamples.FormatCIC]T
tran_inf [in HistoricalExamples.Manna]tran_inf [in HistoricalExamples.MannaCIC]
U
Unbound [in HistoricalExamples.Manna]Constructor Index
C
consbl [in HistoricalExamples.FormatCIC]consltr [in HistoricalExamples.FormatCIC]
E
Eq_tran [in HistoricalExamples.FormatCIC]Eq_bl_bl [in HistoricalExamples.FormatCIC]
Eq_co_ltr [in HistoricalExamples.FormatCIC]
Eq_co_bl [in HistoricalExamples.FormatCIC]
Eq_bl_nil [in HistoricalExamples.FormatCIC]
Eq_nil [in HistoricalExamples.FormatCIC]
ExFormat [in HistoricalExamples.FormatCIC]
F
fsp [in HistoricalExamples.FormatCIC]fword [in HistoricalExamples.FormatCIC]
fwordinf [in HistoricalExamples.FormatCIC]
fwordsup [in HistoricalExamples.FormatCIC]
I
inNV [in HistoricalExamples.FormatCIC]inval [in HistoricalExamples.FormatCIC]
N
nil [in HistoricalExamples.FormatCIC]NVapp1 [in HistoricalExamples.FormatCIC]
NVapp2 [in HistoricalExamples.FormatCIC]
NVword [in HistoricalExamples.FormatCIC]
S
space_co_bl [in HistoricalExamples.FormatCIC]space_bl [in HistoricalExamples.FormatCIC]
V
vapp [in HistoricalExamples.FormatCIC]vword [in HistoricalExamples.FormatCIC]
W
wordltr [in HistoricalExamples.FormatCIC]wordnil [in HistoricalExamples.FormatCIC]
Inductive Index
E
Eq [in HistoricalExamples.FormatCIC]F
formn [in HistoricalExamples.FormatCIC]L
l_ch [in HistoricalExamples.FormatCIC]N
NV [in HistoricalExamples.FormatCIC]S
SigFormat [in HistoricalExamples.FormatCIC]space [in HistoricalExamples.FormatCIC]
V
valide [in HistoricalExamples.FormatCIC]val_or_no [in HistoricalExamples.FormatCIC]
W
word [in HistoricalExamples.FormatCIC]Section Index
A
AND [in HistoricalExamples.Tarski]and_projections [in HistoricalExamples.Base]
C
Casebl [in HistoricalExamples.Format]conj [in HistoricalExamples.Base]
F
Format [in HistoricalExamples.FormatCIC]Format.Casebl_section [in HistoricalExamples.FormatCIC]
Format.Equivalence [in HistoricalExamples.FormatCIC]
f_equal [in HistoricalExamples.Base]
K
Knaster [in HistoricalExamples.Tarski]N
Newman [in HistoricalExamples.Newman]Newman.Newman_section.Induct.Newman_ [in HistoricalExamples.Newman]
Newman.Newman_section.Induct [in HistoricalExamples.Newman]
Newman.Newman_section [in HistoricalExamples.Newman]
O
or [in HistoricalExamples.Base]P
prod [in HistoricalExamples.Base]projections [in HistoricalExamples.Base]
R
refl_equal [in HistoricalExamples.Base]Rstar [in HistoricalExamples.Rstar]
S
sig [in HistoricalExamples.Base]sig2 [in HistoricalExamples.Base]
sumor [in HistoricalExamples.Base]
T
Tarski [in HistoricalExamples.Tarski]Tarski.lemme1 [in HistoricalExamples.Tarski]
V
Valltr [in HistoricalExamples.Format]Abbreviation Index
D
Data [in HistoricalExamples.Base]S
Spec [in HistoricalExamples.Base]Definition Index
A
add [in HistoricalExamples.Manna]add [in HistoricalExamples.MannaCIC]
AND [in HistoricalExamples.Tarski]
and [in HistoricalExamples.Base]
app [in HistoricalExamples.Format]
app [in HistoricalExamples.FormatCIC]
applf [in HistoricalExamples.Format]
appsp [in HistoricalExamples.Format]
B
bd [in HistoricalExamples.Manna]bd [in HistoricalExamples.MannaCIC]
bound [in HistoricalExamples.Manna]
bound [in HistoricalExamples.MannaCIC]
C
Casebl [in HistoricalExamples.Format]Casebl [in HistoricalExamples.FormatCIC]
Class [in HistoricalExamples.Tarski]
coherence [in HistoricalExamples.Newman]
commut [in HistoricalExamples.Rstar]
confluence [in HistoricalExamples.Newman]
conj [in HistoricalExamples.Base]
consbl [in HistoricalExamples.Format]
conslf [in HistoricalExamples.Format]
consltr [in HistoricalExamples.Format]
conssp [in HistoricalExamples.Format]
E
Eq [in HistoricalExamples.Format]eq [in HistoricalExamples.Base]
Equal [in HistoricalExamples.Tarski]
Eq_re [in HistoricalExamples.Format]
Eq_tran [in HistoricalExamples.Format]
Eq_bl_bl [in HistoricalExamples.Format]
Eq_co_ltr [in HistoricalExamples.Format]
Eq_co_bl [in HistoricalExamples.Format]
Eq_bl_nil [in HistoricalExamples.Format]
Eq_nil [in HistoricalExamples.Format]
exist [in HistoricalExamples.Base]
exist2 [in HistoricalExamples.Base]
I
Ind [in HistoricalExamples.Manna]Induct [in HistoricalExamples.MannaCIC]
Inf [in HistoricalExamples.Manna]
Inf [in HistoricalExamples.MannaCIC]
inflg [in HistoricalExamples.Format]
Inf_Sup_abs [in HistoricalExamples.Manna]
Inf_Sup [in HistoricalExamples.Manna]
Inf_Sup_abs [in HistoricalExamples.MannaCIC]
Inf_Sup [in HistoricalExamples.MannaCIC]
inleft [in HistoricalExamples.Base]
inNV [in HistoricalExamples.Format]
inright [in HistoricalExamples.Base]
inval [in HistoricalExamples.Format]
L
Lambo [in HistoricalExamples.Manna]Lambo [in HistoricalExamples.MannaCIC]
Lambo1 [in HistoricalExamples.Manna]
Lambo1 [in HistoricalExamples.MannaCIC]
lgth [in HistoricalExamples.Format]
lgth [in HistoricalExamples.FormatCIC]
Limbo [in HistoricalExamples.Manna]
Limbo [in HistoricalExamples.MannaCIC]
LimboSig [in HistoricalExamples.Manna]
LimboSig [in HistoricalExamples.MannaCIC]
local_confluence [in HistoricalExamples.Newman]
l_ch [in HistoricalExamples.Format]
l_ch_it [in HistoricalExamples.FormatCIC]
M
Map [in HistoricalExamples.Tarski]N
nat [in HistoricalExamples.Base]nat_match [in HistoricalExamples.Manna]
nat_match [in HistoricalExamples.MannaCIC]
nat_it [in HistoricalExamples.FormatCIC]
nil [in HistoricalExamples.Format]
noetherian [in HistoricalExamples.Newman]
NV [in HistoricalExamples.Format]
NVapp1 [in HistoricalExamples.Format]
NVapp2 [in HistoricalExamples.Format]
NVword [in HistoricalExamples.Format]
O
O [in HistoricalExamples.Base]one [in HistoricalExamples.Manna]
one [in HistoricalExamples.MannaCIC]
one [in HistoricalExamples.Base]
or [in HistoricalExamples.Base]
or_intror [in HistoricalExamples.Base]
or_introl [in HistoricalExamples.Base]
Over [in HistoricalExamples.Tarski]
P
pair [in HistoricalExamples.Base]peano [in HistoricalExamples.MannaCIC]
peano_set [in HistoricalExamples.MannaCIC]
plus [in HistoricalExamples.Format]
preproc [in HistoricalExamples.Format]
prod [in HistoricalExamples.Base]
P0 [in HistoricalExamples.Tarski]
R
Rstar [in HistoricalExamples.Rstar]Rstar' [in HistoricalExamples.Rstar]
S
S [in HistoricalExamples.Tarski]S [in HistoricalExamples.Base]
set [in HistoricalExamples.Tarski]
Sig [in HistoricalExamples.Base]
Sig2 [in HistoricalExamples.Base]
Small [in HistoricalExamples.Manna]
Small [in HistoricalExamples.MannaCIC]
space [in HistoricalExamples.Format]
space_co_bl [in HistoricalExamples.Format]
space_bl [in HistoricalExamples.Format]
Stable [in HistoricalExamples.Tarski]
Subset [in HistoricalExamples.Tarski]
Subset_trans [in HistoricalExamples.Tarski]
sumbool [in HistoricalExamples.Base]
sumor [in HistoricalExamples.Base]
Sup [in HistoricalExamples.Manna]
sup [in HistoricalExamples.Manna]
Sup [in HistoricalExamples.MannaCIC]
sup [in HistoricalExamples.MannaCIC]
suplg [in HistoricalExamples.Format]
T
trans [in HistoricalExamples.Base]twice [in HistoricalExamples.Manna]
twice [in HistoricalExamples.MannaCIC]
U
Union [in HistoricalExamples.Tarski]Union_least [in HistoricalExamples.Tarski]
Union_upperb [in HistoricalExamples.Tarski]
V
valbl [in HistoricalExamples.Format]valide [in HistoricalExamples.Format]
Valltr [in HistoricalExamples.Format]
val_or_no [in HistoricalExamples.Format]
Vand [in HistoricalExamples.Format]
vapp [in HistoricalExamples.Format]
Vfst [in HistoricalExamples.Format]
void [in HistoricalExamples.Base]
Vsnd [in HistoricalExamples.Format]
vword [in HistoricalExamples.Format]
W
wf_bd [in HistoricalExamples.Manna]wf_bd [in HistoricalExamples.MannaCIC]
word [in HistoricalExamples.Format]
wordltr [in HistoricalExamples.Format]
wordnil [in HistoricalExamples.Format]
X
x0 [in HistoricalExamples.Tarski]| 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 | (424 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 | (12 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 | (94 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 | (8 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 | (92 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 | (27 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 | (25 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 | (9 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 | (24 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (131 entries) |