OAI/GroupTheory/PeriodicGroups/Formulas/LocalPredicates.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceBurnside.PhysicalFormula.x line 12
  2. def OAI.SourceBurnside.PhysicalFormula.y line 14
  3. lemma OAI.SourceBurnside.PhysicalFormula.x_exact line 19
  4. lemma OAI.SourceBurnside.PhysicalFormula.y_exact line 27
  5. def OAI.SourceBurnside.PhysicalFormula.localAddress line 35
  6. lemma OAI.SourceBurnside.PhysicalFormula.localAddress_exact line 40
  7. lemma OAI.SourceBurnside.PhysicalFormula.lookup_ofFn_exact line 56
  8. def OAI.SourceBurnside.PhysicalFormula.localClause line 65
  9. lemma OAI.SourceBurnside.PhysicalFormula.localClause_exact line 78
  10. def OAI.SourceBurnside.PhysicalFormula.chooseIndex line 107
  11. def OAI.SourceBurnside.PhysicalFormula.clauseIndex line 109
  12. def OAI.SourceBurnside.PhysicalFormula.indexEval line 123
  13. lemma OAI.SourceBurnside.PhysicalFormula.clauseIndex_exact line 126
  14. def OAI.SourceBurnside.PhysicalFormula.fallback line 139
  15. def OAI.SourceBurnside.PhysicalFormula.initialFamily line 140
  16. lemma OAI.SourceBurnside.PhysicalFormula.initialFamily_exact line 144
  17. def OAI.SourceBurnside.PhysicalFormula.boundaryFamily line 157
  18. lemma OAI.SourceBurnside.PhysicalFormula.boundaryFamily_exact line 161
  19. def OAI.SourceBurnside.PhysicalFormula.finalFamily line 177
  20. lemma OAI.SourceBurnside.PhysicalFormula.finalFamily_exact line 180
  21. def OAI.SourceBurnside.PhysicalFormula.familyClause line 191
  22. lemma OAI.SourceBurnside.PhysicalFormula.familyClause_exact line 198
  23. def OAI.SourceBurnside.PhysicalFormula.clauseAt line 239
  24. lemma OAI.SourceBurnside.PhysicalFormula.clauseAt_exact line 243
  25. def OAI.SourceBurnside.CellFormula.side line 261
  26. def OAI.SourceBurnside.CellFormula.clause line 262
  27. def OAI.SourceBurnside.CellFormula.register line 263
  28. def OAI.SourceBurnside.CellFormula.zeroReg line 264
  29. def OAI.SourceBurnside.CellFormula.unaryMove line 266
  30. lemma OAI.SourceBurnside.CellFormula.side_exact line 286
  31. lemma OAI.SourceBurnside.CellFormula.clause_exact line 289
  32. lemma OAI.SourceBurnside.CellFormula.register_exact line 292
  33. lemma OAI.SourceBurnside.CellFormula.notSide_exact line 298
  34. lemma OAI.SourceBurnside.CellFormula.zeroReg_exact line 303
  35. lemma OAI.SourceBurnside.CellFormula.zeroClause_exact line 305
  36. lemma OAI.SourceBurnside.CellFormula.equals_exact line 307
  37. lemma OAI.SourceBurnside.CellFormula.unaryMove_exact line 313
  38. def OAI.SourceBurnside.CellFormula.addReg line 347
  39. lemma OAI.SourceBurnside.CellFormula.addReg_exact line 350
  40. def OAI.SourceBurnside.CellFormula.acquireMove line 355
  41. def OAI.SourceBurnside.CellFormula.readLeftMove line 359
  42. def OAI.SourceBurnside.CellFormula.readRightMove line 363
  43. def OAI.SourceBurnside.CellFormula.undoLeftMove line 367
  44. def OAI.SourceBurnside.CellFormula.undoRightMove line 371
  45. def OAI.SourceBurnside.CellFormula.checkerCreateMove line 375
  46. def OAI.SourceBurnside.CellFormula.checkerAdvanceMove line 378
  47. def OAI.SourceBurnside.CellFormula.swapMove line 381
  48. def OAI.SourceBurnside.CellFormula.binaryMove line 384
  49. lemma OAI.SourceBurnside.CellFormula.acquireMove_exact line 394
  50. lemma OAI.SourceBurnside.CellFormula.readLeftMove_exact line 401
  51. lemma OAI.SourceBurnside.CellFormula.readRightMove_exact line 410
  52. lemma OAI.SourceBurnside.CellFormula.undoLeftMove_exact line 417
  53. lemma OAI.SourceBurnside.CellFormula.undoRightMove_exact line 424
  54. lemma OAI.SourceBurnside.CellFormula.checkerCreateMove_exact line 433
  55. lemma OAI.SourceBurnside.CellFormula.checkerAdvanceMove_exact line 442
  56. lemma OAI.SourceBurnside.CellFormula.swapMove_exact line 456
  57. lemma OAI.SourceBurnside.CellFormula.binaryMove_exact line 465
  58. structure OAI.SourceBurnside.PredicateFormula.Table line 484
  59. def OAI.SourceBurnside.PredicateFormula.Table.Represents line 487
  60. def OAI.SourceBurnside.PredicateFormula.Table.truth line 492
  61. def OAI.SourceBurnside.PredicateFormula.Table.delta line 494
  62. lemma OAI.SourceBurnside.PredicateFormula.Table.truth_exact line 496
  63. lemma OAI.SourceBurnside.PredicateFormula.Table.delta_exact line 500
  64. def OAI.SourceBurnside.PredicateFormula.unaryRep line 506
  65. def OAI.SourceBurnside.PredicateFormula.binaryRep line 509
  66. lemma OAI.SourceBurnside.PredicateFormula.unaryRep_exact line 513
  67. lemma OAI.SourceBurnside.PredicateFormula.binaryRep_exact line 524
  68. def OAI.SourceBurnside.PredicateFormula.clauseCount line 543
  69. lemma OAI.SourceBurnside.PredicateFormula.clauseCount_exact line 547
  70. def OAI.SourceBurnside.PredicateFormula.physical line 551
  71. def OAI.SourceBurnside.PredicateFormula.initial line 562
  72. lemma OAI.SourceBurnside.PredicateFormula.physical_exact line 568
  73. def OAI.SourceBurnside.Structured.Device.Formula.bind line 599
  74. lemma OAI.SourceBurnside.Structured.Device.Formula.bind_eval line 612
  75. lemma OAI.SourceBurnside.PredicateFormula.branch_value line 622
  76. def OAI.SourceBurnside.PredicateFormula.valid line 624
  77. lemma OAI.SourceBurnside.PredicateFormula.valid_value line 626
  78. lemma OAI.SourceBurnside.PredicateFormula.rawRepresents line 639
  79. def OAI.SourceBurnside.PredicateFormula.rawUnaryZero line 645
  80. def OAI.SourceBurnside.PredicateFormula.rawBinaryZero line 648
  81. def OAI.SourceBurnside.PredicateFormula.rawUnaryRep line 650
  82. def OAI.SourceBurnside.PredicateFormula.rawBinaryRep line 652
  83. lemma OAI.SourceBurnside.PredicateFormula.rawUnaryZero_exact line 656
  84. lemma OAI.SourceBurnside.PredicateFormula.rawBinaryZero_exact line 667
  85. lemma OAI.SourceBurnside.PredicateFormula.rawUnaryRep_exact line 679