OAI/Computability/WeisfeilerLeman/Sweep.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.StackMachine.Machine.Tops line 9
  2. abbrev OAI.WLTime.StackMachine.Machine.TrackSymbol line 10
  3. inductive OAI.WLTime.StackMachine.Machine.Purpose line 12
  4. inductive OAI.WLTime.StackMachine.Machine.SweepControl line 18
  5. abbrev OAI.WLTime.StackMachine.Machine.Control line 33
  6. abbrev OAI.WLTime.StackMachine.Machine.Purpose' line 34
  7. abbrev OAI.WLTime.StackMachine.Machine.TapeSymbol line 35
  8. abbrev OAI.WLTime.StackMachine.Machine.TapeState line 36
  9. abbrev OAI.WLTime.StackMachine.Machine.TapeConfig line 37
  10. def OAI.WLTime.StackMachine.Machine.symbolTracks line 39
  11. def OAI.WLTime.StackMachine.Machine.symbolBottom line 43
  12. def OAI.WLTime.StackMachine.Machine.trackSymbol line 47
  13. theorem OAI.WLTime.StackMachine.Machine.tracks_trackSymbol line 50
  14. theorem OAI.WLTime.StackMachine.Machine.bottom_trackSymbol line 57
  15. def OAI.WLTime.StackMachine.Machine.purposeStack line 64
  16. def OAI.WLTime.StackMachine.Machine.dispatch line 69
  17. def OAI.WLTime.StackMachine.Machine.finishPeek line 76
  18. def OAI.WLTime.StackMachine.Machine.sweepTransition line 81
  19. def OAI.WLTime.StackMachine.Machine.sweep line 115
  20. def OAI.WLTime.StackMachine.Machine.stackCell line 117
  21. def OAI.WLTime.StackMachine.Machine.storageTracks line 120
  22. def OAI.WLTime.StackMachine.Machine.storage line 123
  23. theorem OAI.WLTime.StackMachine.Machine.storage_bottom line 126
  24. theorem OAI.WLTime.StackMachine.Machine.storage_tracks line 129
  25. theorem OAI.WLTime.StackMachine.Machine.storage_origin line 132
  26. theorem OAI.WLTime.StackMachine.Machine.storageTracks_origin line 136
  27. theorem OAI.WLTime.StackMachine.Machine.storageTracks_index line 139
  28. theorem OAI.WLTime.StackMachine.Machine.stackCell_push line 145
  29. theorem OAI.WLTime.StackMachine.Machine.stackCell_pop line 159
  30. theorem OAI.WLTime.StackMachine.Machine.stackCell_none line 169
  31. theorem OAI.WLTime.StackMachine.Machine.stackCell_some line 172
  32. theorem OAI.WLTime.StackMachine.Machine.stackCell_last line 177
  33. def OAI.WLTime.StackMachine.Machine.located line 184
  34. def OAI.WLTime.StackMachine.Machine.sweepEmbed line 187
  35. theorem OAI.WLTime.StackMachine.Machine.storage_change line 191
  36. theorem OAI.WLTime.StackMachine.Machine.storage_push line 219
  37. theorem OAI.WLTime.StackMachine.Machine.storage_pop line 228
  38. theorem OAI.WLTime.StackMachine.Machine.seek_run line 242
  39. theorem OAI.WLTime.StackMachine.Machine.return_run line 259
  40. theorem OAI.WLTime.StackMachine.Machine.storage_top line 278
  41. theorem OAI.WLTime.StackMachine.Machine.peek_run line 289
  42. def OAI.WLTime.StackMachine.Machine.partialTops line 328
  43. def OAI.WLTime.StackMachine.Machine.topTuple line 331
  44. theorem OAI.WLTime.StackMachine.Machine.partialTops_update line 334
  45. theorem OAI.WLTime.StackMachine.Machine.partialTops_all line 345
  46. theorem OAI.WLTime.StackMachine.Machine.finish_next line 350
  47. def OAI.WLTime.StackMachine.Machine.dispatchLocation line 361
  48. theorem OAI.WLTime.StackMachine.Machine.finish_last line 368
  49. theorem OAI.WLTime.StackMachine.Machine.scan_prefix line 379
  50. theorem OAI.WLTime.StackMachine.Machine.collect_run line 402
  51. theorem OAI.WLTime.StackMachine.Machine.ret_run line 425
  52. theorem OAI.WLTime.StackMachine.Machine.push_run line 440
  53. theorem OAI.WLTime.StackMachine.Machine.pop_run line 470
  54. theorem OAI.WLTime.StackMachine.Machine.dispatch_run line 528
  55. theorem OAI.WLTime.StackMachine.Machine.sweep_simulate_step line 538