OAI/Computability/BinPacking/Search/SearchFinalizeMachine.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.SearchFinalizeMachine.Tape line 12
  2. abbrev OAI.BinPackingGap.SearchFinalizeMachine.Tape.enumList line 16
  3. theorem OAI.BinPackingGap.SearchFinalizeMachine.Tape.enumList_getElem?_ctorIdx_eq line 18
  4. theorem OAI.BinPackingGap.SearchFinalizeMachine.Tape.enumList_nodup line 22
  5. instance OAI.BinPackingGap.SearchFinalizeMachine.(instance at line 24) line 24
  6. inductive OAI.BinPackingGap.SearchFinalizeMachine.Label line 28
  7. abbrev OAI.BinPackingGap.SearchFinalizeMachine.Register line 36
  8. def OAI.BinPackingGap.SearchFinalizeMachine.tapes line 38
  9. theorem OAI.BinPackingGap.SearchFinalizeMachine.tapes_input line 45
  10. theorem OAI.BinPackingGap.SearchFinalizeMachine.tapes_binary line 46
  11. theorem OAI.BinPackingGap.SearchFinalizeMachine.tapes_scratch line 47
  12. theorem OAI.BinPackingGap.SearchFinalizeMachine.tapes_reversed line 48
  13. theorem OAI.BinPackingGap.SearchFinalizeMachine.tapes_output line 49
  14. theorem OAI.BinPackingGap.SearchFinalizeMachine.update_input line 51
  15. theorem OAI.BinPackingGap.SearchFinalizeMachine.update_binary line 55
  16. theorem OAI.BinPackingGap.SearchFinalizeMachine.update_scratch line 59
  17. theorem OAI.BinPackingGap.SearchFinalizeMachine.update_reversed line 63
  18. theorem OAI.BinPackingGap.SearchFinalizeMachine.update_output line 67
  19. def OAI.BinPackingGap.SearchFinalizeMachine.go line 71
  20. def OAI.BinPackingGap.SearchFinalizeMachine.reject line 74
  21. def OAI.BinPackingGap.SearchFinalizeMachine.skipUnary line 77
  22. def OAI.BinPackingGap.SearchFinalizeMachine.skipDigit line 81
  23. def OAI.BinPackingGap.SearchFinalizeMachine.code line 84
  24. def OAI.BinPackingGap.SearchFinalizeMachine.program line 118
  25. abbrev OAI.BinPackingGap.SearchFinalizeMachine.machine line 125
  26. def OAI.BinPackingGap.SearchFinalizeMachine.cfg line 127
  27. theorem OAI.BinPackingGap.SearchFinalizeMachine.oneStepTrace line 131
  28. theorem OAI.BinPackingGap.SearchFinalizeMachine.transferNext line 135
  29. theorem OAI.BinPackingGap.SearchFinalizeMachine.joinTrace line 139
  30. theorem OAI.BinPackingGap.SearchFinalizeMachine.skipStep line 143
  31. theorem OAI.BinPackingGap.SearchFinalizeMachine.digitStep line 152
  32. theorem OAI.BinPackingGap.SearchFinalizeMachine.skipUnaryTrace line 161
  33. theorem OAI.BinPackingGap.SearchFinalizeMachine.skipNameTrace line 177
  34. theorem OAI.BinPackingGap.SearchFinalizeMachine.skipItemsTrace line 200
  35. theorem OAI.BinPackingGap.SearchFinalizeMachine.emitBinaryStep_nil line 232
  36. theorem OAI.BinPackingGap.SearchFinalizeMachine.emitBinaryStep_cons line 239
  37. theorem OAI.BinPackingGap.SearchFinalizeMachine.emitBinaryTrace line 246
  38. theorem OAI.BinPackingGap.SearchFinalizeMachine.fixedStep line 260
  39. theorem OAI.BinPackingGap.SearchFinalizeMachine.optionStep line 267
  40. theorem OAI.BinPackingGap.SearchFinalizeMachine.nameStep line 275
  41. theorem OAI.BinPackingGap.SearchFinalizeMachine.nameDigitStep line 282
  42. theorem OAI.BinPackingGap.SearchFinalizeMachine.nameTrace line 289
  43. theorem OAI.BinPackingGap.SearchFinalizeMachine.fixedTrace line 310
  44. theorem OAI.BinPackingGap.SearchFinalizeMachine.convertTrace line 362
  45. theorem OAI.BinPackingGap.SearchFinalizeMachine.reverseTrace line 374
  46. theorem OAI.BinPackingGap.SearchFinalizeMachine.startDone line 383
  47. theorem OAI.BinPackingGap.SearchFinalizeMachine.startFalse line 390
  48. theorem OAI.BinPackingGap.SearchFinalizeMachine.startInvalid line 397
  49. def OAI.BinPackingGap.SearchFinalizeMachine.bodyBits line 404
  50. def OAI.BinPackingGap.SearchFinalizeMachine.resultBits line 408
  51. def OAI.BinPackingGap.SearchFinalizeMachine.doneSteps line 411
  52. theorem OAI.BinPackingGap.SearchFinalizeMachine.doneTrace line 416
  53. theorem OAI.BinPackingGap.SearchFinalizeMachine.labelsBits_le line 460
  54. theorem OAI.BinPackingGap.SearchFinalizeMachine.resultBits_length_le line 472
  55. def OAI.BinPackingGap.SearchFinalizeMachine.rawTime line 480
  56. theorem OAI.BinPackingGap.SearchFinalizeMachine.doneSteps_le line 482
  57. theorem OAI.BinPackingGap.SearchFinalizeMachine.init_eq line 497
  58. def OAI.BinPackingGap.SearchFinalizeMachine.rejectedRun line 504
  59. def OAI.BinPackingGap.SearchFinalizeMachine.rawRun line 526
  60. def OAI.BinPackingGap.SearchFinalizeMachine.cleanupTapes line 563
  61. theorem OAI.BinPackingGap.SearchFinalizeMachine.cleanup_complete line 565
  62. def OAI.BinPackingGap.SearchFinalizeMachine.computation line 568
  63. theorem OAI.BinPackingGap.SearchFinalizeMachine.finiteAlphabet line 573