OAI/GroupTheory/PeriodicGroups/Rules/Palette.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.SourceBurnside.Palette.Check line 10
  2. structure OAI.SourceBurnside.Palette.Cell line 16
  3. inductive OAI.SourceBurnside.Palette.Pair line 26
  4. def OAI.SourceBurnside.Palette.LastOK line 32
  5. def OAI.SourceBurnside.Palette.Syntax line 37
  6. def OAI.SourceBurnside.Palette.Form line 41
  7. lemma OAI.SourceBurnside.Palette.syntax_tail line 46
  8. lemma OAI.SourceBurnside.Palette.syntax_form line 54
  9. lemma OAI.SourceBurnside.Palette.chain_change_head line 127
  10. lemma OAI.SourceBurnside.Palette.chain_change_last line 133
  11. lemma OAI.SourceBurnside.Palette.chain_replace_one line 144
  12. lemma OAI.SourceBurnside.Palette.chain_replace_two line 150
  13. def OAI.SourceBurnside.Palette.setCheck line 159
  14. lemma OAI.SourceBurnside.Palette.setCheck_check line 161
  15. lemma OAI.SourceBurnside.Palette.setCheck_color line 162
  16. lemma OAI.SourceBurnside.Palette.setCheck_aux line 163
  17. lemma OAI.SourceBurnside.Palette.setCheck_self line 164
  18. lemma OAI.SourceBurnside.Palette.pair_in_head_passed line 166
  19. lemma OAI.SourceBurnside.Palette.pair_out_head_idle line 170
  20. lemma OAI.SourceBurnside.Palette.syntax_create line 174
  21. lemma OAI.SourceBurnside.Palette.syntax_walk line 183
  22. def OAI.SourceBurnside.Palette.Safe line 197
  23. lemma OAI.SourceBurnside.Palette.safe_nil line 200
  24. lemma OAI.SourceBurnside.Palette.safe_append line 201
  25. lemma OAI.SourceBurnside.Palette.safe_cons line 203
  26. lemma OAI.SourceBurnside.Palette.safe_create line 207
  27. lemma OAI.SourceBurnside.Palette.safe_walk line 210
  28. inductive OAI.SourceBurnside.Palette.Edge line 215
  29. def OAI.SourceBurnside.Palette.Step line 229
  30. abbrev OAI.SourceBurnside.Palette.Reach line 231
  31. lemma OAI.SourceBurnside.Palette.forall₂_colors line 233
  32. lemma OAI.SourceBurnside.Palette.forall₂_checks line 240
  33. lemma OAI.SourceBurnside.Palette.syntax_of_checks line 247
  34. lemma OAI.SourceBurnside.Palette.safe_of_forall₂ line 264
  35. lemma OAI.SourceBurnside.Palette.edge_safe line 271
  36. lemma OAI.SourceBurnside.Palette.edge_syntax line 278
  37. lemma OAI.SourceBurnside.Palette.edge_color_perm line 286
  38. def OAI.SourceBurnside.Palette.Zero line 296
  39. lemma OAI.SourceBurnside.Palette.prefix_passed line 301
  40. theorem OAI.SourceBurnside.Palette.not_zero_of_invariants line 328
  41. theorem OAI.SourceBurnside.Palette.reach_invariants line 343
  42. theorem OAI.SourceBurnside.Palette.clean_not_zero line 355
  43. def OAI.SourceBurnside.Palette.idle line 366
  44. lemma OAI.SourceBurnside.Palette.idle_append line 368
  45. lemma OAI.SourceBurnside.Palette.idle_cons line 370
  46. lemma OAI.SourceBurnside.Palette.idle_setCheck line 372
  47. lemma OAI.SourceBurnside.Palette.idle_eq line 375
  48. lemma OAI.SourceBurnside.Palette.rollback_head line 383
  49. theorem OAI.SourceBurnside.Palette.rollback line 411
  50. def OAI.SourceBurnside.Palette.Survives line 427
  51. lemma OAI.SourceBurnside.Palette.seek_missing line 429
  52. theorem OAI.SourceBurnside.Palette.survives_all_colors line 449
  53. lemma OAI.SourceBurnside.Palette.perm_reach line 469
  54. theorem OAI.SourceBurnside.Palette.survives_distinct line 487
  55. theorem OAI.SourceBurnside.Palette.survives_length line 507
  56. theorem OAI.SourceBurnside.Palette.survives_enumeration line 519