| 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
CoqlibP
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