Global Index

B

H

J

K

U

V

Y

_

(352 entries)

Instance Index

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

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

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

B

H

J

K

T

U

V

Y

_

(249 entries)

Section Index

B

C

F

G

H

I

J

K

L

M

Q

R

U

V

W

X

Y

Z

_

(16 entries)

Constructor Index

B

C

D

E

F

G

H

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

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

Definition Index

B

E

G

H

J

K

L

M

R

T

U

V

X

Y

_

(57 entries)

Axiom Index

A

B

D

E

G

H

I

J

K

L

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(11 entries)

Library Index

B

D

E

G

H

J

K

L

N

O

P

R

S

T

U

V

W

X

Y

_

(11 entries)

Global Index

A

abshmake [constructor, in abstraction_hfl_prim_def]
absh_b0 [projection, in abstraction_hfl_prim_def]
absh_b0_neg_impl_ones_ge_a [lemma, in abstraction_hfl_prim_aux]
absh_b1 [projection, in abstraction_hfl_prim_def]
absh_equal [definition, in abstraction_hfl_prim_aux]
absh_equal_correctness [lemma, in abstraction_hfl_prim_aux]
absh_equal_impl_absh_equiv_test [lemma, in abstraction_hfl_prim_aux]
absh_equal_impl_absh_included_test [lemma, in abstraction_hfl_prim_aux]
absh_equal_is_equiv [instance, in abstraction_hfl_prim_aux]
absh_equal_sym [lemma, in abstraction_hfl_prim_aux]
absh_equiv [definition, in abstraction_hfl_prim_aux]
absh_equiv_test [definition, in abstraction_hfl_prim_aux]
absh_equiv_test_impl_absh_equal [lemma, in abstraction_hfl_prim_aux]
absh_included [definition, in abstraction_hfl_prim_def]
absh_included_test [definition, in abstraction_hfl_prim_def]
absh_included_test_correctness [lemma, in abstraction_hfl_prim_prop]
absh_included_test_impl_absh_included [lemma, in abstraction_hfl_prim_aux]
absh_included_test_not_not_absh [lemma, in abstraction_hfl_prim_aux]
absh_r [projection, in abstraction_hfl_prim_def]
absh_std [definition, in abstraction_hfl_prim_def]
absh_weakening [lemma, in abstraction_hfl_prim_prop]
absh_weakening_aux [lemma, in abstraction_hfl_prim_aux]
absh_weakening_0 [lemma, in abstraction_hfl_prim_aux]
abstractionh [record, in abstraction_hfl_prim_def]
Abstractionh_def [section, in abstraction_hfl_prim_aux]
abstraction_equivalence_properties [section, in abstraction_hfl_prim_aux]
abstraction_hfl_prim_aux [library]
abstraction_hfl_prim_def [library]
abstraction_hfl_prim_prop [library]
abs_equal_abs_std_non_empty [lemma, in abstraction_hfl_prim_aux]
abs_le_compat [lemma, in Q_misc]
abs_le_compat_prim [lemma, in Q_misc]
a_prec_w_late [lemma, in abstraction_hfl_prim_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]
comparison [library]

D

