OAI/GroupTheory/PeriodicGroups/Machines/TapePrograms.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SourceBurnside.OneTape.Move line 10
  2. instance OAI.SourceBurnside.OneTape.(instance at line 13) line 13
  3. def OAI.SourceBurnside.OneTape.Move.shift line 15
  4. structure OAI.SourceBurnside.OneTape.Command line 17
  5. structure OAI.SourceBurnside.OneTape.Config line 22
  6. structure OAI.SourceBurnside.OneTape.Label line 27
  7. def OAI.SourceBurnside.OneTape.Config.cell line 35
  8. def OAI.SourceBurnside.OneTape.step line 38
  9. def OAI.SourceBurnside.OneTape.localStep line 42
  10. theorem OAI.SourceBurnside.OneTape.local_cell line 56
  11. def OAI.SourceBurnside.OneTape.run line 75
  12. lemma OAI.SourceBurnside.OneTape.step_position_bound line 79
  13. lemma OAI.SourceBurnside.OneTape.run_position_bound line 85
  14. lemma OAI.SourceBurnside.OneTape.run_tape_untouched line 94
  15. lemma OAI.SourceBurnside.OneTape.run_from line 107
  16. lemma OAI.SourceBurnside.OneTape.run_succ_start line 114
  17. inductive OAI.SourceBurnside.StackMachine.Instr line 125
  18. structure OAI.SourceBurnside.StackMachine.Config line 131
  19. def OAI.SourceBurnside.StackMachine.next line 137
  20. def OAI.SourceBurnside.StackMachine.ticks line 143
  21. structure OAI.SourceBurnside.StackMachine.Symbol line 148
  22. inductive OAI.SourceBurnside.StackMachine.State line 153
  23. def OAI.SourceBurnside.StackMachine.compile line 161
  24. def OAI.SourceBurnside.StackMachine.tape line 175
  25. def OAI.SourceBurnside.StackMachine.place line 177
  26. def OAI.SourceBurnside.StackMachine.encode line 179
  27. lemma OAI.SourceBurnside.StackMachine.tape_origin line 183
  28. lemma OAI.SourceBurnside.StackMachine.tape_track_succ line 185
  29. lemma OAI.SourceBurnside.StackMachine.tape_track_zero line 188
  30. lemma OAI.SourceBurnside.StackMachine.step_back_zero line 191
  31. lemma OAI.SourceBurnside.StackMachine.step_back_succ line 195
  32. lemma OAI.SourceBurnside.StackMachine.run_back line 200
  33. lemma OAI.SourceBurnside.StackMachine.tape_push line 208
  34. lemma OAI.SourceBurnside.StackMachine.step_push_scan line 240
  35. lemma OAI.SourceBurnside.StackMachine.step_pop_scan line 247
  36. lemma OAI.SourceBurnside.StackMachine.run_push_scan line 254
  37. lemma OAI.SourceBurnside.StackMachine.run_pop_scan line 264
  38. lemma OAI.SourceBurnside.StackMachine.step_push_write line 274
  39. lemma OAI.SourceBurnside.StackMachine.run_push line 281
  40. lemma OAI.SourceBurnside.StackMachine.tape_pop line 294
  41. lemma OAI.SourceBurnside.StackMachine.step_pop_turn line 327
  42. lemma OAI.SourceBurnside.StackMachine.step_pop_read line 333
  43. lemma OAI.SourceBurnside.StackMachine.step_pop_empty line 344
  44. lemma OAI.SourceBurnside.StackMachine.run_pop line 349
  45. theorem OAI.SourceBurnside.StackMachine.compile_next line 371
  46. def OAI.SourceBurnside.StackMachine.exec line 378
  47. def OAI.SourceBurnside.StackMachine.clock line 381
  48. theorem OAI.SourceBurnside.StackMachine.compile_exec line 385
  49. lemma OAI.SourceBurnside.StackMachine.next_length line 393
  50. lemma OAI.SourceBurnside.StackMachine.exec_length line 406
  51. lemma OAI.SourceBurnside.StackMachine.ticks_bound line 416
  52. theorem OAI.SourceBurnside.StackMachine.clock_bound line 423
  53. lemma OAI.SourceBurnside.StackMachine.halt_step line 434
  54. lemma OAI.SourceBurnside.StackMachine.halt_run line 438
  55. theorem OAI.SourceBurnside.StackMachine.compile_finish line 444