Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

U1 · Internal unproven

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

exec::derive: DerivedFacts from the evaluated generation, never from a proposal (I14’s other half; property-tested)

Sites: C

If it is false

These invariants fall: I10, I14, I21, I22.