| 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) |
S
SA [projection, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]salt_location [definition, in SSProve.Crypt.examples.PRF]
sameSome [definition, in SSProve.Crypt.package.pkg_user_util]
sameSomeRel [definition, in SSProve.Crypt.package.pkg_user_util]
sameSomeRel_sameSome [lemma, in SSProve.Crypt.package.pkg_user_util]
sameSome_None_l [lemma, in SSProve.Crypt.package.pkg_user_util]
SAMP [definition, in SSProve.Crypt.examples.PRPCCA]
samp [definition, in SSProve.Crypt.examples.PRPCCA]
Sample [record, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
samplee [constructor, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
sampleFsq_support [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
sampleFsq_f_coupling [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
sampleFsq_f [definition, in SSProve.Crypt.rules.UniformDistrLemmas]
sampler [constructor, in SSProve.Crypt.package.pkg_core_definition]
sampler [definition, in SSProve.Crypt.package.pkg_interpreter]
sampler [definition, in SSProve.Crypt.examples.Executor]
samplerC_rule.SD_ret [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.SD_bind [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.utheta_dens_fld [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.sploP [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.Frp_fld [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.splo [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.Arst [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.Opst [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.Ar [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule.Op [variable, in SSProve.Crypt.rules.RulesStateProb]
samplerC_rule [section, in SSProve.Crypt.rules.RulesStateProb]
sampler_case [lemma, in SSProve.Crypt.package.pkg_rhl]
sampler_morphism [instance, in SSProve.Crypt.package.pkg_tactics]
sample_c_is_c_sample [lemma, in SSProve.Crypt.rules.RulesStateProb]
sample_c [definition, in SSProve.Crypt.rules.RulesStateProb]
sample_subset_in [lemma, in SSProve.Crypt.examples.PRPCCA]
sample_subset [definition, in SSProve.Crypt.examples.PRPCCA]
sample_rule [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
SAMP_pkg_ff [definition, in SSProve.Crypt.examples.PRPCCA]
SAMP_pkg_tt [definition, in SSProve.Crypt.examples.PRPCCA]
samp_no_repl [definition, in SSProve.Crypt.examples.PRPCCA]
sand [definition, in SSProve.Mon.SPropBase]
saturated_signed [definition, in SSProve.Crypt.jasmin_word]
SB [projection, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
scheme_spec [definition, in SSProve.Crypt.package.pkg_rhl]
Schnorr [module, in SSProve.Crypt.examples.Schnorr]
Schnorr [library]
Schnorr_Z3 [module, in SSProve.Crypt.examples.Schnorr]
Schnorr.bij_f [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.compat [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.cyclic_zeta [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.extractor_success [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.f [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.group_prodA [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.group_prodC [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg [module, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.choiceBool [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.choiceChallenge [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.choiceMessage [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.choiceResponse [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.choiceStatement [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.choiceTranscript [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.choiceWitness [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.Commit [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.commit_loc [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.Extractor [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.i_witness [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.KeyGen [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.Response [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.Sigma_locs [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.Simulate [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.Simulator_locs [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyAlg.Verify [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam [module, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Bool_pos [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Challenge [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Challenge_pos [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.e0 [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Message [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Message_pos [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.positive_gT [instance, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.R [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Response [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Response_pos [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Statement [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Statement_pos [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Transcript [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Witness [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.Witness_pos [instance, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.w0 [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.MyParam.z0 [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.neq_pos [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.order_ge1 [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.otf_neq [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.q [definition, in SSProve.Crypt.examples.Schnorr]
Schnorr.schnorr_com_binding [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.schnorr_com_hiding [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.schnorr_SHVZK [lemma, in SSProve.Crypt.examples.Schnorr]
Schnorr.Sigma [module, in SSProve.Crypt.examples.Schnorr]
schoice [lemma, in SSProve.Crypt.Axioms]
SCond [projection, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
SDistr [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_squ [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_assoc [lemma, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_leftneutral [lemma, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_rightneutral [lemma, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_bind [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_unit [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_carrier [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_carrier0_preorder_preorder [instance, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_carrier0_preorder [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_carrier0 [definition, in SSProve.Crypt.rhl_semantics.only_prob.SubDistr]
SDistr_unit_F_choice_prod_coupling [lemma, in SSProve.Crypt.rhl_semantics.only_prob.Couplings]
SDistr_bind_unit_unit [lemma, in SSProve.Crypt.package.pkg_rhl]
SD_commutativity' [lemma, in SSProve.Crypt.rules.RulesStateProb]
SD_commutativity [lemma, in SSProve.Crypt.rules.RulesStateProb]
se [definition, in SSProve.Mon.Monoid]
SecretSharing [library]
'set _ (package_scope) [notation, in SSProve.Crypt.examples.SecretSharing]
pack_type:'set _ [notation, in SSProve.Crypt.examples.SecretSharing]
'seq _ (package_scope) [notation, in SSProve.Crypt.examples.SecretSharing]
pack_type:'seq _ [notation, in SSProve.Crypt.examples.SecretSharing]
'word (package_scope) [notation, in SSProve.Crypt.examples.SecretSharing]
pack_type:'word [notation, in SSProve.Crypt.examples.SecretSharing]
_ ⊕ _ [notation, in SSProve.Crypt.examples.SecretSharing]
SecretSharing_example.n [variable, in SSProve.Crypt.examples.SecretSharing]
SecretSharing_example [section, in SSProve.Crypt.examples.SecretSharing]
security_based_on_mac [lemma, in SSProve.Crypt.examples.MACCCA]
security_based_on_prg [lemma, in SSProve.Crypt.examples.StretchPRG]
security_based_on_prf [lemma, in SSProve.Crypt.examples.PRF]
security_based_on_prf [lemma, in SSProve.Crypt.examples.PRFMAC]
security_based_on_prp [lemma, in SSProve.Crypt.examples.PRPCCA]
security_based_on_prf [lemma, in SSProve.Crypt.examples.PRFPRG]
sec_share_bij [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
sec_poly_bij [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
sec_poly_bij_rec [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
sec_poly_bij_part [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
self_commute [lemma, in SSProve.Mon.FiniteProbabilities]
SemanticNotation [module, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
⊨ ⦃ _ ⦄ _ ≈ _ ⦃ _ ⦄ (semantic_scope) [notation, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
⊨ _ ≈ _ [{ _ }] (semantic_scope) [notation, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
semantic_judgement [definition, in SSProve.Crypt.rules.RulesStateProb]
semantic_judgement [definition, in SSProve.Relational.GenericRulesSimple]
semantic_judgement [definition, in SSProve.Crypt.rhl_semantics.only_prob.Theta_exCP]
SemiInvariant [record, in SSProve.Crypt.package.pkg_invariants]
SemiInvariant_triple_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
SemiInvariant_couple_rhs [lemma, in SSProve.Crypt.package.pkg_invariants]
SemiInvariant_couple_lhs [lemma, in SSProve.Crypt.package.pkg_invariants]
sem_to_det [lemma, in SSProve.Crypt.package.pkg_rhl]
seq_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
seq_to_chseq [definition, in SSProve.Crypt.examples.SymmRatchet]
seq_rule [lemma, in SSProve.Relational.GenericRulesSimple]
seq_dup_lo [definition, in SSProve.Crypt.jasmin_word]
seq_dup_hi [definition, in SSProve.Crypt.jasmin_word]
seq_eq_injL [lemma, in SSProve.Crypt.jasmin_util]
SET [definition, in SSProve.Crypt.examples.KEMDEM]
set_heap_commut [lemma, in SSProve.Crypt.package.pkg_heap]
set_heap_contract [lemma, in SSProve.Crypt.package.pkg_heap]
set_heap [definition, in SSProve.Crypt.package.pkg_heap]
set_rhs [definition, in SSProve.Crypt.package.pkg_invariants]
set_lhs [definition, in SSProve.Crypt.package.pkg_invariants]
sgett [constructor, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
ShamirSecretSharing [library]
ShamirSecretSharing_example.t' [variable, in SSProve.Crypt.examples.ShamirSecretSharing]
'party (package_scope) [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
pack_type:'party [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
ShamirSecretSharing_example.n [variable, in SSProve.Crypt.examples.ShamirSecretSharing]
'set _ (package_scope) [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
pack_type:'set _ [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
'seq _ (package_scope) [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
pack_type:'seq _ [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
'share (package_scope) [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
pack_type:'share [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
'word (package_scope) [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
pack_type:'word [notation, in SSProve.Crypt.examples.ShamirSecretSharing]
ShamirSecretSharing_example.p [variable, in SSProve.Crypt.examples.ShamirSecretSharing]
ShamirSecretSharing_example [section, in SSProve.Crypt.examples.ShamirSecretSharing]
SHARE [definition, in SSProve.Crypt.examples.SecretSharing]
SHARE [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
Share [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
shares [definition, in SSProve.Crypt.examples.SecretSharing]
shares [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
SHARE_equiv [lemma, in SSProve.Crypt.examples.SecretSharing]
SHARE_pkg_ff [definition, in SSProve.Crypt.examples.SecretSharing]
SHARE_pkg_tt [definition, in SSProve.Crypt.examples.SecretSharing]
SHARE_equiv [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
SHARE_pkg_ff [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
SHARE_pkg_tt [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
share_bij [definition, in SSProve.Crypt.examples.ShamirSecretSharing]
side [inductive, in SSProve.Crypt.package.pkg_invariants]
side_sind [definition, in SSProve.Crypt.package.pkg_invariants]
side_rec [definition, in SSProve.Crypt.package.pkg_invariants]
side_ind [definition, in SSProve.Crypt.package.pkg_invariants]
side_rect [definition, in SSProve.Crypt.package.pkg_invariants]
sig [definition, in SSProve.Crypt.examples.package_usage_example]
sigLemmas [section, in SSProve.Mon.SPropBase]
sigMap [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SigmaProtocol [module, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol [library]
SigmaProtocolAlgorithms [module, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.choiceBool [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.choiceChallenge [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.choiceMessage [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.choiceResponse [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.choiceStatement [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.choiceTranscript [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.choiceWitness [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.Commit [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.Extractor [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.KeyGen [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.Response [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.Sigma_locs [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.Simulate [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.Simulator_locs [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolAlgorithms.Verify [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams [module, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Bool_pos [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Challenge [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Challenge_pos [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.e0 [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Message [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Message_pos [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.R [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Response [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Response_pos [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Statement [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Statement_pos [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Witness [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.Witness_pos [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.w0 [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocolParams.z0 [axiom, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.ADV [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.challenge_loc [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.choiceInput [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.choiceOpen [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.COM [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Commitments [section, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chHiding [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chKeys [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chOpen [notation, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.commitment_binding [lemma, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.commitment_hiding [lemma, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Com_Binding [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Com_locs [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.FiatShamir [section, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.fiat_shamir_correct [lemma, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Fiat_Shamir_SIM [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Fiat_Shamir [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.GET [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.HIDING [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Hiding_ideal [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Hiding_real [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Hiding_E [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.INIT [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.inv [abbreviation, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Invariant_inv [instance, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.IRUN [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.i_witness_pos [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.i_challenge_pos [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.i_witness [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.i_challenge [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.KEY [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.KEY_locs [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.OPEN [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Opening [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Oracle [module, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.OracleParams [module, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.OracleParams.Query [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.OracleParams.Query_pos [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.OracleParams.Random [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.OracleParams.Random_pos [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.prod_assoc [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.response_loc [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.RUN [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.run_interactive_shvzk [lemma, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.RUN_interactive [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.setup_loc [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.SHVZK_real_aux [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.SHVZK_ideal [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.SHVZK_real [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Sigma_to_Com_Aux [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Sigma_to_Com [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Sigma_to_Com_locs [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.SIM [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.SOUNDNESS [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Special_Soundness_t [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.Special_Soundness_f [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.statement_loc [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.TRANSCRIPT [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.VER [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.VERIFY [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.witness_loc [definition, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chSoundness [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chTranscript [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chMessage [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chInput [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chRelation [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chChallenge [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chWitness [notation, in SSProve.Crypt.examples.SigmaProtocol]
pack_type:chStatement [notation, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.ɛ_hiding [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.ɛ_soundness [definition, in SSProve.Crypt.examples.SigmaProtocol]
SigmaProtocol.ɛ_SHVZK [definition, in SSProve.Crypt.examples.SigmaProtocol]
Signed [constructor, in SSProve.Crypt.jasmin_wsize]
signedness [inductive, in SSProve.Crypt.jasmin_wsize]
sign_extend0 [lemma, in SSProve.Crypt.jasmin_word]
sign_extend_u [lemma, in SSProve.Crypt.jasmin_word]
sign_extend [definition, in SSProve.Crypt.jasmin_word]
sig_eq [lemma, in SSProve.Mon.Monoid]
sig_rewrite [lemma, in SSProve.Crypt.Prelude]
sig_rewrite_aux [lemma, in SSProve.Crypt.Prelude]
sig_eq [lemma, in SSProve.Mon.SPropBase]
sim [projection, in SSProve.Relational.Category]
SimpleRelationalSpecMonad [section, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
SimpleRelationalSpecMonad.idxid [variable, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
SimpleRelationalSpecMonad.M1 [variable, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
SimpleRelationalSpecMonad.M2 [variable, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
sim_equiv [projection, in SSProve.Relational.Category]
single_key_b [lemma, in SSProve.Crypt.examples.KEMDEM]
single_key_a [lemma, in SSProve.Crypt.examples.KEMDEM]
sinv_empty [projection, in SSProve.Crypt.package.pkg_invariants]
sinv_set [projection, in SSProve.Crypt.package.pkg_invariants]
size_poly_to_nat [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
size_nat_to_poly [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
size_poly_bij [lemma, in SSProve.Crypt.examples.ShamirSecretSharing]
size_tail_poly [lemma, in SSProve.Crypt.examples.PolynomialUtils]
size_lagrange_poly [lemma, in SSProve.Crypt.examples.PolynomialUtils]
size_lagrange_poly_part [lemma, in SSProve.Crypt.examples.PolynomialUtils]
size_lagrange_basis [lemma, in SSProve.Crypt.examples.PolynomialUtils]
size_ziota [lemma, in SSProve.Crypt.jasmin_util]
size_mapi [lemma, in SSProve.Crypt.jasmin_util]
size_mapi_aux [lemma, in SSProve.Crypt.jasmin_util]
size_fmapM2 [lemma, in SSProve.Crypt.jasmin_util]
size_mapM2 [lemma, in SSProve.Crypt.jasmin_util]
size_fold2 [lemma, in SSProve.Crypt.jasmin_util]
size_mapM [lemma, in SSProve.Crypt.jasmin_util]
skip [definition, in SSProve.Relational.GenericRulesSimple]
sk_loc [definition, in SSProve.Crypt.examples.KEMDEM]
SM [definition, in SSProve.Mon.Monoid]
smAlpha' [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
smAlpha'' [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
smBeta'' [definition, in SSProve.Crypt.rhl_semantics.more_categories.TransformingLaxMorph]
smMonEqu1 [lemma, in SSProve.Crypt.rules.RulesStateProb]
smMonEqu2 [lemma, in SSProve.Crypt.rules.RulesStateProb]
smult [definition, in SSProve.Mon.Monoid]
snil [definition, in SSProve.Mon.Monoid]
some_commutativity [lemma, in SSProve.Crypt.rules.RulesStateProb]
SpecificationMonads [library]
spl [definition, in SSProve.Crypt.package.pkg_rhl]
split_vec [definition, in SSProve.Crypt.jasmin_word]
SPropAxioms [module, in SSProve.Mon.SPropBase]
SPropAxioms.sprop_ext [axiom, in SSProve.Mon.SPropBase]
SPropBase [library]
SPropMonadicStructures [library]
SPropMonadicStructuresNotation [module, in SSProve.Mon.SPropMonadicStructures]
_ ≤ _ (SPropMonadicStructures_scope) [notation, in SSProve.Mon.SPropMonadicStructures]
_ ≤[ _ ] _ (SPropMonadicStructures_scope) [notation, in SSProve.Mon.SPropMonadicStructures]
SPropNotations [module, in SSProve.Mon.SPropBase]
_ ∙2 [notation, in SSProve.Mon.SPropBase]
_ ∙1 [notation, in SSProve.Mon.SPropBase]
⦑ _ ⦒ [notation, in SSProve.Mon.SPropBase]
SProp_op_order_preorder [instance, in SSProve.Mon.SPropMonadicStructures]
SProp_op_order [definition, in SSProve.Mon.SPropMonadicStructures]
SProp_order_preorder [instance, in SSProve.Mon.SPropMonadicStructures]
SProp_order [definition, in SSProve.Mon.SPropMonadicStructures]
sputt [constructor, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SP_AR [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SP_OP_sind [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SP_OP_rec [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SP_OP_ind [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SP_OP_rect [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SP_OP [inductive, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SquareUnaryIntState [section, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SquareUnaryIntState.unaryIntState_filled_right [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
SquareUnaryIntState.unaryIntState_filled_left [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
src [definition, in SSProve.Crypt.package.pkg_core_definition]
sSet_carrier [projection, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
St [definition, in SSProve.Mon.MonadExamples]
State [section, in SSProve.Mon.MonadExamples]
StateTransformingLaxMorph [library]
StateTransfThetaDens [library]
state_pass_valid [definition, in SSProve.Crypt.package.pkg_advantage]
state_pass [definition, in SSProve.Crypt.package.pkg_advantage]
state_pass__valid [definition, in SSProve.Crypt.package.pkg_advantage]
state_pass_ [definition, in SSProve.Crypt.package.pkg_advantage]
state_beta' [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
statistical_gap [definition, in SSProve.Crypt.examples.PRF]
statistical_gap [definition, in SSProve.Crypt.examples.PRFMAC]
statistical_gap [definition, in SSProve.Crypt.examples.PRPCCA]
STCont [definition, in SSProve.Mon.SpecificationMonads]
StretchPRG [library]
'word (package_scope) [notation, in SSProve.Crypt.examples.StretchPRG]
pack_type:'word [notation, in SSProve.Crypt.examples.StretchPRG]
StretchPRG_example.n [variable, in SSProve.Crypt.examples.StretchPRG]
StretchPRG_example [section, in SSProve.Crypt.examples.StretchPRG]
StrictList [section, in SSProve.Mon.Monoid]
strictSet [record, in SSProve.Relational.OrderEnrichedRelativeMonadExamples]
strict_list_monoid [definition, in SSProve.Mon.Monoid]
strict_monoid [definition, in SSProve.Mon.Monoid]
strict2laxFunc [definition, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
strict2laxTransf [definition, in SSProve.Crypt.rhl_semantics.more_categories.LaxFunctorsAndTransf]
StrongBind [section, in SSProve.Mon.SPropMonadicStructures]
StrongestPostcondition [module, in SSProve.Mon.SpecificationMonads]
strucIso_rightAdj [lemma, in SSProve.Crypt.rhl_semantics.more_categories.OrderEnrichedRelativeAdjunctions]
StT_vs_squaredMonads.stT_squOf_Frp [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_vs_squaredMonads.squOf_stT_Frp [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_vs_squaredMonads.stT_thetaDex_filled [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_vs_squaredMonads.preInterpretState_filled [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_vs_squaredMonads [section, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
stT_Frp [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
stT_thetaDex [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
stT_thetaDex_adj [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_thetaDex_definition.myJMWprod [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_thetaDex_definition.TingAdj2_0 [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_thetaDex_definition.TingAdj1_0 [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_thetaDex_definition.myThetaDex [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
StT_thetaDex_definition [section, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
stT_thetaDens [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
stT_thetaDens_adj [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
StT_unaryThetaDens.Frp [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
StT_unaryThetaDens.θdens_filled [variable, in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
StT_unaryThetaDens [section, in SSProve.Crypt.rhl_semantics.state_prob.StateTransfThetaDens]
StT_WRelprop [definition, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
StT_rFreeProb_squ [definition, in SSProve.Crypt.rhl_semantics.state_prob.OrderEnrichedRelativeAdjunctionsExamples]
SubDistr [library]
subrelation_iff_flip_arrow [instance, in SSProve.Crypt.jasmin_util]
Subseq [section, in SSProve.Crypt.jasmin_util]
subseqs [definition, in SSProve.Crypt.examples.PolynomialUtils]
subseqs_rec [definition, in SSProve.Crypt.examples.PolynomialUtils]
subseq_all [lemma, in SSProve.Crypt.jasmin_util]
subseq_has [lemma, in SSProve.Crypt.jasmin_util]
subtype [record, in SSProve.Mon.Base]
subtype_eq [lemma, in SSProve.Mon.Base]
subword_make_vec_bits_low [lemma, in SSProve.Crypt.jasmin_word]
subword0 [lemma, in SSProve.Crypt.jasmin_word]
sub_nmn [lemma, in SSProve.Crypt.jasmin_util]
sumbool_of_boolEF [lemma, in SSProve.Crypt.jasmin_util]
sumbool_of_boolET [lemma, in SSProve.Crypt.jasmin_util]
summable_pair_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
summable_eq [lemma, in SSProve.Crypt.package.pkg_rhl]
SumOfTheories [section, in SSProve.Mon.DijkstraMonadExamples]
sumOpSpecs [definition, in SSProve.Mon.DijkstraMonadExamples]
sumP [definition, in SSProve.Mon.DijkstraMonadExamples]
sumr_const [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
sumS [definition, in SSProve.Mon.DijkstraMonadExamples]
sum_prod_bij [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
sum_pred_eq [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
sum_oneq_eq [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
sum_const_seq_finType [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
support_sub_diag_mgs [lemma, in SSProve.Crypt.rules.UniformDistrLemmas]
swap [definition, in SSProve.Relational.Commutativity]
swap_rule_ctx [lemma, in SSProve.Crypt.rules.RulesStateProb]
swap_ruleR' [lemma, in SSProve.Crypt.rules.RulesStateProb]
swap_ruleR [lemma, in SSProve.Crypt.rules.RulesStateProb]
swap_ruleL [lemma, in SSProve.Crypt.rules.RulesStateProb]
swap_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
symmetry_rule [lemma, in SSProve.Crypt.rules.RulesStateProb]
SymmRatchet [library]
'word (package_scope) [notation, in SSProve.Crypt.examples.SymmRatchet]
pack_type:'word [notation, in SSProve.Crypt.examples.SymmRatchet]
SymmRatchet_example.n [variable, in SSProve.Crypt.examples.SymmRatchet]
'seq _ (package_scope) [notation, in SSProve.Crypt.examples.SymmRatchet]
pack_type:'seq _ [notation, in SSProve.Crypt.examples.SymmRatchet]
SymmRatchet_example [section, in SSProve.Crypt.examples.SymmRatchet]
Syncs [record, in SSProve.Crypt.package.pkg_invariants]
Syncs [inductive, in SSProve.Crypt.package.pkg_invariants]
Syncs_conj [lemma, in SSProve.Crypt.package.pkg_invariants]
Syncs_heap_ignore [lemma, in SSProve.Crypt.package.pkg_invariants]
Syncs_eq [lemma, in SSProve.Crypt.package.pkg_invariants]
S_loc [definition, in SSProve.Crypt.examples.MACCCA]
S_AR [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
S_OP_sind [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
S_OP_rec [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
S_OP_ind [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
S_OP_rect [definition, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
S_OP [inductive, in SSProve.Crypt.rhl_semantics.state_prob.StateTransformingLaxMorph]
S_loc [definition, in SSProve.Crypt.examples.PRFMAC]
S_loc [definition, in SSProve.Crypt.examples.PRPCCA]
| 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) |