OAI/GroupTheory/PeriodicGroups/Rules/BoundaryCell.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.FiniteTable.Cell.idle_format line 12
  2. lemma OAI.SourceBurnside.FiniteTable.Cell.boundary_format line 27
  3. def OAI.SourceBurnside.FiniteTable.Region.boundaryCell line 39
  4. def OAI.SourceBurnside.FiniteTable.Region.boundaryWord line 43
  5. def OAI.SourceBurnside.FiniteTable.Region.idleWord line 46
  6. lemma OAI.SourceBurnside.FiniteTable.Region.boundaryCell_format line 48
  7. lemma OAI.SourceBurnside.FiniteTable.Region.boundaryCell_cursor line 64
  8. lemma OAI.SourceBurnside.FiniteTable.Region.acquisition_pair line 68
  9. lemma OAI.SourceBurnside.FiniteTable.Region.release_step line 77
  10. lemma OAI.SourceBurnside.FiniteTable.Region.remove_first line 99
  11. theorem OAI.SourceBurnside.FiniteTable.Region.release line 115
  12. lemma OAI.SourceBurnside.FiniteTable.Region.unfinish line 129
  13. theorem OAI.SourceBurnside.FiniteTable.Region.literal_rollback_release line 152
  14. def OAI.SourceBurnside.FiniteTable.Region.actualState line 162
  15. lemma OAI.SourceBurnside.FiniteTable.Region.actualState_side line 182
  16. lemma OAI.SourceBurnside.FiniteTable.Region.actualState_position line 189
  17. lemma OAI.SourceBurnside.FiniteTable.Region.actualState_phase line 201
  18. lemma OAI.SourceBurnside.FiniteTable.Region.actualState_clause line 206
  19. lemma OAI.SourceBurnside.FiniteTable.Region.actualState_realize line 214
  20. theorem OAI.SourceBurnside.FiniteTable.Region.actual_rollback_release line 251
  21. lemma OAI.SourceBurnside.FiniteTable.Coherent.left_wing line 268
  22. def OAI.SourceBurnside.FiniteTable.Component.headIndex line 291
  23. lemma OAI.SourceBurnside.FiniteTable.Component.offset_headIndex line 298
  24. lemma OAI.SourceBurnside.FiniteTable.Component.before_head line 305
  25. lemma OAI.SourceBurnside.FiniteTable.Component.after_head line 314
  26. theorem OAI.SourceBurnside.FiniteTable.Component.actual_rollback_release line 322
  27. lemma OAI.SourceBurnside.FiniteTable.Cell.setChecker_self line 348
  28. lemma OAI.SourceBurnside.FiniteTable.Cell.setChecker_setChecker line 350
  29. lemma OAI.SourceBurnside.FiniteTable.Cell.setChecker_checker line 353
  30. lemma OAI.SourceBurnside.FiniteTable.Cell.setChecker_pos line 356
  31. lemma OAI.SourceBurnside.FiniteTable.Cell.setChecker_color line 358
  32. lemma OAI.SourceBurnside.FiniteTable.Cell.setChecker_palette line 361
  33. lemma OAI.SourceBurnside.FiniteTable.Cell.setChecker_format line 363
  34. def OAI.SourceBurnside.FiniteTable.checkerIdle line 370
  35. lemma OAI.SourceBurnside.FiniteTable.checkerIdle_append line 372
  36. lemma OAI.SourceBurnside.FiniteTable.checkerIdle_cons line 375
  37. lemma OAI.SourceBurnside.FiniteTable.checkerIdle_eq line 378
  38. lemma OAI.SourceBurnside.FiniteTable.checker_create_step line 385
  39. lemma OAI.SourceBurnside.FiniteTable.checker_advance_step line 398
  40. lemma OAI.SourceBurnside.FiniteTable.checker_rollback_head line 415
  41. def OAI.SourceBurnside.FiniteTable.asChecker line 460
  42. lemma OAI.SourceBurnside.FiniteTable.checker_pattern line 461
  43. theorem OAI.SourceBurnside.FiniteTable.Survives.checker_rollback line 494
  44. lemma OAI.SourceBurnside.FiniteTable.checker_seek_missing line 520
  45. lemma OAI.SourceBurnside.FiniteTable.Survives.idle_palette_all_colors line 545
  46. theorem OAI.SourceBurnside.FiniteTable.Survives.palette_all_colors line 571
  47. lemma OAI.SourceBurnside.FiniteTable.Cell.palette_idle_canonical line 590
  48. lemma OAI.SourceBurnside.FiniteTable.canonical_palette_swap line 610
  49. def OAI.SourceBurnside.FiniteTable.canonicalPalette line 622
  50. lemma OAI.SourceBurnside.FiniteTable.canonicalPalette_perm line 625
  51. theorem OAI.SourceBurnside.FiniteTable.Survives.idle_palette_normalize line 639