OAI/GroupTheory/PeriodicGroups/Formulas/ClauseEncoding.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceBurnside.Addressable.tripleEquiv_symm_values line 10
  2. def OAI.SourceBurnside.Addressable.Layout.family line 19
  3. def OAI.SourceBurnside.Addressable.Layout.coordinates line 25
  4. def OAI.SourceBurnside.Addressable.Layout.directIndex line 31
  5. lemma OAI.SourceBurnside.Addressable.Layout.natural_unpair line 44
  6. lemma OAI.SourceBurnside.Addressable.Layout.clause_index_direct line 54
  7. theorem OAI.SourceBurnside.Addressable.Layout.clause_index_lookup line 103
  8. abbrev OAI.SourceBurnside.AddressFormula.Expr line 113
  9. def OAI.SourceBurnside.AddressFormula.record line 114
  10. def OAI.SourceBurnside.AddressFormula.evaluate line 117
  11. def OAI.SourceBurnside.AddressFormula.data line 119
  12. def OAI.SourceBurnside.AddressFormula.certificate line 120
  13. lemma OAI.SourceBurnside.AddressFormula.data_exact line 122
  14. lemma OAI.SourceBurnside.AddressFormula.certificate_exact line 127
  15. def OAI.SourceBurnside.AddressFormula.readAt line 131
  16. lemma OAI.SourceBurnside.AddressFormula.readAt_exact line 135
  17. structure OAI.SourceBurnside.ClauseFormula.Expr line 155
  18. def OAI.SourceBurnside.ClauseFormula.Represents line 159
  19. def OAI.SourceBurnside.ClauseFormula.matchReg line 163
  20. def OAI.SourceBurnside.ClauseFormula.regs line 165
  21. lemma OAI.SourceBurnside.ClauseFormula.mem_regs line 166
  22. def OAI.SourceBurnside.ClauseFormula.truth line 173
  23. lemma OAI.SourceBurnside.ClauseFormula.bit_injective line 176
  24. lemma OAI.SourceBurnside.ClauseFormula.matchReg_exact line 178
  25. lemma OAI.SourceBurnside.ClauseFormula.truth_exact line 182
  26. lemma OAI.SourceBurnside.ClauseFormula.truth_bool line 187
  27. lemma OAI.SourceBurnside.ClauseFormula.truth_value line 189
  28. def OAI.SourceBurnside.ClauseFormula.delta line 204
  29. lemma OAI.SourceBurnside.ClauseFormula.delta_exact line 206
  30. def OAI.SourceBurnside.ClauseFormula.choose line 211
  31. lemma OAI.SourceBurnside.ClauseFormula.choose_true line 215
  32. lemma OAI.SourceBurnside.ClauseFormula.choose_false line 222
  33. def OAI.SourceBurnside.ClauseFormula.lookup line 229
  34. lemma OAI.SourceBurnside.ClauseFormula.lookup_exact line 233
  35. def OAI.SourceBurnside.ClauseFormula.truthTable line 259
  36. lemma OAI.SourceBurnside.ClauseFormula.truthTable_value line 262
  37. structure OAI.SourceBurnside.ClauseFormula.ReadingExpr line 271
  38. def OAI.SourceBurnside.ClauseFormula.readValue line 275
  39. def OAI.SourceBurnside.ClauseFormula.RepresentsReading line 279
  40. def OAI.SourceBurnside.ClauseFormula.fixedReading line 283
  41. def OAI.SourceBurnside.ClauseFormula.addressReading line 285
  42. lemma OAI.SourceBurnside.ClauseFormula.fixedReading_exact line 287
  43. lemma OAI.SourceBurnside.ClauseFormula.addressReading_exact line 291
  44. def OAI.SourceBurnside.ClauseFormula.make line 294
  45. lemma OAI.SourceBurnside.ClauseFormula.make_exact line 297
  46. def OAI.SourceBurnside.ClauseFormula.unit line 318
  47. lemma OAI.SourceBurnside.ClauseFormula.unit_exact line 320
  48. def OAI.SourceBurnside.ClauseFormula.equalReading line 328
  49. lemma OAI.SourceBurnside.ClauseFormula.equalReading_exact line 331
  50. def OAI.SourceBurnside.ClauseFormula.initialData line 347
  51. lemma OAI.SourceBurnside.ClauseFormula.initialData_exact line 352
  52. def OAI.SourceBurnside.ClauseFormula.wire line 374
  53. lemma OAI.SourceBurnside.ClauseFormula.wire_exact line 378
  54. def OAI.SourceBurnside.ClauseFormula.circuitClause line 384
  55. lemma OAI.SourceBurnside.ClauseFormula.circuitClause_exact line 386
  56. structure OAI.SourceBurnside.InitialFormula.Expr line 396
  57. def OAI.SourceBurnside.InitialFormula.Represents line 401
  58. def OAI.SourceBurnside.InitialFormula.fixed line 406
  59. def OAI.SourceBurnside.InitialFormula.data line 407
  60. def OAI.SourceBurnside.InitialFormula.choose line 408
  61. lemma OAI.SourceBurnside.InitialFormula.fixed_exact line 413
  62. lemma OAI.SourceBurnside.InitialFormula.data_exact line 416
  63. lemma OAI.SourceBurnside.InitialFormula.choose_true line 420
  64. lemma OAI.SourceBurnside.InitialFormula.choose_false line 429
  65. def OAI.SourceBurnside.InitialFormula.clauses line 438
  66. lemma OAI.SourceBurnside.InitialFormula.clauses_exact line 440
  67. def OAI.SourceBurnside.InitialFormula.mapBit line 448
  68. def OAI.SourceBurnside.InitialFormula.symbol line 451
  69. lemma OAI.SourceBurnside.InitialFormula.symbol_exact line 455
  70. structure OAI.SourceBurnside.InitialFormula.Piece line 465
  71. def OAI.SourceBurnside.InitialFormula.Piece.Represents line 468
  72. def OAI.SourceBurnside.InitialFormula.Piece.append line 471
  73. lemma OAI.SourceBurnside.InitialFormula.Piece.append_exact line 475
  74. lemma OAI.SourceBurnside.InitialFormula.bitAt_value line 491
  75. def OAI.SourceBurnside.InitialFormula.fixedBits line 498
  76. lemma OAI.SourceBurnside.InitialFormula.fixedBits_exact line 502
  77. def OAI.SourceBurnside.InitialFormula.binSize line 511
  78. def OAI.SourceBurnside.InitialFormula.bin line 512
  79. def OAI.SourceBurnside.InitialFormula.enc line 513
  80. lemma OAI.SourceBurnside.InitialFormula.bin_length line 514
  81. lemma OAI.SourceBurnside.InitialFormula.enc_length line 515
  82. lemma OAI.SourceBurnside.InitialFormula.bin_zero line 516
  83. def OAI.SourceBurnside.InitialFormula.number line 518
  84. lemma OAI.SourceBurnside.InitialFormula.number_exact line 522
  85. def OAI.SourceBurnside.InitialFormula.ones line 531
  86. lemma OAI.SourceBurnside.InitialFormula.ones_exact line 535
  87. def OAI.SourceBurnside.InitialFormula.header line 543
  88. lemma OAI.SourceBurnside.InitialFormula.header_exact line 546
  89. def OAI.SourceBurnside.InitialFormula.bits line 557
  90. lemma OAI.SourceBurnside.InitialFormula.bits_exact line 561
  91. def OAI.SourceBurnside.InitialFormula.single line 571
  92. lemma OAI.SourceBurnside.InitialFormula.single_exact line 575
  93. def OAI.SourceBurnside.InitialFormula.inputData line 582
  94. def OAI.SourceBurnside.InitialFormula.dataPiece line 588
  95. lemma OAI.SourceBurnside.InitialFormula.dataPiece_exact line 592
  96. def OAI.SourceBurnside.InitialFormula.sourceInput line 607
  97. def OAI.SourceBurnside.InitialFormula.inputPiece line 612
  98. lemma OAI.SourceBurnside.InitialFormula.inputPiece_exact line 616
  99. def OAI.SourceBurnside.InitialFormula.row line 637
  100. def OAI.SourceBurnside.InitialFormula.cell line 644
  101. lemma OAI.SourceBurnside.InitialFormula.cell_exact line 651