OAI/Computability/WeisfeilerLeman/Enumeration.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.WLTime.Compression.NameTag line 9
  2. def OAI.WLTime.Compression.ReadoutName.tag line 16
  3. theorem OAI.WLTime.Compression.link_endpoints_ne line 21
  4. abbrev OAI.WLTime.Compression.ConsistencyData.Tag line 36
  5. abbrev OAI.WLTime.Compression.ConsistencyData.TagValue line 37
  6. abbrev OAI.WLTime.Compression.ConsistencyData.TagValues line 40
  7. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 42) line 42
  8. instance OAI.WLTime.Compression.ConsistencyData.(instance at line 44) line 44
  9. def OAI.WLTime.Compression.ConsistencyData.tagRead line 47
  10. theorem OAI.WLTime.Compression.ConsistencyData.tag_injective_on_footprint line 51
  11. def OAI.WLTime.Compression.ConsistencyData.TagSupported line 70
  12. theorem OAI.WLTime.Compression.ConsistencyData.tagRead_injective line 74
  13. def OAI.WLTime.Compression.ConsistencyData.toTag line 87
  14. def OAI.WLTime.Compression.ConsistencyData.encodeTags line 91
  15. theorem OAI.WLTime.Compression.ConsistencyData.encodeTags_supported line 99
  16. theorem OAI.WLTime.Compression.ConsistencyData.encodeTags_apply line 108
  17. theorem OAI.WLTime.Compression.ConsistencyData.tagRead_encodeTags line 122
  18. def OAI.WLTime.Compression.ConsistencyData.tagSpaceEquiv line 135
  19. abbrev OAI.WLTime.Compression.ConsistencyData.Descriptor line 146
  20. def OAI.WLTime.Compression.ConsistencyData.DescriptorValid line 148
  21. def OAI.WLTime.Compression.ConsistencyData.descriptorEquiv line 152
  22. theorem OAI.WLTime.Marking.degree_detect_base_spaced line 176
  23. theorem OAI.WLTime.Marking.wins_bases_spaced line 207
  24. abbrev OAI.WLTime.Marking.Slot line 260
  25. def OAI.WLTime.Marking.slotAdj line 264
  26. def OAI.WLTime.Marking.rawAdj line 270
  27. def OAI.WLTime.Marking.rawGraph line 278
  28. theorem OAI.WLTime.Marking.raw_diameter line 295
  29. def OAI.WLTime.Marking.rawEquiv line 300
  30. theorem OAI.WLTime.Marking.rawEquiv_adj line 346
  31. def OAI.WLTime.Marking.decodeSlots line 382
  32. theorem OAI.WLTime.Marking.decodeSlots_complete line 393
  33. theorem OAI.WLTime.Marking.raw_holes_eq line 452