OAI/GroupTheory/PeriodicGroups/Machines/UniversalInput.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.UniversalInput.Packet line 13
  2. abbrev OAI.SourceBurnside.UniversalInput.width line 14
  3. lemma OAI.SourceBurnside.UniversalInput.width_pos line 16
  4. def OAI.SourceBurnside.UniversalInput.packetBits line 18
  5. lemma OAI.SourceBurnside.UniversalInput.packetBits_injective line 20
  6. def OAI.SourceBurnside.UniversalInput.packetDecode line 26
  7. lemma OAI.SourceBurnside.UniversalInput.packetDecode_bits line 27
  8. def OAI.SourceBurnside.UniversalInput.packetWord line 30
  9. def OAI.SourceBurnside.UniversalInput.binaryCode line 31
  10. def OAI.SourceBurnside.UniversalInput.header line 34
  11. inductive OAI.SourceBurnside.UniversalInput.State line 36
  12. def OAI.SourceBurnside.UniversalInput.first line 43
  13. def OAI.SourceBurnside.UniversalInput.collectNext line 44
  14. def OAI.SourceBurnside.UniversalInput.machine line 51
  15. def OAI.SourceBurnside.UniversalInput.inputRegs line 70
  16. def OAI.SourceBurnside.UniversalInput.config line 72
  17. lemma OAI.SourceBurnside.UniversalInput.exec_one line 77
  18. lemma OAI.SourceBurnside.UniversalInput.reverse_token line 85
  19. lemma OAI.SourceBurnside.UniversalInput.reverse_empty line 104
  20. lemma OAI.SourceBurnside.UniversalInput.reverse_all line 116
  21. lemma OAI.SourceBurnside.UniversalInput.header_true line 126
  22. lemma OAI.SourceBurnside.UniversalInput.config_pop_dst line 143
  23. lemma OAI.SourceBurnside.UniversalInput.header_false line 163
  24. lemma OAI.SourceBurnside.UniversalInput.skip_pick_zero line 169
  25. lemma OAI.SourceBurnside.UniversalInput.skip_pick_succ line 178
  26. lemma OAI.SourceBurnside.UniversalInput.skip_read line 186
  27. lemma OAI.SourceBurnside.UniversalInput.header_ones line 191
  28. lemma OAI.SourceBurnside.UniversalInput.skip_bits line 201
  29. lemma OAI.SourceBurnside.UniversalInput.header_all line 214
  30. lemma OAI.SourceBurnside.UniversalInput.collect_bit line 223
  31. def OAI.SourceBurnside.UniversalInput.packetState line 229
  32. lemma OAI.SourceBurnside.UniversalInput.collect_complete line 233
  33. lemma OAI.SourceBurnside.UniversalInput.collect_prefix line 245
  34. lemma OAI.SourceBurnside.UniversalInput.parse_packet line 254
  35. lemma OAI.SourceBurnside.UniversalInput.parse_packet_first line 285
  36. lemma OAI.SourceBurnside.UniversalInput.emit_token line 293
  37. lemma OAI.SourceBurnside.UniversalInput.parse_code line 301
  38. def OAI.SourceBurnside.UniversalInput.liftConfig line 321
  39. lemma OAI.SourceBurnside.UniversalInput.lift_next line 326
  40. lemma OAI.SourceBurnside.UniversalInput.lift_exec line 334
  41. lemma OAI.SourceBurnside.UniversalInput.reset_code line 342
  42. def OAI.SourceBurnside.UniversalInput.loadTime line 350
  43. def OAI.SourceBurnside.UniversalInput.rawInput line 352
  44. theorem OAI.SourceBurnside.UniversalInput.load_raw line 355
  45. lemma OAI.SourceBurnside.UniversalInput.packet_length line 367
  46. lemma OAI.SourceBurnside.UniversalInput.binaryCode_length line 370
  47. lemma OAI.SourceBurnside.UniversalInput.rawInput_length line 379
  48. lemma OAI.SourceBurnside.UniversalInput.loadTime_bound line 383
  49. lemma OAI.SourceBurnside.UniversalInput.initial_store_length line 391
  50. theorem OAI.SourceBurnside.UniversalInput.raw_program_halt line 399
  51. inductive OAI.SourceBurnside.Structured.Program line 451
  52. def OAI.SourceBurnside.Structured.Program.Loc line 461
  53. instance OAI.SourceBurnside.Structured.Program.locFintype line 467
  54. def OAI.SourceBurnside.Structured.Program.start line 481
  55. def OAI.SourceBurnside.Structured.Program.mapInstr line 486
  56. lemma OAI.SourceBurnside.Structured.Program.mapInstr_comp line 491
  57. def OAI.SourceBurnside.Structured.Program.done line 495
  58. def OAI.SourceBurnside.Structured.Program.operation line 498
  59. def OAI.SourceBurnside.Structured.Program.machine line 510
  60. abbrev OAI.SourceBurnside.Structured.Store line 517
  61. def OAI.SourceBurnside.Structured.extendStore line 519
  62. inductive OAI.SourceBurnside.Structured.Run line 522
  63. lemma OAI.SourceBurnside.Structured.extendStore_update line 536
  64. lemma OAI.SourceBurnside.Structured.next_map line 543
  65. theorem OAI.SourceBurnside.Structured.compile_run line 552
  66. theorem OAI.SourceBurnside.Structured.run_machine line 639