OAI/GroupTheory/PeriodicGroups/Machines/StackCompression.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.TwoInputBody.K line 11
  2. def OAI.SourceBurnside.TwoInputBody.codeSlot line 12
  3. def OAI.SourceBurnside.TwoInputBody.requestSlot line 13
  4. def OAI.SourceBurnside.TwoInputBody.source line 14
  5. def OAI.SourceBurnside.TwoInputBody.start line 15
  6. def OAI.SourceBurnside.TwoInputBody.transfer line 16
  7. def OAI.SourceBurnside.TwoInputBody.program line 18
  8. lemma OAI.SourceBurnside.TwoInputBody.start_eq line 20
  9. lemma OAI.SourceBurnside.TwoInputBody.update_ready line 25
  10. lemma OAI.SourceBurnside.TwoInputBody.transfer_run line 37
  11. theorem OAI.SourceBurnside.TwoInputBody.trace line 65
  12. inductive OAI.SourceBurnside.CompactStacks.State line 100
  13. def OAI.SourceBurnside.CompactStacks.pred line 112
  14. def OAI.SourceBurnside.CompactStacks.operation line 113
  15. def OAI.SourceBurnside.CompactStacks.seeking line 118
  16. def OAI.SourceBurnside.CompactStacks.machine line 120
  17. def OAI.SourceBurnside.CompactStacks.block line 141
  18. def OAI.SourceBurnside.CompactStacks.words line 142
  19. lemma OAI.SourceBurnside.CompactStacks.block_length line 143
  20. lemma OAI.SourceBurnside.CompactStacks.block_cons line 145
  21. lemma OAI.SourceBurnside.CompactStacks.block_nil line 146
  22. lemma OAI.SourceBurnside.CompactStacks.words_nil line 147
  23. lemma OAI.SourceBurnside.CompactStacks.words_cons line 148
  24. def OAI.SourceBurnside.CompactStacks.config line 150
  25. lemma OAI.SourceBurnside.CompactStacks.skip_bit line 153
  26. lemma OAI.SourceBurnside.CompactStacks.skip_end line 159
  27. lemma OAI.SourceBurnside.CompactStacks.skip_block line 166
  28. lemma OAI.SourceBurnside.CompactStacks.skip_words line 178
  29. lemma OAI.SourceBurnside.CompactStacks.restore line 193
  30. lemma OAI.SourceBurnside.CompactStacks.at_push line 204
  31. lemma OAI.SourceBurnside.CompactStacks.at_pop_cons line 212
  32. lemma OAI.SourceBurnside.CompactStacks.at_pop_nil line 219
  33. lemma OAI.SourceBurnside.CompactStacks.start_push line 225
  34. lemma OAI.SourceBurnside.CompactStacks.start_pop line 234
  35. lemma OAI.SourceBurnside.CompactStacks.words_append line 243
  36. def OAI.SourceBurnside.CompactStacks.registers line 246
  37. lemma OAI.SourceBurnside.CompactStacks.registers_length line 247
  38. lemma OAI.SourceBurnside.CompactStacks.registers_getElem line 248
  39. lemma OAI.SourceBurnside.CompactStacks.registers_update line 251
  40. lemma OAI.SourceBurnside.CompactStacks.registers_split line 261
  41. lemma OAI.SourceBurnside.CompactStacks.full_push line 267
  42. lemma OAI.SourceBurnside.CompactStacks.full_pop_cons line 279
  43. lemma OAI.SourceBurnside.CompactStacks.full_pop_nil line 292
  44. def OAI.SourceBurnside.CompactStacks.encode line 304
  45. def OAI.SourceBurnside.CompactStacks.ticks line 307
  46. lemma OAI.SourceBurnside.CompactStacks.words_update line 312
  47. lemma OAI.SourceBurnside.CompactStacks.encode_push line 318
  48. lemma OAI.SourceBurnside.CompactStacks.encode_pop line 329
  49. theorem OAI.SourceBurnside.CompactStacks.encode_next line 350
  50. def OAI.SourceBurnside.CompactStacks.clock line 357
  51. theorem OAI.SourceBurnside.CompactStacks.encode_exec line 361
  52. lemma OAI.SourceBurnside.CompactStacks.words_length_le line 369
  53. lemma OAI.SourceBurnside.CompactStacks.words_registers_length_le line 379
  54. lemma OAI.SourceBurnside.CompactStacks.words_take_length_le line 388
  55. lemma OAI.SourceBurnside.CompactStacks.ticks_bound line 394
  56. theorem OAI.SourceBurnside.CompactStacks.clock_bound line 406
  57. abbrev OAI.SourceBurnside.CompactInit.K line 422
  58. def OAI.SourceBurnside.CompactInit.store line 423
  59. def OAI.SourceBurnside.CompactInit.pairs line 424
  60. def OAI.SourceBurnside.CompactInit.packet line 425
  61. lemma OAI.SourceBurnside.CompactInit.push_run line 426
  62. lemma OAI.SourceBurnside.CompactInit.packet_run line 430
  63. lemma OAI.SourceBurnside.CompactInit.packet_length line 444
  64. def OAI.SourceBurnside.CompactInit.program line 446
  65. def OAI.SourceBurnside.CompactInit.layout line 448
  66. lemma OAI.SourceBurnside.CompactInit.program_run line 450
  67. lemma OAI.SourceBurnside.CompactInit.layout_length line 476
  68. lemma OAI.SourceBurnside.CompactInit.program_time_le line 478
  69. lemma OAI.SourceBurnside.CompactInit.words_empty line 481
  70. lemma OAI.SourceBurnside.CompactInit.words_single line 485
  71. lemma OAI.SourceBurnside.CompactInit.layout_eq_words line 506
  72. def OAI.SourceBurnside.FixedArity.renameInstr line 524
  73. def OAI.SourceBurnside.FixedArity.renameConfig line 528
  74. def OAI.SourceBurnside.FixedArity.rename line 529
  75. lemma OAI.SourceBurnside.FixedArity.update_comp line 530
  76. lemma OAI.SourceBurnside.FixedArity.rename_next line 537
  77. lemma OAI.SourceBurnside.FixedArity.rename_exec line 540
  78. def OAI.SourceBurnside.FixedArity.liftInstr line 545
  79. def OAI.SourceBurnside.FixedArity.liftConfig line 549
  80. lemma OAI.SourceBurnside.FixedArity.lift_next line 550
  81. lemma OAI.SourceBurnside.FixedArity.lift_exec line 554
  82. abbrev OAI.SourceBurnside.FixedArity.AnswerState line 560
  83. def OAI.SourceBurnside.FixedArity.answerMachine line 561
  84. lemma OAI.SourceBurnside.FixedArity.answer_trace line 565
  85. lemma OAI.SourceBurnside.FixedArity.output_bit line 571
  86. def OAI.SourceBurnside.CompactProgram.inputStore line 585
  87. def OAI.SourceBurnside.CompactProgram.virtual line 586
  88. def OAI.SourceBurnside.CompactProgram.initial line 587
  89. def OAI.SourceBurnside.CompactProgram.boot line 589
  90. abbrev OAI.SourceBurnside.CompactProgram.State line 590
  91. def OAI.SourceBurnside.CompactProgram.enter line 592
  92. def OAI.SourceBurnside.CompactProgram.machine line 595
  93. def OAI.SourceBurnside.CompactProgram.initialConfig line 599
  94. def OAI.SourceBurnside.CompactProgram.bootTime line 602
  95. lemma OAI.SourceBurnside.CompactProgram.initial_store line 605
  96. lemma OAI.SourceBurnside.CompactProgram.boot_trace line 613
  97. lemma OAI.SourceBurnside.CompactProgram.execution line 627
  98. lemma OAI.SourceBurnside.CompactProgram.initial_length line 634
  99. lemma OAI.SourceBurnside.CompactProgram.time_bound line 638
  100. lemma OAI.SourceBurnside.CompactProgram.answer_execution line 644
  101. lemma OAI.SourceBurnside.CompactProgram.halted line 656