OAI/GroupTheory/PeriodicGroups/Rules/WordRewriting.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.FiniteTable.Survives line 12
  2. lemma OAI.SourceBurnside.FiniteTable.Survives.of_reach line 15
  3. lemma OAI.SourceBurnside.FiniteTable.Survives.infix line 20
  4. lemma OAI.SourceBurnside.FiniteTable.Survives.not_zero line 28
  5. lemma OAI.SourceBurnside.FiniteTable.Survives.format line 31
  6. lemma OAI.SourceBurnside.FiniteTable.Survives.pair line 37
  7. lemma OAI.SourceBurnside.FiniteTable.Survives.chain line 42
  8. def OAI.SourceBurnside.FiniteTable.Cell.transactionRank line 56
  9. def OAI.SourceBurnside.FiniteTable.Cell.checkerRank line 59
  10. def OAI.SourceBurnside.FiniteTable.Cell.paletteRank line 62
  11. lemma OAI.SourceBurnside.FiniteTable.Cell.paletteRank_lt line 65
  12. def OAI.SourceBurnside.FiniteTable.Cell.eraseColor line 69
  13. def OAI.SourceBurnside.FiniteTable.Cell.color line 71
  14. lemma OAI.SourceBurnside.FiniteTable.Cell.setColor_setColor line 75
  15. lemma OAI.SourceBurnside.FiniteTable.Cell.setColor_of_palette line 80
  16. lemma OAI.SourceBurnside.FiniteTable.Cell.recoverColor line 84
  17. lemma OAI.SourceBurnside.FiniteTable.Cell.not_first_of_palette line 90
  18. lemma OAI.SourceBurnside.FiniteTable.Cell.not_last_of_palette line 96
  19. lemma OAI.SourceBurnside.FiniteTable.palette_marker_pair line 102
  20. lemma OAI.SourceBurnside.FiniteTable.palette_rank_nondecreasing line 121
  21. lemma OAI.SourceBurnside.FiniteTable.palette_equal_markerRank line 134
  22. lemma OAI.SourceBurnside.FiniteTable.palette_equal_checkerRank line 142
  23. lemma OAI.SourceBurnside.FiniteTable.palette_internal_metadata line 151
  24. lemma OAI.SourceBurnside.FiniteTable.palette_equal_metadata line 167
  25. lemma OAI.SourceBurnside.FiniteTable.palette_equal_rank line 180
  26. lemma OAI.SourceBurnside.FiniteTable.replacement_swap_of_same_fields line 222
  27. lemma OAI.SourceBurnside.FiniteTable.Survives.palette_rank_chain line 234
  28. lemma OAI.SourceBurnside.FiniteTable.Survives.palette_rank_head_le line 242
  29. lemma OAI.SourceBurnside.FiniteTable.Survives.palette_no_collision line 248
  30. def OAI.SourceBurnside.FiniteTable.Cell.paletteSignature line 285
  31. lemma OAI.SourceBurnside.FiniteTable.Cell.paletteRank_setColor line 289
  32. lemma OAI.SourceBurnside.FiniteTable.Cell.paletteRank_eq_of_eraseColor_eq line 292
  33. lemma OAI.SourceBurnside.FiniteTable.Survives.palette_signature_nodup line 297
  34. theorem OAI.SourceBurnside.FiniteTable.palette_fragment_bound line 319
  35. theorem OAI.SourceBurnside.FiniteTable.eligible_adjacent_swap line 325
  36. theorem OAI.SourceBurnside.FiniteTable.eligible_run_distinct line 330
  37. def OAI.SourceBurnside.FiniteTable.Cell.Cut line 353
  38. def OAI.SourceBurnside.FiniteTable.Cell.blockRank line 356
  39. def OAI.SourceBurnside.FiniteTable.Cell.geometryRank line 358
  40. lemma OAI.SourceBurnside.FiniteTable.Cell.cut_of_first line 360
  41. lemma OAI.SourceBurnside.FiniteTable.Cell.blockRank_lt line 366
  42. lemma OAI.SourceBurnside.FiniteTable.Cell.blockRank_lt_ten line 373
  43. lemma OAI.SourceBurnside.FiniteTable.Cell.positionRank_lt line 380
  44. lemma OAI.SourceBurnside.FiniteTable.Cell.geometryRank_lt line 388
  45. lemma OAI.SourceBurnside.FiniteTable.pair_noCut_external_idle line 395
  46. lemma OAI.SourceBurnside.FiniteTable.pair_internal_nonidle line 402
  47. lemma OAI.SourceBurnside.FiniteTable.pair_noCut_blockRank line 409
  48. lemma OAI.SourceBurnside.FiniteTable.pair_noCut_stop_core line 421
  49. lemma OAI.SourceBurnside.FiniteTable.pair_noCut_geometry line 439
  50. lemma OAI.SourceBurnside.FiniteTable.Survives.geometry_rank_chain line 473
  51. lemma OAI.SourceBurnside.FiniteTable.Survives.geometry_rank_head_le line 479
  52. lemma OAI.SourceBurnside.FiniteTable.Survives.palette_of_geometry_collision line 484
  53. abbrev OAI.SourceBurnside.FiniteTable.Cell.GeometrySignature line 507
  54. def OAI.SourceBurnside.FiniteTable.Cell.geometrySignature line 509
  55. def OAI.SourceBurnside.FiniteTable.Cell.GeometrySignature.geometry line 515
  56. lemma OAI.SourceBurnside.FiniteTable.Cell.geometrySignature_geometry line 518
  57. lemma OAI.SourceBurnside.FiniteTable.Cell.geometryRank_eq_of_signature_eq line 523
  58. lemma OAI.SourceBurnside.FiniteTable.Cell.paletteSignature_eq_of_geometrySignature_eq line 527
  59. lemma OAI.SourceBurnside.FiniteTable.Survives.geometry_signature_nodup line 536
  60. lemma OAI.SourceBurnside.FiniteTable.Survives.cut_free_length line 561
  61. theorem OAI.SourceBurnside.FiniteTable.cut_free_fragment_bound line 570
  62. def OAI.SourceBurnside.FiniteTable.canonicalCell line 580
  63. def OAI.SourceBurnside.FiniteTable.canonicalBlock line 590
  64. def OAI.SourceBurnside.FiniteTable.encodeWord line 595
  65. lemma OAI.SourceBurnside.FiniteTable.canonicalCell_pos line 597
  66. lemma OAI.SourceBurnside.FiniteTable.canonicalCell_marker line 600
  67. lemma OAI.SourceBurnside.FiniteTable.canonicalCell_checker line 603
  68. lemma OAI.SourceBurnside.FiniteTable.canonicalBlock_length line 606
  69. lemma OAI.SourceBurnside.FiniteTable.encodeWord_length line 610
  70. lemma OAI.SourceBurnside.FiniteTable.canonicalCell_format line 619
  71. lemma OAI.SourceBurnside.FiniteTable.canonicalBlock_format line 637
  72. lemma OAI.SourceBurnside.FiniteTable.finRange_head line 643
  73. lemma OAI.SourceBurnside.FiniteTable.finRange_last line 648
  74. lemma OAI.SourceBurnside.FiniteTable.canonicalCell_pair line 655
  75. lemma OAI.SourceBurnside.FiniteTable.canonicalBlock_pair_chain line 663
  76. lemma OAI.SourceBurnside.FiniteTable.canonicalBlock_head line 696
  77. lemma OAI.SourceBurnside.FiniteTable.canonicalBlock_last line 700
  78. lemma OAI.SourceBurnside.FiniteTable.encodeWord_pair_chain line 704
  79. lemma OAI.SourceBurnside.FiniteTable.closed_of_pair_chain line 728
  80. lemma OAI.SourceBurnside.FiniteTable.encodeWord_syntax line 758