OAI/GroupTheory/PeriodicGroups/Rules/TableEncoding.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_idle_metadata line 11
  2. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.palette_link_left line 27
  3. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.palette_link_right line 36
  4. lemma OAI.SourceBurnside.LocalSyntax.Skeleton.closed_palette_color line 45
  5. lemma OAI.SourceBurnside.FiniteTable.unary_transaction_context line 60
  6. lemma OAI.SourceBurnside.FiniteTable.binary_transaction_context line 73
  7. theorem OAI.SourceBurnside.FiniteTable.replacement_transaction_context line 107
  8. lemma OAI.SourceBurnside.Palette.pair_from_idle line 123
  9. lemma OAI.SourceBurnside.Palette.pair_from_head line 127
  10. lemma OAI.SourceBurnside.Palette.pair_to_head line 131
  11. lemma OAI.SourceBurnside.Palette.pair_to_passed line 135
  12. lemma OAI.SourceBurnside.FiniteTable.unary_checker_context line 145
  13. lemma OAI.SourceBurnside.FiniteTable.checker_right_idle_head line 153
  14. lemma OAI.SourceBurnside.FiniteTable.checker_left_head_passed line 158
  15. lemma OAI.SourceBurnside.FiniteTable.checker_color_left line 163
  16. lemma OAI.SourceBurnside.FiniteTable.checker_color_right line 168
  17. lemma OAI.SourceBurnside.FiniteTable.binary_checker_context line 172
  18. theorem OAI.SourceBurnside.FiniteTable.replacement_checker_context line 210
  19. def OAI.SourceBurnside.FiniteTable.Syntax line 221
  20. theorem OAI.SourceBurnside.FiniteTable.replacement_syntax_context line 225
  21. def OAI.SourceBurnside.FiniteTable.Step line 235
  22. abbrev OAI.SourceBurnside.FiniteTable.Reach line 238
  23. theorem OAI.SourceBurnside.FiniteTable.reach_syntax line 240
  24. lemma OAI.SourceBurnside.FiniteTable.step_symm line 254
  25. lemma OAI.SourceBurnside.FiniteTable.step_context line 258
  26. lemma OAI.SourceBurnside.FiniteTable.reach_symm line 264
  27. lemma OAI.SourceBurnside.FiniteTable.reach_context line 269
  28. lemma OAI.SourceBurnside.FiniteTable.step_length line 275
  29. lemma OAI.SourceBurnside.FiniteTable.reach_length line 279
  30. def OAI.SourceBurnside.FiniteTable.repRel line 284
  31. def OAI.SourceBurnside.FiniteTable.reachCon line 287
  32. theorem OAI.SourceBurnside.FiniteTable.reach_iff_conGen line 299
  33. lemma OAI.SourceBurnside.FiniteTable.unary_idle_first line 319
  34. lemma OAI.SourceBurnside.FiniteTable.unary_ne_idle_right line 325
  35. lemma OAI.SourceBurnside.FiniteTable.no_step_interior_idle line 328
  36. theorem OAI.SourceBurnside.FiniteTable.reach_interior_idle_iff line 350
  37. def OAI.SourceBurnside.FiniteTable.idleCore line 360
  38. lemma OAI.SourceBurnside.FiniteTable.idleCore_format line 363
  39. lemma OAI.SourceBurnside.FiniteTable.idleCore_not_zero line 367
  40. def OAI.SourceBurnside.FiniteTable.shortWords line 379
  41. lemma OAI.SourceBurnside.FiniteTable.shortWords_finite line 384
  42. lemma OAI.SourceBurnside.FiniteTable.replacement_mem_short line 387
  43. lemma OAI.SourceBurnside.FiniteTable.replacement_finite line 396
  44. lemma OAI.SourceBurnside.FiniteTable.zero_mem_short line 400
  45. lemma OAI.SourceBurnside.FiniteTable.zero_finite line 406
  46. theorem OAI.SourceBurnside.FiniteTable.idleCore_not_contextual_zero line 410
  47. abbrev OAI.SourceBurnside.FiniteTable.Codec.Raw line 432
  48. lemma OAI.SourceBurnside.FiniteTable.Codec.reserve_lt line 434
  49. def OAI.SourceBurnside.FiniteTable.Codec.intPosition line 436
  50. def OAI.SourceBurnside.FiniteTable.Codec.flagPosition line 442
  51. def OAI.SourceBurnside.FiniteTable.Codec.write line 445
  52. def OAI.SourceBurnside.FiniteTable.Codec.readInt line 452
  53. def OAI.SourceBurnside.FiniteTable.Codec.readFlag line 455
  54. lemma OAI.SourceBurnside.FiniteTable.Codec.write_int line 457
  55. lemma OAI.SourceBurnside.FiniteTable.Codec.readFlag_write line 472
  56. lemma OAI.SourceBurnside.FiniteTable.Codec.readInt_write line 478
  57. def OAI.SourceBurnside.FiniteTable.Codec.positionTag line 495
  58. def OAI.SourceBurnside.FiniteTable.Codec.positionIndex line 497
  59. def OAI.SourceBurnside.FiniteTable.Codec.markerTag line 499
  60. def OAI.SourceBurnside.FiniteTable.Codec.checkerTag line 501
  61. def OAI.SourceBurnside.FiniteTable.Codec.checkerIndex line 503
  62. def OAI.SourceBurnside.FiniteTable.Codec.phaseTag line 505
  63. def OAI.SourceBurnside.FiniteTable.Codec.bit line 509
  64. def OAI.SourceBurnside.FiniteTable.Codec.unbit line 510
  65. lemma OAI.SourceBurnside.FiniteTable.Codec.unbit_bit line 511
  66. lemma OAI.SourceBurnside.FiniteTable.Codec.bit_unbit line 517
  67. def OAI.SourceBurnside.FiniteTable.Codec.integers line 519
  68. def OAI.SourceBurnside.FiniteTable.Codec.flags line 531
  69. def OAI.SourceBurnside.FiniteTable.Codec.encode line 542
  70. def OAI.SourceBurnside.FiniteTable.Codec.getFin line 544
  71. lemma OAI.SourceBurnside.FiniteTable.Codec.getFin_val line 545
  72. def OAI.SourceBurnside.FiniteTable.Codec.getPosition line 547
  73. def OAI.SourceBurnside.FiniteTable.Codec.getMarker line 553
  74. def OAI.SourceBurnside.FiniteTable.Codec.getChecker line 557
  75. def OAI.SourceBurnside.FiniteTable.Codec.getPhase line 563
  76. lemma OAI.SourceBurnside.FiniteTable.Codec.getPosition_encode line 568
  77. lemma OAI.SourceBurnside.FiniteTable.Codec.getMarker_encode line 571
  78. lemma OAI.SourceBurnside.FiniteTable.Codec.getChecker_encode line 572
  79. lemma OAI.SourceBurnside.FiniteTable.Codec.getPhase_encode line 575
  80. def OAI.SourceBurnside.FiniteTable.Codec.parse line 577
  81. def OAI.SourceBurnside.FiniteTable.Codec.decode line 591
  82. lemma OAI.SourceBurnside.FiniteTable.Codec.positionTag_lt line 595
  83. lemma OAI.SourceBurnside.FiniteTable.Codec.positionIndex_lt line 596
  84. lemma OAI.SourceBurnside.FiniteTable.Codec.markerTag_lt line 601
  85. lemma OAI.SourceBurnside.FiniteTable.Codec.checkerTag_lt line 602
  86. lemma OAI.SourceBurnside.FiniteTable.Codec.checkerIndex_lt line 603
  87. lemma OAI.SourceBurnside.FiniteTable.Codec.phaseTag_lt line 608
  88. lemma OAI.SourceBurnside.FiniteTable.Codec.integers_lt line 610
  89. lemma OAI.SourceBurnside.FiniteTable.Codec.readInt_encode line 626
  90. lemma OAI.SourceBurnside.FiniteTable.Codec.readFlag_encode line 636
  91. lemma OAI.SourceBurnside.FiniteTable.Codec.parse_encode line 639
  92. lemma OAI.SourceBurnside.FiniteTable.Codec.decode_encode line 648
  93. lemma OAI.SourceBurnside.FiniteTable.Codec.encode_injective line 651
  94. lemma OAI.SourceBurnside.FiniteTable.Codec.decode_eq_some_iff line 658
  95. lemma OAI.SourceBurnside.FiniteTable.Codec.raw_card line 674
  96. def OAI.SourceBurnside.FiniteTable.Codec.decodeWord line 676
  97. lemma OAI.SourceBurnside.FiniteTable.Codec.decodeWord_encode line 683
  98. lemma OAI.SourceBurnside.FiniteTable.Codec.decodeWord_eq_some_iff line 689
  99. def OAI.SourceBurnside.FiniteTable.Codec.unaryZero line 721
  100. def OAI.SourceBurnside.FiniteTable.Codec.binaryZero line 726
  101. def OAI.SourceBurnside.FiniteTable.Codec.replacement line 731
  102. def OAI.SourceBurnside.FiniteTable.Codec.zero line 737
  103. lemma OAI.SourceBurnside.FiniteTable.Codec.unaryZero_encode line 743
  104. lemma OAI.SourceBurnside.FiniteTable.Codec.binaryZero_encode line 746
  105. lemma OAI.SourceBurnside.FiniteTable.Codec.replacement_encode line 749
  106. lemma OAI.SourceBurnside.FiniteTable.Codec.zero_encode line 753
  107. lemma OAI.SourceBurnside.FiniteTable.Codec.replacement_has_encodings line 763
  108. lemma OAI.SourceBurnside.FiniteTable.Codec.replacement_lengths line 776
  109. lemma OAI.SourceBurnside.FiniteTable.Codec.zero_lengths line 782