delay [definition, in ibw_aux]
delay_d_w_eq_false [lemma, in ibw_aux]
delay_d_w_eq_w [lemma, in ibw_aux]
delay_properties [section, in ibw_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_hfl_prim_aux]
early_def [lemma, in abstraction_hfl_prim_prop]
early_in_abs [lemma, in abstraction_hfl_prim_aux]
early_is_infimum [lemma, in abstraction_hfl_prim_prop]
early_prec_late_impl_early_in_a [lemma, in abstraction_hfl_prim_prop]
early_prec_late_impl_early_late_in_a [lemma, in abstraction_hfl_prim_prop]
early_prec_late_impl_late_in_a [lemma, in abstraction_hfl_prim_prop]
early_prec_late_impl_non_empty [lemma, in abstraction_hfl_prim_prop]
early_prec_late_impl_non_empty_and_early_is_infimum_and_late_is_supremum [lemma, in abstraction_hfl_prim_prop]
early_prec_w [lemma, in abstraction_hfl_prim_prop]

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 [axiom, in floor]
fl_integerp [lemma, in floor]
fl_le_cg [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_correctness [lemma, in ibw_prop]
infimum_is_lowerbound [lemma, in ibw_prop]
infimum_well_formed [lemma, in ibw_aux]
inv_Qden_x_le_inv_Qden_Qred_x [lemma, in Q_misc]
in_abstractionh [definition, in abstraction_hfl_prim_def]
in_Z [definition, in Q_misc]
iof [constructor, in ibw_aux]

L

late_def [lemma, in abstraction_hfl_prim_prop]
late_in_abs [lemma, in abstraction_hfl_prim_aux]
late_is_supremum [lemma, in abstraction_hfl_prim_prop]
le_impl_Qle [lemma, in Q_misc]
le_impl_Zle [lemma, in Q_misc]
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_hfl_prim_def]
non_empty_alt [definition, in abstraction_hfl_prim_aux]
non_empty_equiv_early_prec_late [lemma, in abstraction_hfl_prim_prop]
non_empty_impl_early_prec_late [lemma, in abstraction_hfl_prim_prop]
non_empty_impl_ones_late_le_ones_early [lemma, in abstraction_hfl_prim_aux]
non_empty_test [definition, in abstraction_hfl_prim_def]
non_empty_test_alt [definition, in abstraction_hfl_prim_def]
non_empty_test_correctness [lemma, in abstraction_hfl_prim_prop]
non_empty_test_equal_compat [lemma, in abstraction_hfl_prim_aux]
non_empty_test_impl_ones_late_le_ones_early [lemma, in abstraction_hfl_prim_aux]
non_empty_test_impl_ones_late_le_ones_early_aux [lemma, in abstraction_hfl_prim_aux]
non_empty_test_properties [section, in abstraction_hfl_prim_aux]
non_null_impl_ones_i_eq_j [lemma, in ibw_aux]
non_null_impl_ones_i_ge_j [lemma, in ibw_aux]
non_null_impl_ones_i_le_j [lemma, in ibw_aux]
non_null_stream [definition, in ibw_aux]
not [definition, in ibw_def]
not_absh [definition, in abstraction_hfl_prim_def]
not_absh_correctness [lemma, in abstraction_hfl_prim_prop]
not_absh_correctness_aux [lemma, in abstraction_hfl_prim_aux]
not_absh_well_formed_abstractionh_compat [lemma, in abstraction_hfl_prim_aux]
not_not_absh_equal_absh [lemma, in abstraction_hfl_prim_aux]
not_not_absh_included_test_absh [lemma, in abstraction_hfl_prim_aux]
not_properties [section, in ibw_aux]
not_properties [section, in abstraction_hfl_prim_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]
ones [definition, in ibw_def]
ones_continuous [lemma, in ibw_aux]
ones_delay_d_w_eq_ones_w [lemma, in ibw_aux]
ones_delay_d_w_eq_0 [lemma, in ibw_aux]
ones_delay_d_w_i_eq_ones_w_i_m_d [lemma, in ibw_aux]
ones_early [definition, in abstraction_hfl_prim_def]
ones_early_alt [definition, in abstraction_hfl_prim_def]
ones_early_alt_correctness [lemma, in abstraction_hfl_prim_prop]
ones_early_alt_remove_Zabs_nat [lemma, in abstraction_hfl_prim_aux]
ones_early_eq_ones_early_alt [lemma, in abstraction_hfl_prim_aux]
ones_early_eq_ones_w_early [lemma, in abstraction_hfl_prim_aux]
ones_early_opt [definition, in abstraction_hfl_prim_aux]
ones_early_opt_impl_ones_early [lemma, in abstraction_hfl_prim_aux]
ones_early_rewrite [lemma, in abstraction_hfl_prim_aux]
ones_early_well_formed [lemma, in abstraction_hfl_prim_aux]
ones_eq_equiv_w_eq [lemma, in ibw_prop]
ones_eq_impl_w_eq [lemma, in ibw_aux]
ones_eq_0_impl_w_eq_false [lemma, in ibw_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_increasing [lemma, in ibw_aux]
ones_increasing_by_one [lemma, in ibw_prop]
ones_increasing_one [lemma, in ibw_aux]
ones_increasing_rev [lemma, in ibw_aux]
ones_increasing_x [lemma, in ibw_aux]
ones_infimum [definition, in ibw_def]
ones_infimum_correctness [lemma, in ibw_aux]
ones_infimum_well_formed [lemma, in ibw_aux]
ones_i_eq_0_impl_w_i'_eq_false [lemma, in ibw_aux]
ones_i_le_i [lemma, in ibw_prop]
ones_i_le_i_aux [lemma, in ibw_aux]
ones_late [definition, in abstraction_hfl_prim_def]
ones_late_alt [definition, in abstraction_hfl_prim_def]
ones_late_alt_remove_Zabs_nat [lemma, in abstraction_hfl_prim_aux]
ones_late_eq_ones_early [lemma, in abstraction_hfl_prim_aux]
ones_late_eq_ones_late_alt [lemma, in abstraction_hfl_prim_aux]
ones_late_eq_ones_w_late [lemma, in abstraction_hfl_prim_aux]
ones_late_le_ones_early_impl_early_in_a [lemma, in abstraction_hfl_prim_aux]
ones_late_le_ones_early_impl_late_in_a [lemma, in abstraction_hfl_prim_aux]
ones_late_le_ones_early_impl_non_empty [lemma, in abstraction_hfl_prim_aux]
ones_late_le_ones_w [lemma, in abstraction_hfl_prim_aux]
ones_late_opt [definition, in abstraction_hfl_prim_aux]
ones_late_opt_impl_ones_late [lemma, in abstraction_hfl_prim_aux]
ones_late_rewrite [lemma, in abstraction_hfl_prim_aux]
ones_late_well_formed [lemma, in abstraction_hfl_prim_aux]
ones_not_def [lemma, in ibw_aux]
ones_on [lemma, in ibw_prop]
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_pred_ones_i [lemma, in ibw_aux]
ones_properties [section, in ibw_aux]
ones_supremum [definition, in ibw_def]
ones_supremum_correctness [lemma, in ibw_aux]
ones_supremum_well_formed [lemma, in ibw_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 ibw_aux]
ones_w_le_ones_delay_d_w_p_d [lemma, in ibw_aux]
ones_w_le_ones_early [lemma, in abstraction_hfl_prim_aux]
ones_w_m_d_le_ones_delay_d_w [lemma, in ibw_aux]
on_absh [definition, in abstraction_hfl_prim_def]
on_absh_correctness [lemma, in abstraction_hfl_prim_prop]
on_absh_correctness_aux [lemma, in abstraction_hfl_prim_aux]
on_assoc [lemma, in ibw_prop]
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 ibw_aux]
on_ge_0 [lemma, in abstraction_hfl_prim_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 ibw_aux]
on_prec_reg_l [lemma, in ibw_aux]
on_properties [section, in abstraction_hfl_prim_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_wf_compat [lemma, in ibw_aux]
on_w1_w2_ge_on_a1_a2 [lemma, in abstraction_hfl_prim_aux]
on_w1_w2_le_on_a1_a2 [lemma, in abstraction_hfl_prim_aux]
on_w_false [lemma, in ibw_aux]
on_w_true [lemma, in ibw_aux]

P

plus_impl_Qplus [lemma, in Q_misc]
prec [definition, in ibw_def]
prec_absh [definition, in abstraction_hfl_prim_def]
prec_absh_alt [definition, in abstraction_hfl_prim_def]
prec_absh_alt_complet [lemma, in abstraction_hfl_prim_aux]
prec_absh_alt_correctness [lemma, in abstraction_hfl_prim_aux]
prec_absh_equiv_prec_absh_alt [lemma, in abstraction_hfl_prim_prop]
prec_absh_properties [section, in abstraction_hfl_prim_aux]
prec_absh_test [definition, in abstraction_hfl_prim_def]
prec_absh_test_correctness [lemma, in abstraction_hfl_prim_prop]
prec_absh_test_correctness_aux [lemma, in abstraction_hfl_prim_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_properties [section, in ibw_aux]
prec_refl [lemma, in ibw_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_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 ibw_aux]
red_ones_early [lemma, in abstraction_hfl_prim_aux]
red_ones_early_opt [lemma, in abstraction_hfl_prim_aux]
red_ones_late [lemma, in abstraction_hfl_prim_aux]
red_ones_late_opt [lemma, in abstraction_hfl_prim_aux]

S

simply_1 [lemma, in Q_misc]
simply_1_prim [lemma, in Q_misc]
simpl_std [lemma, in abstraction_hfl_prim_aux]
size [definition, in ibw_def]
subtyping [definition, in ibw_def]
subtyping_absh [definition, in abstraction_hfl_prim_def]
subtyping_absh_alt [definition, in abstraction_hfl_prim_def]
subtyping_absh_alt_impl_subtyping_absh [lemma, in abstraction_hfl_prim_aux]
subtyping_absh_equiv_subtyping_absh_alt [lemma, in abstraction_hfl_prim_prop]
subtyping_absh_impl_subtyping_absh_alt [lemma, in abstraction_hfl_prim_aux]
subtyping_properties [section, in ibw_aux]
subtyping_properties [section, in abstraction_hfl_prim_aux]
supremum [definition, in ibw_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]
sync [definition, in ibw_def]
sync_absh [definition, in abstraction_hfl_prim_def]
sync_absh_test [definition, in abstraction_hfl_prim_def]
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_refl [lemma, in ibw_aux]
sync_sym [lemma, in ibw_aux]
sync_trans [lemma, in ibw_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 ibw_aux]

W

well_formed_abstractionh [definition, in abstraction_hfl_prim_def]
well_formed_abstractionh_absh_equal_compat [lemma, in abstraction_hfl_prim_aux]
well_formed_ibw [definition, in ibw_aux]
well_formed_ones [definition, in ibw_aux]
w_early [definition, in abstraction_hfl_prim_def]
w_early_prec_a [lemma, in abstraction_hfl_prim_aux]
w_early_S_i_eq_false_impl_ones_early_i_gt_a [lemma, in abstraction_hfl_prim_aux]
w_early_S_i_eq_true_impl_ones_early_S_i_le_a [lemma, in abstraction_hfl_prim_aux]
w_early_well_formed [lemma, in abstraction_hfl_prim_aux]
w_eq_impl_ones_eq [lemma, in ibw_aux]
w_false [definition, in ibw_aux]
w_false_well_formed [lemma, in ibw_aux]
w_in_a1_and_a1_in_a2_impl_w_in_a2 [lemma, in abstraction_hfl_prim_aux]
w_i'_eq_false_impl_ones_i_eq_0 [lemma, in ibw_aux]
w_i_eq_true_impl_ones_pos [lemma, in ibw_aux]
w_late [definition, in abstraction_hfl_prim_def]
w_late_well_formed [lemma, in abstraction_hfl_prim_aux]
w_prec_late [lemma, in abstraction_hfl_prim_prop]
w_true [definition, in ibw_aux]
w_true_well_formed [lemma, in ibw_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_hfl_prim_aux]

Projection Index

A

absh_b0 [in abstraction_hfl_prim_def]
absh_b1 [in abstraction_hfl_prim_def]
absh_r [in abstraction_hfl_prim_def]

Record Index

A

abstractionh [in abstraction_hfl_prim_def]

Lemma Index

A

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

C

cg_def [in floor]
cg_def_linear [in floor]
cg_integerp [in floor]
cg_monotone_linear [in floor]
cg_rewrite [in floor]

D

delay_d_w_eq_false [in ibw_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_hfl_prim_prop]
early_in_abs [in abstraction_hfl_prim_aux]
early_is_infimum [in abstraction_hfl_prim_prop]
early_prec_late_impl_early_in_a [in abstraction_hfl_prim_prop]
early_prec_late_impl_early_late_in_a [in abstraction_hfl_prim_prop]
early_prec_late_impl_late_in_a [in abstraction_hfl_prim_prop]
early_prec_late_impl_non_empty [in abstraction_hfl_prim_prop]
early_prec_late_impl_non_empty_and_early_is_infimum_and_late_is_supremum [in abstraction_hfl_prim_prop]
early_prec_w [in abstraction_hfl_prim_prop]

F

fl_cg_in_Z [in floor]
fl_cg_not_in_Z [in floor]
fl_def [in floor]
fl_integerp [in floor]
fl_le_cg [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]
inv_Qden_x_le_inv_Qden_Qred_x [in Q_misc]

L

late_def [in abstraction_hfl_prim_prop]
late_in_abs [in abstraction_hfl_prim_aux]
late_is_supremum [in abstraction_hfl_prim_prop]
le_impl_Qle [in Q_misc]
le_impl_Zle [in Q_misc]
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_hfl_prim_prop]
non_empty_impl_early_prec_late [in abstraction_hfl_prim_prop]
non_empty_impl_ones_late_le_ones_early [in abstraction_hfl_prim_aux]
non_empty_test_correctness [in abstraction_hfl_prim_prop]
non_empty_test_equal_compat [in abstraction_hfl_prim_aux]
non_empty_test_impl_ones_late_le_ones_early [in abstraction_hfl_prim_aux]
non_empty_test_impl_ones_late_le_ones_early_aux [in abstraction_hfl_prim_aux]
non_null_impl_ones_i_eq_j [in ibw_aux]
non_null_impl_ones_i_ge_j [in ibw_aux]
non_null_impl_ones_i_le_j [in ibw_aux]
not_absh_correctness [in abstraction_hfl_prim_prop]
not_absh_correctness_aux [in abstraction_hfl_prim_aux]
not_absh_well_formed_abstractionh_compat [in abstraction_hfl_prim_aux]
not_not_absh_equal_absh [in abstraction_hfl_prim_aux]
not_not_absh_included_test_absh [in abstraction_hfl_prim_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_0 [in ibw_aux]
ones_delay_d_w_i_eq_ones_w_i_m_d [in ibw_aux]
ones_early_alt_correctness [in abstraction_hfl_prim_prop]
ones_early_alt_remove_Zabs_nat [in abstraction_hfl_prim_aux]
ones_early_eq_ones_early_alt [in abstraction_hfl_prim_aux]
ones_early_eq_ones_w_early [in abstraction_hfl_prim_aux]
ones_early_opt_impl_ones_early [in abstraction_hfl_prim_aux]
ones_early_rewrite [in abstraction_hfl_prim_aux]
ones_early_well_formed [in abstraction_hfl_prim_aux]
ones_eq_equiv_w_eq [in ibw_prop]
ones_eq_impl_w_eq [in ibw_aux]
ones_eq_0_impl_w_eq_false [in ibw_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_increasing [in ibw_aux]
ones_increasing_by_one [in ibw_prop]
ones_increasing_one [in ibw_aux]
ones_increasing_rev [in ibw_aux]
ones_increasing_x [in ibw_aux]
ones_infimum_correctness [in ibw_aux]
ones_infimum_well_formed [in ibw_aux]
ones_i_eq_0_impl_w_i'_eq_false [in ibw_aux]
ones_i_le_i [in ibw_prop]
ones_i_le_i_aux [in ibw_aux]
ones_late_alt_remove_Zabs_nat [in abstraction_hfl_prim_aux]
ones_late_eq_ones_early [in abstraction_hfl_prim_aux]
ones_late_eq_ones_late_alt [in abstraction_hfl_prim_aux]
ones_late_eq_ones_w_late [in abstraction_hfl_prim_aux]
ones_late_le_ones_early_impl_early_in_a [in abstraction_hfl_prim_aux]
ones_late_le_ones_early_impl_late_in_a [in abstraction_hfl_prim_aux]
ones_late_le_ones_early_impl_non_empty [in abstraction_hfl_prim_aux]
ones_late_le_ones_w [in abstraction_hfl_prim_aux]
ones_late_opt_impl_ones_late [in abstraction_hfl_prim_aux]
ones_late_rewrite [in abstraction_hfl_prim_aux]
ones_late_well_formed [in abstraction_hfl_prim_aux]
ones_not_def [in ibw_aux]
ones_on [in ibw_prop]
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_pred_ones_i [in ibw_aux]
ones_supremum_correctness [in ibw_aux]
ones_supremum_well_formed [in ibw_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 ibw_aux]
ones_w_le_ones_delay_d_w_p_d [in ibw_aux]
ones_w_le_ones_early [in abstraction_hfl_prim_aux]
ones_w_m_d_le_ones_delay_d_w [in ibw_aux]
on_absh_correctness [in abstraction_hfl_prim_prop]
on_absh_correctness_aux [in abstraction_hfl_prim_aux]
on_assoc [in ibw_prop]
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 ibw_aux]
on_ge_0 [in abstraction_hfl_prim_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 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_wf_compat [in ibw_aux]
on_w1_w2_ge_on_a1_a2 [in abstraction_hfl_prim_aux]
on_w1_w2_le_on_a1_a2 [in abstraction_hfl_prim_aux]
on_w_false [in ibw_aux]
on_w_true [in ibw_aux]

P

plus_impl_Qplus [in Q_misc]
prec_absh_alt_complet [in abstraction_hfl_prim_aux]
prec_absh_alt_correctness [in abstraction_hfl_prim_aux]
prec_absh_equiv_prec_absh_alt [in abstraction_hfl_prim_prop]
prec_absh_test_correctness [in abstraction_hfl_prim_prop]
prec_absh_test_correctness_aux [in abstraction_hfl_prim_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_refl [in ibw_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_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 ibw_aux]
red_ones_early [in abstraction_hfl_prim_aux]
red_ones_early_opt [in abstraction_hfl_prim_aux]
red_ones_late [in abstraction_hfl_prim_aux]
red_ones_late_opt [in abstraction_hfl_prim_aux]

S

simply_1 [in Q_misc]
simply_1_prim [in Q_misc]
simpl_std [in abstraction_hfl_prim_aux]
subtyping_absh_alt_impl_subtyping_absh [in abstraction_hfl_prim_aux]
subtyping_absh_equiv_subtyping_absh_alt [in abstraction_hfl_prim_prop]
subtyping_absh_impl_subtyping_absh_alt [in abstraction_hfl_prim_aux]
supremum_correctness [in ibw_prop]
supremum_is_upperbound [in ibw_prop]
supremum_prec_upperbounds [in ibw_prop]
supremum_well_formed [in ibw_aux]
sync_equiv_relation [in ibw_prop]
sync_popl_impl_sync [in ibw_aux]
sync_refl [in ibw_aux]
sync_sym [in ibw_aux]
sync_trans [in ibw_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_hfl_prim_aux]
w_early_prec_a [in abstraction_hfl_prim_aux]
w_early_S_i_eq_false_impl_ones_early_i_gt_a [in abstraction_hfl_prim_aux]
w_early_S_i_eq_true_impl_ones_early_S_i_le_a [in abstraction_hfl_prim_aux]
w_early_well_formed [in abstraction_hfl_prim_aux]
w_eq_impl_ones_eq [in ibw_aux]
w_false_well_formed [in ibw_aux]
w_in_a1_and_a1_in_a2_impl_w_in_a2 [in abstraction_hfl_prim_aux]
w_i'_eq_false_impl_ones_i_eq_0 [in ibw_aux]
w_i_eq_true_impl_ones_pos [in ibw_aux]
w_late_well_formed [in abstraction_hfl_prim_aux]
w_prec_late [in abstraction_hfl_prim_prop]
w_true_well_formed [in ibw_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_hfl_prim_aux]
abstraction_equivalence_properties [in abstraction_hfl_prim_aux]

D

delay_properties [in ibw_aux]

E

early_and_late_properties [in abstraction_hfl_prim_aux]

N

non_empty_test_properties [in abstraction_hfl_prim_aux]
not_properties [in ibw_aux]
not_properties [in abstraction_hfl_prim_aux]

O

ones_properties [in ibw_aux]
on_properties [in abstraction_hfl_prim_aux]
on_properties [in ibw_aux]

P

prec_absh_properties [in abstraction_hfl_prim_aux]
prec_properties [in ibw_aux]

S

subtyping_properties [in ibw_aux]
subtyping_properties [in abstraction_hfl_prim_aux]
sync_properties [in ibw_aux]

T

true_and_false_properties [in ibw_aux]

Constructor Index

A

abshmake [in abstraction_hfl_prim_def]

I

iof [in ibw_aux]

Inductive Index

I

index_of_one [in ibw_aux]

Definition Index

A

absh_equal [in abstraction_hfl_prim_aux]
absh_equiv [in abstraction_hfl_prim_aux]
absh_equiv_test [in abstraction_hfl_prim_aux]
absh_included [in abstraction_hfl_prim_def]
absh_included_test [in abstraction_hfl_prim_def]
absh_std [in abstraction_hfl_prim_def]

C

cg [in floor]

D

delay [in ibw_aux]

F

fl [in floor]

I

ibw [in ibw_def]
ibw_of_ones [in ibw_def]
infimum [in ibw_def]
in_abstractionh [in abstraction_hfl_prim_def]
in_Z [in Q_misc]

N

non_empty [in abstraction_hfl_prim_def]
non_empty_alt [in abstraction_hfl_prim_aux]
non_empty_test [in abstraction_hfl_prim_def]
non_empty_test_alt [in abstraction_hfl_prim_def]
non_null_stream [in ibw_aux]
not [in ibw_def]
not_absh [in abstraction_hfl_prim_def]

O

on [in ibw_def]
ones [in ibw_def]
ones_early [in abstraction_hfl_prim_def]
ones_early_alt [in abstraction_hfl_prim_def]
ones_early_opt [in abstraction_hfl_prim_aux]
ones_infimum [in ibw_def]
ones_late [in abstraction_hfl_prim_def]
ones_late_alt [in abstraction_hfl_prim_def]
ones_late_opt [in abstraction_hfl_prim_aux]
ones_supremum [in ibw_def]
on_absh [in abstraction_hfl_prim_def]

P

prec [in ibw_def]
prec_absh [in abstraction_hfl_prim_def]
prec_absh_alt [in abstraction_hfl_prim_def]
prec_absh_test [in abstraction_hfl_prim_def]

Q

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

S

size [in ibw_def]
subtyping [in ibw_def]
subtyping_absh [in abstraction_hfl_prim_def]
subtyping_absh_alt [in abstraction_hfl_prim_def]
supremum [in ibw_def]
sync [in ibw_def]
sync_absh [in abstraction_hfl_prim_def]
sync_absh_test [in abstraction_hfl_prim_def]
sync_popl [in ibw_aux]

W

well_formed_abstractionh [in abstraction_hfl_prim_def]
well_formed_ibw [in ibw_aux]
well_formed_ones [in ibw_aux]
w_early [in abstraction_hfl_prim_def]
w_false [in ibw_aux]
w_late [in abstraction_hfl_prim_def]
w_true [in ibw_aux]

Z

zeros [in ibw_aux]
Z_of_positive [in floor]

Axiom Index

C

cg_div_int_rewrite [in floor]
cg_plus_int_rewrite [in floor]

F

fl_div_int_rewrite [in floor]
fl_eq_cg [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_hfl_prim_aux
abstraction_hfl_prim_def
abstraction_hfl_prim_prop

C

F

floor

I

ibw_aux
ibw_def
ibw_prop

M

misc

Q

Q_misc

Z

Z_misc

Global Index

B

H

J

K

U

V

Y

_

(352 entries)

Instance Index

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

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

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

B

H

J

K

T

U

V

Y

_

(249 entries)

Section Index

B

C

F

G

H

I

J

K

L

M

Q

R

U

V

W

X

Y

Z

_

(16 entries)

Constructor Index

B

C

D

E

F

G

H

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

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(1 entry)

Definition Index

B

E

G

H

J

K

L

M

R

T

U

V

X

Y

_

(57 entries)

Axiom Index

A

B

D

E

G

H

I

J

K

L

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(11 entries)

Library Index

B

D

E

G

H

J

K

L

N

O

P

R

S

T

U

V

W

X

Y

_

(11 entries)

This page has been generated by coqdoc