OAI/Computability/WeisfeilerLeman/SparseSearch.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.BitWords.value line 8
  2. theorem OAI.WLTime.BitWords.value_nil line 9
  3. theorem OAI.WLTime.BitWords.value_cons line 10
  4. theorem OAI.WLTime.BitWords.value_ofFn line 11
  5. theorem OAI.WLTime.BitWords.value_lt line 18
  6. theorem OAI.WLTime.BitWords.value_word line 21
  7. theorem OAI.WLTime.BitWords.testBit_value line 23
  8. theorem OAI.WLTime.BitWords.word_of_value line 30
  9. def OAI.WLTime.BitWords.inc line 36
  10. theorem OAI.WLTime.BitWords.length_inc line 40
  11. theorem OAI.WLTime.BitWords.inc_value line 44
  12. theorem OAI.WLTime.BitWords.word_injective line 56
  13. def OAI.WLTime.BitWords.carry line 63
  14. def OAI.WLTime.BitWords.rest line 66
  15. def OAI.WLTime.BitWords.raise line 69
  16. theorem OAI.WLTime.BitWords.carry_le line 72
  17. theorem OAI.WLTime.BitWords.inc_decompose line 76
  18. def OAI.WLTime.TypedStack.Code.carryCode line 84
  19. def OAI.WLTime.TypedStack.Code.raiseCode line 86
  20. def OAI.WLTime.TypedStack.Code.increment line 88
  21. theorem OAI.WLTime.TypedStack.Code.carryCode_exec line 90
  22. theorem OAI.WLTime.TypedStack.Code.raiseCode_exec line 130
  23. theorem OAI.WLTime.TypedStack.Code.increment_exec line 144
  24. abbrev OAI.WLTime.SparseMatch.Reg line 170
  25. def OAI.WLTime.SparseMatch.state line 171
  26. def OAI.WLTime.SparseMatch.body line 172
  27. def OAI.WLTime.SparseMatch.program line 175
  28. theorem OAI.WLTime.SparseMatch.body_exec line 178
  29. theorem OAI.WLTime.SparseMatch.program_exec line 195
  30. theorem OAI.WLTime.SparseMatch.program_size line 216
  31. abbrev OAI.WLTime.SparseTake.Reg line 223
  32. def OAI.WLTime.SparseTake.state line 224
  33. def OAI.WLTime.SparseTake.body line 225
  34. def OAI.WLTime.SparseTake.program line 228
  35. theorem OAI.WLTime.SparseTake.body_exec line 231
  36. theorem OAI.WLTime.SparseTake.program_exec line 245
  37. theorem OAI.WLTime.SparseTake.program_size line 253
  38. abbrev OAI.WLTime.SparseLookup.Reg line 261
  39. def OAI.WLTime.SparseLookup.state line 262
  40. def OAI.WLTime.SparseLookup.matchMap line 264
  41. def OAI.WLTime.SparseLookup.takeMap line 265
  42. theorem OAI.WLTime.SparseLookup.matchMap_inj line 266
  43. theorem OAI.WLTime.SparseLookup.takeMap_inj line 267
  44. def OAI.WLTime.SparseLookup.first line 268
  45. def OAI.WLTime.SparseLookup.finish line 271
  46. def OAI.WLTime.SparseLookup.one line 273
  47. theorem OAI.WLTime.SparseLookup.first_exec line 274
  48. theorem OAI.WLTime.SparseLookup.finish_exec line 316
  49. theorem OAI.WLTime.SparseLookup.one_exec line 348
  50. def OAI.WLTime.TypedStack.Code.pushList line 363
  51. theorem OAI.WLTime.TypedStack.Code.pushList_exec line 366
  52. theorem OAI.WLTime.TypedStack.Code.pushList_size line 375
  53. abbrev OAI.WLTime.SparseLookup.Entry line 382
  54. def OAI.WLTime.SparseLookup.flatten line 383
  55. def OAI.WLTime.SparseLookup.WellFormed line 384
  56. def OAI.WLTime.SparseLookup.consumed line 385
  57. def OAI.WLTime.SparseLookup.remaining line 388
  58. def OAI.WLTime.SparseLookup.found line 391
  59. theorem OAI.WLTime.SparseLookup.split_log line 394
  60. theorem OAI.WLTime.SparseLookup.flatten_append line 398
  61. theorem OAI.WLTime.SparseLookup.flatten_length line 399
  62. theorem OAI.WLTime.SparseLookup.consumed_length line 409
  63. theorem OAI.WLTime.SparseLookup.found_length line 413
  64. def OAI.WLTime.SparseLookup.keepGoing line 421
  65. def OAI.WLTime.SparseLookup.search line 422
  66. theorem OAI.WLTime.SparseLookup.search_exec line 423