OAI/Computability/SpaceSimulation/Stack/Views.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Sliding representation of a tape/configuration for emulating a multi-work-tape program with stacks.

  1. structure OAI.Fifths.WorkSplit line 9
  2. def OAI.Fifths.WorkSplit.init line 17
  3. structure OAI.Fifths.WorkSplit.Good line 20

    Source documentation

    Full-tape agreement (padding by blank), plus inclusion of both lists in the allowed tape window.

    structure Good (z : WorkSplit A) (t : Tape A) (b : A) (l r : ℕ) : Prop where
…

    Mentions: OAI.Fifths.WorkSplit, OAI.Fifths.Tape

  4. theorem OAI.Fifths.WorkSplit.init_good line 27
  5. theorem OAI.Fifths.WorkSplit.good_lengths line 35
  6. def OAI.Fifths.WorkSplit.slide line 41
  7. theorem OAI.Fifths.WorkSplit.good_slide line 47
  8. structure OAI.Fifths.ArgSplit line 125

    Source documentation

    Unlike the work splits, never push either marker.

    structure ArgSplit where
…
  9. def OAI.Fifths.ArgSplit.init line 131
  10. inductive OAI.Fifths.ArgSplit.Good line 133
  11. theorem OAI.Fifths.ArgSplit.good_see line 138
  12. theorem OAI.Fifths.ArgSplit.good_lengths line 147
  13. def OAI.Fifths.ArgSplit.slide line 154
  14. theorem OAI.Fifths.ArgSplit.good_slide line 164