OAI/Combinatorics/VariableWL/Circuit.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Circuit.Gate line 11
  2. abbrev OAI.VariableWL.Circuit.Port line 12
  3. abbrev OAI.VariableWL.Circuit.target line 14
  4. abbrev OAI.VariableWL.Circuit.Value line 18
  5. def OAI.VariableWL.Circuit.output line 22
  6. def OAI.VariableWL.Circuit.input line 26
  7. structure OAI.VariableWL.Circuit.System line 31
  8. inductive OAI.VariableWL.Circuit.System.TrueGate line 42
  9. def OAI.VariableWL.Circuit.System.TruePort line 50
  10. theorem OAI.VariableWL.Circuit.System.true_scalar_iff line 52
  11. theorem OAI.VariableWL.Circuit.System.true_and_iff line 62
  12. structure OAI.VariableWL.Circuit.System.Witness line 71
  13. theorem OAI.VariableWL.Circuit.System.Witness.propagates line 85
  14. theorem OAI.VariableWL.Circuit.System.Witness.true_zero line 91
  15. theorem OAI.VariableWL.Circuit.System.Witness.tests_false line 115
  16. def OAI.VariableWL.Circuit.System.gateSets line 125
  17. theorem OAI.VariableWL.Circuit.System.gateSets_nonempty line 129
  18. theorem OAI.VariableWL.Circuit.System.gateSets_output_scalar line 138
  19. theorem OAI.VariableWL.Circuit.System.gateSets_output_and line 142
  20. theorem OAI.VariableWL.Circuit.System.gateSets_source line 147
  21. theorem OAI.VariableWL.Circuit.System.gateSets_input_true line 154
  22. def OAI.VariableWL.Circuit.System.bufferSets line 171
  23. theorem OAI.VariableWL.Circuit.System.bufferSets_nonempty line 175
  24. theorem OAI.VariableWL.Circuit.System.bufferSets_first line 182
  25. theorem OAI.VariableWL.Circuit.System.bufferSets_second line 191
  26. theorem OAI.VariableWL.Circuit.System.bufferSets_last line 201
  27. def OAI.VariableWL.Circuit.System.witness line 209
  28. theorem OAI.VariableWL.Circuit.System.consistent_iff line 223
  29. abbrev OAI.VariableWL.Circuit.dimension line 234
  30. def OAI.VariableWL.Circuit.scalarVector line 238
  31. def OAI.VariableWL.Circuit.pairVector line 239
  32. def OAI.VariableWL.Circuit.vector line 241
  33. def OAI.VariableWL.Circuit.scalarValue line 246
  34. def OAI.VariableWL.Circuit.pairValue line 247
  35. def OAI.VariableWL.Circuit.value line 249
  36. theorem OAI.VariableWL.Circuit.scalarValue_vector line 254
  37. theorem OAI.VariableWL.Circuit.pairValue_vector line 255
  38. theorem OAI.VariableWL.Circuit.scalarVector_value line 257
  39. theorem OAI.VariableWL.Circuit.pairVector_value line 260
  40. theorem OAI.VariableWL.Circuit.value_vector line 264
  41. theorem OAI.VariableWL.Circuit.vector_value line 266
  42. def OAI.VariableWL.Circuit.outputLinear line 269
  43. def OAI.VariableWL.Circuit.inputLinear line 274
  44. theorem OAI.VariableWL.Circuit.outputLinear_vector line 280
  45. theorem OAI.VariableWL.Circuit.inputLinear_vector line 283
  46. theorem OAI.VariableWL.Circuit.output_value line 288
  47. theorem OAI.VariableWL.Circuit.input_value line 291
  48. def OAI.VariableWL.Circuit.gateAt line 295
  49. def OAI.VariableWL.Circuit.portAt line 299
  50. theorem OAI.VariableWL.Circuit.target_portAt line 303
  51. structure OAI.VariableWL.Circuit.Description line 307
  52. def OAI.VariableWL.Circuit.Description.Allowed line 323
  53. def OAI.VariableWL.Circuit.Description.RequestAllowed line 324
  54. def OAI.VariableWL.Circuit.Description.mapAddress line 325
  55. abbrev OAI.VariableWL.Circuit.Description.ExpandedEdges line 327
  56. def OAI.VariableWL.Circuit.Description.requests line 329
  57. def OAI.VariableWL.Circuit.Description.Terminal line 332
  58. abbrev OAI.VariableWL.Circuit.Description.expanded line 335
  59. abbrev OAI.VariableWL.Circuit.Description.Real line 342
  60. abbrev OAI.VariableWL.Circuit.Description.Comparison line 343
  61. abbrev OAI.VariableWL.Circuit.Description.realDimension line 345
  62. abbrev OAI.VariableWL.Circuit.Description.comparisonSource line 350
  63. abbrev OAI.VariableWL.Circuit.Description.comparisonTarget line 356
  64. abbrev OAI.VariableWL.Circuit.Description.consistency line 362
  65. theorem OAI.VariableWL.Circuit.Description.real_count line 406
  66. theorem OAI.VariableWL.Circuit.Description.comparison_count line 411