OAI/GroupTheory/PeriodicGroups/Rules/HeadTour.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.HeadTour.Registers line 12
  2. inductive OAI.SourceBurnside.HeadTour.Control line 14
  3. structure OAI.SourceBurnside.HeadTour.State line 19
  4. structure OAI.SourceBurnside.HeadTour.Payload line 27
  5. def OAI.SourceBurnside.HeadTour.Payload.first line 36
  6. def OAI.SourceBurnside.HeadTour.Payload.last line 37
  7. def OAI.SourceBurnside.HeadTour.Payload.partialSum line 39
  8. def OAI.SourceBurnside.HeadTour.Payload.total line 41
  9. lemma OAI.SourceBurnside.HeadTour.Payload.partialSum_zero line 43
  10. lemma OAI.SourceBurnside.HeadTour.Payload.partialSum_N line 44
  11. lemma OAI.SourceBurnside.HeadTour.Payload.partialSum_succ line 45
  12. lemma OAI.SourceBurnside.HeadTour.Payload.partialSum_last line 59
  13. def OAI.SourceBurnside.HeadTour.Payload.potential line 65
  14. def OAI.SourceBurnside.HeadTour.Payload.passed line 75
  15. def OAI.SourceBurnside.HeadTour.Payload.Good line 79
  16. def OAI.SourceBurnside.HeadTour.Payload.SemanticZero line 82
  17. inductive OAI.SourceBurnside.HeadTour.Payload.Edge line 86
  18. def OAI.SourceBurnside.HeadTour.Payload.Step line 103
  19. abbrev OAI.SourceBurnside.HeadTour.Payload.Reach line 104
  20. lemma OAI.SourceBurnside.HeadTour.Payload.edge_good line 106
  21. lemma OAI.SourceBurnside.HeadTour.Payload.reach_good line 139
  22. lemma OAI.SourceBurnside.HeadTour.Payload.good_not_zero line 146
  23. lemma OAI.SourceBurnside.HeadTour.Payload.good_initial line 154
  24. theorem OAI.SourceBurnside.HeadTour.Payload.acquisition_safe line 156
  25. theorem OAI.SourceBurnside.HeadTour.Payload.finish_sound line 160
  26. def OAI.SourceBurnside.HeadTour.Payload.rank line 165
  27. lemma OAI.SourceBurnside.HeadTour.Payload.predecessor line 175
  28. theorem OAI.SourceBurnside.HeadTour.Payload.rollback line 235
  29. lemma OAI.SourceBurnside.HeadTour.Payload.reach_symm line 252
  30. theorem OAI.SourceBurnside.HeadTour.Payload.finish_iff line 258
  31. lemma OAI.SourceBurnside.HeadTour.Payload.addressed_total line 268
  32. inductive OAI.SourceBurnside.HeadTour.FullControl line 276
  33. structure OAI.SourceBurnside.HeadTour.FullState line 281
  34. def OAI.SourceBurnside.HeadTour.atClause line 287
  35. structure OAI.SourceBurnside.HeadTour.Plan line 290
  36. def OAI.SourceBurnside.HeadTour.Plan.first line 298
  37. def OAI.SourceBurnside.HeadTour.Plan.last line 299
  38. def OAI.SourceBurnside.HeadTour.Plan.Holds line 300
  39. def OAI.SourceBurnside.HeadTour.Plan.Before line 302
  40. def OAI.SourceBurnside.HeadTour.Plan.Good line 304
  41. def OAI.SourceBurnside.HeadTour.Plan.Bad line 308
  42. def OAI.SourceBurnside.HeadTour.Plan.SemanticZero line 312
  43. inductive OAI.SourceBurnside.HeadTour.Plan.Edge line 315
  44. def OAI.SourceBurnside.HeadTour.Plan.Step line 323
  45. abbrev OAI.SourceBurnside.HeadTour.Plan.Reach line 324
  46. lemma OAI.SourceBurnside.HeadTour.Plan.before_next line 326
  47. lemma OAI.SourceBurnside.HeadTour.Plan.before_last line 337
  48. lemma OAI.SourceBurnside.HeadTour.Plan.edge_good line 348
  49. lemma OAI.SourceBurnside.HeadTour.Plan.reach_good line 361
  50. lemma OAI.SourceBurnside.HeadTour.Plan.good_not_bad line 367
  51. lemma OAI.SourceBurnside.HeadTour.Plan.good_initial line 377
  52. theorem OAI.SourceBurnside.HeadTour.Plan.success_sound line 380
  53. theorem OAI.SourceBurnside.HeadTour.Plan.zero_sound line 384
  54. lemma OAI.SourceBurnside.HeadTour.Plan.lift_reach line 392
  55. lemma OAI.SourceBurnside.HeadTour.Plan.rollback_clause line 400
  56. theorem OAI.SourceBurnside.HeadTour.Plan.rollback line 422
  57. lemma OAI.SourceBurnside.HeadTour.Plan.reach_symm line 438
  58. theorem OAI.SourceBurnside.HeadTour.Plan.success_iff line 444
  59. abbrev OAI.SourceBurnside.FiniteTable.Meta line 462
  60. abbrev OAI.SourceBurnside.FiniteTable.Reg line 463
  61. instance OAI.SourceBurnside.FiniteTable.(instance at line 465) line 465
  62. inductive OAI.SourceBurnside.FiniteTable.Phase line 472
  63. instance OAI.SourceBurnside.FiniteTable.(instance at line 477) line 477
  64. structure OAI.SourceBurnside.FiniteTable.Head line 481
  65. structure OAI.SourceBurnside.FiniteTable.Cell line 488
  66. structure OAI.SourceBurnside.FiniteTable.Task line 496
  67. def OAI.SourceBurnside.FiniteTable.Meta.task line 501
  68. inductive OAI.SourceBurnside.FiniteTable.Address line 503
  69. structure OAI.SourceBurnside.FiniteTable.Clause line 508
  70. structure OAI.SourceBurnside.FiniteTable.Schedule line 512
  71. def OAI.SourceBurnside.FiniteTable.defaultMeta line 519
  72. def OAI.SourceBurnside.FiniteTable.defaultHead line 520
  73. def OAI.SourceBurnside.FiniteTable.Cell.pos line 524
  74. def OAI.SourceBurnside.FiniteTable.Cell.marker line 525
  75. def OAI.SourceBurnside.FiniteTable.Cell.metadata line 526
  76. def OAI.SourceBurnside.FiniteTable.Cell.wing line 528
  77. def OAI.SourceBurnside.FiniteTable.Cell.boundary line 531
  78. def OAI.SourceBurnside.FiniteTable.Cell.full line 534
  79. def OAI.SourceBurnside.FiniteTable.Cell.idle line 537
  80. def OAI.SourceBurnside.FiniteTable.Cell.setChecker line 544
  81. def OAI.SourceBurnside.FiniteTable.Cell.setColor line 547
  82. def OAI.SourceBurnside.FiniteTable.Cell.isPalette line 550
  83. def OAI.SourceBurnside.FiniteTable.Cell.isCore line 551
  84. def OAI.SourceBurnside.FiniteTable.Cell.endpoint line 553
  85. def OAI.SourceBurnside.FiniteTable.Cell.Format line 556
  86. def OAI.SourceBurnside.FiniteTable.Cell.read line 571
  87. def OAI.SourceBurnside.FiniteTable.Cell.delta line 579
  88. lemma OAI.SourceBurnside.FiniteTable.Cell.read_stop line 582
  89. lemma OAI.SourceBurnside.FiniteTable.Cell.delta_stop line 586
  90. def OAI.SourceBurnside.FiniteTable.Cell.SameNonColor line 589
  91. def OAI.SourceBurnside.FiniteTable.Cell.HeadFree line 592
  92. def OAI.SourceBurnside.FiniteTable.CheckerPair line 597
  93. def OAI.SourceBurnside.FiniteTable.Pair line 601
  94. inductive OAI.SourceBurnside.FiniteTable.Unary line 603
  95. inductive OAI.SourceBurnside.FiniteTable.Binary line 632
  96. def OAI.SourceBurnside.FiniteTable.Replacement line 663
  97. def OAI.SourceBurnside.FiniteTable.SemanticZero line 669
  98. def OAI.SourceBurnside.FiniteTable.UnaryZero line 676
  99. def OAI.SourceBurnside.FiniteTable.BinaryZero line 680
  100. def OAI.SourceBurnside.FiniteTable.Zero line 684
  101. lemma OAI.SourceBurnside.FiniteTable.replacement_lengths line 688
  102. lemma OAI.SourceBurnside.FiniteTable.zero_lengths line 693
  103. lemma OAI.SourceBurnside.FiniteTable.replacement_symm line 697