SSProve.Mon.SpecificationMonads

Global Index

(4242 entries)

Notation Index

B

C

H

I

J

L

N

Q

T

U

V

W

X

Y

Z

_

(243 entries)

Module Index

B

C

H

I

J

K

L

M

N

Q

T

U

V

W

X

Y

_

other

(51 entries)

Variable Index

G

I

J

K

N

Q

V

W

X

Y

Z

_

other

(197 entries)

Library Index

H

N

Q

V

W

X

Y

Z

_

other

(85 entries)

Constructor Index

B

J

K

M

Q

X

Y

other

(122 entries)

Lemma Index

J

Q

_

(1037 entries)

Axiom Index

B

C

F

H

I

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

other

(66 entries)

Inductive Index

B

G

J

K

M

Q

U

X

Y

_

other

(51 entries)

Projection Index

G

J

Q

T

U

X

Y

Z

other

(271 entries)

Section Index

J

Q

V

X

Y

_

other

(291 entries)

Instance Index

F

H

J

K

N

Q

T

V

X

Y

_

other

(46 entries)

Abbreviation Index

B

C

E

H

J

K

N

Q

T

V

X

Y

_

(68 entries)

Definition Index

X

Y

_

(1638 entries)

Record Index

B

G

H

J

Q

U

W

X

Y

Z

_

other

(76 entries)

R

