OAI/Combinatorics/VariableWL/PrefixWiring.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.SubcubicRealization.PortGraph.ofSlots line 11
  2. theorem OAI.VariableWL.SubcubicRealization.PortGraph.ofSlots_graph line 23
  3. def OAI.VariableWL.SubcubicRealization.PortGraph.sigma line 29
  4. def OAI.VariableWL.SubcubicRealization.PortGraph.union line 51
  5. def OAI.VariableWL.PrefixParts.Data.ports line 70
  6. theorem OAI.VariableWL.PrefixParts.Data.ports_graph line 73
  7. abbrev OAI.VariableWL.PrefixParts.Channel line 83
  8. structure OAI.VariableWL.PrefixParts.Wiring line 85
  9. abbrev OAI.VariableWL.PrefixParts.Wiring.Vertex line 93
  10. abbrev OAI.VariableWL.PrefixParts.Wiring.Root line 95
  11. abbrev OAI.VariableWL.PrefixParts.Wiring.RootLabel line 97
  12. def OAI.VariableWL.PrefixParts.Wiring.rootVertex line 99
  13. theorem OAI.VariableWL.PrefixParts.Wiring.rootVertex_injective line 103
  14. def OAI.VariableWL.PrefixParts.Wiring.pad line 114
  15. theorem OAI.VariableWL.PrefixParts.Wiring.pad_injective line 116
  16. theorem OAI.VariableWL.PrefixParts.Wiring.pad_add line 121
  17. def OAI.VariableWL.PrefixParts.Wiring.internal line 126
  18. def OAI.VariableWL.PrefixParts.Wiring.rootPorts line 129
  19. theorem OAI.VariableWL.PrefixParts.Wiring.internal_root_disjoint line 159
  20. def OAI.VariableWL.PrefixParts.Wiring.anchor line 172
  21. def OAI.VariableWL.PrefixParts.Wiring.anchorPorts line 174
  22. theorem OAI.VariableWL.PrefixParts.Wiring.internal_anchor_disjoint line 210
  23. theorem OAI.VariableWL.PrefixParts.Wiring.root_anchor_disjoint line 223
  24. def OAI.VariableWL.PrefixParts.Wiring.ports line 232
  25. abbrev OAI.VariableWL.PrefixParts.Data.SortTag line 245
  26. def OAI.VariableWL.PrefixParts.Data.sort line 248
  27. theorem OAI.VariableWL.PrefixParts.Data.sort_translation line 253
  28. theorem OAI.VariableWL.PrefixParts.Data.ports_translation line 257
  29. theorem OAI.VariableWL.PrefixParts.Data.localPorts_anchor line 276
  30. abbrev OAI.VariableWL.PrefixParts.Wiring.SortTag line 286
  31. def OAI.VariableWL.PrefixParts.Wiring.sort line 289
  32. def OAI.VariableWL.PrefixParts.Wiring.color line 291
  33. theorem OAI.VariableWL.PrefixParts.Wiring.color_pos line 295
  34. theorem OAI.VariableWL.PrefixParts.Wiring.color_eq_iff line 298
  35. def OAI.VariableWL.PrefixParts.Wiring.vertexTranslation line 303
  36. theorem OAI.VariableWL.PrefixParts.Wiring.vertexTranslation_apply line 307
  37. theorem OAI.VariableWL.PrefixParts.Wiring.color_translation line 311
  38. def OAI.VariableWL.PrefixParts.Wiring.localPorts line 316
  39. def OAI.VariableWL.PrefixParts.Wiring.incidenceTranslation line 319
  40. theorem OAI.VariableWL.PrefixParts.Wiring.root_truncated line 328
  41. def OAI.VariableWL.PrefixParts.Wiring.rootTranslation line 335
  42. theorem OAI.VariableWL.PrefixParts.Wiring.translate_root_incidence line 343
  43. def OAI.VariableWL.PrefixParts.Wiring.rootShift line 349
  44. def OAI.VariableWL.PrefixParts.Wiring.Compatible line 352
  45. theorem OAI.VariableWL.PrefixParts.Wiring.rootTranslation_bits line 356
  46. theorem OAI.VariableWL.PrefixParts.Wiring.internal_translation line 370
  47. def OAI.VariableWL.PrefixParts.Wiring.CompatiblePair line 386
  48. theorem OAI.VariableWL.PrefixParts.Wiring.compatiblePair_symm line 390
  49. theorem OAI.VariableWL.PrefixParts.Wiring.rootPorts_translation line 398
  50. theorem OAI.VariableWL.PrefixParts.Wiring.translate_anchor_incidence line 429
  51. theorem OAI.VariableWL.PrefixParts.Wiring.anchorPorts_translation line 433
  52. theorem OAI.VariableWL.PrefixParts.Wiring.ports_translation line 454
  53. def OAI.VariableWL.PrefixParts.Wiring.partHom line 469
  54. theorem OAI.VariableWL.PrefixParts.Wiring.part_reachable line 474
  55. theorem OAI.VariableWL.PrefixParts.Wiring.anchor_adj line 479
  56. theorem OAI.VariableWL.PrefixParts.Wiring.connected line 486
  57. abbrev OAI.VariableWL.PrefixParts.Wiring.UncoloredVertex line 509
  58. def OAI.VariableWL.PrefixParts.Wiring.uncolored line 511
  59. theorem OAI.VariableWL.PrefixParts.Wiring.uncolored_connected line 514
  60. theorem OAI.VariableWL.PrefixParts.Wiring.uncolored_subcubic line 517
  61. def OAI.VariableWL.PrefixParts.Wiring.uncoloredTranslation line 520
  62. theorem OAI.VariableWL.PrefixParts.Wiring.uncoloredTranslation_adj line 524
  63. theorem OAI.VariableWL.PrefixParts.Wiring.equal_order line 532