OAI/Computability/BinPacking/Machines/MachineKeepDecisionTyped.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.MachineKeepDecision.frame line 12
  2. theorem OAI.BinPackingGap.MachineKeepDecision.frame_length line 16
  3. def OAI.BinPackingGap.MachineKeepDecision.inputBits line 22
  4. def OAI.BinPackingGap.MachineKeepDecision.outputBits line 24
  5. def OAI.BinPackingGap.MachineKeepDecision.keep line 26
  6. theorem OAI.BinPackingGap.MachineKeepDecision.inputBits_length line 29
  7. inductive OAI.BinPackingGap.MachineKeepDecision.ExtraTape line 33
  8. abbrev OAI.BinPackingGap.MachineKeepDecision.ExtraTape.enumList line 37
  9. theorem OAI.BinPackingGap.MachineKeepDecision.ExtraTape.enumList_getElem?_ctorIdx_eq line 39
  10. theorem OAI.BinPackingGap.MachineKeepDecision.ExtraTape.enumList_nodup line 43
  11. instance OAI.BinPackingGap.MachineKeepDecision.(instance at line 45) line 45
  12. inductive OAI.BinPackingGap.MachineKeepDecision.Phase line 49
  13. abbrev OAI.BinPackingGap.MachineKeepDecision.Phase.enumList line 53
  14. theorem OAI.BinPackingGap.MachineKeepDecision.Phase.enumList_getElem?_ctorIdx_eq line 55
  15. theorem OAI.BinPackingGap.MachineKeepDecision.Phase.enumList_nodup line 59
  16. instance OAI.BinPackingGap.MachineKeepDecision.(instance at line 61) line 61
  17. abbrev OAI.BinPackingGap.MachineKeepDecision.Tape line 65
  18. abbrev OAI.BinPackingGap.MachineKeepDecision.Symbols line 66
  19. abbrev OAI.BinPackingGap.MachineKeepDecision.Label line 68
  20. abbrev OAI.BinPackingGap.MachineKeepDecision.State line 69
  21. def OAI.BinPackingGap.MachineKeepDecision.extraTapes line 71
  22. def OAI.BinPackingGap.MachineKeepDecision.auxProgram line 76
  23. def OAI.BinPackingGap.MachineKeepDecision.program line 92
  24. def OAI.BinPackingGap.MachineKeepDecision.machine line 96
  25. def OAI.BinPackingGap.MachineKeepDecision.inputTapes line 115
  26. theorem OAI.BinPackingGap.MachineKeepDecision.inputTapes_input line 119
  27. theorem OAI.BinPackingGap.MachineKeepDecision.inputTapes_saved line 123
  28. def OAI.BinPackingGap.MachineKeepDecision.inputConfig line 126
  29. def OAI.BinPackingGap.MachineKeepDecision.embedded line 130
  30. def OAI.BinPackingGap.MachineKeepDecision.returnTapes line 135
  31. def OAI.BinPackingGap.MachineKeepDecision.returnConfig line 139
  32. theorem OAI.BinPackingGap.MachineKeepDecision.inputTapes_update_input line 143
  33. theorem OAI.BinPackingGap.MachineKeepDecision.inputTapes_update_saved line 155
  34. def OAI.BinPackingGap.MachineKeepDecision.oneStep line 164
  35. theorem OAI.BinPackingGap.MachineKeepDecision.parseStep_digit line 172
  36. theorem OAI.BinPackingGap.MachineKeepDecision.parseStep_end line 182
  37. theorem OAI.BinPackingGap.MachineKeepDecision.parseTrace line 193
  38. theorem OAI.BinPackingGap.MachineKeepDecision.inputConfig_init line 213
  39. def OAI.BinPackingGap.MachineKeepDecision.decisionExecution line 225
  40. theorem OAI.BinPackingGap.MachineKeepDecision.returnTransfer_tapes line 235
  41. def OAI.BinPackingGap.MachineKeepDecision.returnTransfer line 246
  42. theorem OAI.BinPackingGap.MachineKeepDecision.finish_tapes line 260
  43. theorem OAI.BinPackingGap.MachineKeepDecision.finishStep line 275
  44. def OAI.BinPackingGap.MachineKeepDecision.outputsInTime line 290
  45. theorem OAI.BinPackingGap.MachineKeepDecision.machine_finiteAlphabet line 326
  46. def OAI.BinPackingGap.MachineKeepDecision.computation line 333
  47. theorem OAI.BinPackingGap.MachineKeepDecision.computation_finiteAlphabet line 356
  48. def OAI.BinPackingGap.MachineKeepDecision.typedInputBits line 367
  49. def OAI.BinPackingGap.MachineKeepDecision.typedOutputBits line 370
  50. def OAI.BinPackingGap.MachineKeepDecision.typedKeep line 373
  51. def OAI.BinPackingGap.MachineKeepDecision.computationWithSavedCodec line 376
  52. theorem OAI.BinPackingGap.MachineKeepDecision.computationWithSavedCodec_finiteAlphabet line 388