OAI/Computability/WeisfeilerLeman/Transducer.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.tm_integer_lower line 10
  2. theorem OAI.WLTime.tm_real_lower line 46
  3. def OAI.WLTime.TypedStack.Code.casesList line 65
  4. theorem OAI.WLTime.TypedStack.Code.casesList_exec line 68
  5. def OAI.WLTime.TypedStack.Code.casesAll line 80
  6. theorem OAI.WLTime.TypedStack.Code.casesAll_exec line 82
  7. instance OAI.WLTime.instFintypeMove line 90
  8. abbrev OAI.WLTime.TMTransducer.Letter line 96
  9. abbrev OAI.WLTime.TMTransducer.Reg line 97
  10. def OAI.WLTime.TMTransducer.stateReg line 98
  11. def OAI.WLTime.TMTransducer.historyReg line 99
  12. def OAI.WLTime.TMTransducer.symbolDecode line 100
  13. def OAI.WLTime.TMTransducer.stateDecode line 103
  14. def OAI.WLTime.TMTransducer.store line 106
  15. abbrev OAI.WLTime.TMTransducer.Key line 109
  16. def OAI.WLTime.TMTransducer.select line 110
  17. def OAI.WLTime.TMTransducer.live line 112
  18. def OAI.WLTime.TMTransducer.stepBody line 114
  19. def OAI.WLTime.TMTransducer.step line 118
  20. def OAI.WLTime.TMTransducer.runCode line 120
  21. theorem OAI.WLTime.TMTransducer.select_store line 122
  22. theorem OAI.WLTime.TMTransducer.body_exec line 130
  23. def OAI.WLTime.TMTransducer.stepFactor line 154
  24. theorem OAI.WLTime.TMTransducer.step_exec line 155
  25. theorem OAI.WLTime.TMTransducer.run_exec line 178
  26. def OAI.WLTime.Move.inverse line 221
  27. theorem OAI.WLTime.Move.inverse_displacement line 222
  28. def OAI.WLTime.TapePair.move line 226
  29. theorem OAI.WLTime.TapePair.contents_move line 227
  30. def OAI.WLTime.TMTransducer.zeroTape line 237
  31. def OAI.WLTime.TMTransducer.historyDecode line 238
  32. def OAI.WLTime.TMTransducer.rewindKey line 241
  33. def OAI.WLTime.TMTransducer.rewindBody line 243
  34. def OAI.WLTime.TMTransducer.rewindStep line 246
  35. def OAI.WLTime.TMTransducer.rewindCode line 248
  36. def OAI.WLTime.TMTransducer.moveOrigin line 250
  37. def OAI.WLTime.TMTransducer.rewindTapes line 252
  38. theorem OAI.WLTime.TMTransducer.rewindBody_exec line 256
  39. def OAI.WLTime.TMTransducer.rewindFactor line 272
  40. theorem OAI.WLTime.TMTransducer.rewindStep_exec line 273
  41. theorem OAI.WLTime.TMTransducer.rewind_exec line 289
  42. theorem OAI.WLTime.TMTransducer.rewind_contents line 302
  43. theorem OAI.WLTime.TMTransducer.rewind_absolute line 313
  44. def OAI.WLTime.TypedStack.Code.takeN line 323
  45. def OAI.WLTime.TypedStack.Code.readN line 326
  46. theorem OAI.WLTime.TypedStack.Code.takeN_exec line 327
  47. theorem OAI.WLTime.TypedStack.Code.takeN_size line 364
  48. theorem OAI.WLTime.TMTransducer.output_prefix line 373
  49. def OAI.WLTime.TypedStack.Code.mass line 390
  50. theorem OAI.WLTime.TypedStack.Code.mass_update line 391
  51. theorem OAI.WLTime.TypedStack.Code.mass_exec line 400
  52. def OAI.WLTime.TypedStack.Code.clearList line 413
  53. def OAI.WLTime.TypedStack.Code.cleared line 416
  54. theorem OAI.WLTime.TypedStack.Code.clearList_exec line 418
  55. theorem OAI.WLTime.TypedStack.Code.clearList_cost line 440