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 _ (478 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 _ (1 entry)
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 _ (3 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 _ (1 entry)
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 _ (337 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 _ (27 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2 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 _ (1 entry)
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 _ (81 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 _ (11 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 _ (14 entries)

Global Index

A

abshmake [constructor, in abstraction_phd_def]
absh_b0 [projection, in abstraction_phd_def]
absh_b0_neg_impl_ones_ge_a [lemma, in abstraction_phd_aux]
absh_b1 [projection, in abstraction_phd_def]
absh_equal [definition, in abstraction_phd_aux]
absh_equal_correctness [lemma, in abstraction_phd_aux]
absh_equal_impl_absh_equiv_test [lemma, in abstraction_phd_aux]
absh_equal_impl_absh_included_test [lemma, in abstraction_phd_aux]
absh_equal_is_equiv [instance, in abstraction_phd_aux]
absh_equal_sym [lemma, in abstraction_phd_aux]
absh_equiv [definition, in abstraction_phd_aux]
absh_equiv_test [definition, in abstraction_phd_aux]
absh_equiv_test_impl_absh_equal [lemma, in abstraction_phd_aux]
absh_included [definition, in abstraction_phd_def]
absh_included_test [definition, in abstraction_phd_def]
absh_included_test_correctness [lemma, in abstraction_phd_prop]
absh_included_test_impl_absh_included [lemma, in abstraction_phd_aux]
absh_included_test_not_not_absh [lemma, in abstraction_phd_aux]
absh_r [projection, in abstraction_phd_def]
absh_std [definition, in abstraction_phd_def]
absh_weakening [lemma, in abstraction_phd_prop]
absh_weakening_aux [lemma, in abstraction_phd_aux]
absh_weakening_0 [lemma, in abstraction_phd_aux]
abstractionh [record, in abstraction_phd_def]
Abstractionh_def [section, in abstraction_phd_aux]
abstraction_equivalence_properties [section, in abstraction_phd_aux]
abstraction_phd_aux [library]
abstraction_phd_def [library]
abstraction_phd_prop [library]
abs_equal_abs_std_non_empty [lemma, in abstraction_phd_aux]
abs_le_compat [lemma, in Q_misc]
abs_le_compat_prim [lemma, in Q_misc]
ADMITTED [axiom, in misc]
a_prec_w_late [lemma, in abstraction_phd_aux]


C

cg [definition, in floor]
cg_def [lemma, in floor]
cg_def_linear [lemma, in floor]
cg_div_int_rewrite [axiom, in floor]
cg_integerp [lemma, in floor]
cg_monotone_linear [lemma, in floor]
cg_plus_int_rewrite [axiom, in floor]
cg_rewrite [lemma, in floor]
communication_through_buffer [lemma, in ibw_prop]
communication_through_buffer_aux [lemma, in ibw_aux]
comparison [library]


D

delay [definition, in ibw_aux]
delay [definition, in inw_aux]
delay_d_w_eq_false [lemma, in inw_aux]
delay_d_w_eq_false [lemma, in ibw_aux]
delay_d_w_eq_w [lemma, in inw_aux]
delay_d_w_eq_w [lemma, in ibw_aux]
delay_properties [section, in ibw_aux]
delay_properties [section, in inw_aux]
den_r_i_p_b_le_den_r [lemma, in Q_misc]
den_r_le_den_r_i_p_b [lemma, in Q_misc]


E

early_and_late_properties [section, in abstraction_phd_aux]
early_def [lemma, in abstraction_phd_prop]
early_in_abs [lemma, in abstraction_phd_aux]
early_is_infimum [lemma, in abstraction_phd_prop]
early_prec_late_impl_early_in_a [lemma, in abstraction_phd_prop]
early_prec_late_impl_early_late_in_a [lemma, in abstraction_phd_prop]
early_prec_late_impl_late_in_a [lemma, in abstraction_phd_prop]
early_prec_late_impl_non_empty [lemma, in abstraction_phd_prop]
early_prec_late_impl_non_empty_and_early_is_infimum_and_late_is_supremum [lemma, in abstraction_phd_prop]
early_prec_w [lemma, in abstraction_phd_prop]
exists_i_st_ones_early1_and_ones_late2_eq_r_i_plus_b [lemma, in abstraction_phd_aux]
exists_i_st_ones_early_and_ones_late_eq_r_i_plus_b [lemma, in abstraction_phd_aux]
exists_i_st_ones_early_eq_r_i_plus_b [lemma, in abstraction_phd_aux]
exists_i_st_ones_late_eq_r_i_plus_b [lemma, in abstraction_phd_aux]


F

fl [definition, in floor]
floor [library]
fl_cg_in_Z [lemma, in floor]
fl_cg_not_in_Z [lemma, in floor]
fl_def [lemma, in floor]
fl_div_int_rewrite [axiom, in floor]
fl_eq_cg [lemma, in floor]
fl_eq_0 [lemma, in floor]
fl_integerp [lemma, in floor]
fl_le_cg [lemma, in floor]
fl_minus_cg_le_fl [lemma, in floor]
fl_minus_in_Z [axiom, in floor]
fl_minus_not_in_Z [axiom, in floor]
fl_monotone_linear [lemma, in floor]
fl_m_n [axiom, in floor]
fl_plus_int_rewrite [axiom, in floor]
fl_rewrite [axiom, in floor]


G

ge_impl_Qge [lemma, in Q_misc]


I

ibw [definition, in ibw_def]
ibw_aux [library]
ibw_def [library]
ibw_of_ones [definition, in ibw_def]
ibw_of_ones_correctness [lemma, in ibw_prop]
ibw_of_ones_correctness2 [lemma, in ibw_prop]
ibw_of_ones_ones_w_eq_w [lemma, in ibw_aux]
ibw_prop [library]
index_of_one [inductive, in ibw_aux]
index_of_one_functional [lemma, in ibw_aux]
infimum [definition, in ibw_def]
infimum [definition, in inw_def]
infimum_correctness [lemma, in ibw_prop]
infimum_is_lowerbound [lemma, in ibw_prop]
infimum_well_formed [lemma, in ibw_aux]
infimum_well_formed [lemma, in inw_aux]
inv_Qden_x_le_inv_Qden_Qred_x [lemma, in Q_misc]
inw [definition, in inw_def]
inw_aux [library]
inw_def [library]
inw_of_ones [definition, in inw_def]
inw_of_ones_correctness [lemma, in inw_prop]
inw_of_ones_correctness2 [lemma, in inw_prop]
inw_of_ones_ones_w_eq_w [lemma, in inw_aux]
inw_prop [library]
in_abstractionh [definition, in abstraction_phd_def]
in_Z [definition, in Q_misc]
iof [constructor, in ibw_aux]


L

late_def [lemma, in abstraction_phd_prop]
late_in_abs [lemma, in abstraction_phd_aux]
late_is_supremum [lemma, in abstraction_phd_prop]
le_impl_Qle [lemma, in Q_misc]
le_impl_Zle [lemma, in Q_misc]
le_prop_aux [lemma, in inw_aux]
le_prop_aux [lemma, in ibw_aux]
lowerbound_prec_infimum [lemma, in ibw_prop]
lt_impl_Qlt [lemma, in Q_misc]


M

minus_impl_Qminus [lemma, in Q_misc]
misc [library]


N

nat_in_Z [lemma, in Q_misc]
non_empty [definition, in abstraction_phd_def]
non_empty_alt [definition, in abstraction_phd_aux]
non_empty_equiv_early_prec_late [lemma, in abstraction_phd_prop]
non_empty_impl_early_prec_late [lemma, in abstraction_phd_prop]
non_empty_impl_ones_late_le_ones_early [lemma, in abstraction_phd_aux]
non_empty_test [definition, in abstraction_phd_def]
non_empty_test_alt [definition, in abstraction_phd_def]
non_empty_test_correctness [lemma, in abstraction_phd_prop]
non_empty_test_equal_compat [lemma, in abstraction_phd_aux]
non_empty_test_impl_ones_late_le_ones_early [lemma, in abstraction_phd_aux]
non_empty_test_impl_ones_late_le_ones_early_aux [lemma, in abstraction_phd_aux]
non_empty_test_properties [section, in abstraction_phd_aux]
non_null_impl_ones_i_eq_j [lemma, in ibw_aux]
non_null_impl_ones_i_ge_j [lemma, in inw_aux]
non_null_impl_ones_i_ge_j [lemma, in ibw_aux]
non_null_impl_ones_i_le_j [lemma, in inw_aux]
non_null_impl_ones_i_le_j [lemma, in ibw_aux]
non_null_stream [definition, in inw_aux]
non_null_stream [definition, in ibw_aux]
not [definition, in ibw_def]
not_absh [definition, in abstraction_phd_def]
not_absh_correctness [lemma, in abstraction_phd_prop]
not_absh_correctness_aux [lemma, in abstraction_phd_aux]
not_absh_well_formed_abstractionh_compat [lemma, in abstraction_phd_aux]
not_not_absh_equal_absh [lemma, in abstraction_phd_aux]
not_not_absh_included_test_absh [lemma, in abstraction_phd_aux]
not_properties [section, in ibw_aux]
not_properties [section, in abstraction_phd_aux]
not_wf_compat [lemma, in ibw_aux]
n_ge_cg_linear [axiom, in floor]
n_le_fl_linear [axiom, in floor]
n_plus_1_eq_S_n [lemma, in Q_misc]


O

on [definition, in ibw_def]
on [definition, in inw_def]
ones [definition, in ibw_def]
ones [definition, in inw_def]
ones_continuous [lemma, in ibw_aux]
ones_delay_d_w_eq_ones_w [lemma, in ibw_aux]
ones_delay_d_w_eq_ones_w [lemma, in inw_aux]
ones_delay_d_w_eq_0 [lemma, in ibw_aux]
ones_delay_d_w_eq_0 [lemma, in inw_aux]
ones_delay_d_w_i_eq_ones_w_i_m_d [lemma, in inw_aux]
ones_delay_d_w_i_eq_ones_w_i_m_d [lemma, in ibw_aux]
ones_early [definition, in abstraction_phd_def]
ones_early_alt [definition, in abstraction_phd_def]
ones_early_alt_correctness [lemma, in abstraction_phd_prop]
ones_early_alt_remove_Zabs_nat [lemma, in abstraction_phd_aux]
ones_early_eq_ones_early_alt [lemma, in abstraction_phd_aux]
ones_early_eq_ones_w_early [lemma, in abstraction_phd_aux]
ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b [lemma, in abstraction_phd_aux]
ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i_plus_x_plus_b [lemma, in abstraction_phd_aux]
ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_S_i_plus_b [lemma, in abstraction_phd_aux]
ones_early_opt [definition, in abstraction_phd_aux]
ones_early_opt_impl_ones_early [lemma, in abstraction_phd_aux]
ones_early_rewrite [lemma, in abstraction_phd_aux]
ones_early_well_formed [lemma, in abstraction_phd_aux]
ones_eq_equiv_w_eq [lemma, in ibw_prop]
ones_eq_equiv_w_eq [lemma, in inw_prop]
ones_eq_impl_w_eq [lemma, in inw_aux]
ones_eq_impl_w_eq [lemma, in ibw_aux]
ones_eq_0_impl_w_eq_false [lemma, in ibw_aux]
ones_eq_0_impl_w_eq_0 [lemma, in inw_aux]
ones_false_i_eq_0 [lemma, in inw_aux]
ones_false_i_eq_0 [lemma, in ibw_aux]
ones_ibw_of_ones_ones_w_eq_ones_w [lemma, in ibw_aux]
ones_impl_well_formed_ones [lemma, in ibw_aux]
ones_impl_well_formed_ones [lemma, in inw_aux]
ones_increasing [lemma, in inw_aux]
ones_increasing [lemma, in ibw_aux]
ones_increasing_by_one [lemma, in ibw_prop]
ones_increasing_one [lemma, in ibw_aux]
ones_increasing_one [lemma, in inw_aux]
ones_increasing_rev [lemma, in inw_aux]
ones_increasing_rev [lemma, in ibw_aux]
ones_increasing_x [lemma, in inw_aux]
ones_increasing_x [lemma, in ibw_aux]
ones_infimum [definition, in ibw_def]
ones_infimum [definition, in inw_def]
ones_infimum_correctness [lemma, in ibw_aux]
ones_infimum_well_formed [lemma, in ibw_aux]
ones_inw_of_ones_ones_w_eq_ones_w [lemma, in inw_aux]
ones_i_eq_0_impl_w_i'_eq_false [lemma, in ibw_aux]
ones_i_eq_0_impl_w_i'_eq_0 [lemma, in inw_aux]
ones_i_le_i [lemma, in ibw_prop]
ones_i_le_i_aux [lemma, in ibw_aux]
ones_i_le_i_mult_n [lemma, in inw_aux]
ones_late [definition, in abstraction_phd_def]
ones_late_alt [definition, in abstraction_phd_def]
ones_late_alt_correctness [lemma, in abstraction_phd_prop]
ones_late_alt_remove_Zabs_nat [lemma, in abstraction_phd_aux]
ones_late_eq_ones_early [lemma, in abstraction_phd_aux]
ones_late_eq_ones_late_alt [lemma, in abstraction_phd_aux]
ones_late_eq_ones_w_late [lemma, in abstraction_phd_aux]
ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b [lemma, in abstraction_phd_aux]
ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i_plus_x_plus_b [lemma, in abstraction_phd_aux]
ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_S_i_plus_b [lemma, in abstraction_phd_aux]
ones_late_le_ones_early_impl_early_in_a [lemma, in abstraction_phd_aux]
ones_late_le_ones_early_impl_late_in_a [lemma, in abstraction_phd_aux]
ones_late_le_ones_early_impl_non_empty [lemma, in abstraction_phd_aux]
ones_late_le_ones_w [lemma, in abstraction_phd_aux]
ones_late_opt [definition, in abstraction_phd_aux]
ones_late_opt_impl_ones_late [lemma, in abstraction_phd_aux]
ones_late_rewrite [lemma, in abstraction_phd_aux]
ones_late_well_formed [lemma, in abstraction_phd_aux]
ones_not_def [lemma, in ibw_aux]
ones_n_impl_well_formed_ones_n [lemma, in inw_aux]
ones_on [lemma, in ibw_prop]
ones_on [lemma, in inw_prop]
ones_on_def [lemma, in inw_aux]
ones_on_def [lemma, in ibw_aux]
ones_on_le_ones_w1 [lemma, in ibw_aux]
ones_on_le_ones_w2 [lemma, in ibw_aux]
ones_pred_i_eq_ones_i [lemma, in ibw_aux]
ones_pred_i_eq_ones_i_minus_n [lemma, in inw_aux]
ones_pred_i_eq_pred_ones_i [lemma, in ibw_aux]
ones_properties [section, in ibw_aux]
ones_properties [section, in inw_aux]
ones_supremum [definition, in ibw_def]
ones_supremum [definition, in inw_def]
ones_supremum_correctness [lemma, in ibw_aux]
ones_supremum_well_formed [lemma, in inw_aux]
ones_supremum_well_formed [lemma, in ibw_aux]
ones_S_i_eq_n_plus_ones_i [lemma, in inw_aux]
ones_S_i_eq_ones_i [lemma, in ibw_aux]
ones_S_i_eq_S_ones_i [lemma, in ibw_aux]
ones_true_i_eq_i [lemma, in inw_aux]
ones_true_i_eq_i [lemma, in ibw_aux]
ones_w_le_ones_delay_d_w_p_d [lemma, in ibw_aux]
ones_w_le_ones_early [lemma, in abstraction_phd_aux]
ones_w_m_d_le_ones_delay_d_w [lemma, in ibw_aux]
on_absh [definition, in abstraction_phd_def]
on_absh_correctness [lemma, in abstraction_phd_prop]
on_absh_correctness_aux [lemma, in abstraction_phd_aux]
on_assoc [lemma, in inw_prop]
on_assoc [lemma, in ibw_prop]
on_assoc_aux [lemma, in inw_aux]
on_assoc_aux [lemma, in ibw_aux]
on_eq_0_and_w1_eq_1_impl_w2_eq_0 [lemma, in ibw_aux]
on_eq_1_impl_w1_eq_1 [lemma, in ibw_aux]
on_eq_1_impl_w2_eq_1 [lemma, in ibw_aux]
on_false_w [lemma, in inw_aux]
on_false_w [lemma, in ibw_aux]
on_ge_0 [lemma, in abstraction_phd_aux]
on_gt_0_impl_w1_gt_0 [lemma, in inw_aux]
on_infimum_distr_l [lemma, in ibw_aux]
on_infimum_distr_r [lemma, in ibw_aux]
on_le_i [lemma, in ibw_aux]
on_prec_compat [lemma, in inw_aux]
on_prec_compat [lemma, in ibw_aux]
on_prec_reg_l [lemma, in ibw_aux]
on_properties [section, in abstraction_phd_aux]
on_properties [section, in inw_aux]
on_properties [section, in ibw_aux]
on_subtyping_compat [lemma, in ibw_aux]
on_supremum_distr_l [lemma, in ibw_aux]
on_supremum_distr_r [lemma, in ibw_aux]
on_sync_compat [lemma, in ibw_aux]
on_true_w [lemma, in ibw_aux]
on_true_w [lemma, in inw_aux]
on_wf_compat [lemma, in ibw_aux]
on_wf_compat [lemma, in inw_aux]
on_w1_w2_ge_on_a1_a2 [lemma, in abstraction_phd_aux]
on_w1_w2_le_on_a1_a2 [lemma, in abstraction_phd_aux]
on_w_false [lemma, in ibw_aux]
on_w_false [lemma, in inw_aux]
on_w_true [lemma, in ibw_aux]
on_w_true [lemma, in inw_aux]


P

plus_impl_Qplus [lemma, in Q_misc]
prec [definition, in inw_def]
prec [definition, in ibw_def]
prec_absh [definition, in abstraction_phd_def]
prec_absh_alt [definition, in abstraction_phd_def]
prec_absh_alt_complet [lemma, in abstraction_phd_aux]
prec_absh_alt_correctness [lemma, in abstraction_phd_aux]
prec_absh_equiv_prec_absh_alt [lemma, in abstraction_phd_prop]
prec_absh_properties [section, in abstraction_phd_aux]
prec_absh_test [definition, in abstraction_phd_def]
prec_absh_test_correctness [lemma, in abstraction_phd_prop]
prec_absh_test_correctness_aux [lemma, in abstraction_phd_aux]
prec_antisym [lemma, in inw_aux]
prec_antisym [lemma, in ibw_aux]
prec_infimum_w1 [lemma, in ibw_aux]
prec_infimum_w2 [lemma, in ibw_aux]
prec_partial_order [lemma, in ibw_prop]
prec_partial_order [lemma, in inw_prop]
prec_properties [section, in inw_aux]
prec_properties [section, in ibw_aux]
prec_refl [lemma, in inw_aux]
prec_refl [lemma, in ibw_aux]
prec_trans [lemma, in inw_aux]
prec_trans [lemma, in ibw_aux]
prec_w1_supremum [lemma, in ibw_aux]
prec_w2_supremum [lemma, in ibw_aux]


Q

QDen_Qred_def [lemma, in Q_misc]
QDen_Qred_x_le_QDen_x [lemma, in Q_misc]
Qdiv_le_compat [lemma, in Q_misc]
Qeq_impl_Zeq [lemma, in Q_misc]
Qinv_ge_inv [lemma, in Q_misc]
Qinv_pos [lemma, in Q_misc]
Qinv_pos_strict [lemma, in Q_misc]
Qle_impl_le [lemma, in Q_misc]
Qle_impl_Qlt [lemma, in comparison]
Qle_impl_Zle [lemma, in Q_misc]
Qle_max_l [lemma, in Q_misc]
Qle_max_r [lemma, in Q_misc]
Qle_min_l [lemma, in Q_misc]
Qle_min_r [lemma, in Q_misc]
Qle_plus [lemma, in Q_misc]
Qlt_impl_lt [lemma, in Q_misc]
Qlt_impl_Qle [lemma, in comparison]
Qlt_impl_Qle_aux [lemma, in comparison]
Qlt_impl_Qle_red [lemma, in comparison]
Qlt_impl_Zlt [lemma, in Q_misc]
Qlt_plus [lemma, in Q_misc]
Qmax [definition, in Q_misc]
Qmax_dec [lemma, in Q_misc]
Qmax_irreducible [lemma, in Q_misc]
Qmin [definition, in Q_misc]
Qmin_dec [lemma, in Q_misc]
Qmin_irreducible [lemma, in Q_misc]
Qmult_le_compat_l [lemma, in Q_misc]
Qmult_lt_compat_l [lemma, in Q_misc]
Qmult_lt_0_lt_reg_r [lemma, in Q_misc]
Qplus_eq_compat [lemma, in Q_misc]
Qplus_in_Z_compat [lemma, in Q_misc]
Qplus_lt_compat_l [lemma, in Q_misc]
Q_misc [library]
Q_of_nat [definition, in Q_misc]


R

red_ones [lemma, in inw_aux]
red_ones [lemma, in ibw_aux]
red_ones_early [lemma, in abstraction_phd_aux]
red_ones_early_opt [lemma, in abstraction_phd_aux]
red_ones_late [lemma, in abstraction_phd_aux]
red_ones_late_opt [lemma, in abstraction_phd_aux]


S

simply_1 [lemma, in Q_misc]
simply_1_prim [lemma, in Q_misc]
simpl_std [lemma, in abstraction_phd_aux]
size [definition, in ibw_def]
size [definition, in inw_def]
sizei [definition, in ibw_def]
size_absh [definition, in abstraction_phd_def]
size_absh_correctness [lemma, in abstraction_phd_prop]
size_absh_correctness_aux [lemma, in abstraction_phd_aux]
size_early1_late2_le_size_absh [lemma, in abstraction_phd_aux]
size_early1_late2_le_size_absh_aux [lemma, in abstraction_phd_aux]
size_properties [section, in abstraction_phd_aux]
size_properties [section, in ibw_aux]
strong_well_formed_abstractionh [definition, in abstraction_phd_def]
subtype_impl_a2_b0_le_a1_b1 [lemma, in abstraction_phd_aux]
subtyping [definition, in inw_def]
subtyping [definition, in ibw_def]
subtyping_absh [definition, in abstraction_phd_def]
subtyping_absh_alt [definition, in abstraction_phd_def]
subtyping_absh_alt_impl_subtyping_absh [lemma, in abstraction_phd_aux]
subtyping_absh_equiv_subtyping_absh_alt [lemma, in abstraction_phd_prop]
subtyping_absh_impl_subtyping_absh_alt [lemma, in abstraction_phd_aux]
subtyping_properties [section, in abstraction_phd_aux]
subtyping_properties [section, in ibw_aux]
subtyping_properties [section, in inw_aux]
sum [definition, in inw_def]
supremum [definition, in ibw_def]
supremum [definition, in inw_def]
supremum_correctness [lemma, in ibw_prop]
supremum_is_upperbound [lemma, in ibw_prop]
supremum_prec_upperbounds [lemma, in ibw_prop]
supremum_well_formed [lemma, in ibw_aux]
supremum_well_formed [lemma, in inw_aux]
sync [definition, in ibw_def]
sync [definition, in inw_def]
sync_absh [definition, in abstraction_phd_def]
sync_absh_equiv_sync_absh_test [lemma, in abstraction_phd_prop]
sync_absh_refl [lemma, in abstraction_phd_aux]
sync_absh_sym [lemma, in abstraction_phd_aux]
sync_absh_test [definition, in abstraction_phd_def]
sync_absh_test_completeness [lemma, in abstraction_phd_aux]
sync_absh_test_correctness [lemma, in abstraction_phd_aux]
sync_absh_trans [lemma, in abstraction_phd_aux]
sync_early_late [lemma, in abstraction_phd_aux]
sync_equiv_relation [lemma, in inw_prop]
sync_equiv_relation [lemma, in ibw_prop]
sync_popl [definition, in ibw_aux]
sync_popl_impl_sync [lemma, in ibw_aux]
sync_properties [section, in ibw_aux]
sync_properties [section, in abstraction_phd_aux]
sync_properties [section, in inw_aux]
sync_refl [lemma, in inw_aux]
sync_refl [lemma, in ibw_aux]
sync_sym [lemma, in ibw_aux]
sync_sym [lemma, in inw_aux]
sync_trans [lemma, in ibw_aux]
sync_trans [lemma, in inw_aux]
S_n_m_1_eq_n [lemma, in Q_misc]
S_n_nbeq_n [lemma, in misc]


T

true_and_false_properties [section, in inw_aux]
true_and_false_properties [section, in ibw_aux]


W

well_formed_abstractionh [definition, in abstraction_phd_def]
well_formed_abstractionh_absh_equal_compat [lemma, in abstraction_phd_aux]
well_formed_ibw [definition, in ibw_aux]
well_formed_inw [definition, in inw_aux]
well_formed_inw_n [definition, in inw_aux]
well_formed_inw_n_weakening [lemma, in inw_aux]
well_formed_n_properties [section, in inw_aux]
well_formed_ones [definition, in inw_aux]
well_formed_ones [definition, in ibw_aux]
well_formed_ones_n [definition, in inw_aux]
well_formed_ones_n_weakening [lemma, in inw_aux]
w_early [definition, in abstraction_phd_def]
w_early_prec_a [lemma, in abstraction_phd_aux]
w_early_S_i_eq_false_impl_ones_early_i_gt_a [lemma, in abstraction_phd_aux]
w_early_S_i_eq_true_impl_ones_early_S_i_le_a [lemma, in abstraction_phd_aux]
w_early_well_formed [lemma, in abstraction_phd_aux]
w_eq_impl_ones_eq [lemma, in inw_aux]
w_eq_impl_ones_eq [lemma, in ibw_aux]
w_false [definition, in inw_aux]
w_false [definition, in ibw_aux]
w_false_well_formed [lemma, in ibw_aux]
w_false_well_formed [lemma, in inw_aux]
w_false_well_formed_n [lemma, in inw_aux]
w_in_a1_and_a1_in_a2_impl_w_in_a2 [lemma, in abstraction_phd_aux]
w_i'_eq_false_impl_ones_i_eq_0 [lemma, in ibw_aux]
w_i'_eq_0_impl_ones_i_eq_0 [lemma, in inw_aux]
w_i_eq_true_impl_ones_pos [lemma, in ibw_aux]
w_i_ge_1_impl_ones_pos [lemma, in inw_aux]
w_late [definition, in abstraction_phd_def]
w_late_well_formed [lemma, in abstraction_phd_aux]
w_prec_late [lemma, in abstraction_phd_prop]
w_true [definition, in inw_aux]
w_true [definition, in ibw_aux]
w_true_well_formed [lemma, in ibw_aux]
w_true_well_formed [lemma, in inw_aux]


X

x_lt_y_impl_fl_x_lt_cg_y [lemma, in floor]


Z

Zabs_le_impl_between [lemma, in Z_misc]
Zdiv_ge_denom [lemma, in Z_misc]
Zdiv_le_denom [lemma, in Z_misc]
Zeq_impl_nat_eq [lemma, in misc]
zeros [definition, in ibw_aux]
zeros_def [lemma, in ibw_aux]
Zgcd_gt_0_l [lemma, in Z_misc]
Zgcd_gt_0_r [lemma, in Z_misc]
Zgt_impl_Zge [lemma, in Z_misc]
Zle_impl_Qle [lemma, in Q_misc]
Zle_impl_Zlt [lemma, in Z_misc]
Zlt_impl_Qlt [lemma, in Q_misc]
Zlt_impl_Zle [lemma, in Z_misc]
Zmax_le_compat_l [lemma, in Z_misc]
Zmin_left [lemma, in Z_misc]
Zmin_le_compat_l [lemma, in Z_misc]
Zmin_right [lemma, in Z_misc]
Zplus_eq_Qplus [lemma, in Q_misc]
Z_misc [library]
Z_of_positive [definition, in floor]



Instance Index

A

absh_equal_is_equiv [in abstraction_phd_aux]



Projection Index

A

absh_b0 [in abstraction_phd_def]
absh_b1 [in abstraction_phd_def]
absh_r [in abstraction_phd_def]



Record Index

A

abstractionh [in abstraction_phd_def]



Lemma Index

A

absh_b0_neg_impl_ones_ge_a [in abstraction_phd_aux]
absh_equal_correctness [in abstraction_phd_aux]
absh_equal_impl_absh_equiv_test [in abstraction_phd_aux]
absh_equal_impl_absh_included_test [in abstraction_phd_aux]
absh_equal_sym [in abstraction_phd_aux]
absh_equiv_test_impl_absh_equal [in abstraction_phd_aux]
absh_included_test_correctness [in abstraction_phd_prop]
absh_included_test_impl_absh_included [in abstraction_phd_aux]
absh_included_test_not_not_absh [in abstraction_phd_aux]
absh_weakening [in abstraction_phd_prop]
absh_weakening_aux [in abstraction_phd_aux]
absh_weakening_0 [in abstraction_phd_aux]
abs_equal_abs_std_non_empty [in abstraction_phd_aux]
abs_le_compat [in Q_misc]
abs_le_compat_prim [in Q_misc]
a_prec_w_late [in abstraction_phd_aux]


C

cg_def [in floor]
cg_def_linear [in floor]
cg_integerp [in floor]
cg_monotone_linear [in floor]
cg_rewrite [in floor]
communication_through_buffer [in ibw_prop]
communication_through_buffer_aux [in ibw_aux]


D

delay_d_w_eq_false [in inw_aux]
delay_d_w_eq_false [in ibw_aux]
delay_d_w_eq_w [in inw_aux]
delay_d_w_eq_w [in ibw_aux]
den_r_i_p_b_le_den_r [in Q_misc]
den_r_le_den_r_i_p_b [in Q_misc]


E

early_def [in abstraction_phd_prop]
early_in_abs [in abstraction_phd_aux]
early_is_infimum [in abstraction_phd_prop]
early_prec_late_impl_early_in_a [in abstraction_phd_prop]
early_prec_late_impl_early_late_in_a [in abstraction_phd_prop]
early_prec_late_impl_late_in_a [in abstraction_phd_prop]
early_prec_late_impl_non_empty [in abstraction_phd_prop]
early_prec_late_impl_non_empty_and_early_is_infimum_and_late_is_supremum [in abstraction_phd_prop]
early_prec_w [in abstraction_phd_prop]
exists_i_st_ones_early1_and_ones_late2_eq_r_i_plus_b [in abstraction_phd_aux]
exists_i_st_ones_early_and_ones_late_eq_r_i_plus_b [in abstraction_phd_aux]
exists_i_st_ones_early_eq_r_i_plus_b [in abstraction_phd_aux]
exists_i_st_ones_late_eq_r_i_plus_b [in abstraction_phd_aux]


F

fl_cg_in_Z [in floor]
fl_cg_not_in_Z [in floor]
fl_def [in floor]
fl_eq_cg [in floor]
fl_eq_0 [in floor]
fl_integerp [in floor]
fl_le_cg [in floor]
fl_minus_cg_le_fl [in floor]
fl_monotone_linear [in floor]


G

ge_impl_Qge [in Q_misc]


I

ibw_of_ones_correctness [in ibw_prop]
ibw_of_ones_correctness2 [in ibw_prop]
ibw_of_ones_ones_w_eq_w [in ibw_aux]
index_of_one_functional [in ibw_aux]
infimum_correctness [in ibw_prop]
infimum_is_lowerbound [in ibw_prop]
infimum_well_formed [in ibw_aux]
infimum_well_formed [in inw_aux]
inv_Qden_x_le_inv_Qden_Qred_x [in Q_misc]
inw_of_ones_correctness [in inw_prop]
inw_of_ones_correctness2 [in inw_prop]
inw_of_ones_ones_w_eq_w [in inw_aux]


L

late_def [in abstraction_phd_prop]
late_in_abs [in abstraction_phd_aux]
late_is_supremum [in abstraction_phd_prop]
le_impl_Qle [in Q_misc]
le_impl_Zle [in Q_misc]
le_prop_aux [in inw_aux]
le_prop_aux [in ibw_aux]
lowerbound_prec_infimum [in ibw_prop]
lt_impl_Qlt [in Q_misc]


M

minus_impl_Qminus [in Q_misc]


N

nat_in_Z [in Q_misc]
non_empty_equiv_early_prec_late [in abstraction_phd_prop]
non_empty_impl_early_prec_late [in abstraction_phd_prop]
non_empty_impl_ones_late_le_ones_early [in abstraction_phd_aux]
non_empty_test_correctness [in abstraction_phd_prop]
non_empty_test_equal_compat [in abstraction_phd_aux]
non_empty_test_impl_ones_late_le_ones_early [in abstraction_phd_aux]
non_empty_test_impl_ones_late_le_ones_early_aux [in abstraction_phd_aux]
non_null_impl_ones_i_eq_j [in ibw_aux]
non_null_impl_ones_i_ge_j [in inw_aux]
non_null_impl_ones_i_ge_j [in ibw_aux]
non_null_impl_ones_i_le_j [in inw_aux]
non_null_impl_ones_i_le_j [in ibw_aux]
not_absh_correctness [in abstraction_phd_prop]
not_absh_correctness_aux [in abstraction_phd_aux]
not_absh_well_formed_abstractionh_compat [in abstraction_phd_aux]
not_not_absh_equal_absh [in abstraction_phd_aux]
not_not_absh_included_test_absh [in abstraction_phd_aux]
not_wf_compat [in ibw_aux]
n_plus_1_eq_S_n [in Q_misc]


O

ones_continuous [in ibw_aux]
ones_delay_d_w_eq_ones_w [in ibw_aux]
ones_delay_d_w_eq_ones_w [in inw_aux]
ones_delay_d_w_eq_0 [in ibw_aux]
ones_delay_d_w_eq_0 [in inw_aux]
ones_delay_d_w_i_eq_ones_w_i_m_d [in inw_aux]
ones_delay_d_w_i_eq_ones_w_i_m_d [in ibw_aux]
ones_early_alt_correctness [in abstraction_phd_prop]
ones_early_alt_remove_Zabs_nat [in abstraction_phd_aux]
ones_early_eq_ones_early_alt [in abstraction_phd_aux]
ones_early_eq_ones_w_early [in abstraction_phd_aux]
ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b [in abstraction_phd_aux]
ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i_plus_x_plus_b [in abstraction_phd_aux]
ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_S_i_plus_b [in abstraction_phd_aux]
ones_early_opt_impl_ones_early [in abstraction_phd_aux]
ones_early_rewrite [in abstraction_phd_aux]
ones_early_well_formed [in abstraction_phd_aux]
ones_eq_equiv_w_eq [in ibw_prop]
ones_eq_equiv_w_eq [in inw_prop]
ones_eq_impl_w_eq [in inw_aux]
ones_eq_impl_w_eq [in ibw_aux]
ones_eq_0_impl_w_eq_false [in ibw_aux]
ones_eq_0_impl_w_eq_0 [in inw_aux]
ones_false_i_eq_0 [in inw_aux]
ones_false_i_eq_0 [in ibw_aux]
ones_ibw_of_ones_ones_w_eq_ones_w [in ibw_aux]
ones_impl_well_formed_ones [in ibw_aux]
ones_impl_well_formed_ones [in inw_aux]
ones_increasing [in inw_aux]
ones_increasing [in ibw_aux]
ones_increasing_by_one [in ibw_prop]
ones_increasing_one [in ibw_aux]
ones_increasing_one [in inw_aux]
ones_increasing_rev [in inw_aux]
ones_increasing_rev [in ibw_aux]
ones_increasing_x [in inw_aux]
ones_increasing_x [in ibw_aux]
ones_infimum_correctness [in ibw_aux]
ones_infimum_well_formed [in ibw_aux]
ones_inw_of_ones_ones_w_eq_ones_w [in inw_aux]
ones_i_eq_0_impl_w_i'_eq_false [in ibw_aux]
ones_i_eq_0_impl_w_i'_eq_0 [in inw_aux]
ones_i_le_i [in ibw_prop]
ones_i_le_i_aux [in ibw_aux]
ones_i_le_i_mult_n [in inw_aux]
ones_late_alt_correctness [in abstraction_phd_prop]
ones_late_alt_remove_Zabs_nat [in abstraction_phd_aux]
ones_late_eq_ones_early [in abstraction_phd_aux]
ones_late_eq_ones_late_alt [in abstraction_phd_aux]
ones_late_eq_ones_w_late [in abstraction_phd_aux]
ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b [in abstraction_phd_aux]
ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i_plus_x_plus_b [in abstraction_phd_aux]
ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_S_i_plus_b [in abstraction_phd_aux]
ones_late_le_ones_early_impl_early_in_a [in abstraction_phd_aux]
ones_late_le_ones_early_impl_late_in_a [in abstraction_phd_aux]
ones_late_le_ones_early_impl_non_empty [in abstraction_phd_aux]
ones_late_le_ones_w [in abstraction_phd_aux]
ones_late_opt_impl_ones_late [in abstraction_phd_aux]
ones_late_rewrite [in abstraction_phd_aux]
ones_late_well_formed [in abstraction_phd_aux]
ones_not_def [in ibw_aux]
ones_n_impl_well_formed_ones_n [in inw_aux]
ones_on [in ibw_prop]
ones_on [in inw_prop]
ones_on_def [in inw_aux]
ones_on_def [in ibw_aux]
ones_on_le_ones_w1 [in ibw_aux]
ones_on_le_ones_w2 [in ibw_aux]
ones_pred_i_eq_ones_i [in ibw_aux]
ones_pred_i_eq_ones_i_minus_n [in inw_aux]
ones_pred_i_eq_pred_ones_i [in ibw_aux]
ones_supremum_correctness [in ibw_aux]
ones_supremum_well_formed [in inw_aux]
ones_supremum_well_formed [in ibw_aux]
ones_S_i_eq_n_plus_ones_i [in inw_aux]
ones_S_i_eq_ones_i [in ibw_aux]
ones_S_i_eq_S_ones_i [in ibw_aux]
ones_true_i_eq_i [in inw_aux]
ones_true_i_eq_i [in ibw_aux]
ones_w_le_ones_delay_d_w_p_d [in ibw_aux]
ones_w_le_ones_early [in abstraction_phd_aux]
ones_w_m_d_le_ones_delay_d_w [in ibw_aux]
on_absh_correctness [in abstraction_phd_prop]
on_absh_correctness_aux [in abstraction_phd_aux]
on_assoc [in inw_prop]
on_assoc [in ibw_prop]
on_assoc_aux [in inw_aux]
on_assoc_aux [in ibw_aux]
on_eq_0_and_w1_eq_1_impl_w2_eq_0 [in ibw_aux]
on_eq_1_impl_w1_eq_1 [in ibw_aux]
on_eq_1_impl_w2_eq_1 [in ibw_aux]
on_false_w [in inw_aux]
on_false_w [in ibw_aux]
on_ge_0 [in abstraction_phd_aux]
on_gt_0_impl_w1_gt_0 [in inw_aux]
on_infimum_distr_l [in ibw_aux]
on_infimum_distr_r [in ibw_aux]
on_le_i [in ibw_aux]
on_prec_compat [in inw_aux]
on_prec_compat [in ibw_aux]
on_prec_reg_l [in ibw_aux]
on_subtyping_compat [in ibw_aux]
on_supremum_distr_l [in ibw_aux]
on_supremum_distr_r [in ibw_aux]
on_sync_compat [in ibw_aux]
on_true_w [in ibw_aux]
on_true_w [in inw_aux]
on_wf_compat [in ibw_aux]
on_wf_compat [in inw_aux]
on_w1_w2_ge_on_a1_a2 [in abstraction_phd_aux]
on_w1_w2_le_on_a1_a2 [in abstraction_phd_aux]
on_w_false [in ibw_aux]
on_w_false [in inw_aux]
on_w_true [in ibw_aux]
on_w_true [in inw_aux]


P

plus_impl_Qplus [in Q_misc]
prec_absh_alt_complet [in abstraction_phd_aux]
prec_absh_alt_correctness [in abstraction_phd_aux]
prec_absh_equiv_prec_absh_alt [in abstraction_phd_prop]
prec_absh_test_correctness [in abstraction_phd_prop]
prec_absh_test_correctness_aux [in abstraction_phd_aux]
prec_antisym [in inw_aux]
prec_antisym [in ibw_aux]
prec_infimum_w1 [in ibw_aux]
prec_infimum_w2 [in ibw_aux]
prec_partial_order [in ibw_prop]
prec_partial_order [in inw_prop]
prec_refl [in inw_aux]
prec_refl [in ibw_aux]
prec_trans [in inw_aux]
prec_trans [in ibw_aux]
prec_w1_supremum [in ibw_aux]
prec_w2_supremum [in ibw_aux]


Q

QDen_Qred_def [in Q_misc]
QDen_Qred_x_le_QDen_x [in Q_misc]
Qdiv_le_compat [in Q_misc]
Qeq_impl_Zeq [in Q_misc]
Qinv_ge_inv [in Q_misc]
Qinv_pos [in Q_misc]
Qinv_pos_strict [in Q_misc]
Qle_impl_le [in Q_misc]
Qle_impl_Qlt [in comparison]
Qle_impl_Zle [in Q_misc]
Qle_max_l [in Q_misc]
Qle_max_r [in Q_misc]
Qle_min_l [in Q_misc]
Qle_min_r [in Q_misc]
Qle_plus [in Q_misc]
Qlt_impl_lt [in Q_misc]
Qlt_impl_Qle [in comparison]
Qlt_impl_Qle_aux [in comparison]
Qlt_impl_Qle_red [in comparison]
Qlt_impl_Zlt [in Q_misc]
Qlt_plus [in Q_misc]
Qmax_dec [in Q_misc]
Qmax_irreducible [in Q_misc]
Qmin_dec [in Q_misc]
Qmin_irreducible [in Q_misc]
Qmult_le_compat_l [in Q_misc]
Qmult_lt_compat_l [in Q_misc]
Qmult_lt_0_lt_reg_r [in Q_misc]
Qplus_eq_compat [in Q_misc]
Qplus_in_Z_compat [in Q_misc]
Qplus_lt_compat_l [in Q_misc]


R

red_ones [in inw_aux]
red_ones [in ibw_aux]
red_ones_early [in abstraction_phd_aux]
red_ones_early_opt [in abstraction_phd_aux]
red_ones_late [in abstraction_phd_aux]
red_ones_late_opt [in abstraction_phd_aux]


S

simply_1 [in Q_misc]
simply_1_prim [in Q_misc]
simpl_std [in abstraction_phd_aux]
size_absh_correctness [in abstraction_phd_prop]
size_absh_correctness_aux [in abstraction_phd_aux]
size_early1_late2_le_size_absh [in abstraction_phd_aux]
size_early1_late2_le_size_absh_aux [in abstraction_phd_aux]
subtype_impl_a2_b0_le_a1_b1 [in abstraction_phd_aux]
subtyping_absh_alt_impl_subtyping_absh [in abstraction_phd_aux]
subtyping_absh_equiv_subtyping_absh_alt [in abstraction_phd_prop]
subtyping_absh_impl_subtyping_absh_alt [in abstraction_phd_aux]
supremum_correctness [in ibw_prop]
supremum_is_upperbound [in ibw_prop]
supremum_prec_upperbounds [in ibw_prop]
supremum_well_formed [in ibw_aux]
supremum_well_formed [in inw_aux]
sync_absh_equiv_sync_absh_test [in abstraction_phd_prop]
sync_absh_refl [in abstraction_phd_aux]
sync_absh_sym [in abstraction_phd_aux]
sync_absh_test_completeness [in abstraction_phd_aux]
sync_absh_test_correctness [in abstraction_phd_aux]
sync_absh_trans [in abstraction_phd_aux]
sync_early_late [in abstraction_phd_aux]
sync_equiv_relation [in inw_prop]
sync_equiv_relation [in ibw_prop]
sync_popl_impl_sync [in ibw_aux]
sync_refl [in inw_aux]
sync_refl [in ibw_aux]
sync_sym [in ibw_aux]
sync_sym [in inw_aux]
sync_trans [in ibw_aux]
sync_trans [in inw_aux]
S_n_m_1_eq_n [in Q_misc]
S_n_nbeq_n [in misc]


W

well_formed_abstractionh_absh_equal_compat [in abstraction_phd_aux]
well_formed_inw_n_weakening [in inw_aux]
well_formed_ones_n_weakening [in inw_aux]
w_early_prec_a [in abstraction_phd_aux]
w_early_S_i_eq_false_impl_ones_early_i_gt_a [in abstraction_phd_aux]
w_early_S_i_eq_true_impl_ones_early_S_i_le_a [in abstraction_phd_aux]
w_early_well_formed [in abstraction_phd_aux]
w_eq_impl_ones_eq [in inw_aux]
w_eq_impl_ones_eq [in ibw_aux]
w_false_well_formed [in ibw_aux]
w_false_well_formed [in inw_aux]
w_false_well_formed_n [in inw_aux]
w_in_a1_and_a1_in_a2_impl_w_in_a2 [in abstraction_phd_aux]
w_i'_eq_false_impl_ones_i_eq_0 [in ibw_aux]
w_i'_eq_0_impl_ones_i_eq_0 [in inw_aux]
w_i_eq_true_impl_ones_pos [in ibw_aux]
w_i_ge_1_impl_ones_pos [in inw_aux]
w_late_well_formed [in abstraction_phd_aux]
w_prec_late [in abstraction_phd_prop]
w_true_well_formed [in ibw_aux]
w_true_well_formed [in inw_aux]


X

x_lt_y_impl_fl_x_lt_cg_y [in floor]


Z

Zabs_le_impl_between [in Z_misc]
Zdiv_ge_denom [in Z_misc]
Zdiv_le_denom [in Z_misc]
Zeq_impl_nat_eq [in misc]
zeros_def [in ibw_aux]
Zgcd_gt_0_l [in Z_misc]
Zgcd_gt_0_r [in Z_misc]
Zgt_impl_Zge [in Z_misc]
Zle_impl_Qle [in Q_misc]
Zle_impl_Zlt [in Z_misc]
Zlt_impl_Qlt [in Q_misc]
Zlt_impl_Zle [in Z_misc]
Zmax_le_compat_l [in Z_misc]
Zmin_left [in Z_misc]
Zmin_le_compat_l [in Z_misc]
Zmin_right [in Z_misc]
Zplus_eq_Qplus [in Q_misc]



Section Index

A

Abstractionh_def [in abstraction_phd_aux]
abstraction_equivalence_properties [in abstraction_phd_aux]


D

delay_properties [in ibw_aux]
delay_properties [in inw_aux]


E

early_and_late_properties [in abstraction_phd_aux]


N

non_empty_test_properties [in abstraction_phd_aux]
not_properties [in ibw_aux]
not_properties [in abstraction_phd_aux]


O

ones_properties [in ibw_aux]
ones_properties [in inw_aux]
on_properties [in abstraction_phd_aux]
on_properties [in inw_aux]
on_properties [in ibw_aux]


P

prec_absh_properties [in abstraction_phd_aux]
prec_properties [in inw_aux]
prec_properties [in ibw_aux]


S

size_properties [in abstraction_phd_aux]
size_properties [in ibw_aux]
subtyping_properties [in abstraction_phd_aux]
subtyping_properties [in ibw_aux]
subtyping_properties [in inw_aux]
sync_properties [in ibw_aux]
sync_properties [in abstraction_phd_aux]
sync_properties [in inw_aux]


T

true_and_false_properties [in inw_aux]
true_and_false_properties [in ibw_aux]


W

well_formed_n_properties [in inw_aux]



Constructor Index

A

abshmake [in abstraction_phd_def]


I

iof [in ibw_aux]



Inductive Index

I

index_of_one [in ibw_aux]



Definition Index

A

absh_equal [in abstraction_phd_aux]
absh_equiv [in abstraction_phd_aux]
absh_equiv_test [in abstraction_phd_aux]
absh_included [in abstraction_phd_def]
absh_included_test [in abstraction_phd_def]
absh_std [in abstraction_phd_def]


C

cg [in floor]


D

delay [in ibw_aux]
delay [in inw_aux]


F

fl [in floor]


I

ibw [in ibw_def]
ibw_of_ones [in ibw_def]
infimum [in ibw_def]
infimum [in inw_def]
inw [in inw_def]
inw_of_ones [in inw_def]
in_abstractionh [in abstraction_phd_def]
in_Z [in Q_misc]


N

non_empty [in abstraction_phd_def]
non_empty_alt [in abstraction_phd_aux]
non_empty_test [in abstraction_phd_def]
non_empty_test_alt [in abstraction_phd_def]
non_null_stream [in inw_aux]
non_null_stream [in ibw_aux]
not [in ibw_def]
not_absh [in abstraction_phd_def]


O

on [in ibw_def]
on [in inw_def]
ones [in ibw_def]
ones [in inw_def]
ones_early [in abstraction_phd_def]
ones_early_alt [in abstraction_phd_def]
ones_early_opt [in abstraction_phd_aux]
ones_infimum [in ibw_def]
ones_infimum [in inw_def]
ones_late [in abstraction_phd_def]
ones_late_alt [in abstraction_phd_def]
ones_late_opt [in abstraction_phd_aux]
ones_supremum [in ibw_def]
ones_supremum [in inw_def]
on_absh [in abstraction_phd_def]


P

prec [in inw_def]
prec [in ibw_def]
prec_absh [in abstraction_phd_def]
prec_absh_alt [in abstraction_phd_def]
prec_absh_test [in abstraction_phd_def]


Q

Qmax [in Q_misc]
Qmin [in Q_misc]
Q_of_nat [in Q_misc]


S

size [in ibw_def]
size [in inw_def]
sizei [in ibw_def]
size_absh [in abstraction_phd_def]
strong_well_formed_abstractionh [in abstraction_phd_def]
subtyping [in inw_def]
subtyping [in ibw_def]
subtyping_absh [in abstraction_phd_def]
subtyping_absh_alt [in abstraction_phd_def]
sum [in inw_def]
supremum [in ibw_def]
supremum [in inw_def]
sync [in ibw_def]
sync [in inw_def]
sync_absh [in abstraction_phd_def]
sync_absh_test [in abstraction_phd_def]
sync_popl [in ibw_aux]


W

well_formed_abstractionh [in abstraction_phd_def]
well_formed_ibw [in ibw_aux]
well_formed_inw [in inw_aux]
well_formed_inw_n [in inw_aux]
well_formed_ones [in inw_aux]
well_formed_ones [in ibw_aux]
well_formed_ones_n [in inw_aux]
w_early [in abstraction_phd_def]
w_false [in inw_aux]
w_false [in ibw_aux]
w_late [in abstraction_phd_def]
w_true [in inw_aux]
w_true [in ibw_aux]


Z

zeros [in ibw_aux]
Z_of_positive [in floor]



Axiom Index

A

ADMITTED [in misc]


C

cg_div_int_rewrite [in floor]
cg_plus_int_rewrite [in floor]


F

fl_div_int_rewrite [in floor]
fl_minus_in_Z [in floor]
fl_minus_not_in_Z [in floor]
fl_m_n [in floor]
fl_plus_int_rewrite [in floor]
fl_rewrite [in floor]


N

n_ge_cg_linear [in floor]
n_le_fl_linear [in floor]



Library Index

A

abstraction_phd_aux
abstraction_phd_def
abstraction_phd_prop


C

comparison


F

floor


I

ibw_aux
ibw_def
ibw_prop
inw_aux
inw_def
inw_prop


M

misc


Q

Q_misc


Z

Z_misc



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 _ (478 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 _ (1 entry)
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 _ (3 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 _ (1 entry)
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 _ (337 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 _ (27 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2 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 _ (1 entry)
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 _ (81 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 _ (11 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 _ (14 entries)

This page has been generated by coqdoc