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

_

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

_

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

_

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

_

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

_

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

_

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

_

(2 entries)

---

Global Index

A

align [definition, in Coqlib]
align_le [lemma, in Coqlib]

C

Coqlib [library]

D

dec_eq_false [lemma, in Coqlib]
dec_eq_sym [lemma, in Coqlib]
dec_eq_true [lemma, in Coqlib]
dests [definition, in Parmov]
dests_append [lemma, in Parmov]
dests_decomp [lemma, in Parmov]
dests_disjoint [definition, in Parmov]
dests_disjoint_append_left [lemma, in Parmov]
dests_disjoint_append_right [lemma, in Parmov]
dests_disjoint_cons_left [lemma, in Parmov]
dests_disjoint_cons_right [lemma, in Parmov]
dests_disjoint_sym [lemma, in Parmov]
disjoint_list [definition, in Parmov]
disjoint_list_notin [lemma, in Parmov]
disjoint_temps [definition, in Parmov]
disjoint_temps_not_temp [lemma, in Parmov]
dtransition [inductive, in Parmov]
dtransitions [definition, in Parmov]
dtransitions_correctness [lemma, in Parmov]
dtransitions_preserve_wf_state [lemma, in Parmov]
dtransition_preserves_wf_state [lemma, in Parmov]
dtr_last [constructor, in Parmov]
dtr_loop_pop [constructor, in Parmov]
dtr_nop [constructor, in Parmov]
dtr_pop [constructor, in Parmov]
dtr_push [constructor, in Parmov]
dtr_start [constructor, in Parmov]

E

env [definition, in Parmov]
env_equiv [definition, in Parmov]
env_equiv_refl [lemma, in Parmov]
env_equiv_refl' [lemma, in Parmov]
env_equiv_sym [lemma, in Parmov]
env_equiv_trans [lemma, in Parmov]
env_ext [lemma, in Parmov]
env_match [definition, in Parmov]
exec_par [definition, in Parmov]
exec_par_append_eq [lemma, in Parmov]
exec_par_combine [lemma, in Parmov]
exec_par_env_equiv [lemma, in Parmov]
exec_par_ident [lemma, in Parmov]
exec_par_lift [lemma, in Parmov]
exec_par_outside [lemma, in Parmov]
exec_par_update_no_read [lemma, in Parmov]
exec_seq [definition, in Parmov]
exec_seq_app [lemma, in Parmov]
exec_seq_exec_seq_rev [lemma, in Parmov]
exec_seq_rev [definition, in Parmov]
exec_seq_rev_app [lemma, in Parmov]
exec_seq_rev_exec_seq [lemma, in Parmov]
extensionality [axiom, in Coqlib]

F

final_state [definition, in Parmov]

I

incl_app_inv_l [lemma, in Coqlib]
incl_app_inv_r [lemma, in Coqlib]
incl_cons_inv [lemma, in Coqlib]
incl_same_head [lemma, in Coqlib]
in_app [lemma, in Coqlib]
in_cns [lemma, in Coqlib]
is_class_compatible [definition, in Parmov]
is_first_dest [definition, in Parmov]
is_last_source_charact [lemma, in Parmov]
is_mill [definition, in Parmov]
is_mill_append [lemma, in Parmov]
is_mill_cons [lemma, in Parmov]
is_not_temp [definition, in Parmov]
is_path [inductive, in Parmov]
is_path_change_last_source [lemma, in Parmov]
is_path_cons [constructor, in Parmov]
is_path_nil [constructor, in Parmov]
is_path_pop [lemma, in Parmov]
is_tail [inductive, in Coqlib]
is_tail_cons [constructor, in Coqlib]
is_tail_cons_left [lemma, in Coqlib]
is_tail_in [lemma, in Coqlib]
is_tail_incl [lemma, in Coqlib]
is_tail_refl [constructor, in Coqlib]
is_tail_trans [lemma, in Coqlib]
is_temp [definition, in Parmov]

L

