OAI/GroupTheory/PeriodicGroups/Machines/ProgramAssembly.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.RawNumberPrep.K line 10
  2. def OAI.SourceBurnside.RawNumberPrep.store line 12
  3. def OAI.SourceBurnside.RawNumberPrep.raw line 18
  4. def OAI.SourceBurnside.RawNumberPrep.before line 20
  5. def OAI.SourceBurnside.RawNumberPrep.parsed line 21
  6. def OAI.SourceBurnside.RawNumberPrep.headerSlots line 23
  7. def OAI.SourceBurnside.RawNumberPrep.unarySlots line 24
  8. def OAI.SourceBurnside.RawNumberPrep.seedSlots line 25
  9. lemma OAI.SourceBurnside.RawNumberPrep.headerSlots_injective line 30
  10. lemma OAI.SourceBurnside.RawNumberPrep.unarySlots_injective line 31
  11. lemma OAI.SourceBurnside.RawNumberPrep.seedSlots_injective line 32
  12. def OAI.SourceBurnside.RawNumberPrep.readHeader line 41
  13. def OAI.SourceBurnside.RawNumberPrep.makeUnary line 42
  14. lemma OAI.SourceBurnside.RawNumberPrep.header_run line 44
  15. lemma OAI.SourceBurnside.RawNumberPrep.unary_run line 62
  16. def OAI.SourceBurnside.RawNumberPrep.items line 87
  17. def OAI.SourceBurnside.RawNumberPrep.offset line 88
  18. def OAI.SourceBurnside.RawNumberPrep.width line 89
  19. def OAI.SourceBurnside.RawNumberPrep.seed line 91
  20. lemma OAI.SourceBurnside.RawNumberPrep.seed_run line 93
  21. def OAI.SourceBurnside.RawNumberPrep.countSlots line 119
  22. lemma OAI.SourceBurnside.RawNumberPrep.countSlots_injective line 121
  23. def OAI.SourceBurnside.RawNumberPrep.count line 122
  24. lemma OAI.SourceBurnside.RawNumberPrep.count_run line 123
  25. def OAI.SourceBurnside.RawNumberPrep.program line 139
  26. theorem OAI.SourceBurnside.RawNumberPrep.program_run line 142
  27. abbrev OAI.SourceBurnside.RawPreparedInputs.I line 174
  28. def OAI.SourceBurnside.RawPreparedInputs.bound line 175
  29. def OAI.SourceBurnside.RawPreparedInputs.semantic line 177
  30. def OAI.SourceBurnside.RawPreparedInputs.fields line 179
  31. lemma OAI.SourceBurnside.RawPreparedInputs.fields_injective line 180
  32. def OAI.SourceBurnside.RawPreparedInputs.inputs line 181
  33. lemma OAI.SourceBurnside.RawPreparedInputs.agrees_inputs line 184
  34. lemma OAI.SourceBurnside.RawPreparedInputs.bound_limits line 189
  35. lemma OAI.SourceBurnside.RawPreparedInputs.semantic_bounded line 196
  36. lemma OAI.SourceBurnside.RawPreparedInputs.inputs_lengths line 211
  37. lemma OAI.SourceBurnside.RawPreparedInputs.inputs_values line 224
  38. def OAI.SourceBurnside.RawPreparedInputs.packed line 239
  39. lemma OAI.SourceBurnside.RawPreparedInputs.packed_lengths line 241
  40. lemma OAI.SourceBurnside.RawPreparedInputs.packed_values line 244
  41. lemma OAI.SourceBurnside.RawPreparedInputs.body_exponents line 248
  42. lemma OAI.SourceBurnside.Structured.Run.extend_left line 261
  43. abbrev OAI.SourceBurnside.RawAssembler.K line 271
  44. def OAI.SourceBurnside.RawAssembler.store line 272
  45. def OAI.SourceBurnside.RawAssembler.packSlots line 273
  46. lemma OAI.SourceBurnside.RawAssembler.packSlots_injective line 279
  47. def OAI.SourceBurnside.RawAssembler.pack line 280
  48. lemma OAI.SourceBurnside.RawAssembler.pack_run line 281
  49. def OAI.SourceBurnside.RawAssembler.program line 305
  50. lemma OAI.SourceBurnside.RawAssembler.time_bound line 306
  51. theorem OAI.SourceBurnside.RawAssembler.program_run line 326
  52. abbrev OAI.SourceBurnside.RawCompiled.K line 356
  53. def OAI.SourceBurnside.RawCompiled.slots line 357
  54. lemma OAI.SourceBurnside.RawCompiled.slots_injective line 360
  55. def OAI.SourceBurnside.RawCompiled.before line 362
  56. def OAI.SourceBurnside.RawCompiled.prepared line 364
  57. def OAI.SourceBurnside.RawCompiled.program line 369
  58. lemma OAI.SourceBurnside.RawCompiled.body_lift line 371
  59. def OAI.SourceBurnside.RawCompiled.setupBound line 381
  60. lemma OAI.SourceBurnside.RawCompiled.setup_tag_independent line 387
  61. theorem OAI.SourceBurnside.RawCompiled.generic_trace line 391
  62. theorem OAI.SourceBurnside.RawCompiled.program_trace line 421
  63. def OAI.SourceBurnside.RawPolynomial.size line 436
  64. def OAI.SourceBurnside.RawPolynomial.factor line 437
  65. lemma OAI.SourceBurnside.RawPolynomial.size_bounds line 438
  66. lemma OAI.SourceBurnside.RawPolynomial.width_le line 444
  67. lemma OAI.SourceBurnside.RawPolynomial.squash line 456
  68. lemma OAI.SourceBurnside.RawPolynomial.linear_square line 459
  69. lemma OAI.SourceBurnside.RawPolynomial.setup_le line 462
  70. lemma OAI.SourceBurnside.RawPolynomial.body_le line 496
  71. abbrev OAI.SourceBurnside.RawFit.F line 509
  72. def OAI.SourceBurnside.RawFit.height line 510
  73. def OAI.SourceBurnside.RawFit.q line 511
  74. def OAI.SourceBurnside.RawFit.capacity line 512
  75. def OAI.SourceBurnside.RawFit.time line 513
  76. def OAI.SourceBurnside.RawFit.width line 514
  77. def OAI.SourceBurnside.RawFit.nextHeight line 515
  78. def OAI.SourceBurnside.RawFit.payload line 516
  79. def OAI.SourceBurnside.RawFit.binSize line 517
  80. def OAI.SourceBurnside.RawFit.certificate line 518
  81. def OAI.SourceBurnside.RawFit.clauses line 521
  82. def OAI.SourceBurnside.RawFit.inputLength line 525
  83. def OAI.SourceBurnside.RawFit.fits line 529
  84. def OAI.SourceBurnside.RawFit.trivialBody line 537
  85. def OAI.SourceBurnside.RawFit.body line 538
  86. lemma OAI.SourceBurnside.RawFit.binSize_eval line 541
  87. lemma OAI.SourceBurnside.RawFit.fits_exponents line 543
  88. lemma OAI.SourceBurnside.RawFit.trivial_exponents line 571
  89. lemma OAI.SourceBurnside.RawFit.body_exponents line 579
  90. def OAI.SourceBurnside.RawFit.Fits line 587
  91. instance OAI.SourceBurnside.RawFit.(instance at line 595) line 595
  92. lemma OAI.SourceBurnside.RawFit.fits_eval line 596
  93. lemma OAI.SourceBurnside.RawFit.fallback_eval line 601
  94. lemma OAI.SourceBurnside.RawFit.body_eval line 604
  95. lemma OAI.SourceBurnside.Structured.Run.extend_right line 614