Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersCslib.CCS.bisimilarity_congr_par
Plain-language statement
P ~ Q → P | R ~ Q | R
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_is_congruence
Plain-language statement
Bisimilarity is a congruence in CCS.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_par_assoc
Plain-language statement
P | (Q | R) ~ (P | Q) | R
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.Context.complete
Plain-language statement
Any Process can be obtained by filling a Context with an atom. This proves that Context is a complete formalisation of syntactic contexts for CCS.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Computability.Turing.SingleTape.SingleTapeNTM.mYields_mTr
Plain-language statement
Characterisation of executions in terms of multistep transitions.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.PerfectSecrecy.ciphertextIndist_of_perfectlySecret
Plain-language statement
Perfect secrecy implies ciphertext indistinguishability.
Source project: Lean Computer Science Library
Person-level attribution pending.