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)

F

Fbern [definition, in ALEA.Bernoulli]
Fbern_simpl [lemma, in ALEA.Bernoulli]
Fbern_mon [instance, in ALEA.Bernoulli]
fc [definition, in ALEA.Bernoulli]
fcomp [definition, in ALEA.Ccpo]
fcomp_simpl [lemma, in ALEA.Ccpo]
fcomp2 [definition, in ALEA.Ccpo]
fcomp2_simpl [lemma, in ALEA.Ccpo]
Fconj [definition, in ALEA.Uprop]
fconj [definition, in ALEA.Uprop]
fconj_continuous2 [instance, in ALEA.Uprop]
Fconj_sym [lemma, in ALEA.Uprop]
fconj_sym [lemma, in ALEA.Uprop]
Fconj_simpl [lemma, in ALEA.Uprop]
fconj_fplusok [lemma, in ALEA.Uprop]
fconj_decomp [lemma, in ALEA.Uprop]
fconj_le_compat [lemma, in ALEA.Uprop]
fconj_mon2 [instance, in ALEA.Uprop]
fconj_eq_compat [lemma, in ALEA.Uprop]
fconj_def [lemma, in ALEA.Uprop]
fconj_simpl [lemma, in ALEA.Uprop]
fconj_zero_one [lemma, in ALEA.Cover]
fcont [record, in ALEA.Ccpo]
fcontinuous [projection, in ALEA.Ccpo]
Fcontm [definition, in ALEA.Ccpo]
fcontm [projection, in ALEA.Ccpo]
fcontm_fcont_comp_simpl [lemma, in ALEA.Ccpo]
Fcontm_continuous [instance, in ALEA.Ccpo]
fcontm_monotonic [instance, in ALEA.Ccpo]
fcont_compn_com [lemma, in ALEA.Ccpo]
fcont_compn_Sn_simpl [lemma, in ALEA.Ccpo]
fcont_compn [definition, in ALEA.Ccpo]
fcont_SEQ_simpl [lemma, in ALEA.Ccpo]
fcont_SEQ [definition, in ALEA.Ccpo]
fcont_continuous2 [instance, in ALEA.Ccpo]
fcont_continuous [lemma, in ALEA.Ccpo]
fcont_eq_compat2 [lemma, in ALEA.Ccpo]
fcont_le_compat2 [lemma, in ALEA.Ccpo]
fcont_COMP_simpl [lemma, in ALEA.Ccpo]
fcont_COMP [definition, in ALEA.Ccpo]
fcont_Comp_continuous2 [instance, in ALEA.Ccpo]
fcont_Comp_simpl [lemma, in ALEA.Ccpo]
fcont_Comp [definition, in ALEA.Ccpo]
fcont_comp_le_compat [lemma, in ALEA.Ccpo]
fcont_comp_simpl [lemma, in ALEA.Ccpo]
fcont_comp [definition, in ALEA.Ccpo]
fcont_comp_continuous [instance, in ALEA.Ccpo]
fcont_lub_simpl [lemma, in ALEA.Ccpo]
fcont_app_continuous [lemma, in ALEA.Ccpo]
fcont_mshift [definition, in ALEA.Ccpo]
fcont_ishift [definition, in ALEA.Ccpo]
fcont_app_simpl [lemma, in ALEA.Ccpo]
fcont_app [definition, in ALEA.Ccpo]
fcont_cpo [instance, in ALEA.Ccpo]
fcont_lub [definition, in ALEA.Ccpo]
fcont_lub_continuous [instance, in ALEA.Ccpo]
fcont_eq [lemma, in ALEA.Ccpo]
fcont_le [lemma, in ALEA.Ccpo]
fcont_eq_elim [lemma, in ALEA.Ccpo]
fcont_eq_intro [lemma, in ALEA.Ccpo]
fcont_le_elim [lemma, in ALEA.Ccpo]
fcont_le_intro [lemma, in ALEA.Ccpo]
fcont_ord [instance, in ALEA.Ccpo]
fcont_fun [definition, in ALEA.Ccpo]
fcont0 [definition, in ALEA.Ccpo]
fcont2_comp_simpl [lemma, in ALEA.Ccpo]
fcont2_comp [definition, in ALEA.Ccpo]
fcont2_COMP [definition, in ALEA.Ccpo]
fcpo [instance, in ALEA.Ccpo]
fcpo_lub_simpl [lemma, in ALEA.Ccpo]
fcp_S [lemma, in ALEA.Bernoulli]
fcp_not_le [lemma, in ALEA.Bernoulli]
fcp_n [lemma, in ALEA.Bernoulli]
fcp_0 [lemma, in ALEA.Bernoulli]
Fcte [definition, in ALEA.Uprop]
fcte [definition, in ALEA.Uprop]
fcte_def [lemma, in ALEA.Uprop]
fcte_simpl [lemma, in ALEA.Uprop]
fc_Nmult_def [lemma, in ALEA.Bernoulli]
fc_retract [lemma, in ALEA.Bernoulli]
fc0 [lemma, in ALEA.Bernoulli]
fdiv [definition, in ALEA.Uprop]
fdiv_def [lemma, in ALEA.Uprop]
fdiv_simpl [lemma, in ALEA.Uprop]
feq [definition, in ALEA.Misc]
feq_finv_finv [lemma, in ALEA.Uprop]
feq_intro [lemma, in ALEA.Uprop]
feq_trans [lemma, in ALEA.Misc]
feq_sym [lemma, in ALEA.Misc]
feq_refl [lemma, in ALEA.Misc]
fesp [definition, in ALEA.Uprop]
fesp_le_compat [lemma, in ALEA.Uprop]
fesp_mon2 [instance, in ALEA.Uprop]
fesp_eq_compat [lemma, in ALEA.Uprop]
fesp_def [lemma, in ALEA.Uprop]
fesp_simpl [lemma, in ALEA.Uprop]
fesp_zero_one_mult_right [lemma, in ALEA.Cover]
fesp_zero_one_mult_left [lemma, in ALEA.Cover]
fesp_conj_zero_one [lemma, in ALEA.Cover]
fesp_zero_one [definition, in ALEA.Cover]
Fif [definition, in ALEA.Ccpo]
fif [definition, in ALEA.Ccpo]
fif_continuous2 [lemma, in ALEA.Ccpo]
Fif_continuous2 [instance, in ALEA.Ccpo]
fif_continuous_right [lemma, in ALEA.Ccpo]
fif_continuous_left [lemma, in ALEA.Ccpo]
Fif_continuous_left [lemma, in ALEA.Ccpo]
Fif_continuous_right [lemma, in ALEA.Ccpo]
Fif_simpl [lemma, in ALEA.Ccpo]
fif_mon2 [instance, in ALEA.Ccpo]
Finf [definition, in ALEA.Uprop]
finf [definition, in ALEA.Uprop]
finf_fn [lemma, in ALEA.Uprop]
finf_mon [instance, in ALEA.Uprop]
finf_incr [lemma, in ALEA.Uprop]
finite [inductive, in ALEA.Sets]
finite_inter [lemma, in ALEA.Sets]
finite_full_dec [lemma, in ALEA.Sets]
finite_union [lemma, in ALEA.Sets]
finite_dec [lemma, in ALEA.Sets]
finite_incl [lemma, in ALEA.Sets]
finite_rem [lemma, in ALEA.Sets]
finv [definition, in ALEA.Uprop]
finv_le_compat [lemma, in ALEA.Uprop]
finv_mon [instance, in ALEA.Uprop]
finv_eq_compat [lemma, in ALEA.Uprop]
finv_def [lemma, in ALEA.Uprop]
finv_simpl [lemma, in ALEA.Uprop]
finv_zero_one [lemma, in ALEA.Cover]
fin_add_in [lemma, in ALEA.Sets]
fin_eqset [lemma, in ALEA.Sets]
fin_add [lemma, in ALEA.Sets]
fin_empty [lemma, in ALEA.Sets]
fin_eq_add [constructor, in ALEA.Sets]
fin_eq_empty [constructor, in ALEA.Sets]
Fiter [definition, in ALEA.IterFlip]
Fiter_simpl [lemma, in ALEA.IterFlip]
Fiter_mon [instance, in ALEA.IterFlip]
FixDef [section, in ALEA.Uprop]
FixDef.A [variable, in ALEA.Uprop]
FixDef.F [variable, in ALEA.Uprop]
FIXP [definition, in ALEA.Ccpo]
Fixp [definition, in ALEA.Ccpo]
fixp [definition, in ALEA.Ccpo]
fixp_le_lub [lemma, in ALEA.Ccpo]
fixp_ind_rel [lemma, in ALEA.Ccpo]
fixp_ind [lemma, in ALEA.Ccpo]
fixp_double [lemma, in ALEA.Ccpo]
FIXP_compn [lemma, in ALEA.Ccpo]
FIXP_comp [lemma, in ALEA.Ccpo]
FIXP_comp_com [lemma, in ALEA.Ccpo]
FIXP_inv [lemma, in ALEA.Ccpo]
FIXP_eq [lemma, in ALEA.Ccpo]
FIXP_eq_compat [lemma, in ALEA.Ccpo]
FIXP_le_compat [lemma, in ALEA.Ccpo]
FIXP_simpl [lemma, in ALEA.Ccpo]
Fixp_cont_continuous [instance, in ALEA.Ccpo]
Fixp_cont_simpl [lemma, in ALEA.Ccpo]
Fixp_cont [definition, in ALEA.Ccpo]
fixp_continuous_eq [lemma, in ALEA.Ccpo]
fixp_continuous [lemma, in ALEA.Ccpo]
Fixp_simpl [lemma, in ALEA.Ccpo]
fixp_monotonic [instance, in ALEA.Ccpo]
fixp_le_compat [lemma, in ALEA.Ccpo]
fixp_cte [definition, in ALEA.Ccpo]
fixp_inv [lemma, in ALEA.Ccpo]
fixp_eq [lemma, in ALEA.Ccpo]
fixp_le [lemma, in ALEA.Ccpo]
fixrule [lemma, in ALEA.Prog]
Fixrule [section, in ALEA.Prog]
fixrule_up_lub [lemma, in ALEA.Prog]
fixrule_up_Ulub [lemma, in ALEA.Prog]
fixrule_Ulub [lemma, in ALEA.Prog]
Fixrule.A [variable, in ALEA.Prog]
Fixrule.B [variable, in ALEA.Prog]
Fixrule.F [variable, in ALEA.Prog]
Fixrule.LoopRule [section, in ALEA.Prog]
Fixrule.LoopRule.a [variable, in ALEA.Prog]
Fixrule.LoopRule.q [variable, in ALEA.Prog]
Fixrule.LoopRule.step [variable, in ALEA.Prog]
Fixrule.LoopRule.stop [variable, in ALEA.Prog]
Fixrule.Ruleseq [section, in ALEA.Prog]
Fixrule.Ruleseq.q [variable, in ALEA.Prog]
Fixrule.TransformFix [section, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF_Term.F_muF_le [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF_Term.muFq [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF_Term.F_muF_le_inv [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF_Term.muFqinv [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF_Term.q [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF_Term [section, in ALEA.Prog]
Fixrule.TransformFix.Fix_Term.muF_cont [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_Term.F_muF_eq_one [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_Term.muFone [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_Term [section, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF.F_muF_results.muF_F_le [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF.F_muF_results.F_muF_le [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF.F_muF_results [section, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF.muF [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF.q [variable, in ALEA.Prog]
Fixrule.TransformFix.Fix_muF [section, in ALEA.Prog]
fle_fconj_right [lemma, in ALEA.Uprop]
fle_fconj_left [lemma, in ALEA.Uprop]
fle_fesp_right [lemma, in ALEA.Uprop]
fle_fesp_left [lemma, in ALEA.Uprop]
fle_one [lemma, in ALEA.Uprop]
fle_zero [lemma, in ALEA.Uprop]
fle_fmult [lemma, in ALEA.Uprop]
fle_fplus_right [lemma, in ALEA.Uprop]
fle_fplus_left [lemma, in ALEA.Uprop]
fle_intro [lemma, in ALEA.Uprop]
Flip [definition, in ALEA.Probas]
flip [definition, in ALEA.Probas]
Flip_eq [lemma, in ALEA.Prog]
Flip_false [lemma, in ALEA.Prog]
Flip_true [lemma, in ALEA.Prog]
flip_term [instance, in ALEA.Probas]
Flip_simpl [lemma, in ALEA.Probas]
flip_false [lemma, in ALEA.Probas]
flip_true [lemma, in ALEA.Probas]
flip_continuous [lemma, in ALEA.Probas]
flip_stable_mult [lemma, in ALEA.Probas]
flip_stable_plus [lemma, in ALEA.Probas]
flip_stable_inv [lemma, in ALEA.Probas]
floor [definition, in ALEA.Rplus]
floorN2Rp [lemma, in ALEA.Rplus]
floorR0 [lemma, in ALEA.Rplus]
floorU1 [lemma, in ALEA.Rplus]
floorU1_eq [lemma, in ALEA.Rplus]
floorU2Rp [lemma, in ALEA.Rplus]
floor_U1div0 [lemma, in ALEA.Rplus]
floor_Rpplus_simpl_over [lemma, in ALEA.Rplus]
floor_Rpplus_simpl_ok [lemma, in ALEA.Rplus]
floor_gt_S [lemma, in ALEA.Rplus]
floor_le [lemma, in ALEA.Rplus]
floor_decimal_R0 [lemma, in ALEA.Rplus]
floor_decimal [lemma, in ALEA.Rplus]
floor_eq_R0 [lemma, in ALEA.Rplus]
floor_decimal_U2Rp_elim [lemma, in ALEA.Rplus]
floor_decimal_mkRp_elim [lemma, in ALEA.Rplus]
floor_mkRp_S_int [lemma, in ALEA.Rplus]
floor_S_int_equiv [lemma, in ALEA.Rplus]
floor_S_int [lemma, in ALEA.Rplus]
floor_mkRp_int [lemma, in ALEA.Rplus]
floor_int_equiv [lemma, in ALEA.Rplus]
floor_int [lemma, in ALEA.Rplus]
flub [definition, in ALEA.Uprop]
flub_def [lemma, in ALEA.Uprop]
flub_simpl [lemma, in ALEA.Uprop]
fminus [definition, in ALEA.Uprop]
fminus_le_compat [lemma, in ALEA.Uprop]
fminus_mon2 [instance, in ALEA.Uprop]
fminus_eq_compat [lemma, in ALEA.Uprop]
fminus_def [lemma, in ALEA.Uprop]
fminus_simpl [lemma, in ALEA.Uprop]
fmon [record, in ALEA.Ccpo]
fmono [instance, in ALEA.Ccpo]
fmonotonic [projection, in ALEA.Ccpo]
fmonotonic2 [instance, in ALEA.Ccpo]
fmont [projection, in ALEA.Ccpo]
fmon_lub_simpl [lemma, in ALEA.Ccpo]
fmon_cpo [instance, in ALEA.Ccpo]
fmon_cte_comp [lemma, in ALEA.Ccpo]
fmon_le_compat2 [lemma, in ALEA.Ccpo]
fmon_diag_simpl [lemma, in ALEA.Ccpo]
fmon_eq [lemma, in ALEA.Ccpo]
fmon_le [lemma, in ALEA.Ccpo]
fmon2_mon [instance, in ALEA.Ccpo]
Fmult [definition, in ALEA.Uprop]
fmult [definition, in ALEA.Uprop]
fmult_fplusok [lemma, in ALEA.Prog]
fmult_continuous2 [lemma, in ALEA.Uprop]
Fmult_simpl2 [lemma, in ALEA.Uprop]
Fmult_simpl [lemma, in ALEA.Uprop]
fmult_le_compat [lemma, in ALEA.Uprop]
fmult_mon2 [instance, in ALEA.Uprop]
fmult_eq_compat [lemma, in ALEA.Uprop]
fmult_def [lemma, in ALEA.Uprop]
fmult_simpl [lemma, in ALEA.Uprop]
fmult_mon [instance, in ALEA.Cover]
fnatO_elim [lemma, in ALEA.Ccpo]
fnatO_intro [definition, in ALEA.Ccpo]
fnth [definition, in ALEA.Probas]
fnth_retract [lemma, in ALEA.Probas]
fnth_retract_fin [lemma, in ALEA.Cover]
fn_fsup [lemma, in ALEA.Uprop]
fone [definition, in ALEA.Uprop]
fone_def [lemma, in ALEA.Uprop]
fone_simpl [lemma, in ALEA.Uprop]
ford [instance, in ALEA.Ccpo]
ford_eq_intro [lemma, in ALEA.Ccpo]
ford_eq_elim [lemma, in ALEA.Ccpo]
ford_le_intro [lemma, in ALEA.Ccpo]
ford_le_elim [lemma, in ALEA.Ccpo]
fplus [definition, in ALEA.Uprop]
fplusok [definition, in ALEA.Uprop]
fplusok_mu_term [lemma, in ALEA.Probas]
fplusok_plus_esp [lemma, in ALEA.Probas]
fplusok_le_compat [lemma, in ALEA.Uprop]
fplusok_inv [lemma, in ALEA.Uprop]
fplusok_sym [lemma, in ALEA.Uprop]
fplus_le_compat [lemma, in ALEA.Uprop]
fplus_mon2 [instance, in ALEA.Uprop]
fplus_eq_compat [lemma, in ALEA.Uprop]
fplus_def [lemma, in ALEA.Uprop]
fplus_simpl [lemma, in ALEA.Uprop]
fplus_zero_one [lemma, in ALEA.Cover]
frac [projection, in ALEA.Rplus]
frac_simpl [lemma, in ALEA.Rplus]
fstable [instance, in ALEA.Ccpo]
fstable2 [instance, in ALEA.Ccpo]
fst_prod_distr_term [lemma, in ALEA.Prog]
fst_prod_distr [lemma, in ALEA.Prog]
fst_distr [definition, in ALEA.Prog]
Fsup [definition, in ALEA.Uprop]
fsup [definition, in ALEA.Uprop]
fsup_mon [instance, in ALEA.Uprop]
fsup_incr [lemma, in ALEA.Uprop]
full [definition, in ALEA.Intervals]
full [definition, in ALEA.Sets]
fun_cte_zero [lemma, in ALEA.Uprop]
fun_cte_eq [lemma, in ALEA.Uprop]
fun_cte [definition, in ALEA.Uprop]
fun_ext [definition, in ALEA.Ccpo]
fun2 [definition, in ALEA.Ccpo]
fun2_mon2 [lemma, in ALEA.Ccpo]
fun2_monotonic [instance, in ALEA.Ccpo]
fzero [definition, in ALEA.Uprop]
fzero_def [lemma, in ALEA.Uprop]
fzero_simpl [lemma, in ALEA.Uprop]

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)