| 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 | (112 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 | (14 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 | (5 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 | (29 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 | (16 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 | (13 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 | (10 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 | (25 entries) |
Global Index
A
Accesible_and_Infinte.R [variable, in CoinductiveExamples.ARITH.Acc_and_Inf]Accesible_and_Infinte.A [variable, in CoinductiveExamples.ARITH.Acc_and_Inf]
Accesible_and_Infinte [section, in CoinductiveExamples.ARITH.Acc_and_Inf]
Acc_and_Inf [library]
allnats [definition, in CoinductiveExamples.STREAMS.Examples]
all_greater_than_m__are_here [lemma, in CoinductiveExamples.STREAMS.Examples]
all_infinite_is_OO [lemma, in CoinductiveExamples.ARITH.Omega]
alter [definition, in CoinductiveExamples.STREAMS.Examples]
Alter [library]
Alter_II.alter2 [variable, in CoinductiveExamples.STREAMS.Alter]
Alter_II.alter1 [variable, in CoinductiveExamples.STREAMS.Alter]
Alter_II [section, in CoinductiveExamples.STREAMS.Alter]
Alter_I.alter2 [variable, in CoinductiveExamples.STREAMS.Alter]
Alter_I.alter1 [variable, in CoinductiveExamples.STREAMS.Alter]
Alter_I.gen2 [variable, in CoinductiveExamples.STREAMS.Alter]
Alter_I.gen1 [variable, in CoinductiveExamples.STREAMS.Alter]
Alter_I [section, in CoinductiveExamples.STREAMS.Alter]
alter1 [definition, in CoinductiveExamples.STREAMS.Examples]
alter2 [definition, in CoinductiveExamples.STREAMS.Examples]
Arithmetic_with_an_explicit_infinity.The_Infinity [section, in CoinductiveExamples.ARITH.Omega]
Arithmetic_with_an_explicit_infinity [section, in CoinductiveExamples.ARITH.Omega]
B
build [constructor, in CoinductiveExamples.STREAMS.Alter]buildeq [constructor, in CoinductiveExamples.STREAMS.Alter]
C
cls [constructor, in CoinductiveExamples.STREAMS.Alter]Cls [inductive, in CoinductiveExamples.STREAMS.Alter]
Cons2 [constructor, in CoinductiveExamples.STREAMS.Examples]
D
derived_eqst2 [definition, in CoinductiveExamples.STREAMS.Examples]derived_eqst [definition, in CoinductiveExamples.STREAMS.Examples]
E
eqalters_III [lemma, in CoinductiveExamples.STREAMS.Alter]eqalters_II [lemma, in CoinductiveExamples.STREAMS.Alter]
eqalters_body [lemma, in CoinductiveExamples.STREAMS.Alter]
eqalters_I_bis [lemma, in CoinductiveExamples.STREAMS.Alter]
eqalters_I [lemma, in CoinductiveExamples.STREAMS.Alter]
EqNat [inductive, in CoinductiveExamples.ARITH.Omega]
EqNat_inj [lemma, in CoinductiveExamples.ARITH.Omega]
EqNat_reflex [lemma, in CoinductiveExamples.ARITH.Omega]
EqSt [inductive, in CoinductiveExamples.STREAMS.Alter]
eqst1 [constructor, in CoinductiveExamples.STREAMS.Alter]
EqSt1 [inductive, in CoinductiveExamples.STREAMS.Alter]
eqst2 [constructor, in CoinductiveExamples.STREAMS.Examples]
EqSt2 [inductive, in CoinductiveExamples.STREAMS.Examples]
EqSt2_trans [lemma, in CoinductiveExamples.STREAMS.Examples]
EqSt2_sym [lemma, in CoinductiveExamples.STREAMS.Examples]
EqSt2_reflex [lemma, in CoinductiveExamples.STREAMS.Examples]
eqSUCC [constructor, in CoinductiveExamples.ARITH.Omega]
Equiv1 [lemma, in CoinductiveExamples.STREAMS.Examples]
Equiv2 [lemma, in CoinductiveExamples.STREAMS.Examples]
eqZ [constructor, in CoinductiveExamples.ARITH.Omega]
Examples [section, in CoinductiveExamples.STREAMS.Examples]
Examples [library]
Examples.Map [section, in CoinductiveExamples.STREAMS.Examples]
Examples.Map.A [variable, in CoinductiveExamples.STREAMS.Examples]
Examples.Map.B [variable, in CoinductiveExamples.STREAMS.Examples]
Examples.Map.f [variable, in CoinductiveExamples.STREAMS.Examples]
F
from [definition, in CoinductiveExamples.STREAMS.Examples]G
gen1 [definition, in CoinductiveExamples.STREAMS.Alter]gen2 [definition, in CoinductiveExamples.STREAMS.Alter]
H
H [lemma, in CoinductiveExamples.STREAMS.Alter]hd [definition, in CoinductiveExamples.STREAMS.Alter]
I
inf [constructor, in CoinductiveExamples.ARITH.Acc_and_Inf]Inf [inductive, in CoinductiveExamples.ARITH.Acc_and_Inf]
Invariant [definition, in CoinductiveExamples.STREAMS.Alter]
is_definitional_for_finite_numbers [lemma, in CoinductiveExamples.ARITH.Omega]
iter [definition, in CoinductiveExamples.STREAMS.Examples]
L
Le [inductive, in CoinductiveExamples.ARITH.Omega]Le_S [constructor, in CoinductiveExamples.ARITH.Omega]
Le_n [constructor, in CoinductiveExamples.ARITH.Omega]
M
makeinv [constructor, in CoinductiveExamples.STREAMS.Alter]map [definition, in CoinductiveExamples.STREAMS.Examples]
mapS [definition, in CoinductiveExamples.STREAMS.Examples]
mapS2 [definition, in CoinductiveExamples.STREAMS.Examples]
map_iter_eq [lemma, in CoinductiveExamples.STREAMS.Examples]
N
Nat [inductive, in CoinductiveExamples.ARITH.Omega]natInj [lemma, in CoinductiveExamples.ARITH.Omega]
Nat_Induction [lemma, in CoinductiveExamples.ARITH.Omega]
Nat_unfold [lemma, in CoinductiveExamples.ARITH.Omega]
NotBoth [lemma, in CoinductiveExamples.ARITH.Acc_and_Inf]
ntoN [definition, in CoinductiveExamples.ARITH.Omega]
O
Omega [library]only_OO_is_grater_than_OO [lemma, in CoinductiveExamples.ARITH.Omega]
only_OO_expands_forever [lemma, in CoinductiveExamples.ARITH.Omega]
OO [definition, in CoinductiveExamples.ARITH.Omega]
OO_is_infiniteII [lemma, in CoinductiveExamples.ARITH.Omega]
OO_is_not_Acc [lemma, in CoinductiveExamples.ARITH.Omega]
OO_is_infinite [lemma, in CoinductiveExamples.ARITH.Omega]
OO_unfold [definition, in CoinductiveExamples.ARITH.Omega]
P
Plus [definition, in CoinductiveExamples.ARITH.Omega]Plus_Idemp [lemma, in CoinductiveExamples.ARITH.Omega]
S
scons [constructor, in CoinductiveExamples.STREAMS.Specified_Streams]shd [definition, in CoinductiveExamples.STREAMS.Specified_Streams]
SimplerInvariant [inductive, in CoinductiveExamples.STREAMS.Alter]
snth [definition, in CoinductiveExamples.STREAMS.Specified_Streams]
Specified_Streams.A [variable, in CoinductiveExamples.STREAMS.Specified_Streams]
Specified_Streams [section, in CoinductiveExamples.STREAMS.Specified_Streams]
Specified_Streams [library]
SStream [inductive, in CoinductiveExamples.STREAMS.Specified_Streams]
St [inductive, in CoinductiveExamples.STREAMS.Alter]
stl [definition, in CoinductiveExamples.STREAMS.Specified_Streams]
Stream_Equalities.Example.f [variable, in CoinductiveExamples.STREAMS.Examples]
Stream_Equalities.Example [section, in CoinductiveExamples.STREAMS.Examples]
Stream_Equalities.A [variable, in CoinductiveExamples.STREAMS.Examples]
Stream_Equalities [section, in CoinductiveExamples.STREAMS.Examples]
St2 [inductive, in CoinductiveExamples.STREAMS.Examples]
SUCC [constructor, in CoinductiveExamples.ARITH.Omega]
T
T [definition, in CoinductiveExamples.STREAMS.Alter]times [constructor, in CoinductiveExamples.STREAMS.Examples]
Times [inductive, in CoinductiveExamples.STREAMS.Examples]
tl [definition, in CoinductiveExamples.STREAMS.Alter]
Z
Z [constructor, in CoinductiveExamples.ARITH.Omega]zeros [definition, in CoinductiveExamples.STREAMS.Examples]
zeros_unfold [lemma, in CoinductiveExamples.STREAMS.Examples]
Z_is_minimum [lemma, in CoinductiveExamples.ARITH.Omega]
Variable Index
A
Accesible_and_Infinte.R [in CoinductiveExamples.ARITH.Acc_and_Inf]Accesible_and_Infinte.A [in CoinductiveExamples.ARITH.Acc_and_Inf]
Alter_II.alter2 [in CoinductiveExamples.STREAMS.Alter]
Alter_II.alter1 [in CoinductiveExamples.STREAMS.Alter]
Alter_I.alter2 [in CoinductiveExamples.STREAMS.Alter]
Alter_I.alter1 [in CoinductiveExamples.STREAMS.Alter]
Alter_I.gen2 [in CoinductiveExamples.STREAMS.Alter]
Alter_I.gen1 [in CoinductiveExamples.STREAMS.Alter]
E
Examples.Map.A [in CoinductiveExamples.STREAMS.Examples]Examples.Map.B [in CoinductiveExamples.STREAMS.Examples]
Examples.Map.f [in CoinductiveExamples.STREAMS.Examples]
S
Specified_Streams.A [in CoinductiveExamples.STREAMS.Specified_Streams]Stream_Equalities.Example.f [in CoinductiveExamples.STREAMS.Examples]
Stream_Equalities.A [in CoinductiveExamples.STREAMS.Examples]
Library Index
A
Acc_and_InfAlter
E
ExamplesO
OmegaS
Specified_StreamsLemma Index
A
all_greater_than_m__are_here [in CoinductiveExamples.STREAMS.Examples]all_infinite_is_OO [in CoinductiveExamples.ARITH.Omega]
E
eqalters_III [in CoinductiveExamples.STREAMS.Alter]eqalters_II [in CoinductiveExamples.STREAMS.Alter]
eqalters_body [in CoinductiveExamples.STREAMS.Alter]
eqalters_I_bis [in CoinductiveExamples.STREAMS.Alter]
eqalters_I [in CoinductiveExamples.STREAMS.Alter]
EqNat_inj [in CoinductiveExamples.ARITH.Omega]
EqNat_reflex [in CoinductiveExamples.ARITH.Omega]
EqSt2_trans [in CoinductiveExamples.STREAMS.Examples]
EqSt2_sym [in CoinductiveExamples.STREAMS.Examples]
EqSt2_reflex [in CoinductiveExamples.STREAMS.Examples]
Equiv1 [in CoinductiveExamples.STREAMS.Examples]
Equiv2 [in CoinductiveExamples.STREAMS.Examples]
H
H [in CoinductiveExamples.STREAMS.Alter]I
is_definitional_for_finite_numbers [in CoinductiveExamples.ARITH.Omega]M
map_iter_eq [in CoinductiveExamples.STREAMS.Examples]N
natInj [in CoinductiveExamples.ARITH.Omega]Nat_Induction [in CoinductiveExamples.ARITH.Omega]
Nat_unfold [in CoinductiveExamples.ARITH.Omega]
NotBoth [in CoinductiveExamples.ARITH.Acc_and_Inf]
O
only_OO_is_grater_than_OO [in CoinductiveExamples.ARITH.Omega]only_OO_expands_forever [in CoinductiveExamples.ARITH.Omega]
OO_is_infiniteII [in CoinductiveExamples.ARITH.Omega]
OO_is_not_Acc [in CoinductiveExamples.ARITH.Omega]
OO_is_infinite [in CoinductiveExamples.ARITH.Omega]
P
Plus_Idemp [in CoinductiveExamples.ARITH.Omega]Z
zeros_unfold [in CoinductiveExamples.STREAMS.Examples]Z_is_minimum [in CoinductiveExamples.ARITH.Omega]
Constructor Index
B
build [in CoinductiveExamples.STREAMS.Alter]buildeq [in CoinductiveExamples.STREAMS.Alter]
C
cls [in CoinductiveExamples.STREAMS.Alter]Cons2 [in CoinductiveExamples.STREAMS.Examples]
E
eqst1 [in CoinductiveExamples.STREAMS.Alter]eqst2 [in CoinductiveExamples.STREAMS.Examples]
eqSUCC [in CoinductiveExamples.ARITH.Omega]
eqZ [in CoinductiveExamples.ARITH.Omega]
I
inf [in CoinductiveExamples.ARITH.Acc_and_Inf]L
Le_S [in CoinductiveExamples.ARITH.Omega]Le_n [in CoinductiveExamples.ARITH.Omega]
M
makeinv [in CoinductiveExamples.STREAMS.Alter]S
scons [in CoinductiveExamples.STREAMS.Specified_Streams]SUCC [in CoinductiveExamples.ARITH.Omega]
T
times [in CoinductiveExamples.STREAMS.Examples]Z
Z [in CoinductiveExamples.ARITH.Omega]Inductive Index
C
Cls [in CoinductiveExamples.STREAMS.Alter]E
EqNat [in CoinductiveExamples.ARITH.Omega]EqSt [in CoinductiveExamples.STREAMS.Alter]
EqSt1 [in CoinductiveExamples.STREAMS.Alter]
EqSt2 [in CoinductiveExamples.STREAMS.Examples]
I
Inf [in CoinductiveExamples.ARITH.Acc_and_Inf]L
Le [in CoinductiveExamples.ARITH.Omega]N
Nat [in CoinductiveExamples.ARITH.Omega]S
SimplerInvariant [in CoinductiveExamples.STREAMS.Alter]SStream [in CoinductiveExamples.STREAMS.Specified_Streams]
St [in CoinductiveExamples.STREAMS.Alter]
St2 [in CoinductiveExamples.STREAMS.Examples]
T
Times [in CoinductiveExamples.STREAMS.Examples]Section Index
A
Accesible_and_Infinte [in CoinductiveExamples.ARITH.Acc_and_Inf]Alter_II [in CoinductiveExamples.STREAMS.Alter]
Alter_I [in CoinductiveExamples.STREAMS.Alter]
Arithmetic_with_an_explicit_infinity.The_Infinity [in CoinductiveExamples.ARITH.Omega]
Arithmetic_with_an_explicit_infinity [in CoinductiveExamples.ARITH.Omega]
E
Examples [in CoinductiveExamples.STREAMS.Examples]Examples.Map [in CoinductiveExamples.STREAMS.Examples]
S
Specified_Streams [in CoinductiveExamples.STREAMS.Specified_Streams]Stream_Equalities.Example [in CoinductiveExamples.STREAMS.Examples]
Stream_Equalities [in CoinductiveExamples.STREAMS.Examples]
Definition Index
A
allnats [in CoinductiveExamples.STREAMS.Examples]alter [in CoinductiveExamples.STREAMS.Examples]
alter1 [in CoinductiveExamples.STREAMS.Examples]
alter2 [in CoinductiveExamples.STREAMS.Examples]
D
derived_eqst2 [in CoinductiveExamples.STREAMS.Examples]derived_eqst [in CoinductiveExamples.STREAMS.Examples]
F
from [in CoinductiveExamples.STREAMS.Examples]G
gen1 [in CoinductiveExamples.STREAMS.Alter]gen2 [in CoinductiveExamples.STREAMS.Alter]
H
hd [in CoinductiveExamples.STREAMS.Alter]I
Invariant [in CoinductiveExamples.STREAMS.Alter]iter [in CoinductiveExamples.STREAMS.Examples]
M
map [in CoinductiveExamples.STREAMS.Examples]mapS [in CoinductiveExamples.STREAMS.Examples]
mapS2 [in CoinductiveExamples.STREAMS.Examples]
N
ntoN [in CoinductiveExamples.ARITH.Omega]O
OO [in CoinductiveExamples.ARITH.Omega]OO_unfold [in CoinductiveExamples.ARITH.Omega]
P
Plus [in CoinductiveExamples.ARITH.Omega]S
shd [in CoinductiveExamples.STREAMS.Specified_Streams]snth [in CoinductiveExamples.STREAMS.Specified_Streams]
stl [in CoinductiveExamples.STREAMS.Specified_Streams]
T
T [in CoinductiveExamples.STREAMS.Alter]tl [in CoinductiveExamples.STREAMS.Alter]
Z
zeros [in CoinductiveExamples.STREAMS.Examples]| 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 | (112 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 | (14 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 | (5 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 | (29 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 | (16 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 | (13 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 | (10 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 | (25 entries) |