r [definition, in SSProve.Crypt.rules.UniformDistrLemmas]
R [axiom, in SSProve.Crypt.Axioms]
raise [definition, in SSProve.Mon.MonadExamples]
Raise [constructor, in SSProve.Mon.MonadExamples]
ran [definition, in SSProve.Mon.SPropMonadicStructures]
RandomOracle [library]
ran_iso [definition, in SSProve.Mon.SPropMonadicStructures]
ran_mono [definition, in SSProve.Mon.SPropMonadicStructures]
rapp [abbreviation, in SSProve.Crypt.jasmin_util]
raw_package [definition, in SSProve.Crypt.package.pkg_core_definition]
raw_code_sind [definition, in SSProve.Crypt.package.pkg_core_definition]
raw_code_rec [definition, in SSProve.Crypt.package.pkg_core_definition]
raw_code_ind [definition, in SSProve.Crypt.package.pkg_core_definition]
raw_code_rect [definition, in SSProve.Crypt.package.pkg_core_definition]
raw_code [inductive, in SSProve.Crypt.package.pkg_core_definition]
rbind [abbreviation, in SSProve.Relational.OrderEnrichedCategory]
rbind [abbreviation, in SSProve.Relational.RelativeMonads]
rbind [abbreviation, in SSProve.Crypt.jasmin_util]
rbindP [lemma, in SSProve.Crypt.jasmin_util]
rbind_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rcoupling_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rdflt [abbreviation, in SSProve.Crypt.jasmin_util]
read [definition, in SSProve.Mon.MonadExamples]
Read [constructor, in SSProve.Mon.MonadExamples]
Redefined_sprop_constructs.unbox [projection, in SSProve.Mon.SPropBase]
Redefined_sprop_constructs.Box [record, in SSProve.Mon.SPropBase]
Redefined_sprop_constructs [module, in SSProve.Mon.SPropBase]
Reduction [lemma, in SSProve.Crypt.package.pkg_advantage]
ReductionLem [lemma, in SSProve.Crypt.package.pkg_advantage]
reflection_nonsense [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
reflect_m [instance, in SSProve.Crypt.jasmin_util]
reflect_all2_eqb [lemma, in SSProve.Crypt.jasmin_util]
reflect_inj [lemma, in SSProve.Crypt.jasmin_util]
reflexivity_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
refl_true [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
Rel [definition, in SSProve.Relational.Rel]
Rel [section, in SSProve.Relational.Rel]
Rel [library]
relationalEffectObservation [record, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalEffectObservation [section, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalEffectObservation.RelationalEffectObservationComponents [section, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalEffectObservation0 [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalLaxEffectObservation0 [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalProgramLogicFromRelativeMonadZero [section, in SSProve.Relational.GenericRulesSimple]
⊨ _ ≈ _ [{ _ }] [notation, in SSProve.Relational.GenericRulesSimple]
RelationalSpecMonad [record, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalSpecMonad [section, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalSpecMonadZeroFromOrderedMonad [section, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RelationalSpecMonad0 [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
Relational_effobs [section, in SSProve.Crypt.rhl_semantics.only_prob.Theta_dens]
relation_from_mmorph [definition, in SSProve.Mon.SPropMonadicStructures]
RelativeFreeMonad [section, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
RelativeKleisli [section, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
RelativeKleisliAdjunction [section, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
relativeLaxMonadMorphism [record, in SSProve.Relational.OrderEnrichedCategory]
RelativeLaxMonadMorphism [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonad [section, in SSProve.Relational.OrderEnrichedCategory]
relativeMonad [record, in SSProve.Relational.RelativeMonads]
RelativeMonad [section, in SSProve.Relational.RelativeMonads]
RelativeMonadFromLeftRelAdjunction [section, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
RelativeMonadFromLeftRelAdjunction.Chi [variable, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
RelativeMonadIso [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadIso [section, in SSProve.Relational.RelativeMonads]
RelativeMonadLifting [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadLifting.LiftingDatum [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadLifting.LiftingDatum.uMC [variable, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadLifting.LiftingDatum.uMCF [variable, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadLifting.LiftingDatum.uMD [variable, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadLifting.LiftingOf [section, in SSProve.Relational.OrderEnrichedCategory]
relativeMonadMorphism [record, in SSProve.Relational.OrderEnrichedCategory]
relativeMonadMorphism [record, in SSProve.Relational.RelativeMonads]
RelativeMonadMorphism [section, in SSProve.Relational.RelativeMonads]
RelativeMonadMorphismToRightModule [section, in SSProve.Relational.RelativeMonads]
RelativeMonadMorphismToRightModule.W [variable, in SSProve.Relational.RelativeMonads]
relativeMonadMorphism_to_lax [definition, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadMorph_prod [library]
RelativeMonadPostcomposition [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadPostcomposition [section, in SSProve.Relational.RelativeMonads]
RelativeMonadPostcomposition.FJ [variable, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadPostcomposition.FJ [variable, in SSProve.Relational.RelativeMonads]
RelativeMonadPrecomposition [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadPrecomposition [section, in SSProve.Relational.RelativeMonads]
RelativeMonadPrecomposition.OnMorphism [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadPrecomposition.OnMorphism [section, in SSProve.Relational.RelativeMonads]
RelativeMonadPrecomposition.OnObjects [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadPrecomposition.OnObjects [section, in SSProve.Relational.RelativeMonads]
J* [notation, in SSProve.Relational.OrderEnrichedCategory]
J* [notation, in SSProve.Relational.RelativeMonads]
RelativeMonads [library]
RelativeMonadToFunctor [section, in SSProve.Relational.OrderEnrichedCategory]
RelativeMonadToFunctor [section, in SSProve.Relational.RelativeMonads]
relativeMonad_postcomposition [definition, in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_precomposition_lax_morph [definition, in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_precomposition_morph [definition, in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_precomposition [definition, in SSProve.Relational.OrderEnrichedCategory]
relativeMonad_postcomposition [definition, in SSProve.Relational.RelativeMonads]
relativeMonad_precomposition_morph [definition, in SSProve.Relational.RelativeMonads]
relativeMonad_precomposition [definition, in SSProve.Relational.RelativeMonads]
RelCat [definition, in SSProve.Relational.Rel]
RelCat [section, in SSProve.Relational.Rel]
releffobs_eq_effobs2 [lemma, in SSProve.Relational.Commutativity]
releffobs_eq_effobs1 [lemma, in SSProve.Relational.Commutativity]
relKleisli [definition, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
relmonObj [projection, in SSProve.Relational.RelativeMonads]
Relmon_equations [section, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
relmon_law3 [projection, in SSProve.Relational.RelativeMonads]
relmon_law2 [projection, in SSProve.Relational.RelativeMonads]
relmon_law1 [projection, in SSProve.Relational.RelativeMonads]
relmon_bind_proper [projection, in SSProve.Relational.RelativeMonads]
relmon_bind [projection, in SSProve.Relational.RelativeMonads]
relmon_unit [projection, in SSProve.Relational.RelativeMonads]
relMon_fromLeftAdj [definition, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
RelNotations [module, in SSProve.Relational.Rel]
_ ,∙ _ [notation, in SSProve.Relational.Rel]
_ ,∘ _ [notation, in SSProve.Relational.Rel]
_ @R _ [notation, in SSProve.Relational.Rel]
_ R==> _ [notation, in SSProve.Relational.Rel]
_ R=> _ [notation, in SSProve.Relational.Rel]
[< _ | _ >] [notation, in SSProve.Relational.Rel]
⟬ _ ⟭ [notation, in SSProve.Relational.Rel]
⦑ _ , _ | _ | _ ⦒ [notation, in SSProve.Relational.Rel]
⦑ _ , _ | _ ⦒ [notation, in SSProve.Relational.Rel]
⦑ _ , _ ⦒ [notation, in SSProve.Relational.Rel]
RelNotations.πl [abbreviation, in SSProve.Relational.Rel]
RelNotations.πr [abbreviation, in SSProve.Relational.Rel]
RelNotations.πw [abbreviation, in SSProve.Relational.Rel]
Relw [definition, in SSProve.Relational.Rel]
rel_jdg_replace_sem [lemma, in SSProve.Crypt.package.pkg_user_util]
rel_jdg_replace [lemma, in SSProve.Crypt.package.pkg_user_util]
rel_prod_fmap [definition, in SSProve.Relational.Rel]
rel_prod [definition, in SSProve.Relational.Rel]
rel_one [definition, in SSProve.Relational.Rel]
Rel_mon_morph_prod [section, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
rel_jdg_sind [definition, in SSProve.Crypt.package.pkg_rhl]
rel_jdg_rec [definition, in SSProve.Crypt.package.pkg_rhl]
rel_jdg_ind [definition, in SSProve.Crypt.package.pkg_rhl]
rel_jdg_rect [definition, in SSProve.Crypt.package.pkg_rhl]
rel_jdg [inductive, in SSProve.Crypt.package.pkg_rhl]
_ @R _ [notation, in SSProve.Relational.Rel]
_ R==> _ [notation, in SSProve.Relational.Rel]
_ R=> _ [notation, in SSProve.Relational.Rel]
[< _ | _ >] [notation, in SSProve.Relational.Rel]
⟬ _ ⟭ [notation, in SSProve.Relational.Rel]
⦑ _ , _ | _ | _ ⦒ [notation, in SSProve.Relational.Rel]
⦑ _ , _ | _ ⦒ [notation, in SSProve.Relational.Rel]
⦑ _ , _ ⦒ [notation, in SSProve.Relational.Rel]
Remembers_rhs_from_tracked_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_from_tracked_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs_conj_left [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs_conj_right [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_conj_left [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_conj_right [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs_rem_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs_rem_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs [record, in SSProve.Crypt.package.pkg_invariants]
Remembers_rhs [inductive, in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs [record, in SSProve.Crypt.package.pkg_invariants]
Remembers_lhs [inductive, in SSProve.Crypt.package.pkg_invariants]
remember_pre_conj [lemma, in SSProve.Crypt.package.pkg_invariants]
remember_pre_pre [lemma, in SSProve.Crypt.package.pkg_invariants]
remember_pre [definition, in SSProve.Crypt.package.pkg_invariants]
rem_rhs [definition, in SSProve.Crypt.package.pkg_invariants]
rem_lhs [definition, in SSProve.Crypt.package.pkg_invariants]
reoc_law2 [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
reoc_law1 [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
reoc_carrier [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
reo_rel [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
reo_right [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
reo_left [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
reo_components [record, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
repr [definition, in SSProve.Crypt.package.pkg_semantics]
repr_cmd_Uniform [lemma, in SSProve.Crypt.package.pkg_distr]
repr_Uniform [lemma, in SSProve.Crypt.package.pkg_distr]
repr_if [lemma, in SSProve.Crypt.package.pkg_semantics]
repr_cmd_bind [lemma, in SSProve.Crypt.package.pkg_semantics]
repr_cmd [definition, in SSProve.Crypt.package.pkg_semantics]
repr_bind [lemma, in SSProve.Crypt.package.pkg_semantics]
resolve [definition, in SSProve.Crypt.package.pkg_composition]
resolve_ID_set [lemma, in SSProve.Crypt.package.pkg_composition]
resolve_ID [lemma, in SSProve.Crypt.package.pkg_composition]
resolve_par [lemma, in SSProve.Crypt.package.pkg_composition]
resolve_link [lemma, in SSProve.Crypt.package.pkg_composition]
resolve_set [lemma, in SSProve.Crypt.package.pkg_composition]
restore_update_pre [lemma, in SSProve.Crypt.package.pkg_invariants]
restore_update_mem [lemma, in SSProve.Crypt.package.pkg_invariants]
restore_set_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
restore_set_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
Result [module, in SSProve.Crypt.jasmin_util]
result [inductive, in SSProve.Crypt.jasmin_util]
results_from_the_paper [definition, in SSProve.Crypt.Main]
Result.apply [definition, in SSProve.Crypt.jasmin_util]
Result.bind [definition, in SSProve.Crypt.jasmin_util]
Result.default [definition, in SSProve.Crypt.jasmin_util]
Result.map [definition, in SSProve.Crypt.jasmin_util]
ret [definition, in SSProve.Mon.SPropMonadicStructures]
ret [constructor, in SSProve.Crypt.package.pkg_core_definition]
retF [definition, in SSProve.Crypt.rules.RulesStateProb]
retFree [constructor, in SSProve.Mon.MonadExamples]
retrFree [constructor, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
retW [definition, in SSProve.Crypt.rules.RulesStateProb]
retW [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
retWUpd [definition, in SSProve.Mon.SpecificationMonads]
ret_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
ret_mmorph [definition, in SSProve.Mon.MonadExamples]
ret_rule2 [lemma, in SSProve.Relational.GenericRulesSimple]
ret_rule [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
rewrite_eqDistrR [lemma, in SSProve.Crypt.rules.RulesStateProb]
rewrite_eqDistrL [lemma, in SSProve.Crypt.rules.RulesStateProb]
rFree [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF [inductive, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_sind [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_rec [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_ind [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeF_rect [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreePr [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeProb_squ [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rFreeProb_squ_fromProd [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
rf_preserves_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rhs [constructor, in SSProve.Crypt.package.pkg_invariants]
rif_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rightHom [definition, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
RightModule [section, in SSProve.Relational.RelativeMonads]
rightModuleHomomorphism [record, in SSProve.Relational.RelativeMonads]
rightModuleHomomorphism [inductive, in SSProve.Relational.RelativeMonads]
RightModuleHomomorphism [section, in SSProve.Relational.RelativeMonads]
RightModuleId [section, in SSProve.Relational.RelativeMonads]
RightModuleId.FM [variable, in SSProve.Relational.RelativeMonads]
RightModulePostcomposition [section, in SSProve.Relational.RelativeMonads]
RightModulePostcomposition.GF [variable, in SSProve.Relational.RelativeMonads]
rightModuleStructure [record, in SSProve.Relational.RelativeMonads]
rightModule_postcomp [definition, in SSProve.Relational.RelativeMonads]
right_assoc_rlmm_comp [definition, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
right_proj_functor [definition, in SSProve.Relational.OrderEnrichedCategory]
right_module_law2 [lemma, in SSProve.Relational.RelativeMonads]
right_module_law1 [lemma, in SSProve.Relational.RelativeMonads]
right_module_nattrans [definition, in SSProve.Relational.RelativeMonads]
right_proj_functor [definition, in SSProve.Relational.Category]
rlmm_comp_pointwise_formula [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
rlmm_comp_assoc [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
rlmm_comp [definition, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
rlmm_law2 [projection, in SSProve.Relational.OrderEnrichedCategory]
rlmm_law1 [projection, in SSProve.Relational.OrderEnrichedCategory]
rlmm_map [projection, in SSProve.Relational.OrderEnrichedCategory]
rlmm_from_lmla [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
rlmm_codomain [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
rlmm_domain [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
rlmm_codomain [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
rlmm_domain [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
rmap [abbreviation, in SSProve.Crypt.jasmin_util]
rmg [definition, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
rmg_SDistr_unit [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
rmm_law2 [projection, in SSProve.Relational.OrderEnrichedCategory]
rmm_law1 [projection, in SSProve.Relational.OrderEnrichedCategory]
rmm_map [projection, in SSProve.Relational.OrderEnrichedCategory]
rmm_law2 [projection, in SSProve.Relational.RelativeMonads]
rmm_law1 [projection, in SSProve.Relational.RelativeMonads]
rmm_map [projection, in SSProve.Relational.RelativeMonads]
rMonad [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RMonadAsMonad [section, in SSProve.Relational.RelativeMonads]
RmonadUnit [section, in SSProve.Relational.RelativeMonads]
rmon_transp_natIso [definition, in SSProve.Relational.OrderEnrichedCategory]
rmon_to_ord_functor [definition, in SSProve.Relational.OrderEnrichedCategory]
rmon_morph_right_module [definition, in SSProve.Relational.RelativeMonads]
rmon_transp_natIso [definition, in SSProve.Relational.RelativeMonads]
rmon_id_law3 [lemma, in SSProve.Relational.RelativeMonads]
rmon_id_law2 [lemma, in SSProve.Relational.RelativeMonads]
rmon_id_law1 [lemma, in SSProve.Relational.RelativeMonads]
rmon_id_mult [definition, in SSProve.Relational.RelativeMonads]
rmon_unit [definition, in SSProve.Relational.RelativeMonads]
rmon_to_functor [definition, in SSProve.Relational.RelativeMonads]
rm_homo [projection, in SSProve.Relational.RelativeMonads]
rm_homo [constructor, in SSProve.Relational.RelativeMonads]
rm_law2_id [lemma, in SSProve.Relational.RelativeMonads]
rm_law3 [projection, in SSProve.Relational.RelativeMonads]
rm_law2 [projection, in SSProve.Relational.RelativeMonads]
rm_law1 [projection, in SSProve.Relational.RelativeMonads]
rm_bind_proper [projection, in SSProve.Relational.RelativeMonads]
rm_bind [projection, in SSProve.Relational.RelativeMonads]
RO [module, in SSProve.Crypt.examples.RandomOracle]
ROParams [module, in SSProve.Crypt.examples.RandomOracle]
ROParams.Query [axiom, in SSProve.Crypt.examples.RandomOracle]
ROParams.Query_pos [axiom, in SSProve.Crypt.examples.RandomOracle]
ROParams.Random [axiom, in SSProve.Crypt.examples.RandomOracle]
ROParams.Random_pos [axiom, in SSProve.Crypt.examples.RandomOracle]
ropr [constructor, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]
RO.chQuery [definition, in SSProve.Crypt.examples.RandomOracle]
RO.chRandom [definition, in SSProve.Crypt.examples.RandomOracle]
RO.INIT [definition, in SSProve.Crypt.examples.RandomOracle]
RO.i_random [definition, in SSProve.Crypt.examples.RandomOracle]
RO.queries_loc [definition, in SSProve.Crypt.examples.RandomOracle]
RO.QUERY [definition, in SSProve.Crypt.examples.RandomOracle]
RO.RO [definition, in SSProve.Crypt.examples.RandomOracle]
RO.RO_exports [definition, in SSProve.Crypt.examples.RandomOracle]
RO.RO_locs [definition, in SSProve.Crypt.examples.RandomOracle]
pack_type:'random [notation, in SSProve.Crypt.examples.RandomOracle]
pack_type:'query [notation, in SSProve.Crypt.examples.RandomOracle]
rpost_conclusion_rule_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
rpost_conclusion_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rpost_weaken_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rpre_strong_hypothesis_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rpre_hypothesis_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rpre_weaken_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rreflexivity_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rrewrite_eqDistrR [lemma, in SSProve.Crypt.package.pkg_rhl]
rrewrite_eqDistrL [lemma, in SSProve.Crypt.package.pkg_rhl]
rsame_head_alt [lemma, in SSProve.Crypt.package.pkg_rhl]
rsame_head_alt_pre [lemma, in SSProve.Crypt.package.pkg_rhl]
rsame_head_cmd_alt [lemma, in SSProve.Crypt.package.pkg_rhl]
rsame_head_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
rsame_head [lemma, in SSProve.Crypt.package.pkg_rhl]
rsamplerC [lemma, in SSProve.Crypt.package.pkg_rhl]
rsamplerC_sym'_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
rsamplerC_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
rsamplerC_sym' [lemma, in SSProve.Crypt.package.pkg_rhl]
rsamplerC' [lemma, in SSProve.Crypt.package.pkg_rhl]
rsamplerC'_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
RSemanticNotation [module, in SSProve.Crypt.rules.RulesStateProb]
⊨ ⦃ _ ⦄ _ ≈ _ ⦃ _ ⦄ (rsemantic_scope) [notation, in SSProve.Crypt.rules.RulesStateProb]
⊨ _ ≈ _ [{ _ }] (rsemantic_scope) [notation, in SSProve.Crypt.rules.RulesStateProb]
rsmc_law3 [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsmc_law2 [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsmc_law1 [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsmc_act_proper [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsmc_act [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsmc_return [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsmc_carrier [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsm_rel [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsm_right [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsm_left [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
rsm_components [record, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
RSPNotation [module, in SSProve.Crypt.rules.RulesStateProb]
_ ;; _ (RulesStateProb_scope) [notation, in SSProve.Crypt.rules.RulesStateProb]
_ ∈ _ <<- _ ;; _ (RulesStateProb_scope) [notation, in SSProve.Crypt.rules.RulesStateProb]
_ <- _ ;; _ (RulesStateProb_scope) [notation, in SSProve.Crypt.rules.RulesStateProb]
rswap_assertD_assertD_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_assertD_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_assertD_cmd_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_ruleR_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_bind_cmd_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_bind_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_repr_cmd_helper [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_helper_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_cmd_helper [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_rule_ctx [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_ruleR [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_helper [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_ruleL [lemma, in SSProve.Crypt.package.pkg_rhl]
rswap_rule [lemma, in SSProve.Crypt.package.pkg_rhl]
rsymmetry [lemma, in SSProve.Crypt.package.pkg_rhl]
rsym_pre [lemma, in SSProve.Crypt.package.pkg_rhl]
RT_TRANSN.SPEC [section, in SSProve.Crypt.jasmin_util]
RT_TRANSN [section, in SSProve.Crypt.jasmin_util]
RulesProb [library]
RulesStateProb [library]
RUN [definition, in SSProve.Crypt.package.pkg_advantage]
Run [definition, in SSProve.Crypt.package.pkg_interpreter]
Run [definition, in SSProve.Crypt.examples.Executor]
RUN_in_A_export [lemma, in SSProve.Crypt.package.pkg_advantage]
Run_aux [definition, in SSProve.Crypt.package.pkg_interpreter]
Run_aux [definition, in SSProve.Crypt.examples.Executor]
rwR1 [lemma, in SSProve.Crypt.jasmin_util]
rwR2 [lemma, in SSProve.Crypt.jasmin_util]
r_nonneg [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
r_scheme_bind_spec [lemma, in SSProve.Crypt.package.pkg_rhl]
r_put_get [lemma, in SSProve.Crypt.package.pkg_rhl]
r_put_get_swap' [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_put_swap' [lemma, in SSProve.Crypt.package.pkg_rhl]
r_put_get_swap [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_put_swap [lemma, in SSProve.Crypt.package.pkg_rhl]
r_put_swap [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_swap [lemma, in SSProve.Crypt.package.pkg_rhl]
r_bind_assertD_sym [lemma, in SSProve.Crypt.package.pkg_rhl]
r_bind_assertD [lemma, in SSProve.Crypt.package.pkg_rhl]
r_cmd_fail [lemma, in SSProve.Crypt.package.pkg_rhl]
r_assertD_same [lemma, in SSProve.Crypt.package.pkg_rhl]
r_assertD [lemma, in SSProve.Crypt.package.pkg_rhl]
r_fail [lemma, in SSProve.Crypt.package.pkg_rhl]
r_assertR [lemma, in SSProve.Crypt.package.pkg_rhl]
r_assertL [lemma, in SSProve.Crypt.package.pkg_rhl]
r_assert [lemma, in SSProve.Crypt.package.pkg_rhl]
r_assert' [lemma, in SSProve.Crypt.package.pkg_rhl]
r_fail_unit [lemma, in SSProve.Crypt.package.pkg_rhl]
r_uniform_prod [lemma, in SSProve.Crypt.package.pkg_rhl]
r_uniform_bij [lemma, in SSProve.Crypt.package.pkg_rhl]
r_const_sample_R [lemma, in SSProve.Crypt.package.pkg_rhl]
r_const_sample_L [lemma, in SSProve.Crypt.package.pkg_rhl]
r_dead_sample_R [lemma, in SSProve.Crypt.package.pkg_rhl]
r_dead_sample_L [lemma, in SSProve.Crypt.package.pkg_rhl]
r_dead_sample [lemma, in SSProve.Crypt.package.pkg_rhl]
r_swap_cmd_scheme [lemma, in SSProve.Crypt.package.pkg_rhl]
r_swap_scheme_cmd [lemma, in SSProve.Crypt.package.pkg_rhl]
r_restore_mem [lemma, in SSProve.Crypt.package.pkg_rhl]
r_restore_pre [lemma, in SSProve.Crypt.package.pkg_rhl]
r_restore_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_restore_lhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_put_vs_put [lemma, in SSProve.Crypt.package.pkg_rhl]
r_put_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_put_lhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_rem_triple_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_rem_couple_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_rem_couple_lhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_remind_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_remind_lhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_forget_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_forget_lhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_vs_get_remember [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_vs_get_remember_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_vs_get_remember_lhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_remember_rhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_get_remember_lhs [lemma, in SSProve.Crypt.package.pkg_rhl]
r_reflexivity_alt [lemma, in SSProve.Crypt.package.pkg_rhl]
r_transL_val [lemma, in SSProve.Crypt.package.pkg_rhl]
r_transR [lemma, in SSProve.Crypt.package.pkg_rhl]
r_transL [lemma, in SSProve.Crypt.package.pkg_rhl]
r_ret [lemma, in SSProve.Crypt.package.pkg_rhl]
r_bind [lemma, in SSProve.Crypt.package.pkg_rhl]
R_loc [definition, in SSProve.Crypt.examples.PRPCCA]

Global Index

(4242 entries)

Notation Index

B

C

H

I

J

L

N

Q

T

U

V

W

X

Y

Z

_

(243 entries)

Module Index

B

C

H

I

J

K

L

M

N

Q

T

U

V

W

X

Y

_

other

(51 entries)

Variable Index

G

I

J

K

N

Q

V

W

X

Y

Z

_

other

(197 entries)

Library Index

H

N

Q

V

W

X

Y

Z

_

other

(85 entries)

Constructor Index

B

J

K

M

Q

X

Y

other

(122 entries)

Lemma Index

J

Q

_

(1037 entries)

Axiom Index

B

C

F

H

I

J

K

L

M

N

O

P

Q

T

V

W

X

Y

Z

_

other

(66 entries)

Inductive Index

B

G

J

K

M

Q

U

X

Y

_

other

(51 entries)

Projection Index

G

J

Q

T

U

X

Y

Z

other

(271 entries)

Section Index

J

Q

V

X

Y

_

other

(291 entries)

Instance Index

F

H

J

K

N

Q

T

V

X

Y

_

other

(46 entries)

Abbreviation Index

B

C

E

H

J

K

N

Q

T

V

X

Y

_

(68 entries)

Definition Index

X

Y

_

(1638 entries)

Record Index

B

G

H

J

Q

U

W

X

Y

Z

_

other

(76 entries)