OAI/GroupTheory/PeriodicGroups/Formulas/Addressable.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.Addressable.Reading line 13
  2. def OAI.SourceBurnside.Addressable.Reading.eval line 15
  3. lemma OAI.SourceBurnside.Addressable.Reading.eval_map line 21
  4. def OAI.SourceBurnside.Addressable.bit line 25
  5. def OAI.SourceBurnside.Addressable.unbit line 26
  6. lemma OAI.SourceBurnside.Addressable.unbit_bit line 27
  7. lemma OAI.SourceBurnside.Addressable.bit_unbit line 28
  8. structure OAI.SourceBurnside.Addressable.Clause line 35
  9. def OAI.SourceBurnside.Addressable.Clause.Holds line 39
  10. def OAI.SourceBurnside.Addressable.Clause.compile line 42
  11. lemma OAI.SourceBurnside.Addressable.Clause.compile_holds line 50
  12. def OAI.SourceBurnside.Addressable.unit line 63
  13. lemma OAI.SourceBurnside.Addressable.unit_holds line 66
  14. def OAI.SourceBurnside.Addressable.equal line 73
  15. lemma OAI.SourceBurnside.Addressable.equal_holds line 76
  16. abbrev OAI.SourceBurnside.Addressable.DataAddress line 82
  17. def OAI.SourceBurnside.Addressable.dataAddress line 84
  18. inductive OAI.SourceBurnside.Addressable.InputBit line 86
  19. def OAI.SourceBurnside.Addressable.InputBit.eval line 90
  20. def OAI.SourceBurnside.Addressable.initial line 95
  21. lemma OAI.SourceBurnside.Addressable.initial_holds line 103
  22. def OAI.SourceBurnside.Addressable.ofCircuitClause line 115
  23. lemma OAI.SourceBurnside.Addressable.ofCircuitClause_holds line 120
  24. abbrev OAI.SourceBurnside.Addressable.Triple line 130
  25. def OAI.SourceBurnside.Addressable.tripleEquiv line 132
  26. lemma OAI.SourceBurnside.Addressable.tripleEquiv_val line 135
  27. structure OAI.SourceBurnside.Addressable.Layout line 140
  28. abbrev OAI.SourceBurnside.Addressable.Layout.XIndex line 151
  29. abbrev OAI.SourceBurnside.Addressable.Layout.YIndex line 152
  30. abbrev OAI.SourceBurnside.Addressable.Layout.CIndex line 153
  31. def OAI.SourceBurnside.Addressable.Layout.certEquiv line 155
  32. def OAI.SourceBurnside.Addressable.Layout.core line 159
  33. def OAI.SourceBurnside.Addressable.Layout.x line 162
  34. def OAI.SourceBurnside.Addressable.Layout.y line 164
  35. lemma OAI.SourceBurnside.Addressable.Layout.core_x_val line 168
  36. lemma OAI.SourceBurnside.Addressable.Layout.core_y_val line 173
  37. lemma OAI.SourceBurnside.Addressable.Layout.core_injective line 180
  38. def OAI.SourceBurnside.Addressable.Layout.certificate line 183
  39. lemma OAI.SourceBurnside.Addressable.Layout.certificate_core line 188
  40. def OAI.SourceBurnside.Addressable.Layout.payload line 196
  41. lemma OAI.SourceBurnside.Addressable.Layout.payload_data line 201
  42. lemma OAI.SourceBurnside.Addressable.Layout.payload_x line 205
  43. lemma OAI.SourceBurnside.Addressable.Layout.payload_y line 211
  44. abbrev OAI.SourceBurnside.Addressable.Layout.InitialIndex line 217
  45. abbrev OAI.SourceBurnside.Addressable.Layout.BoundaryIndex line 218
  46. abbrev OAI.SourceBurnside.Addressable.Layout.LocalIndex line 219
  47. abbrev OAI.SourceBurnside.Addressable.Layout.ClauseIndex line 220
  48. def OAI.SourceBurnside.Addressable.Layout.clauseEquiv line 224
  49. def OAI.SourceBurnside.Addressable.Layout.currentTime line 232
  50. def OAI.SourceBurnside.Addressable.Layout.nextTime line 233
  51. def OAI.SourceBurnside.Addressable.Layout.interior line 234
  52. def OAI.SourceBurnside.Addressable.Layout.boundary line 235
  53. def OAI.SourceBurnside.Addressable.Layout.localRead line 238
  54. def OAI.SourceBurnside.Addressable.Layout.localClause line 247
  55. def OAI.SourceBurnside.Addressable.Layout.clause line 256
  56. def OAI.SourceBurnside.Addressable.Layout.clauseAt line 266
  57. lemma OAI.SourceBurnside.Addressable.Layout.all_clauses_iff line 272
  58. lemma OAI.SourceBurnside.Addressable.Layout.localClause_gate line 285
  59. def OAI.SourceBurnside.Addressable.Layout.outputIndex line 291
  60. lemma OAI.SourceBurnside.Addressable.Layout.localClause_output line 294
  61. lemma OAI.SourceBurnside.Addressable.Layout.localClause_holds line 304
  62. def OAI.SourceBurnside.Addressable.Layout.FiniteValid line 337
  63. lemma OAI.SourceBurnside.Addressable.Layout.clauseAt_holds_iff line 348
  64. def OAI.SourceBurnside.Addressable.Layout.rows line 377
  65. def OAI.SourceBurnside.Addressable.Layout.gates line 380
  66. lemma OAI.SourceBurnside.Addressable.Layout.rows_at line 384
  67. lemma OAI.SourceBurnside.Addressable.Layout.gates_at line 387
  68. lemma OAI.SourceBurnside.Addressable.Layout.localRead_rows line 391
  69. def OAI.SourceBurnside.Addressable.Layout.inputRow line 406
  70. lemma OAI.SourceBurnside.Addressable.Layout.inputRow_at line 410
  71. lemma OAI.SourceBurnside.Addressable.Layout.rectangle_of_finiteValid line 415
  72. theorem OAI.SourceBurnside.Addressable.Layout.clause_sound line 454
  73. def OAI.SourceBurnside.Addressable.Layout.assemble line 464
  74. lemma OAI.SourceBurnside.Addressable.Layout.inputBit_assemble line 469
  75. lemma OAI.SourceBurnside.Addressable.Layout.inputBit_payload line 474
  76. lemma OAI.SourceBurnside.Addressable.Layout.inputRow_assemble line 480
  77. def OAI.SourceBurnside.Addressable.Layout.rectCertificate line 488
  78. lemma OAI.SourceBurnside.Addressable.Layout.localRead_rect line 494
  79. lemma OAI.SourceBurnside.Addressable.Layout.finiteValid_of_rectangle line 507
  80. theorem OAI.SourceBurnside.Addressable.Layout.certificate_iff line 538
  81. lemma OAI.SourceBurnside.Addressable.Layout.clauseCount_pos line 560
  82. def OAI.SourceBurnside.Addressable.Layout.schedule line 565
  83. lemma OAI.SourceBurnside.Addressable.Layout.schedule_clause line 573
  84. theorem OAI.SourceBurnside.Addressable.Layout.schedule_holds_iff line 580
  85. theorem OAI.SourceBurnside.Addressable.Layout.schedule_certificate_iff line 589
  86. def OAI.SourceBurnside.Addressable.physicalBits line 607
  87. theorem OAI.SourceBurnside.Addressable.physical_clauses_iff line 609
  88. theorem OAI.SourceBurnside.Addressable.physical_accepts line 625
  89. theorem OAI.SourceBurnside.Addressable.reached_success_accepts line 641