OAI/GroupTheory/PeriodicGroups/Machines/Compilation.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.LocalBody.Registers line 11
  2. def OAI.SourceBurnside.LocalBody.code line 12
  3. def OAI.SourceBurnside.LocalBody.codeLength line 13
  4. def OAI.SourceBurnside.LocalBody.height line 14
  5. def OAI.SourceBurnside.LocalBody.arity line 15
  6. def OAI.SourceBurnside.LocalBody.zeroTask line 16
  7. def OAI.SourceBurnside.LocalBody.word line 17
  8. def OAI.SourceBurnside.LocalBody.time line 19
  9. def OAI.SourceBurnside.LocalBody.width line 20
  10. def OAI.SourceBurnside.LocalBody.origin line 21
  11. def OAI.SourceBurnside.LocalBody.size line 22
  12. def OAI.SourceBurnside.LocalBody.bound line 23
  13. def OAI.SourceBurnside.LocalBody.nextHeight line 24
  14. def OAI.SourceBurnside.LocalBody.table line 25
  15. def OAI.SourceBurnside.LocalBody.body line 28
  16. def OAI.SourceBurnside.LocalBody.exponentLimit line 32
  17. lemma OAI.SourceBurnside.LocalBody.limit_height line 33
  18. lemma OAI.SourceBurnside.LocalBody.limit_code line 34
  19. lemma OAI.SourceBurnside.LocalBody.limit_next line 35
  20. lemma OAI.SourceBurnside.LocalBody.body_exponents line 36
  21. def OAI.SourceBurnside.LocalBody.inputs line 60
  22. lemma OAI.SourceBurnside.LocalBody.inputs_bounded line 62
  23. theorem OAI.SourceBurnside.LocalBody.body_trace line 78
  24. abbrev OAI.SourceBurnside.HeaderProgram.K line 106
  25. def OAI.SourceBurnside.HeaderProgram.store line 108
  26. def OAI.SourceBurnside.HeaderProgram.step line 110
  27. def OAI.SourceBurnside.HeaderProgram.scanPrefix line 112
  28. def OAI.SourceBurnside.HeaderProgram.digit line 113
  29. def OAI.SourceBurnside.HeaderProgram.digits line 115
  30. def OAI.SourceBurnside.HeaderProgram.program line 116
  31. lemma OAI.SourceBurnside.HeaderProgram.step_true line 117
  32. lemma OAI.SourceBurnside.HeaderProgram.step_false line 128
  33. lemma OAI.SourceBurnside.HeaderProgram.prefix_run line 136
  34. lemma OAI.SourceBurnside.HeaderProgram.digit_run line 156
  35. lemma OAI.SourceBurnside.HeaderProgram.digits_run line 165
  36. theorem OAI.SourceBurnside.HeaderProgram.header_run line 181
  37. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryValue_eq line 199
  38. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryValue_append line 205
  39. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryValue_prefix line 208
  40. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryValue_suffix line 211
  41. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryValue_slice line 214
  42. lemma OAI.SourceBurnside.InitialFormula.bin_value line 221
  43. abbrev OAI.SourceBurnside.RawHeader.K line 244
  44. def OAI.SourceBurnside.RawHeader.store line 245
  45. def OAI.SourceBurnside.RawHeader.heightSlots line 246
  46. def OAI.SourceBurnside.RawHeader.aritySlots line 247
  47. lemma OAI.SourceBurnside.RawHeader.heightSlots_injective line 248
  48. lemma OAI.SourceBurnside.RawHeader.aritySlots_injective line 249
  49. def OAI.SourceBurnside.RawHeader.readTask line 250
  50. def OAI.SourceBurnside.RawHeader.program line 251
  51. lemma OAI.SourceBurnside.RawHeader.height_run line 253
  52. lemma OAI.SourceBurnside.RawHeader.arity_run line 266
  53. lemma OAI.SourceBurnside.RawHeader.task_run line 279
  54. def OAI.SourceBurnside.RawHeader.request line 289
  55. lemma OAI.SourceBurnside.RawHeader.program_run line 291
  56. lemma OAI.SourceBurnside.RawHeader.parsed_values line 302
  57. abbrev OAI.SourceBurnside.BinaryUnary.K line 317
  58. def OAI.SourceBurnside.BinaryUnary.store line 318
  59. def OAI.SourceBurnside.BinaryUnary.lastBit line 319
  60. def OAI.SourceBurnside.BinaryUnary.step line 320
  61. def OAI.SourceBurnside.BinaryUnary.program line 321
  62. lemma OAI.SourceBurnside.BinaryUnary.step_run line 322
  63. lemma OAI.SourceBurnside.BinaryUnary.feed_ge line 341
  64. lemma OAI.SourceBurnside.BinaryUnary.program_run line 345
  65. theorem OAI.SourceBurnside.BinaryUnary.numeral_run line 364
  66. def OAI.SourceBurnside.Structured.Binary.pushes line 375
  67. lemma OAI.SourceBurnside.Structured.Binary.pushes_run line 378
  68. def OAI.SourceBurnside.Structured.Binary.inflate line 392
  69. lemma OAI.SourceBurnside.Structured.Binary.inflate_run line 393
  70. abbrev OAI.SourceBurnside.DropPadding.K line 425
  71. def OAI.SourceBurnside.DropPadding.store line 426
  72. def OAI.SourceBurnside.DropPadding.step line 427
  73. def OAI.SourceBurnside.DropPadding.program line 428
  74. lemma OAI.SourceBurnside.DropPadding.program_run line 429
  75. abbrev OAI.SourceBurnside.PadRegister.K line 452
  76. def OAI.SourceBurnside.PadRegister.store line 453
  77. def OAI.SourceBurnside.PadRegister.dropSlots line 455
  78. lemma OAI.SourceBurnside.PadRegister.dropSlots_injective line 456
  79. def OAI.SourceBurnside.PadRegister.program line 457
  80. lemma OAI.SourceBurnside.PadRegister.program_run line 459
  81. lemma OAI.SourceBurnside.PadRegister.result_length line 497
  82. lemma OAI.SourceBurnside.PadRegister.result_value line 499
  83. def OAI.SourceBurnside.WrappedInput.plain line 509
  84. def OAI.SourceBurnside.WrappedInput.specialize line 510
  85. inductive OAI.SourceBurnside.WrappedInput.State line 512
  86. def OAI.SourceBurnside.WrappedInput.machine line 517
  87. def OAI.SourceBurnside.WrappedInput.config line 535
  88. lemma OAI.SourceBurnside.WrappedInput.exec_one line 539
  89. lemma OAI.SourceBurnside.WrappedInput.reverse_token line 543
  90. lemma OAI.SourceBurnside.WrappedInput.reverse_empty line 562
  91. lemma OAI.SourceBurnside.WrappedInput.reverse_all line 574
  92. lemma OAI.SourceBurnside.WrappedInput.header_true line 584
  93. lemma OAI.SourceBurnside.WrappedInput.config_pop_dst line 601
  94. lemma OAI.SourceBurnside.WrappedInput.header_false line 621
  95. lemma OAI.SourceBurnside.WrappedInput.skip_pick_zero line 627
  96. lemma OAI.SourceBurnside.WrappedInput.skip_pick_succ line 636
  97. lemma OAI.SourceBurnside.WrappedInput.skip_read line 644
  98. lemma OAI.SourceBurnside.WrappedInput.header_ones line 649
  99. lemma OAI.SourceBurnside.WrappedInput.skip_bits line 659
  100. lemma OAI.SourceBurnside.WrappedInput.header_all line 672
  101. lemma OAI.SourceBurnside.WrappedInput.marker_true line 681
  102. lemma OAI.SourceBurnside.WrappedInput.marker_false line 685
  103. def OAI.SourceBurnside.WrappedInput.liftConfig line 691
  104. lemma OAI.SourceBurnside.WrappedInput.lift_next line 694
  105. lemma OAI.SourceBurnside.WrappedInput.lift_exec line 699
  106. def OAI.SourceBurnside.WrappedInput.envelope line 705
  107. lemma OAI.SourceBurnside.WrappedInput.enc_header line 707
  108. theorem OAI.SourceBurnside.WrappedInput.specialize_trace line 710
  109. lemma OAI.SourceBurnside.WrappedInput.plain_trace line 723
  110. theorem OAI.SourceBurnside.WrappedInput.raw_specialize_trace line 743