OAI/Computability/MinUncut/Graphs/CanonicalPathGraph.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.PathRealization.number line 12
  2. lemma OAI.MinUncut.PathRealization.number_left line 15
  3. lemma OAI.MinUncut.PathRealization.number_right line 16
  4. def OAI.MinUncut.PathRealization.canonicalAdjacent line 20
  5. lemma OAI.MinUncut.PathRealization.canonicalAdjacent_symmetric line 27
  6. lemma OAI.MinUncut.PathRealization.canonicalAdjacent_loopless line 36
  7. def OAI.MinUncut.PathRealization.canonicalOutput line 42
  8. lemma OAI.MinUncut.PathRealization.canonicalOutput_eq line 50
  9. lemma OAI.MinUncut.PathRealization.canonicalOutput_yes line 68
  10. lemma OAI.MinUncut.PathRealization.canonicalOutput_no line 73
  11. def OAI.MinUncut.Costed.GraphRegisters.demandOffset line 84
  12. def OAI.MinUncut.Costed.GraphRegisters.demandLeft line 85
  13. def OAI.MinUncut.Costed.GraphRegisters.demandRight line 86
  14. def OAI.MinUncut.Costed.GraphRegisters.demandEqual line 87
  15. def OAI.MinUncut.Costed.GraphRegisters.privateBase line 88
  16. def OAI.MinUncut.Costed.GraphRegisters.localEdge line 89
  17. def OAI.MinUncut.Costed.GraphRegisters.accumulatedEdge line 97
  18. lemma OAI.MinUncut.Costed.GraphRegisters.localEdge_le_one line 99
  19. lemma OAI.MinUncut.Costed.GraphRegisters.accumulatedEdge_le_one line 107
  20. def OAI.MinUncut.Costed.GraphRegisters.cumulative line 112
  21. lemma OAI.MinUncut.Costed.GraphRegisters.cumulative_le_one line 115
  22. def OAI.MinUncut.Costed.GraphRegisters.adjacencyProgram line 120
  23. structure OAI.MinUncut.Costed.GraphRegisters.RenderState line 128
  24. def OAI.MinUncut.Costed.GraphRegisters.RenderState.encode line 138
  25. def OAI.MinUncut.Costed.GraphRegisters.parseState line 141
  26. lemma OAI.MinUncut.Costed.GraphRegisters.parse_encode line 145
  27. def OAI.MinUncut.Costed.GraphRegisters.RenderState.tick line 148
  28. def OAI.MinUncut.Costed.GraphRegisters.renderTick line 154
  29. lemma OAI.MinUncut.Costed.GraphRegisters.renderTick_encode line 156
  30. def OAI.MinUncut.Costed.GraphRegisters.nextRow line 159
  31. def OAI.MinUncut.Costed.GraphRegisters.nextCol line 160
  32. def OAI.MinUncut.Costed.GraphRegisters.nextCount line 161
  33. def OAI.MinUncut.Costed.GraphRegisters.normalizeProgram line 163
  34. def OAI.MinUncut.Costed.GraphRegisters.tickProgram line 167
  35. lemma OAI.MinUncut.Costed.GraphRegisters.parse_encode_magnitude line 174
  36. lemma OAI.MinUncut.Costed.GraphRegisters.tick_V line 183
  37. lemma OAI.MinUncut.Costed.GraphRegisters.tick_magnitude line 185
  38. lemma OAI.MinUncut.Costed.GraphRegisters.tick_iter_V line 194
  39. lemma OAI.MinUncut.Costed.GraphRegisters.tick_iter_magnitude line 199
  40. lemma OAI.MinUncut.Costed.GraphRegisters.renderTick_iter_encode line 210
  41. lemma OAI.MinUncut.Costed.GraphRegisters.renderTick_iter_succ line 216
  42. lemma OAI.MinUncut.Costed.GraphRegisters.renderTick_iter_bound line 220
  43. def OAI.MinUncut.Costed.GraphRegisters.renderLoop line 244
  44. def OAI.MinUncut.Costed.GraphRegisters.queryState line 250
  45. def OAI.MinUncut.Costed.GraphRegisters.endpoint line 253
  46. instance OAI.MinUncut.Costed.GraphRegisters.(instance at line 254) line 254
  47. def OAI.MinUncut.Costed.GraphRegisters.localAdj line 256
  48. instance OAI.MinUncut.Costed.GraphRegisters.(instance at line 260) line 260
  49. def OAI.MinUncut.Costed.GraphRegisters.rawLocal line 263
  50. instance OAI.MinUncut.Costed.GraphRegisters.(instance at line 266) line 266
  51. lemma OAI.MinUncut.Costed.GraphRegisters.data_address line 269
  52. lemma OAI.MinUncut.Costed.GraphRegisters.bit_or line 279
  53. lemma OAI.MinUncut.Costed.GraphRegisters.localEdge_query line 284
  54. lemma OAI.MinUncut.Costed.GraphRegisters.cumulative_query line 309
  55. def OAI.MinUncut.Costed.GraphRegisters.rawCell line 331
  56. def OAI.MinUncut.Costed.GraphRegisters.rawRow line 334
  57. def OAI.MinUncut.Costed.GraphRegisters.rawTable line 337
  58. lemma OAI.MinUncut.Costed.GraphRegisters.tick_query line 340
  59. lemma OAI.MinUncut.Costed.GraphRegisters.tick_row line 348
  60. lemma OAI.MinUncut.Costed.GraphRegisters.tick_rows line 361
  61. lemma OAI.MinUncut.Costed.GraphRegisters.tick_table line 380
  62. def OAI.MinUncut.PathRealization.Demand.map line 397
  63. lemma OAI.MinUncut.PathRealization.failure_map line 400
  64. def OAI.MinUncut.PathRealization.listFailure line 403
  65. lemma OAI.MinUncut.PathRealization.listFailure_eq line 406
  66. def OAI.MinUncut.PathRealization.demandList line 413
  67. lemma OAI.MinUncut.PathRealization.sum_enumerate line 416
  68. lemma OAI.MinUncut.PathRealization.listFailure_demandList line 421
  69. lemma OAI.MinUncut.PathRealization.length_demandList line 438
  70. def OAI.MinUncut.PathRealization.extendAssignment line 445
  71. lemma OAI.MinUncut.PathRealization.extendAssignment_apply line 450
  72. lemma OAI.MinUncut.PathRealization.mapDemand_extend line 455