OAI/GroupTheory/PeriodicGroups/Rules/Transactions.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.FiniteTable.Cell.read_wing line 13
  2. lemma OAI.SourceBurnside.FiniteTable.Cell.read_boundary line 14
  3. lemma OAI.SourceBurnside.FiniteTable.Cell.read_full line 16
  4. lemma OAI.SourceBurnside.FiniteTable.Cell.read_setChecker line 19
  5. lemma OAI.SourceBurnside.FiniteTable.Cell.read_palette line 22
  6. lemma OAI.SourceBurnside.FiniteTable.Cell.read_setColor line 26
  7. def OAI.SourceBurnside.FiniteTable.Cell.LockedReads line 30
  8. lemma OAI.SourceBurnside.FiniteTable.Cell.lockedReads_refl line 33
  9. lemma OAI.SourceBurnside.FiniteTable.Cell.LockedReads.symm line 35
  10. lemma OAI.SourceBurnside.FiniteTable.Unary.lockedReads line 39
  11. lemma OAI.SourceBurnside.FiniteTable.Binary.lockedReads line 43
  12. lemma OAI.SourceBurnside.FiniteTable.replacement_lockedReads line 61
  13. lemma OAI.SourceBurnside.FiniteTable.step_lockedReads line 70
  14. def OAI.SourceBurnside.FiniteTable.Cell.PayloadFormat line 84
  15. structure OAI.SourceBurnside.FiniteTable.Region line 89
  16. def OAI.SourceBurnside.FiniteTable.Region.first line 104
  17. def OAI.SourceBurnside.FiniteTable.Region.last line 105
  18. lemma OAI.SourceBurnside.FiniteTable.Region.first_first line 108
  19. lemma OAI.SourceBurnside.FiniteTable.Region.last_last line 110
  20. def OAI.SourceBurnside.FiniteTable.Region.clauseIndex line 115
  21. def OAI.SourceBurnside.FiniteTable.Region.plan line 118
  22. def OAI.SourceBurnside.FiniteTable.Region.controlPosition line 127
  23. def OAI.SourceBurnside.FiniteTable.Region.controlPhase line 131
  24. def OAI.SourceBurnside.FiniteTable.Region.position line 141
  25. def OAI.SourceBurnside.FiniteTable.Region.phase line 146
  26. def OAI.SourceBurnside.FiniteTable.Region.clause line 151
  27. def OAI.SourceBurnside.FiniteTable.Region.realizeCell line 156
  28. def OAI.SourceBurnside.FiniteTable.Region.realize line 161
  29. lemma OAI.SourceBurnside.FiniteTable.Region.realize_head line 164
  30. lemma OAI.SourceBurnside.FiniteTable.Region.realizeCell_read line 169
  31. lemma OAI.SourceBurnside.FiniteTable.Region.realizeCell_payload line 176
  32. lemma OAI.SourceBurnside.FiniteTable.Region.endpoint_position line 185
  33. lemma OAI.SourceBurnside.FiniteTable.Region.realizeCell_format line 192
  34. lemma OAI.SourceBurnside.FiniteTable.ofFn_take_congr line 249
  35. lemma OAI.SourceBurnside.FiniteTable.ofFn_drop_congr line 259
  36. lemma OAI.SourceBurnside.FiniteTable.ofFn_split_one line 268
  37. lemma OAI.SourceBurnside.FiniteTable.ofFn_split_two line 274
  38. lemma OAI.SourceBurnside.FiniteTable.step_one_ofFn line 283
  39. lemma OAI.SourceBurnside.FiniteTable.step_two_ofFn line 293
  40. def OAI.SourceBurnside.FiniteTable.Region.SideOK line 310
  41. lemma OAI.SourceBurnside.FiniteTable.Region.edge_side line 314
  42. lemma OAI.SourceBurnside.FiniteTable.Region.adjacent_pair line 325
  43. lemma OAI.SourceBurnside.FiniteTable.Region.realizeCell_eq_off_head line 334
  44. lemma OAI.SourceBurnside.FiniteTable.Region.step_unary line 346
  45. lemma OAI.SourceBurnside.FiniteTable.Region.realizeCell_eq_off_adjacent line 363
  46. lemma OAI.SourceBurnside.FiniteTable.Region.step_adjacent line 378
  47. lemma OAI.SourceBurnside.FiniteTable.Region.payload_first line 398
  48. lemma OAI.SourceBurnside.FiniteTable.Region.payload_last line 401
  49. lemma OAI.SourceBurnside.FiniteTable.Region.tour_realize_step line 404
  50. lemma OAI.SourceBurnside.FiniteTable.Region.edge_realize_step line 460
  51. lemma OAI.SourceBurnside.FiniteTable.Region.reach_side line 485
  52. lemma OAI.SourceBurnside.FiniteTable.Region.realize_reach line 493
  53. lemma OAI.SourceBurnside.FiniteTable.Region.realize_semanticZero line 505
  54. theorem OAI.SourceBurnside.FiniteTable.Region.literal_rollback line 536
  55. theorem OAI.SourceBurnside.FiniteTable.Region.literal_success line 549