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

_

other

(4242 entries)

Notation 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

_

other

(243 entries)

Module 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

_

other

(51 entries)

Variable 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

_

other

(197 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

_

other

(85 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

_

other

(122 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1037 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

_

other

(66 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

_

other

(51 entries)

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

_

other

(271 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

_

other

(291 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

_

other

(46 entries)

Abbreviation 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

_

other

(68 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1638 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

_

other

(76 entries)

---

R (lemma)

rbindP [in SSProve.Crypt.jasmin_util]
rbind_rule [in SSProve.Crypt.package.pkg_rhl]
rcoupling_eq [in SSProve.Crypt.package.pkg_rhl]
Reduction [in SSProve.Crypt.package.pkg_advantage]
ReductionLem [in SSProve.Crypt.package.pkg_advantage]
reflection_nonsense [in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
reflect_all2_eqb [in SSProve.Crypt.jasmin_util]
reflect_inj [in SSProve.Crypt.jasmin_util]
reflexivity_rule [in SSProve.Crypt.rules.RulesStateProb]
refl_true [in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
releffobs_eq_effobs2 [in SSProve.Relational.Commutativity]
releffobs_eq_effobs1 [in SSProve.Relational.Commutativity]
rel_jdg_replace_sem [in SSProve.Crypt.package.pkg_user_util]
rel_jdg_replace [in SSProve.Crypt.package.pkg_user_util]
Remembers_rhs_from_tracked_lhs [in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_from_tracked_rhs [in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs_conj_left [in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs_conj_right [in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_conj_left [in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_conj_right [in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs_rem_rhs [in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_rem_lhs [in SSProve.Crypt.package.pkg_invariants]
remember_pre_conj [in SSProve.Crypt.package.pkg_invariants]
remember_pre_pre [in SSProve.Crypt.package.pkg_invariants]
repr_cmd_Uniform [in SSProve.Crypt.package.pkg_distr]
repr_Uniform [in SSProve.Crypt.package.pkg_distr]
repr_if [in SSProve.Crypt.package.pkg_semantics]
repr_cmd_bind [in SSProve.Crypt.package.pkg_semantics]
repr_bind [in SSProve.Crypt.package.pkg_semantics]
resolve_ID_set [in SSProve.Crypt.package.pkg_composition]
resolve_ID [in SSProve.Crypt.package.pkg_composition]
resolve_par [in SSProve.Crypt.package.pkg_composition]
resolve_link [in SSProve.Crypt.package.pkg_composition]
resolve_set [in SSProve.Crypt.package.pkg_composition]
restore_update_pre [in SSProve.Crypt.package.pkg_invariants]
restore_update_mem [in SSProve.Crypt.package.pkg_invariants]
restore_set_rhs [in SSProve.Crypt.package.pkg_invariants]
restore_set_lhs [in SSProve.Crypt.package.pkg_invariants]
ret_rule [in SSProve.Crypt.rules.RulesStateProb]
ret_rule2 [in SSProve.Relational.GenericRulesSimple]
ret_rule [in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
rewrite_eqDistrR [in SSProve.Crypt.rules.RulesStateProb]
rewrite_eqDistrL [in SSProve.Crypt.rules.RulesStateProb]
rf_preserves_eq [in SSProve.Crypt.package.pkg_rhl]
rif_rule [in SSProve.Crypt.package.pkg_rhl]
right_module_law2 [in SSProve.Relational.RelativeMonads]
right_module_law1 [in SSProve.Relational.RelativeMonads]
rlmm_comp_pointwise_formula [in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
rlmm_comp_assoc [in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
rmg_SDistr_unit [in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
rmon_id_law3 [in SSProve.Relational.RelativeMonads]
rmon_id_law2 [in SSProve.Relational.RelativeMonads]
rmon_id_law1 [in SSProve.Relational.RelativeMonads]
rm_law2_id [in SSProve.Relational.RelativeMonads]
rpost_conclusion_rule_cmd [in SSProve.Crypt.package.pkg_rhl]
rpost_conclusion_rule [in SSProve.Crypt.package.pkg_rhl]
rpost_weaken_rule [in SSProve.Crypt.package.pkg_rhl]
rpre_strong_hypothesis_rule [in SSProve.Crypt.package.pkg_rhl]
rpre_hypothesis_rule [in SSProve.Crypt.package.pkg_rhl]
rpre_weaken_rule [in SSProve.Crypt.package.pkg_rhl]
rreflexivity_rule [in SSProve.Crypt.package.pkg_rhl]
rrewrite_eqDistrR [in SSProve.Crypt.package.pkg_rhl]
rrewrite_eqDistrL [in SSProve.Crypt.package.pkg_rhl]
rsame_head_alt [in SSProve.Crypt.package.pkg_rhl]
rsame_head_alt_pre [in SSProve.Crypt.package.pkg_rhl]
rsame_head_cmd_alt [in SSProve.Crypt.package.pkg_rhl]
rsame_head_cmd [in SSProve.Crypt.package.pkg_rhl]
rsame_head [in SSProve.Crypt.package.pkg_rhl]
rsamplerC [in SSProve.Crypt.package.pkg_rhl]
rsamplerC_sym'_cmd [in SSProve.Crypt.package.pkg_rhl]
rsamplerC_cmd [in SSProve.Crypt.package.pkg_rhl]
rsamplerC_sym' [in SSProve.Crypt.package.pkg_rhl]
rsamplerC' [in SSProve.Crypt.package.pkg_rhl]
rsamplerC'_cmd [in SSProve.Crypt.package.pkg_rhl]
rswap_assertD_assertD_eq [in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_assertD_eq [in SSProve.Crypt.package.pkg_rhl]
rswap_assertD_cmd_eq [in SSProve.Crypt.package.pkg_rhl]
rswap_ruleR_cmd [in SSProve.Crypt.package.pkg_rhl]
rswap_bind_cmd_eq [in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_bind_eq [in SSProve.Crypt.package.pkg_rhl]
rswap_repr_cmd_helper [in SSProve.Crypt.package.pkg_rhl]
rswap_helper_cmd [in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_eq [in SSProve.Crypt.package.pkg_rhl]
rswap_cmd [in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_helper [in SSProve.Crypt.package.pkg_rhl]
rswap_rule_ctx [in SSProve.Crypt.package.pkg_rhl]
rswap_ruleR [in SSProve.Crypt.package.pkg_rhl]
rswap_helper [in SSProve.Crypt.package.pkg_rhl]
rswap_ruleL [in SSProve.Crypt.package.pkg_rhl]
rswap_rule [in SSProve.Crypt.package.pkg_rhl]
rsymmetry [in SSProve.Crypt.package.pkg_rhl]
rsym_pre [in SSProve.Crypt.package.pkg_rhl]
RUN_in_A_export [in SSProve.Crypt.package.pkg_advantage]
rwR1 [in SSProve.Crypt.jasmin_util]
rwR2 [in SSProve.Crypt.jasmin_util]
r_nonneg [in SSProve.Crypt.rules.UniformDistrLemmas]
r_scheme_bind_spec [in SSProve.Crypt.package.pkg_rhl]
r_put_get [in SSProve.Crypt.package.pkg_rhl]
r_put_get_swap' [in SSProve.Crypt.package.pkg_rhl]
r_get_put_swap' [in SSProve.Crypt.package.pkg_rhl]
r_put_get_swap [in SSProve.Crypt.package.pkg_rhl]
r_get_put_swap [in SSProve.Crypt.package.pkg_rhl]
r_put_swap [in SSProve.Crypt.package.pkg_rhl]
r_get_swap [in SSProve.Crypt.package.pkg_rhl]
r_bind_assertD_sym [in SSProve.Crypt.package.pkg_rhl]
r_bind_assertD [in SSProve.Crypt.package.pkg_rhl]
r_cmd_fail [in SSProve.Crypt.package.pkg_rhl]
r_assertD_same [in SSProve.Crypt.package.pkg_rhl]
r_assertD [in SSProve.Crypt.package.pkg_rhl]
r_fail [in SSProve.Crypt.package.pkg_rhl]
r_assertR [in SSProve.Crypt.package.pkg_rhl]
r_assertL [in SSProve.Crypt.package.pkg_rhl]
r_assert [in SSProve.Crypt.package.pkg_rhl]
r_assert' [in SSProve.Crypt.package.pkg_rhl]
r_fail_unit [in SSProve.Crypt.package.pkg_rhl]
r_uniform_prod [in SSProve.Crypt.package.pkg_rhl]
r_uniform_bij [in SSProve.Crypt.package.pkg_rhl]
r_const_sample_R [in SSProve.Crypt.package.pkg_rhl]
r_const_sample_L [in SSProve.Crypt.package.pkg_rhl]
r_dead_sample_R [in SSProve.Crypt.package.pkg_rhl]
r_dead_sample_L [in SSProve.Crypt.package.pkg_rhl]
r_dead_sample [in SSProve.Crypt.package.pkg_rhl]
r_swap_cmd_scheme [in SSProve.Crypt.package.pkg_rhl]
r_swap_scheme_cmd [in SSProve.Crypt.package.pkg_rhl]
r_restore_mem [in SSProve.Crypt.package.pkg_rhl]
r_restore_pre [in SSProve.Crypt.package.pkg_rhl]
r_restore_rhs [in SSProve.Crypt.package.pkg_rhl]
r_restore_lhs [in SSProve.Crypt.package.pkg_rhl]
r_put_vs_put [in SSProve.Crypt.package.pkg_rhl]
r_put_rhs [in SSProve.Crypt.package.pkg_rhl]
r_put_lhs [in SSProve.Crypt.package.pkg_rhl]
r_rem_triple_rhs [in SSProve.Crypt.package.pkg_rhl]
r_rem_couple_rhs [in SSProve.Crypt.package.pkg_rhl]
r_rem_couple_lhs [in SSProve.Crypt.package.pkg_rhl]
r_get_remind_rhs [in SSProve.Crypt.package.pkg_rhl]
r_get_remind_lhs [in SSProve.Crypt.package.pkg_rhl]
r_forget_rhs [in SSProve.Crypt.package.pkg_rhl]
r_forget_lhs [in SSProve.Crypt.package.pkg_rhl]
r_get_vs_get_remember [in SSProve.Crypt.package.pkg_rhl]
r_get_vs_get_remember_rhs [in SSProve.Crypt.package.pkg_rhl]
r_get_vs_get_remember_lhs [in SSProve.Crypt.package.pkg_rhl]
r_get_remember_rhs [in SSProve.Crypt.package.pkg_rhl]
r_get_remember_lhs [in SSProve.Crypt.package.pkg_rhl]
r_reflexivity_alt [in SSProve.Crypt.package.pkg_rhl]
r_transL_val [in SSProve.Crypt.package.pkg_rhl]
r_transR [in SSProve.Crypt.package.pkg_rhl]
r_transL [in SSProve.Crypt.package.pkg_rhl]
r_ret [in SSProve.Crypt.package.pkg_rhl]
r_bind [in SSProve.Crypt.package.pkg_rhl]

---

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

_

other

(4242 entries)

Notation 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

_

other

(243 entries)

Module 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

_

other

(51 entries)

Variable 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

_

other

(197 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

_

other

(85 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

_

other

(122 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1037 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

_

other

(66 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

_

other

(51 entries)

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

_

other

(271 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

_

other

(291 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

_

other

(46 entries)

Abbreviation 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

_

other

(68 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1638 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

_

other

(76 entries)

---

Index

---

This page has been generated by coqdoc