Comp.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Sequencing elementary stack computations.

def OAI.Fifths.SM.peek line 9
def OAI.Fifths.SM.pure line 14
theorem OAI.Fifths.SM.exec_peek line 16
theorem OAI.Fifths.SM.exec_pure line 21
def OAI.Fifths.SM.act line 25
Source documentation
Read, carry out one stack/head transition, and return a label.
```
def act [Finite Y] (f : Reads X J → (K → Option Bool) → Y × StChange J K) :
    SM X J K Y where
…
```
Mentions: OAI.Fifths.Reads, OAI.Fifths.StChange, OAI.Fifths.SM
theorem OAI.Fifths.SM.exec_act line 36
def OAI.Fifths.SM.change line 43
theorem OAI.Fifths.SM.exec_change line 45
def OAI.Fifths.SM.bind line 53
def OAI.Fifths.SM.bindFst line 67
def OAI.Fifths.SM.bindSnd line 68
theorem OAI.Fifths.SM.bind_stepFst line 71
theorem OAI.Fifths.SM.bind_stepSnd line 79
theorem OAI.Fifths.SM.run_bindSnd line 87
theorem OAI.Fifths.SM.run_bind line 94
theorem OAI.Fifths.SM.exec_bind line 104
def OAI.Fifths.SM.seq line 112
theorem OAI.Fifths.SM.exec_seq line 113
def OAI.Fifths.SM.loop line 121

theorem OAI.Fifths.SM.loop_step line 131

Source documentation

"Continue" label splices in a silent start move.

theorem loop_step (i : Inputs X J) (s : M.Cfg) :
    M.loop.step i s =
      match M.step i s with
      | Sum.inl none => Sum.inr (M.start, s.2)
      | Sum.inl (some y) => Sum.inl y
      | Sum.inr w => Sum.inr w := by
…

Mentions: OAI.Fifths.Inputs

theorem OAI.Fifths.SM.run_loop line 143

Source comment

Keep the label general through induction

theorem run_loop {i : Inputs X J} {s t w : M.Cfg} {B y v}
    (next : match v with
      | none => M.loop.Run i B (M.start, t.2) w y
      | some y' => y = y' ∧ t = w)
    (e : M.Run i B s t v) :
    M.loop.Run i B s w y := by
…

Mentions: OAI.Fifths.Inputs

theorem OAI.Fifths.SM.loop_stop line 159
theorem OAI.Fifths.SM.loop_continue line 164