OAI/GroupTheory/PeriodicGroups/Rules/DataWords.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.FiniteTable.Region.dataWord line 12
  2. inductive OAI.SourceBurnside.FiniteTable.CheckedSwap line 16
  3. def OAI.SourceBurnside.FiniteTable.CheckedZero line 21
  4. def OAI.SourceBurnside.FiniteTable.CheckedReach line 25
  5. lemma OAI.SourceBurnside.FiniteTable.Rigid.decoded_step line 28
  6. theorem OAI.SourceBurnside.FiniteTable.Rigid.decoded_reach line 41
  7. lemma OAI.SourceBurnside.FiniteTable.Rigid.encoded_idle line 69
  8. theorem OAI.SourceBurnside.FiniteTable.Rigid.clean_decoded_reach line 72
  9. lemma OAI.SourceBurnside.FiniteTable.Rigid.component_context line 84
  10. theorem OAI.SourceBurnside.FiniteTable.Rigid.semanticZero_checked line 107
  11. def OAI.SourceBurnside.FiniteTable.Cell.CheckerSafe line 127
  12. lemma OAI.SourceBurnside.FiniteTable.Cell.checkerSafe_idle line 129
  13. lemma OAI.SourceBurnside.FiniteTable.unary_checkerSafe line 134
  14. lemma OAI.SourceBurnside.FiniteTable.binary_checkerSafe line 137
  15. lemma OAI.SourceBurnside.FiniteTable.checkerSafe_step line 152
  16. lemma OAI.SourceBurnside.FiniteTable.checkerSafe_reach line 161
  17. lemma OAI.SourceBurnside.FiniteTable.encodeWord_checkerSafe line 167
  18. lemma OAI.SourceBurnside.FiniteTable.Cell.color_eq line 181
  19. def OAI.SourceBurnside.FiniteTable.Rigid.palCell line 186
  20. def OAI.SourceBurnside.FiniteTable.Rigid.colors line 189
  21. lemma OAI.SourceBurnside.FiniteTable.Rigid.position_palette_iff line 192
  22. lemma OAI.SourceBurnside.FiniteTable.Rigid.layout_palette_iff line 197
  23. lemma OAI.SourceBurnside.FiniteTable.Rigid.palCell_injective line 208
  24. lemma OAI.SourceBurnside.FiniteTable.Rigid.palCell_palette line 215
  25. def OAI.SourceBurnside.FiniteTable.Rigid.palOffset line 224
  26. lemma OAI.SourceBurnside.FiniteTable.Rigid.palOffset_cell line 228
  27. lemma OAI.SourceBurnside.FiniteTable.Rigid.adjacent_palettes_block line 239
  28. lemma OAI.SourceBurnside.FiniteTable.Rigid.colors_pos line 247
  29. lemma OAI.SourceBurnside.FiniteTable.Rigid.colors_swap line 253
  30. lemma OAI.SourceBurnside.FiniteTable.Rigid.unary_colors line 297
  31. lemma OAI.SourceBurnside.FiniteTable.Rigid.binary_colors line 308
  32. lemma OAI.SourceBurnside.FiniteTable.Rigid.colors_step line 330
  33. lemma OAI.SourceBurnside.FiniteTable.Rigid.colors_reach line 347
  34. lemma OAI.SourceBurnside.FiniteTable.Rigid.pal_position line 368
  35. lemma OAI.SourceBurnside.FiniteTable.Rigid.encoded_colors line 372
  36. lemma OAI.SourceBurnside.FiniteTable.Rigid.clean_colors line 380
  37. lemma OAI.SourceBurnside.FiniteTable.Rigid.checker_adjacent line 388
  38. def OAI.SourceBurnside.FiniteTable.Rigid.viewCell line 396
  39. def OAI.SourceBurnside.FiniteTable.Rigid.paletteView line 399
  40. lemma OAI.SourceBurnside.FiniteTable.Rigid.paletteView_syntax line 401
  41. lemma OAI.SourceBurnside.FiniteTable.Rigid.palette_equal_colors_absurd line 423
  42. lemma OAI.SourceBurnside.FiniteTable.Rigid.paletteView_safe line 445
  43. lemma OAI.SourceBurnside.FiniteTable.Rigid.paletteView_nonzero line 457
  44. lemma OAI.SourceBurnside.FiniteTable.Rigid.palette_stop_last line 465
  45. lemma OAI.SourceBurnside.FiniteTable.Rigid.no_failed_checker line 483
  46. lemma OAI.SourceBurnside.FiniteTable.Rigid.no_binaryZero line 504
  47. lemma OAI.SourceBurnside.FiniteTable.Rigid.unaryZero_semantic line 513
  48. theorem OAI.SourceBurnside.FiniteTable.Rigid.contextualZero_checked line 521
  49. theorem OAI.SourceBurnside.FiniteTable.Rigid.clean_zero_decodes line 541
  50. theorem OAI.SourceBurnside.FiniteTable.Rigid.clean_survives line 570