OAI/GroupTheory/PeriodicGroups/Machines/InputEncoding.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.Structured.Device.Formula.exponents_mono line 10
  2. abbrev OAI.SourceBurnside.RawLocalBody.Registers line 28
  3. def OAI.SourceBurnside.RawLocalBody.height line 29
  4. def OAI.SourceBurnside.RawLocalBody.length line 30
  5. def OAI.SourceBurnside.RawLocalBody.sideStart line 31
  6. def OAI.SourceBurnside.RawLocalBody.offset line 32
  7. def OAI.SourceBurnside.RawLocalBody.piece line 34
  8. def OAI.SourceBurnside.RawLocalBody.substitution line 35
  9. def OAI.SourceBurnside.RawLocalBody.body line 37
  10. def OAI.SourceBurnside.RawLocalBody.lengthOK line 41
  11. def OAI.SourceBurnside.RawLocalBody.checkedBody line 43
  12. def OAI.SourceBurnside.RawLocalBody.limit line 46
  13. lemma OAI.SourceBurnside.RawLocalBody.offset_eval_bound line 47
  14. lemma OAI.SourceBurnside.RawLocalBody.pieces_exponents line 54
  15. lemma OAI.SourceBurnside.RawLocalBody.body_exponents line 62
  16. lemma OAI.SourceBurnside.RawLocalBody.lengthOK_exponents line 72
  17. lemma OAI.SourceBurnside.RawLocalBody.checkedBody_exponents line 78
  18. def OAI.SourceBurnside.Structured.Binary.appendMap line 87
  19. lemma OAI.SourceBurnside.Structured.Binary.appendMap_run line 89
  20. lemma OAI.SourceBurnside.Structured.Binary.appendReverse_run line 110
  21. lemma OAI.SourceBurnside.Structured.Binary.appendOnes_run line 116
  22. abbrev OAI.SourceBurnside.QuoteCode.K line 127
  23. def OAI.SourceBurnside.QuoteCode.store line 129
  24. def OAI.SourceBurnside.QuoteCode.copyCode line 130
  25. def OAI.SourceBurnside.QuoteCode.copyBin line 131
  26. def OAI.SourceBurnside.QuoteCode.ones line 132
  27. def OAI.SourceBurnside.QuoteCode.reverseHeader line 133
  28. def OAI.SourceBurnside.QuoteCode.stage line 134
  29. def OAI.SourceBurnside.QuoteCode.program line 135
  30. lemma OAI.SourceBurnside.QuoteCode.copyCode_run line 136
  31. lemma OAI.SourceBurnside.QuoteCode.copyBin_run line 141
  32. lemma OAI.SourceBurnside.QuoteCode.ones_run line 146
  33. lemma OAI.SourceBurnside.QuoteCode.push_run line 151
  34. lemma OAI.SourceBurnside.QuoteCode.reverseHeader_run line 155
  35. lemma OAI.SourceBurnside.QuoteCode.stage_run line 163
  36. theorem OAI.SourceBurnside.QuoteCode.program_run line 169
  37. abbrev OAI.SourceBurnside.TakePrefix.K line 186
  38. def OAI.SourceBurnside.TakePrefix.store line 187
  39. def OAI.SourceBurnside.TakePrefix.step line 189
  40. def OAI.SourceBurnside.TakePrefix.program line 190
  41. lemma OAI.SourceBurnside.TakePrefix.step_run line 191
  42. lemma OAI.SourceBurnside.TakePrefix.program_run line 201
  43. abbrev OAI.SourceBurnside.TwoInputQuote.K line 221
  44. def OAI.SourceBurnside.TwoInputQuote.store line 223
  45. def OAI.SourceBurnside.TwoInputQuote.headerSlots line 225
  46. def OAI.SourceBurnside.TwoInputQuote.unarySlots line 226
  47. def OAI.SourceBurnside.TwoInputQuote.takeSlots line 227
  48. def OAI.SourceBurnside.TwoInputQuote.quoteSlots line 228
  49. lemma OAI.SourceBurnside.TwoInputQuote.headerSlots_injective line 229
  50. lemma OAI.SourceBurnside.TwoInputQuote.unarySlots_injective line 230
  51. lemma OAI.SourceBurnside.TwoInputQuote.takeSlots_injective line 231
  52. lemma OAI.SourceBurnside.TwoInputQuote.quoteSlots_injective line 232
  53. def OAI.SourceBurnside.TwoInputQuote.readHeader line 233
  54. def OAI.SourceBurnside.TwoInputQuote.reverseBin line 234
  55. def OAI.SourceBurnside.TwoInputQuote.makeUnary line 235
  56. def OAI.SourceBurnside.TwoInputQuote.takeCode line 236
  57. def OAI.SourceBurnside.TwoInputQuote.qcopyCode line 237
  58. def OAI.SourceBurnside.TwoInputQuote.qcopyBin line 238
  59. def OAI.SourceBurnside.TwoInputQuote.qones line 239
  60. def OAI.SourceBurnside.TwoInputQuote.qheader line 240
  61. def OAI.SourceBurnside.TwoInputQuote.qstage line 241
  62. def OAI.SourceBurnside.TwoInputQuote.quote line 242
  63. def OAI.SourceBurnside.TwoInputQuote.program line 243
  64. lemma OAI.SourceBurnside.TwoInputQuote.readHeader_run line 244
  65. lemma OAI.SourceBurnside.TwoInputQuote.reverseBin_run line 260
  66. lemma OAI.SourceBurnside.TwoInputQuote.makeUnary_run line 265
  67. lemma OAI.SourceBurnside.TwoInputQuote.takeCode_run line 281
  68. lemma OAI.SourceBurnside.TwoInputQuote.qcopyCode_run line 294
  69. lemma OAI.SourceBurnside.TwoInputQuote.qcopyBin_run line 299
  70. lemma OAI.SourceBurnside.TwoInputQuote.qones_run line 304
  71. lemma OAI.SourceBurnside.TwoInputQuote.qpush_run line 309
  72. lemma OAI.SourceBurnside.TwoInputQuote.qheader_run line 313
  73. lemma OAI.SourceBurnside.TwoInputQuote.qstage_run line 321
  74. lemma OAI.SourceBurnside.TwoInputQuote.quote_run line 326
  75. theorem OAI.SourceBurnside.TwoInputQuote.program_run line 340
  76. def OAI.SourceBurnside.Structured.Binary.copyInflate line 361
  77. lemma OAI.SourceBurnside.Structured.Binary.copyInflate_run line 363
  78. abbrev OAI.SourceBurnside.RawPadSeed.K line 388
  79. def OAI.SourceBurnside.RawPadSeed.store line 389
  80. def OAI.SourceBurnside.RawPadSeed.step line 393
  81. lemma OAI.SourceBurnside.RawPadSeed.step_run line 395
  82. def OAI.SourceBurnside.RawPadSeed.steps line 404
  83. def OAI.SourceBurnside.RawPadSeed.added line 407
  84. def OAI.SourceBurnside.RawPadSeed.time line 410
  85. lemma OAI.SourceBurnside.RawPadSeed.steps_run line 413
  86. def OAI.SourceBurnside.RawPadSeed.program line 422
  87. lemma OAI.SourceBurnside.RawPadSeed.program_run line 424
  88. abbrev OAI.SourceBurnside.CountLength.K line 439
  89. def OAI.SourceBurnside.CountLength.store line 440
  90. def OAI.SourceBurnside.CountLength.work line 442
  91. def OAI.SourceBurnside.CountLength.slots line 444
  92. lemma OAI.SourceBurnside.CountLength.slots_injective line 445
  93. def OAI.SourceBurnside.CountLength.program line 446
  94. def OAI.SourceBurnside.CountLength.countBits line 448
  95. lemma OAI.SourceBurnside.CountLength.program_run line 450
  96. lemma OAI.SourceBurnside.CountLength.countBits_length line 504
  97. lemma OAI.SourceBurnside.CountLength.countBits_value line 507
  98. abbrev OAI.SourceBurnside.PackFamily.K line 516
  99. def OAI.SourceBurnside.PackFamily.store line 518
  100. def OAI.SourceBurnside.PackFamily.slots line 523
  101. lemma OAI.SourceBurnside.PackFamily.slots_injective line 525
  102. def OAI.SourceBurnside.PackFamily.pad line 528
  103. def OAI.SourceBurnside.PackFamily.step line 529
  104. lemma OAI.SourceBurnside.PackFamily.step_run line 530
  105. def OAI.SourceBurnside.PackFamily.program line 546
  106. def OAI.SourceBurnside.PackFamily.time line 549
  107. def OAI.SourceBurnside.PackFamily.outputs line 552
  108. lemma OAI.SourceBurnside.PackFamily.program_run line 554
  109. theorem OAI.SourceBurnside.PackFamily.all_run line 578
  110. lemma OAI.SourceBurnside.PackFamily.time_le line 586