therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.32.0

Triple writer T iff forall support

OracleComp.ProgramLogic.StdDo.triple_writerT_iff_forall_support

Plain-language statement

Support characterization of Std.Do.Triple on WriterT Ļ‰ (OracleComp spec). A triple ā¦ƒPā¦„ mx ā¦ƒQā¦„ over the writer log holds iff every outcome (a, w) in the support of mx.run satisfies Q.1 a (s ++ w) for every starting log s satisfying P. The starting log s threads through the WP interpretation itself, not through mx: WriterT.run mx alway...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record