OAI/Computability/PerfectCompleteness/Machines/TupleInitializationMachine.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.TupleInitializationMachine.Alphabet line 15
  2. abbrev OAI.PerfectCompleteness.TupleInitializationMachine.State line 16
  3. def OAI.PerfectCompleteness.TupleInitializationMachine.clean line 18
  4. inductive OAI.PerfectCompleteness.TupleInitializationMachine.Label line 20
  5. abbrev OAI.PerfectCompleteness.TupleInitializationMachine.Label.enumList line 25
  6. theorem OAI.PerfectCompleteness.TupleInitializationMachine.Label.enumList_getElem?_ctorIdx_eq line 27
  7. theorem OAI.PerfectCompleteness.TupleInitializationMachine.Label.enumList_nodup line 31
  8. instance OAI.PerfectCompleteness.TupleInitializationMachine.(instance at line 33) line 33
  9. def OAI.PerfectCompleteness.TupleInitializationMachine.prefixOn line 37
  10. theorem OAI.PerfectCompleteness.TupleInitializationMachine.prefixOn_nil line 41
  11. theorem OAI.PerfectCompleteness.TupleInitializationMachine.prefixOn_comp line 46
  12. theorem OAI.PerfectCompleteness.TupleInitializationMachine.prefixOn_update line 53
  13. def OAI.PerfectCompleteness.TupleInitializationMachine.pushEach line 63
  14. theorem OAI.PerfectCompleteness.TupleInitializationMachine.stepAux_pushEach line 70
  15. theorem OAI.PerfectCompleteness.TupleInitializationMachine.pushEach_pushBound line 93
  16. def OAI.PerfectCompleteness.TupleInitializationMachine.finish line 103
  17. theorem OAI.PerfectCompleteness.TupleInitializationMachine.stepAux_finish line 107
  18. theorem OAI.PerfectCompleteness.TupleInitializationMachine.finish_pushBound line 113
  19. def OAI.PerfectCompleteness.TupleInitializationMachine.instruction line 117
  20. theorem OAI.PerfectCompleteness.TupleInitializationMachine.instruction_pushBound line 127
  21. theorem OAI.PerfectCompleteness.TupleInitializationMachine.scanStep_false line 142
  22. theorem OAI.PerfectCompleteness.TupleInitializationMachine.scanStep_true line 154
  23. theorem OAI.PerfectCompleteness.TupleInitializationMachine.scanTrace line 171
  24. theorem OAI.PerfectCompleteness.TupleInitializationMachine.seedStep line 202
  25. def OAI.PerfectCompleteness.TupleInitializationMachine.initializedTapes line 218
  26. theorem OAI.PerfectCompleteness.TupleInitializationMachine.joinTrace line 224
  27. theorem OAI.PerfectCompleteness.TupleInitializationMachine.initializeTrace line 228
  28. def OAI.PerfectCompleteness.TupleInitializationMachine.initializeInTime line 257
  29. theorem OAI.PerfectCompleteness.TupleInitializationMachine.initializedTapes_source line 273
  30. theorem OAI.PerfectCompleteness.TupleInitializationMachine.initializedTapes_current line 278
  31. theorem OAI.PerfectCompleteness.TupleInitializationMachine.initializedTapes_remaining line 285
  32. theorem OAI.PerfectCompleteness.TupleInitializationMachine.initializedTapes_frame line 291
  33. abbrev OAI.PerfectCompleteness.TupleInitializationMachine.Arena line 301
  34. def OAI.PerfectCompleteness.TupleInitializationMachine.currentDestinations line 303
  35. def OAI.PerfectCompleteness.TupleInitializationMachine.remainingDestinations line 306
  36. theorem OAI.PerfectCompleteness.TupleInitializationMachine.destinations_nodup line 309
  37. theorem OAI.PerfectCompleteness.TupleInitializationMachine.source_not_destination line 326
  38. def OAI.PerfectCompleteness.TupleInitializationMachine.arenaInstruction line 333
  39. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arenaInstruction_pushBound line 339
  40. def OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializedTapes line 348
  41. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializedTapes_source line 353
  42. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializedTapes_current line 358
  43. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializedTapes_remaining line 364
  44. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializedTapes_scratch line 371
  45. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializedTapes_output line 377
  46. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializedTapes_other line 383
  47. def OAI.PerfectCompleteness.TupleInitializationMachine.arenaInitializeInTime line 389
  48. theorem OAI.PerfectCompleteness.TupleInitializationMachine.arena_finite line 405