OAI/GroupTheory/PeriodicGroups/Rules/PrefixRewriting.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.FiniteTable.Cell.left_format line 12
  2. structure OAI.SourceBurnside.FiniteTable.AcquiredPrefix line 21
  3. def OAI.SourceBurnside.FiniteTable.AcquiredPrefix.first line 33
  4. def OAI.SourceBurnside.FiniteTable.AcquiredPrefix.last line 34
  5. lemma OAI.SourceBurnside.FiniteTable.AcquiredPrefix.first_first line 36
  6. def OAI.SourceBurnside.FiniteTable.AcquiredPrefix.boundaryCell line 38
  7. def OAI.SourceBurnside.FiniteTable.AcquiredPrefix.boundaryWord line 42
  8. def OAI.SourceBurnside.FiniteTable.AcquiredPrefix.idleWord line 44
  9. lemma OAI.SourceBurnside.FiniteTable.AcquiredPrefix.boundaryCell_format line 46
  10. lemma OAI.SourceBurnside.FiniteTable.AcquiredPrefix.boundaryCell_cursor line 59
  11. lemma OAI.SourceBurnside.FiniteTable.AcquiredPrefix.acquisition_pair line 63
  12. lemma OAI.SourceBurnside.FiniteTable.AcquiredPrefix.release_step line 72
  13. lemma OAI.SourceBurnside.FiniteTable.AcquiredPrefix.remove_first line 94
  14. theorem OAI.SourceBurnside.FiniteTable.AcquiredPrefix.release line 110
  15. lemma OAI.SourceBurnside.FiniteTable.Cell.wing_self line 127
  16. lemma OAI.SourceBurnside.FiniteTable.Cell.boundary_self line 135
  17. lemma OAI.SourceBurnside.FiniteTable.Cell.idle_marker line 144
  18. lemma OAI.SourceBurnside.FiniteTable.Component.boundary_right line 150
  19. def OAI.SourceBurnside.FiniteTable.Component.partialRegion line 157
  20. lemma OAI.SourceBurnside.FiniteTable.Component.headIndex_prefix_last line 170
  21. theorem OAI.SourceBurnside.FiniteTable.Component.actual_partial_release line 180
  22. def OAI.SourceBurnside.FiniteTable.lockedCount line 223
  23. lemma OAI.SourceBurnside.FiniteTable.lockedCount_eq_zero line 225
  24. lemma OAI.SourceBurnside.FiniteTable.lockedCount_pos line 228
  25. lemma OAI.SourceBurnside.FiniteTable.lockedCount_append line 231
  26. def OAI.SourceBurnside.FiniteTable.Component.word line 236
  27. lemma OAI.SourceBurnside.FiniteTable.Component.word_slice line 239
  28. lemma OAI.SourceBurnside.FiniteTable.Component.word_split line 253
  29. lemma OAI.SourceBurnside.FiniteTable.Component.word_infix line 264
  30. lemma OAI.SourceBurnside.FiniteTable.Component.word_head_mem line 268
  31. lemma OAI.SourceBurnside.FiniteTable.Component.word_locked_pos line 272
  32. theorem OAI.SourceBurnside.FiniteTable.Component.normalize line 277
  33. theorem OAI.SourceBurnside.FiniteTable.Survives.transactions_idle line 299
  34. abbrev OAI.SourceBurnside.FiniteTable.StructuralChain line 333
  35. def OAI.SourceBurnside.FiniteTable.EndsStop line 336
  36. lemma OAI.SourceBurnside.FiniteTable.endsStop_cons_tail line 339
  37. lemma OAI.SourceBurnside.FiniteTable.coreRange_cons line 344
  38. lemma OAI.SourceBurnside.FiniteTable.scan_core line 350
  39. lemma OAI.SourceBurnside.FiniteTable.scan_palette line 384
  40. structure OAI.SourceBurnside.FiniteTable.StructuralBlock line 415
  41. def OAI.SourceBurnside.FiniteTable.StructuralBlock.word line 425
  42. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.cores_length line 427
  43. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.word_nonempty line 431
  44. lemma OAI.SourceBurnside.FiniteTable.endsStop_suffix line 436
  45. lemma OAI.SourceBurnside.FiniteTable.scan_block line 444
  46. def OAI.SourceBurnside.FiniteTable.StartsCore line 454
  47. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.last_stop line 459
  48. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.starts_after line 461
  49. theorem OAI.SourceBurnside.FiniteTable.structural_decompose line 479
  50. lemma OAI.SourceBurnside.FiniteTable.Cell.stop_idle_canonical line 500
  51. lemma OAI.SourceBurnside.FiniteTable.Cell.core_idle_canonical line 518
  52. def OAI.SourceBurnside.FiniteTable.StructuralBlock.coreCell line 548
  53. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.coreCell_mem line 550
  54. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.coreCell_position line 552
  55. def OAI.SourceBurnside.FiniteTable.StructuralBlock.bits line 557
  56. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.cores_canonical line 560
  57. lemma OAI.SourceBurnside.FiniteTable.StructuralBlock.core_ends line 573
  58. theorem OAI.SourceBurnside.FiniteTable.StructuralBlock.normalize_idle line 583
  59. theorem OAI.SourceBurnside.FiniteTable.idle_blocks_normalize line 616