OAI/Computability/WeisfeilerLeman/Consistency.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.Compression.frameTransition line 10
  2. theorem OAI.WLTime.Compression.frameTransition_link line 13
  3. theorem OAI.WLTime.Compression.frameTransition_walk line 30
  4. structure OAI.WLTime.Compression.ConsistencyData line 53
  5. abbrev OAI.WLTime.Compression.ConsistencyData.RealValue line 68
  6. abbrev OAI.WLTime.Compression.ConsistencyData.Address line 69
  7. def OAI.WLTime.Compression.ConsistencyData.Allowed line 71
  8. def OAI.WLTime.Compression.ConsistencyData.transmit line 73
  9. def OAI.WLTime.Compression.ConsistencyData.affineSrc line 76
  10. def OAI.WLTime.Compression.ConsistencyData.affineDst line 78
  11. def OAI.WLTime.Compression.ConsistencyData.ArcConsistent line 80
  12. def OAI.WLTime.Compression.ConsistencyData.coordinatePerm line 87
  13. theorem OAI.WLTime.Compression.ConsistencyData.coordinatePerm_apply line 90
  14. def OAI.WLTime.Compression.ConsistencyData.permuteAddress line 94
  15. theorem OAI.WLTime.Compression.ConsistencyData.permuteAddress_eq line 96
  16. abbrev OAI.WLTime.Compression.ConsistencyData.Value line 101
  17. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 105) line 105
  18. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 108) line 108
  19. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 111) line 111
  20. def OAI.WLTime.Compression.ConsistencyData.transportForm line 114
  21. theorem OAI.WLTime.Compression.ConsistencyData.transportForm_apply line 117
  22. def OAI.WLTime.Compression.ConsistencyData.leftForm line 123
  23. def OAI.WLTime.Compression.ConsistencyData.rightForm line 132
  24. def OAI.WLTime.Compression.ConsistencyData.linkBias line 141
  25. def OAI.WLTime.Compression.ConsistencyData.ShiftSolves line 145
  26. def OAI.WLTime.Compression.ConsistencyData.rootedShift line 150
  27. theorem OAI.WLTime.Compression.ConsistencyData.rootedShift_link line 156
  28. def OAI.WLTime.Compression.ConsistencyData.interiorShift line 181
  29. theorem OAI.WLTime.Compression.ConsistencyData.interiorShift_link line 185
  30. theorem OAI.WLTime.Compression.ConsistencyData.leftForm_section_zero line 194
  31. theorem OAI.WLTime.Compression.ConsistencyData.leftForm_section_internal line 200
  32. theorem OAI.WLTime.Compression.ConsistencyData.rightForm_section_last line 207
  33. theorem OAI.WLTime.Compression.ConsistencyData.rightForm_section_internal line 213
  34. def OAI.WLTime.Compression.ConsistencyData.canonicalShift line 220
  35. theorem OAI.WLTime.Compression.ConsistencyData.canonicalShift_solves line 228
  36. theorem OAI.WLTime.Compression.ConsistencyData.rootedShift_congr line 264
  37. structure OAI.WLTime.Compression.ConsistencyData.ArcWitness line 279
  38. theorem OAI.WLTime.Compression.ConsistencyData.arcConsistent_iff line 286
  39. def OAI.WLTime.Compression.ConsistencyData.ArcWitness.internalSet line 294
  40. theorem OAI.WLTime.Compression.ConsistencyData.ArcWitness.internal_nonempty line 296
  41. theorem OAI.WLTime.Compression.ConsistencyData.ArcWitness.src_preimage line 299
  42. theorem OAI.WLTime.Compression.ConsistencyData.ArcWitness.dst_preimage line 302
  43. theorem OAI.WLTime.Compression.ConsistencyData.ArcWitness.src_mem_internal line 310
  44. theorem OAI.WLTime.Compression.ConsistencyData.ArcWitness.dst_mem_internal line 314
  45. def OAI.WLTime.Compression.ConsistencyData.scalarOf line 323
  46. theorem OAI.WLTime.Compression.ConsistencyData.scalar_eq_on_internal_link line 327
  47. theorem OAI.WLTime.Compression.ConsistencyData.scalar_eq_on_internal_edge line 341
  48. theorem OAI.WLTime.Compression.ConsistencyData.scalar_eq_on_rootfree_walk line 357
  49. structure OAI.WLTime.Compression.Corner line 376
  50. inductive OAI.WLTime.Compression.BlockName line 382
  51. def OAI.WLTime.Compression.BlockName.row line 390
  52. def OAI.WLTime.Compression.BlockName.low line 394
  53. def OAI.WLTime.Compression.BlockName.high line 400
  54. def OAI.WLTime.Compression.BlockName.drawing line 406
  55. def OAI.WLTime.Compression.BlockName.blockLinks line 415
  56. def OAI.WLTime.Compression.BlockName.links line 419
  57. theorem OAI.WLTime.Compression.BlockName.links_card line 422
  58. theorem OAI.WLTime.Compression.BlockName.square_link_mem line 429
  59. theorem OAI.WLTime.Compression.BlockName.links_mono line 433
  60. theorem OAI.WLTime.Compression.BlockName.drawing_aligned line 439
  61. def OAI.WLTime.Compression.BlockDrawing.restrict line 459
  62. theorem OAI.WLTime.Compression.BlockDrawing.graph_mono line 467
  63. theorem OAI.WLTime.Compression.BlockDrawing.map_reachable line 471