list_append_map [lemma, in Coqlib]
list_disjoint [definition, in Coqlib]
list_disjoint_cons_left [lemma, in Coqlib]
list_disjoint_cons_right [lemma, in Coqlib]
list_disjoint_dec [lemma, in Coqlib]
list_disjoint_notin [lemma, in Coqlib]
list_disjoint_sym [lemma, in Coqlib]
list_drop1 [definition, in Coqlib]
list_drop1_incl [lemma, in Coqlib]
list_drop1_norepet [lemma, in Coqlib]
list_drop2 [definition, in Coqlib]
list_drop2_incl [lemma, in Coqlib]
list_drop2_norepet [lemma, in Coqlib]
list_forall2 [inductive, in Coqlib]
list_forall2_cons [constructor, in Coqlib]
list_forall2_imply [lemma, in Coqlib]
list_forall2_nil [constructor, in Coqlib]
list_in_insert [lemma, in Coqlib]
list_in_map_inv [lemma, in Coqlib]
list_length_map [lemma, in Coqlib]
list_map_compose [lemma, in Coqlib]
list_map_drop1 [lemma, in Coqlib]
list_map_drop2 [lemma, in Coqlib]
list_map_exten [lemma, in Coqlib]
list_map_identity [lemma, in Coqlib]
list_map_norepet [lemma, in Coqlib]
list_map_nth [lemma, in Coqlib]
list_norepet [inductive, in Coqlib]
list_norepet_app [lemma, in Coqlib]
list_norepet_append [lemma, in Coqlib]
list_norepet_append_left [lemma, in Coqlib]
list_norepet_append_right [lemma, in Coqlib]
list_norepet_cons [constructor, in Coqlib]
list_norepet_dec [lemma, in Coqlib]
list_norepet_nil [constructor, in Coqlib]

M

measure [definition, in Parmov]
measure_decreasing_1 [lemma, in Parmov]
measure_decreasing_2 [lemma, in Parmov]
modusponens [lemma, in Coqlib]
moves [definition, in Parmov]
move_no_temp [definition, in Parmov]
move_no_temp_append [lemma, in Parmov]
move_no_temp_rev [lemma, in Parmov]
mu_is_mill [lemma, in Parmov]
mu_move_no_temp [lemma, in Parmov]

N

notin_dests_append [lemma, in Parmov]
notin_dests_cons [lemma, in Parmov]
no_adherence [definition, in Parmov]
no_adherence_dst [lemma, in Parmov]
no_adherence_src [lemma, in Parmov]
no_adherence_tmp [lemma, in Parmov]
no_overlap [definition, in Parmov]
no_overlap_pairwise [lemma, in Parmov]
no_overlap_sym [lemma, in Parmov]
no_read [definition, in Parmov]
no_read_path [lemma, in Parmov]
nth_error_in [lemma, in Coqlib]
nth_error_nil [lemma, in Coqlib]

O

option_map [definition, in Coqlib]

P

pairwise_disjoint [inductive, in Parmov]
pairwise_disjoint_cons [constructor, in Parmov]
pairwise_disjoint_nil [constructor, in Parmov]
pairwise_disjoint_norepet [lemma, in Parmov]
Parmov [library]
parmove [definition, in Parmov]
parmove2 [definition, in Parmov]
parmove2_correctness [lemma, in Parmov]
parmove2_correctness_with_overlap [lemma, in Parmov]
parmove2_wf_moves [lemma, in Parmov]
parmove_aux_transitions [lemma, in Parmov]
parmove_correctness [lemma, in Parmov]
parmove_dests_initial_reg_or_temp [lemma, in Parmov]
parmove_initial_reg_or_temp [lemma, in Parmov]
parmove_preserves_register_classes [lemma, in Parmov]
parmove_srcs_initial_reg_or_temp [lemma, in Parmov]
parmove_step_compatible [lemma, in Parmov]
parmove_wf_moves [lemma, in Parmov]
path_sources_dests [lemma, in Parmov]
peq [definition, in Coqlib]
peq_false [lemma, in Coqlib]
peq_true [lemma, in Coqlib]
Ple [definition, in Coqlib]
Ple_refl [lemma, in Coqlib]
Ple_succ [lemma, in Coqlib]
Ple_trans [lemma, in Coqlib]
plt [definition, in Coqlib]
Plt [definition, in Coqlib]
Plt_ne [lemma, in Coqlib]
Plt_Ple [lemma, in Coqlib]
Plt_Ple_trans [lemma, in Coqlib]
Plt_strict [lemma, in Coqlib]
Plt_succ [lemma, in Coqlib]
Plt_succ_inv [lemma, in Coqlib]
Plt_trans [lemma, in Coqlib]
Plt_trans_succ [lemma, in Coqlib]
Plt_wf [lemma, in Coqlib]
positive_Peano_ind [lemma, in Coqlib]
positive_rec [definition, in Coqlib]
positive_rec_base [lemma, in Coqlib]
positive_rec_succ [lemma, in Coqlib]
Ppred_Plt [lemma, in Coqlib]
proj_sumbool [definition, in Coqlib]
proj_sumbool_true [lemma, in Coqlib]
proof_irrelevance [axiom, in Coqlib]

