OAI/GroupTheory/PeriodicGroups/Rules/ConnectedWords.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.FiniteTable.Connected line 11
  2. instance OAI.SourceBurnside.FiniteTable.(instance at line 14) line 14
  3. lemma OAI.SourceBurnside.FiniteTable.Connected.refl line 19
  4. lemma OAI.SourceBurnside.FiniteTable.Connected.symm line 21
  5. lemma OAI.SourceBurnside.FiniteTable.Connected.trans line 23
  6. lemma OAI.SourceBurnside.FiniteTable.Connected.subinterval line 28
  7. lemma OAI.SourceBurnside.FiniteTable.Connected.adjacent_iff line 34
  8. lemma OAI.SourceBurnside.FiniteTable.Connected.congr line 40
  9. lemma OAI.SourceBurnside.FiniteTable.Connected.right_barrier line 43
  10. lemma OAI.SourceBurnside.FiniteTable.Connected.edit_unrelated line 46
  11. def OAI.SourceBurnside.FiniteTable.cellCut line 76
  12. instance OAI.SourceBurnside.FiniteTable.(instance at line 77) line 77
  13. abbrev OAI.SourceBurnside.FiniteTable.SameRegion line 81
  14. def OAI.SourceBurnside.FiniteTable.Coherent line 83
  15. lemma OAI.SourceBurnside.FiniteTable.Coherent.internal line 86
  16. lemma OAI.SourceBurnside.FiniteTable.SameRegion.task line 91
  17. lemma OAI.SourceBurnside.FiniteTable.Coherent.left_barrier line 116
  18. lemma OAI.SourceBurnside.FiniteTable.Coherent.idle_component line 128
  19. lemma OAI.SourceBurnside.FiniteTable.Coherent.right_wing line 136
  20. lemma OAI.SourceBurnside.FiniteTable.Coherent.unique_head line 159
  21. lemma OAI.SourceBurnside.FiniteTable.Coherent.region_locked line 174
  22. lemma OAI.SourceBurnside.FiniteTable.Unary.cut_iff line 184
  23. structure OAI.SourceBurnside.FiniteTable.UnaryAt line 190
  24. lemma OAI.SourceBurnside.FiniteTable.UnaryAt.cuts line 197
  25. lemma OAI.SourceBurnside.FiniteTable.UnaryAt.reads line 202
  26. structure OAI.SourceBurnside.FiniteTable.BinaryAt line 209
  27. lemma OAI.SourceBurnside.FiniteTable.BinaryAt.ne line 217
  28. lemma OAI.SourceBurnside.FiniteTable.BinaryAt.reads line 218
  29. lemma OAI.SourceBurnside.FiniteTable.BinaryAt.cuts line 225
  30. lemma OAI.SourceBurnside.FiniteTable.BinaryAt.cuts_off line 233
  31. def OAI.SourceBurnside.FiniteTable.Verification.sum line 245
  32. def OAI.SourceBurnside.FiniteTable.Verification.total line 248
  33. def OAI.SourceBurnside.FiniteTable.Verification.leftSum line 249
  34. lemma OAI.SourceBurnside.FiniteTable.Verification.sum_zero line 252
  35. lemma OAI.SourceBurnside.FiniteTable.Verification.sum_succ line 256
  36. lemma OAI.SourceBurnside.FiniteTable.Verification.sum_congr line 280
  37. lemma OAI.SourceBurnside.FiniteTable.Verification.leftSum_first line 300
  38. lemma OAI.SourceBurnside.FiniteTable.Verification.total_last line 312
  39. def OAI.SourceBurnside.FiniteTable.Verification.potential line 334
  40. def OAI.SourceBurnside.FiniteTable.Verification.passed line 340
  41. def OAI.SourceBurnside.FiniteTable.Verification.holds line 344
  42. def OAI.SourceBurnside.FiniteTable.Verification.Good line 347
  43. def OAI.SourceBurnside.FiniteTable.Verification.AllGood line 354
  44. lemma OAI.SourceBurnside.FiniteTable.Verification.good_initial line 356
  45. lemma OAI.SourceBurnside.FiniteTable.Verification.good_congr line 361
  46. lemma OAI.SourceBurnside.FiniteTable.Verification.good_same_cuts line 370
  47. lemma OAI.SourceBurnside.FiniteTable.Verification.good_semanticZero line 381
  48. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_of_idle line 401
  49. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_single line 405
  50. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_pair line 423
  51. lemma OAI.SourceBurnside.FiniteTable.Verification.total_eq_left_of_last line 446
  52. lemma OAI.SourceBurnside.FiniteTable.Verification.leftSum_eq_zero_of_first line 454
  53. lemma OAI.SourceBurnside.FiniteTable.Verification.unary_full_sums line 458
  54. lemma OAI.SourceBurnside.FiniteTable.Verification.below_next line 472
  55. lemma OAI.SourceBurnside.FiniteTable.Verification.below_success line 484
  56. lemma OAI.SourceBurnside.FiniteTable.Verification.unary_local line 495
  57. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_unary line 556
  58. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_fields line 562
  59. lemma OAI.SourceBurnside.FiniteTable.Verification.moving_sum_congr line 578
  60. lemma OAI.SourceBurnside.FiniteTable.Verification.move_sums line 591
  61. lemma OAI.SourceBurnside.FiniteTable.Verification.good_read_left line 608
  62. lemma OAI.SourceBurnside.FiniteTable.Verification.good_undo_right line 629
  63. lemma OAI.SourceBurnside.FiniteTable.Verification.good_other_move line 645
  64. lemma OAI.SourceBurnside.FiniteTable.Verification.allGood_binary_cuts line 655