OAI/Computability/BinPacking/Search/SearchInitialShapeMachine.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.SearchInitialShapeMachine.Continuation line 11
  2. abbrev OAI.BinPackingGap.SearchInitialShapeMachine.Continuation.enumList line 16
  3. theorem OAI.BinPackingGap.SearchInitialShapeMachine.Continuation.enumList_getElem?_ctorIdx_eq line 18
  4. theorem OAI.BinPackingGap.SearchInitialShapeMachine.Continuation.enumList_nodup line 22
  5. instance OAI.BinPackingGap.SearchInitialShapeMachine.(instance at line 24) line 24
  6. inductive OAI.BinPackingGap.SearchInitialShapeMachine.Mode line 28
  7. def OAI.BinPackingGap.SearchInitialShapeMachine.afterName line 36
  8. def OAI.BinPackingGap.SearchInitialShapeMachine.nextMode line 40
  9. def OAI.BinPackingGap.SearchInitialShapeMachine.run line 49
  10. theorem OAI.BinPackingGap.SearchInitialShapeMachine.run_reject line 53
  11. theorem OAI.BinPackingGap.SearchInitialShapeMachine.run_done_iff line 58
  12. theorem OAI.BinPackingGap.SearchInitialShapeMachine.finalDigit_true_iff line 63
  13. theorem OAI.BinPackingGap.SearchInitialShapeMachine.run_frame line 79
  14. theorem OAI.BinPackingGap.SearchInitialShapeMachine.run_name line 93
  15. theorem OAI.BinPackingGap.SearchInitialShapeMachine.run_items line 99
  16. theorem OAI.BinPackingGap.SearchInitialShapeMachine.run_rawInstanceBits line 108
  17. theorem OAI.BinPackingGap.SearchInitialShapeMachine.frame_inverse line 112
  18. theorem OAI.BinPackingGap.SearchInitialShapeMachine.name_inverse line 142
  19. theorem OAI.BinPackingGap.SearchInitialShapeMachine.items_inverse_aux line 151
  20. theorem OAI.BinPackingGap.SearchInitialShapeMachine.run_items_iff line 182
  21. def OAI.BinPackingGap.SearchInitialShapeMachine.accepts line 190
  22. def OAI.BinPackingGap.SearchInitialShapeMachine.decodeAccepts line 192
  23. theorem OAI.BinPackingGap.SearchInitialShapeMachine.accepts_eq_decode line 194
  24. inductive OAI.BinPackingGap.SearchInitialShapeMachine.Label line 216
  25. abbrev OAI.BinPackingGap.SearchInitialShapeMachine.Label.enumList line 222
  26. theorem OAI.BinPackingGap.SearchInitialShapeMachine.Label.enumList_getElem?_ctorIdx_eq line 224
  27. theorem OAI.BinPackingGap.SearchInitialShapeMachine.Label.enumList_nodup line 228
  28. instance OAI.BinPackingGap.SearchInitialShapeMachine.(instance at line 230) line 230
  29. abbrev OAI.BinPackingGap.SearchInitialShapeMachine.Alphabet line 234
  30. abbrev OAI.BinPackingGap.SearchInitialShapeMachine.State line 235
  31. def OAI.BinPackingGap.SearchInitialShapeMachine.instruction line 237
  32. abbrev OAI.BinPackingGap.SearchInitialShapeMachine.machine line 250
  33. def OAI.BinPackingGap.SearchInitialShapeMachine.tapes line 261
  34. def OAI.BinPackingGap.SearchInitialShapeMachine.cfg line 266
  35. theorem OAI.BinPackingGap.SearchInitialShapeMachine.tapes_input line 270
  36. theorem OAI.BinPackingGap.SearchInitialShapeMachine.tapes_output line 273
  37. theorem OAI.BinPackingGap.SearchInitialShapeMachine.tapes_saved line 276
  38. theorem OAI.BinPackingGap.SearchInitialShapeMachine.update_input line 279
  39. theorem OAI.BinPackingGap.SearchInitialShapeMachine.update_output line 285
  40. theorem OAI.BinPackingGap.SearchInitialShapeMachine.update_saved line 291
  41. theorem OAI.BinPackingGap.SearchInitialShapeMachine.step_scan_empty line 297
  42. theorem OAI.BinPackingGap.SearchInitialShapeMachine.step_scan_cons line 305
  43. theorem OAI.BinPackingGap.SearchInitialShapeMachine.scanTrace line 313
  44. theorem OAI.BinPackingGap.SearchInitialShapeMachine.restoreTrace line 330
  45. theorem OAI.BinPackingGap.SearchInitialShapeMachine.step_finish line 342
  46. theorem OAI.BinPackingGap.SearchInitialShapeMachine.joinTrace line 350
  47. theorem OAI.BinPackingGap.SearchInitialShapeMachine.rawTrace line 354
  48. theorem OAI.BinPackingGap.SearchInitialShapeMachine.initList_eq line 371
  49. theorem OAI.BinPackingGap.SearchInitialShapeMachine.haltList_eq line 378
  50. theorem OAI.BinPackingGap.SearchInitialShapeMachine.totalTrace line 385
  51. def OAI.BinPackingGap.SearchInitialShapeMachine.outputsInTime line 392
  52. def OAI.BinPackingGap.SearchInitialShapeMachine.computableInPolyTime line 399
  53. theorem OAI.BinPackingGap.SearchInitialShapeMachine.machine_finiteAlphabet line 413
  54. theorem OAI.BinPackingGap.SearchInitialShapeMachine.computation_finiteAlphabet line 418