recognition / VM / VM.State / lCycle

def

`lCycle`

definition

show as: view math explainer →

module: IndisputableMonolith.VM.State
domain: VM
line: 59 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.VM.State on GitHub at line 59.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

depends on

used by

cycleReport IndisputableMonolith.VM.Commit

formal source

  56    { s' with winJ := s.winJ, winJPrev := s.winJPrev }
  57
  58/-- Eight-tick cycle helper derived from the wrapped stepper. -/
  59def lCycle (P : LProgram) (s : LState) : LState :=
  60  Nat.iterate (lStep P) 8 s
  61
  62end IndisputableMonolith.VM

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.