R

replace_last_source_charact [lemma, in Parmov]

S

split_move_charact [lemma, in Parmov]
srcs [definition, in Parmov]
srcs_append [lemma, in Parmov]
srcs_decomp [lemma, in Parmov]
srcs_dests_combine [lemma, in Parmov]
state [inductive, in Parmov]
State [constructor, in Parmov]
statemove [definition, in Parmov]
state_wf [inductive, in Parmov]
state_wf_intro [constructor, in Parmov]
state_wf_start [lemma, in Parmov]
sum_left_map [definition, in Coqlib]

T

temp_last [definition, in Parmov]
temp_last_change_last_source [lemma, in Parmov]
temp_last_pop [lemma, in Parmov]
temp_last_push [lemma, in Parmov]
transition [inductive, in Parmov]
transitions [definition, in Parmov]
transitions_correctness [lemma, in Parmov]
transitions_determ [lemma, in Parmov]
transitions_preserve_semantics [lemma, in Parmov]
transitions_preserve_wf [lemma, in Parmov]
transition_determ [lemma, in Parmov]
transition_preserves_semantics [lemma, in Parmov]
transition_preserves_wf [lemma, in Parmov]
tr_last [constructor, in Parmov]
tr_loop [constructor, in Parmov]
tr_nop [constructor, in Parmov]
tr_pop [constructor, in Parmov]
tr_push [constructor, in Parmov]
tr_start [constructor, in Parmov]
two_power_nat_O [lemma, in Coqlib]
two_power_nat_pos [lemma, in Coqlib]

U

unroll_positive_rec [lemma, in Coqlib]
update [definition, in Parmov]
update_commut [lemma, in Parmov]
update_ident [lemma, in Parmov]
update_o [lemma, in Parmov]
update_s [lemma, in Parmov]
update_twice [lemma, in Parmov]

W

weak_exec_seq [definition, in Parmov]
weak_exec_seq_match [lemma, in Parmov]
weak_update_match [lemma, in Parmov]
wf_move [inductive, in Parmov]
wf_moves [definition, in Parmov]
wf_moves_append [lemma, in Parmov]
wf_moves_cons [lemma, in Parmov]
wf_move_same [constructor, in Parmov]
wf_move_temp_left [constructor, in Parmov]
wf_move_temp_right [constructor, in Parmov]
wf_state [inductive, in Parmov]
wf_state_intro [constructor, in Parmov]

Z

Zdiv_small [lemma, in Coqlib]
Zdiv_unique [lemma, in Coqlib]
zeq [definition, in Coqlib]
zeq_false [lemma, in Coqlib]
zeq_true [lemma, in Coqlib]
zle [definition, in Coqlib]
zle_false [lemma, in Coqlib]
zle_true [lemma, in Coqlib]
zlt [definition, in Coqlib]
zlt_false [lemma, in Coqlib]
zlt_true [lemma, in Coqlib]
Zmax_bound_l [lemma, in Coqlib]
Zmax_bound_r [lemma, in Coqlib]
Zmax_spec [lemma, in Coqlib]
Zmin_spec [lemma, in Coqlib]
Zmod_small [lemma, in Coqlib]
Zmod_unique [lemma, in Coqlib]

---

Axiom Index

E

extensionality [in Coqlib]

P

proof_irrelevance [in Coqlib]

---

Lemma Index

A

align_le [in Coqlib]

D

dec_eq_false [in Coqlib]
dec_eq_sym [in Coqlib]
dec_eq_true [in Coqlib]
dests_append [in Parmov]
dests_decomp [in Parmov]
dests_disjoint_append_left [in Parmov]
dests_disjoint_append_right [in Parmov]
dests_disjoint_cons_left [in Parmov]
dests_disjoint_cons_right [in Parmov]
dests_disjoint_sym [in Parmov]
disjoint_list_notin [in Parmov]
disjoint_temps_not_temp [in Parmov]
dtransitions_correctness [in Parmov]
dtransitions_preserve_wf_state [in Parmov]
dtransition_preserves_wf_state [in Parmov]

E

env_equiv_refl [in Parmov]
env_equiv_refl' [in Parmov]
env_equiv_sym [in Parmov]
env_equiv_trans [in Parmov]
env_ext [in Parmov]
exec_par_append_eq [in Parmov]
exec_par_combine [in Parmov]
exec_par_env_equiv [in Parmov]
exec_par_ident [in Parmov]
exec_par_lift [in Parmov]
exec_par_outside [in Parmov]
exec_par_update_no_read [in Parmov]
exec_seq_app [in Parmov]
exec_seq_exec_seq_rev [in Parmov]
exec_seq_rev_app [in Parmov]
exec_seq_rev_exec_seq [in Parmov]

