OAI/Combinatorics/VariableWL/ProductCellular.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Circuit.ProductCellular.Address line 12
  2. def OAI.VariableWL.Circuit.ProductCellular.timeBits line 14
  3. def OAI.VariableWL.Circuit.ProductCellular.positionBits line 15
  4. def OAI.VariableWL.Circuit.ProductCellular.join line 16
  5. theorem OAI.VariableWL.Circuit.ProductCellular.join_left line 18
  6. theorem OAI.VariableWL.Circuit.ProductCellular.join_right line 20
  7. theorem OAI.VariableWL.Circuit.ProductCellular.join_addNat line 22
  8. theorem OAI.VariableWL.Circuit.ProductCellular.time_join line 25
  9. theorem OAI.VariableWL.Circuit.ProductCellular.position_join line 26
  10. theorem OAI.VariableWL.Circuit.ProductCellular.join_parts line 27
  11. theorem OAI.VariableWL.Circuit.ProductCellular.all_parts line 31
  12. abbrev OAI.VariableWL.Circuit.ProductCellular.Kind line 34
  13. abbrev OAI.VariableWL.Circuit.ProductCellular.Edge line 35
  14. def OAI.VariableWL.Circuit.ProductCellular.left line 37
  15. def OAI.VariableWL.Circuit.ProductCellular.center line 38
  16. def OAI.VariableWL.Circuit.ProductCellular.right line 39
  17. def OAI.VariableWL.Circuit.ProductCellular.same line 40
  18. def OAI.VariableWL.Circuit.ProductCellular.timeDomain line 42
  19. def OAI.VariableWL.Circuit.ProductCellular.positionDomain line 48
  20. def OAI.VariableWL.Circuit.ProductCellular.timeMap line 54
  21. def OAI.VariableWL.Circuit.ProductCellular.positionMap line 60
  22. def OAI.VariableWL.Circuit.ProductCellular.source line 66
  23. def OAI.VariableWL.Circuit.ProductCellular.destination line 72
  24. theorem OAI.VariableWL.Circuit.ProductCellular.timeDomain_nonempty line 79
  25. theorem OAI.VariableWL.Circuit.ProductCellular.positionDomain_nonempty line 84
  26. theorem OAI.VariableWL.Circuit.ProductCellular.timeMap_injective line 89
  27. theorem OAI.VariableWL.Circuit.ProductCellular.positionMap_injective line 93
  28. structure OAI.VariableWL.Circuit.ProductCellular.Data line 97
  29. def OAI.VariableWL.Circuit.ProductCellular.Data.threshold line 106
  30. theorem OAI.VariableWL.Circuit.ProductCellular.Data.number_threshold line 107
  31. abbrev OAI.VariableWL.Circuit.ProductCellular.Data.Request line 111
  32. def OAI.VariableWL.Circuit.ProductCellular.Data.requestGate line 113
  33. def OAI.VariableWL.Circuit.ProductCellular.Data.requestTest line 118
  34. def OAI.VariableWL.Circuit.ProductCellular.Data.inputBits line 122
  35. theorem OAI.VariableWL.Circuit.ProductCellular.Data.number_inputBits line 123
  36. def OAI.VariableWL.Circuit.ProductCellular.Data.requestTimeDomain line 126
  37. def OAI.VariableWL.Circuit.ProductCellular.Data.requestPositionDomain line 129
  38. def OAI.VariableWL.Circuit.ProductCellular.Data.description line 134
  39. theorem OAI.VariableWL.Circuit.ProductCellular.Data.allowed_parts line 156
  40. theorem OAI.VariableWL.Circuit.ProductCellular.Data.time_mapAddress line 163
  41. theorem OAI.VariableWL.Circuit.ProductCellular.Data.position_mapAddress line 167
  42. theorem OAI.VariableWL.Circuit.ProductCellular.Data.request_parts line 172
  43. def OAI.VariableWL.Circuit.ProductCellular.Data.initial line 180
  44. theorem OAI.VariableWL.Circuit.ProductCellular.Data.seeds_exact line 182
  45. theorem OAI.VariableWL.Circuit.ProductCellular.Data.tests_exact line 226
  46. theorem OAI.VariableWL.Circuit.ProductCellular.Data.terminal line 249
  47. theorem OAI.VariableWL.Circuit.ProductCellular.schema_count line 267
  48. instance OAI.VariableWL.Circuit.ProductCellular.powTwoNeZero line 278
  49. def OAI.VariableWL.Circuit.ProductCellular.position line 280
  50. theorem OAI.VariableWL.Circuit.ProductCellular.address_ext line 282
  51. theorem OAI.VariableWL.Circuit.ProductCellular.position_index_join line 288
  52. theorem OAI.VariableWL.Circuit.ProductCellular.index_increment line 291
  53. theorem OAI.VariableWL.Circuit.ProductCellular.index_decrement line 296
  54. abbrev OAI.VariableWL.Circuit.ProductCellular.Data.system line 317
  55. def OAI.VariableWL.Circuit.ProductCellular.Data.cellular line 319
  56. abbrev OAI.VariableWL.Circuit.ProductCellular.Data.state line 326
  57. theorem OAI.VariableWL.Circuit.ProductCellular.Data.left_coordinates line 328
  58. theorem OAI.VariableWL.Circuit.ProductCellular.Data.center_coordinates line 342
  59. theorem OAI.VariableWL.Circuit.ProductCellular.Data.right_coordinates line 353
  60. theorem OAI.VariableWL.Circuit.ProductCellular.Data.same_allowed line 367
  61. theorem OAI.VariableWL.Circuit.ProductCellular.Data.same_map line 371
  62. def OAI.VariableWL.Circuit.ProductCellular.Data.gateMeaning line 377
  63. def OAI.VariableWL.Circuit.ProductCellular.Data.portMeaning line 385
  64. theorem OAI.VariableWL.Circuit.ProductCellular.Data.meaningful_edge line 395
  65. theorem OAI.VariableWL.Circuit.ProductCellular.Data.true_meaning line 438
  66. def OAI.VariableWL.Circuit.ProductCellular.previousTime line 468
  67. def OAI.VariableWL.Circuit.ProductCellular.backAddress line 470
  68. theorem OAI.VariableWL.Circuit.ProductCellular.number_previousTime line 473
  69. theorem OAI.VariableWL.Circuit.ProductCellular.time_backAddress line 475
  70. theorem OAI.VariableWL.Circuit.ProductCellular.position_backAddress line 478
  71. theorem OAI.VariableWL.Circuit.ProductCellular.previousTime_case line 481
  72. theorem OAI.VariableWL.Circuit.ProductCellular.Data.incoming_left line 493
  73. theorem OAI.VariableWL.Circuit.ProductCellular.Data.incoming_center line 517
  74. theorem OAI.VariableWL.Circuit.ProductCellular.Data.incoming_right line 541
  75. theorem OAI.VariableWL.Circuit.ProductCellular.Data.state_true line 565
  76. theorem OAI.VariableWL.Circuit.ProductCellular.Data.scalar_true_iff line 606
  77. theorem OAI.VariableWL.Circuit.ProductCellular.Data.true_test_iff line 612
  78. theorem OAI.VariableWL.Circuit.ProductCellular.Data.consistency_iff line 631