OAI/Computability/WeisfeilerLeman/GraphFormula.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.OneTape.inputPredicate_bounded line 10
  2. def OAI.WLTime.Compression.FormalName.Bounded line 20
  3. theorem OAI.WLTime.Compression.FormalName.equal_bounded line 22
  4. theorem OAI.WLTime.Compression.ConsistencyData.blockPredicate_bounded line 30
  5. theorem OAI.WLTime.Compression.ConsistencyData.validPredicate_bounded line 40
  6. theorem OAI.WLTime.Compression.ConsistencyData.formalFootprint_bounded line 46
  7. theorem OAI.WLTime.Compression.ConsistencyData.overlapPredicate_bounded line 67
  8. theorem OAI.WLTime.Compression.ConsistencyData.agreePredicate_bounded line 77
  9. theorem OAI.WLTime.Compression.ConsistencyData.adjacencyPredicate_bounded line 87
  10. abbrev OAI.WLTime.OneTape.Symbolic.Node line 104
  11. abbrev OAI.WLTime.OneTape.Symbolic.Edge line 105
  12. def OAI.WLTime.OneTape.Symbolic.schema line 108
  13. def OAI.WLTime.OneTape.Symbolic.instanceData line 112
  14. def OAI.WLTime.OneTape.Symbolic.domain line 116
  15. def OAI.WLTime.OneTape.Symbolic.coord line 123
  16. theorem OAI.WLTime.OneTape.Symbolic.domain_correct line 127
  17. theorem OAI.WLTime.OneTape.Symbolic.coord_correct line 139
  18. abbrev OAI.WLTime.OneTape.Symbolic.BlockTag line 147
  19. abbrev OAI.WLTime.OneTape.Symbolic.Values line 148
  20. theorem OAI.WLTime.OneTape.Symbolic.fixedLegal_iff line 150
  21. def OAI.WLTime.OneTape.Symbolic.validity line 158
  22. def OAI.WLTime.OneTape.Symbolic.adjacent line 162
  23. theorem OAI.WLTime.OneTape.Symbolic.validity_correct line 166
  24. theorem OAI.WLTime.OneTape.Symbolic.adjacent_correct line 177
  25. theorem OAI.WLTime.OneTape.Symbolic.domain_bounded line 195
  26. theorem OAI.WLTime.OneTape.Symbolic.coord_bounded line 209
  27. theorem OAI.WLTime.OneTape.Symbolic.validity_bounded line 217
  28. theorem OAI.WLTime.OneTape.Symbolic.adjacent_bounded line 225
  29. abbrev OAI.WLTime.Compression.ConsistencyData.Rect line 242
  30. def OAI.WLTime.Compression.ConsistencyData.rectEquiv line 244
  31. def OAI.WLTime.Compression.ConsistencyData.RectValid line 252
  32. def OAI.WLTime.Compression.ConsistencyData.rectVertexEquiv line 255
  33. def OAI.WLTime.Compression.ConsistencyData.mixedCode line 262
  34. theorem OAI.WLTime.Compression.ConsistencyData.mixedCode_pos line 265
  35. theorem OAI.WLTime.Compression.ConsistencyData.mixedCode_le line 268
  36. theorem OAI.WLTime.Compression.ConsistencyData.mixedCode_injective line 275
  37. def OAI.WLTime.Compression.ConsistencyData.rawCode line 291
  38. theorem OAI.WLTime.Compression.ConsistencyData.rawCode_make line 295
  39. theorem OAI.WLTime.Compression.ConsistencyData.rawCode_injective line 298
  40. theorem OAI.WLTime.Compression.ConsistencyData.rawCode_pos line 306
  41. theorem OAI.WLTime.Compression.ConsistencyData.rawCode_le line 309
  42. def OAI.WLTime.Compression.ConsistencyData.rectCoefficient line 313
  43. theorem OAI.WLTime.Compression.ConsistencyData.rect_card line 316
  44. theorem OAI.WLTime.Compression.ConsistencyData.tagValues_card_pos line 320
  45. theorem OAI.WLTime.Compression.ConsistencyData.rectangle_code_le line 324
  46. theorem OAI.WLTime.Compression.ConsistencyData.card_bases_le_rectangle line 332
  47. def OAI.WLTime.Compression.ConsistencyData.spacedCount line 337
  48. def OAI.WLTime.Compression.ConsistencyData.slotLimit line 340
  49. theorem OAI.WLTime.Compression.ConsistencyData.spacedCount_lt_limit line 342
  50. def OAI.WLTime.Compression.ConsistencyData.slots line 348
  51. theorem OAI.WLTime.Compression.ConsistencyData.slots_complete line 352
  52. def OAI.WLTime.Compression.ConsistencyData.rectangularGraph line 358
  53. theorem OAI.WLTime.Pebble.wins_transport_iff line 363
  54. theorem OAI.WLTime.Marking.raw_wins_iff line 383
  55. theorem OAI.WLTime.Compression.ConsistencyData.spaced_wins_iff_ac line 403
  56. theorem OAI.WLTime.Compression.ConsistencyData.rectangular_wins_iff_ac line 422
  57. theorem OAI.WLTime.Compression.ConsistencyData.rectangular_card line 435