| 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) |
C
callrFree [definition, in SSProve.Crypt.rhl_semantics.free_monad.FreeProbProg]cardinality_bound [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
card_non_zero [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
card_prod_iprod [lemma, in SSProve.Crypt.package.pkg_distr]
Carrier [section, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
CartesianCategory [section, in SSProve.Relational.EnrichedSetting]
cartesian_category [record, in SSProve.Relational.EnrichedSetting]
Casts [library]
catch [definition, in SSProve.Mon.MonadExamples]
Category [section, in SSProve.Relational.OrderEnrichedCategory]
category [record, in SSProve.Relational.Category]
Category [section, in SSProve.Relational.Category]
Category [library]
cat_law3 [projection, in SSProve.Relational.Category]
cat_law2 [projection, in SSProve.Relational.Category]
cat_law1 [projection, in SSProve.Relational.Category]
cat_inj_tail [lemma, in SSProve.Crypt.jasmin_util]
cat_inj_head [lemma, in SSProve.Crypt.jasmin_util]
cat_mapM2 [lemma, in SSProve.Crypt.jasmin_util]
cat_fold2 [lemma, in SSProve.Crypt.jasmin_util]
CCA_EVAL_equiv_false [lemma, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_HYB_equiv_false [lemma, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_HYB_equiv_true [lemma, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_equiv_true [lemma, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_HYB_pkg [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_HYB_locs [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_TAG_pkg_ff [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_TAG_pkg_tt [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_TAG_locs [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_pkg_ff [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_pkg_tt [definition, in SSProve.Crypt.examples.MACCCA]
CCA_EVAL_locs [definition, in SSProve.Crypt.examples.MACCCA]
cc_law4 [projection, in SSProve.Relational.EnrichedSetting]
cc_law3 [projection, in SSProve.Relational.EnrichedSetting]
cc_law2 [projection, in SSProve.Relational.EnrichedSetting]
cc_law1 [projection, in SSProve.Relational.EnrichedSetting]
cc_prod_into_proper [projection, in SSProve.Relational.EnrichedSetting]
cc_prod_into [projection, in SSProve.Relational.EnrichedSetting]
cc_projr [projection, in SSProve.Relational.EnrichedSetting]
cc_projl [projection, in SSProve.Relational.EnrichedSetting]
cc_prod [projection, in SSProve.Relational.EnrichedSetting]
cc_into_one [projection, in SSProve.Relational.EnrichedSetting]
cc_one [projection, in SSProve.Relational.EnrichedSetting]
cc_cat [projection, in SSProve.Relational.EnrichedSetting]
cenum [projection, in SSProve.Crypt.jasmin_util]
cenumP [projection, in SSProve.Crypt.jasmin_util]
ceqP [projection, in SSProve.Crypt.jasmin_util]
ceqT_eqType [definition, in SSProve.Crypt.jasmin_util]
cfinT_finType [definition, in SSProve.Crypt.jasmin_util]
chBool [constructor, in SSProve.Crypt.choice_type]
chCanonical [definition, in SSProve.Crypt.choice_type]
chCipher [definition, in SSProve.Crypt.examples.KEMDEM]
chDiscr [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
checktag [definition, in SSProve.Crypt.examples.MACCCA]
checktag [definition, in SSProve.Crypt.examples.PRFMAC]
check_size_128_256 [definition, in SSProve.Crypt.jasmin_wsize]
check_size_32_64 [definition, in SSProve.Crypt.jasmin_wsize]
check_size_16_64 [definition, in SSProve.Crypt.jasmin_wsize]
check_size_16_32 [definition, in SSProve.Crypt.jasmin_wsize]
check_size_8_32 [definition, in SSProve.Crypt.jasmin_wsize]
check_size_8_64 [definition, in SSProve.Crypt.jasmin_wsize]
check_scale [definition, in SSProve.Crypt.jasmin_word]
chEKey [definition, in SSProve.Crypt.examples.KEMDEM]
chElement [definition, in SSProve.Crypt.choice_type]
chElement_ordType [definition, in SSProve.Crypt.choice_type]
chFin [constructor, in SSProve.Crypt.choice_type]
ChiKleisli [definition, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
ChiKleisli0 [definition, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
chInt [constructor, in SSProve.Crypt.choice_type]
Chi_CodomainStateAdj [definition, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
Chi_CodomainStateAdj0 [definition, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
Chi_DomainStateAdj [definition, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
Chi_transformedAdjunction [definition, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
chKey [definition, in SSProve.Crypt.examples.KEMDEM]
chList [constructor, in SSProve.Crypt.choice_type]
chMap [constructor, in SSProve.Crypt.choice_type]
chNat [constructor, in SSProve.Crypt.choice_type]
ChoiceAsOrd [section, in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
ChoiceAsOrd [library]
choice_snd_proj [definition, in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
choice_fst_proj [definition, in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
choice_incl [definition, in SSProve.Crypt.rhl_semantics.ChoiceAsOrd]
choice_type_sind [definition, in SSProve.Crypt.choice_type]
choice_type_rec [definition, in SSProve.Crypt.choice_type]
choice_type_ind [definition, in SSProve.Crypt.choice_type]
choice_type_rect [definition, in SSProve.Crypt.choice_type]
choice_type [inductive, in SSProve.Crypt.choice_type]
choice_Countable__to__choice_Choice_isCountable [definition, in SSProve.Crypt.examples.concrete_groups]
choice_Choice__to__choice_hasChoice [definition, in SSProve.Crypt.examples.concrete_groups]
choice_Choice__to__eqtype_hasDecEq [definition, in SSProve.Crypt.Casts]
choice_Choice__to__choice_hasChoice [definition, in SSProve.Crypt.Casts]
choice_type [library]
choose [definition, in SSProve.Mon.MonadExamples]
choose_heap_same [lemma, in SSProve.Crypt.package.pkg_invariants]
choose_heap [definition, in SSProve.Crypt.package.pkg_invariants]
chOption [constructor, in SSProve.Crypt.choice_type]
chProd [constructor, in SSProve.Crypt.choice_type]
chSeq [definition, in SSProve.Crypt.examples.SecretSharing]
chSeq [definition, in SSProve.Crypt.examples.SymmRatchet]
chSeq [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
chSet [definition, in SSProve.Crypt.examples.MACCCA]
chSet [definition, in SSProve.Crypt.examples.SecretSharing]
chSet [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
chSet [definition, in SSProve.Crypt.examples.PRFMAC]
chSet [definition, in SSProve.Crypt.examples.PRPCCA]
chsrc [definition, in SSProve.Crypt.package.pkg_core_definition]
chSum [constructor, in SSProve.Crypt.choice_type]
chtgt [definition, in SSProve.Crypt.package.pkg_core_definition]
chUnit [constructor, in SSProve.Crypt.choice_type]
chWord [constructor, in SSProve.Crypt.choice_type]
ch_nat_ch [lemma, in SSProve.Crypt.package.pkg_interpreter]
ch_nat [definition, in SSProve.Crypt.package.pkg_interpreter]
ch_nat_ch [lemma, in SSProve.Crypt.examples.Executor]
ch_nat [definition, in SSProve.Crypt.examples.Executor]
ch2key [definition, in SSProve.Crypt.examples.OTP]
ch2key_words2ch [lemma, in SSProve.Crypt.examples.OTP]
ch2prod [definition, in SSProve.Crypt.package.pkg_distr]
ch2prod_prod2ch [definition, in SSProve.Crypt.package.pkg_distr]
ch2words [definition, in SSProve.Crypt.examples.OTP]
ch2words_words2ch [lemma, in SSProve.Crypt.examples.OTP]
Ciph [definition, in SSProve.Crypt.examples.PRPCCA]
cipher_location [definition, in SSProve.Crypt.examples.PRF]
ciph_to_pair_mkciph [lemma, in SSProve.Crypt.examples.PRPCCA]
ciph_to_pair [definition, in SSProve.Crypt.examples.PRPCCA]
Ciph_N [definition, in SSProve.Crypt.examples.PRPCCA]
cmd_bind [definition, in SSProve.Crypt.package.pkg_core_definition]
cmd_sample [constructor, in SSProve.Crypt.package.pkg_core_definition]
cmd_put [constructor, in SSProve.Crypt.package.pkg_core_definition]
cmd_get [constructor, in SSProve.Crypt.package.pkg_core_definition]
cmd_op [constructor, in SSProve.Crypt.package.pkg_core_definition]
cmd_put_preserve_pre [lemma, in SSProve.Crypt.package.pkg_rhl]
cmd_get_preserve_pre [lemma, in SSProve.Crypt.package.pkg_rhl]
cmd_sample_preserve_pre [lemma, in SSProve.Crypt.package.pkg_rhl]
cmd_bind_morphism [instance, in SSProve.Crypt.package.pkg_tactics]
CMP [section, in SSProve.Crypt.jasmin_util]
Cmp [record, in SSProve.Crypt.jasmin_util]
CMprod [definition, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
cmp_le_max [lemma, in SSProve.Crypt.jasmin_util]
cmp_max_geR [lemma, in SSProve.Crypt.jasmin_util]
cmp_max_geL [lemma, in SSProve.Crypt.jasmin_util]
cmp_maxP [lemma, in SSProve.Crypt.jasmin_util]
cmp_max [definition, in SSProve.Crypt.jasmin_util]
cmp_le_min [lemma, in SSProve.Crypt.jasmin_util]
cmp_min_leR [lemma, in SSProve.Crypt.jasmin_util]
cmp_min_leL [lemma, in SSProve.Crypt.jasmin_util]
cmp_minP [lemma, in SSProve.Crypt.jasmin_util]
cmp_min [definition, in SSProve.Crypt.jasmin_util]
cmp_le_antisym [lemma, in SSProve.Crypt.jasmin_util]
cmp_le_eq_lt [lemma, in SSProve.Crypt.jasmin_util]
cmp_nle_le [lemma, in SSProve.Crypt.jasmin_util]
cmp_lt_le [lemma, in SSProve.Crypt.jasmin_util]
cmp_le_lt_trans [lemma, in SSProve.Crypt.jasmin_util]
cmp_lt_le_trans [lemma, in SSProve.Crypt.jasmin_util]
cmp_nlt_le [lemma, in SSProve.Crypt.jasmin_util]
cmp_nle_lt [lemma, in SSProve.Crypt.jasmin_util]
cmp_le_trans [lemma, in SSProve.Crypt.jasmin_util]
cmp_lt_trans [lemma, in SSProve.Crypt.jasmin_util]
cmp_le_refl [lemma, in SSProve.Crypt.jasmin_util]
cmp_le [definition, in SSProve.Crypt.jasmin_util]
cmp_lt [definition, in SSProve.Crypt.jasmin_util]
cmp_refl [lemma, in SSProve.Crypt.jasmin_util]
cmp_trans [lemma, in SSProve.Crypt.jasmin_util]
cmp_eq [projection, in SSProve.Crypt.jasmin_util]
cmp_ctrans [projection, in SSProve.Crypt.jasmin_util]
cmp_sym [projection, in SSProve.Crypt.jasmin_util]
cmtSqu [definition, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
cmtSqu_prod [definition, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
code [record, in SSProve.Crypt.package.pkg_core_definition]
code_link_scheme [lemma, in SSProve.Crypt.package.pkg_user_util]
code_link_assertD [lemma, in SSProve.Crypt.package.pkg_user_util]
code_link_assert [lemma, in SSProve.Crypt.package.pkg_user_util]
code_link_map_loop [lemma, in SSProve.Crypt.examples.SymmRatchet]
code_link_if [lemma, in SSProve.Crypt.package.pkg_composition]
code_link_id [lemma, in SSProve.Crypt.package.pkg_composition]
code_link_par_right [lemma, in SSProve.Crypt.package.pkg_composition]
code_link_par_left [lemma, in SSProve.Crypt.package.pkg_composition]
code_link_assoc [lemma, in SSProve.Crypt.package.pkg_composition]
code_link_bind [lemma, in SSProve.Crypt.package.pkg_composition]
code_link [definition, in SSProve.Crypt.package.pkg_composition]
code_ext [lemma, in SSProve.Crypt.package.pkg_core_definition]
CodomainStateAdj [section, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
CodomainStateAdj.J [variable, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
CodomainStateAdj.Lflat [variable, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
CodomainStateAdj.Ordid [variable, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
CodomainStateAdj.preHom [variable, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
CodomainStateAdj.R [variable, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
CodomainStateAdj.S [variable, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
CodomainStateAdj.SConst [variable, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
cod_rel_ord [instance, in SSProve.Mon.SpecificationMonads]
cod_rel [definition, in SSProve.Mon.SpecificationMonads]
coef_poly_eq [lemma, in SSProve.Crypt.examples.PolynomialUtils]
coerce [definition, in SSProve.Crypt.choice_type]
coerceE [lemma, in SSProve.Crypt.choice_type]
coerce_kleisliE [lemma, in SSProve.Crypt.package.pkg_composition]
coerce_kleisli [definition, in SSProve.Crypt.package.pkg_composition]
command [inductive, in SSProve.Crypt.package.pkg_core_definition]
command_sind [definition, in SSProve.Crypt.package.pkg_core_definition]
command_rec [definition, in SSProve.Crypt.package.pkg_core_definition]
command_ind [definition, in SSProve.Crypt.package.pkg_core_definition]
command_rect [definition, in SSProve.Crypt.package.pkg_core_definition]
Commutations [section, in SSProve.Relational.Commutativity]
Commutativity [library]
commute [definition, in SSProve.Relational.Commutativity]
CommuteEffectObs [section, in SSProve.Relational.Commutativity]
commute_effObs [definition, in SSProve.Relational.Commutativity]
commute_bind [lemma, in SSProve.Relational.Commutativity]
commute_ret [lemma, in SSProve.Relational.Commutativity]
commute_sym [lemma, in SSProve.Relational.Commutativity]
commute_elim [lemma, in SSProve.Relational.Commutativity]
commuting_unary_base_square [definition, in SSProve.Crypt.rhl_semantics.only_prob.Theta_dens]
Comp [section, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
Comp [projection, in SSProve.Relational.OrderEnrichedCategory]
Comp [projection, in SSProve.Relational.Category]
comparison_beqP [lemma, in SSProve.Crypt.jasmin_util]
comparison_eq_dec [definition, in SSProve.Crypt.jasmin_util]
compl [definition, in SSProve.Crypt.examples.PRPCCA]
compPair [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
compPairRMonad [definition, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
compRel [definition, in SSProve.Relational.Rel]
computational_sliceMorph [lemma, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
compVsOrder [lemma, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
CompVsOrder [section, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
comp_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
comp_monmon [definition, in SSProve.Mon.SPropMonadicStructures]
comp_monad_morphism [definition, in SSProve.Mon.SPropMonadicStructures]
Comp_proper [projection, in SSProve.Relational.OrderEnrichedCategory]
Comp_proper [projection, in SSProve.Relational.Category]
Comp.J13 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
Comp.phi13 [variable, in SSProve.Crypt.rhl_semantics.more_categories.LaxComp]
ComRing_sort__canonical__CountRing_ComRing [definition, in SSProve.Crypt.Casts]
ComRing_sort__canonical__GRing_ComRing [definition, in SSProve.Crypt.Casts]
ComRing_sort__canonical__choice_SubCountable [definition, in SSProve.Crypt.Casts]
ComRing_sort__canonical__Ord_Ord [definition, in SSProve.Crypt.Casts]
concat_map_nil [lemma, in SSProve.Mon.MonadExamples]
concrete_groups_Z3__canonical__fingroup_FinGroup [definition, in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__fingroup_BaseFinGroup [definition, in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__fintype_Finite [definition, in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__choice_Countable [definition, in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__choice_Choice [definition, in SSProve.Crypt.examples.concrete_groups]
concrete_groups_Z3__canonical__eqtype_Equality [definition, in SSProve.Crypt.examples.concrete_groups]
concrete_groups [library]
conc_map [definition, in SSProve.Crypt.jasmin_util]
cond_pos [projection, in SSProve.Crypt.Prelude]
ConsCtx [definition, in SSProve.Relational.Rel]
ConstantFunctor [section, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
cons_poly_add [lemma, in SSProve.Crypt.examples.PolynomialUtils]
cons_eq_head_tail_poly [lemma, in SSProve.Crypt.examples.PolynomialUtils]
cons_head_tail_poly [lemma, in SSProve.Crypt.examples.PolynomialUtils]
contract_put [lemma, in SSProve.Crypt.package.pkg_rhl]
contract_get [lemma, in SSProve.Crypt.package.pkg_rhl]
cont_perform [definition, in SSProve.Mon.DijkstraMonadExamples]
ConverseCommute [section, in SSProve.Relational.Commutativity]
ConverseCommute.Wrel [variable, in SSProve.Relational.Commutativity]
ConverseCommute.θapp [variable, in SSProve.Relational.Commutativity]
ConverseCommute.θ' [variable, in SSProve.Relational.Commutativity]
ConverseCommute.θ1 [variable, in SSProve.Relational.Commutativity]
ConverseCommute.θ2 [variable, in SSProve.Relational.Commutativity]
converse_to_commute_effObs [lemma, in SSProve.Relational.Commutativity]
count_loc [definition, in SSProve.Crypt.examples.PRFPRG]
Couples_rhs_conj_left [lemma, in SSProve.Crypt.package.pkg_invariants]
Couples_rhs_conj_right [lemma, in SSProve.Crypt.package.pkg_invariants]
Couples_lhs_conj_left [lemma, in SSProve.Crypt.package.pkg_invariants]
Couples_lhs_conj_right [lemma, in SSProve.Crypt.package.pkg_invariants]
Couples_couple_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
Couples_couple_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
Couples_rhs [record, in SSProve.Crypt.package.pkg_invariants]
Couples_rhs [inductive, in SSProve.Crypt.package.pkg_invariants]
Couples_lhs [record, in SSProve.Crypt.package.pkg_invariants]
Couples_lhs [inductive, in SSProve.Crypt.package.pkg_invariants]
couple_rhs [definition, in SSProve.Crypt.package.pkg_invariants]
couple_lhs [definition, in SSProve.Crypt.package.pkg_invariants]
coupling [definition, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
Couplings [library]
Couplings_vs_bind [section, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
Couplings_vs_ret [section, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
coupling_self [lemma, in SSProve.Crypt.rules.RulesStateProb]
coupling_self_SDistr [definition, in SSProve.Crypt.rules.RulesStateProb]
coupling_eq [lemma, in SSProve.Crypt.rules.RulesStateProb]
coupling_vs_bind [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
coupling_vs_ret [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
coupling_SDistr_unit_F_choice_prod [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
Coupling_def [section, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
cpa_epsilon [definition, in SSProve.Crypt.examples.MACCCA]
CPA_EVAL [definition, in SSProve.Crypt.examples.MACCCA]
CPA_EVAL_pkg_ff [definition, in SSProve.Crypt.examples.MACCCA]
CPA_EVAL_pkg_tt [definition, in SSProve.Crypt.examples.MACCCA]
CPA_EVAL_locs [definition, in SSProve.Crypt.examples.MACCCA]
cpa_epsilon [definition, in SSProve.Crypt.examples.SymmRatchet]
Cprod [definition, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
ctrans [definition, in SSProve.Crypt.jasmin_util]
CTRANS [section, in SSProve.Crypt.jasmin_util]
ctransC [lemma, in SSProve.Crypt.jasmin_util]
ctransI [lemma, in SSProve.Crypt.jasmin_util]
ctrans_Gt [lemma, in SSProve.Crypt.jasmin_util]
ctrans_Lt [lemma, in SSProve.Crypt.jasmin_util]
ctrans_Eq [lemma, in SSProve.Crypt.jasmin_util]
CTXT [definition, in SSProve.Crypt.examples.SymmRatchet]
ctxt [definition, in SSProve.Crypt.examples.SymmRatchet]
CTXT [definition, in SSProve.Crypt.examples.PRPCCA]
ctxt [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_pkg_ff [definition, in SSProve.Crypt.examples.SymmRatchet]
CTXT_pkg_tt [definition, in SSProve.Crypt.examples.SymmRatchet]
CTXT_equiv_false [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_equiv_false [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_equiv_6 [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_equiv_5 [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_equiv_4 [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_equiv_3 [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_equiv_2 [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_equiv_1 [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_equiv_true [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_equiv_true [lemma, in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_pkg_ff [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_5 [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_4 [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_3 [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_2 [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_locs_2 [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_pkg_1 [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_HYB_locs_1 [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_SAMP_pkg [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_SAMP_locs [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_pkg_tt [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_EVAL_locs [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_pkg_ff [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_pkg_tt [definition, in SSProve.Crypt.examples.PRPCCA]
CTXT_locs [definition, in SSProve.Crypt.examples.PRPCCA]
cucumber [definition, in SSProve.Crypt.choice_type]
Cucumber [section, in SSProve.Crypt.choice_type]
cucumberK [lemma, in SSProve.Crypt.choice_type]
cucumber' [definition, in SSProve.Crypt.choice_type]
cucumber'K [lemma, in SSProve.Crypt.choice_type]
cucumber''K [lemma, in SSProve.Crypt.choice_type]
CWprod [definition, in SSProve.Crypt.rhl_semantics.more_categories.RelativeMonadMorph_prod]
c_loc [definition, in SSProve.Crypt.examples.KEMDEM]
c_sample [definition, in SSProve.Crypt.rules.RulesStateProb]
| 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) |