OAI/Computability/BinPacking/Search/ExtensionShapeMachine.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.ExtensionShapeMachine.Kind line 11
  2. abbrev OAI.BinPackingGap.ExtensionShapeMachine.Kind.enumList line 16
  3. theorem OAI.BinPackingGap.ExtensionShapeMachine.Kind.enumList_getElem?_ctorIdx_eq line 18
  4. theorem OAI.BinPackingGap.ExtensionShapeMachine.Kind.enumList_nodup line 22
  5. instance OAI.BinPackingGap.ExtensionShapeMachine.(instance at line 24) line 24
  6. inductive OAI.BinPackingGap.ExtensionShapeMachine.Continuation line 28
  7. abbrev OAI.BinPackingGap.ExtensionShapeMachine.Continuation.enumList line 36
  8. theorem OAI.BinPackingGap.ExtensionShapeMachine.Continuation.enumList_getElem?_ctorIdx_eq line 39
  9. theorem OAI.BinPackingGap.ExtensionShapeMachine.Continuation.enumList_nodup line 43
  10. instance OAI.BinPackingGap.ExtensionShapeMachine.(instance at line 45) line 45
  11. inductive OAI.BinPackingGap.ExtensionShapeMachine.Mode line 49
  12. def OAI.BinPackingGap.ExtensionShapeMachine.start line 60
  13. def OAI.BinPackingGap.ExtensionShapeMachine.afterName line 64
  14. def OAI.BinPackingGap.ExtensionShapeMachine.nextMode line 71
  15. def OAI.BinPackingGap.ExtensionShapeMachine.run line 86
  16. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_reject line 90
  17. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_done_iff line 95
  18. theorem OAI.BinPackingGap.ExtensionShapeMachine.finalDigit_true_iff line 100
  19. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_frame line 116
  20. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_name line 130
  21. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_items line 136
  22. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_fixed line 145
  23. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_assignments line 157
  24. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_extension line 165
  25. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_assignmentBits line 171
  26. theorem OAI.BinPackingGap.ExtensionShapeMachine.frame_inverse line 175
  27. theorem OAI.BinPackingGap.ExtensionShapeMachine.name_inverse line 205
  28. theorem OAI.BinPackingGap.ExtensionShapeMachine.fixed_inverse_aux line 214
  29. theorem OAI.BinPackingGap.ExtensionShapeMachine.assignments_inverse_aux line 253
  30. theorem OAI.BinPackingGap.ExtensionShapeMachine.items_inverse_aux line 279
  31. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_extension_iff line 310
  32. theorem OAI.BinPackingGap.ExtensionShapeMachine.run_assignments_iff line 321
  33. def OAI.BinPackingGap.ExtensionShapeMachine.accepts line 329
  34. def OAI.BinPackingGap.ExtensionShapeMachine.decodeAccepts line 332
  35. theorem OAI.BinPackingGap.ExtensionShapeMachine.accepts_eq_decode line 336
  36. inductive OAI.BinPackingGap.ExtensionShapeMachine.Label line 375
  37. abbrev OAI.BinPackingGap.ExtensionShapeMachine.Label.enumList line 381
  38. theorem OAI.BinPackingGap.ExtensionShapeMachine.Label.enumList_getElem?_ctorIdx_eq line 383
  39. theorem OAI.BinPackingGap.ExtensionShapeMachine.Label.enumList_nodup line 387
  40. instance OAI.BinPackingGap.ExtensionShapeMachine.(instance at line 389) line 389
  41. abbrev OAI.BinPackingGap.ExtensionShapeMachine.Alphabet line 393
  42. abbrev OAI.BinPackingGap.ExtensionShapeMachine.State line 394
  43. def OAI.BinPackingGap.ExtensionShapeMachine.instruction line 396
  44. abbrev OAI.BinPackingGap.ExtensionShapeMachine.machine line 409
  45. def OAI.BinPackingGap.ExtensionShapeMachine.tapes line 420
  46. def OAI.BinPackingGap.ExtensionShapeMachine.cfg line 425
  47. theorem OAI.BinPackingGap.ExtensionShapeMachine.tapes_input line 429
  48. theorem OAI.BinPackingGap.ExtensionShapeMachine.tapes_output line 432
  49. theorem OAI.BinPackingGap.ExtensionShapeMachine.tapes_saved line 435
  50. theorem OAI.BinPackingGap.ExtensionShapeMachine.update_input line 438
  51. theorem OAI.BinPackingGap.ExtensionShapeMachine.update_output line 444
  52. theorem OAI.BinPackingGap.ExtensionShapeMachine.update_saved line 450
  53. theorem OAI.BinPackingGap.ExtensionShapeMachine.step_scan_empty line 456
  54. theorem OAI.BinPackingGap.ExtensionShapeMachine.step_scan_cons line 464
  55. theorem OAI.BinPackingGap.ExtensionShapeMachine.scanTrace line 472
  56. theorem OAI.BinPackingGap.ExtensionShapeMachine.restoreTrace line 489
  57. theorem OAI.BinPackingGap.ExtensionShapeMachine.step_finish line 501
  58. theorem OAI.BinPackingGap.ExtensionShapeMachine.joinTrace line 509
  59. theorem OAI.BinPackingGap.ExtensionShapeMachine.rawTrace line 513
  60. theorem OAI.BinPackingGap.ExtensionShapeMachine.initList_eq line 530
  61. theorem OAI.BinPackingGap.ExtensionShapeMachine.haltList_eq line 537
  62. theorem OAI.BinPackingGap.ExtensionShapeMachine.totalTrace line 544
  63. def OAI.BinPackingGap.ExtensionShapeMachine.outputsInTime line 551
  64. def OAI.BinPackingGap.ExtensionShapeMachine.computableInPolyTime line 558
  65. theorem OAI.BinPackingGap.ExtensionShapeMachine.machine_finiteAlphabet line 572
  66. theorem OAI.BinPackingGap.ExtensionShapeMachine.computation_finiteAlphabet line 577