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

(537 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

(20 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

(25 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

(26 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

(255 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

(41 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

(17 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)

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

(55 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

(17 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

(3 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

(69 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

(3 entries)

---

Global Index

A

AbstractHeapMachine [library]
AbstractSubstMachine [library]
allSub [lemma, in LM.Base.FiniteTypes.FinTypes]
all_Fin [definition, in LM.Base.FiniteTypes.Arbitrary]
Analysis [section, in LM.AbstractHeapMachine]
Analysis.H [variable, in LM.AbstractHeapMachine]
Analysis.i [variable, in LM.AbstractHeapMachine]
Analysis.R [variable, in LM.AbstractHeapMachine]
Analysis.s [variable, in LM.AbstractHeapMachine]
Analysis.T [variable, in LM.AbstractHeapMachine]
Analysis.V [variable, in LM.AbstractHeapMachine]
and_dec [instance, in LM.Base.Prelim]
app [constructor, in LM.L]
appendNil [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
appT [constructor, in LM.Programs]
app_closed [lemma, in LM.L]
app_equi_proper [instance, in LM.Base.Lists.BaseLists]
app_incl_proper [instance, in LM.Base.Lists.BaseLists]
Arbitrary [library]
ARS [library]
AutoIndTac [library]

B

Base [library]
BaseLists [library]
BasicDefinitions [library]
BasicFinTypes [library]
Bijection [library]
bijections [section, in LM.Base.Extra.Bijection]
bijections.A [variable, in LM.Base.Extra.Bijection]
bijections.B [variable, in LM.Base.Extra.Bijection]
bijective [definition, in LM.Base.Extra.Bijection]
bndApp [constructor, in LM.L]
bndlam [constructor, in LM.L]
bndvar [constructor, in LM.L]
bool_enum_ok [lemma, in LM.Base.FiniteTypes.BasicFinTypes]
bool_eq_dec [instance, in LM.Base.Prelim]
bool_dec [instance, in LM.Base.Prelim]
bool_Prop_false [lemma, in LM.Base.Prelim]
bool_Prop_true [lemma, in LM.Base.Prelim]
bound [inductive, in LM.L]
bound_subst [lemma, in LM.L]
bound_closed [lemma, in LM.L]
bound_ge [lemma, in LM.L]
bound_closed_k [lemma, in LM.L]
bound_unfolds_id [lemma, in LM.AbstractHeapMachine]

C

card [definition, in LM.Base.Lists.Cardinality]
Cardinality [section, in LM.Base.Lists.Cardinality]
Cardinality [library]
Cardinality.X [variable, in LM.Base.Lists.Cardinality]
card_equi_proper [instance, in LM.Base.Lists.Cardinality]
card_or [lemma, in LM.Base.Lists.Cardinality]
card_lt [lemma, in LM.Base.Lists.Cardinality]
card_equi [lemma, in LM.Base.Lists.Cardinality]
card_ex [lemma, in LM.Base.Lists.Cardinality]
card_0 [lemma, in LM.Base.Lists.Cardinality]
card_cons_rem [lemma, in LM.Base.Lists.Cardinality]
card_eq [lemma, in LM.Base.Lists.Cardinality]
card_le [lemma, in LM.Base.Lists.Cardinality]
card_not_in_rem [lemma, in LM.Base.Lists.Cardinality]
card_in_rem [lemma, in LM.Base.Lists.Cardinality]
card_cons' [lemma, in LM.Base.Lists.Cardinality]
card_cons [lemma, in LM.Base.Lists.Cardinality]
card_length_leq [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
cfind [lemma, in LM.Base.Lists.BaseLists]
class [projection, in LM.Base.FiniteTypes.FinTypes]
clos [inductive, in LM.AbstractHeapMachine]
closC [constructor, in LM.AbstractHeapMachine]
closed [definition, in LM.L]
closed_subst2 [lemma, in LM.L]
closed_app [lemma, in LM.L]
closed_subst [lemma, in LM.L]
closed_subst_iff [lemma, in LM.L]
closed_k_bound [lemma, in LM.L]
compile [definition, in LM.Programs]
compile_inj [lemma, in LM.Programs]
complete_induction [lemma, in LM.Base.Numbers]
CompoundFinTypes [library]
cons_equi_proper [instance, in LM.Base.Lists.BaseLists]
cons_incl_proper [instance, in LM.Base.Lists.BaseLists]
cons_incll [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
correctSpace [lemma, in LM.AbstractSubstMachine]
correctSpace [lemma, in LM.AbstractHeapMachine]
correctSpace' [lemma, in LM.AbstractSubstMachine]
correctTime [lemma, in LM.AbstractSubstMachine]
correctTime [lemma, in LM.AbstractHeapMachine]
correctTime' [lemma, in LM.AbstractSubstMachine]
correctTime' [lemma, in LM.AbstractHeapMachine]
count [definition, in LM.Base.FiniteTypes.BasicDefinitions]
countApp [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
countIn [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
countMap [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
countMapZero [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
countSplit [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
countZero [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
count_in_equiv [lemma, in LM.Base.FiniteTypes.BasicDefinitions]

D

Dec [definition, in LM.Base.Prelim]
dec [definition, in LM.Base.Prelim]
Decb [abbreviation, in LM.Base.Prelim]
decompile [definition, in LM.Programs]
decompile_correct' [lemma, in LM.Programs]
dec_transfer [lemma, in LM.Base.Prelim]
dec_DM_impl [lemma, in LM.Base.Prelim]
dec_DM_and [lemma, in LM.Base.Prelim]
dec_DN [lemma, in LM.Base.Prelim]
Dec_false [lemma, in LM.Base.Prelim]
Dec_true [lemma, in LM.Base.Prelim]
Dec_auto_not [lemma, in LM.Base.Prelim]
Dec_auto [lemma, in LM.Base.Prelim]
Dec_reflect_eq [lemma, in LM.Base.Prelim]
Dec_reflect [lemma, in LM.Base.Prelim]
disjoint [definition, in LM.Base.Lists.BaseLists]
disjoint_app [lemma, in LM.Base.Lists.BaseLists]
disjoint_cons [lemma, in LM.Base.Lists.BaseLists]
disjoint_nil' [lemma, in LM.Base.Lists.BaseLists]
disjoint_nil [lemma, in LM.Base.Lists.BaseLists]
disjoint_incl [lemma, in LM.Base.Lists.BaseLists]
disjoint_symm [lemma, in LM.Base.Lists.BaseLists]
disjoint_forall [lemma, in LM.Base.Lists.BaseLists]
DM_exists [lemma, in LM.Base.Prelim]
DM_or [lemma, in LM.Base.Prelim]
DM_exists [lemma, in LM.Base.FiniteTypes.FinTypes]
DM_notAll [lemma, in LM.Base.FiniteTypes.FinTypes]
do_unLock [lemma, in LM.Base.Tactics.Tactics]
do_Lock [lemma, in LM.Base.Tactics.Tactics]
Dupfree [section, in LM.Base.Lists.Dupfree]
dupfree [inductive, in LM.Base.Lists.Dupfree]
Dupfree [library]
dupfreeC [constructor, in LM.Base.Lists.Dupfree]
dupfreeCount [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
dupfreeN [constructor, in LM.Base.Lists.Dupfree]
dupfree_in_power [lemma, in LM.Base.Lists.Power]
dupfree_power [lemma, in LM.Base.Lists.Power]
dupfree_undup [lemma, in LM.Base.Lists.Dupfree]
dupfree_card [lemma, in LM.Base.Lists.Dupfree]
dupfree_dec [lemma, in LM.Base.Lists.Dupfree]
dupfree_filter [lemma, in LM.Base.Lists.Dupfree]
dupfree_map [lemma, in LM.Base.Lists.Dupfree]
dupfree_app [lemma, in LM.Base.Lists.Dupfree]
dupfree_cons [lemma, in LM.Base.Lists.Dupfree]
dupfree_elAt [lemma, in LM.Base.Lists.Position]
Dupfree.X [variable, in LM.Base.Lists.Dupfree]

E

elAt [definition, in LM.Base.Lists.Position]
elAt_el [lemma, in LM.Base.Lists.Position]
elAt_app [lemma, in LM.Base.Lists.Position]
elem [definition, in LM.Base.FiniteTypes.FinTypes]
elem_spec [lemma, in LM.Base.FiniteTypes.FinTypes]
el_elAt [lemma, in LM.Base.Lists.Position]
el_pos [lemma, in LM.Base.Lists.Position]
Empty_set_enum_ok [lemma, in LM.Base.FiniteTypes.BasicFinTypes]
Empty_set_eq_dec [instance, in LM.Base.Prelim]
enum [projection, in LM.Base.FiniteTypes.FinTypes]
enum_ok [projection, in LM.Base.FiniteTypes.FinTypes]
enum_ok_fromList [lemma, in LM.Base.FiniteTypes.Arbitrary]
eqType [record, in LM.Base.Prelim]
EqType [constructor, in LM.Base.Prelim]
eqType_dec [projection, in LM.Base.Prelim]
eqType_X [projection, in LM.Base.Prelim]
Equi [section, in LM.Base.Lists.BaseLists]
equi [definition, in LM.Base.Lists.BaseLists]
Equivalence_property_exists [lemma, in LM.Base.FiniteTypes.FinTypes]
Equivalence_property_all [lemma, in LM.Base.FiniteTypes.FinTypes]
equi_rotate [lemma, in LM.Base.Lists.BaseLists]
equi_shift [lemma, in LM.Base.Lists.BaseLists]
equi_swap [lemma, in LM.Base.Lists.BaseLists]
equi_dup [lemma, in LM.Base.Lists.BaseLists]
equi_push [lemma, in LM.Base.Lists.BaseLists]
equi_Equivalence [instance, in LM.Base.Lists.BaseLists]
Equi.X [variable, in LM.Base.Lists.BaseLists]
extended [definition, in LM.AbstractHeapMachine]
extended_PO [instance, in LM.AbstractHeapMachine]
Extra [library]

F

f [definition, in LM.AbstractHeapMachine]
False_enum_ok [lemma, in LM.Base.FiniteTypes.BasicFinTypes]
False_eq_dec [instance, in LM.Base.Prelim]
False_dec [instance, in LM.Base.Prelim]
filter [definition, in LM.Base.Lists.Filter]
Filter [section, in LM.Base.Lists.Filter]
Filter [library]
filter_comm [lemma, in LM.Base.Lists.Filter]
filter_and [lemma, in LM.Base.Lists.Filter]
filter_pq_eq [lemma, in LM.Base.Lists.Filter]
filter_pq_mono [lemma, in LM.Base.Lists.Filter]
filter_fst' [lemma, in LM.Base.Lists.Filter]
filter_fst [lemma, in LM.Base.Lists.Filter]
filter_app [lemma, in LM.Base.Lists.Filter]
filter_id [lemma, in LM.Base.Lists.Filter]
filter_mono [lemma, in LM.Base.Lists.Filter]
filter_incl [lemma, in LM.Base.Lists.Filter]
Filter.X [variable, in LM.Base.Lists.Filter]
finType [record, in LM.Base.FiniteTypes.FinTypes]
FinType [constructor, in LM.Base.FiniteTypes.FinTypes]
finTypeC [record, in LM.Base.FiniteTypes.FinTypes]
FinTypeC [constructor, in LM.Base.FiniteTypes.FinTypes]
finTypeC_False [instance, in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_True [instance, in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_unit [instance, in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_bool [instance, in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_Empty_set [instance, in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_sum [instance, in LM.Base.FiniteTypes.CompoundFinTypes]
finTypeC_Option [instance, in LM.Base.FiniteTypes.CompoundFinTypes]
finTypeC_Prod [instance, in LM.Base.FiniteTypes.CompoundFinTypes]
FinTypes [library]
finType_cc [definition, in LM.Base.FiniteTypes.FinTypes]
finType_exists_dec [instance, in LM.Base.FiniteTypes.FinTypes]
finType_forall_dec [instance, in LM.Base.FiniteTypes.FinTypes]
Fin_finTypeC [instance, in LM.Base.FiniteTypes.Arbitrary]
Fin_eq_dec [instance, in LM.Base.FiniteTypes.Arbitrary]
FixX [section, in LM.ARS]
FixX.X [variable, in LM.ARS]
Fix_X.X [variable, in LM.Base.Lists.Position]
Fix_X [section, in LM.Base.Lists.Position]
FP [definition, in LM.Base.Numbers]
fromListC [instance, in LM.Base.FiniteTypes.Arbitrary]
functional [definition, in LM.ARS]
f_correct_final [lemma, in LM.AbstractHeapMachine]
f_correct [lemma, in LM.AbstractHeapMachine]
f_correct' [lemma, in LM.AbstractHeapMachine]
f_mono [lemma, in LM.AbstractHeapMachine]

G

get [definition, in LM.AbstractHeapMachine]
getPosition [definition, in LM.Base.FiniteTypes.FinTypes]
getPosition_correct [lemma, in LM.Base.FiniteTypes.FinTypes]
get_current [lemma, in LM.AbstractHeapMachine]

H

heapEntry [inductive, in LM.AbstractHeapMachine]
heapEntryC [constructor, in LM.AbstractHeapMachine]
helperF [lemma, in LM.AbstractSubstMachine]
helperF' [lemma, in LM.AbstractSubstMachine]
helper2 [lemma, in LM.AbstractSubstMachine]

I

iff_dec [instance, in LM.Base.Prelim]
impl_dec [instance, in LM.Base.Prelim]
inclp [definition, in LM.Base.Lists.BaseLists]
Inclusion [section, in LM.Base.Lists.BaseLists]
Inclusion.X [variable, in LM.Base.Lists.BaseLists]
incl_equi_proper [instance, in LM.Base.Lists.BaseLists]
incl_preorder [instance, in LM.Base.Lists.BaseLists]
incl_app_left [lemma, in LM.Base.Lists.BaseLists]
incl_lrcons [lemma, in LM.Base.Lists.BaseLists]
incl_rcons [lemma, in LM.Base.Lists.BaseLists]
incl_sing [lemma, in LM.Base.Lists.BaseLists]
incl_lcons [lemma, in LM.Base.Lists.BaseLists]
incl_shift [lemma, in LM.Base.Lists.BaseLists]
incl_nil_eq [lemma, in LM.Base.Lists.BaseLists]
incl_map [lemma, in LM.Base.Lists.BaseLists]
incl_nil [lemma, in LM.Base.Lists.BaseLists]
InCount [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
index [definition, in LM.Base.FiniteTypes.FinTypes]
index_nth [lemma, in LM.Base.FiniteTypes.FinTypes]
init [definition, in LM.AbstractSubstMachine]
init [definition, in LM.AbstractHeapMachine]
injective [definition, in LM.Base.Extra.Bijection]
injective_index [lemma, in LM.Base.FiniteTypes.FinTypes]
inverse [definition, in LM.Base.Extra.Bijection]
inv2bij [lemma, in LM.Base.Extra.Bijection]
in_concat_iff [lemma, in LM.Base.Lists.BaseLists]
in_equi_proper [instance, in LM.Base.Lists.BaseLists]
in_incl_proper [instance, in LM.Base.Lists.BaseLists]
in_cons_neq [lemma, in LM.Base.Lists.BaseLists]
in_sing [lemma, in LM.Base.Lists.BaseLists]
in_filter_iff [lemma, in LM.Base.Lists.Filter]
in_undup_iff [lemma, in LM.Base.FiniteTypes.Arbitrary]
in_rem_iff [lemma, in LM.Base.Lists.Removal]
it [definition, in LM.Base.Numbers]
Iteration [section, in LM.Base.Numbers]
Iteration.f [variable, in LM.Base.Numbers]
Iteration.X [variable, in LM.Base.Numbers]
it_fp [lemma, in LM.Base.Numbers]
it_ind [lemma, in LM.Base.Numbers]

J

jumpTarget [definition, in LM.Programs]
jumpTarget_correct [lemma, in LM.Programs]
jumpTarget_eq [lemma, in LM.AbstractHeapMachine]

L

L [constructor, in LM.Base.Tactics.Tactics]
L [library]
lam [constructor, in LM.L]
lambda [definition, in LM.L]
lambda_lam [lemma, in LM.L]
lamT [constructor, in LM.Programs]
left_inv_inj [lemma, in LM.Base.Extra.Bijection]
left_inverse [definition, in LM.Base.Extra.Bijection]
length_TV [lemma, in LM.AbstractHeapMachine]
length_H [lemma, in LM.AbstractHeapMachine]
le_preorder [instance, in LM.Prelims]
Lin [section, in LM.AbstractHeapMachine]
Lin.HA [variable, in LM.AbstractHeapMachine]
Lin.Heap [variable, in LM.AbstractHeapMachine]
_ ! _ [notation, in LM.AbstractHeapMachine]
list_eq_dec [instance, in LM.Base.Prelim]
list_cc [lemma, in LM.Base.Lists.BaseLists]
list_exists_not_incl [lemma, in LM.Base.Lists.BaseLists]
list_exists_DM [lemma, in LM.Base.Lists.BaseLists]
list_exists_dec [instance, in LM.Base.Lists.BaseLists]
list_forall_dec [instance, in LM.Base.Lists.BaseLists]
list_in_dec [instance, in LM.Base.Lists.BaseLists]
list_cycle [lemma, in LM.Base.Lists.BaseLists]
list_bound [lemma, in LM.AbstractHeapMachine]
Lock [inductive, in LM.Base.Tactics.Tactics]
lookup [definition, in LM.AbstractHeapMachine]
lookup_el [lemma, in LM.AbstractHeapMachine]
lookup_extend [lemma, in LM.AbstractHeapMachine]

M

Membership [section, in LM.Base.Lists.BaseLists]
Membership.X [variable, in LM.Base.Lists.BaseLists]
mult_le_proper [instance, in LM.Prelims]

N

nat_eq_dec [instance, in LM.Base.Prelim]
nat_le_dec [instance, in LM.Base.Numbers]
NoneElement [lemma, in LM.Base.FiniteTypes.CompoundFinTypes]
notInZero [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
not_dec [instance, in LM.Base.Prelim]
not_in_cons [lemma, in LM.Base.Lists.BaseLists]
nth_error_Some_lt [lemma, in LM.Prelims]
nth_error_none [lemma, in LM.Base.Lists.Position]
NullMul [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
Numbers [library]

O

option_eq_dec [instance, in LM.Base.Prelim]
option_enum_ok [lemma, in LM.Base.FiniteTypes.CompoundFinTypes]
or_dec [instance, in LM.Base.Prelim]

P

pickx [definition, in LM.Base.FiniteTypes.FinTypes]
plus_le_proper [instance, in LM.Prelims]
pos [definition, in LM.Base.Lists.Position]
Position [library]
pos_def [definition, in LM.Base.FiniteTypes.FinTypes]
pos_length [lemma, in LM.Base.Lists.Position]
pos_second_S [lemma, in LM.Base.Lists.Position]
pos_first_S [lemma, in LM.Base.Lists.Position]
pos_None [lemma, in LM.Base.Lists.Position]
pos_elAt [lemma, in LM.Base.Lists.Position]
pow [definition, in LM.ARS]
power [definition, in LM.Base.Lists.Power]
Power [section, in LM.Base.Lists.Power]
Power [library]
PowerRep [section, in LM.Base.Lists.Power]
PowerRep.X [variable, in LM.Base.Lists.Power]
power_extensional [lemma, in LM.Base.Lists.Power]
power_nil [lemma, in LM.Base.Lists.Power]
power_incl [lemma, in LM.Base.Lists.Power]
Power.X [variable, in LM.Base.Lists.Power]
pow_step_congR [instance, in LM.L]
pow_step_congL [instance, in LM.L]
pow_add [lemma, in LM.ARS]
pow_star [lemma, in LM.ARS]
Prelim [library]
Prelims [library]
Pro [abbreviation, in LM.Programs]
ProdCount [lemma, in LM.Base.FiniteTypes.CompoundFinTypes]
prodLists [definition, in LM.Base.FiniteTypes.BasicDefinitions]
prod_eq_dec [instance, in LM.Base.Prelim]
prod_nil [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
prod_enum_ok [lemma, in LM.Base.FiniteTypes.CompoundFinTypes]
Programs [library]
proveOne [lemma, in LM.Base.FiniteTypes.CompoundFinTypes]
pure [definition, in LM.Base.FiniteTypes.Arbitrary]
pure_eq [lemma, in LM.Base.FiniteTypes.Arbitrary]
pure_impure [lemma, in LM.Base.FiniteTypes.Arbitrary]
pure_equiv [lemma, in LM.Base.FiniteTypes.Arbitrary]
purify [lemma, in LM.Base.FiniteTypes.Arbitrary]
put [definition, in LM.AbstractHeapMachine]
put_extends [lemma, in LM.AbstractHeapMachine]

R

rcomp [definition, in LM.ARS]
rcomp_1 [lemma, in LM.ARS]
redWithMaxSize [inductive, in LM.ARS]
redWithMaxSizeC [constructor, in LM.ARS]
redWithMaxSizeL [definition, in LM.L]
redWithMaxSizeL_congR [lemma, in LM.L]
redWithMaxSizeL_congL [lemma, in LM.L]
redWithMaxSizeR [constructor, in LM.ARS]
redWithMaxSizeS [definition, in LM.AbstractSubstMachine]
redWithMaxSize_trans [lemma, in LM.ARS]
redWithMaxSize_ge [lemma, in LM.ARS]
reflexive [definition, in LM.ARS]
rem [definition, in LM.Base.Lists.Removal]
Removal [section, in LM.Base.Lists.Removal]
Removal [library]
Removal.X [variable, in LM.Base.Lists.Removal]
rem_inclr [lemma, in LM.Base.Lists.Removal]
rem_reorder [lemma, in LM.Base.Lists.Removal]
rem_id [lemma, in LM.Base.Lists.Removal]
rem_fst' [lemma, in LM.Base.Lists.Removal]
rem_fst [lemma, in LM.Base.Lists.Removal]
rem_comm [lemma, in LM.Base.Lists.Removal]
rem_equi [lemma, in LM.Base.Lists.Removal]
rem_app' [lemma, in LM.Base.Lists.Removal]
rem_app [lemma, in LM.Base.Lists.Removal]
rem_neq [lemma, in LM.Base.Lists.Removal]
rem_in [lemma, in LM.Base.Lists.Removal]
rem_cons' [lemma, in LM.Base.Lists.Removal]
rem_cons [lemma, in LM.Base.Lists.Removal]
rem_mono [lemma, in LM.Base.Lists.Removal]
rem_incl [lemma, in LM.Base.Lists.Removal]
rem_not_in [lemma, in LM.Base.Lists.Removal]
rep [definition, in LM.Base.Lists.Power]
replace [definition, in LM.Base.Lists.Position]
replace_pos [lemma, in LM.Base.Lists.Position]
replace_diff [lemma, in LM.Base.Lists.Position]
replace_same [lemma, in LM.Base.Lists.Position]
reprC [inductive, in LM.AbstractHeapMachine]
reprCC [constructor, in LM.AbstractHeapMachine]
reprC_extend [lemma, in LM.AbstractHeapMachine]
reprP [inductive, in LM.Programs]
reprPC [constructor, in LM.Programs]
rep_dupfree [lemma, in LM.Base.Lists.Power]
rep_idempotent [lemma, in LM.Base.Lists.Power]
rep_injective [lemma, in LM.Base.Lists.Power]
rep_eq [lemma, in LM.Base.Lists.Power]
rep_eq' [lemma, in LM.Base.Lists.Power]
rep_mono [lemma, in LM.Base.Lists.Power]
rep_equi [lemma, in LM.Base.Lists.Power]
rep_in [lemma, in LM.Base.Lists.Power]
rep_incl [lemma, in LM.Base.Lists.Power]
rep_power [lemma, in LM.Base.Lists.Power]
rep_cons_eq [lemma, in LM.Base.Lists.Power]
rep_cons' [lemma, in LM.Base.Lists.Power]
rep_cons [lemma, in LM.Base.Lists.Power]
retT [constructor, in LM.Programs]
right_inv_surj [lemma, in LM.Base.Extra.Bijection]
right_inverse [definition, in LM.Base.Extra.Bijection]
R_star [lemma, in LM.ARS]

S

size [definition, in LM.L]
sizeC [definition, in LM.AbstractHeapMachine]
sizeH [definition, in LM.AbstractHeapMachine]
sizeHE [definition, in LM.AbstractHeapMachine]
sizeP [definition, in LM.Programs]
sizeP_size [lemma, in LM.Programs]
sizeP_size' [lemma, in LM.Programs]
sizeSt [definition, in LM.AbstractHeapMachine]
sizeT [definition, in LM.Programs]
size_recursion [lemma, in LM.Base.Numbers]
size_induction [lemma, in LM.Base.Numbers]
size_geq_1 [lemma, in LM.Programs]
size_clos [lemma, in LM.AbstractHeapMachine]
SomeElement [lemma, in LM.Base.FiniteTypes.CompoundFinTypes]
spaceBS [inductive, in LM.L]
spaceBSBeta [constructor, in LM.L]
spaceBSVal [constructor, in LM.L]
spaceBS_correct [lemma, in LM.L]
spaceBS_ge [lemma, in LM.L]
star [inductive, in LM.ARS]
starC [constructor, in LM.ARS]
starR [constructor, in LM.ARS]
star_pow [lemma, in LM.ARS]
star_PO [instance, in LM.ARS]
star_trans [lemma, in LM.ARS]
state [abbreviation, in LM.AbstractSubstMachine]
state [definition, in LM.AbstractHeapMachine]
step [inductive, in LM.AbstractSubstMachine]
step [inductive, in LM.L]
step [inductive, in LM.AbstractHeapMachine]
stepApp [constructor, in LM.L]
stepAppL [constructor, in LM.L]
stepAppR [constructor, in LM.L]
step_beta [constructor, in LM.AbstractSubstMachine]
step_pushVal [constructor, in LM.AbstractSubstMachine]
step_evaluatesSpace [lemma, in LM.L]
step_evaluatesIn [lemma, in LM.L]
step_nil [constructor, in LM.AbstractHeapMachine]
step_load [constructor, in LM.AbstractHeapMachine]
step_beta [constructor, in LM.AbstractHeapMachine]
step_pushVal [constructor, in LM.AbstractHeapMachine]
subst [definition, in LM.L]
substP [definition, in LM.Programs]
substP_correct [lemma, in LM.Programs]
substP_correct' [lemma, in LM.Programs]
subtype [definition, in LM.Base.FiniteTypes.Arbitrary]
subType_eq_dec [instance, in LM.Base.FiniteTypes.Arbitrary]
subtype_extensionality [lemma, in LM.Base.FiniteTypes.Arbitrary]
sum [definition, in LM.Programs]
sum_eq_dec [instance, in LM.Base.Prelim]
sum_enum_ok [lemma, in LM.Base.FiniteTypes.CompoundFinTypes]
sum_app [lemma, in LM.Programs]
surjective [definition, in LM.Base.Extra.Bijection]
symmetric [definition, in LM.ARS]
S_le_proper [instance, in LM.Prelims]

T

Tactics [library]
tc [definition, in LM.AbstractSubstMachine]
tc_compile [lemma, in LM.AbstractSubstMachine]
term [inductive, in LM.L]
term_eq_dec [instance, in LM.L]
timeBS [inductive, in LM.L]
timeBSBeta [constructor, in LM.L]
timeBSVal [constructor, in LM.L]
timeBS_correct [lemma, in LM.L]
Tok [inductive, in LM.Programs]
toOptionList [definition, in LM.Base.FiniteTypes.BasicDefinitions]
toSubList [definition, in LM.Base.FiniteTypes.Arbitrary]
toSubList_count [lemma, in LM.Base.FiniteTypes.Arbitrary]
toSumList1 [definition, in LM.Base.FiniteTypes.BasicDefinitions]
toSumList1_missing [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
toSumList1_count [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
toSumList2 [definition, in LM.Base.FiniteTypes.BasicDefinitions]
toSumList2_missing [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
toSumList2_count [lemma, in LM.Base.FiniteTypes.BasicDefinitions]
transitive [definition, in LM.ARS]
True_enum_ok [lemma, in LM.Base.FiniteTypes.BasicFinTypes]
True_eq_dec [instance, in LM.Base.Prelim]
True_dec [instance, in LM.Base.Prelim]
type [projection, in LM.Base.FiniteTypes.FinTypes]

U

undup [definition, in LM.Base.Lists.Dupfree]
Undup [section, in LM.Base.Lists.Dupfree]
undup_idempotent [lemma, in LM.Base.Lists.Dupfree]
undup_id [lemma, in LM.Base.Lists.Dupfree]
undup_equi [lemma, in LM.Base.Lists.Dupfree]
undup_incl [lemma, in LM.Base.Lists.Dupfree]
undup_id_equi [lemma, in LM.Base.Lists.Dupfree]
Undup.X [variable, in LM.Base.Lists.Dupfree]
UnfoldPro [section, in LM.AbstractHeapMachine]
UnfoldPro.H [variable, in LM.AbstractHeapMachine]
unfolds [inductive, in LM.AbstractHeapMachine]
unfoldsApp [constructor, in LM.AbstractHeapMachine]
unfoldsBound [constructor, in LM.AbstractHeapMachine]
unfoldsLam [constructor, in LM.AbstractHeapMachine]
unfoldsUnbound [constructor, in LM.AbstractHeapMachine]
unfolds_inj [lemma, in LM.AbstractHeapMachine]
unfolds_extend [lemma, in LM.AbstractHeapMachine]
unfolds_subst [lemma, in LM.AbstractHeapMachine]
unfolds_subst' [lemma, in LM.AbstractHeapMachine]
unfolds_bound [lemma, in LM.AbstractHeapMachine]
unit_enum_ok [lemma, in LM.Base.FiniteTypes.BasicFinTypes]
unit_eq_dec [instance, in LM.Base.Prelim]

V

var [constructor, in LM.L]
varT [constructor, in LM.Programs]
Vectors [library]
Vector_replace_nth2 [lemma, in LM.Base.Extra.Vectors]
Vector_replace_nth [lemma, in LM.Base.Extra.Vectors]

other

[| _ ; _ ; .. ; _ |] (vector_scope) [notation, in LM.Base.Extra.Vectors]
[| _ |] (vector_scope) [notation, in LM.Base.Extra.Vectors]
_ ::: _ (vector_scope) [notation, in LM.Base.Extra.Vectors]
[||] (vector_scope) [notation, in LM.Base.Extra.Vectors]
_ >> _ [notation, in LM.L]
_ [@ _ ] [notation, in LM.Base.Extra.Vectors]
_ === _ [notation, in LM.Base.Lists.BaseLists]
_ <<= _ [notation, in LM.Base.Lists.BaseLists]
_ el _ [notation, in LM.Base.Lists.BaseLists]
_ =2 _ [notation, in LM.ARS]
_ <=2 _ [notation, in LM.ARS]
_ =1 _ [notation, in LM.ARS]
_ <=1 _ [notation, in LM.ARS]
_ .[ _ ] [notation, in LM.Base.Lists.Position]
_ ! _ [notation, in LM.AbstractHeapMachine]
eq_dec _ [notation, in LM.Base.Prelim]
Subtype _ [notation, in LM.Base.FiniteTypes.Arbitrary]
(λ _ ) [notation, in LM.L]
| _ | [notation, in LM.Base.Lists.BaseLists]

---

Notation Index

L

_ ! _ [in LM.AbstractHeapMachine]

other

[| _ ; _ ; .. ; _ |] (vector_scope) [in LM.Base.Extra.Vectors]
[| _ |] (vector_scope) [in LM.Base.Extra.Vectors]
_ ::: _ (vector_scope) [in LM.Base.Extra.Vectors]
[||] (vector_scope) [in LM.Base.Extra.Vectors]
_ >> _ [in LM.L]
_ [@ _ ] [in LM.Base.Extra.Vectors]
_ === _ [in LM.Base.Lists.BaseLists]
_ <<= _ [in LM.Base.Lists.BaseLists]
_ el _ [in LM.Base.Lists.BaseLists]
_ =2 _ [in LM.ARS]
_ <=2 _ [in LM.ARS]
_ =1 _ [in LM.ARS]
_ <=1 _ [in LM.ARS]
_ .[ _ ] [in LM.Base.Lists.Position]
_ ! _ [in LM.AbstractHeapMachine]
eq_dec _ [in LM.Base.Prelim]
Subtype _ [in LM.Base.FiniteTypes.Arbitrary]
(λ _ ) [in LM.L]
| _ | [in LM.Base.Lists.BaseLists]

---

Variable Index

A

Analysis.H [in LM.AbstractHeapMachine]
Analysis.i [in LM.AbstractHeapMachine]
Analysis.R [in LM.AbstractHeapMachine]
Analysis.s [in LM.AbstractHeapMachine]
Analysis.T [in LM.AbstractHeapMachine]
Analysis.V [in LM.AbstractHeapMachine]

B

bijections.A [in LM.Base.Extra.Bijection]
bijections.B [in LM.Base.Extra.Bijection]

C

Cardinality.X [in LM.Base.Lists.Cardinality]

D

Dupfree.X [in LM.Base.Lists.Dupfree]

E

Equi.X [in LM.Base.Lists.BaseLists]

F

Filter.X [in LM.Base.Lists.Filter]
FixX.X [in LM.ARS]
Fix_X.X [in LM.Base.Lists.Position]

I

Inclusion.X [in LM.Base.Lists.BaseLists]
Iteration.f [in LM.Base.Numbers]
Iteration.X [in LM.Base.Numbers]

L

Lin.HA [in LM.AbstractHeapMachine]
Lin.Heap [in LM.AbstractHeapMachine]

M

Membership.X [in LM.Base.Lists.BaseLists]

P

PowerRep.X [in LM.Base.Lists.Power]
Power.X [in LM.Base.Lists.Power]

R

Removal.X [in LM.Base.Lists.Removal]

U

Undup.X [in LM.Base.Lists.Dupfree]
UnfoldPro.H [in LM.AbstractHeapMachine]

---

Library Index

A

AbstractHeapMachine
AbstractSubstMachine
Arbitrary
ARS
AutoIndTac

B

Base
BaseLists
BasicDefinitions
BasicFinTypes
Bijection

C

Cardinality
CompoundFinTypes

D

Dupfree

E

Extra

F

Filter
FinTypes

L

L

N

Numbers

P

Position
Power
Prelim
Prelims
Programs

R

Removal

T

Tactics

V

Vectors

---

Lemma Index

A

allSub [in LM.Base.FiniteTypes.FinTypes]
appendNil [in LM.Base.FiniteTypes.BasicDefinitions]
app_closed [in LM.L]

B

bool_enum_ok [in LM.Base.FiniteTypes.BasicFinTypes]
bool_Prop_false [in LM.Base.Prelim]
bool_Prop_true [in LM.Base.Prelim]
bound_subst [in LM.L]
bound_closed [in LM.L]
bound_ge [in LM.L]
bound_closed_k [in LM.L]
bound_unfolds_id [in LM.AbstractHeapMachine]

C

card_or [in LM.Base.Lists.Cardinality]
card_lt [in LM.Base.Lists.Cardinality]
card_equi [in LM.Base.Lists.Cardinality]
card_ex [in LM.Base.Lists.Cardinality]
card_0 [in LM.Base.Lists.Cardinality]
card_cons_rem [in LM.Base.Lists.Cardinality]
card_eq [in LM.Base.Lists.Cardinality]
card_le [in LM.Base.Lists.Cardinality]
card_not_in_rem [in LM.Base.Lists.Cardinality]
card_in_rem [in LM.Base.Lists.Cardinality]
card_cons' [in LM.Base.Lists.Cardinality]
card_cons [in LM.Base.Lists.Cardinality]
card_length_leq [in LM.Base.FiniteTypes.BasicDefinitions]
cfind [in LM.Base.Lists.BaseLists]
closed_subst2 [in LM.L]
closed_app [in LM.L]
closed_subst [in LM.L]
closed_subst_iff [in LM.L]
closed_k_bound [in LM.L]
compile_inj [in LM.Programs]
complete_induction [in LM.Base.Numbers]
cons_incll [in LM.Base.FiniteTypes.BasicDefinitions]
correctSpace [in LM.AbstractSubstMachine]
correctSpace [in LM.AbstractHeapMachine]
correctSpace' [in LM.AbstractSubstMachine]
correctTime [in LM.AbstractSubstMachine]
correctTime [in LM.AbstractHeapMachine]
correctTime' [in LM.AbstractSubstMachine]
correctTime' [in LM.AbstractHeapMachine]
countApp [in LM.Base.FiniteTypes.BasicDefinitions]
countIn [in LM.Base.FiniteTypes.BasicDefinitions]
countMap [in LM.Base.FiniteTypes.BasicDefinitions]
countMapZero [in LM.Base.FiniteTypes.BasicDefinitions]
countSplit [in LM.Base.FiniteTypes.BasicDefinitions]
countZero [in LM.Base.FiniteTypes.BasicDefinitions]
count_in_equiv [in LM.Base.FiniteTypes.BasicDefinitions]

D

decompile_correct' [in LM.Programs]
dec_transfer [in LM.Base.Prelim]
dec_DM_impl [in LM.Base.Prelim]
dec_DM_and [in LM.Base.Prelim]
dec_DN [in LM.Base.Prelim]
Dec_false [in LM.Base.Prelim]
Dec_true [in LM.Base.Prelim]
Dec_auto_not [in LM.Base.Prelim]
Dec_auto [in LM.Base.Prelim]
Dec_reflect_eq [in LM.Base.Prelim]
Dec_reflect [in LM.Base.Prelim]
disjoint_app [in LM.Base.Lists.BaseLists]
disjoint_cons [in LM.Base.Lists.BaseLists]
disjoint_nil' [in LM.Base.Lists.BaseLists]
disjoint_nil [in LM.Base.Lists.BaseLists]
disjoint_incl [in LM.Base.Lists.BaseLists]
disjoint_symm [in LM.Base.Lists.BaseLists]
disjoint_forall [in LM.Base.Lists.BaseLists]
DM_exists [in LM.Base.Prelim]
DM_or [in LM.Base.Prelim]
DM_exists [in LM.Base.FiniteTypes.FinTypes]
DM_notAll [in LM.Base.FiniteTypes.FinTypes]
do_unLock [in LM.Base.Tactics.Tactics]
do_Lock [in LM.Base.Tactics.Tactics]
dupfreeCount [in LM.Base.FiniteTypes.BasicDefinitions]
dupfree_in_power [in LM.Base.Lists.Power]
dupfree_power [in LM.Base.Lists.Power]
dupfree_undup [in LM.Base.Lists.Dupfree]
dupfree_card [in LM.Base.Lists.Dupfree]
dupfree_dec [in LM.Base.Lists.Dupfree]
dupfree_filter [in LM.Base.Lists.Dupfree]
dupfree_map [in LM.Base.Lists.Dupfree]
dupfree_app [in LM.Base.Lists.Dupfree]
dupfree_cons [in LM.Base.Lists.Dupfree]
dupfree_elAt [in LM.Base.Lists.Position]

E

elAt_el [in LM.Base.Lists.Position]
elAt_app [in LM.Base.Lists.Position]
elem_spec [in LM.Base.FiniteTypes.FinTypes]
el_elAt [in LM.Base.Lists.Position]
el_pos [in LM.Base.Lists.Position]
Empty_set_enum_ok [in LM.Base.FiniteTypes.BasicFinTypes]
enum_ok_fromList [in LM.Base.FiniteTypes.Arbitrary]
Equivalence_property_exists [in LM.Base.FiniteTypes.FinTypes]
Equivalence_property_all [in LM.Base.FiniteTypes.FinTypes]
equi_rotate [in LM.Base.Lists.BaseLists]
equi_shift [in LM.Base.Lists.BaseLists]
equi_swap [in LM.Base.Lists.BaseLists]
equi_dup [in LM.Base.Lists.BaseLists]
equi_push [in LM.Base.Lists.BaseLists]

F

False_enum_ok [in LM.Base.FiniteTypes.BasicFinTypes]
filter_comm [in LM.Base.Lists.Filter]
filter_and [in LM.Base.Lists.Filter]
filter_pq_eq [in LM.Base.Lists.Filter]
filter_pq_mono [in LM.Base.Lists.Filter]
filter_fst' [in LM.Base.Lists.Filter]
filter_fst [in LM.Base.Lists.Filter]
filter_app [in LM.Base.Lists.Filter]
filter_id [in LM.Base.Lists.Filter]
filter_mono [in LM.Base.Lists.Filter]
filter_incl [in LM.Base.Lists.Filter]
f_correct_final [in LM.AbstractHeapMachine]
f_correct [in LM.AbstractHeapMachine]
f_correct' [in LM.AbstractHeapMachine]
f_mono [in LM.AbstractHeapMachine]

G

getPosition_correct [in LM.Base.FiniteTypes.FinTypes]
get_current [in LM.AbstractHeapMachine]

H

helperF [in LM.AbstractSubstMachine]
helperF' [in LM.AbstractSubstMachine]
helper2 [in LM.AbstractSubstMachine]

I

incl_app_left [in LM.Base.Lists.BaseLists]
incl_lrcons [in LM.Base.Lists.BaseLists]
incl_rcons [in LM.Base.Lists.BaseLists]
incl_sing [in LM.Base.Lists.BaseLists]
incl_lcons [in LM.Base.Lists.BaseLists]
incl_shift [in LM.Base.Lists.BaseLists]
incl_nil_eq [in LM.Base.Lists.BaseLists]
incl_map [in LM.Base.Lists.BaseLists]
incl_nil [in LM.Base.Lists.BaseLists]
InCount [in LM.Base.FiniteTypes.BasicDefinitions]
index_nth [in LM.Base.FiniteTypes.FinTypes]
injective_index [in LM.Base.FiniteTypes.FinTypes]
inv2bij [in LM.Base.Extra.Bijection]
in_concat_iff [in LM.Base.Lists.BaseLists]
in_cons_neq [in LM.Base.Lists.BaseLists]
in_sing [in LM.Base.Lists.BaseLists]
in_filter_iff [in LM.Base.Lists.Filter]
in_undup_iff [in LM.Base.FiniteTypes.Arbitrary]
in_rem_iff [in LM.Base.Lists.Removal]
it_fp [in LM.Base.Numbers]
it_ind [in LM.Base.Numbers]

J

jumpTarget_correct [in LM.Programs]
jumpTarget_eq [in LM.AbstractHeapMachine]

L

lambda_lam [in LM.L]
left_inv_inj [in LM.Base.Extra.Bijection]
length_TV [in LM.AbstractHeapMachine]
length_H [in LM.AbstractHeapMachine]
list_cc [in LM.Base.Lists.BaseLists]
list_exists_not_incl [in LM.Base.Lists.BaseLists]
list_exists_DM [in LM.Base.Lists.BaseLists]
list_cycle [in LM.Base.Lists.BaseLists]
list_bound [in LM.AbstractHeapMachine]
lookup_el [in LM.AbstractHeapMachine]
lookup_extend [in LM.AbstractHeapMachine]

N

NoneElement [in LM.Base.FiniteTypes.CompoundFinTypes]
notInZero [in LM.Base.FiniteTypes.BasicDefinitions]
not_in_cons [in LM.Base.Lists.BaseLists]
nth_error_Some_lt [in LM.Prelims]
nth_error_none [in LM.Base.Lists.Position]
NullMul [in LM.Base.FiniteTypes.BasicDefinitions]

O

option_enum_ok [in LM.Base.FiniteTypes.CompoundFinTypes]

P

pos_length [in LM.Base.Lists.Position]
pos_second_S [in LM.Base.Lists.Position]
pos_first_S [in LM.Base.Lists.Position]
pos_None [in LM.Base.Lists.Position]
pos_elAt [in LM.Base.Lists.Position]
power_extensional [in LM.Base.Lists.Power]
power_nil [in LM.Base.Lists.Power]
power_incl [in LM.Base.Lists.Power]
pow_add [in LM.ARS]
pow_star [in LM.ARS]
ProdCount [in LM.Base.FiniteTypes.CompoundFinTypes]
prod_nil [in LM.Base.FiniteTypes.BasicDefinitions]
prod_enum_ok [in LM.Base.FiniteTypes.CompoundFinTypes]
proveOne [in LM.Base.FiniteTypes.CompoundFinTypes]
pure_eq [in LM.Base.FiniteTypes.Arbitrary]
pure_impure [in LM.Base.FiniteTypes.Arbitrary]
pure_equiv [in LM.Base.FiniteTypes.Arbitrary]
purify [in LM.Base.FiniteTypes.Arbitrary]
put_extends [in LM.AbstractHeapMachine]

R

rcomp_1 [in LM.ARS]
redWithMaxSizeL_congR [in LM.L]
redWithMaxSizeL_congL [in LM.L]
redWithMaxSize_trans [in LM.ARS]
redWithMaxSize_ge [in LM.ARS]
rem_inclr [in LM.Base.Lists.Removal]
rem_reorder [in LM.Base.Lists.Removal]
rem_id [in LM.Base.Lists.Removal]
rem_fst' [in LM.Base.Lists.Removal]
rem_fst [in LM.Base.Lists.Removal]
rem_comm [in LM.Base.Lists.Removal]
rem_equi [in LM.Base.Lists.Removal]
rem_app' [in LM.Base.Lists.Removal]
rem_app [in LM.Base.Lists.Removal]
rem_neq [in LM.Base.Lists.Removal]
rem_in [in LM.Base.Lists.Removal]
rem_cons' [in LM.Base.Lists.Removal]
rem_cons [in LM.Base.Lists.Removal]
rem_mono [in LM.Base.Lists.Removal]
rem_incl [in LM.Base.Lists.Removal]
rem_not_in [in LM.Base.Lists.Removal]
replace_pos [in LM.Base.Lists.Position]
replace_diff [in LM.Base.Lists.Position]
replace_same [in LM.Base.Lists.Position]
reprC_extend [in LM.AbstractHeapMachine]
rep_dupfree [in LM.Base.Lists.Power]
rep_idempotent [in LM.Base.Lists.Power]
rep_injective [in LM.Base.Lists.Power]
rep_eq [in LM.Base.Lists.Power]
rep_eq' [in LM.Base.Lists.Power]
rep_mono [in LM.Base.Lists.Power]
rep_equi [in LM.Base.Lists.Power]
rep_in [in LM.Base.Lists.Power]
rep_incl [in LM.Base.Lists.Power]
rep_power [in LM.Base.Lists.Power]
rep_cons_eq [in LM.Base.Lists.Power]
rep_cons' [in LM.Base.Lists.Power]
rep_cons [in LM.Base.Lists.Power]
right_inv_surj [in LM.Base.Extra.Bijection]
R_star [in LM.ARS]

S

sizeP_size [in LM.Programs]
sizeP_size' [in LM.Programs]
size_recursion [in LM.Base.Numbers]
size_induction [in LM.Base.Numbers]
size_geq_1 [in LM.Programs]
size_clos [in LM.AbstractHeapMachine]
SomeElement [in LM.Base.FiniteTypes.CompoundFinTypes]
spaceBS_correct [in LM.L]
spaceBS_ge [in LM.L]
star_pow [in LM.ARS]
star_trans [in LM.ARS]
step_evaluatesSpace [in LM.L]
step_evaluatesIn [in LM.L]
substP_correct [in LM.Programs]
substP_correct' [in LM.Programs]
subtype_extensionality [in LM.Base.FiniteTypes.Arbitrary]
sum_enum_ok [in LM.Base.FiniteTypes.CompoundFinTypes]
sum_app [in LM.Programs]

T

tc_compile [in LM.AbstractSubstMachine]
timeBS_correct [in LM.L]
toSubList_count [in LM.Base.FiniteTypes.Arbitrary]
toSumList1_missing [in LM.Base.FiniteTypes.BasicDefinitions]
toSumList1_count [in LM.Base.FiniteTypes.BasicDefinitions]
toSumList2_missing [in LM.Base.FiniteTypes.BasicDefinitions]
toSumList2_count [in LM.Base.FiniteTypes.BasicDefinitions]
True_enum_ok [in LM.Base.FiniteTypes.BasicFinTypes]

U

undup_idempotent [in LM.Base.Lists.Dupfree]
undup_id [in LM.Base.Lists.Dupfree]
undup_equi [in LM.Base.Lists.Dupfree]
undup_incl [in LM.Base.Lists.Dupfree]
undup_id_equi [in LM.Base.Lists.Dupfree]
unfolds_inj [in LM.AbstractHeapMachine]
unfolds_extend [in LM.AbstractHeapMachine]
unfolds_subst [in LM.AbstractHeapMachine]
unfolds_subst' [in LM.AbstractHeapMachine]
unfolds_bound [in LM.AbstractHeapMachine]
unit_enum_ok [in LM.Base.FiniteTypes.BasicFinTypes]

V

Vector_replace_nth2 [in LM.Base.Extra.Vectors]
Vector_replace_nth [in LM.Base.Extra.Vectors]

---

Constructor Index

A

app [in LM.L]
appT [in LM.Programs]

B

bndApp [in LM.L]
bndlam [in LM.L]
bndvar [in LM.L]

C

closC [in LM.AbstractHeapMachine]

D

dupfreeC [in LM.Base.Lists.Dupfree]
dupfreeN [in LM.Base.Lists.Dupfree]

E

EqType [in LM.Base.Prelim]

F

FinType [in LM.Base.FiniteTypes.FinTypes]
FinTypeC [in LM.Base.FiniteTypes.FinTypes]

H

heapEntryC [in LM.AbstractHeapMachine]

L

L [in LM.Base.Tactics.Tactics]
lam [in LM.L]
lamT [in LM.Programs]

R

redWithMaxSizeC [in LM.ARS]
redWithMaxSizeR [in LM.ARS]
reprCC [in LM.AbstractHeapMachine]
reprPC [in LM.Programs]
retT [in LM.Programs]

S

spaceBSBeta [in LM.L]
spaceBSVal [in LM.L]
starC [in LM.ARS]
starR [in LM.ARS]
stepApp [in LM.L]
stepAppL [in LM.L]
stepAppR [in LM.L]
step_beta [in LM.AbstractSubstMachine]
step_pushVal [in LM.AbstractSubstMachine]
step_nil [in LM.AbstractHeapMachine]
step_load [in LM.AbstractHeapMachine]
step_beta [in LM.AbstractHeapMachine]
step_pushVal [in LM.AbstractHeapMachine]

T

timeBSBeta [in LM.L]
timeBSVal [in LM.L]

U

unfoldsApp [in LM.AbstractHeapMachine]
unfoldsBound [in LM.AbstractHeapMachine]
unfoldsLam [in LM.AbstractHeapMachine]
unfoldsUnbound [in LM.AbstractHeapMachine]

V

var [in LM.L]
varT [in LM.Programs]

---

Inductive Index

B

bound [in LM.L]

C

clos [in LM.AbstractHeapMachine]

D

dupfree [in LM.Base.Lists.Dupfree]

H

heapEntry [in LM.AbstractHeapMachine]

L

Lock [in LM.Base.Tactics.Tactics]

R

redWithMaxSize [in LM.ARS]
reprC [in LM.AbstractHeapMachine]
reprP [in LM.Programs]

S

spaceBS [in LM.L]
star [in LM.ARS]
step [in LM.AbstractSubstMachine]
step [in LM.L]
step [in LM.AbstractHeapMachine]

T

term [in LM.L]
timeBS [in LM.L]
Tok [in LM.Programs]

U

unfolds [in LM.AbstractHeapMachine]

---

Projection Index

C

class [in LM.Base.FiniteTypes.FinTypes]

E

enum [in LM.Base.FiniteTypes.FinTypes]
enum_ok [in LM.Base.FiniteTypes.FinTypes]
eqType_dec [in LM.Base.Prelim]
eqType_X [in LM.Base.Prelim]

T

type [in LM.Base.FiniteTypes.FinTypes]

---

Instance Index

A

and_dec [in LM.Base.Prelim]
app_equi_proper [in LM.Base.Lists.BaseLists]
app_incl_proper [in LM.Base.Lists.BaseLists]

B

bool_eq_dec [in LM.Base.Prelim]
bool_dec [in LM.Base.Prelim]

C

card_equi_proper [in LM.Base.Lists.Cardinality]
cons_equi_proper [in LM.Base.Lists.BaseLists]
cons_incl_proper [in LM.Base.Lists.BaseLists]

E

Empty_set_eq_dec [in LM.Base.Prelim]
equi_Equivalence [in LM.Base.Lists.BaseLists]
extended_PO [in LM.AbstractHeapMachine]

F

False_eq_dec [in LM.Base.Prelim]
False_dec [in LM.Base.Prelim]
finTypeC_False [in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_True [in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_unit [in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_bool [in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_Empty_set [in LM.Base.FiniteTypes.BasicFinTypes]
finTypeC_sum [in LM.Base.FiniteTypes.CompoundFinTypes]
finTypeC_Option [in LM.Base.FiniteTypes.CompoundFinTypes]
finTypeC_Prod [in LM.Base.FiniteTypes.CompoundFinTypes]
finType_exists_dec [in LM.Base.FiniteTypes.FinTypes]
finType_forall_dec [in LM.Base.FiniteTypes.FinTypes]
Fin_finTypeC [in LM.Base.FiniteTypes.Arbitrary]
Fin_eq_dec [in LM.Base.FiniteTypes.Arbitrary]
fromListC [in LM.Base.FiniteTypes.Arbitrary]

I

iff_dec [in LM.Base.Prelim]
impl_dec [in LM.Base.Prelim]
incl_equi_proper [in LM.Base.Lists.BaseLists]
incl_preorder [in LM.Base.Lists.BaseLists]
in_equi_proper [in LM.Base.Lists.BaseLists]
in_incl_proper [in LM.Base.Lists.BaseLists]

L

le_preorder [in LM.Prelims]
list_eq_dec [in LM.Base.Prelim]
list_exists_dec [in LM.Base.Lists.BaseLists]
list_forall_dec [in LM.Base.Lists.BaseLists]
list_in_dec [in LM.Base.Lists.BaseLists]

M

mult_le_proper [in LM.Prelims]

N

nat_eq_dec [in LM.Base.Prelim]
nat_le_dec [in LM.Base.Numbers]
not_dec [in LM.Base.Prelim]

O

option_eq_dec [in LM.Base.Prelim]
or_dec [in LM.Base.Prelim]

P

plus_le_proper [in LM.Prelims]
pow_step_congR [in LM.L]
pow_step_congL [in LM.L]
prod_eq_dec [in LM.Base.Prelim]

S

star_PO [in LM.ARS]
subType_eq_dec [in LM.Base.FiniteTypes.Arbitrary]
sum_eq_dec [in LM.Base.Prelim]
S_le_proper [in LM.Prelims]

T

term_eq_dec [in LM.L]
True_eq_dec [in LM.Base.Prelim]
True_dec [in LM.Base.Prelim]

U

unit_eq_dec [in LM.Base.Prelim]

---

Section Index

A

Analysis [in LM.AbstractHeapMachine]

B

bijections [in LM.Base.Extra.Bijection]

C

Cardinality [in LM.Base.Lists.Cardinality]

D

Dupfree [in LM.Base.Lists.Dupfree]

E

Equi [in LM.Base.Lists.BaseLists]

F

Filter [in LM.Base.Lists.Filter]
FixX [in LM.ARS]
Fix_X [in LM.Base.Lists.Position]

I

Inclusion [in LM.Base.Lists.BaseLists]
Iteration [in LM.Base.Numbers]

L

Lin [in LM.AbstractHeapMachine]

M

Membership [in LM.Base.Lists.BaseLists]

P

Power [in LM.Base.Lists.Power]
PowerRep [in LM.Base.Lists.Power]

R

Removal [in LM.Base.Lists.Removal]

U

Undup [in LM.Base.Lists.Dupfree]
UnfoldPro [in LM.AbstractHeapMachine]

---

Abbreviation Index

D

Decb [in LM.Base.Prelim]

P

Pro [in LM.Programs]

S

state [in LM.AbstractSubstMachine]

---

Definition Index

A

all_Fin [in LM.Base.FiniteTypes.Arbitrary]

B

bijective [in LM.Base.Extra.Bijection]

C

card [in LM.Base.Lists.Cardinality]
closed [in LM.L]
compile [in LM.Programs]
count [in LM.Base.FiniteTypes.BasicDefinitions]

D

Dec [in LM.Base.Prelim]
dec [in LM.Base.Prelim]
decompile [in LM.Programs]
disjoint [in LM.Base.Lists.BaseLists]

E

elAt [in LM.Base.Lists.Position]
elem [in LM.Base.FiniteTypes.FinTypes]
equi [in LM.Base.Lists.BaseLists]
extended [in LM.AbstractHeapMachine]

F

f [in LM.AbstractHeapMachine]
filter [in LM.Base.Lists.Filter]
finType_cc [in LM.Base.FiniteTypes.FinTypes]
FP [in LM.Base.Numbers]
functional [in LM.ARS]

G

get [in LM.AbstractHeapMachine]
getPosition [in LM.Base.FiniteTypes.FinTypes]

I

inclp [in LM.Base.Lists.BaseLists]
index [in LM.Base.FiniteTypes.FinTypes]
init [in LM.AbstractSubstMachine]
init [in LM.AbstractHeapMachine]
injective [in LM.Base.Extra.Bijection]
inverse [in LM.Base.Extra.Bijection]
it [in LM.Base.Numbers]

J

jumpTarget [in LM.Programs]

L

lambda [in LM.L]
left_inverse [in LM.Base.Extra.Bijection]
lookup [in LM.AbstractHeapMachine]

P

pickx [in LM.Base.FiniteTypes.FinTypes]
pos [in LM.Base.Lists.Position]
pos_def [in LM.Base.FiniteTypes.FinTypes]
pow [in LM.ARS]
power [in LM.Base.Lists.Power]
prodLists [in LM.Base.FiniteTypes.BasicDefinitions]
pure [in LM.Base.FiniteTypes.Arbitrary]
put [in LM.AbstractHeapMachine]

R

rcomp [in LM.ARS]
redWithMaxSizeL [in LM.L]
redWithMaxSizeS [in LM.AbstractSubstMachine]
reflexive [in LM.ARS]
rem [in LM.Base.Lists.Removal]
rep [in LM.Base.Lists.Power]
replace [in LM.Base.Lists.Position]
right_inverse [in LM.Base.Extra.Bijection]

S

size [in LM.L]
sizeC [in LM.AbstractHeapMachine]
sizeH [in LM.AbstractHeapMachine]
sizeHE [in LM.AbstractHeapMachine]
sizeP [in LM.Programs]
sizeSt [in LM.AbstractHeapMachine]
sizeT [in LM.Programs]
state [in LM.AbstractHeapMachine]
subst [in LM.L]
substP [in LM.Programs]
subtype [in LM.Base.FiniteTypes.Arbitrary]
sum [in LM.Programs]
surjective [in LM.Base.Extra.Bijection]
symmetric [in LM.ARS]

T

tc [in LM.AbstractSubstMachine]
toOptionList [in LM.Base.FiniteTypes.BasicDefinitions]
toSubList [in LM.Base.FiniteTypes.Arbitrary]
toSumList1 [in LM.Base.FiniteTypes.BasicDefinitions]
toSumList2 [in LM.Base.FiniteTypes.BasicDefinitions]
transitive [in LM.ARS]

U

undup [in LM.Base.Lists.Dupfree]

---

Record Index

E

eqType [in LM.Base.Prelim]

F

finType [in LM.Base.FiniteTypes.FinTypes]
finTypeC [in LM.Base.FiniteTypes.FinTypes]

---

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

(537 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

(20 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

(25 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

(26 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

(255 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

(41 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

(17 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)

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

(55 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

(17 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

(3 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

(69 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

(3 entries)

Generated by coqdoc and improved with CoqdocJS