OAI/Combinatorics/VariableWL/CircuitCatalog.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.VariableWL.AffineCatalog.Program.Listing line 11
  2. def OAI.VariableWL.AffineCatalog.Program.Listing.eval line 21
  3. def OAI.VariableWL.AffineCatalog.Program.Listing.up line 30
  4. theorem OAI.VariableWL.AffineCatalog.Program.Listing.eval_up line 39
  5. def OAI.VariableWL.AffineCatalog.Program.Listing.vertexDimension line 48
  6. def OAI.VariableWL.AffineCatalog.Program.Listing.horizontalDimension line 49
  7. def OAI.VariableWL.AffineCatalog.Program.Listing.squareLeftDimension line 50
  8. def OAI.VariableWL.AffineCatalog.Program.Listing.squareRightDimension line 51
  9. def OAI.VariableWL.AffineCatalog.Program.Listing.dimension line 52
  10. def OAI.VariableWL.AffineCatalog.Program.Listing.readDimension line 54
  11. def OAI.VariableWL.AffineCatalog.Program.Listing.linkLeft line 55
  12. def OAI.VariableWL.AffineCatalog.Program.Listing.linkRight line 58
  13. def OAI.VariableWL.AffineCatalog.Program.Listing.linkLeftConstant line 61
  14. def OAI.VariableWL.AffineCatalog.Program.Listing.linkRightConstant line 63
  15. def OAI.VariableWL.AffineCatalog.Program.Listing.constant line 65
  16. def OAI.VariableWL.AffineCatalog.Program.Listing.zeroOrder line 67
  17. def OAI.VariableWL.AffineCatalog.Program.Listing.readOrder line 68
  18. def OAI.VariableWL.AffineCatalog.Program.Listing.legal line 75
  19. theorem OAI.VariableWL.AffineCatalog.Program.Listing.vertexDimension_number line 79
  20. theorem OAI.VariableWL.AffineCatalog.Program.Listing.horizontalDimension_number line 82
  21. theorem OAI.VariableWL.AffineCatalog.Program.Listing.squareLeftDimension_number line 85
  22. theorem OAI.VariableWL.AffineCatalog.Program.Listing.squareRightDimension_number line 88
  23. theorem OAI.VariableWL.AffineCatalog.Program.Listing.dimension_number line 91
  24. theorem OAI.VariableWL.AffineCatalog.Program.Listing.readDimension_number line 94
  25. theorem OAI.VariableWL.AffineCatalog.Program.Listing.linkLeft_number line 97
  26. theorem OAI.VariableWL.AffineCatalog.Program.Listing.linkRight_number line 100
  27. theorem OAI.VariableWL.AffineCatalog.Program.Listing.linkLeftConstant_number line 103
  28. theorem OAI.VariableWL.AffineCatalog.Program.Listing.linkRightConstant_number line 106
  29. theorem OAI.VariableWL.AffineCatalog.Program.Listing.constant_number line 109
  30. theorem OAI.VariableWL.AffineCatalog.Program.Listing.zeroOrder_number line 112
  31. theorem OAI.VariableWL.AffineCatalog.Program.Listing.readOrder_number line 115
  32. theorem OAI.VariableWL.AffineCatalog.Program.Listing.legal_bit line 118
  33. def OAI.VariableWL.AffineCatalog.Program.Listing.core line 121
  34. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_blocks_field line 132
  35. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_blocks_eval line 133
  36. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_validBlock_field line 137
  37. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_validBlock_eval line 138
  38. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_reads_field line 143
  39. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_reads_eval line 144
  40. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_validRead_field line 148
  41. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_validRead_eval line 149
  42. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_has_eval line 154
  43. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_dimension_eval line 160
  44. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_readDimension_eval line 164
  45. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_zeroOrder_eval line 168
  46. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_readOrder_eval line 172
  47. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_legal_eval line 177
  48. theorem OAI.VariableWL.AffineCatalog.Program.Listing.core_eval line 182
  49. theorem OAI.VariableWL.Descriptor.Presentation.sum_bound line 190
  50. def OAI.VariableWL.Descriptor.Presentation.unit line 191
  51. theorem OAI.VariableWL.Descriptor.Presentation.unit_encode line 194
  52. def OAI.VariableWL.Descriptor.Presentation.fixed line 195
  53. def OAI.VariableWL.Descriptor.Presentation.optionEquiv line 200
  54. def OAI.VariableWL.Descriptor.Presentation.option line 205
  55. theorem OAI.VariableWL.Descriptor.Presentation.option_none line 207
  56. theorem OAI.VariableWL.Descriptor.Presentation.option_some line 208
  57. structure OAI.VariableWL.CircuitCatalog.Data line 214
  58. def OAI.VariableWL.CircuitCatalog.Data.gates line 237
  59. def OAI.VariableWL.CircuitCatalog.Data.edgeCode line 238
  60. def OAI.VariableWL.CircuitCatalog.Data.affine line 239
  61. def OAI.VariableWL.CircuitCatalog.real line 273
  62. def OAI.VariableWL.CircuitCatalog.comparison line 275
  63. structure OAI.VariableWL.CircuitCatalog.Good line 277
  64. theorem OAI.VariableWL.CircuitCatalog.edge_first line 302
  65. theorem OAI.VariableWL.CircuitCatalog.edge_second line 304
  66. theorem OAI.VariableWL.CircuitCatalog.edge_third line 308
  67. theorem OAI.VariableWL.CircuitCatalog.output_form line 313
  68. theorem OAI.VariableWL.CircuitCatalog.affine_good line 321
  69. theorem OAI.VariableWL.BlockCatalog.Data.ext_fields line 398
  70. theorem OAI.VariableWL.AffineCatalog.Data.ext_fields line 405