OAI/GroupTheory/PeriodicGroups/Machines/UniversalStack.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SourceBurnside.UniversalStack.Instruction line 13
  2. inductive OAI.SourceBurnside.UniversalStack.Token line 19
  3. inductive OAI.SourceBurnside.UniversalStack.Stack line 27
  4. inductive OAI.SourceBurnside.UniversalStack.Target line 31
  5. instance OAI.SourceBurnside.UniversalStack.(instance at line 34) line 34
  6. inductive OAI.SourceBurnside.UniversalStack.Mode line 36
  7. inductive OAI.SourceBurnside.UniversalStack.State line 39
  8. def OAI.SourceBurnside.UniversalStack.afterToken line 46
  9. def OAI.SourceBurnside.UniversalStack.interpreter line 61
  10. def OAI.SourceBurnside.UniversalStack.encodeInstruction line 73
  11. def OAI.SourceBurnside.UniversalStack.encodeProgram line 78
  12. def OAI.SourceBurnside.UniversalStack.config line 80
  13. lemma OAI.SourceBurnside.UniversalStack.config_state line 87
  14. lemma OAI.SourceBurnside.UniversalStack.exec_from line 90
  15. lemma OAI.SourceBurnside.UniversalStack.exec_start line 98
  16. lemma OAI.SourceBurnside.UniversalStack.config_ext line 104
  17. lemma OAI.SourceBurnside.UniversalStack.read_token line 110
  18. lemma OAI.SourceBurnside.UniversalStack.save_target line 118
  19. lemma OAI.SourceBurnside.UniversalStack.reset_token line 126
  20. lemma OAI.SourceBurnside.UniversalStack.reset_empty line 134
  21. lemma OAI.SourceBurnside.UniversalStack.reset_all line 141
  22. lemma OAI.SourceBurnside.UniversalStack.pick_zero line 152
  23. lemma OAI.SourceBurnside.UniversalStack.pick_succ line 158
  24. lemma OAI.SourceBurnside.UniversalStack.after_skip line 166
  25. lemma OAI.SourceBurnside.UniversalStack.skip_fragment line 169
  26. def OAI.SourceBurnside.UniversalStack.codePrefix line 181
  27. lemma OAI.SourceBurnside.UniversalStack.encode_end line 187
  28. lemma OAI.SourceBurnside.UniversalStack.codePrefix_no_stop line 190
  29. lemma OAI.SourceBurnside.UniversalStack.skip_instruction line 194
  30. lemma OAI.SourceBurnside.UniversalStack.skip_instructions line 204
  31. lemma OAI.SourceBurnside.UniversalStack.fetch line 225
  32. lemma OAI.SourceBurnside.UniversalStack.after_target_tick line 237
  33. lemma OAI.SourceBurnside.UniversalStack.skip_ticks line 241
  34. lemma OAI.SourceBurnside.UniversalStack.one_target_tick line 252
  35. lemma OAI.SourceBurnside.UniversalStack.read_ticks line 259
  36. lemma OAI.SourceBurnside.UniversalStack.push_register line 269
  37. lemma OAI.SourceBurnside.UniversalStack.pop_empty line 282
  38. lemma OAI.SourceBurnside.UniversalStack.pop_snoc line 295
  39. lemma OAI.SourceBurnside.UniversalStack.stop_target line 309
  40. lemma OAI.SourceBurnside.UniversalStack.sep_during line 314
  41. lemma OAI.SourceBurnside.UniversalStack.sep_after line 318
  42. lemma OAI.SourceBurnside.UniversalStack.sep_beforeOne line 322
  43. lemma OAI.SourceBurnside.UniversalStack.sep_beforeTwo line 326
  44. def OAI.SourceBurnside.UniversalStack.popBody line 331
  45. def OAI.SourceBurnside.UniversalStack.selected line 335
  46. lemma OAI.SourceBurnside.UniversalStack.pop_body line 338
  47. lemma OAI.SourceBurnside.UniversalStack.opcode_push line 369
  48. lemma OAI.SourceBurnside.UniversalStack.opcode_pop_empty line 383
  49. lemma OAI.SourceBurnside.UniversalStack.opcode_pop_snoc line 396
  50. inductive OAI.SourceBurnside.UniversalStack.Transfer line 412
  51. lemma OAI.SourceBurnside.UniversalStack.opcode_transfer line 421
  52. lemma OAI.SourceBurnside.UniversalStack.transfer_jump_le line 443
  53. lemma OAI.SourceBurnside.UniversalStack.instruction_length_pos line 450
  54. lemma OAI.SourceBurnside.UniversalStack.program_length line 453
  55. lemma OAI.SourceBurnside.UniversalStack.program_step line 462
  56. lemma OAI.SourceBurnside.UniversalStack.step_clock_le line 476
  57. inductive OAI.SourceBurnside.UniversalStack.Run line 488
  58. theorem OAI.SourceBurnside.UniversalStack.simulate_run line 495
  59. lemma OAI.SourceBurnside.UniversalStack.opcode_halt line 511
  60. lemma OAI.SourceBurnside.UniversalStack.program_halt line 516
  61. lemma OAI.SourceBurnside.UniversalStack.halt_clock_le line 527
  62. theorem OAI.SourceBurnside.UniversalStack.simulate_halt line 534
  63. lemma OAI.SourceBurnside.UniversalStack.config_length_bound line 548
  64. theorem OAI.SourceBurnside.UniversalStack.one_tape_halt line 558
  65. def OAI.SourceBurnside.UniversalStack.instructionOf line 582
  66. def OAI.SourceBurnside.UniversalStack.programOf line 588
  67. lemma OAI.SourceBurnside.UniversalStack.programOf_split line 592
  68. lemma OAI.SourceBurnside.UniversalStack.programOf_prefix_length line 601
  69. lemma OAI.SourceBurnside.UniversalStack.instructionOf_transfer line 605
  70. lemma OAI.SourceBurnside.UniversalStack.finite_control_run line 627
  71. theorem OAI.SourceBurnside.UniversalStack.universal_finite_control line 647