OAI/Computability/WeisfeilerLeman/MatrixWriter.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WLTime.Enumeration.Listing line 9
  2. def OAI.WLTime.Enumeration.Listing.equiv line 14
  3. theorem OAI.WLTime.Enumeration.Listing.equiv_apply line 17
  4. def OAI.WLTime.Enumeration.ofFintype line 19
  5. def OAI.WLTime.Enumeration.fin line 23
  6. def OAI.WLTime.Enumeration.Listing.prod line 25
  7. def OAI.WLTime.Enumeration.Listing.sum line 41
  8. def OAI.WLTime.Enumeration.Listing.option line 56
  9. theorem OAI.WLTime.Enumeration.fin_values line 66
  10. theorem OAI.WLTime.Enumeration.range_flatMap line 71
  11. theorem OAI.WLTime.Enumeration.Listing.length_eq_card line 75
  12. abbrev OAI.WLTime.Enumeration.Vertex line 83
  13. def OAI.WLTime.Enumeration.rectangle line 85
  14. theorem OAI.WLTime.Enumeration.rectangle_flatMap line 88
  15. def OAI.WLTime.Enumeration.writer line 97
  16. theorem OAI.WLTime.Enumeration.writer_eval line 103
  17. theorem OAI.WLTime.Enumeration.writer_safe line 119
  18. theorem OAI.WLTime.Enumeration.writer_depth line 134
  19. def OAI.WLTime.Enumeration.Listing.matrix line 152
  20. theorem OAI.WLTime.Enumeration.Listing.ofFn_eq_map line 155
  21. theorem OAI.WLTime.Enumeration.Listing.matrix_bits line 160
  22. instance OAI.WLTime.OneTape.Symbolic.valuesFintype line 184
  23. abbrev OAI.WLTime.OneTape.Symbolic.RawVertex line 194
  24. def OAI.WLTime.OneTape.Symbolic.listing line 198
  25. inductive OAI.WLTime.OneTape.Symbolic.Location line 202
  26. def OAI.WLTime.OneTape.Symbolic.Location.rename line 208
  27. inductive OAI.WLTime.OneTape.Symbolic.Represents line 215
  28. theorem OAI.WLTime.OneTape.Symbolic.Represents.rename line 224
  29. def OAI.WLTime.OneTape.Symbolic.adjacency line 235
  30. theorem OAI.WLTime.OneTape.Symbolic.adjacency_correct line 243
  31. abbrev OAI.WLTime.OneTape.Symbolic.up3 line 255
  32. def OAI.WLTime.OneTape.Symbolic.slotLocation line 257
  33. def OAI.WLTime.OneTape.Symbolic.columns line 260
  34. theorem OAI.WLTime.OneTape.Symbolic.columns_eval line 266
  35. def OAI.WLTime.OneTape.Symbolic.matrixWriter line 298
  36. theorem OAI.WLTime.OneTape.Symbolic.matrixWriter_eval line 304
  37. theorem OAI.WLTime.OneTape.Symbolic.columns_depth line 326
  38. theorem OAI.WLTime.OneTape.Symbolic.matrixWriter_depth line 330
  39. theorem OAI.WLTime.OneTape.Symbolic.coefficient_eq line 340
  40. theorem OAI.WLTime.OneTape.Symbolic.tagIndex_le line 343
  41. theorem OAI.WLTime.OneTape.Symbolic.countExpr_bounded line 348
  42. theorem OAI.WLTime.OneTape.Symbolic.sameRect_bounded line 392
  43. theorem OAI.WLTime.OneTape.Symbolic.slotPredicate_bounded line 397
  44. def OAI.WLTime.OneTape.Symbolic.Location.Bounded line 428
  45. theorem OAI.WLTime.OneTape.Symbolic.Location.rename_bounded line 432
  46. theorem OAI.WLTime.OneTape.Symbolic.adjacency_bounded line 438
  47. theorem OAI.WLTime.OneTape.Symbolic.columns_safe line 450
  48. theorem OAI.WLTime.OneTape.Symbolic.matrixWriter_safe line 481