ALEA.Prog_Intervals

Global Index

J

K

X

Y

_

(2841 entries)

Instance Index

E

G

H

J

K

Q

T

V

W

X

Y

Z

_

other

(149 entries)

Projection Index

A

B

G

H

J

K

Q

V

W

X

Y

Z

_

other

(50 entries)

Record Index

A

B

E

G

H

J

K

L

P

Q

U

V

W

X

Y

Z

_

other

(22 entries)

Lemma Index

J

K

V

X

Y

_

other

(1991 entries)

Section Index

A

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(35 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

(41 entries)

Constructor Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(17 entries)

Inductive Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(9 entries)

Abbreviation Index

A

B

C

D

E

F

G

I

J

K

L

M

N

O

P

Q

S

T

U

W

X

Y

Z

_

other

(4 entries)

Definition Index

J

K

T

V

X

Y

_

other

(345 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(2 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Variable Index

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(148 entries)

Library Index

A

E

F

G

H

J

K

L

N

O

Q

T

V

W

X

Y

Z

_

other

(22 entries)

I

Iapply_rule [lemma, in ALEA.Prog_Intervals]
Id [definition, in ALEA.Ccpo]
id [definition, in ALEA.Ccpo]
Id_simpl [lemma, in ALEA.Ccpo]
Id_mon [instance, in ALEA.Ccpo]
Ieq [definition, in ALEA.Intervals]
Ieq_trans [lemma, in ALEA.Intervals]
Ieq_sym [lemma, in ALEA.Intervals]
Ieq_refl [lemma, in ALEA.Intervals]
Ieq_incl_trans [lemma, in ALEA.Intervals]
Ieq_incl_sym [lemma, in ALEA.Intervals]
Ieq_incl [lemma, in ALEA.Intervals]
Ieq_class [lemma, in ALEA.Intervals]
If [definition, in ALEA.Prog]
Ifixrule [lemma, in ALEA.Prog_Intervals]
IFixrule [section, in ALEA.Prog_Intervals]
IFixrule.A [variable, in ALEA.Prog_Intervals]
IFixrule.B [variable, in ALEA.Prog_Intervals]
IFixrule.F [variable, in ALEA.Prog_Intervals]
IFixrule.IRuleseq [section, in ALEA.Prog_Intervals]
IFixrule.IRuleseq.I [variable, in ALEA.Prog_Intervals]
IFixrule.IRuleseq.Q [variable, in ALEA.Prog_Intervals]
IFixrule.ITransformFix [section, in ALEA.Prog_Intervals]
IFixrule.ITransformFix.IFix_muF.IF_muF_results.Iincl_F_ImuF [variable, in ALEA.Prog_Intervals]
IFixrule.ITransformFix.IFix_muF.IF_muF_results [section, in ALEA.Prog_Intervals]
IFixrule.ITransformFix.IFix_muF.ImuF [variable, in ALEA.Prog_Intervals]
IFixrule.ITransformFix.IFix_muF.Q [variable, in ALEA.Prog_Intervals]
IFixrule.ITransformFix.IFix_muF [section, in ALEA.Prog_Intervals]
IFlip_eq [lemma, in ALEA.Prog_Intervals]
ifok [lemma, in ALEA.Prog]
ifrule [lemma, in ALEA.Prog]
ifte [definition, in ALEA.Misc]
if_mon [instance, in ALEA.Prog]
if_else_not [lemma, in ALEA.Misc]
if_then_not [lemma, in ALEA.Misc]
if_else [lemma, in ALEA.Misc]
if_then [lemma, in ALEA.Misc]
if_beq_nat_nat_eq_dec [lemma, in ALEA.Misc]
if1 [definition, in ALEA.Rplus]
if1_elim [lemma, in ALEA.Rplus]
if1_lt1 [lemma, in ALEA.Rplus]
if1_eq1 [lemma, in ALEA.Rplus]
Iifrule [lemma, in ALEA.Prog_Intervals]
IIim_incl_stable [lemma, in ALEA.Intervals]
Iin [definition, in ALEA.Intervals]
Iincl [definition, in ALEA.Intervals]
Iincl_lim [lemma, in ALEA.Intervals]
Iincl_full [lemma, in ALEA.Intervals]
Iincl_antisym [lemma, in ALEA.Intervals]
Iincl_trans [lemma, in ALEA.Intervals]
Iincl_refl [lemma, in ALEA.Intervals]
Iincl_up [lemma, in ALEA.Intervals]
Iincl_low [lemma, in ALEA.Intervals]
Iincl_in [lemma, in ALEA.Intervals]
Iincl_class [lemma, in ALEA.Intervals]
Iincl_fix_ifix [lemma, in ALEA.Prog_Intervals]
Iin_class [lemma, in ALEA.Intervals]
Iin_sup_intro [lemma, in ALEA.Intervals]
Iin_inf_intro [lemma, in ALEA.Intervals]
Iin_singl_intro [lemma, in ALEA.Intervals]
Iin_sup_elim [lemma, in ALEA.Intervals]
Iin_inf_elim [lemma, in ALEA.Intervals]
Iin_singl_elim [lemma, in ALEA.Intervals]
Iin_up [lemma, in ALEA.Intervals]
Iin_low [lemma, in ALEA.Intervals]
Iin_mu_Iok [lemma, in ALEA.Prog_Intervals]
Iin_mu_Imu [lemma, in ALEA.Prog_Intervals]
Ilambda_rule [lemma, in ALEA.Prog_Intervals]
Ilet_eq [lemma, in ALEA.Prog_Intervals]
Ilim [definition, in ALEA.Intervals]
Imon [definition, in ALEA.Ccpo]
imon [definition, in ALEA.Ccpo]
Imonotonic [lemma, in ALEA.Ccpo]
Imonotonic2 [lemma, in ALEA.Ccpo]
Imon_simpl [lemma, in ALEA.Ccpo]
imon_simpl [lemma, in ALEA.Ccpo]
imon2 [definition, in ALEA.Ccpo]
Imon2 [definition, in ALEA.Ccpo]
Imon2_plus_continuous [lemma, in ALEA.Uprop]
imon2_simpl [lemma, in ALEA.Ccpo]
Imon2_simpl [lemma, in ALEA.Ccpo]
Imu [definition, in ALEA.Prog_Intervals]
ImuF_stable [lemma, in ALEA.Prog_Intervals]
Imult [definition, in ALEA.Intervals]
Imultk [definition, in ALEA.Intervals]
Imultk_in [lemma, in ALEA.Intervals]
Imult_in [lemma, in ALEA.Intervals]
Imu_Mif_eq [lemma, in ALEA.Prog_Intervals]
Imu_sup [lemma, in ALEA.Prog_Intervals]
Imu_inf [lemma, in ALEA.Prog_Intervals]
Imu_singl [lemma, in ALEA.Prog_Intervals]
Imu_stable_eq [lemma, in ALEA.Prog_Intervals]
Imu_monotonic [lemma, in ALEA.Prog_Intervals]
im_range_prop [lemma, in ALEA.Prog]
im_range_map [lemma, in ALEA.Prog]
im_range [lemma, in ALEA.Prog]
im_distr_term [instance, in ALEA.Prog]
im_distr_id [lemma, in ALEA.Prog]
im_distr_comp [lemma, in ALEA.Prog]
im_distr_simpl [lemma, in ALEA.Prog]
im_distr [definition, in ALEA.Prog]
im_range_elim [lemma, in ALEA.Cover]
incl [definition, in ALEA.Sets]
incl_union_stable [lemma, in ALEA.Sets]
incl_add_rem [lemma, in ALEA.Sets]
incl_rem_add [lemma, in ALEA.Sets]
incl_rem_add_iff [lemma, in ALEA.Sets]
incl_add_stable [lemma, in ALEA.Sets]
incl_rem_stable [lemma, in ALEA.Sets]
incl_add_empty [lemma, in ALEA.Sets]
incl_empty_false [lemma, in ALEA.Sets]
incl_empty [lemma, in ALEA.Sets]
incl_trans [lemma, in ALEA.Sets]
incl_refl [lemma, in ALEA.Sets]
incr_decomp [lemma, in ALEA.Uprop]
incr_decomp_aux [lemma, in ALEA.Uprop]
inf [definition, in ALEA.Intervals]
inj_strict_mon [lemma, in ALEA.Ccpo]
int [projection, in ALEA.Rplus]
inter [definition, in ALEA.Sets]
Intervals [library]
inter_dec [lemma, in ALEA.Sets]
inter_add_right_out [lemma, in ALEA.Sets]
inter_add_right_in [lemma, in ALEA.Sets]
inter_add_left_out [lemma, in ALEA.Sets]
inter_add_left_in [lemma, in ALEA.Sets]
inter_empty_right [lemma, in ALEA.Sets]
inter_empty_left [lemma, in ALEA.Sets]
inter_sym [lemma, in ALEA.Sets]
int_floor_le [lemma, in ALEA.Rplus]
int_simpl [lemma, in ALEA.Rplus]
invx_not0 [instance, in ALEA.Rplus]
inv_minus_distr [lemma, in ALEA.Monads]
in_classes_in_class [lemma, in ALEA.IsDiscrete]
in_classes_refl [lemma, in ALEA.IsDiscrete]
in_class_wretract [lemma, in ALEA.IsDiscrete]
In_class [definition, in ALEA.IsDiscrete]
in_class [definition, in ALEA.IsDiscrete]
In_classes [definition, in ALEA.IsDiscrete]
in_classes [definition, in ALEA.IsDiscrete]
In_nth [lemma, in ALEA.RandomList]
Iok [definition, in ALEA.Prog_Intervals]
Iokfun [definition, in ALEA.Prog_Intervals]
Iokfun_le_compat [lemma, in ALEA.Prog_Intervals]
Iok_le_compat [lemma, in ALEA.Prog_Intervals]
Iord [definition, in ALEA.Ccpo]
Iord_app [lemma, in ALEA.Ccpo]
Iplus [definition, in ALEA.Intervals]
Iplus_in [lemma, in ALEA.Intervals]
IsDiscrete [library]
isempty [definition, in ALEA.Sets]
isempty_dec [lemma, in ALEA.Sets]
iseq_dec [lemma, in ALEA.Rplus]
isglb [definition, in ALEA.Ccpo]
isglb_decr_lift [lemma, in ALEA.Ccpo]
isglb_decr_ext [lemma, in ALEA.Ccpo]
isglb_eq_compat_right [lemma, in ALEA.Ccpo]
isglb_eq_compat_left [lemma, in ALEA.Ccpo]
isglb_eq_compat [lemma, in ALEA.Ccpo]
isglb_le [lemma, in ALEA.Ccpo]
isglb_glb_U [lemma, in ALEA.Rplus]
ishift [definition, in ALEA.Ccpo]
ishift_continuous [instance, in ALEA.Ccpo]
ishift_le_compat [lemma, in ALEA.Ccpo]
ishift_simpl [lemma, in ALEA.Ccpo]
ishift_mon [instance, in ALEA.Ccpo]
Isingl_eq [lemma, in ALEA.Intervals]
isle [variable, in ALEA.Rplus]
isle_dec [lemma, in ALEA.Rplus]
isle_lt_dec [lemma, in ALEA.Rplus]
isle_rec [lemma, in ALEA.Rplus]
isle_false [lemma, in ALEA.Rplus]
isle_false_nle [lemma, in ALEA.Rplus]
isle_false_iff [lemma, in ALEA.Rplus]
isle_true [lemma, in ALEA.Rplus]
isle_true_eq [variable, in ALEA.Rplus]
islub [record, in ALEA.Ccpo]
islub_lub [lemma, in ALEA.Ccpo]
islub_mlub [lemma, in ALEA.Ccpo]
islub_fun_intro [lemma, in ALEA.Ccpo]
islub_unique [lemma, in ALEA.Ccpo]
islub_unique_eq [lemma, in ALEA.Ccpo]
islub_decr [lemma, in ALEA.Ccpo]
islub_exch [lemma, in ALEA.Ccpo]
islub_incr_lift [lemma, in ALEA.Ccpo]
islub_incr_ext [lemma, in ALEA.Ccpo]
islub_eq_compat_right [lemma, in ALEA.Ccpo]
islub_eq_compat_left [lemma, in ALEA.Ccpo]
islub_eq_compat [lemma, in ALEA.Ccpo]
islub_le [projection, in ALEA.Ccpo]
islub_U2Rp [lemma, in ALEA.Rplus]
islub_Rpsigma [lemma, in ALEA.Rplus]
islub_lub_U [lemma, in ALEA.Rplus]
islub_Rpmult [lemma, in ALEA.Rplus]
islub_Rpplus_cte_right [lemma, in ALEA.Rplus]
islub_Rpplus_cte_left [lemma, in ALEA.Rplus]
islub_zero [lemma, in ALEA.Rplus]
islub_fcte [lemma, in ALEA.Rplus]
islub_cte [lemma, in ALEA.Rplus]
islub_Rpminus [lemma, in ALEA.Rplus]
islub_Rpplus [lemma, in ALEA.Rplus]
is_discrete_swap_mu [lemma, in ALEA.Prog]
is_discrete_swap [lemma, in ALEA.Prog]
is_discrete [definition, in ALEA.Probas]
is_dec [projection, in ALEA.Markov]
is_limit [definition, in ALEA.Uprop]
is_Rp1div [lemma, in ALEA.Rplus]
is_ge [definition, in ALEA.Cover]
is_gt [definition, in ALEA.Cover]
is_lt [definition, in ALEA.Cover]
is_le [definition, in ALEA.Cover]
is_eq [definition, in ALEA.Cover]
is0 [definition, in ALEA.Rplus]
is1 [definition, in ALEA.Rplus]
Iter [definition, in ALEA.Ccpo]
iter [definition, in ALEA.Ccpo]
iterflip [definition, in ALEA.IterFlip]
IterFlip [library]
iterflip_term [lemma, in ALEA.IterFlip]
iterO_simpl [lemma, in ALEA.Ccpo]
iterS_simpl [lemma, in ALEA.Ccpo]
IterS_simpl [lemma, in ALEA.Ccpo]
iter_continuous_eq [lemma, in ALEA.Ccpo]
iter_continuous [lemma, in ALEA.Ccpo]
iter_monotonic [instance, in ALEA.Ccpo]
iter_mon [instance, in ALEA.Ccpo]
iter_incr [lemma, in ALEA.Ccpo]
iter_ [definition, in ALEA.Ccpo]
IU [record, in ALEA.Intervals]
IUcpo [instance, in ALEA.Intervals]
Iunit_eq [lemma, in ALEA.Prog_Intervals]
IUord [instance, in ALEA.Intervals]

Global Index

J

K

X

Y

_

(2841 entries)

Instance Index

E

G

H

J

K

Q

T

V

W

X

Y

Z

_

other

(149 entries)

Projection Index

A

B

G

H

J

K

Q

V

W

X

Y

Z

_

other

(50 entries)

Record Index

A

B

E

G

H

J

K

L

P

Q

U

V

W

X

Y

Z

_

other

(22 entries)

Lemma Index

J

K

V

X

Y

_

other

(1991 entries)

Section Index

A

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(35 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

(41 entries)

Constructor Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(17 entries)

Inductive Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(9 entries)

Abbreviation Index

A

B

C

D

E

F

G

I

J

K

L

M

N

O

P

Q

S

T

U

W

X

Y

Z

_

other

(4 entries)

Definition Index

J

K

T

V

X

Y

_

other

(345 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(2 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Variable Index

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(148 entries)

Library Index

A

E

F

G

H

J

K

L

N

O

Q

T

V

W

X

Y

Z

_

other

(22 entries)