OAI/Computability/MinUncut/Estimates/TM2Costed.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Costed.Steps line 11
  2. theorem OAI.MinUncut.Costed.steps_zero line 14
  3. theorem OAI.MinUncut.Costed.steps_one line 18
  4. theorem OAI.MinUncut.Costed.steps_head line 21
  5. theorem OAI.MinUncut.Costed.steps_trans line 25
  6. def OAI.MinUncut.Costed.steps_timed line 30
  7. def OAI.MinUncut.Costed.Within line 34
  8. theorem OAI.MinUncut.Costed.Steps.within line 37
  9. theorem OAI.MinUncut.Costed.Within.mono line 40
  10. theorem OAI.MinUncut.Costed.Within.trans line 45
  11. theorem OAI.MinUncut.Costed.Within.head line 51
  12. theorem OAI.MinUncut.Costed.within_one line 56
  13. theorem OAI.Turing.PartrecToTM2.move_steps line 67
  14. theorem OAI.Turing.PartrecToTM2.clear_steps line 95
  15. theorem OAI.Turing.PartrecToTM2.unrev_steps line 118
  16. theorem OAI.Turing.PartrecToTM2.copy_steps line 123
  17. theorem OAI.Turing.PartrecToTM2.move₂_steps line 138
  18. theorem OAI.Turing.PartrecToTM2.head_main_steps line 164
  19. theorem OAI.Turing.PartrecToTM2.head_stack_time line 187
  20. theorem OAI.Turing.PartrecToTM2.succ_time line 225
  21. theorem OAI.Turing.PartrecToTM2.pred_time line 269
  22. inductive OAI.MinUncut.Costed.WordTransducer.Tape line 335
  23. abbrev OAI.MinUncut.Costed.WordTransducer.Tape.enumList line 337
  24. theorem OAI.MinUncut.Costed.WordTransducer.Tape.enumList_getElem?_ctorIdx_eq line 339
  25. theorem OAI.MinUncut.Costed.WordTransducer.Tape.enumList_nodup line 343
  26. instance OAI.MinUncut.Costed.WordTransducer.(instance at line 345) line 345
  27. def OAI.MinUncut.Costed.WordTransducer.Alphabet line 349
  28. def OAI.MinUncut.Costed.WordTransducer.tapes line 353
  29. lemma OAI.MinUncut.Costed.WordTransducer.update_input line 359
  30. lemma OAI.MinUncut.Costed.WordTransducer.update_work line 363
  31. lemma OAI.MinUncut.Costed.WordTransducer.update_output line 366
  32. def OAI.MinUncut.Costed.WordTransducer.pushWord line 370
  33. lemma OAI.MinUncut.Costed.WordTransducer.pushWord_aux line 375
  34. inductive OAI.MinUncut.Costed.WordTransducer.Label line 386
  35. abbrev OAI.MinUncut.Costed.WordTransducer.State line 388
  36. def OAI.MinUncut.Costed.WordTransducer.output line 390
  37. def OAI.MinUncut.Costed.WordTransducer.program line 394
  38. def OAI.MinUncut.Costed.WordTransducer.machine line 408
  39. lemma OAI.MinUncut.Costed.WordTransducer.finiteAlphabet line 421
  40. lemma OAI.MinUncut.Costed.WordTransducer.reverse_steps line 428
  41. lemma OAI.MinUncut.Costed.WordTransducer.emit_steps line 452
  42. lemma OAI.MinUncut.Costed.WordTransducer.read_steps line 469
  43. def OAI.MinUncut.Costed.WordTransducer.outputsInTime line 488
  44. theorem OAI.MinUncut.Costed.head_tail_length line 518
  45. theorem OAI.MinUncut.Costed.head_length line 522
  46. theorem OAI.MinUncut.Costed.tail_length line 525
  47. theorem OAI.MinUncut.Costed.save_steps line 528
  48. theorem OAI.MinUncut.Costed.swap_steps line 541
  49. theorem OAI.MinUncut.Costed.fix_done_steps line 564
  50. theorem OAI.MinUncut.Costed.fix_more_steps line 577
  51. theorem OAI.MinUncut.Costed.CodeRun.compiled line 597
  52. def OAI.MinUncut.Costed.FiniteControl.stmt line 660
  53. def OAI.MinUncut.Costed.FiniteControl.project line 670
  54. lemma OAI.MinUncut.Costed.FiniteControl.project_injective line 674
  55. lemma OAI.MinUncut.Costed.FiniteControl.project_aux line 683
  56. def OAI.MinUncut.Costed.FiniteControl.program line 697
  57. lemma OAI.MinUncut.Costed.FiniteControl.project_step line 701
  58. lemma OAI.MinUncut.Costed.FiniteControl.projected_iterate line 709