I

incl_app_inv_l [in Coqlib]
incl_app_inv_r [in Coqlib]
incl_cons_inv [in Coqlib]
incl_same_head [in Coqlib]
in_app [in Coqlib]
in_cns [in Coqlib]
is_last_source_charact [in Parmov]
is_mill_append [in Parmov]
is_mill_cons [in Parmov]
is_path_change_last_source [in Parmov]
is_path_pop [in Parmov]
is_tail_cons_left [in Coqlib]
is_tail_in [in Coqlib]
is_tail_incl [in Coqlib]
is_tail_trans [in Coqlib]

L

list_append_map [in Coqlib]
list_disjoint_cons_left [in Coqlib]
list_disjoint_cons_right [in Coqlib]
list_disjoint_dec [in Coqlib]
list_disjoint_notin [in Coqlib]
list_disjoint_sym [in Coqlib]
list_drop1_incl [in Coqlib]
list_drop1_norepet [in Coqlib]
list_drop2_incl [in Coqlib]
list_drop2_norepet [in Coqlib]
list_forall2_imply [in Coqlib]
list_in_insert [in Coqlib]
list_in_map_inv [in Coqlib]
list_length_map [in Coqlib]
list_map_compose [in Coqlib]
list_map_drop1 [in Coqlib]
list_map_drop2 [in Coqlib]
list_map_exten [in Coqlib]
list_map_identity [in Coqlib]
list_map_norepet [in Coqlib]
list_map_nth [in Coqlib]
list_norepet_app [in Coqlib]
list_norepet_append [in Coqlib]
list_norepet_append_left [in Coqlib]
list_norepet_append_right [in Coqlib]
list_norepet_dec [in Coqlib]

M

measure_decreasing_1 [in Parmov]
measure_decreasing_2 [in Parmov]
modusponens [in Coqlib]
move_no_temp_append [in Parmov]
move_no_temp_rev [in Parmov]
mu_is_mill [in Parmov]
mu_move_no_temp [in Parmov]

N

notin_dests_append [in Parmov]
notin_dests_cons [in Parmov]
no_adherence_dst [in Parmov]
no_adherence_src [in Parmov]
no_adherence_tmp [in Parmov]
no_overlap_pairwise [in Parmov]
no_overlap_sym [in Parmov]
no_read_path [in Parmov]
nth_error_in [in Coqlib]
nth_error_nil [in Coqlib]

P

pairwise_disjoint_norepet [in Parmov]
parmove2_correctness [in Parmov]
parmove2_correctness_with_overlap [in Parmov]
parmove2_wf_moves [in Parmov]
parmove_aux_transitions [in Parmov]
parmove_correctness [in Parmov]
parmove_dests_initial_reg_or_temp [in Parmov]
parmove_initial_reg_or_temp [in Parmov]
parmove_preserves_register_classes [in Parmov]
parmove_srcs_initial_reg_or_temp [in Parmov]
parmove_step_compatible [in Parmov]
parmove_wf_moves [in Parmov]
path_sources_dests [in Parmov]
peq_false [in Coqlib]
peq_true [in Coqlib]
Ple_refl [in Coqlib]
Ple_succ [in Coqlib]
Ple_trans [in Coqlib]
Plt_ne [in Coqlib]
Plt_Ple [in Coqlib]
Plt_Ple_trans [in Coqlib]
Plt_strict [in Coqlib]
Plt_succ [in Coqlib]
Plt_succ_inv [in Coqlib]
Plt_trans [in Coqlib]
Plt_trans_succ [in Coqlib]
Plt_wf [in Coqlib]
positive_Peano_ind [in Coqlib]
positive_rec_base [in Coqlib]
positive_rec_succ [in Coqlib]
Ppred_Plt [in Coqlib]
proj_sumbool_true [in Coqlib]

R

replace_last_source_charact [in Parmov]

S

split_move_charact [in Parmov]
srcs_append [in Parmov]
srcs_decomp [in Parmov]
srcs_dests_combine [in Parmov]
state_wf_start [in Parmov]

T

