OAI/Combinatorics/VariableWL/CellularCatalog.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.CircuitCatalog.Program.Listing line 10
  2. def OAI.VariableWL.CircuitCatalog.Program.Listing.eval line 33
  3. def OAI.VariableWL.CircuitCatalog.Program.Listing.up line 54
  4. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.eval_up line 75
  5. def OAI.VariableWL.CircuitCatalog.Program.Listing.gates line 90
  6. def OAI.VariableWL.CircuitCatalog.Program.Listing.edgeCode line 91
  7. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineSource line 93
  8. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineTarget line 96
  9. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineDomain line 99
  10. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineMap line 101
  11. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineDimension line 104
  12. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineLeft line 106
  13. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineRight line 113
  14. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineConstant line 118
  15. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineValidReal line 120
  16. def OAI.VariableWL.CircuitCatalog.Program.Listing.affineValidComparison line 123
  17. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.gates_number line 127
  18. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.edgeCode_number line 129
  19. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineSource_number line 131
  20. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineTarget_number line 133
  21. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineDomain_bit line 135
  22. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineMap_number line 137
  23. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineDimension_number line 139
  24. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineLeft_number line 141
  25. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineRight_number line 143
  26. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineConstant_number line 145
  27. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineValidReal_bit line 147
  28. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affineValidComparison_bit line 149
  29. def OAI.VariableWL.CircuitCatalog.Program.Listing.affine line 151
  30. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affine_base_eval line 169
  31. theorem OAI.VariableWL.CircuitCatalog.Program.Listing.affine_eval line 197
  32. theorem OAI.VariableWL.Binary.number_bit line 219
  33. theorem OAI.VariableWL.Circuit.ProductCellular.Data.threshold_bit line 233
  34. theorem OAI.VariableWL.Circuit.ProductCellular.Data.input_bit line 235
  35. theorem OAI.VariableWL.Computation.Stack.PolyRecipe.binaryDigit_total line 240
  36. def OAI.VariableWL.CellularCatalog.triple line 257
  37. def OAI.VariableWL.CellularCatalog.ands line 258
  38. def OAI.VariableWL.CellularCatalog.kind line 259
  39. def OAI.VariableWL.CellularCatalog.edge line 262
  40. def OAI.VariableWL.CellularCatalog.zeroBit line 263
  41. def OAI.VariableWL.CellularCatalog.accepting line 266
  42. def OAI.VariableWL.CellularCatalog.request line 269
  43. structure OAI.VariableWL.CellularCatalog.Data line 271
  44. def OAI.VariableWL.CellularCatalog.Data.leftEnd line 284
  45. def OAI.VariableWL.CellularCatalog.Data.centerEnd line 285
  46. def OAI.VariableWL.CellularCatalog.Data.rightEnd line 286
  47. def OAI.VariableWL.CellularCatalog.Data.kinds line 287
  48. def OAI.VariableWL.CellularCatalog.Data.triples line 288
  49. def OAI.VariableWL.CellularCatalog.Data.tripleCode line 289
  50. def OAI.VariableWL.CellularCatalog.Data.kindCode line 290
  51. def OAI.VariableWL.CellularCatalog.Data.first line 291
  52. def OAI.VariableWL.CellularCatalog.Data.second line 292
  53. def OAI.VariableWL.CellularCatalog.Data.third line 293
  54. def OAI.VariableWL.CellularCatalog.Data.kindTime line 294
  55. def OAI.VariableWL.CellularCatalog.Data.kindPosition line 296
  56. def OAI.VariableWL.CellularCatalog.Data.source line 297
  57. def OAI.VariableWL.CellularCatalog.Data.destination line 300
  58. def OAI.VariableWL.CellularCatalog.Data.destinationForm line 303
  59. def OAI.VariableWL.CellularCatalog.Data.carryDomain line 308
  60. def OAI.VariableWL.CellularCatalog.Data.cyclicDomain line 309
  61. def OAI.VariableWL.CellularCatalog.Data.domain line 310
  62. def OAI.VariableWL.CellularCatalog.Data.map line 315
  63. def OAI.VariableWL.CellularCatalog.Data.initialEnd line 320
  64. def OAI.VariableWL.CellularCatalog.Data.validRequest line 321
  65. def OAI.VariableWL.CellularCatalog.Data.requestGate line 323
  66. def OAI.VariableWL.CellularCatalog.Data.requestTest line 324
  67. def OAI.VariableWL.CellularCatalog.Data.requestPositionDomain line 325
  68. def OAI.VariableWL.CellularCatalog.Data.requestDomain line 329
  69. def OAI.VariableWL.CellularCatalog.Data.catalog line 331
  70. theorem OAI.VariableWL.Descriptor.Presentation.product_bound line 357
  71. theorem OAI.VariableWL.Descriptor.Presentation.product_valid line 358
  72. theorem OAI.VariableWL.Descriptor.Presentation.sum_valid line 359
  73. theorem OAI.VariableWL.Descriptor.Presentation.filter_bound line 360
  74. theorem OAI.VariableWL.Descriptor.Presentation.filter_valid line 361
  75. theorem OAI.VariableWL.Descriptor.Presentation.option_bound line 362
  76. theorem OAI.VariableWL.Descriptor.Presentation.option_valid line 363
  77. theorem OAI.VariableWL.Descriptor.Presentation.fin_bound line 364
  78. theorem OAI.VariableWL.Descriptor.Presentation.fin_valid line 365