OAI/Computability/WeisfeilerLeman/Frames.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.Compression.BlockDrawing.address_exists line 11
  2. theorem OAI.WLTime.Compression.BlockDrawing.addresses_agree line 35
  3. abbrev OAI.WLTime.Compression.TypeNode line 59
  4. abbrev OAI.WLTime.Compression.TypeLink line 60
  5. def OAI.WLTime.Compression.linkLeft line 62
  6. def OAI.WLTime.Compression.linkRight line 66
  7. def OAI.WLTime.Compression.typeDepth line 70
  8. def OAI.WLTime.Compression.realRoot line 74
  9. def OAI.WLTime.Compression.linkDepth line 78
  10. theorem OAI.WLTime.Compression.link_depth_near line 81
  11. theorem OAI.WLTime.Compression.link_midpoint_depth line 88
  12. theorem OAI.WLTime.Compression.link_root_preserved line 97
  13. theorem OAI.WLTime.Compression.exists_missing_depth line 105
  14. def OAI.WLTime.Compression.typeSupportGraph line 118
  15. theorem OAI.WLTime.Compression.equal_cut_of_near line 129
  16. theorem OAI.WLTime.Compression.support_cut_preserved line 132
  17. theorem OAI.WLTime.Compression.support_walk_cut line 144
  18. theorem OAI.WLTime.Compression.reachable_real_depth line 152
  19. theorem OAI.WLTime.Compression.support_edge_root_of_real line 167
  20. theorem OAI.WLTime.Compression.support_walk_root_of_real line 187
  21. theorem OAI.WLTime.Compression.support_unique_real line 198
  22. def OAI.WLTime.Compression.nodeWire line 204
  23. theorem OAI.WLTime.Compression.link_internal_same_wire line 208
  24. theorem OAI.WLTime.Compression.support_edge_wire line 220
  25. theorem OAI.WLTime.Compression.support_walk_wire line 230
  26. def OAI.WLTime.Compression.extendCoordinate line 244
  27. theorem OAI.WLTime.Compression.extendCoordinate_apply line 248
  28. def OAI.WLTime.Compression.typeFrame line 253
  29. def OAI.WLTime.Compression.linkMatch line 258
  30. theorem OAI.WLTime.Compression.frame_match line 262
  31. theorem OAI.WLTime.Compression.support_link_reachable line 276
  32. def OAI.WLTime.Compression.HasReal line 283
  33. theorem OAI.WLTime.Compression.hasReal_of_reachable line 287
  34. theorem OAI.WLTime.Compression.hasReal_inl line 295
  35. def OAI.WLTime.Compression.supportFrame line 298
  36. theorem OAI.WLTime.Compression.supportFrame_match line 304
  37. theorem OAI.WLTime.Compression.support_graph_mono line 328
  38. theorem OAI.WLTime.Compression.hasReal_mono line 339
  39. theorem OAI.WLTime.Compression.realRoot_eq_of_reachable line 344
  40. theorem OAI.WLTime.Compression.root_eq_on_real_component line 350
  41. theorem OAI.WLTime.Compression.frame_eq_on_internal_edge line 359
  42. theorem OAI.WLTime.Compression.frame_eq_on_rootfree_walk line 376