temp_last_change_last_source [in Parmov]
temp_last_pop [in Parmov]
temp_last_push [in Parmov]
transitions_correctness [in Parmov]
transitions_determ [in Parmov]
transitions_preserve_semantics [in Parmov]
transitions_preserve_wf [in Parmov]
transition_determ [in Parmov]
transition_preserves_semantics [in Parmov]
transition_preserves_wf [in Parmov]
two_power_nat_O [in Coqlib]
two_power_nat_pos [in Coqlib]

U

unroll_positive_rec [in Coqlib]
update_commut [in Parmov]
update_ident [in Parmov]
update_o [in Parmov]
update_s [in Parmov]
update_twice [in Parmov]

W

weak_exec_seq_match [in Parmov]
weak_update_match [in Parmov]
wf_moves_append [in Parmov]
wf_moves_cons [in Parmov]

Z

Zdiv_small [in Coqlib]
Zdiv_unique [in Coqlib]
zeq_false [in Coqlib]
zeq_true [in Coqlib]
zle_false [in Coqlib]
zle_true [in Coqlib]
zlt_false [in Coqlib]
zlt_true [in Coqlib]
Zmax_bound_l [in Coqlib]
Zmax_bound_r [in Coqlib]
Zmax_spec [in Coqlib]
Zmin_spec [in Coqlib]
Zmod_small [in Coqlib]
Zmod_unique [in Coqlib]

---

Constructor Index

D

dtr_last [in Parmov]
dtr_loop_pop [in Parmov]
dtr_nop [in Parmov]
dtr_pop [in Parmov]
dtr_push [in Parmov]
dtr_start [in Parmov]

I

is_path_cons [in Parmov]
is_path_nil [in Parmov]
is_tail_cons [in Coqlib]
is_tail_refl [in Coqlib]

L

list_forall2_cons [in Coqlib]
list_forall2_nil [in Coqlib]
list_norepet_cons [in Coqlib]
list_norepet_nil [in Coqlib]

P

pairwise_disjoint_cons [in Parmov]
pairwise_disjoint_nil [in Parmov]

S

State [in Parmov]
state_wf_intro [in Parmov]

T

tr_last [in Parmov]
tr_loop [in Parmov]
tr_nop [in Parmov]
tr_pop [in Parmov]
tr_push [in Parmov]
tr_start [in Parmov]

W

wf_move_same [in Parmov]
wf_move_temp_left [in Parmov]
wf_move_temp_right [in Parmov]
wf_state_intro [in Parmov]

---

Inductive Index

D

dtransition [in Parmov]

I

is_path [in Parmov]
is_tail [in Coqlib]

L

list_forall2 [in Coqlib]
list_norepet [in Coqlib]

P

pairwise_disjoint [in Parmov]

S

state [in Parmov]
state_wf [in Parmov]

T

transition [in Parmov]

W

wf_move [in Parmov]
wf_state [in Parmov]

---

Definition Index

A

align [in Coqlib]

D

dests [in Parmov]
dests_disjoint [in Parmov]
disjoint_list [in Parmov]
disjoint_temps [in Parmov]
dtransitions [in Parmov]

E

env [in Parmov]
env_equiv [in Parmov]
env_match [in Parmov]
exec_par [in Parmov]
exec_seq [in Parmov]
exec_seq_rev [in Parmov]

F

final_state [in Parmov]

I

is_class_compatible [in Parmov]
is_first_dest [in Parmov]
is_mill [in Parmov]
is_not_temp [in Parmov]
is_temp [in Parmov]

L

list_disjoint [in Coqlib]
list_drop1 [in Coqlib]
list_drop2 [in Coqlib]

M

measure [in Parmov]
moves [in Parmov]
move_no_temp [in Parmov]

N

no_adherence [in Parmov]
no_overlap [in Parmov]
no_read [in Parmov]

O

option_map [in Coqlib]

P

parmove [in Parmov]
parmove2 [in Parmov]
peq [in Coqlib]
Ple [in Coqlib]
plt [in Coqlib]
Plt [in Coqlib]
positive_rec [in Coqlib]
proj_sumbool [in Coqlib]

S

srcs [in Parmov]
statemove [in Parmov]
sum_left_map [in Coqlib]

T

temp_last [in Parmov]
transitions [in Parmov]

U

update [in Parmov]

W

weak_exec_seq [in Parmov]
wf_moves [in Parmov]

Z

zeq [in Coqlib]
zle [in Coqlib]
zlt [in Coqlib]

---

Library Index

C

Coqlib

P

Parmov

---

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

_

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

_

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

_

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

_

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

_

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

_

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

_

(2 entries)

---

This page has been generated by coqdoc