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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 589 to 594 of 2,569 results.
Cslib.CCS.bisimilarity_congr_choice
Mathematical statement
P ~ Q → P + R ~ Q + R
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_congr_par
Mathematical statement
P ~ Q → P | R ~ Q | R
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_is_congruence
Mathematical statement
Bisimilarity is a congruence in CCS.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.bisimilarity_par_assoc
Mathematical statement
P | (Q | R) ~ (P | Q) | R
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.CCS.Context.complete
Mathematical 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
Mathematical statement
Characterisation of executions in terms of multistep transitions.
Source project: Lean Computer Science Library
Person-level attribution pending.